Metamath Proof Explorer

Theorem cgratr

Description: Angle congruence is transitive. Theorem 11.8 of Schwabhauser p. 97. (Contributed by Thierry Arnoux, 5-Mar-2020)

Ref Expression
Hypotheses cgraid.p 
|- P = ( Base ` G )
cgraid.i 
|- I = ( Itv ` G )
cgraid.g 
|- ( ph -> G e. TarskiG )
cgraid.k 
|- K = ( hlG ` G )
cgraid.a 
|- ( ph -> A e. P )
cgraid.b 
|- ( ph -> B e. P )
cgraid.c 
|- ( ph -> C e. P )
cgracom.d 
|- ( ph -> D e. P )
cgracom.e 
|- ( ph -> E e. P )
cgracom.f 
|- ( ph -> F e. P )
cgracom.1 
|- ( ph -> <" A B C "> ( cgrA ` G ) <" D E F "> )
cgratr.h 
|- ( ph -> H e. P )
cgratr.i 
|- ( ph -> U e. P )
cgratr.j 
|- ( ph -> J e. P )
cgratr.1 
|- ( ph -> <" D E F "> ( cgrA ` G ) <" H U J "> )
Assertion cgratr 
|- ( ph -> <" A B C "> ( cgrA ` G ) <" H U J "> )

Proof

Step Hyp Ref Expression
1 cgraid.p 
 |-  P = ( Base ` G )
2 cgraid.i 
 |-  I = ( Itv ` G )
3 cgraid.g 
 |-  ( ph -> G e. TarskiG )
4 cgraid.k 
 |-  K = ( hlG ` G )
5 cgraid.a 
 |-  ( ph -> A e. P )
6 cgraid.b 
 |-  ( ph -> B e. P )
7 cgraid.c 
 |-  ( ph -> C e. P )
8 cgracom.d 
 |-  ( ph -> D e. P )
9 cgracom.e 
 |-  ( ph -> E e. P )
10 cgracom.f 
 |-  ( ph -> F e. P )
11 cgracom.1 
 |-  ( ph -> <" A B C "> ( cgrA ` G ) <" D E F "> )
12 cgratr.h 
 |-  ( ph -> H e. P )
13 cgratr.i 
 |-  ( ph -> U e. P )
14 cgratr.j 
 |-  ( ph -> J e. P )
