Metamath Proof Explorer

Theorem cgrg3col4

Description: Lemma 11.28 of Schwabhauser p. 102. Extend a congruence of three points with a fourth colinear point. (Contributed by Thierry Arnoux, 8-Oct-2020)

Ref Expression
Hypotheses isleag.p 
|- P = ( Base ` G )
isleag.g 
|- ( ph -> G e. TarskiG )
isleag.a 
|- ( ph -> A e. P )
isleag.b 
|- ( ph -> B e. P )
isleag.c 
|- ( ph -> C e. P )
isleag.d 
|- ( ph -> D e. P )
isleag.e 
|- ( ph -> E e. P )
isleag.f 
|- ( ph -> F e. P )
cgrg3col4.l 
|- L = ( LineG ` G )
cgrg3col4.x 
|- ( ph -> X e. P )
cgrg3col4.1 
|- ( ph -> <" A B C "> ( cgrG ` G ) <" D E F "> )
cgrg3col4.2 
|- ( ph -> ( X e. ( A L C ) \/ A = C ) )
Assertion cgrg3col4 
|- ( ph -> E. y e. P <" A B C X "> ( cgrG ` G ) <" D E F y "> )

Proof

Step Hyp Ref Expression
1 isleag.p 
 |-  P = ( Base ` G )
2 isleag.g 
 |-  ( ph -> G e. TarskiG )
3 isleag.a 
 |-  ( ph -> A e. P )
4 isleag.b 
 |-  ( ph -> B e. P )
5 isleag.c 
 |-  ( ph -> C e. P )
6 isleag.d 
 |-  ( ph -> D e. P )
7 isleag.e 
 |-  ( ph -> E e. P )
8 isleag.f 
 |-  ( ph -> F e. P )
9 cgrg3col4.l 
 |-  L = ( LineG ` G )
10 cgrg3col4.x 
 |-  ( ph -> X e. P )
11 cgrg3col4.1 
 |-  ( ph -> <" A B C "> ( cgrG ` G ) <" D E F "> )
12 cgrg3col4.2 
 |-  ( ph -> ( X e. ( A L C ) \/ A = C ) )
13 eqid 
 |-  ( Itv ` G ) = ( Itv ` G )
14 2 ad2antrr 
 |-  ( ( ( ph /\ A = C ) /\ ( B e. ( A L X ) \/ A = X ) ) -> G e. TarskiG )
15 3 ad2antrr 
 |-  ( ( ( ph /\ A = C ) /\ ( B e. ( A L X ) \/ A = X ) ) -> A e. P )
16 4 ad2antrr 
 |-  ( ( ( ph /\ A = C ) /\ ( B e. ( A L X ) \/ A = X ) ) -> B e. P )
17 10 ad2antrr 
 |-  ( ( ( ph /\ A = C ) /\ ( B e. ( A L X ) \/ A = X ) ) -> X e. P )
18 eqid 
 |-  ( cgrG ` G ) = ( cgrG ` G )
19 6 ad2antrr 
 |-  ( ( ( ph /\ A = C ) /\ ( B e. ( A L X ) \/ A = X ) ) -> D e. P )
20 7 ad2antrr 
 |-  ( ( ( ph /\ A = C ) /\ ( B e. ( A L X ) \/ A = X ) ) -> E e. P )
21 eqid 
 |-  ( dist ` G ) = ( dist ` G )
22 simpr 
 |-  ( ( ( ph /\ A = C ) /\ ( B e. ( A L X ) \/ A = X ) ) -> ( B e. ( A L X ) \/ A = X ) )
23 1 21 13 18 2 3 4 5 6 7 8 11 cgr3simp1 
 |-  ( ph -> ( A ( dist ` G ) B ) = ( D ( dist ` G ) E ) )
24 23 ad2antrr 
 |-  ( ( ( ph /\ A = C ) /\ ( B e. ( A L X ) \/ A = X ) ) -> ( A ( dist ` G ) B ) = ( D ( dist ` G ) E ) )
25 1 9 13 14 15 16 17 18 19 20 21 22 24 lnext 
 |-  ( ( ( ph /\ A = C ) /\ ( B e. ( A L X ) \/ A = X ) ) -> E. y e. P <" A B X "> ( cgrG ` G ) <" D E y "> )
