Metamath Proof Explorer

Theorem hypcgrlem2

Description: Lemma for hypcgr , case where triangles share one vertex B . (Contributed by Thierry Arnoux, 16-Dec-2019)

Ref Expression
Hypotheses hypcgr.p 
|- P = ( Base ` G )
hypcgr.m 
|- .- = ( dist ` G )
hypcgr.i 
|- I = ( Itv ` G )
hypcgr.g 
|- ( ph -> G e. TarskiG )
hypcgr.h 
|- ( ph -> G TarskiGDim>= 2 )
hypcgr.a 
|- ( ph -> A e. P )
hypcgr.b 
|- ( ph -> B e. P )
hypcgr.c 
|- ( ph -> C e. P )
hypcgr.d 
|- ( ph -> D e. P )
hypcgr.e 
|- ( ph -> E e. P )
hypcgr.f 
|- ( ph -> F e. P )
hypcgr.1 
|- ( ph -> <" A B C "> e. ( raG ` G ) )
hypcgr.2 
|- ( ph -> <" D E F "> e. ( raG ` G ) )
hypcgr.3 
|- ( ph -> ( A .- B ) = ( D .- E ) )
hypcgr.4 
|- ( ph -> ( B .- C ) = ( E .- F ) )
hypcgrlem2.b 
|- ( ph -> B = E )
hypcgrlem2.s 
|- S = ( ( lInvG ` G ) ` ( ( C ( midG ` G ) F ) ( LineG ` G ) B ) )
Assertion hypcgrlem2 
|- ( ph -> ( A .- C ) = ( D .- F ) )

Proof

Step Hyp Ref Expression
1 hypcgr.p 
 |-  P = ( Base ` G )
2 hypcgr.m 
 |-  .- = ( dist ` G )
3 hypcgr.i 
 |-  I = ( Itv ` G )
4 hypcgr.g 
 |-  ( ph -> G e. TarskiG )
5 hypcgr.h 
 |-  ( ph -> G TarskiGDim>= 2 )
6 hypcgr.a 
 |-  ( ph -> A e. P )
7 hypcgr.b 
 |-  ( ph -> B e. P )
8 hypcgr.c 
 |-  ( ph -> C e. P )
9 hypcgr.d 
 |-  ( ph -> D e. P )
10 hypcgr.e 
 |-  ( ph -> E e. P )
11 hypcgr.f 
 |-  ( ph -> F e. P )
12 hypcgr.1 
 |-  ( ph -> <" A B C "> e. ( raG ` G ) )
13 hypcgr.2 
 |-  ( ph -> <" D E F "> e. ( raG ` G ) )
14 hypcgr.3 
 |-  ( ph -> ( A .- B ) = ( D .- E ) )
15 hypcgr.4 
 |-  ( ph -> ( B .- C ) = ( E .- F ) )
16 hypcgrlem2.b 
 |-  ( ph -> B = E )
17 hypcgrlem2.s 
 |-  S = ( ( lInvG ` G ) ` ( ( C ( midG ` G ) F ) ( LineG ` G ) B ) )
18 4 adantr 
 |-  ( ( ph /\ ( C ( midG ` G ) F ) = B ) -> G e. TarskiG )
19 5 adantr 
 |-  ( ( ph /\ ( C ( midG ` G ) F ) = B ) -> G TarskiGDim>= 2 )
20 6 adantr 
 |-  ( ( ph /\ ( C ( midG ` G ) F ) = B ) -> A e. P )
21 7 adantr 
 |-  ( ( ph /\ ( C ( midG ` G ) F ) = B ) -> B e. P )
22 8 adantr 
 |-  ( ( ph /\ ( C ( midG ` G ) F ) = B ) -> C e. P )
23 eqid 
 |-  ( LineG ` G ) = ( LineG ` G )
24 eqid 
 |-  ( pInvG ` G ) = ( pInvG ` G )
25 eqid 
 |-  ( ( pInvG ` G ) ` B ) = ( ( pInvG ` G ) ` B )
26 9 adantr 
 |-  ( ( ph /\ ( C ( midG ` G ) F ) = B ) -> D e. P )