15 cgratr.1 
 |-  ( ph -> <" D E F "> ( cgrA ` G ) <" H U J "> )
16 eqid 
 |-  ( dist ` G ) = ( dist ` G )
17 eqid 
 |-  ( cgrG ` G ) = ( cgrG ` G )
18 3 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` U ) H /\ ( U ( dist ` G ) x ) = ( B ( dist ` G ) A ) ) /\ ( y ( K ` U ) J /\ ( U ( dist ` G ) y ) = ( B ( dist ` G ) C ) ) ) ) -> G e. TarskiG )
19 5 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` U ) H /\ ( U ( dist ` G ) x ) = ( B ( dist ` G ) A ) ) /\ ( y ( K ` U ) J /\ ( U ( dist ` G ) y ) = ( B ( dist ` G ) C ) ) ) ) -> A e. P )
20 6 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` U ) H /\ ( U ( dist ` G ) x ) = ( B ( dist ` G ) A ) ) /\ ( y ( K ` U ) J /\ ( U ( dist ` G ) y ) = ( B ( dist ` G ) C ) ) ) ) -> B e. P )
21 7 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` U ) H /\ ( U ( dist ` G ) x ) = ( B ( dist ` G ) A ) ) /\ ( y ( K ` U ) J /\ ( U ( dist ` G ) y ) = ( B ( dist ` G ) C ) ) ) ) -> C e. P )
22 simpllr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` U ) H /\ ( U ( dist ` G ) x ) = ( B ( dist ` G ) A ) ) /\ ( y ( K ` U ) J /\ ( U ( dist ` G ) y ) = ( B ( dist ` G ) C ) ) ) ) -> x e. P )
23 13 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` U ) H /\ ( U ( dist ` G ) x ) = ( B ( dist ` G ) A ) ) /\ ( y ( K ` U ) J /\ ( U ( dist ` G ) y ) = ( B ( dist ` G ) C ) ) ) ) -> U e. P )
24 simplr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` U ) H /\ ( U ( dist ` G ) x ) = ( B ( dist ` G ) A ) ) /\ ( y ( K ` U ) J /\ ( U ( dist ` G ) y ) = ( B ( dist ` G ) C ) ) ) ) -> y e. P )
25 simprlr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` U ) H /\ ( U ( dist ` G ) x ) = ( B ( dist ` G ) A ) ) /\ ( y ( K ` U ) J /\ ( U ( dist ` G ) y ) = ( B ( dist ` G ) C ) ) ) ) -> ( U ( dist ` G ) x ) = ( B ( dist ` G ) A ) )
26 25 eqcomd 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` U ) H /\ ( U ( dist ` G ) x ) = ( B ( dist ` G ) A ) ) /\ ( y ( K ` U ) J /\ ( U ( dist ` G ) y ) = ( B ( dist ` G ) C ) ) ) ) -> ( B ( dist ` G ) A ) = ( U ( dist ` G ) x ) )
27 1 16 2 18 20 19 23 22 26 tgcgrcomlr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` U ) H /\ ( U ( dist ` G ) x ) = ( B ( dist ` G ) A ) ) /\ ( y ( K ` U ) J /\ ( U ( dist ` G ) y ) = ( B ( dist ` G ) C ) ) ) ) -> ( A ( dist ` G ) B ) = ( x ( dist ` G ) U ) )
28 simprrr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` U ) H /\ ( U ( dist ` G ) x ) = ( B ( dist ` G ) A ) ) /\ ( y ( K ` U ) J /\ ( U ( dist ` G ) y ) = ( B ( dist ` G ) C ) ) ) ) -> ( U ( dist ` G ) y ) = ( B ( dist ` G ) C ) )
29 28 eqcomd 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` U ) H /\ ( U ( dist ` G ) x ) = ( B ( dist ` G ) A ) ) /\ ( y ( K ` U ) J /\ ( U ( dist ` G ) y ) = ( B ( dist ` G ) C ) ) ) ) -> ( B ( dist ` G ) C ) = ( U ( dist ` G ) y ) )
30 18 ad3antrrr 
 |-  ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` U ) H /\ ( U ( dist ` G ) x ) = ( B ( dist ` G ) A ) ) /\ ( y ( K ` U ) J /\ ( U ( dist ` G ) y ) = ( B ( dist ` G ) C ) ) ) ) /\ u e. P ) /\ v e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" u E v "> /\ u ( K ` E ) D /\ v ( K ` E ) F ) ) -> G e. TarskiG )
31 19 ad3antrrr 
 |-  ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` U ) H /\ ( U ( dist ` G ) x ) = ( B ( dist ` G ) A ) ) /\ ( y ( K ` U ) J /\ ( U ( dist ` G ) y ) = ( B ( dist ` G ) C ) ) ) ) /\ u e. P ) /\ v e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" u E v "> /\ u ( K ` E ) D /\ v ( K ` E ) F ) ) -> A e. P )
32 20 ad3antrrr 
 |-  ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` U ) H /\ ( U ( dist ` G ) x ) = ( B ( dist ` G ) A ) ) /\ ( y ( K ` U ) J /\ ( U ( dist ` G ) y ) = ( B ( dist ` G ) C ) ) ) ) /\ u e. P ) /\ v e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" u E v "> /\ u ( K ` E ) D /\ v ( K ` E ) F ) ) -> B e. P )
33 21 ad3antrrr 
 |-  ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` U ) H /\ ( U ( dist ` G ) x ) = ( B ( dist ` G ) A ) ) /\ ( y ( K ` U ) J /\ ( U ( dist ` G ) y ) = ( B ( dist ` G ) C ) ) ) ) /\ u e. P ) /\ v e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" u E v "> /\ u ( K ` E ) D /\ v ( K ` E ) F ) ) -> C e. P )
34 simpllr 
 |-  ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` U ) H /\ ( U ( dist ` G ) x ) = ( B ( dist ` G ) A ) ) /\ ( y ( K ` U ) J /\ ( U ( dist ` G ) y ) = ( B ( dist ` G ) C ) ) ) ) /\ u e. P ) /\ v e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" u E v "> /\ u ( K ` E ) D /\ v ( K ` E ) F ) ) -> u e. P )
35 9 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` U ) H /\ ( U ( dist ` G ) x ) = ( B ( dist ` G ) A ) ) /\ ( y ( K ` U ) J /\ ( U ( dist ` G ) y ) = ( B ( dist ` G ) C ) ) ) ) /\ u e. P ) /\ v e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" u E v "> /\ u ( K ` E ) D /\ v ( K ` E ) F ) ) -> E e. P )
36 simplr 
 |-  ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` U ) H /\ ( U ( dist ` G ) x ) = ( B ( dist ` G ) A ) ) /\ ( y ( K ` U ) J /\ ( U ( dist ` G ) y ) = ( B ( dist ` G ) C ) ) ) ) /\ u e. P ) /\ v e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" u E v "> /\ u ( K ` E ) D /\ v ( K ` E ) F ) ) -> v e. P )
37 simpr1 
 |-  ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` U ) H /\ ( U ( dist ` G ) x ) = ( B ( dist ` G ) A ) ) /\ ( y ( K ` U ) J /\ ( U ( dist ` G ) y ) = ( B ( dist ` G ) C ) ) ) ) /\ u e. P ) /\ v e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" u E v "> /\ u ( K ` E ) D /\ v ( K ` E ) F ) ) -> <" A B C "> ( cgrG ` G ) <" u E v "> )
