eqtr.5 Show Code edit
thm (eqtr.5 () () (-> (z.= (bottom B) (z.0)) (-> (/\ (= A B) (= B C)) (= A C)))
B A eqtr.4
(-> (/\ (z.= (bottom B) (z.0)) (= A B)) (z.= (bottom A) (z.0)))
(bottom A) (z.0) (top C) z.muleq1
(-> (z.= (bottom A) (z.0)) (z.= (z.* (bottom A) (top C)) (z.* (z.0) (top C))))
## <d 'Multiply by 0 '>
(top C) z.mul0r
(z.= (z.* (z.0) (top C)) (z.0))
ZeqReplaceImp1Zeq1
(-> (z.= (bottom A) (z.0)) (z.= (z.* (bottom A) (top C)) (z.0)))
## </d 'Multiply by 0 '>
syl
(-> (/\ (z.= (bottom B) (z.0)) (= A B)) (z.= (z.* (bottom A) (top C)) (z.0)))
B C eqtr.4
(-> (/\ (z.= (bottom B) (z.0)) (= C B)) (z.= (bottom C) (z.0)))
## <d>
C B eqcom
(<-> (= C B) (= B C))
BiReplaceImp0An1
(-> (/\ (z.= (bottom B) (z.0)) (= B C)) (z.= (bottom C) (z.0)))
## </d>
(bottom C) (z.0) (top A) z.muleq2
(-> (z.= (bottom C) (z.0)) (z.= (z.* (top A) (bottom C)) (z.* (top A) (z.0))))
## <d 'Multiply by 0 '>
(top A) z.mul0
(z.= (z.* (top A) (z.0)) (z.0))
ZeqReplaceImp1Zeq1
(-> (z.= (bottom C) (z.0)) (z.= (z.* (top A) (bottom C)) (z.0)))
## </d 'Multiply by 0 '>
syl
(-> (/\ (z.= (bottom B) (z.0)) (= B C)) (z.= (z.* (top A) (bottom C)) (z.0)))
anim12i
(-> (/\ (/\ (z.= (bottom B) (z.0)) (= A B)) (/\ (z.= (bottom B) (z.0)) (= B C))) (/\ (z.= (z.* (bottom A) (top C)) (z.0)) (z.= (z.* (top A) (bottom C)) (z.0))))
(z.= (bottom B) (z.0)) (= A B) (z.= (bottom B) (z.0)) (= B C) an4
(<-> (/\ (/\ (z.= (bottom B) (z.0)) (= A B)) (/\ (z.= (bottom B) (z.0)) (= B C))) (/\ (/\ (z.= (bottom B) (z.0)) (z.= (bottom B) (z.0))) (/\ (= A B) (= B C))))
## <d 'Conjunction is Idempotent '>
(z.= (bottom B) (z.0)) anidm
(<-> (/\ (z.= (bottom B) (z.0)) (z.= (bottom B) (z.0))) (z.= (bottom B) (z.0)))
BiReplaceBi1An0
(<-> (/\ (/\ (z.= (bottom B) (z.0)) (= A B)) (/\ (z.= (bottom B) (z.0)) (= B C))) (/\ (z.= (bottom B) (z.0)) (/\ (= A B) (= B C))))
## </d 'Conjunction is Idempotent '>
sylbi2
(-> (/\ (z.= (bottom B) (z.0)) (/\ (= A B) (= B C))) (/\ (z.= (z.* (bottom A) (top C)) (z.0)) (z.= (z.* (top A) (bottom C)) (z.0))))
## <d 'Symmetric Property '>
(z.* (top A) (bottom C)) (z.0) z.eqcom
(<-> (z.= (z.* (top A) (bottom C)) (z.0)) (z.= (z.0) (z.* (top A) (bottom C))))
BiReplaceImp1An1
(-> (/\ (z.= (bottom B) (z.0)) (/\ (= A B) (= B C))) (/\ (z.= (z.* (bottom A) (top C)) (z.0)) (z.= (z.0) (z.* (top A) (bottom C)))))
## </d 'Symmetric Property '>
## <d 'Transitive Property '>
(z.* (bottom A) (top C)) (z.0) (z.* (top A) (bottom C)) z.eqtr
(-> (/\ (z.= (z.* (bottom A) (top C)) (z.0)) (z.= (z.0) (z.* (top A) (bottom C)))) (z.= (z.* (bottom A) (top C)) (z.* (top A) (bottom C))))
syl
(-> (/\ (z.= (bottom B) (z.0)) (/\ (= A B) (= B C))) (z.= (z.* (bottom A) (top C)) (z.* (top A) (bottom C))))
## </d 'Transitive Property '>
## <d 'Import-Export Theorem '>
(z.= (bottom B) (z.0)) (/\ (= A B) (= B C)) (z.= (z.* (bottom A) (top C)) (z.* (top A) (bottom C))) impexp
(<-> (-> (/\ (z.= (bottom B) (z.0)) (/\ (= A B) (= B C))) (z.= (z.* (bottom A) (top C)) (z.* (top A) (bottom C)))) (-> (z.= (bottom B) (z.0)) (-> (/\ (= A B) (= B C)) (z.= (z.* (bottom A) (top C)) (z.* (top A) (bottom C))))))
mpbi
(-> (z.= (bottom B) (z.0)) (-> (/\ (= A B) (= B C)) (z.= (z.* (bottom A) (top C)) (z.* (top A) (bottom C)))))
## </d 'Import-Export Theorem '>
A B C eqtr.0
(-> (/\ (= A B) (= B C)) (<-> (z.= (bottom A) (z.0)) (z.= (bottom C) (z.0))))
(z.= (bottom B) (z.0)) a1i
(-> (z.= (bottom B) (z.0)) (-> (/\ (= A B) (= B C)) (<-> (z.= (bottom A) (z.0)) (z.= (bottom C) (z.0)))))
jcad
(-> (z.= (bottom B) (z.0)) (-> (/\ (= A B) (= B C)) (/\ (z.= (z.* (bottom A) (top C)) (z.* (top A) (bottom C))) (<-> (z.= (bottom A) (z.0)) (z.= (bottom C) (z.0))))))
A C df-eq
(<-> (= A C) (/\ (z.= (z.* (top A) (bottom C)) (z.* (top C) (bottom A))) (<-> (z.= (bottom A) (z.0)) (z.= (bottom C) (z.0)))))
## <d 'Symmetric Property '>
(z.* (top A) (bottom C)) (z.* (top C) (bottom A)) z.eqcom
(<-> (z.= (z.* (top A) (bottom C)) (z.* (top C) (bottom A))) (z.= (z.* (top C) (bottom A)) (z.* (top A) (bottom C))))
BiReplaceBi1An0
(<-> (= A C) (/\ (z.= (z.* (top C) (bottom A)) (z.* (top A) (bottom C))) (<-> (z.= (bottom A) (z.0)) (z.= (bottom C) (z.0)))))
## </d 'Symmetric Property '>
## <d 'Commutative Property of Multiplication '>
(top C) (bottom A) z.mulcom
(z.= (z.* (top C) (bottom A)) (z.* (bottom A) (top C)))
ZeqReplaceBi1An0Zeq0
(<-> (= A C) (/\ (z.= (z.* (bottom A) (top C)) (z.* (top A) (bottom C))) (<-> (z.= (bottom A) (z.0)) (z.= (bottom C) (z.0)))))
## </d 'Commutative Property of Multiplication '>
bicomi
(<-> (/\ (z.= (z.* (bottom A) (top C)) (z.* (top A) (bottom C))) (<-> (z.= (bottom A) (z.0)) (z.= (bottom C) (z.0)))) (= A C))
BiReplaceImp1Imp1
(-> (z.= (bottom B) (z.0)) (-> (/\ (= A B) (= B C)) (= A C)))
)
edit