27 1 2 3 23 24 18 21 25 26 mircl 
 |-  ( ( ph /\ ( C ( midG ` G ) F ) = B ) -> ( ( ( pInvG ` G ) ` B ) ` D ) e. P )
28 10 adantr 
 |-  ( ( ph /\ ( C ( midG ` G ) F ) = B ) -> E e. P )
29 12 adantr 
 |-  ( ( ph /\ ( C ( midG ` G ) F ) = B ) -> <" A B C "> e. ( raG ` G ) )
30 eqidd 
 |-  ( ( ph /\ ( C ( midG ` G ) F ) = B ) -> ( ( ( pInvG ` G ) ` B ) ` D ) = ( ( ( pInvG ` G ) ` B ) ` D ) )
31 16 adantr 
 |-  ( ( ph /\ ( C ( midG ` G ) F ) = B ) -> B = E )
32 1 2 3 23 24 18 21 25 28 mirinv 
 |-  ( ( ph /\ ( C ( midG ` G ) F ) = B ) -> ( ( ( ( pInvG ` G ) ` B ) ` E ) = E <-> B = E ) )
33 31 32 mpbird 
 |-  ( ( ph /\ ( C ( midG ` G ) F ) = B ) -> ( ( ( pInvG ` G ) ` B ) ` E ) = E )
34 33 eqcomd 
 |-  ( ( ph /\ ( C ( midG ` G ) F ) = B ) -> E = ( ( ( pInvG ` G ) ` B ) ` E ) )
35 11 adantr 
 |-  ( ( ph /\ ( C ( midG ` G ) F ) = B ) -> F e. P )
36 1 2 3 18 19 22 35 midcom 
 |-  ( ( ph /\ ( C ( midG ` G ) F ) = B ) -> ( C ( midG ` G ) F ) = ( F ( midG ` G ) C ) )
37 simpr 
 |-  ( ( ph /\ ( C ( midG ` G ) F ) = B ) -> ( C ( midG ` G ) F ) = B )
38 36 37 eqtr3d 
 |-  ( ( ph /\ ( C ( midG ` G ) F ) = B ) -> ( F ( midG ` G ) C ) = B )
39 1 2 3 18 19 35 22 24 21 ismidb 
 |-  ( ( ph /\ ( C ( midG ` G ) F ) = B ) -> ( C = ( ( ( pInvG ` G ) ` B ) ` F ) <-> ( F ( midG ` G ) C ) = B ) )
40 38 39 mpbird 
 |-  ( ( ph /\ ( C ( midG ` G ) F ) = B ) -> C = ( ( ( pInvG ` G ) ` B ) ` F ) )
41 30 34 40 s3eqd 
 |-  ( ( ph /\ ( C ( midG ` G ) F ) = B ) -> <" ( ( ( pInvG ` G ) ` B ) ` D ) E C "> = <" ( ( ( pInvG ` G ) ` B ) ` D ) ( ( ( pInvG ` G ) ` B ) ` E ) ( ( ( pInvG ` G ) ` B ) ` F ) "> )
42 13 adantr 
 |-  ( ( ph /\ ( C ( midG ` G ) F ) = B ) -> <" D E F "> e. ( raG ` G ) )
43 1 2 3 23 24 18 26 28 35 42 25 21 mirrag 
 |-  ( ( ph /\ ( C ( midG ` G ) F ) = B ) -> <" ( ( ( pInvG ` G ) ` B ) ` D ) ( ( ( pInvG ` G ) ` B ) ` E ) ( ( ( pInvG ` G ) ` B ) ` F ) "> e. ( raG ` G ) )
44 41 43 eqeltrd 
 |-  ( ( ph /\ ( C ( midG ` G ) F ) = B ) -> <" ( ( ( pInvG ` G ) ` B ) ` D ) E C "> e. ( raG ` G ) )
45 14 adantr 
 |-  ( ( ph /\ ( C ( midG ` G ) F ) = B ) -> ( A .- B ) = ( D .- E ) )
46 1 2 3 23 24 18 21 25 26 28 miriso 
 |-  ( ( ph /\ ( C ( midG ` G ) F ) = B ) -> ( ( ( ( pInvG ` G ) ` B ) ` D ) .- ( ( ( pInvG ` G ) ` B ) ` E ) ) = ( D .- E ) )
47 33 oveq2d 
 |-  ( ( ph /\ ( C ( midG ` G ) F ) = B ) -> ( ( ( ( pInvG ` G ) ` B ) ` D ) .- ( ( ( pInvG ` G ) ` B ) ` E ) ) = ( ( ( ( pInvG ` G ) ` B ) ` D ) .- E ) )
48 45 46 47 3eqtr2d 
 |-  ( ( ph /\ ( C ( midG ` G ) F ) = B ) -> ( A .- B ) = ( ( ( ( pInvG ` G ) ` B ) ` D ) .- E ) )
49 31 oveq1d 
 |-  ( ( ph /\ ( C ( midG ` G ) F ) = B ) -> ( B .- C ) = ( E .- C ) )