26 11 ad4antr 
 |-  ( ( ( ( ( ph /\ A = C ) /\ ( B e. ( A L X ) \/ A = X ) ) /\ y e. P ) /\ <" A B X "> ( cgrG ` G ) <" D E y "> ) -> <" A B C "> ( cgrG ` G ) <" D E F "> )
27 14 ad2antrr 
 |-  ( ( ( ( ( ph /\ A = C ) /\ ( B e. ( A L X ) \/ A = X ) ) /\ y e. P ) /\ <" A B X "> ( cgrG ` G ) <" D E y "> ) -> G e. TarskiG )
28 17 ad2antrr 
 |-  ( ( ( ( ( ph /\ A = C ) /\ ( B e. ( A L X ) \/ A = X ) ) /\ y e. P ) /\ <" A B X "> ( cgrG ` G ) <" D E y "> ) -> X e. P )
29 15 ad2antrr 
 |-  ( ( ( ( ( ph /\ A = C ) /\ ( B e. ( A L X ) \/ A = X ) ) /\ y e. P ) /\ <" A B X "> ( cgrG ` G ) <" D E y "> ) -> A e. P )
30 simplr 
 |-  ( ( ( ( ( ph /\ A = C ) /\ ( B e. ( A L X ) \/ A = X ) ) /\ y e. P ) /\ <" A B X "> ( cgrG ` G ) <" D E y "> ) -> y e. P )
31 19 ad2antrr 
 |-  ( ( ( ( ( ph /\ A = C ) /\ ( B e. ( A L X ) \/ A = X ) ) /\ y e. P ) /\ <" A B X "> ( cgrG ` G ) <" D E y "> ) -> D e. P )
32 16 ad2antrr 
 |-  ( ( ( ( ( ph /\ A = C ) /\ ( B e. ( A L X ) \/ A = X ) ) /\ y e. P ) /\ <" A B X "> ( cgrG ` G ) <" D E y "> ) -> B e. P )
33 20 ad2antrr 
 |-  ( ( ( ( ( ph /\ A = C ) /\ ( B e. ( A L X ) \/ A = X ) ) /\ y e. P ) /\ <" A B X "> ( cgrG ` G ) <" D E y "> ) -> E e. P )
34 simpr 
 |-  ( ( ( ( ( ph /\ A = C ) /\ ( B e. ( A L X ) \/ A = X ) ) /\ y e. P ) /\ <" A B X "> ( cgrG ` G ) <" D E y "> ) -> <" A B X "> ( cgrG ` G ) <" D E y "> )
35 1 21 13 18 27 29 32 28 31 33 30 34 cgr3simp3 
 |-  ( ( ( ( ( ph /\ A = C ) /\ ( B e. ( A L X ) \/ A = X ) ) /\ y e. P ) /\ <" A B X "> ( cgrG ` G ) <" D E y "> ) -> ( X ( dist ` G ) A ) = ( y ( dist ` G ) D ) )
36 1 21 13 27 28 29 30 31 35 tgcgrcomlr 
 |-  ( ( ( ( ( ph /\ A = C ) /\ ( B e. ( A L X ) \/ A = X ) ) /\ y e. P ) /\ <" A B X "> ( cgrG ` G ) <" D E y "> ) -> ( A ( dist ` G ) X ) = ( D ( dist ` G ) y ) )
37 1 21 13 18 27 29 32 28 31 33 30 34 cgr3simp2 
 |-  ( ( ( ( ( ph /\ A = C ) /\ ( B e. ( A L X ) \/ A = X ) ) /\ y e. P ) /\ <" A B X "> ( cgrG ` G ) <" D E y "> ) -> ( B ( dist ` G ) X ) = ( E ( dist ` G ) y ) )
38 5 ad4antr 
 |-  ( ( ( ( ( ph /\ A = C ) /\ ( B e. ( A L X ) \/ A = X ) ) /\ y e. P ) /\ <" A B X "> ( cgrG ` G ) <" D E y "> ) -> C e. P )
39 8 ad4antr 
 |-  ( ( ( ( ( ph /\ A = C ) /\ ( B e. ( A L X ) \/ A = X ) ) /\ y e. P ) /\ <" A B X "> ( cgrG ` G ) <" D E y "> ) -> F e. P )
40 simpr 
 |-  ( ( ph /\ A = C ) -> A = C )
41 40 ad3antrrr 
 |-  ( ( ( ( ( ph /\ A = C ) /\ ( B e. ( A L X ) \/ A = X ) ) /\ y e. P ) /\ <" A B X "> ( cgrG ` G ) <" D E y "> ) -> A = C )
42 41 oveq2d 
 |-  ( ( ( ( ( ph /\ A = C ) /\ ( B e. ( A L X ) \/ A = X ) ) /\ y e. P ) /\ <" A B X "> ( cgrG ` G ) <" D E y "> ) -> ( X ( dist ` G ) A ) = ( X ( dist ` G ) C ) )
43 2 adantr 
 |-  ( ( ph /\ A = C ) -> G e. TarskiG )
44 3 adantr 
 |-  ( ( ph /\ A = C ) -> A e. P )
45 5 adantr 
 |-  ( ( ph /\ A = C ) -> C e. P )
46 6 adantr 
 |-  ( ( ph /\ A = C ) -> D e. P )
47 8 adantr 
 |-  ( ( ph /\ A = C ) -> F e. P )
48 1 21 13 18 2 3 4 5 6 7 8 11 cgr3simp3 
 |-  ( ph -> ( C ( dist ` G ) A ) = ( F ( dist ` G ) D ) )
49 1 21 13 2 5 3 8 6 48 tgcgrcomlr 
 |-  ( ph -> ( A ( dist ` G ) C ) = ( D ( dist ` G ) F ) )
50 49 adantr 
 |-  ( ( ph /\ A = C ) -> ( A ( dist ` G ) C ) = ( D ( dist ` G ) F ) )
51 1 21 13 43 44 45 46 47 50 40 tgcgreq 
 |-  ( ( ph /\ A = C ) -> D = F )