38 1 16 2 17 30 31 32 33 34 35 36 37 cgr3simp3 
 |-  ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` U ) H /\ ( U ( dist ` G ) x ) = ( B ( dist ` G ) A ) ) /\ ( y ( K ` U ) J /\ ( U ( dist ` G ) y ) = ( B ( dist ` G ) C ) ) ) ) /\ u e. P ) /\ v e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" u E v "> /\ u ( K ` E ) D /\ v ( K ` E ) F ) ) -> ( C ( dist ` G ) A ) = ( v ( dist ` G ) u ) )
39 22 ad3antrrr 
 |-  ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` U ) H /\ ( U ( dist ` G ) x ) = ( B ( dist ` G ) A ) ) /\ ( y ( K ` U ) J /\ ( U ( dist ` G ) y ) = ( B ( dist ` G ) C ) ) ) ) /\ u e. P ) /\ v e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" u E v "> /\ u ( K ` E ) D /\ v ( K ` E ) F ) ) -> x e. P )
40 24 ad3antrrr 
 |-  ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` U ) H /\ ( U ( dist ` G ) x ) = ( B ( dist ` G ) A ) ) /\ ( y ( K ` U ) J /\ ( U ( dist ` G ) y ) = ( B ( dist ` G ) C ) ) ) ) /\ u e. P ) /\ v e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" u E v "> /\ u ( K ` E ) D /\ v ( K ` E ) F ) ) -> y e. P )
41 8 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` U ) H /\ ( U ( dist ` G ) x ) = ( B ( dist ` G ) A ) ) /\ ( y ( K ` U ) J /\ ( U ( dist ` G ) y ) = ( B ( dist ` G ) C ) ) ) ) /\ u e. P ) /\ v e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" u E v "> /\ u ( K ` E ) D /\ v ( K ` E ) F ) ) -> D e. P )
42 10 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` U ) H /\ ( U ( dist ` G ) x ) = ( B ( dist ` G ) A ) ) /\ ( y ( K ` U ) J /\ ( U ( dist ` G ) y ) = ( B ( dist ` G ) C ) ) ) ) /\ u e. P ) /\ v e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" u E v "> /\ u ( K ` E ) D /\ v ( K ` E ) F ) ) -> F e. P )
43 23 ad3antrrr 
 |-  ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` U ) H /\ ( U ( dist ` G ) x ) = ( B ( dist ` G ) A ) ) /\ ( y ( K ` U ) J /\ ( U ( dist ` G ) y ) = ( B ( dist ` G ) C ) ) ) ) /\ u e. P ) /\ v e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" u E v "> /\ u ( K ` E ) D /\ v ( K ` E ) F ) ) -> U e. P )
