Metamath Proof Explorer

Theorem cgracgr

Description: First direction of proposition 11.4 of Schwabhauser p. 95. Again, this is "half" of the proposition, i.e. only two additional points are used, while Schwabhauser has four. (Contributed by Thierry Arnoux, 31-Jul-2020)

Ref Expression
Hypotheses iscgra.p 
|- P = ( Base ` G )
iscgra.i 
|- I = ( Itv ` G )
iscgra.k 
|- K = ( hlG ` G )
iscgra.g 
|- ( ph -> G e. TarskiG )
iscgra.a 
|- ( ph -> A e. P )
iscgra.b 
|- ( ph -> B e. P )
iscgra.c 
|- ( ph -> C e. P )
iscgra.d 
|- ( ph -> D e. P )
iscgra.e 
|- ( ph -> E e. P )
iscgra.f 
|- ( ph -> F e. P )
cgrahl1.2 
|- ( ph -> <" A B C "> ( cgrA ` G ) <" D E F "> )
cgrahl1.x 
|- ( ph -> X e. P )
cgracgr.m 
|- .- = ( dist ` G )
cgracgr.y 
|- ( ph -> Y e. P )
cgracgr.1 
|- ( ph -> X ( K ` B ) A )
cgracgr.2 
|- ( ph -> Y ( K ` B ) C )
cgracgr.3 
|- ( ph -> ( B .- X ) = ( E .- D ) )
cgracgr.4 
|- ( ph -> ( B .- Y ) = ( E .- F ) )
Assertion cgracgr 
|- ( ph -> ( X .- Y ) = ( D .- F ) )

Proof

Step Hyp Ref Expression
1 iscgra.p 
 |-  P = ( Base ` G )
2 iscgra.i 
 |-  I = ( Itv ` G )
3 iscgra.k 
 |-  K = ( hlG ` G )
4 iscgra.g 
 |-  ( ph -> G e. TarskiG )
5 iscgra.a 
 |-  ( ph -> A e. P )
6 iscgra.b 
 |-  ( ph -> B e. P )
7 iscgra.c 
 |-  ( ph -> C e. P )
8 iscgra.d 
 |-  ( ph -> D e. P )
9 iscgra.e 
 |-  ( ph -> E e. P )
10 iscgra.f 
 |-  ( ph -> F e. P )
11 cgrahl1.2 
 |-  ( ph -> <" A B C "> ( cgrA ` G ) <" D E F "> )
12 cgrahl1.x 
 |-  ( ph -> X e. P )
13 cgracgr.m 
 |-  .- = ( dist ` G )
14 cgracgr.y 
 |-  ( ph -> Y e. P )
15 cgracgr.1 
 |-  ( ph -> X ( K ` B ) A )
16 cgracgr.2 
 |-  ( ph -> Y ( K ` B ) C )
17 cgracgr.3 
 |-  ( ph -> ( B .- X ) = ( E .- D ) )
18 cgracgr.4 
 |-  ( ph -> ( B .- Y ) = ( E .- F ) )
19 eqid 
 |-  ( LineG ` G ) = ( LineG ` G )
20 4 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) -> G e. TarskiG )
21 5 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) -> A e. P )
22 6 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) -> B e. P )
23 12 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) -> X e. P )
24 eqid 
 |-  ( cgrG ` G ) = ( cgrG ` G )
25 simpllr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) -> x e. P )
26 9 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) -> E e. P )
27 14 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) -> Y e. P )
28 8 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) -> D e. P )
29 10 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) -> F e. P )
30 1 2 3 12 5 6 4 15 hlne2 
 |-  ( ph -> A =/= B )
31 30 necomd 
 |-  ( ph -> B =/= A )
32 1 2 3 12 5 6 4 19 15 hlln 
 |-  ( ph -> X e. ( A ( LineG ` G ) B ) )
33 1 2 19 4 6 5 12 31 32 lncom 
 |-  ( ph -> X e. ( B ( LineG ` G ) A ) )
34 33 orcd 
 |-  ( ph -> ( X e. ( B ( LineG ` G ) A ) \/ B = A ) )
35 1 19 2 4 6 5 12 34 colrot1 
 |-  ( ph -> ( B e. ( A ( LineG ` G ) X ) \/ A = X ) )
36 35 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) -> ( B e. ( A ( LineG ` G ) X ) \/ A = X ) )
37 7 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) -> C e. P )
38 simplr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) -> y e. P )
39 simpr1 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) -> <" A B C "> ( cgrG ` G ) <" x E y "> )
40 1 13 2 24 20 21 22 37 25 26 38 39 cgr3simp1 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) -> ( A .- B ) = ( x .- E ) )
41 17 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) -> ( B .- X ) = ( E .- D ) )
42 eqid 
 |-  ( leG ` G ) = ( leG ` G )