52 51 ad3antrrr 
 |-  ( ( ( ( ( ph /\ A = C ) /\ ( B e. ( A L X ) \/ A = X ) ) /\ y e. P ) /\ <" A B X "> ( cgrG ` G ) <" D E y "> ) -> D = F )
53 52 oveq2d 
 |-  ( ( ( ( ( ph /\ A = C ) /\ ( B e. ( A L X ) \/ A = X ) ) /\ y e. P ) /\ <" A B X "> ( cgrG ` G ) <" D E y "> ) -> ( y ( dist ` G ) D ) = ( y ( dist ` G ) F ) )
54 35 42 53 3eqtr3d 
 |-  ( ( ( ( ( ph /\ A = C ) /\ ( B e. ( A L X ) \/ A = X ) ) /\ y e. P ) /\ <" A B X "> ( cgrG ` G ) <" D E y "> ) -> ( X ( dist ` G ) C ) = ( y ( dist ` G ) F ) )
55 1 21 13 27 28 38 30 39 54 tgcgrcomlr 
 |-  ( ( ( ( ( ph /\ A = C ) /\ ( B e. ( A L X ) \/ A = X ) ) /\ y e. P ) /\ <" A B X "> ( cgrG ` G ) <" D E y "> ) -> ( C ( dist ` G ) X ) = ( F ( dist ` G ) y ) )
56 36 37 55 3jca 
 |-  ( ( ( ( ( ph /\ A = C ) /\ ( B e. ( A L X ) \/ A = X ) ) /\ y e. P ) /\ <" A B X "> ( cgrG ` G ) <" D E y "> ) -> ( ( A ( dist ` G ) X ) = ( D ( dist ` G ) y ) /\ ( B ( dist ` G ) X ) = ( E ( dist ` G ) y ) /\ ( C ( dist ` G ) X ) = ( F ( dist ` G ) y ) ) )
57 1 21 13 18 27 29 32 38 28 31 33 39 30 tgcgr4 
 |-  ( ( ( ( ( ph /\ A = C ) /\ ( B e. ( A L X ) \/ A = X ) ) /\ y e. P ) /\ <" A B X "> ( cgrG ` G ) <" D E y "> ) -> ( <" A B C X "> ( cgrG ` G ) <" D E F y "> <-> ( <" A B C "> ( cgrG ` G ) <" D E F "> /\ ( ( A ( dist ` G ) X ) = ( D ( dist ` G ) y ) /\ ( B ( dist ` G ) X ) = ( E ( dist ` G ) y ) /\ ( C ( dist ` G ) X ) = ( F ( dist ` G ) y ) ) ) ) )