44 14 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` U ) H /\ ( U ( dist ` G ) x ) = ( B ( dist ` G ) A ) ) /\ ( y ( K ` U ) J /\ ( U ( dist ` G ) y ) = ( B ( dist ` G ) C ) ) ) ) /\ u e. P ) /\ v e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" u E v "> /\ u ( K ` E ) D /\ v ( K ` E ) F ) ) -> J e. P )
45 12 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` U ) H /\ ( U ( dist ` G ) x ) = ( B ( dist ` G ) A ) ) /\ ( y ( K ` U ) J /\ ( U ( dist ` G ) y ) = ( B ( dist ` G ) C ) ) ) ) /\ u e. P ) /\ v e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" u E v "> /\ u ( K ` E ) D /\ v ( K ` E ) F ) ) -> H e. P )
46 15 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` U ) H /\ ( U ( dist ` G ) x ) = ( B ( dist ` G ) A ) ) /\ ( y ( K ` U ) J /\ ( U ( dist ` G ) y ) = ( B ( dist ` G ) C ) ) ) ) /\ u e. P ) /\ v e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" u E v "> /\ u ( K ` E ) D /\ v ( K ` E ) F ) ) -> <" D E F "> ( cgrA ` G ) <" H U J "> )
47 simprll 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` U ) H /\ ( U ( dist ` G ) x ) = ( B ( dist ` G ) A ) ) /\ ( y ( K ` U ) J /\ ( U ( dist ` G ) y ) = ( B ( dist ` G ) C ) ) ) ) -> x ( K ` U ) H )
48 47 ad3antrrr 
 |-  ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` U ) H /\ ( U ( dist ` G ) x ) = ( B ( dist ` G ) A ) ) /\ ( y ( K ` U ) J /\ ( U ( dist ` G ) y ) = ( B ( dist ` G ) C ) ) ) ) /\ u e. P ) /\ v e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" u E v "> /\ u ( K ` E ) D /\ v ( K ` E ) F ) ) -> x ( K ` U ) H )
49 1 2 4 30 41 35 42 45 43 44 46 39 48 cgrahl1 
 |-  ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` U ) H /\ ( U ( dist ` G ) x ) = ( B ( dist ` G ) A ) ) /\ ( y ( K ` U ) J /\ ( U ( dist ` G ) y ) = ( B ( dist ` G ) C ) ) ) ) /\ u e. P ) /\ v e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" u E v "> /\ u ( K ` E ) D /\ v ( K ` E ) F ) ) -> <" D E F "> ( cgrA ` G ) <" x U J "> )
50 simprrl 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` U ) H /\ ( U ( dist ` G ) x ) = ( B ( dist ` G ) A ) ) /\ ( y ( K ` U ) J /\ ( U ( dist ` G ) y ) = ( B ( dist ` G ) C ) ) ) ) -> y ( K ` U ) J )
51 50 ad3antrrr 
 |-  ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` U ) H /\ ( U ( dist ` G ) x ) = ( B ( dist ` G ) A ) ) /\ ( y ( K ` U ) J /\ ( U ( dist ` G ) y ) = ( B ( dist ` G ) C ) ) ) ) /\ u e. P ) /\ v e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" u E v "> /\ u ( K ` E ) D /\ v ( K ` E ) F ) ) -> y ( K ` U ) J )