50 eqid 
 |-  ( ( lInvG ` G ) ` ( ( A ( midG ` G ) ( ( ( pInvG ` G ) ` B ) ` D ) ) ( LineG ` G ) B ) ) = ( ( lInvG ` G ) ` ( ( A ( midG ` G ) ( ( ( pInvG ` G ) ` B ) ` D ) ) ( LineG ` G ) B ) )
51 eqidd 
 |-  ( ( ph /\ ( C ( midG ` G ) F ) = B ) -> C = C )
52 1 2 3 18 19 20 21 22 27 28 22 29 44 48 49 31 50 51 hypcgrlem1 
 |-  ( ( ph /\ ( C ( midG ` G ) F ) = B ) -> ( A .- C ) = ( ( ( ( pInvG ` G ) ` B ) ` D ) .- C ) )
53 40 oveq2d 
 |-  ( ( ph /\ ( C ( midG ` G ) F ) = B ) -> ( ( ( ( pInvG ` G ) ` B ) ` D ) .- C ) = ( ( ( ( pInvG ` G ) ` B ) ` D ) .- ( ( ( pInvG ` G ) ` B ) ` F ) ) )
54 1 2 3 23 24 18 21 25 26 35 miriso 
 |-  ( ( ph /\ ( C ( midG ` G ) F ) = B ) -> ( ( ( ( pInvG ` G ) ` B ) ` D ) .- ( ( ( pInvG ` G ) ` B ) ` F ) ) = ( D .- F ) )
55 52 53 54 3eqtrd 
 |-  ( ( ph /\ ( C ( midG ` G ) F ) = B ) -> ( A .- C ) = ( D .- F ) )
56 4 ad2antrr 
 |-  ( ( ( ph /\ ( C ( midG ` G ) F ) =/= B ) /\ C = F ) -> G e. TarskiG )
57 5 ad2antrr 
 |-  ( ( ( ph /\ ( C ( midG ` G ) F ) =/= B ) /\ C = F ) -> G TarskiGDim>= 2 )
58 6 ad2antrr 
 |-  ( ( ( ph /\ ( C ( midG ` G ) F ) =/= B ) /\ C = F ) -> A e. P )
59 7 ad2antrr 
 |-  ( ( ( ph /\ ( C ( midG ` G ) F ) =/= B ) /\ C = F ) -> B e. P )
60 8 ad2antrr 
 |-  ( ( ( ph /\ ( C ( midG ` G ) F ) =/= B ) /\ C = F ) -> C e. P )
61 9 ad2antrr 
 |-  ( ( ( ph /\ ( C ( midG ` G ) F ) =/= B ) /\ C = F ) -> D e. P )
62 10 ad2antrr 
 |-  ( ( ( ph /\ ( C ( midG ` G ) F ) =/= B ) /\ C = F ) -> E e. P )
63 11 ad2antrr 
 |-  ( ( ( ph /\ ( C ( midG ` G ) F ) =/= B ) /\ C = F ) -> F e. P )
64 12 ad2antrr 
 |-  ( ( ( ph /\ ( C ( midG ` G ) F ) =/= B ) /\ C = F ) -> <" A B C "> e. ( raG ` G ) )
65 13 ad2antrr 
 |-  ( ( ( ph /\ ( C ( midG ` G ) F ) =/= B ) /\ C = F ) -> <" D E F "> e. ( raG ` G ) )
66 14 ad2antrr 
 |-  ( ( ( ph /\ ( C ( midG ` G ) F ) =/= B ) /\ C = F ) -> ( A .- B ) = ( D .- E ) )
67 15 ad2antrr 
 |-  ( ( ( ph /\ ( C ( midG ` G ) F ) =/= B ) /\ C = F ) -> ( B .- C ) = ( E .- F ) )
68 16 ad2antrr 
 |-  ( ( ( ph /\ ( C ( midG ` G ) F ) =/= B ) /\ C = F ) -> B = E )