58 26 56 57 mpbir2and 
 |-  ( ( ( ( ( ph /\ A = C ) /\ ( B e. ( A L X ) \/ A = X ) ) /\ y e. P ) /\ <" A B X "> ( cgrG ` G ) <" D E y "> ) -> <" A B C X "> ( cgrG ` G ) <" D E F y "> )
59 58 ex 
 |-  ( ( ( ( ph /\ A = C ) /\ ( B e. ( A L X ) \/ A = X ) ) /\ y e. P ) -> ( <" A B X "> ( cgrG ` G ) <" D E y "> -> <" A B C X "> ( cgrG ` G ) <" D E F y "> ) )
60 59 reximdva 
 |-  ( ( ( ph /\ A = C ) /\ ( B e. ( A L X ) \/ A = X ) ) -> ( E. y e. P <" A B X "> ( cgrG ` G ) <" D E y "> -> E. y e. P <" A B C X "> ( cgrG ` G ) <" D E F y "> ) )
61 25 60 mpd 
 |-  ( ( ( ph /\ A = C ) /\ ( B e. ( A L X ) \/ A = X ) ) -> E. y e. P <" A B C X "> ( cgrG ` G ) <" D E F y "> )
62 eqid 
 |-  ( hlG ` G ) = ( hlG ` G )
63 2 ad2antrr 
 |-  ( ( ( ph /\ A = C ) /\ -. ( B e. ( A L X ) \/ A = X ) ) -> G e. TarskiG )
64 63 ad2antrr 
 |-  ( ( ( ( ( ph /\ A = C ) /\ -. ( B e. ( A L X ) \/ A = X ) ) /\ x e. P ) /\ -. x e. ( D L E ) ) -> G e. TarskiG )
65 4 ad2antrr 
 |-  ( ( ( ph /\ A = C ) /\ -. ( B e. ( A L X ) \/ A = X ) ) -> B e. P )
66 65 ad2antrr 
 |-  ( ( ( ( ( ph /\ A = C ) /\ -. ( B e. ( A L X ) \/ A = X ) ) /\ x e. P ) /\ -. x e. ( D L E ) ) -> B e. P )
67 3 ad2antrr 
 |-  ( ( ( ph /\ A = C ) /\ -. ( B e. ( A L X ) \/ A = X ) ) -> A e. P )
68 67 ad2antrr 
 |-  ( ( ( ( ( ph /\ A = C ) /\ -. ( B e. ( A L X ) \/ A = X ) ) /\ x e. P ) /\ -. x e. ( D L E ) ) -> A e. P )
69 10 ad2antrr 
 |-  ( ( ( ph /\ A = C ) /\ -. ( B e. ( A L X ) \/ A = X ) ) -> X e. P )
70 69 ad2antrr 
 |-  ( ( ( ( ( ph /\ A = C ) /\ -. ( B e. ( A L X ) \/ A = X ) ) /\ x e. P ) /\ -. x e. ( D L E ) ) -> X e. P )
71 7 ad2antrr 
 |-  ( ( ( ph /\ A = C ) /\ -. ( B e. ( A L X ) \/ A = X ) ) -> E e. P )
72 71 ad2antrr 
 |-  ( ( ( ( ( ph /\ A = C ) /\ -. ( B e. ( A L X ) \/ A = X ) ) /\ x e. P ) /\ -. x e. ( D L E ) ) -> E e. P )
73 6 ad2antrr 
 |-  ( ( ( ph /\ A = C ) /\ -. ( B e. ( A L X ) \/ A = X ) ) -> D e. P )
74 73 ad2antrr 
 |-  ( ( ( ( ( ph /\ A = C ) /\ -. ( B e. ( A L X ) \/ A = X ) ) /\ x e. P ) /\ -. x e. ( D L E ) ) -> D e. P )
75 simplr 
 |-  ( ( ( ( ( ph /\ A = C ) /\ -. ( B e. ( A L X ) \/ A = X ) ) /\ x e. P ) /\ -. x e. ( D L E ) ) -> x e. P )
76 simpllr 
 |-  ( ( ( ( ( ph /\ A = C ) /\ -. ( B e. ( A L X ) \/ A = X ) ) /\ x e. P ) /\ -. x e. ( D L E ) ) -> -. ( B e. ( A L X ) \/ A = X ) )
77 simpr 
 |-  ( ( ( ( ( ph /\ A = C ) /\ -. ( B e. ( A L X ) \/ A = X ) ) /\ x e. P ) /\ -. x e. ( D L E ) ) -> -. x e. ( D L E ) )
78 23 ad2antrr 
 |-  ( ( ( ph /\ A = C ) /\ -. ( B e. ( A L X ) \/ A = X ) ) -> ( A ( dist ` G ) B ) = ( D ( dist ` G ) E ) )
79 simpr 
 |-  ( ( ( ph /\ A = C ) /\ -. ( B e. ( A L X ) \/ A = X ) ) -> -. ( B e. ( A L X ) \/ A = X ) )
80 1 13 9 63 65 67 69 79 ncolne1 
 |-  ( ( ( ph /\ A = C ) /\ -. ( B e. ( A L X ) \/ A = X ) ) -> B =/= A )
81 80 necomd 
 |-  ( ( ( ph /\ A = C ) /\ -. ( B e. ( A L X ) \/ A = X ) ) -> A =/= B )
82 1 21 13 63 67 65 73 71 78 81 tgcgrneq 
 |-  ( ( ( ph /\ A = C ) /\ -. ( B e. ( A L X ) \/ A = X ) ) -> D =/= E )
83 82 ad2antrr 
 |-  ( ( ( ( ( ph /\ A = C ) /\ -. ( B e. ( A L X ) \/ A = X ) ) /\ x e. P ) /\ -. x e. ( D L E ) ) -> D =/= E )
84 83 neneqd 
 |-  ( ( ( ( ( ph /\ A = C ) /\ -. ( B e. ( A L X ) \/ A = X ) ) /\ x e. P ) /\ -. x e. ( D L E ) ) -> -. D = E )
85 ioran 
 |-  ( -. ( x e. ( D L E ) \/ D = E ) <-> ( -. x e. ( D L E ) /\ -. D = E ) )
86 77 84 85 sylanbrc 
 |-  ( ( ( ( ( ph /\ A = C ) /\ -. ( B e. ( A L X ) \/ A = X ) ) /\ x e. P ) /\ -. x e. ( D L E ) ) -> -. ( x e. ( D L E ) \/ D = E ) )
87 1 9 13 64 74 72 75 86 ncolcom 
 |-  ( ( ( ( ( ph /\ A = C ) /\ -. ( B e. ( A L X ) \/ A = X ) ) /\ x e. P ) /\ -. x e. ( D L E ) ) -> -. ( x e. ( E L D ) \/ E = D ) )
88 1 9 13 64 72 74 75 87 ncolrot1 
 |-  ( ( ( ( ( ph /\ A = C ) /\ -. ( B e. ( A L X ) \/ A = X ) ) /\ x e. P ) /\ -. x e. ( D L E ) ) -> -. ( E e. ( D L x ) \/ D = x ) )
89 1 21 13 2 3 4 6 7 23 tgcgrcomlr 
 |-  ( ph -> ( B ( dist ` G ) A ) = ( E ( dist ` G ) D ) )
90 89 ad4antr 
 |-  ( ( ( ( ( ph /\ A = C ) /\ -. ( B e. ( A L X ) \/ A = X ) ) /\ x e. P ) /\ -. x e. ( D L E ) ) -> ( B ( dist ` G ) A ) = ( E ( dist ` G ) D ) )
91 1 21 13 9 62 64 66 68 70 72 74 75 76 88 90 trgcopy 
 |-  ( ( ( ( ( ph /\ A = C ) /\ -. ( B e. ( A L X ) \/ A = X ) ) /\ x e. P ) /\ -. x e. ( D L E ) ) -> E. y e. P ( <" B A X "> ( cgrG ` G ) <" E D y "> /\ y ( ( hpG ` G ) ` ( E L D ) ) x ) )
92 11 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ A = C ) /\ -. ( B e. ( A L X ) \/ A = X ) ) /\ x e. P ) /\ -. x e. ( D L E ) ) /\ y e. P ) /\ <" B A X "> ( cgrG ` G ) <" E D y "> ) -> <" A B C "> ( cgrG ` G ) <" D E F "> )
93 64 ad2antrr 
 |-  ( ( ( ( ( ( ( ph /\ A = C ) /\ -. ( B e. ( A L X ) \/ A = X ) ) /\ x e. P ) /\ -. x e. ( D L E ) ) /\ y e. P ) /\ <" B A X "> ( cgrG ` G ) <" E D y "> ) -> G e. TarskiG )
94 66 ad2antrr 
 |-  ( ( ( ( ( ( ( ph /\ A = C ) /\ -. ( B e. ( A L X ) \/ A = X ) ) /\ x e. P ) /\ -. x e. ( D L E ) ) /\ y e. P ) /\ <" B A X "> ( cgrG ` G ) <" E D y "> ) -> B e. P )