52 1 2 4 30 41 35 42 39 43 44 49 40 51 cgrahl2 
 |-  ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` U ) H /\ ( U ( dist ` G ) x ) = ( B ( dist ` G ) A ) ) /\ ( y ( K ` U ) J /\ ( U ( dist ` G ) y ) = ( B ( dist ` G ) C ) ) ) ) /\ u e. P ) /\ v e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" u E v "> /\ u ( K ` E ) D /\ v ( K ` E ) F ) ) -> <" D E F "> ( cgrA ` G ) <" x U y "> )
53 simpr2 
 |-  ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` U ) H /\ ( U ( dist ` G ) x ) = ( B ( dist ` G ) A ) ) /\ ( y ( K ` U ) J /\ ( U ( dist ` G ) y ) = ( B ( dist ` G ) C ) ) ) ) /\ u e. P ) /\ v e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" u E v "> /\ u ( K ` E ) D /\ v ( K ` E ) F ) ) -> u ( K ` E ) D )
54 simpr3 
 |-  ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` U ) H /\ ( U ( dist ` G ) x ) = ( B ( dist ` G ) A ) ) /\ ( y ( K ` U ) J /\ ( U ( dist ` G ) y ) = ( B ( dist ` G ) C ) ) ) ) /\ u e. P ) /\ v e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" u E v "> /\ u ( K ` E ) D /\ v ( K ` E ) F ) ) -> v ( K ` E ) F )
55 1 16 2 17 30 31 32 33 34 35 36 37 cgr3simp1 
 |-  ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` U ) H /\ ( U ( dist ` G ) x ) = ( B ( dist ` G ) A ) ) /\ ( y ( K ` U ) J /\ ( U ( dist ` G ) y ) = ( B ( dist ` G ) C ) ) ) ) /\ u e. P ) /\ v e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" u E v "> /\ u ( K ` E ) D /\ v ( K ` E ) F ) ) -> ( A ( dist ` G ) B ) = ( u ( dist ` G ) E ) )
56 55 eqcomd 
 |-  ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` U ) H /\ ( U ( dist ` G ) x ) = ( B ( dist ` G ) A ) ) /\ ( y ( K ` U ) J /\ ( U ( dist ` G ) y ) = ( B ( dist ` G ) C ) ) ) ) /\ u e. P ) /\ v e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" u E v "> /\ u ( K ` E ) D /\ v ( K ` E ) F ) ) -> ( u ( dist ` G ) E ) = ( A ( dist ` G ) B ) )
57 1 16 2 30 34 35 31 32 56 tgcgrcomlr 
 |-  ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` U ) H /\ ( U ( dist ` G ) x ) = ( B ( dist ` G ) A ) ) /\ ( y ( K ` U ) J /\ ( U ( dist ` G ) y ) = ( B ( dist ` G ) C ) ) ) ) /\ u e. P ) /\ v e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" u E v "> /\ u ( K ` E ) D /\ v ( K ` E ) F ) ) -> ( E ( dist ` G ) u ) = ( B ( dist ` G ) A ) )
58 26 ad3antrrr 
 |-  ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` U ) H /\ ( U ( dist ` G ) x ) = ( B ( dist ` G ) A ) ) /\ ( y ( K ` U ) J /\ ( U ( dist ` G ) y ) = ( B ( dist ` G ) C ) ) ) ) /\ u e. P ) /\ v e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" u E v "> /\ u ( K ` E ) D /\ v ( K ` E ) F ) ) -> ( B ( dist ` G ) A ) = ( U ( dist ` G ) x ) )
59 57 58 eqtrd 
 |-  ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` U ) H /\ ( U ( dist ` G ) x ) = ( B ( dist ` G ) A ) ) /\ ( y ( K ` U ) J /\ ( U ( dist ` G ) y ) = ( B ( dist ` G ) C ) ) ) ) /\ u e. P ) /\ v e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" u E v "> /\ u ( K ` E ) D /\ v ( K ` E ) F ) ) -> ( E ( dist ` G ) u ) = ( U ( dist ` G ) x ) )
60 1 16 2 17 30 31 32 33 34 35 36 37 cgr3simp2 
 |-  ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` U ) H /\ ( U ( dist ` G ) x ) = ( B ( dist ` G ) A ) ) /\ ( y ( K ` U ) J /\ ( U ( dist ` G ) y ) = ( B ( dist ` G ) C ) ) ) ) /\ u e. P ) /\ v e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" u E v "> /\ u ( K ` E ) D /\ v ( K ` E ) F ) ) -> ( B ( dist ` G ) C ) = ( E ( dist ` G ) v ) )
61 29 ad3antrrr 
 |-  ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` U ) H /\ ( U ( dist ` G ) x ) = ( B ( dist ` G ) A ) ) /\ ( y ( K ` U ) J /\ ( U ( dist ` G ) y ) = ( B ( dist ` G ) C ) ) ) ) /\ u e. P ) /\ v e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" u E v "> /\ u ( K ` E ) D /\ v ( K ` E ) F ) ) -> ( B ( dist ` G ) C ) = ( U ( dist ` G ) y ) )
62 60 61 eqtr3d 
 |-  ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` U ) H /\ ( U ( dist ` G ) x ) = ( B ( dist ` G ) A ) ) /\ ( y ( K ` U ) J /\ ( U ( dist ` G ) y ) = ( B ( dist ` G ) C ) ) ) ) /\ u e. P ) /\ v e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" u E v "> /\ u ( K ` E ) D /\ v ( K ` E ) F ) ) -> ( E ( dist ` G ) v ) = ( U ( dist ` G ) y ) )
63 1 2 4 30 41 35 42 39 43 40 52 34 16 36 53 54 59 62 cgracgr 
 |-  ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` U ) H /\ ( U ( dist ` G ) x ) = ( B ( dist ` G ) A ) ) /\ ( y ( K ` U ) J /\ ( U ( dist ` G ) y ) = ( B ( dist ` G ) C ) ) ) ) /\ u e. P ) /\ v e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" u E v "> /\ u ( K ` E ) D /\ v ( K ` E ) F ) ) -> ( u ( dist ` G ) v ) = ( x ( dist ` G ) y ) )
64 1 16 2 30 34 36 39 40 63 tgcgrcomlr 
 |-  ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` U ) H /\ ( U ( dist ` G ) x ) = ( B ( dist ` G ) A ) ) /\ ( y ( K ` U ) J /\ ( U ( dist ` G ) y ) = ( B ( dist ` G ) C ) ) ) ) /\ u e. P ) /\ v e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" u E v "> /\ u ( K ` E ) D /\ v ( K ` E ) F ) ) -> ( v ( dist ` G ) u ) = ( y ( dist ` G ) x ) )
65 38 64 eqtrd 
 |-  ( ( ( ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` U ) H /\ ( U ( dist ` G ) x ) = ( B ( dist ` G ) A ) ) /\ ( y ( K ` U ) J /\ ( U ( dist ` G ) y ) = ( B ( dist ` G ) C ) ) ) ) /\ u e. P ) /\ v e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" u E v "> /\ u ( K ` E ) D /\ v ( K ` E ) F ) ) -> ( C ( dist ` G ) A ) = ( y ( dist ` G ) x ) )
66 1 2 4 3 5 6 7 8 9 10 iscgra 
 |-  ( ph -> ( <" A B C "> ( cgrA ` G ) <" D E F "> <-> E. u e. P E. v e. P ( <" A B C "> ( cgrG ` G ) <" u E v "> /\ u ( K ` E ) D /\ v ( K ` E ) F ) ) )
67 11 66 mpbid 
 |-  ( ph -> E. u e. P E. v e. P ( <" A B C "> ( cgrG ` G ) <" u E v "> /\ u ( K ` E ) D /\ v ( K ` E ) F ) )