69 eqid 
 |-  ( ( lInvG ` G ) ` ( ( A ( midG ` G ) D ) ( LineG ` G ) B ) ) = ( ( lInvG ` G ) ` ( ( A ( midG ` G ) D ) ( LineG ` G ) B ) )
70 simpr 
 |-  ( ( ( ph /\ ( C ( midG ` G ) F ) =/= B ) /\ C = F ) -> C = F )
71 1 2 3 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 hypcgrlem1 
 |-  ( ( ( ph /\ ( C ( midG ` G ) F ) =/= B ) /\ C = F ) -> ( A .- C ) = ( D .- F ) )
72 4 ad2antrr 
 |-  ( ( ( ph /\ ( C ( midG ` G ) F ) =/= B ) /\ C =/= F ) -> G e. TarskiG )
73 5 ad2antrr 
 |-  ( ( ( ph /\ ( C ( midG ` G ) F ) =/= B ) /\ C =/= F ) -> G TarskiGDim>= 2 )
74 6 ad2antrr 
 |-  ( ( ( ph /\ ( C ( midG ` G ) F ) =/= B ) /\ C =/= F ) -> A e. P )
75 7 ad2antrr 
 |-  ( ( ( ph /\ ( C ( midG ` G ) F ) =/= B ) /\ C =/= F ) -> B e. P )
76 8 ad2antrr 
 |-  ( ( ( ph /\ ( C ( midG ` G ) F ) =/= B ) /\ C =/= F ) -> C e. P )
77 11 ad2antrr 
 |-  ( ( ( ph /\ ( C ( midG ` G ) F ) =/= B ) /\ C =/= F ) -> F e. P )
78 1 2 3 72 73 76 77 midcl 
 |-  ( ( ( ph /\ ( C ( midG ` G ) F ) =/= B ) /\ C =/= F ) -> ( C ( midG ` G ) F ) e. P )
79 simplr 
 |-  ( ( ( ph /\ ( C ( midG ` G ) F ) =/= B ) /\ C =/= F ) -> ( C ( midG ` G ) F ) =/= B )
80 1 3 23 72 78 75 79 tgelrnln 
 |-  ( ( ( ph /\ ( C ( midG ` G ) F ) =/= B ) /\ C =/= F ) -> ( ( C ( midG ` G ) F ) ( LineG ` G ) B ) e. ran ( LineG ` G ) )
81 9 ad2antrr 
 |-  ( ( ( ph /\ ( C ( midG ` G ) F ) =/= B ) /\ C =/= F ) -> D e. P )
82 1 2 3 72 73 17 23 80 81 lmicl 
 |-  ( ( ( ph /\ ( C ( midG ` G ) F ) =/= B ) /\ C =/= F ) -> ( S ` D ) e. P )
83 10 ad2antrr 
 |-  ( ( ( ph /\ ( C ( midG ` G ) F ) =/= B ) /\ C =/= F ) -> E e. P )
84 1 2 3 72 73 17 23 80 83 lmicl 
 |-  ( ( ( ph /\ ( C ( midG ` G ) F ) =/= B ) /\ C =/= F ) -> ( S ` E ) e. P )
85 1 2 3 72 73 17 23 80 77 lmicl 
 |-  ( ( ( ph /\ ( C ( midG ` G ) F ) =/= B ) /\ C =/= F ) -> ( S ` F ) e. P )
86 12 ad2antrr 
 |-  ( ( ( ph /\ ( C ( midG ` G ) F ) =/= B ) /\ C =/= F ) -> <" A B C "> e. ( raG ` G ) )
87 1 2 3 72 73 17 23 80 lmimot 
 |-  ( ( ( ph /\ ( C ( midG ` G ) F ) =/= B ) /\ C =/= F ) -> S e. ( G Ismt G ) )
88 13 ad2antrr 
 |-  ( ( ( ph /\ ( C ( midG ` G ) F ) =/= B ) /\ C =/= F ) -> <" D E F "> e. ( raG ` G ) )
89 1 2 3 23 24 72 81 83 77 87 88 motrag 
 |-  ( ( ( ph /\ ( C ( midG ` G ) F ) =/= B ) /\ C =/= F ) -> <" ( S ` D ) ( S ` E ) ( S ` F ) "> e. ( raG ` G ) )
90 14 ad2antrr 
 |-  ( ( ( ph /\ ( C ( midG ` G ) F ) =/= B ) /\ C =/= F ) -> ( A .- B ) = ( D .- E ) )
91 1 2 3 72 73 17 23 80 81 83 lmiiso 
 |-  ( ( ( ph /\ ( C ( midG ` G ) F ) =/= B ) /\ C =/= F ) -> ( ( S ` D ) .- ( S ` E ) ) = ( D .- E ) )
92 90 91 eqtr4d 
 |-  ( ( ( ph /\ ( C ( midG ` G ) F ) =/= B ) /\ C =/= F ) -> ( A .- B ) = ( ( S ` D ) .- ( S ` E ) ) )
93 15 ad2antrr 
 |-  ( ( ( ph /\ ( C ( midG ` G ) F ) =/= B ) /\ C =/= F ) -> ( B .- C ) = ( E .- F ) )
94 1 2 3 72 73 17 23 80 83 77 lmiiso 
 |-  ( ( ( ph /\ ( C ( midG ` G ) F ) =/= B ) /\ C =/= F ) -> ( ( S ` E ) .- ( S ` F ) ) = ( E .- F ) )
95 93 94 eqtr4d 
 |-  ( ( ( ph /\ ( C ( midG ` G ) F ) =/= B ) /\ C =/= F ) -> ( B .- C ) = ( ( S ` E ) .- ( S ` F ) ) )
96 1 3 23 72 78 75 79 tglinerflx2 
 |-  ( ( ( ph /\ ( C ( midG ` G ) F ) =/= B ) /\ C =/= F ) -> B e. ( ( C ( midG ` G ) F ) ( LineG ` G ) B ) )
97 1 2 3 72 73 17 23 80 75 96 lmicinv 
 |-  ( ( ( ph /\ ( C ( midG ` G ) F ) =/= B ) /\ C =/= F ) -> ( S ` B ) = B )
98 16 ad2antrr 
 |-  ( ( ( ph /\ ( C ( midG ` G ) F ) =/= B ) /\ C =/= F ) -> B = E )
99 98 fveq2d 
 |-  ( ( ( ph /\ ( C ( midG ` G ) F ) =/= B ) /\ C =/= F ) -> ( S ` B ) = ( S ` E ) )
100 97 99 eqtr3d 
 |-  ( ( ( ph /\ ( C ( midG ` G ) F ) =/= B ) /\ C =/= F ) -> B = ( S ` E ) )
101 eqid 
 |-  ( ( lInvG ` G ) ` ( ( A ( midG ` G ) ( S ` D ) ) ( LineG ` G ) B ) ) = ( ( lInvG ` G ) ` ( ( A ( midG ` G ) ( S ` D ) ) ( LineG ` G ) B ) )
102 1 2 3 72 73 76 77 midcom 
 |-  ( ( ( ph /\ ( C ( midG ` G ) F ) =/= B ) /\ C =/= F ) -> ( C ( midG ` G ) F ) = ( F ( midG ` G ) C ) )
103 1 3 23 72 78 75 79 tglinerflx1 
 |-  ( ( ( ph /\ ( C ( midG ` G ) F ) =/= B ) /\ C =/= F ) -> ( C ( midG ` G ) F ) e. ( ( C ( midG ` G ) F ) ( LineG ` G ) B ) )
104 102 103 eqeltrrd 
 |-  ( ( ( ph /\ ( C ( midG ` G ) F ) =/= B ) /\ C =/= F ) -> ( F ( midG ` G ) C ) e. ( ( C ( midG ` G ) F ) ( LineG ` G ) B ) )
105 simpr 
 |-  ( ( ( ph /\ ( C ( midG ` G ) F ) =/= B ) /\ C =/= F ) -> C =/= F )
106 105 necomd 
 |-  ( ( ( ph /\ ( C ( midG ` G ) F ) =/= B ) /\ C =/= F ) -> F =/= C )
107 1 3 23 72 77 76 106 tgelrnln 
 |-  ( ( ( ph /\ ( C ( midG ` G ) F ) =/= B ) /\ C =/= F ) -> ( F ( LineG ` G ) C ) e. ran ( LineG ` G ) )
108 1 2 3 72 73 76 77 midbtwn 
 |-  ( ( ( ph /\ ( C ( midG ` G ) F ) =/= B ) /\ C =/= F ) -> ( C ( midG ` G ) F ) e. ( C I F ) )
109 1 2 3 72 76 78 77 108 tgbtwncom 
 |-  ( ( ( ph /\ ( C ( midG ` G ) F ) =/= B ) /\ C =/= F ) -> ( C ( midG ` G ) F ) e. ( F I C ) )
110 1 3 23 72 77 76 78 106 109 btwnlng1 
 |-  ( ( ( ph /\ ( C ( midG ` G ) F ) =/= B ) /\ C =/= F ) -> ( C ( midG ` G ) F ) e. ( F ( LineG ` G ) C ) )
111 103 110 elind 
 |-  ( ( ( ph /\ ( C ( midG ` G ) F ) =/= B ) /\ C =/= F ) -> ( C ( midG ` G ) F ) e. ( ( ( C ( midG ` G ) F ) ( LineG ` G ) B ) i^i ( F ( LineG ` G ) C ) ) )
112 1 3 23 72 77 76 106 tglinerflx2 
 |-  ( ( ( ph /\ ( C ( midG ` G ) F ) =/= B ) /\ C =/= F ) -> C e. ( F ( LineG ` G ) C ) )
113 79 necomd 
 |-  ( ( ( ph /\ ( C ( midG ` G ) F ) =/= B ) /\ C =/= F ) -> B =/= ( C ( midG ` G ) F ) )
114 4 ad2antrr 
 |-  ( ( ( ph /\ ( C ( midG ` G ) F ) =/= B ) /\ C = ( C ( midG ` G ) F ) ) -> G e. TarskiG )
115 8 ad2antrr 
 |-  ( ( ( ph /\ ( C ( midG ` G ) F ) =/= B ) /\ C = ( C ( midG ` G ) F ) ) -> C e. P )
116 11 ad2antrr 
 |-  ( ( ( ph /\ ( C ( midG ` G ) F ) =/= B ) /\ C = ( C ( midG ` G ) F ) ) -> F e. P )
117 5 ad2antrr 
 |-  ( ( ( ph /\ ( C ( midG ` G ) F ) =/= B ) /\ C = ( C ( midG ` G ) F ) ) -> G TarskiGDim>= 2 )
118 simpr 
 |-  ( ( ( ph /\ ( C ( midG ` G ) F ) =/= B ) /\ C = ( C ( midG ` G ) F ) ) -> C = ( C ( midG ` G ) F ) )
119 118 eqcomd 
 |-  ( ( ( ph /\ ( C ( midG ` G ) F ) =/= B ) /\ C = ( C ( midG ` G ) F ) ) -> ( C ( midG ` G ) F ) = C )
120 1 2 3 114 117 115 116 119 midcgr 
 |-  ( ( ( ph /\ ( C ( midG ` G ) F ) =/= B ) /\ C = ( C ( midG ` G ) F ) ) -> ( C .- C ) = ( C .- F ) )
121 120 eqcomd 
 |-  ( ( ( ph /\ ( C ( midG ` G ) F ) =/= B ) /\ C = ( C ( midG ` G ) F ) ) -> ( C .- F ) = ( C .- C ) )
122 1 2 3 114 115 116 115 121 axtgcgrid 
 |-  ( ( ( ph /\ ( C ( midG ` G ) F ) =/= B ) /\ C = ( C ( midG ` G ) F ) ) -> C = F )
123 122 ex 
 |-  ( ( ph /\ ( C ( midG ` G ) F ) =/= B ) -> ( C = ( C ( midG ` G ) F ) -> C = F ) )
124 123 necon3d 
 |-  ( ( ph /\ ( C ( midG ` G ) F ) =/= B ) -> ( C =/= F -> C =/= ( C ( midG ` G ) F ) ) )
125 124 imp 
 |-  ( ( ( ph /\ ( C ( midG ` G ) F ) =/= B ) /\ C =/= F ) -> C =/= ( C ( midG ` G ) F ) )
126 98 eqcomd 
 |-  ( ( ( ph /\ ( C ( midG ` G ) F ) =/= B ) /\ C =/= F ) -> E = B )
127 eqidd 
 |-  ( ( ( ph /\ ( C ( midG ` G ) F ) =/= B ) /\ C =/= F ) -> ( C ( midG ` G ) F ) = ( C ( midG ` G ) F ) )
128 1 2 3 72 73 76 77 24 78 ismidb 
 |-  ( ( ( ph /\ ( C ( midG ` G ) F ) =/= B ) /\ C =/= F ) -> ( F = ( ( ( pInvG ` G ) ` ( C ( midG ` G ) F ) ) ` C ) <-> ( C ( midG ` G ) F ) = ( C ( midG ` G ) F ) ) )
129 127 128 mpbird 
 |-  ( ( ( ph /\ ( C ( midG ` G ) F ) =/= B ) /\ C =/= F ) -> F = ( ( ( pInvG ` G ) ` ( C ( midG ` G ) F ) ) ` C ) )
130 126 129 oveq12d 
 |-  ( ( ( ph /\ ( C ( midG ` G ) F ) =/= B ) /\ C =/= F ) -> ( E .- F ) = ( B .- ( ( ( pInvG ` G ) ` ( C ( midG ` G ) F ) ) ` C ) ) )
131 93 130 eqtrd 
 |-  ( ( ( ph /\ ( C ( midG ` G ) F ) =/= B ) /\ C =/= F ) -> ( B .- C ) = ( B .- ( ( ( pInvG ` G ) ` ( C ( midG ` G ) F ) ) ` C ) ) )
132 1 2 3 23 24 72 75 78 76 israg 
 |-  ( ( ( ph /\ ( C ( midG ` G ) F ) =/= B ) /\ C =/= F ) -> ( <" B ( C ( midG ` G ) F ) C "> e. ( raG ` G ) <-> ( B .- C ) = ( B .- ( ( ( pInvG ` G ) ` ( C ( midG ` G ) F ) ) ` C ) ) ) )
133 131 132 mpbird 
 |-  ( ( ( ph /\ ( C ( midG ` G ) F ) =/= B ) /\ C =/= F ) -> <" B ( C ( midG ` G ) F ) C "> e. ( raG ` G ) )
134 1 2 3 23 72 80 107 111 96 112 113 125 133 ragperp 
 |-  ( ( ( ph /\ ( C ( midG ` G ) F ) =/= B ) /\ C =/= F ) -> ( ( C ( midG ` G ) F ) ( LineG ` G ) B ) ( perpG ` G ) ( F ( LineG ` G ) C ) )
135 134 orcd 
 |-  ( ( ( ph /\ ( C ( midG ` G ) F ) =/= B ) /\ C =/= F ) -> ( ( ( C ( midG ` G ) F ) ( LineG ` G ) B ) ( perpG ` G ) ( F ( LineG ` G ) C ) \/ F = C ) )
136 1 2 3 72 73 17 23 80 77 76 islmib 
 |-  ( ( ( ph /\ ( C ( midG ` G ) F ) =/= B ) /\ C =/= F ) -> ( C = ( S ` F ) <-> ( ( F ( midG ` G ) C ) e. ( ( C ( midG ` G ) F ) ( LineG ` G ) B ) /\ ( ( ( C ( midG ` G ) F ) ( LineG ` G ) B ) ( perpG ` G ) ( F ( LineG ` G ) C ) \/ F = C ) ) ) )
137 104 135 136 mpbir2and 
 |-  ( ( ( ph /\ ( C ( midG ` G ) F ) =/= B ) /\ C =/= F ) -> C = ( S ` F ) )
138 1 2 3 72 73 74 75 76 82 84 85 86 89 92 95 100 101 137 hypcgrlem1 
 |-  ( ( ( ph /\ ( C ( midG ` G ) F ) =/= B ) /\ C =/= F ) -> ( A .- C ) = ( ( S ` D ) .- ( S ` F ) ) )
139 1 2 3 72 73 17 23 80 81 77 lmiiso 
 |-  ( ( ( ph /\ ( C ( midG ` G ) F ) =/= B ) /\ C =/= F ) -> ( ( S ` D ) .- ( S ` F ) ) = ( D .- F ) )
140 138 139 eqtrd 
 |-  ( ( ( ph /\ ( C ( midG ` G ) F ) =/= B ) /\ C =/= F ) -> ( A .- C ) = ( D .- F ) )
141 71 140 pm2.61dane 
 |-  ( ( ph /\ ( C ( midG ` G ) F ) =/= B ) -> ( A .- C ) = ( D .- F ) )
142 55 141 pm2.61dane 
 |-  ( ph -> ( A .- C ) = ( D .- F ) )