95 68 ad2antrr 
 |-  ( ( ( ( ( ( ( ph /\ A = C ) /\ -. ( B e. ( A L X ) \/ A = X ) ) /\ x e. P ) /\ -. x e. ( D L E ) ) /\ y e. P ) /\ <" B A X "> ( cgrG ` G ) <" E D y "> ) -> A e. P )
96 70 ad2antrr 
 |-  ( ( ( ( ( ( ( ph /\ A = C ) /\ -. ( B e. ( A L X ) \/ A = X ) ) /\ x e. P ) /\ -. x e. ( D L E ) ) /\ y e. P ) /\ <" B A X "> ( cgrG ` G ) <" E D y "> ) -> X e. P )
97 72 ad2antrr 
 |-  ( ( ( ( ( ( ( ph /\ A = C ) /\ -. ( B e. ( A L X ) \/ A = X ) ) /\ x e. P ) /\ -. x e. ( D L E ) ) /\ y e. P ) /\ <" B A X "> ( cgrG ` G ) <" E D y "> ) -> E e. P )
98 74 ad2antrr 
 |-  ( ( ( ( ( ( ( ph /\ A = C ) /\ -. ( B e. ( A L X ) \/ A = X ) ) /\ x e. P ) /\ -. x e. ( D L E ) ) /\ y e. P ) /\ <" B A X "> ( cgrG ` G ) <" E D y "> ) -> D e. P )
99 simplr 
 |-  ( ( ( ( ( ( ( ph /\ A = C ) /\ -. ( B e. ( A L X ) \/ A = X ) ) /\ x e. P ) /\ -. x e. ( D L E ) ) /\ y e. P ) /\ <" B A X "> ( cgrG ` G ) <" E D y "> ) -> y e. P )
100 simpr 
 |-  ( ( ( ( ( ( ( ph /\ A = C ) /\ -. ( B e. ( A L X ) \/ A = X ) ) /\ x e. P ) /\ -. x e. ( D L E ) ) /\ y e. P ) /\ <" B A X "> ( cgrG ` G ) <" E D y "> ) -> <" B A X "> ( cgrG ` G ) <" E D y "> )
101 1 21 13 18 93 94 95 96 97 98 99 100 cgr3simp2 
 |-  ( ( ( ( ( ( ( ph /\ A = C ) /\ -. ( B e. ( A L X ) \/ A = X ) ) /\ x e. P ) /\ -. x e. ( D L E ) ) /\ y e. P ) /\ <" B A X "> ( cgrG ` G ) <" E D y "> ) -> ( A ( dist ` G ) X ) = ( D ( dist ` G ) y ) )
102 1 21 13 18 93 94 95 96 97 98 99 100 cgr3simp3 
 |-  ( ( ( ( ( ( ( ph /\ A = C ) /\ -. ( B e. ( A L X ) \/ A = X ) ) /\ x e. P ) /\ -. x e. ( D L E ) ) /\ y e. P ) /\ <" B A X "> ( cgrG ` G ) <" E D y "> ) -> ( X ( dist ` G ) B ) = ( y ( dist ` G ) E ) )
103 1 21 13 93 96 94 99 97 102 tgcgrcomlr 
 |-  ( ( ( ( ( ( ( ph /\ A = C ) /\ -. ( B e. ( A L X ) \/ A = X ) ) /\ x e. P ) /\ -. x e. ( D L E ) ) /\ y e. P ) /\ <" B A X "> ( cgrG ` G ) <" E D y "> ) -> ( B ( dist ` G ) X ) = ( E ( dist ` G ) y ) )
104 45 ad5antr 
 |-  ( ( ( ( ( ( ( ph /\ A = C ) /\ -. ( B e. ( A L X ) \/ A = X ) ) /\ x e. P ) /\ -. x e. ( D L E ) ) /\ y e. P ) /\ <" B A X "> ( cgrG ` G ) <" E D y "> ) -> C e. P )
105 47 ad5antr 
 |-  ( ( ( ( ( ( ( ph /\ A = C ) /\ -. ( B e. ( A L X ) \/ A = X ) ) /\ x e. P ) /\ -. x e. ( D L E ) ) /\ y e. P ) /\ <" B A X "> ( cgrG ` G ) <" E D y "> ) -> F e. P )