68 67 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` U ) H /\ ( U ( dist ` G ) x ) = ( B ( dist ` G ) A ) ) /\ ( y ( K ` U ) J /\ ( U ( dist ` G ) y ) = ( B ( dist ` G ) C ) ) ) ) -> E. u e. P E. v e. P ( <" A B C "> ( cgrG ` G ) <" u E v "> /\ u ( K ` E ) D /\ v ( K ` E ) F ) )
69 65 68 r19.29vva 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` U ) H /\ ( U ( dist ` G ) x ) = ( B ( dist ` G ) A ) ) /\ ( y ( K ` U ) J /\ ( U ( dist ` G ) y ) = ( B ( dist ` G ) C ) ) ) ) -> ( C ( dist ` G ) A ) = ( y ( dist ` G ) x ) )
70 1 16 17 18 19 20 21 22 23 24 27 29 69 trgcgr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` U ) H /\ ( U ( dist ` G ) x ) = ( B ( dist ` G ) A ) ) /\ ( y ( K ` U ) J /\ ( U ( dist ` G ) y ) = ( B ( dist ` G ) C ) ) ) ) -> <" A B C "> ( cgrG ` G ) <" x U y "> )
71 70 47 50 3jca 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( x ( K ` U ) H /\ ( U ( dist ` G ) x ) = ( B ( dist ` G ) A ) ) /\ ( y ( K ` U ) J /\ ( U ( dist ` G ) y ) = ( B ( dist ` G ) C ) ) ) ) -> ( <" A B C "> ( cgrG ` G ) <" x U y "> /\ x ( K ` U ) H /\ y ( K ` U ) J ) )
72 1 2 4 3 8 9 10 12 13 14 15 cgrane3 
 |-  ( ph -> U =/= H )
73 72 necomd 
 |-  ( ph -> H =/= U )
74 1 2 4 3 5 6 7 8 9 10 11 cgrane1 
 |-  ( ph -> A =/= B )
75 74 necomd 
 |-  ( ph -> B =/= A )
76 1 2 4 13 6 5 3 12 16 73 75 hlcgrex 
 |-  ( ph -> E. x e. P ( x ( K ` U ) H /\ ( U ( dist ` G ) x ) = ( B ( dist ` G ) A ) ) )