43 simpr2 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) -> x ( K ` E ) D )
44 1 2 3 25 28 26 20 ishlg 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) -> ( x ( K ` E ) D <-> ( x =/= E /\ D =/= E /\ ( x e. ( E I D ) \/ D e. ( E I x ) ) ) ) )
45 43 44 mpbid 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) -> ( x =/= E /\ D =/= E /\ ( x e. ( E I D ) \/ D e. ( E I x ) ) ) )
46 45 simp3d 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) -> ( x e. ( E I D ) \/ D e. ( E I x ) ) )
47 1 2 3 12 5 6 4 ishlg 
 |-  ( ph -> ( X ( K ` B ) A <-> ( X =/= B /\ A =/= B /\ ( X e. ( B I A ) \/ A e. ( B I X ) ) ) ) )
48 15 47 mpbid 
 |-  ( ph -> ( X =/= B /\ A =/= B /\ ( X e. ( B I A ) \/ A e. ( B I X ) ) ) )
49 48 simp3d 
 |-  ( ph -> ( X e. ( B I A ) \/ A e. ( B I X ) ) )
50 49 orcomd 
 |-  ( ph -> ( A e. ( B I X ) \/ X e. ( B I A ) ) )
51 50 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) -> ( A e. ( B I X ) \/ X e. ( B I A ) ) )
52 40 eqcomd 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) -> ( x .- E ) = ( A .- B ) )
53 1 13 2 20 25 26 21 22 52 tgcgrcomlr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) -> ( E .- x ) = ( B .- A ) )
54 41 eqcomd 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) -> ( E .- D ) = ( B .- X ) )
55 1 13 2 42 20 26 25 28 22 22 21 23 46 51 53 54 tgcgrsub2 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) -> ( x .- D ) = ( A .- X ) )
56 55 eqcomd 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) -> ( A .- X ) = ( x .- D ) )
57 1 13 2 20 21 23 25 28 56 tgcgrcomlr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) -> ( X .- A ) = ( D .- x ) )
58 1 13 24 20 21 22 23 25 26 28 40 41 57 trgcgr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) -> <" A B X "> ( cgrG ` G ) <" x E D "> )
59 1 2 3 14 7 6 4 19 16 hlln 
 |-  ( ph -> Y e. ( C ( LineG ` G ) B ) )
60 59 orcd 
 |-  ( ph -> ( Y e. ( C ( LineG ` G ) B ) \/ C = B ) )
61 1 19 2 4 7 6 14 60 colrot1 
 |-  ( ph -> ( C e. ( B ( LineG ` G ) Y ) \/ B = Y ) )
62 61 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) -> ( C e. ( B ( LineG ` G ) Y ) \/ B = Y ) )
63 1 13 2 24 20 21 22 37 25 26 38 39 cgr3simp2 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) -> ( B .- C ) = ( E .- y ) )
64 1 2 3 14 7 6 4 ishlg 
 |-  ( ph -> ( Y ( K ` B ) C <-> ( Y =/= B /\ C =/= B /\ ( Y e. ( B I C ) \/ C e. ( B I Y ) ) ) ) )
65 16 64 mpbid 
 |-  ( ph -> ( Y =/= B /\ C =/= B /\ ( Y e. ( B I C ) \/ C e. ( B I Y ) ) ) )
66 65 simp3d 
 |-  ( ph -> ( Y e. ( B I C ) \/ C e. ( B I Y ) ) )
67 66 orcomd 
 |-  ( ph -> ( C e. ( B I Y ) \/ Y e. ( B I C ) ) )
68 67 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) -> ( C e. ( B I Y ) \/ Y e. ( B I C ) ) )
69 simpr3 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) -> y ( K ` E ) F )
70 1 2 3 38 29 26 20 ishlg 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) -> ( y ( K ` E ) F <-> ( y =/= E /\ F =/= E /\ ( y e. ( E I F ) \/ F e. ( E I y ) ) ) ) )
71 69 70 mpbid 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) -> ( y =/= E /\ F =/= E /\ ( y e. ( E I F ) \/ F e. ( E I y ) ) ) )
72 71 simp3d 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) -> ( y e. ( E I F ) \/ F e. ( E I y ) ) )
73 18 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) -> ( B .- Y ) = ( E .- F ) )
74 1 13 2 42 20 22 37 27 26 26 38 29 68 72 63 73 tgcgrsub2 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) -> ( C .- Y ) = ( y .- F ) )
75 1 13 2 20 22 27 26 29 73 tgcgrcomlr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) -> ( Y .- B ) = ( F .- E ) )
76 1 13 24 20 22 37 27 26 38 29 63 74 75 trgcgr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) -> <" B C Y "> ( cgrG ` G ) <" E y F "> )
77 53 eqcomd 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) -> ( B .- A ) = ( E .- x ) )
78 1 13 2 24 20 21 22 37 25 26 38 39 cgr3simp3 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) -> ( C .- A ) = ( y .- x ) )
79 1 2 3 4 5 6 7 8 9 10 11 cgrane2 
 |-  ( ph -> B =/= C )
80 79 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) -> B =/= C )
81 1 19 2 20 22 37 27 24 26 38 13 21 29 25 62 76 77 78 80 tgfscgr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) -> ( Y .- A ) = ( F .- x ) )
82 1 13 2 20 27 21 29 25 81 tgcgrcomlr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) -> ( A .- Y ) = ( x .- F ) )
83 30 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) -> A =/= B )
84 1 19 2 20 21 22 23 24 25 26 13 27 28 29 36 58 82 73 83 tgfscgr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) -> ( X .- Y ) = ( D .- F ) )
85 1 2 3 4 5 6 7 8 9 10 iscgra 
 |-  ( ph -> ( <" A B C "> ( cgrA ` G ) <" D E F "> <-> E. x e. P E. y e. P ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) )
86 11 85 mpbid 
 |-  ( ph -> E. x e. P E. y e. P ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) )
87 84 86 r19.29vva 
 |-  ( ph -> ( X .- Y ) = ( D .- F ) )