106 1 21 13 93 95 96 98 99 101 tgcgrcomlr 
 |-  ( ( ( ( ( ( ( ph /\ A = C ) /\ -. ( B e. ( A L X ) \/ A = X ) ) /\ x e. P ) /\ -. x e. ( D L E ) ) /\ y e. P ) /\ <" B A X "> ( cgrG ` G ) <" E D y "> ) -> ( X ( dist ` G ) A ) = ( y ( dist ` G ) D ) )
107 simp-6r 
 |-  ( ( ( ( ( ( ( ph /\ A = C ) /\ -. ( B e. ( A L X ) \/ A = X ) ) /\ x e. P ) /\ -. x e. ( D L E ) ) /\ y e. P ) /\ <" B A X "> ( cgrG ` G ) <" E D y "> ) -> A = C )
108 107 oveq2d 
 |-  ( ( ( ( ( ( ( ph /\ A = C ) /\ -. ( B e. ( A L X ) \/ A = X ) ) /\ x e. P ) /\ -. x e. ( D L E ) ) /\ y e. P ) /\ <" B A X "> ( cgrG ` G ) <" E D y "> ) -> ( X ( dist ` G ) A ) = ( X ( dist ` G ) C ) )
109 51 ad5antr 
 |-  ( ( ( ( ( ( ( ph /\ A = C ) /\ -. ( B e. ( A L X ) \/ A = X ) ) /\ x e. P ) /\ -. x e. ( D L E ) ) /\ y e. P ) /\ <" B A X "> ( cgrG ` G ) <" E D y "> ) -> D = F )
110 109 oveq2d 
 |-  ( ( ( ( ( ( ( ph /\ A = C ) /\ -. ( B e. ( A L X ) \/ A = X ) ) /\ x e. P ) /\ -. x e. ( D L E ) ) /\ y e. P ) /\ <" B A X "> ( cgrG ` G ) <" E D y "> ) -> ( y ( dist ` G ) D ) = ( y ( dist ` G ) F ) )
111 106 108 110 3eqtr3d 
 |-  ( ( ( ( ( ( ( ph /\ A = C ) /\ -. ( B e. ( A L X ) \/ A = X ) ) /\ x e. P ) /\ -. x e. ( D L E ) ) /\ y e. P ) /\ <" B A X "> ( cgrG ` G ) <" E D y "> ) -> ( X ( dist ` G ) C ) = ( y ( dist ` G ) F ) )
112 1 21 13 93 96 104 99 105 111 tgcgrcomlr 
 |-  ( ( ( ( ( ( ( ph /\ A = C ) /\ -. ( B e. ( A L X ) \/ A = X ) ) /\ x e. P ) /\ -. x e. ( D L E ) ) /\ y e. P ) /\ <" B A X "> ( cgrG ` G ) <" E D y "> ) -> ( C ( dist ` G ) X ) = ( F ( dist ` G ) y ) )
113 101 103 112 3jca 
 |-  ( ( ( ( ( ( ( ph /\ A = C ) /\ -. ( B e. ( A L X ) \/ A = X ) ) /\ x e. P ) /\ -. x e. ( D L E ) ) /\ y e. P ) /\ <" B A X "> ( cgrG ` G ) <" E D y "> ) -> ( ( A ( dist ` G ) X ) = ( D ( dist ` G ) y ) /\ ( B ( dist ` G ) X ) = ( E ( dist ` G ) y ) /\ ( C ( dist ` G ) X ) = ( F ( dist ` G ) y ) ) )