77 1 2 4 3 8 9 10 12 13 14 15 cgrane4 
 |-  ( ph -> U =/= J )
78 77 necomd 
 |-  ( ph -> J =/= U )
79 1 2 4 3 5 6 7 8 9 10 11 cgrane2 
 |-  ( ph -> B =/= C )
80 1 2 4 13 6 7 3 14 16 78 79 hlcgrex 
 |-  ( ph -> E. y e. P ( y ( K ` U ) J /\ ( U ( dist ` G ) y ) = ( B ( dist ` G ) C ) ) )
81 reeanv 
 |-  ( E. x e. P E. y e. P ( ( x ( K ` U ) H /\ ( U ( dist ` G ) x ) = ( B ( dist ` G ) A ) ) /\ ( y ( K ` U ) J /\ ( U ( dist ` G ) y ) = ( B ( dist ` G ) C ) ) ) <-> ( E. x e. P ( x ( K ` U ) H /\ ( U ( dist ` G ) x ) = ( B ( dist ` G ) A ) ) /\ E. y e. P ( y ( K ` U ) J /\ ( U ( dist ` G ) y ) = ( B ( dist ` G ) C ) ) ) )
82 76 80 81 sylanbrc 
 |-  ( ph -> E. x e. P E. y e. P ( ( x ( K ` U ) H /\ ( U ( dist ` G ) x ) = ( B ( dist ` G ) A ) ) /\ ( y ( K ` U ) J /\ ( U ( dist ` G ) y ) = ( B ( dist ` G ) C ) ) ) )
83 71 82 reximddv2 
 |-  ( ph -> E. x e. P E. y e. P ( <" A B C "> ( cgrG ` G ) <" x U y "> /\ x ( K ` U ) H /\ y ( K ` U ) J ) )
84 1 2 4 3 5 6 7 12 13 14 iscgra 
 |-  ( ph -> ( <" A B C "> ( cgrA ` G ) <" H U J "> <-> E. x e. P E. y e. P ( <" A B C "> ( cgrG ` G ) <" x U y "> /\ x ( K ` U ) H /\ y ( K ` U ) J ) ) )
85 83 84 mpbird 
 |-  ( ph -> <" A B C "> ( cgrA ` G ) <" H U J "> )