Metamath Proof Explorer

Theorem axcgrtr

Description: Congruence is transitive. Axiom A2 of Schwabhauser p. 10. (Contributed by Scott Fenton, 3-Jun-2013)

Ref Expression
Assertion axcgrtr 
|- ( ( 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 ) ) ) -> ( ( <. A , B >. Cgr <. C , D >. /\ <. A , B >. Cgr <. E , F >. ) -> <. C , D >. Cgr <. E , F >. ) )

Proof

Step Hyp Ref Expression
1 eqtr2 
 |-  ( ( sum_ i e. ( 1 ... N ) ( ( ( A ` i ) - ( B ` i ) ) ^ 2 ) = sum_ i e. ( 1 ... N ) ( ( ( C ` i ) - ( D ` i ) ) ^ 2 ) /\ sum_ i e. ( 1 ... N ) ( ( ( A ` i ) - ( B ` i ) ) ^ 2 ) = sum_ i e. ( 1 ... N ) ( ( ( E ` i ) - ( F ` i ) ) ^ 2 ) ) -> sum_ i e. ( 1 ... N ) ( ( ( C ` i ) - ( D ` i ) ) ^ 2 ) = sum_ i e. ( 1 ... N ) ( ( ( E ` i ) - ( F ` i ) ) ^ 2 ) )
2 simpl1 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) -> A e. ( EE ` N ) )
3 simpl2 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) -> B e. ( EE ` N ) )
4 simpl3 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) -> C e. ( EE ` N ) )
5 simpr1 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) -> D e. ( EE ` N ) )
6 brcgr 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> ( <. A , B >. Cgr <. C , D >. <-> sum_ i e. ( 1 ... N ) ( ( ( A ` i ) - ( B ` i ) ) ^ 2 ) = sum_ i e. ( 1 ... N ) ( ( ( C ` i ) - ( D ` i ) ) ^ 2 ) ) )
7 2 3 4 5 6 syl22anc 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) -> ( <. A , B >. Cgr <. C , D >. <-> sum_ i e. ( 1 ... N ) ( ( ( A ` i ) - ( B ` i ) ) ^ 2 ) = sum_ i e. ( 1 ... N ) ( ( ( C ` i ) - ( D ` i ) ) ^ 2 ) ) )
8 simpr2 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) -> E e. ( EE ` N ) )
9 simpr3 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) -> F e. ( EE ` N ) )
10 brcgr 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) -> ( <. A , B >. Cgr <. E , F >. <-> sum_ i e. ( 1 ... N ) ( ( ( A ` i ) - ( B ` i ) ) ^ 2 ) = sum_ i e. ( 1 ... N ) ( ( ( E ` i ) - ( F ` i ) ) ^ 2 ) ) )
11 2 3 8 9 10 syl22anc 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) -> ( <. A , B >. Cgr <. E , F >. <-> sum_ i e. ( 1 ... N ) ( ( ( A ` i ) - ( B ` i ) ) ^ 2 ) = sum_ i e. ( 1 ... N ) ( ( ( E ` i ) - ( F ` i ) ) ^ 2 ) ) )
12 7 11 anbi12d 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) -> ( ( <. A , B >. Cgr <. C , D >. /\ <. A , B >. Cgr <. E , F >. ) <-> ( sum_ i e. ( 1 ... N ) ( ( ( A ` i ) - ( B ` i ) ) ^ 2 ) = sum_ i e. ( 1 ... N ) ( ( ( C ` i ) - ( D ` i ) ) ^ 2 ) /\ sum_ i e. ( 1 ... N ) ( ( ( A ` i ) - ( B ` i ) ) ^ 2 ) = sum_ i e. ( 1 ... N ) ( ( ( E ` i ) - ( F ` i ) ) ^ 2 ) ) ) )
13 brcgr 
 |-  ( ( ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) /\ ( E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) -> ( <. C , D >. Cgr <. E , F >. <-> sum_ i e. ( 1 ... N ) ( ( ( C ` i ) - ( D ` i ) ) ^ 2 ) = sum_ i e. ( 1 ... N ) ( ( ( E ` i ) - ( F ` i ) ) ^ 2 ) ) )
14 4 5 8 9 13 syl22anc 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) -> ( <. C , D >. Cgr <. E , F >. <-> sum_ i e. ( 1 ... N ) ( ( ( C ` i ) - ( D ` i ) ) ^ 2 ) = sum_ i e. ( 1 ... N ) ( ( ( E ` i ) - ( F ` i ) ) ^ 2 ) ) )
15 12 14 imbi12d 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) -> ( ( ( <. A , B >. Cgr <. C , D >. /\ <. A , B >. Cgr <. E , F >. ) -> <. C , D >. Cgr <. E , F >. ) <-> ( ( sum_ i e. ( 1 ... N ) ( ( ( A ` i ) - ( B ` i ) ) ^ 2 ) = sum_ i e. ( 1 ... N ) ( ( ( C ` i ) - ( D ` i ) ) ^ 2 ) /\ sum_ i e. ( 1 ... N ) ( ( ( A ` i ) - ( B ` i ) ) ^ 2 ) = sum_ i e. ( 1 ... N ) ( ( ( E ` i ) - ( F ` i ) ) ^ 2 ) ) -> sum_ i e. ( 1 ... N ) ( ( ( C ` i ) - ( D ` i ) ) ^ 2 ) = sum_ i e. ( 1 ... N ) ( ( ( E ` i ) - ( F ` i ) ) ^ 2 ) ) ) )
16 1 15 mpbiri 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) -> ( ( <. A , B >. Cgr <. C , D >. /\ <. A , B >. Cgr <. E , F >. ) -> <. C , D >. Cgr <. E , F >. ) )
17 16 3adant1 
 |-  ( ( 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 ) ) ) -> ( ( <. A , B >. Cgr <. C , D >. /\ <. A , B >. Cgr <. E , F >. ) -> <. C , D >. Cgr <. E , F >. ) )