114 1 21 13 18 93 95 94 104 96 98 97 105 99 tgcgr4 
 |-  ( ( ( ( ( ( ( ph /\ A = C ) /\ -. ( B e. ( A L X ) \/ A = X ) ) /\ x e. P ) /\ -. x e. ( D L E ) ) /\ y e. P ) /\ <" B A X "> ( cgrG ` G ) <" E D y "> ) -> ( <" A B C X "> ( cgrG ` G ) <" D E F y "> <-> ( <" A B C "> ( cgrG ` G ) <" D E F "> /\ ( ( A ( dist ` G ) X ) = ( D ( dist ` G ) y ) /\ ( B ( dist ` G ) X ) = ( E ( dist ` G ) y ) /\ ( C ( dist ` G ) X ) = ( F ( dist ` G ) y ) ) ) ) )
115 92 113 114 mpbir2and 
 |-  ( ( ( ( ( ( ( ph /\ A = C ) /\ -. ( B e. ( A L X ) \/ A = X ) ) /\ x e. P ) /\ -. x e. ( D L E ) ) /\ y e. P ) /\ <" B A X "> ( cgrG ` G ) <" E D y "> ) -> <" A B C X "> ( cgrG ` G ) <" D E F y "> )
116 115 ex 
 |-  ( ( ( ( ( ( ph /\ A = C ) /\ -. ( B e. ( A L X ) \/ A = X ) ) /\ x e. P ) /\ -. x e. ( D L E ) ) /\ y e. P ) -> ( <" B A X "> ( cgrG ` G ) <" E D y "> -> <" A B C X "> ( cgrG ` G ) <" D E F y "> ) )
117 116 adantrd 
 |-  ( ( ( ( ( ( ph /\ A = C ) /\ -. ( B e. ( A L X ) \/ A = X ) ) /\ x e. P ) /\ -. x e. ( D L E ) ) /\ y e. P ) -> ( ( <" B A X "> ( cgrG ` G ) <" E D y "> /\ y ( ( hpG ` G ) ` ( E L D ) ) x ) -> <" A B C X "> ( cgrG ` G ) <" D E F y "> ) )
118 117 reximdva 
 |-  ( ( ( ( ( ph /\ A = C ) /\ -. ( B e. ( A L X ) \/ A = X ) ) /\ x e. P ) /\ -. x e. ( D L E ) ) -> ( E. y e. P ( <" B A X "> ( cgrG ` G ) <" E D y "> /\ y ( ( hpG ` G ) ` ( E L D ) ) x ) -> E. y e. P <" A B C X "> ( cgrG ` G ) <" D E F y "> ) )
119 91 118 mpd 
 |-  ( ( ( ( ( ph /\ A = C ) /\ -. ( B e. ( A L X ) \/ A = X ) ) /\ x e. P ) /\ -. x e. ( D L E ) ) -> E. y e. P <" A B C X "> ( cgrG ` G ) <" D E F y "> )
120 1 9 13 63 67 69 65 79 ncoltgdim2 
 |-  ( ( ( ph /\ A = C ) /\ -. ( B e. ( A L X ) \/ A = X ) ) -> G TarskiGDim>= 2 )
121 1 13 9 63 120 73 71 82 tglowdim2ln 
 |-  ( ( ( ph /\ A = C ) /\ -. ( B e. ( A L X ) \/ A = X ) ) -> E. x e. P -. x e. ( D L E ) )
122 119 121 r19.29a 
 |-  ( ( ( ph /\ A = C ) /\ -. ( B e. ( A L X ) \/ A = X ) ) -> E. y e. P <" A B C X "> ( cgrG ` G ) <" D E F y "> )
123 61 122 pm2.61dan 
 |-  ( ( ph /\ A = C ) -> E. y e. P <" A B C X "> ( cgrG ` G ) <" D E F y "> )
124 1 9 13 2 3 5 10 12 colcom 
 |-  ( ph -> ( X e. ( C L A ) \/ C = A ) )
125 1 9 13 2 5 3 10 124 colrot1 
 |-  ( ph -> ( C e. ( A L X ) \/ A = X ) )
126 1 9 13 2 3 5 10 18 6 8 21 125 49 lnext 
 |-  ( ph -> E. y e. P <" A C X "> ( cgrG ` G ) <" D F y "> )
127 126 adantr 
 |-  ( ( ph /\ A =/= C ) -> E. y e. P <" A C X "> ( cgrG ` G ) <" D F y "> )
128 11 ad3antrrr 
 |-  ( ( ( ( ph /\ A =/= C ) /\ y e. P ) /\ <" A C X "> ( cgrG ` G ) <" D F y "> ) -> <" A B C "> ( cgrG ` G ) <" D E F "> )
129 2 ad3antrrr 
 |-  ( ( ( ( ph /\ A =/= C ) /\ y e. P ) /\ <" A C X "> ( cgrG ` G ) <" D F y "> ) -> G e. TarskiG )
130 10 ad3antrrr 
 |-  ( ( ( ( ph /\ A =/= C ) /\ y e. P ) /\ <" A C X "> ( cgrG ` G ) <" D F y "> ) -> X e. P )
131 3 ad3antrrr 
 |-  ( ( ( ( ph /\ A =/= C ) /\ y e. P ) /\ <" A C X "> ( cgrG ` G ) <" D F y "> ) -> A e. P )
132 simplr 
 |-  ( ( ( ( ph /\ A =/= C ) /\ y e. P ) /\ <" A C X "> ( cgrG ` G ) <" D F y "> ) -> y e. P )
133 6 ad3antrrr 
 |-  ( ( ( ( ph /\ A =/= C ) /\ y e. P ) /\ <" A C X "> ( cgrG ` G ) <" D F y "> ) -> D e. P )
134 5 ad3antrrr 
 |-  ( ( ( ( ph /\ A =/= C ) /\ y e. P ) /\ <" A C X "> ( cgrG ` G ) <" D F y "> ) -> C e. P )
135 8 ad3antrrr 
 |-  ( ( ( ( ph /\ A =/= C ) /\ y e. P ) /\ <" A C X "> ( cgrG ` G ) <" D F y "> ) -> F e. P )
136 simpr 
 |-  ( ( ( ( ph /\ A =/= C ) /\ y e. P ) /\ <" A C X "> ( cgrG ` G ) <" D F y "> ) -> <" A C X "> ( cgrG ` G ) <" D F y "> )
137 1 21 13 18 129 131 134 130 133 135 132 136 cgr3simp3 
 |-  ( ( ( ( ph /\ A =/= C ) /\ y e. P ) /\ <" A C X "> ( cgrG ` G ) <" D F y "> ) -> ( X ( dist ` G ) A ) = ( y ( dist ` G ) D ) )
138 1 21 13 129 130 131 132 133 137 tgcgrcomlr 
 |-  ( ( ( ( ph /\ A =/= C ) /\ y e. P ) /\ <" A C X "> ( cgrG ` G ) <" D F y "> ) -> ( A ( dist ` G ) X ) = ( D ( dist ` G ) y ) )
139 4 ad3antrrr 
 |-  ( ( ( ( ph /\ A =/= C ) /\ y e. P ) /\ <" A C X "> ( cgrG ` G ) <" D F y "> ) -> B e. P )
140 7 ad3antrrr 
 |-  ( ( ( ( ph /\ A =/= C ) /\ y e. P ) /\ <" A C X "> ( cgrG ` G ) <" D F y "> ) -> E e. P )
141 125 ad3antrrr 
 |-  ( ( ( ( ph /\ A =/= C ) /\ y e. P ) /\ <" A C X "> ( cgrG ` G ) <" D F y "> ) -> ( C e. ( A L X ) \/ A = X ) )
142 23 ad3antrrr 
 |-  ( ( ( ( ph /\ A =/= C ) /\ y e. P ) /\ <" A C X "> ( cgrG ` G ) <" D F y "> ) -> ( A ( dist ` G ) B ) = ( D ( dist ` G ) E ) )
143 1 21 13 18 2 3 4 5 6 7 8 11 cgr3simp2 
 |-  ( ph -> ( B ( dist ` G ) C ) = ( E ( dist ` G ) F ) )
144 1 21 13 2 4 5 7 8 143 tgcgrcomlr 
 |-  ( ph -> ( C ( dist ` G ) B ) = ( F ( dist ` G ) E ) )
145 144 ad3antrrr 
 |-  ( ( ( ( ph /\ A =/= C ) /\ y e. P ) /\ <" A C X "> ( cgrG ` G ) <" D F y "> ) -> ( C ( dist ` G ) B ) = ( F ( dist ` G ) E ) )
146 simpllr 
 |-  ( ( ( ( ph /\ A =/= C ) /\ y e. P ) /\ <" A C X "> ( cgrG ` G ) <" D F y "> ) -> A =/= C )
147 1 9 13 129 131 134 130 18 133 135 21 139 132 140 141 136 142 145 146 tgfscgr 
 |-  ( ( ( ( ph /\ A =/= C ) /\ y e. P ) /\ <" A C X "> ( cgrG ` G ) <" D F y "> ) -> ( X ( dist ` G ) B ) = ( y ( dist ` G ) E ) )
148 1 21 13 129 130 139 132 140 147 tgcgrcomlr 
 |-  ( ( ( ( ph /\ A =/= C ) /\ y e. P ) /\ <" A C X "> ( cgrG ` G ) <" D F y "> ) -> ( B ( dist ` G ) X ) = ( E ( dist ` G ) y ) )
149 1 21 13 18 129 131 134 130 133 135 132 136 cgr3simp2 
 |-  ( ( ( ( ph /\ A =/= C ) /\ y e. P ) /\ <" A C X "> ( cgrG ` G ) <" D F y "> ) -> ( C ( dist ` G ) X ) = ( F ( dist ` G ) y ) )
150 138 148 149 3jca 
 |-  ( ( ( ( ph /\ A =/= C ) /\ y e. P ) /\ <" A C X "> ( cgrG ` G ) <" D F y "> ) -> ( ( A ( dist ` G ) X ) = ( D ( dist ` G ) y ) /\ ( B ( dist ` G ) X ) = ( E ( dist ` G ) y ) /\ ( C ( dist ` G ) X ) = ( F ( dist ` G ) y ) ) )
151 1 21 13 18 129 131 139 134 130 133 140 135 132 tgcgr4 
 |-  ( ( ( ( ph /\ A =/= C ) /\ y e. P ) /\ <" A C X "> ( cgrG ` G ) <" D F y "> ) -> ( <" A B C X "> ( cgrG ` G ) <" D E F y "> <-> ( <" A B C "> ( cgrG ` G ) <" D E F "> /\ ( ( A ( dist ` G ) X ) = ( D ( dist ` G ) y ) /\ ( B ( dist ` G ) X ) = ( E ( dist ` G ) y ) /\ ( C ( dist ` G ) X ) = ( F ( dist ` G ) y ) ) ) ) )
152 128 150 151 mpbir2and 
 |-  ( ( ( ( ph /\ A =/= C ) /\ y e. P ) /\ <" A C X "> ( cgrG ` G ) <" D F y "> ) -> <" A B C X "> ( cgrG ` G ) <" D E F y "> )
153 152 ex 
 |-  ( ( ( ph /\ A =/= C ) /\ y e. P ) -> ( <" A C X "> ( cgrG ` G ) <" D F y "> -> <" A B C X "> ( cgrG ` G ) <" D E F y "> ) )
154 153 reximdva 
 |-  ( ( ph /\ A =/= C ) -> ( E. y e. P <" A C X "> ( cgrG ` G ) <" D F y "> -> E. y e. P <" A B C X "> ( cgrG ` G ) <" D E F y "> ) )
155 127 154 mpd 
 |-  ( ( ph /\ A =/= C ) -> E. y e. P <" A B C X "> ( cgrG ` G ) <" D E F y "> )
156 123 155 pm2.61dane 
 |-  ( ph -> E. y e. P <" A B C X "> ( cgrG ` G ) <" D E F y "> )