MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  cgrg3col4 Structured version   Visualization version   Unicode version

Theorem cgrg3col4 24933
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.)
Hypotheses
Ref Expression
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
Ref Expression
cgrg3col4  |-  ( ph  ->  E. y  e.  P  <" A B C X "> (cgrG `  G ) <" D E F y "> )
Distinct variable groups:    y, A    y, B    y, C    y, D    y, E    y, F    y, G    y, L    y, P    y, X    ph, y

Proof of Theorem cgrg3col4
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 isleag.p . . . . 5  |-  P  =  ( Base `  G
)
2 cgrg3col4.l . . . . 5  |-  L  =  (LineG `  G )
3 eqid 2462 . . . . 5  |-  (Itv `  G )  =  (Itv
`  G )
4 isleag.g . . . . . 6  |-  ( ph  ->  G  e. TarskiG )
54ad2antrr 737 . . . . 5  |-  ( ( ( ph  /\  A  =  C )  /\  ( B  e.  ( A L X )  \/  A  =  X ) )  ->  G  e. TarskiG )
6 isleag.a . . . . . 6  |-  ( ph  ->  A  e.  P )
76ad2antrr 737 . . . . 5  |-  ( ( ( ph  /\  A  =  C )  /\  ( B  e.  ( A L X )  \/  A  =  X ) )  ->  A  e.  P )
8 isleag.b . . . . . 6  |-  ( ph  ->  B  e.  P )
98ad2antrr 737 . . . . 5  |-  ( ( ( ph  /\  A  =  C )  /\  ( B  e.  ( A L X )  \/  A  =  X ) )  ->  B  e.  P )
10 cgrg3col4.x . . . . . 6  |-  ( ph  ->  X  e.  P )
1110ad2antrr 737 . . . . 5  |-  ( ( ( ph  /\  A  =  C )  /\  ( B  e.  ( A L X )  \/  A  =  X ) )  ->  X  e.  P )
12 eqid 2462 . . . . 5  |-  (cgrG `  G )  =  (cgrG `  G )
13 isleag.d . . . . . 6  |-  ( ph  ->  D  e.  P )
1413ad2antrr 737 . . . . 5  |-  ( ( ( ph  /\  A  =  C )  /\  ( B  e.  ( A L X )  \/  A  =  X ) )  ->  D  e.  P )
15 isleag.e . . . . . 6  |-  ( ph  ->  E  e.  P )
1615ad2antrr 737 . . . . 5  |-  ( ( ( ph  /\  A  =  C )  /\  ( B  e.  ( A L X )  \/  A  =  X ) )  ->  E  e.  P )
17 eqid 2462 . . . . 5  |-  ( dist `  G )  =  (
dist `  G )
18 simpr 467 . . . . 5  |-  ( ( ( ph  /\  A  =  C )  /\  ( B  e.  ( A L X )  \/  A  =  X ) )  -> 
( B  e.  ( A L X )  \/  A  =  X ) )
19 isleag.c . . . . . . 7  |-  ( ph  ->  C  e.  P )
20 isleag.f . . . . . . 7  |-  ( ph  ->  F  e.  P )
21 cgrg3col4.1 . . . . . . 7  |-  ( ph  ->  <" A B C "> (cgrG `  G ) <" D E F "> )
221, 17, 3, 12, 4, 6, 8, 19, 13, 15, 20, 21cgr3simp1 24614 . . . . . 6  |-  ( ph  ->  ( A ( dist `  G ) B )  =  ( D (
dist `  G ) E ) )
2322ad2antrr 737 . . . . 5  |-  ( ( ( ph  /\  A  =  C )  /\  ( B  e.  ( A L X )  \/  A  =  X ) )  -> 
( A ( dist `  G ) B )  =  ( D (
dist `  G ) E ) )
241, 2, 3, 5, 7, 9, 11, 12, 14, 16, 17, 18, 23lnext 24661 . . . 4  |-  ( ( ( ph  /\  A  =  C )  /\  ( B  e.  ( A L X )  \/  A  =  X ) )  ->  E. y  e.  P  <" A B X "> (cgrG `  G ) <" D E y "> )
2521ad4antr 743 . . . . . . . 8  |-  ( ( ( ( ( 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 "> )
265ad2antrr 737 . . . . . . . . . 10  |-  ( ( ( ( ( ph  /\  A  =  C )  /\  ( B  e.  ( A L X )  \/  A  =  X ) )  /\  y  e.  P )  /\  <" A B X "> (cgrG `  G ) <" D E y "> )  ->  G  e. TarskiG )
2711ad2antrr 737 . . . . . . . . . 10  |-  ( ( ( ( ( ph  /\  A  =  C )  /\  ( B  e.  ( A L X )  \/  A  =  X ) )  /\  y  e.  P )  /\  <" A B X "> (cgrG `  G ) <" D E y "> )  ->  X  e.  P
)
287ad2antrr 737 . . . . . . . . . 10  |-  ( ( ( ( ( ph  /\  A  =  C )  /\  ( B  e.  ( A L X )  \/  A  =  X ) )  /\  y  e.  P )  /\  <" A B X "> (cgrG `  G ) <" D E y "> )  ->  A  e.  P
)
29 simplr 767 . . . . . . . . . 10  |-  ( ( ( ( ( ph  /\  A  =  C )  /\  ( B  e.  ( A L X )  \/  A  =  X ) )  /\  y  e.  P )  /\  <" A B X "> (cgrG `  G ) <" D E y "> )  ->  y  e.  P
)
3014ad2antrr 737 . . . . . . . . . 10  |-  ( ( ( ( ( ph  /\  A  =  C )  /\  ( B  e.  ( A L X )  \/  A  =  X ) )  /\  y  e.  P )  /\  <" A B X "> (cgrG `  G ) <" D E y "> )  ->  D  e.  P
)
319ad2antrr 737 . . . . . . . . . . 11  |-  ( ( ( ( ( ph  /\  A  =  C )  /\  ( B  e.  ( A L X )  \/  A  =  X ) )  /\  y  e.  P )  /\  <" A B X "> (cgrG `  G ) <" D E y "> )  ->  B  e.  P
)
3216ad2antrr 737 . . . . . . . . . . 11  |-  ( ( ( ( ( ph  /\  A  =  C )  /\  ( B  e.  ( A L X )  \/  A  =  X ) )  /\  y  e.  P )  /\  <" A B X "> (cgrG `  G ) <" D E y "> )  ->  E  e.  P
)
33 simpr 467 . . . . . . . . . . 11  |-  ( ( ( ( ( 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 "> )
341, 17, 3, 12, 26, 28, 31, 27, 30, 32, 29, 33cgr3simp3 24616 . . . . . . . . . 10  |-  ( ( ( ( ( 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 ) )
351, 17, 3, 26, 27, 28, 29, 30, 34tgcgrcomlr 24573 . . . . . . . . 9  |-  ( ( ( ( ( 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 ) )
361, 17, 3, 12, 26, 28, 31, 27, 30, 32, 29, 33cgr3simp2 24615 . . . . . . . . 9  |-  ( ( ( ( ( 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 ) )
3719ad4antr 743 . . . . . . . . . 10  |-  ( ( ( ( ( ph  /\  A  =  C )  /\  ( B  e.  ( A L X )  \/  A  =  X ) )  /\  y  e.  P )  /\  <" A B X "> (cgrG `  G ) <" D E y "> )  ->  C  e.  P
)
3820ad4antr 743 . . . . . . . . . 10  |-  ( ( ( ( ( ph  /\  A  =  C )  /\  ( B  e.  ( A L X )  \/  A  =  X ) )  /\  y  e.  P )  /\  <" A B X "> (cgrG `  G ) <" D E y "> )  ->  F  e.  P
)
39 simpr 467 . . . . . . . . . . . . 13  |-  ( (
ph  /\  A  =  C )  ->  A  =  C )
4039ad3antrrr 741 . . . . . . . . . . . 12  |-  ( ( ( ( ( ph  /\  A  =  C )  /\  ( B  e.  ( A L X )  \/  A  =  X ) )  /\  y  e.  P )  /\  <" A B X "> (cgrG `  G ) <" D E y "> )  ->  A  =  C )
4140oveq2d 6331 . . . . . . . . . . 11  |-  ( ( ( ( ( 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 ) )
424adantr 471 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  A  =  C )  ->  G  e. TarskiG )
436adantr 471 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  A  =  C )  ->  A  e.  P )
4419adantr 471 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  A  =  C )  ->  C  e.  P )
4513adantr 471 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  A  =  C )  ->  D  e.  P )
4620adantr 471 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  A  =  C )  ->  F  e.  P )
471, 17, 3, 12, 4, 6, 8, 19, 13, 15, 20, 21cgr3simp3 24616 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( C ( dist `  G ) A )  =  ( F (
dist `  G ) D ) )
481, 17, 3, 4, 19, 6, 20, 13, 47tgcgrcomlr 24573 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( A ( dist `  G ) C )  =  ( D (
dist `  G ) F ) )
4948adantr 471 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  A  =  C )  ->  ( A ( dist `  G
) C )  =  ( D ( dist `  G ) F ) )
501, 17, 3, 42, 43, 44, 45, 46, 49, 39tgcgreq 24575 . . . . . . . . . . . . 13  |-  ( (
ph  /\  A  =  C )  ->  D  =  F )
5150ad3antrrr 741 . . . . . . . . . . . 12  |-  ( ( ( ( ( ph  /\  A  =  C )  /\  ( B  e.  ( A L X )  \/  A  =  X ) )  /\  y  e.  P )  /\  <" A B X "> (cgrG `  G ) <" D E y "> )  ->  D  =  F )
5251oveq2d 6331 . . . . . . . . . . 11  |-  ( ( ( ( ( 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 ) )
5334, 41, 523eqtr3d 2504 . . . . . . . . . 10  |-  ( ( ( ( ( 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 ) )
541, 17, 3, 26, 27, 37, 29, 38, 53tgcgrcomlr 24573 . . . . . . . . 9  |-  ( ( ( ( ( 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 ) )
5535, 36, 543jca 1194 . . . . . . . 8  |-  ( ( ( ( ( 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 ) ) )
5625, 55jca 539 . . . . . . 7  |-  ( ( ( ( ( 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 ">  /\  (
( A ( dist `  G ) X )  =  ( D (
dist `  G )
y )  /\  ( B ( dist `  G
) X )  =  ( E ( dist `  G ) y )  /\  ( C (
dist `  G ) X )  =  ( F ( dist `  G
) y ) ) ) )
571, 17, 3, 12, 26, 28, 31, 37, 27, 30, 32, 38, 29tgcgr4 24625 . . . . . . 7  |-  ( ( ( ( ( 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 ) ) ) ) )
5856, 57mpbird 240 . . . . . 6  |-  ( ( ( ( ( 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 "> )
5958ex 440 . . . . 5  |-  ( ( ( ( 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 "> )
)
6059reximdva 2874 . . . 4  |-  ( ( ( 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 "> ) )
6124, 60mpd 15 . . 3  |-  ( ( ( 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 2462 . . . . . 6  |-  (hlG `  G )  =  (hlG
`  G )
6342adantr 471 . . . . . . 7  |-  ( ( ( ph  /\  A  =  C )  /\  -.  ( B  e.  ( A L X )  \/  A  =  X ) )  ->  G  e. TarskiG )
6463ad2antrr 737 . . . . . 6  |-  ( ( ( ( ( ph  /\  A  =  C )  /\  -.  ( B  e.  ( A L X )  \/  A  =  X ) )  /\  x  e.  P )  /\  -.  x  e.  ( D L E ) )  ->  G  e. TarskiG )
658ad2antrr 737 . . . . . . 7  |-  ( ( ( ph  /\  A  =  C )  /\  -.  ( B  e.  ( A L X )  \/  A  =  X ) )  ->  B  e.  P )
6665ad2antrr 737 . . . . . 6  |-  ( ( ( ( ( ph  /\  A  =  C )  /\  -.  ( B  e.  ( A L X )  \/  A  =  X ) )  /\  x  e.  P )  /\  -.  x  e.  ( D L E ) )  ->  B  e.  P )
6743adantr 471 . . . . . . 7  |-  ( ( ( ph  /\  A  =  C )  /\  -.  ( B  e.  ( A L X )  \/  A  =  X ) )  ->  A  e.  P )
6867ad2antrr 737 . . . . . 6  |-  ( ( ( ( ( ph  /\  A  =  C )  /\  -.  ( B  e.  ( A L X )  \/  A  =  X ) )  /\  x  e.  P )  /\  -.  x  e.  ( D L E ) )  ->  A  e.  P )
6910ad2antrr 737 . . . . . . 7  |-  ( ( ( ph  /\  A  =  C )  /\  -.  ( B  e.  ( A L X )  \/  A  =  X ) )  ->  X  e.  P )
7069ad2antrr 737 . . . . . 6  |-  ( ( ( ( ( ph  /\  A  =  C )  /\  -.  ( B  e.  ( A L X )  \/  A  =  X ) )  /\  x  e.  P )  /\  -.  x  e.  ( D L E ) )  ->  X  e.  P )
7115ad2antrr 737 . . . . . . 7  |-  ( ( ( ph  /\  A  =  C )  /\  -.  ( B  e.  ( A L X )  \/  A  =  X ) )  ->  E  e.  P )
7271ad2antrr 737 . . . . . 6  |-  ( ( ( ( ( ph  /\  A  =  C )  /\  -.  ( B  e.  ( A L X )  \/  A  =  X ) )  /\  x  e.  P )  /\  -.  x  e.  ( D L E ) )  ->  E  e.  P )
7345adantr 471 . . . . . . 7  |-  ( ( ( ph  /\  A  =  C )  /\  -.  ( B  e.  ( A L X )  \/  A  =  X ) )  ->  D  e.  P )
7473ad2antrr 737 . . . . . 6  |-  ( ( ( ( ( ph  /\  A  =  C )  /\  -.  ( B  e.  ( A L X )  \/  A  =  X ) )  /\  x  e.  P )  /\  -.  x  e.  ( D L E ) )  ->  D  e.  P )
75 simplr 767 . . . . . 6  |-  ( ( ( ( ( ph  /\  A  =  C )  /\  -.  ( B  e.  ( A L X )  \/  A  =  X ) )  /\  x  e.  P )  /\  -.  x  e.  ( D L E ) )  ->  x  e.  P )
76 simpr 467 . . . . . . 7  |-  ( ( ( ph  /\  A  =  C )  /\  -.  ( B  e.  ( A L X )  \/  A  =  X ) )  ->  -.  ( B  e.  ( A L X )  \/  A  =  X ) )
7776ad2antrr 737 . . . . . 6  |-  ( ( ( ( ( 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 ) )
78 simpr 467 . . . . . . . . . 10  |-  ( ( ( ( ( ph  /\  A  =  C )  /\  -.  ( B  e.  ( A L X )  \/  A  =  X ) )  /\  x  e.  P )  /\  -.  x  e.  ( D L E ) )  ->  -.  x  e.  ( D L E ) )
7922ad2antrr 737 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  A  =  C )  /\  -.  ( B  e.  ( A L X )  \/  A  =  X ) )  ->  ( A
( dist `  G ) B )  =  ( D ( dist `  G
) E ) )
801, 3, 2, 63, 65, 67, 69, 76ncolne1 24719 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  A  =  C )  /\  -.  ( B  e.  ( A L X )  \/  A  =  X ) )  ->  B  =/=  A )
8180necomd 2691 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  A  =  C )  /\  -.  ( B  e.  ( A L X )  \/  A  =  X ) )  ->  A  =/=  B )
821, 17, 3, 63, 67, 65, 73, 71, 79, 81tgcgrneq 24576 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  A  =  C )  /\  -.  ( B  e.  ( A L X )  \/  A  =  X ) )  ->  D  =/=  E )
8382ad2antrr 737 . . . . . . . . . . 11  |-  ( ( ( ( ( ph  /\  A  =  C )  /\  -.  ( B  e.  ( A L X )  \/  A  =  X ) )  /\  x  e.  P )  /\  -.  x  e.  ( D L E ) )  ->  D  =/=  E )
8483neneqd 2640 . . . . . . . . . 10  |-  ( ( ( ( ( ph  /\  A  =  C )  /\  -.  ( B  e.  ( A L X )  \/  A  =  X ) )  /\  x  e.  P )  /\  -.  x  e.  ( D L E ) )  ->  -.  D  =  E )
8578, 84jca 539 . . . . . . . . 9  |-  ( ( ( ( ( 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 )
)
86 ioran 497 . . . . . . . . 9  |-  ( -.  ( x  e.  ( D L E )  \/  D  =  E )  <->  ( -.  x  e.  ( D L E )  /\  -.  D  =  E ) )
8785, 86sylibr 217 . . . . . . . 8  |-  ( ( ( ( ( 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 ) )
881, 2, 3, 64, 74, 72, 75, 87ncolcom 24655 . . . . . . 7  |-  ( ( ( ( ( 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 ) )
891, 2, 3, 64, 72, 74, 75, 88ncolrot1 24656 . . . . . 6  |-  ( ( ( ( ( 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 ) )
901, 17, 3, 4, 6, 8, 13, 15, 22tgcgrcomlr 24573 . . . . . . 7  |-  ( ph  ->  ( B ( dist `  G ) A )  =  ( E (
dist `  G ) D ) )
9190ad4antr 743 . . . . . 6  |-  ( ( ( ( ( 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 ) )
921, 17, 3, 2, 62, 64, 66, 68, 70, 72, 74, 75, 77, 89, 91trgcopy 24895 . . . . 5  |-  ( ( ( ( ( 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 ) )
9321ad6antr 747 . . . . . . . . . 10  |-  ( ( ( ( ( ( ( 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 "> )
9464ad2antrr 737 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( ( 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 )
9566ad2antrr 737 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( ( 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
)
9668ad2antrr 737 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( ( 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
)
9770ad2antrr 737 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( ( 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
)
9872ad2antrr 737 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( ( 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
)
9974ad2antrr 737 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( ( 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
)
100 simplr 767 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( ( 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
)
101 simpr 467 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( ( 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 "> )
1021, 17, 3, 12, 94, 95, 96, 97, 98, 99, 100, 101cgr3simp2 24615 . . . . . . . . . . 11  |-  ( ( ( ( ( ( ( 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 ) )
1031, 17, 3, 12, 94, 95, 96, 97, 98, 99, 100, 101cgr3simp3 24616 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( ( 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 ) )
1041, 17, 3, 94, 97, 95, 100, 98, 103tgcgrcomlr 24573 . . . . . . . . . . 11  |-  ( ( ( ( ( ( ( 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 ) )
10544ad5antr 745 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( ( 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
)
10646ad5antr 745 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( ( 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
)
1071, 17, 3, 94, 96, 97, 99, 100, 102tgcgrcomlr 24573 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( 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 ) )
108 simp-6r 786 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( ( 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 )
109108oveq2d 6331 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( 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 ) )
11050ad5antr 745 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( ( 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 )
111110oveq2d 6331 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( 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 ) )
112107, 109, 1113eqtr3d 2504 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( ( 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 ) )
1131, 17, 3, 94, 97, 105, 100, 106, 112tgcgrcomlr 24573 . . . . . . . . . . 11  |-  ( ( ( ( ( ( ( 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 ) )
114102, 104, 1133jca 1194 . . . . . . . . . 10  |-  ( ( ( ( ( ( ( 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 ) ) )
11593, 114jca 539 . . . . . . . . 9  |-  ( ( ( ( ( ( ( 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 ">  /\  (
( A ( dist `  G ) X )  =  ( D (
dist `  G )
y )  /\  ( B ( dist `  G
) X )  =  ( E ( dist `  G ) y )  /\  ( C (
dist `  G ) X )  =  ( F ( dist `  G
) y ) ) ) )
1161, 17, 3, 12, 94, 96, 95, 105, 97, 99, 98, 106, 100tgcgr4 24625 . . . . . . . . 9  |-  ( ( ( ( ( ( ( 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 ) ) ) ) )
117115, 116mpbird 240 . . . . . . . 8  |-  ( ( ( ( ( ( ( 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 "> )
118117ex 440 . . . . . . 7  |-  ( ( ( ( ( (
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 "> )
)
119118adantrd 474 . . . . . 6  |-  ( ( ( ( ( (
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 "> )
)
120119reximdva 2874 . . . . 5  |-  ( ( ( ( ( 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 "> )
)
12192, 120mpd 15 . . . 4  |-  ( ( ( ( ( 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 "> )
1221, 2, 3, 63, 67, 69, 65, 76ncoltgdim2 24659 . . . . 5  |-  ( ( ( ph  /\  A  =  C )  /\  -.  ( B  e.  ( A L X )  \/  A  =  X ) )  ->  GDimTarskiG 2 )
1231, 3, 2, 63, 122, 73, 71, 82tglowdim2ln 24745 . . . 4  |-  ( ( ( ph  /\  A  =  C )  /\  -.  ( B  e.  ( A L X )  \/  A  =  X ) )  ->  E. x  e.  P  -.  x  e.  ( D L E ) )
124121, 123r19.29a 2944 . . 3  |-  ( ( ( ph  /\  A  =  C )  /\  -.  ( B  e.  ( A L X )  \/  A  =  X ) )  ->  E. y  e.  P  <" A B C X "> (cgrG `  G ) <" D E F y "> )
12561, 124pm2.61dan 805 . 2  |-  ( (
ph  /\  A  =  C )  ->  E. y  e.  P  <" A B C X "> (cgrG `  G ) <" D E F y "> )
126 cgrg3col4.2 . . . . . . 7  |-  ( ph  ->  ( X  e.  ( A L C )  \/  A  =  C ) )
1271, 2, 3, 4, 6, 19, 10, 126colcom 24652 . . . . . 6  |-  ( ph  ->  ( X  e.  ( C L A )  \/  C  =  A ) )
1281, 2, 3, 4, 19, 6, 10, 127colrot1 24653 . . . . 5  |-  ( ph  ->  ( C  e.  ( A L X )  \/  A  =  X ) )
1291, 2, 3, 4, 6, 19, 10, 12, 13, 20, 17, 128, 48lnext 24661 . . . 4  |-  ( ph  ->  E. y  e.  P  <" A C X "> (cgrG `  G ) <" D F y "> )
130129adantr 471 . . 3  |-  ( (
ph  /\  A  =/=  C )  ->  E. y  e.  P  <" A C X "> (cgrG `  G ) <" D F y "> )
13121ad3antrrr 741 . . . . . . 7  |-  ( ( ( ( ph  /\  A  =/=  C )  /\  y  e.  P )  /\  <" A C X "> (cgrG `  G ) <" D F y "> )  ->  <" A B C "> (cgrG `  G ) <" D E F "> )
1324ad3antrrr 741 . . . . . . . . 9  |-  ( ( ( ( ph  /\  A  =/=  C )  /\  y  e.  P )  /\  <" A C X "> (cgrG `  G ) <" D F y "> )  ->  G  e. TarskiG )
13310ad3antrrr 741 . . . . . . . . 9  |-  ( ( ( ( ph  /\  A  =/=  C )  /\  y  e.  P )  /\  <" A C X "> (cgrG `  G ) <" D F y "> )  ->  X  e.  P
)
1346ad3antrrr 741 . . . . . . . . 9  |-  ( ( ( ( ph  /\  A  =/=  C )  /\  y  e.  P )  /\  <" A C X "> (cgrG `  G ) <" D F y "> )  ->  A  e.  P
)
135 simplr 767 . . . . . . . . 9  |-  ( ( ( ( ph  /\  A  =/=  C )  /\  y  e.  P )  /\  <" A C X "> (cgrG `  G ) <" D F y "> )  ->  y  e.  P
)
13613ad3antrrr 741 . . . . . . . . 9  |-  ( ( ( ( ph  /\  A  =/=  C )  /\  y  e.  P )  /\  <" A C X "> (cgrG `  G ) <" D F y "> )  ->  D  e.  P
)
13719ad3antrrr 741 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  A  =/=  C )  /\  y  e.  P )  /\  <" A C X "> (cgrG `  G ) <" D F y "> )  ->  C  e.  P
)
13820ad3antrrr 741 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  A  =/=  C )  /\  y  e.  P )  /\  <" A C X "> (cgrG `  G ) <" D F y "> )  ->  F  e.  P
)
139 simpr 467 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  A  =/=  C )  /\  y  e.  P )  /\  <" A C X "> (cgrG `  G ) <" D F y "> )  ->  <" A C X "> (cgrG `  G ) <" D F y "> )
1401, 17, 3, 12, 132, 134, 137, 133, 136, 138, 135, 139cgr3simp3 24616 . . . . . . . . 9  |-  ( ( ( ( ph  /\  A  =/=  C )  /\  y  e.  P )  /\  <" A C X "> (cgrG `  G ) <" D F y "> )  ->  ( X (
dist `  G ) A )  =  ( y ( dist `  G
) D ) )
1411, 17, 3, 132, 133, 134, 135, 136, 140tgcgrcomlr 24573 . . . . . . . 8  |-  ( ( ( ( ph  /\  A  =/=  C )  /\  y  e.  P )  /\  <" A C X "> (cgrG `  G ) <" D F y "> )  ->  ( A (
dist `  G ) X )  =  ( D ( dist `  G
) y ) )
1428ad3antrrr 741 . . . . . . . . 9  |-  ( ( ( ( ph  /\  A  =/=  C )  /\  y  e.  P )  /\  <" A C X "> (cgrG `  G ) <" D F y "> )  ->  B  e.  P
)
14315ad3antrrr 741 . . . . . . . . 9  |-  ( ( ( ( ph  /\  A  =/=  C )  /\  y  e.  P )  /\  <" A C X "> (cgrG `  G ) <" D F y "> )  ->  E  e.  P
)
144128ad3antrrr 741 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  A  =/=  C )  /\  y  e.  P )  /\  <" A C X "> (cgrG `  G ) <" D F y "> )  ->  ( C  e.  ( A L X )  \/  A  =  X ) )
14522ad3antrrr 741 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  A  =/=  C )  /\  y  e.  P )  /\  <" A C X "> (cgrG `  G ) <" D F y "> )  ->  ( A (
dist `  G ) B )  =  ( D ( dist `  G
) E ) )
1461, 17, 3, 12, 4, 6, 8, 19, 13, 15, 20, 21cgr3simp2 24615 . . . . . . . . . . . 12  |-  ( ph  ->  ( B ( dist `  G ) C )  =  ( E (
dist `  G ) F ) )
1471, 17, 3, 4, 8, 19, 15, 20, 146tgcgrcomlr 24573 . . . . . . . . . . 11  |-  ( ph  ->  ( C ( dist `  G ) B )  =  ( F (
dist `  G ) E ) )
148147ad3antrrr 741 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  A  =/=  C )  /\  y  e.  P )  /\  <" A C X "> (cgrG `  G ) <" D F y "> )  ->  ( C (
dist `  G ) B )  =  ( F ( dist `  G
) E ) )
149 simpllr 774 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  A  =/=  C )  /\  y  e.  P )  /\  <" A C X "> (cgrG `  G ) <" D F y "> )  ->  A  =/=  C
)
1501, 2, 3, 132, 134, 137, 133, 12, 136, 138, 17, 142, 135, 143, 144, 139, 145, 148, 149tgfscgr 24662 . . . . . . . . 9  |-  ( ( ( ( ph  /\  A  =/=  C )  /\  y  e.  P )  /\  <" A C X "> (cgrG `  G ) <" D F y "> )  ->  ( X (
dist `  G ) B )  =  ( y ( dist `  G
) E ) )
1511, 17, 3, 132, 133, 142, 135, 143, 150tgcgrcomlr 24573 . . . . . . . 8  |-  ( ( ( ( ph  /\  A  =/=  C )  /\  y  e.  P )  /\  <" A C X "> (cgrG `  G ) <" D F y "> )  ->  ( B (
dist `  G ) X )  =  ( E ( dist `  G
) y ) )
1521, 17, 3, 12, 132, 134, 137, 133, 136, 138, 135, 139cgr3simp2 24615 . . . . . . . 8  |-  ( ( ( ( ph  /\  A  =/=  C )  /\  y  e.  P )  /\  <" A C X "> (cgrG `  G ) <" D F y "> )  ->  ( C (
dist `  G ) X )  =  ( F ( dist `  G
) y ) )
153141, 151, 1523jca 1194 . . . . . . 7  |-  ( ( ( ( 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 ) ) )
154131, 153jca 539 . . . . . 6  |-  ( ( ( ( ph  /\  A  =/=  C )  /\  y  e.  P )  /\  <" A C X "> (cgrG `  G ) <" D 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 ) ) ) )
1551, 17, 3, 12, 132, 134, 142, 137, 133, 136, 143, 138, 135tgcgr4 24625 . . . . . 6  |-  ( ( ( ( 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 ) ) ) ) )
156154, 155mpbird 240 . . . . 5  |-  ( ( ( ( ph  /\  A  =/=  C )  /\  y  e.  P )  /\  <" A C X "> (cgrG `  G ) <" D F y "> )  ->  <" A B C X "> (cgrG `  G ) <" D E F y "> )
157156ex 440 . . . 4  |-  ( ( ( ph  /\  A  =/=  C )  /\  y  e.  P )  ->  ( <" A C X "> (cgrG `  G ) <" D F y ">  ->  <" A B C X "> (cgrG `  G ) <" D E F y "> )
)
158157reximdva 2874 . . 3  |-  ( (
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 "> )
)
159130, 158mpd 15 . 2  |-  ( (
ph  /\  A  =/=  C )  ->  E. y  e.  P  <" A B C X "> (cgrG `  G ) <" D E F y "> )
160125, 159pm2.61dane 2723 1  |-  ( ph  ->  E. y  e.  P  <" A B C X "> (cgrG `  G ) <" D E F y "> )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    \/ wo 374    /\ wa 375    /\ w3a 991    = wceq 1455    e. wcel 1898    =/= wne 2633   E.wrex 2750   class class class wbr 4416   ` cfv 5601  (class class class)co 6315   <"cs3 12975   <"cs4 12976   Basecbs 15170   distcds 15248  TarskiGcstrkg 24527  Itvcitv 24533  LineGclng 24534  cgrGccgrg 24604  hlGchlg 24694  hpGchpg 24848
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-8 1900  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-rep 4529  ax-sep 4539  ax-nul 4548  ax-pow 4595  ax-pr 4653  ax-un 6610  ax-cnex 9621  ax-resscn 9622  ax-1cn 9623  ax-icn 9624  ax-addcl 9625  ax-addrcl 9626  ax-mulcl 9627  ax-mulrcl 9628  ax-mulcom 9629  ax-addass 9630  ax-mulass 9631  ax-distr 9632  ax-i2m1 9633  ax-1ne0 9634  ax-1rid 9635  ax-rnegex 9636  ax-rrecex 9637  ax-cnre 9638  ax-pre-lttri 9639  ax-pre-lttrn 9640  ax-pre-ltadd 9641  ax-pre-mulgt0 9642
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 992  df-3an 993  df-tru 1458  df-fal 1461  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-nel 2636  df-ral 2754  df-rex 2755  df-reu 2756  df-rmo 2757  df-rab 2758  df-v 3059  df-sbc 3280  df-csb 3376  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-pss 3432  df-nul 3744  df-if 3894  df-pw 3965  df-sn 3981  df-pr 3983  df-tp 3985  df-op 3987  df-uni 4213  df-int 4249  df-iun 4294  df-br 4417  df-opab 4476  df-mpt 4477  df-tr 4512  df-eprel 4764  df-id 4768  df-po 4774  df-so 4775  df-fr 4812  df-we 4814  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  df-pred 5399  df-ord 5445  df-on 5446  df-lim 5447  df-suc 5448  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-riota 6277  df-ov 6318  df-oprab 6319  df-mpt2 6320  df-om 6720  df-1st 6820  df-2nd 6821  df-wrecs 7054  df-recs 7116  df-rdg 7154  df-1o 7208  df-oadd 7212  df-er 7389  df-map 7500  df-pm 7501  df-en 7596  df-dom 7597  df-sdom 7598  df-fin 7599  df-card 8399  df-cda 8624  df-pnf 9703  df-mnf 9704  df-xr 9705  df-ltxr 9706  df-le 9707  df-sub 9888  df-neg 9889  df-nn 10638  df-2 10696  df-3 10697  df-4 10698  df-n0 10899  df-z 10967  df-uz 11189  df-fz 11814  df-fzo 11947  df-hash 12548  df-word 12697  df-concat 12699  df-s1 12700  df-s2 12981  df-s3 12982  df-s4 12983  df-trkgc 24545  df-trkgb 24546  df-trkgcb 24547  df-trkgld 24549  df-trkg 24550  df-cgrg 24605  df-ismt 24627  df-leg 24677  df-hlg 24695  df-mir 24747  df-rag 24788  df-perpg 24790  df-hpg 24849  df-mid 24865  df-lmi 24866
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator