Metamath Proof Explorer

Theorem seglecgr12

Description: Substitution law for segment comparison under congruence. Biconditional version. (Contributed by Scott Fenton, 15-Oct-2013) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Assertion seglecgr12 
|- ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> ( ( <. A , B >. Cgr <. E , F >. /\ <. C , D >. Cgr <. G , H >. ) -> ( <. A , B >. Seg<_ <. C , D >. <-> <. E , F >. Seg<_ <. G , H >. ) ) )

Proof

Step Hyp Ref Expression
1 df-3an 
 |-  ( ( <. A , B >. Cgr <. E , F >. /\ <. C , D >. Cgr <. G , H >. /\ <. A , B >. Seg<_ <. C , D >. ) <-> ( ( <. A , B >. Cgr <. E , F >. /\ <. C , D >. Cgr <. G , H >. ) /\ <. A , B >. Seg<_ <. C , D >. ) )
2 seglecgr12im 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> ( ( <. A , B >. Cgr <. E , F >. /\ <. C , D >. Cgr <. G , H >. /\ <. A , B >. Seg<_ <. C , D >. ) -> <. E , F >. Seg<_ <. G , H >. ) )
3 1 2 syl5bir 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> ( ( ( <. A , B >. Cgr <. E , F >. /\ <. C , D >. Cgr <. G , H >. ) /\ <. A , B >. Seg<_ <. C , D >. ) -> <. E , F >. Seg<_ <. G , H >. ) )
4 3 expd 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> ( ( <. A , B >. Cgr <. E , F >. /\ <. C , D >. Cgr <. G , H >. ) -> ( <. A , B >. Seg<_ <. C , D >. -> <. E , F >. Seg<_ <. G , H >. ) ) )
5 simp11 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> N e. NN )
6 simp12 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> A e. ( EE ` N ) )
7 simp13 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> B e. ( EE ` N ) )
8 simp23 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> E e. ( EE ` N ) )
9 simp31 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> F e. ( EE ` N ) )
10 cgrcom 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) -> ( <. A , B >. Cgr <. E , F >. <-> <. E , F >. Cgr <. A , B >. ) )
11 5 6 7 8 9 10 syl122anc 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> ( <. A , B >. Cgr <. E , F >. <-> <. E , F >. Cgr <. A , B >. ) )
12 simp21 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> C e. ( EE ` N ) )
13 simp22 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> D e. ( EE ` N ) )
14 simp32 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> G e. ( EE ` N ) )
15 simp33 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> H e. ( EE ` N ) )
16 cgrcom 
 |-  ( ( N e. NN /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) /\ ( G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> ( <. C , D >. Cgr <. G , H >. <-> <. G , H >. Cgr <. C , D >. ) )
17 5 12 13 14 15 16 syl122anc 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> ( <. C , D >. Cgr <. G , H >. <-> <. G , H >. Cgr <. C , D >. ) )
18 11 17 anbi12d 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> ( ( <. A , B >. Cgr <. E , F >. /\ <. C , D >. Cgr <. G , H >. ) <-> ( <. E , F >. Cgr <. A , B >. /\ <. G , H >. Cgr <. C , D >. ) ) )
19 df-3an 
 |-  ( ( <. E , F >. Cgr <. A , B >. /\ <. G , H >. Cgr <. C , D >. /\ <. E , F >. Seg<_ <. G , H >. ) <-> ( ( <. E , F >. Cgr <. A , B >. /\ <. G , H >. Cgr <. C , D >. ) /\ <. E , F >. Seg<_ <. G , H >. ) )
20 seglecgr12im 
 |-  ( ( ( N e. NN /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) /\ ( G e. ( EE ` N ) /\ H e. ( EE ` N ) /\ A e. ( EE ` N ) ) /\ ( B e. ( EE ` N ) /\ C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> ( ( <. E , F >. Cgr <. A , B >. /\ <. G , H >. Cgr <. C , D >. /\ <. E , F >. Seg<_ <. G , H >. ) -> <. A , B >. Seg<_ <. C , D >. ) )
21 5 8 9 14 15 6 7 12 13 20 syl333anc 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> ( ( <. E , F >. Cgr <. A , B >. /\ <. G , H >. Cgr <. C , D >. /\ <. E , F >. Seg<_ <. G , H >. ) -> <. A , B >. Seg<_ <. C , D >. ) )
22 19 21 syl5bir 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> ( ( ( <. E , F >. Cgr <. A , B >. /\ <. G , H >. Cgr <. C , D >. ) /\ <. E , F >. Seg<_ <. G , H >. ) -> <. A , B >. Seg<_ <. C , D >. ) )
23 22 expd 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> ( ( <. E , F >. Cgr <. A , B >. /\ <. G , H >. Cgr <. C , D >. ) -> ( <. E , F >. Seg<_ <. G , H >. -> <. A , B >. Seg<_ <. C , D >. ) ) )
24 18 23 sylbid 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> ( ( <. A , B >. Cgr <. E , F >. /\ <. C , D >. Cgr <. G , H >. ) -> ( <. E , F >. Seg<_ <. G , H >. -> <. A , B >. Seg<_ <. C , D >. ) ) )
25 4 24 impbidd 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> ( ( <. A , B >. Cgr <. E , F >. /\ <. C , D >. Cgr <. G , H >. ) -> ( <. A , B >. Seg<_ <. C , D >. <-> <. E , F >. Seg<_ <. G , H >. ) ) )