Metamath Proof Explorer

Theorem krippenlem

Description: Lemma for krippen . We can assume krippen.7 "without loss of generality". (Contributed by Thierry Arnoux, 12-Aug-2019)

Ref Expression
Hypotheses mirval.p 
|- P = ( Base ` G )
mirval.d 
|- .- = ( dist ` G )
mirval.i 
|- I = ( Itv ` G )
mirval.l 
|- L = ( LineG ` G )
mirval.s 
|- S = ( pInvG ` G )
mirval.g 
|- ( ph -> G e. TarskiG )
krippen.m 
|- M = ( S ` X )
krippen.n 
|- N = ( S ` Y )
krippen.a 
|- ( ph -> A e. P )
krippen.b 
|- ( ph -> B e. P )
krippen.c 
|- ( ph -> C e. P )
krippen.e 
|- ( ph -> E e. P )
krippen.f 
|- ( ph -> F e. P )
krippen.x 
|- ( ph -> X e. P )
krippen.y 
|- ( ph -> Y e. P )
krippen.1 
|- ( ph -> C e. ( A I E ) )
krippen.2 
|- ( ph -> C e. ( B I F ) )
krippen.3 
|- ( ph -> ( C .- A ) = ( C .- B ) )
krippen.4 
|- ( ph -> ( C .- E ) = ( C .- F ) )
krippen.5 
|- ( ph -> B = ( M ` A ) )
krippen.6 
|- ( ph -> F = ( N ` E ) )
krippen.l 
|- .<_ = ( leG ` G )
krippen.7 
|- ( ph -> ( C .- A ) .<_ ( C .- E ) )
Assertion krippenlem 
|- ( ph -> C e. ( X I Y ) )

Proof

Step Hyp Ref Expression
1 mirval.p 
 |-  P = ( Base ` G )
2 mirval.d 
 |-  .- = ( dist ` G )
3 mirval.i 
 |-  I = ( Itv ` G )
4 mirval.l 
 |-  L = ( LineG ` G )
5 mirval.s 
 |-  S = ( pInvG ` G )
6 mirval.g 
 |-  ( ph -> G e. TarskiG )
7 krippen.m 
 |-  M = ( S ` X )
8 krippen.n 
 |-  N = ( S ` Y )
9 krippen.a 
 |-  ( ph -> A e. P )
10 krippen.b 
 |-  ( ph -> B e. P )
11 krippen.c 
 |-  ( ph -> C e. P )
12 krippen.e 
 |-  ( ph -> E e. P )
13 krippen.f 
 |-  ( ph -> F e. P )
14 krippen.x 
 |-  ( ph -> X e. P )
15 krippen.y 
 |-  ( ph -> Y e. P )
16 krippen.1 
 |-  ( ph -> C e. ( A I E ) )
17 krippen.2 
 |-  ( ph -> C e. ( B I F ) )
18 krippen.3 
 |-  ( ph -> ( C .- A ) = ( C .- B ) )
19 krippen.4 
 |-  ( ph -> ( C .- E ) = ( C .- F ) )
20 krippen.5 
 |-  ( ph -> B = ( M ` A ) )
21 krippen.6 
 |-  ( ph -> F = ( N ` E ) )
22 krippen.l 
 |-  .<_ = ( leG ` G )
23 krippen.7 
 |-  ( ph -> ( C .- A ) .<_ ( C .- E ) )
24 16 adantr 
 |-  ( ( ph /\ E = C ) -> C e. ( A I E ) )
25 6 adantr 
 |-  ( ( ph /\ E = C ) -> G e. TarskiG )
26 11 adantr 
 |-  ( ( ph /\ E = C ) -> C e. P )
27 9 adantr 
 |-  ( ( ph /\ E = C ) -> A e. P )
28 10 adantr 
 |-  ( ( ph /\ E = C ) -> B e. P )
29 18 adantr 
 |-  ( ( ph /\ E = C ) -> ( C .- A ) = ( C .- B ) )
30 23 adantr 
 |-  ( ( ph /\ E = C ) -> ( C .- A ) .<_ ( C .- E ) )
31 simpr 
 |-  ( ( ph /\ E = C ) -> E = C )
32 31 oveq2d 
 |-  ( ( ph /\ E = C ) -> ( C .- E ) = ( C .- C ) )
33 30 32 breqtrd 
 |-  ( ( ph /\ E = C ) -> ( C .- A ) .<_ ( C .- C ) )
34 1 2 3 22 25 26 27 26 28 33 legeq 
 |-  ( ( ph /\ E = C ) -> C = A )
35 1 2 3 25 26 27 26 28 29 34 tgcgreq 
 |-  ( ( ph /\ E = C ) -> C = B )
36 20 adantr 
 |-  ( ( ph /\ E = C ) -> B = ( M ` A ) )
37 35 34 36 3eqtr3rd 
 |-  ( ( ph /\ E = C ) -> ( M ` A ) = A )
38 14 adantr 
 |-  ( ( ph /\ E = C ) -> X e. P )
39 1 2 3 4 5 25 38 7 27 mirinv 
 |-  ( ( ph /\ E = C ) -> ( ( M ` A ) = A <-> X = A ) )
40 37 39 mpbid 
 |-  ( ( ph /\ E = C ) -> X = A )
41 13 adantr 
 |-  ( ( ph /\ E = C ) -> F e. P )
42 19 adantr 
 |-  ( ( ph /\ E = C ) -> ( C .- E ) = ( C .- F ) )
43 42 32 eqtr3d 
 |-  ( ( ph /\ E = C ) -> ( C .- F ) = ( C .- C ) )
44 1 2 3 25 26 41 26 43 axtgcgrid 
 |-  ( ( ph /\ E = C ) -> C = F )
45 21 adantr 
 |-  ( ( ph /\ E = C ) -> F = ( N ` E ) )
46 31 44 45 3eqtrrd 
 |-  ( ( ph /\ E = C ) -> ( N ` E ) = E )
47 15 adantr 
 |-  ( ( ph /\ E = C ) -> Y e. P )
48 12 adantr 
 |-  ( ( ph /\ E = C ) -> E e. P )
49 1 2 3 4 5 25 47 8 48 mirinv 
 |-  ( ( ph /\ E = C ) -> ( ( N ` E ) = E <-> Y = E ) )
50 46 49 mpbid 
 |-  ( ( ph /\ E = C ) -> Y = E )
51 40 50 oveq12d 
 |-  ( ( ph /\ E = C ) -> ( X I Y ) = ( A I E ) )
52 24 51 eleqtrrd 
 |-  ( ( ph /\ E = C ) -> C e. ( X I Y ) )
53 6 adantr 
 |-  ( ( ph /\ E =/= C ) -> G e. TarskiG )
54 53 ad2antrr 
 |-  ( ( ( ( ph /\ E =/= C ) /\ q e. P ) /\ ( q e. ( ( ( S ` C ) ` Y ) I C ) /\ q e. ( A I B ) ) ) -> G e. TarskiG )
55 11 adantr 
 |-  ( ( ph /\ E =/= C ) -> C e. P )
56 eqid 
 |-  ( S ` C ) = ( S ` C )
57 1 2 3 4 5 53 55 56 mirf 
 |-  ( ( ph /\ E =/= C ) -> ( S ` C ) : P --> P )
58 15 adantr 
 |-  ( ( ph /\ E =/= C ) -> Y e. P )
59 57 58 ffvelcdmd 
 |-  ( ( ph /\ E =/= C ) -> ( ( S ` C ) ` Y ) e. P )
60 59 ad2antrr 
 |-  ( ( ( ( ph /\ E =/= C ) /\ q e. P ) /\ ( q e. ( ( ( S ` C ) ` Y ) I C ) /\ q e. ( A I B ) ) ) -> ( ( S ` C ) ` Y ) e. P )
61 simplr 
 |-  ( ( ( ( ph /\ E =/= C ) /\ q e. P ) /\ ( q e. ( ( ( S ` C ) ` Y ) I C ) /\ q e. ( A I B ) ) ) -> q e. P )
62 55 ad2antrr 
 |-  ( ( ( ( ph /\ E =/= C ) /\ q e. P ) /\ ( q e. ( ( ( S ` C ) ` Y ) I C ) /\ q e. ( A I B ) ) ) -> C e. P )
63 58 ad2antrr 
 |-  ( ( ( ( ph /\ E =/= C ) /\ q e. P ) /\ ( q e. ( ( ( S ` C ) ` Y ) I C ) /\ q e. ( A I B ) ) ) -> Y e. P )
64 simprl 
 |-  ( ( ( ( ph /\ E =/= C ) /\ q e. P ) /\ ( q e. ( ( ( S ` C ) ` Y ) I C ) /\ q e. ( A I B ) ) ) -> q e. ( ( ( S ` C ) ` Y ) I C ) )
65 1 2 3 4 5 6 11 56 15 mirbtwn 
 |-  ( ph -> C e. ( ( ( S ` C ) ` Y ) I Y ) )
66 65 ad3antrrr 
 |-  ( ( ( ( ph /\ E =/= C ) /\ q e. P ) /\ ( q e. ( ( ( S ` C ) ` Y ) I C ) /\ q e. ( A I B ) ) ) -> C e. ( ( ( S ` C ) ` Y ) I Y ) )
67 1 2 3 54 60 61 62 63 64 66 tgbtwnexch3 
 |-  ( ( ( ( ph /\ E =/= C ) /\ q e. P ) /\ ( q e. ( ( ( S ` C ) ` Y ) I C ) /\ q e. ( A I B ) ) ) -> C e. ( q I Y ) )
68 14 ad3antrrr 
 |-  ( ( ( ( ph /\ E =/= C ) /\ q e. P ) /\ ( q e. ( ( ( S ` C ) ` Y ) I C ) /\ q e. ( A I B ) ) ) -> X e. P )
69 9 adantr 
 |-  ( ( ph /\ E =/= C ) -> A e. P )
70 69 ad2antrr 
 |-  ( ( ( ( ph /\ E =/= C ) /\ q e. P ) /\ ( q e. ( ( ( S ` C ) ` Y ) I C ) /\ q e. ( A I B ) ) ) -> A e. P )
71 10 adantr 
 |-  ( ( ph /\ E =/= C ) -> B e. P )
72 71 ad2antrr 
 |-  ( ( ( ( ph /\ E =/= C ) /\ q e. P ) /\ ( q e. ( ( ( S ` C ) ` Y ) I C ) /\ q e. ( A I B ) ) ) -> B e. P )
73 eqid 
 |-  ( S ` q ) = ( S ` q )
74 12 adantr 
 |-  ( ( ph /\ E =/= C ) -> E e. P )
75 57 74 ffvelcdmd 
 |-  ( ( ph /\ E =/= C ) -> ( ( S ` C ) ` E ) e. P )
76 13 adantr 
 |-  ( ( ph /\ E =/= C ) -> F e. P )
77 57 76 ffvelcdmd 
 |-  ( ( ph /\ E =/= C ) -> ( ( S ` C ) ` F ) e. P )
78 6 ad2antrr 
 |-  ( ( ( ph /\ E =/= C ) /\ A = C ) -> G e. TarskiG )
79 9 ad2antrr 
 |-  ( ( ( ph /\ E =/= C ) /\ A = C ) -> A e. P )
80 75 adantr 
 |-  ( ( ( ph /\ E =/= C ) /\ A = C ) -> ( ( S ` C ) ` E ) e. P )
81 1 2 3 78 79 80 tgbtwntriv1 
 |-  ( ( ( ph /\ E =/= C ) /\ A = C ) -> A e. ( A I ( ( S ` C ) ` E ) ) )
82 simpr 
 |-  ( ( ( ph /\ E =/= C ) /\ A = C ) -> A = C )
83 82 oveq1d 
 |-  ( ( ( ph /\ E =/= C ) /\ A = C ) -> ( A I ( ( S ` C ) ` E ) ) = ( C I ( ( S ` C ) ` E ) ) )
84 81 83 eleqtrd 
 |-  ( ( ( ph /\ E =/= C ) /\ A = C ) -> A e. ( C I ( ( S ` C ) ` E ) ) )
85 6 ad2antrr 
 |-  ( ( ( ph /\ E =/= C ) /\ A =/= C ) -> G e. TarskiG )
86 9 ad2antrr 
 |-  ( ( ( ph /\ E =/= C ) /\ A =/= C ) -> A e. P )
87 75 adantr 
 |-  ( ( ( ph /\ E =/= C ) /\ A =/= C ) -> ( ( S ` C ) ` E ) e. P )
88 11 ad2antrr 
 |-  ( ( ( ph /\ E =/= C ) /\ A =/= C ) -> C e. P )
89 12 ad2antrr 
 |-  ( ( ( ph /\ E =/= C ) /\ A =/= C ) -> E e. P )
90 simplr 
 |-  ( ( ( ph /\ E =/= C ) /\ A =/= C ) -> E =/= C )
91 1 2 3 6 9 11 12 16 tgbtwncom 
 |-  ( ph -> C e. ( E I A ) )
92 91 ad2antrr 
 |-  ( ( ( ph /\ E =/= C ) /\ A =/= C ) -> C e. ( E I A ) )
93 1 2 3 4 5 85 88 56 89 mirbtwn 
 |-  ( ( ( ph /\ E =/= C ) /\ A =/= C ) -> C e. ( ( ( S ` C ) ` E ) I E ) )
94 1 2 3 85 87 88 89 93 tgbtwncom 
 |-  ( ( ( ph /\ E =/= C ) /\ A =/= C ) -> C e. ( E I ( ( S ` C ) ` E ) ) )
95 1 3 85 89 88 86 87 90 92 94 tgbtwnconn2 
 |-  ( ( ( ph /\ E =/= C ) /\ A =/= C ) -> ( A e. ( C I ( ( S ` C ) ` E ) ) \/ ( ( S ` C ) ` E ) e. ( C I A ) ) )
96 23 adantr 
 |-  ( ( ph /\ E =/= C ) -> ( C .- A ) .<_ ( C .- E ) )
97 1 2 3 4 5 53 55 56 74 mircgr 
 |-  ( ( ph /\ E =/= C ) -> ( C .- ( ( S ` C ) ` E ) ) = ( C .- E ) )
98 96 97 breqtrrd 
 |-  ( ( ph /\ E =/= C ) -> ( C .- A ) .<_ ( C .- ( ( S ` C ) ` E ) ) )
99 98 adantr 
 |-  ( ( ( ph /\ E =/= C ) /\ A =/= C ) -> ( C .- A ) .<_ ( C .- ( ( S ` C ) ` E ) ) )
100 1 2 3 22 85 86 87 88 86 95 99 legbtwn 
 |-  ( ( ( ph /\ E =/= C ) /\ A =/= C ) -> A e. ( C I ( ( S ` C ) ` E ) ) )
101 84 100 pm2.61dane 
 |-  ( ( ph /\ E =/= C ) -> A e. ( C I ( ( S ` C ) ` E ) ) )
102 1 2 3 53 55 69 75 101 tgbtwncom 
 |-  ( ( ph /\ E =/= C ) -> A e. ( ( ( S ` C ) ` E ) I C ) )
103 6 ad2antrr 
 |-  ( ( ( ph /\ E =/= C ) /\ B = C ) -> G e. TarskiG )
104 10 ad2antrr 
 |-  ( ( ( ph /\ E =/= C ) /\ B = C ) -> B e. P )
105 77 adantr 
 |-  ( ( ( ph /\ E =/= C ) /\ B = C ) -> ( ( S ` C ) ` F ) e. P )
106 1 2 3 103 104 105 tgbtwntriv1 
 |-  ( ( ( ph /\ E =/= C ) /\ B = C ) -> B e. ( B I ( ( S ` C ) ` F ) ) )
107 simpr 
 |-  ( ( ( ph /\ E =/= C ) /\ B = C ) -> B = C )
108 107 oveq1d 
 |-  ( ( ( ph /\ E =/= C ) /\ B = C ) -> ( B I ( ( S ` C ) ` F ) ) = ( C I ( ( S ` C ) ` F ) ) )
109 106 108 eleqtrd 
 |-  ( ( ( ph /\ E =/= C ) /\ B = C ) -> B e. ( C I ( ( S ` C ) ` F ) ) )
110 6 ad2antrr 
 |-  ( ( ( ph /\ E =/= C ) /\ B =/= C ) -> G e. TarskiG )
111 10 ad2antrr 
 |-  ( ( ( ph /\ E =/= C ) /\ B =/= C ) -> B e. P )
112 77 adantr 
 |-  ( ( ( ph /\ E =/= C ) /\ B =/= C ) -> ( ( S ` C ) ` F ) e. P )
113 11 ad2antrr 
 |-  ( ( ( ph /\ E =/= C ) /\ B =/= C ) -> C e. P )
114 13 ad2antrr 
 |-  ( ( ( ph /\ E =/= C ) /\ B =/= C ) -> F e. P )
115 6 adantr 
 |-  ( ( ph /\ F = C ) -> G e. TarskiG )
116 11 adantr 
 |-  ( ( ph /\ F = C ) -> C e. P )
117 12 adantr 
 |-  ( ( ph /\ F = C ) -> E e. P )
118 19 adantr 
 |-  ( ( ph /\ F = C ) -> ( C .- E ) = ( C .- F ) )
119 simpr 
 |-  ( ( ph /\ F = C ) -> F = C )
120 119 oveq2d 
 |-  ( ( ph /\ F = C ) -> ( C .- F ) = ( C .- C ) )
121 118 120 eqtrd 
 |-  ( ( ph /\ F = C ) -> ( C .- E ) = ( C .- C ) )
122 1 2 3 115 116 117 116 121 axtgcgrid 
 |-  ( ( ph /\ F = C ) -> C = E )
123 122 eqcomd 
 |-  ( ( ph /\ F = C ) -> E = C )
124 123 adantlr 
 |-  ( ( ( ph /\ E =/= C ) /\ F = C ) -> E = C )
125 simplr 
 |-  ( ( ( ph /\ E =/= C ) /\ F = C ) -> E =/= C )
126 125 neneqd 
 |-  ( ( ( ph /\ E =/= C ) /\ F = C ) -> -. E = C )
127 124 126 pm2.65da 
 |-  ( ( ph /\ E =/= C ) -> -. F = C )
128 127 neqned 
 |-  ( ( ph /\ E =/= C ) -> F =/= C )
129 128 adantr 
 |-  ( ( ( ph /\ E =/= C ) /\ B =/= C ) -> F =/= C )
130 1 2 3 6 10 11 13 17 tgbtwncom 
 |-  ( ph -> C e. ( F I B ) )
131 130 ad2antrr 
 |-  ( ( ( ph /\ E =/= C ) /\ B =/= C ) -> C e. ( F I B ) )
132 1 2 3 4 5 110 113 56 114 mirbtwn 
 |-  ( ( ( ph /\ E =/= C ) /\ B =/= C ) -> C e. ( ( ( S ` C ) ` F ) I F ) )
133 1 2 3 110 112 113 114 132 tgbtwncom 
 |-  ( ( ( ph /\ E =/= C ) /\ B =/= C ) -> C e. ( F I ( ( S ` C ) ` F ) ) )
134 1 3 110 114 113 111 112 129 131 133 tgbtwnconn2 
 |-  ( ( ( ph /\ E =/= C ) /\ B =/= C ) -> ( B e. ( C I ( ( S ` C ) ` F ) ) \/ ( ( S ` C ) ` F ) e. ( C I B ) ) )
135 23 18 19 3brtr3d 
 |-  ( ph -> ( C .- B ) .<_ ( C .- F ) )
136 135 adantr 
 |-  ( ( ph /\ E =/= C ) -> ( C .- B ) .<_ ( C .- F ) )
137 1 2 3 4 5 53 55 56 76 mircgr 
 |-  ( ( ph /\ E =/= C ) -> ( C .- ( ( S ` C ) ` F ) ) = ( C .- F ) )
138 136 137 breqtrrd 
 |-  ( ( ph /\ E =/= C ) -> ( C .- B ) .<_ ( C .- ( ( S ` C ) ` F ) ) )
139 138 adantr 
 |-  ( ( ( ph /\ E =/= C ) /\ B =/= C ) -> ( C .- B ) .<_ ( C .- ( ( S ` C ) ` F ) ) )
140 1 2 3 22 110 111 112 113 111 134 139 legbtwn 
 |-  ( ( ( ph /\ E =/= C ) /\ B =/= C ) -> B e. ( C I ( ( S ` C ) ` F ) ) )
141 109 140 pm2.61dane 
 |-  ( ( ph /\ E =/= C ) -> B e. ( C I ( ( S ` C ) ` F ) ) )
142 1 2 3 53 55 71 77 141 tgbtwncom 
 |-  ( ( ph /\ E =/= C ) -> B e. ( ( ( S ` C ) ` F ) I C ) )
143 19 adantr 
 |-  ( ( ph /\ E =/= C ) -> ( C .- E ) = ( C .- F ) )
144 143 97 137 3eqtr4d 
 |-  ( ( ph /\ E =/= C ) -> ( C .- ( ( S ` C ) ` E ) ) = ( C .- ( ( S ` C ) ` F ) ) )
145 1 2 3 53 55 75 55 77 144 tgcgrcomlr 
 |-  ( ( ph /\ E =/= C ) -> ( ( ( S ` C ) ` E ) .- C ) = ( ( ( S ` C ) ` F ) .- C ) )
146 18 adantr 
 |-  ( ( ph /\ E =/= C ) -> ( C .- A ) = ( C .- B ) )
147 1 2 3 53 55 69 55 71 146 tgcgrcomlr 
 |-  ( ( ph /\ E =/= C ) -> ( A .- C ) = ( B .- C ) )
148 eqid 
 |-  ( S ` ( ( S ` C ) ` Y ) ) = ( S ` ( ( S ` C ) ` Y ) )
149 1 2 3 4 5 53 59 148 75 mircgr 
 |-  ( ( ph /\ E =/= C ) -> ( ( ( S ` C ) ` Y ) .- ( ( S ` ( ( S ` C ) ` Y ) ) ` ( ( S ` C ) ` E ) ) ) = ( ( ( S ` C ) ` Y ) .- ( ( S ` C ) ` E ) ) )
150 eqid 
 |-  ( ( S ` C ) ` Y ) = ( ( S ` C ) ` Y )
151 eqid 
 |-  ( ( S ` C ) ` E ) = ( ( S ` C ) ` E )
152 eqid 
 |-  ( ( S ` C ) ` F ) = ( ( S ` C ) ` F )
153 21 adantr 
 |-  ( ( ph /\ E =/= C ) -> F = ( N ` E ) )
154 8 fveq1i 
 |-  ( N ` E ) = ( ( S ` Y ) ` E )
155 153 154 eqtr2di 
 |-  ( ( ph /\ E =/= C ) -> ( ( S ` Y ) ` E ) = F )
156 1 2 3 4 5 53 56 150 151 152 55 58 74 76 155 mirauto 
 |-  ( ( ph /\ E =/= C ) -> ( ( S ` ( ( S ` C ) ` Y ) ) ` ( ( S ` C ) ` E ) ) = ( ( S ` C ) ` F ) )
157 156 oveq2d 
 |-  ( ( ph /\ E =/= C ) -> ( ( ( S ` C ) ` Y ) .- ( ( S ` ( ( S ` C ) ` Y ) ) ` ( ( S ` C ) ` E ) ) ) = ( ( ( S ` C ) ` Y ) .- ( ( S ` C ) ` F ) ) )
158 149 157 eqtr3d 
 |-  ( ( ph /\ E =/= C ) -> ( ( ( S ` C ) ` Y ) .- ( ( S ` C ) ` E ) ) = ( ( ( S ` C ) ` Y ) .- ( ( S ` C ) ` F ) ) )
159 1 2 3 53 59 75 59 77 158 tgcgrcomlr 
 |-  ( ( ph /\ E =/= C ) -> ( ( ( S ` C ) ` E ) .- ( ( S ` C ) ` Y ) ) = ( ( ( S ` C ) ` F ) .- ( ( S ` C ) ` Y ) ) )
160 eqidd 
 |-  ( ( ph /\ E =/= C ) -> ( C .- ( ( S ` C ) ` Y ) ) = ( C .- ( ( S ` C ) ` Y ) ) )
161 1 2 3 53 75 69 55 59 77 71 55 59 102 142 145 147 159 160 tgifscgr 
 |-  ( ( ph /\ E =/= C ) -> ( A .- ( ( S ` C ) ` Y ) ) = ( B .- ( ( S ` C ) ` Y ) ) )
162 1 2 3 53 69 59 71 59 161 tgcgrcomlr 
 |-  ( ( ph /\ E =/= C ) -> ( ( ( S ` C ) ` Y ) .- A ) = ( ( ( S ` C ) ` Y ) .- B ) )
163 162 ad3antrrr 
 |-  ( ( ( ( ( ph /\ E =/= C ) /\ q e. P ) /\ ( q e. ( ( ( S ` C ) ` Y ) I C ) /\ q e. ( A I B ) ) ) /\ ( ( S ` C ) ` Y ) = C ) -> ( ( ( S ` C ) ` Y ) .- A ) = ( ( ( S ` C ) ` Y ) .- B ) )
164 54 adantr 
 |-  ( ( ( ( ( ph /\ E =/= C ) /\ q e. P ) /\ ( q e. ( ( ( S ` C ) ` Y ) I C ) /\ q e. ( A I B ) ) ) /\ ( ( S ` C ) ` Y ) = C ) -> G e. TarskiG )
165 60 adantr 
 |-  ( ( ( ( ( ph /\ E =/= C ) /\ q e. P ) /\ ( q e. ( ( ( S ` C ) ` Y ) I C ) /\ q e. ( A I B ) ) ) /\ ( ( S ` C ) ` Y ) = C ) -> ( ( S ` C ) ` Y ) e. P )
166 61 adantr 
 |-  ( ( ( ( ( ph /\ E =/= C ) /\ q e. P ) /\ ( q e. ( ( ( S ` C ) ` Y ) I C ) /\ q e. ( A I B ) ) ) /\ ( ( S ` C ) ` Y ) = C ) -> q e. P )
167 64 adantr 
 |-  ( ( ( ( ( ph /\ E =/= C ) /\ q e. P ) /\ ( q e. ( ( ( S ` C ) ` Y ) I C ) /\ q e. ( A I B ) ) ) /\ ( ( S ` C ) ` Y ) = C ) -> q e. ( ( ( S ` C ) ` Y ) I C ) )
168 simpr 
 |-  ( ( ( ( ( ph /\ E =/= C ) /\ q e. P ) /\ ( q e. ( ( ( S ` C ) ` Y ) I C ) /\ q e. ( A I B ) ) ) /\ ( ( S ` C ) ` Y ) = C ) -> ( ( S ` C ) ` Y ) = C )
169 168 oveq2d 
 |-  ( ( ( ( ( ph /\ E =/= C ) /\ q e. P ) /\ ( q e. ( ( ( S ` C ) ` Y ) I C ) /\ q e. ( A I B ) ) ) /\ ( ( S ` C ) ` Y ) = C ) -> ( ( ( S ` C ) ` Y ) I ( ( S ` C ) ` Y ) ) = ( ( ( S ` C ) ` Y ) I C ) )
170 167 169 eleqtrrd 
 |-  ( ( ( ( ( ph /\ E =/= C ) /\ q e. P ) /\ ( q e. ( ( ( S ` C ) ` Y ) I C ) /\ q e. ( A I B ) ) ) /\ ( ( S ` C ) ` Y ) = C ) -> q e. ( ( ( S ` C ) ` Y ) I ( ( S ` C ) ` Y ) ) )
171 1 2 3 164 165 166 170 axtgbtwnid 
 |-  ( ( ( ( ( ph /\ E =/= C ) /\ q e. P ) /\ ( q e. ( ( ( S ` C ) ` Y ) I C ) /\ q e. ( A I B ) ) ) /\ ( ( S ` C ) ` Y ) = C ) -> ( ( S ` C ) ` Y ) = q )
172 171 oveq1d 
 |-  ( ( ( ( ( ph /\ E =/= C ) /\ q e. P ) /\ ( q e. ( ( ( S ` C ) ` Y ) I C ) /\ q e. ( A I B ) ) ) /\ ( ( S ` C ) ` Y ) = C ) -> ( ( ( S ` C ) ` Y ) .- A ) = ( q .- A ) )
173 171 oveq1d 
 |-  ( ( ( ( ( ph /\ E =/= C ) /\ q e. P ) /\ ( q e. ( ( ( S ` C ) ` Y ) I C ) /\ q e. ( A I B ) ) ) /\ ( ( S ` C ) ` Y ) = C ) -> ( ( ( S ` C ) ` Y ) .- B ) = ( q .- B ) )
174 163 172 173 3eqtr3d 
 |-  ( ( ( ( ( ph /\ E =/= C ) /\ q e. P ) /\ ( q e. ( ( ( S ` C ) ` Y ) I C ) /\ q e. ( A I B ) ) ) /\ ( ( S ` C ) ` Y ) = C ) -> ( q .- A ) = ( q .- B ) )
175 53 ad3antrrr 
 |-  ( ( ( ( ( ph /\ E =/= C ) /\ q e. P ) /\ ( q e. ( ( ( S ` C ) ` Y ) I C ) /\ q e. ( A I B ) ) ) /\ ( ( S ` C ) ` Y ) =/= C ) -> G e. TarskiG )
176 59 ad3antrrr 
 |-  ( ( ( ( ( ph /\ E =/= C ) /\ q e. P ) /\ ( q e. ( ( ( S ` C ) ` Y ) I C ) /\ q e. ( A I B ) ) ) /\ ( ( S ` C ) ` Y ) =/= C ) -> ( ( S ` C ) ` Y ) e. P )
177 55 ad3antrrr 
 |-  ( ( ( ( ( ph /\ E =/= C ) /\ q e. P ) /\ ( q e. ( ( ( S ` C ) ` Y ) I C ) /\ q e. ( A I B ) ) ) /\ ( ( S ` C ) ` Y ) =/= C ) -> C e. P )
178 61 adantr 
 |-  ( ( ( ( ( ph /\ E =/= C ) /\ q e. P ) /\ ( q e. ( ( ( S ` C ) ` Y ) I C ) /\ q e. ( A I B ) ) ) /\ ( ( S ` C ) ` Y ) =/= C ) -> q e. P )
179 eqid 
 |-  ( cgrG ` G ) = ( cgrG ` G )
180 69 ad3antrrr 
 |-  ( ( ( ( ( ph /\ E =/= C ) /\ q e. P ) /\ ( q e. ( ( ( S ` C ) ` Y ) I C ) /\ q e. ( A I B ) ) ) /\ ( ( S ` C ) ` Y ) =/= C ) -> A e. P )
181 71 ad3antrrr 
 |-  ( ( ( ( ( ph /\ E =/= C ) /\ q e. P ) /\ ( q e. ( ( ( S ` C ) ` Y ) I C ) /\ q e. ( A I B ) ) ) /\ ( ( S ` C ) ` Y ) =/= C ) -> B e. P )
182 simpr 
 |-  ( ( ( ( ( ph /\ E =/= C ) /\ q e. P ) /\ ( q e. ( ( ( S ` C ) ` Y ) I C ) /\ q e. ( A I B ) ) ) /\ ( ( S ` C ) ` Y ) =/= C ) -> ( ( S ` C ) ` Y ) =/= C )
183 60 adantr 
 |-  ( ( ( ( ( ph /\ E =/= C ) /\ q e. P ) /\ ( q e. ( ( ( S ` C ) ` Y ) I C ) /\ q e. ( A I B ) ) ) /\ ( ( S ` C ) ` Y ) =/= C ) -> ( ( S ` C ) ` Y ) e. P )
184 64 adantr 
 |-  ( ( ( ( ( ph /\ E =/= C ) /\ q e. P ) /\ ( q e. ( ( ( S ` C ) ` Y ) I C ) /\ q e. ( A I B ) ) ) /\ ( ( S ` C ) ` Y ) =/= C ) -> q e. ( ( ( S ` C ) ` Y ) I C ) )
185 1 4 3 175 183 178 177 184 btwncolg3 
 |-  ( ( ( ( ( ph /\ E =/= C ) /\ q e. P ) /\ ( q e. ( ( ( S ` C ) ` Y ) I C ) /\ q e. ( A I B ) ) ) /\ ( ( S ` C ) ` Y ) =/= C ) -> ( C e. ( ( ( S ` C ) ` Y ) L q ) \/ ( ( S ` C ) ` Y ) = q ) )
186 162 ad3antrrr 
 |-  ( ( ( ( ( ph /\ E =/= C ) /\ q e. P ) /\ ( q e. ( ( ( S ` C ) ` Y ) I C ) /\ q e. ( A I B ) ) ) /\ ( ( S ` C ) ` Y ) =/= C ) -> ( ( ( S ` C ) ` Y ) .- A ) = ( ( ( S ` C ) ` Y ) .- B ) )
187 146 ad3antrrr 
 |-  ( ( ( ( ( ph /\ E =/= C ) /\ q e. P ) /\ ( q e. ( ( ( S ` C ) ` Y ) I C ) /\ q e. ( A I B ) ) ) /\ ( ( S ` C ) ` Y ) =/= C ) -> ( C .- A ) = ( C .- B ) )
188 1 4 3 175 176 177 178 179 180 181 2 182 185 186 187 lncgr 
 |-  ( ( ( ( ( ph /\ E =/= C ) /\ q e. P ) /\ ( q e. ( ( ( S ` C ) ` Y ) I C ) /\ q e. ( A I B ) ) ) /\ ( ( S ` C ) ` Y ) =/= C ) -> ( q .- A ) = ( q .- B ) )
189 174 188 pm2.61dane 
 |-  ( ( ( ( ph /\ E =/= C ) /\ q e. P ) /\ ( q e. ( ( ( S ` C ) ` Y ) I C ) /\ q e. ( A I B ) ) ) -> ( q .- A ) = ( q .- B ) )
190 189 eqcomd 
 |-  ( ( ( ( ph /\ E =/= C ) /\ q e. P ) /\ ( q e. ( ( ( S ` C ) ` Y ) I C ) /\ q e. ( A I B ) ) ) -> ( q .- B ) = ( q .- A ) )
191 simprr 
 |-  ( ( ( ( ph /\ E =/= C ) /\ q e. P ) /\ ( q e. ( ( ( S ` C ) ` Y ) I C ) /\ q e. ( A I B ) ) ) -> q e. ( A I B ) )
192 1 2 3 54 70 61 72 191 tgbtwncom 
 |-  ( ( ( ( ph /\ E =/= C ) /\ q e. P ) /\ ( q e. ( ( ( S ` C ) ` Y ) I C ) /\ q e. ( A I B ) ) ) -> q e. ( B I A ) )
193 1 2 3 4 5 54 61 73 70 72 190 192 ismir 
 |-  ( ( ( ( ph /\ E =/= C ) /\ q e. P ) /\ ( q e. ( ( ( S ` C ) ` Y ) I C ) /\ q e. ( A I B ) ) ) -> B = ( ( S ` q ) ` A ) )
194 193 eqcomd 
 |-  ( ( ( ( ph /\ E =/= C ) /\ q e. P ) /\ ( q e. ( ( ( S ` C ) ` Y ) I C ) /\ q e. ( A I B ) ) ) -> ( ( S ` q ) ` A ) = B )
195 20 ad3antrrr 
 |-  ( ( ( ( ph /\ E =/= C ) /\ q e. P ) /\ ( q e. ( ( ( S ` C ) ` Y ) I C ) /\ q e. ( A I B ) ) ) -> B = ( M ` A ) )
196 7 fveq1i 
 |-  ( M ` A ) = ( ( S ` X ) ` A )
197 195 196 eqtr2di 
 |-  ( ( ( ( ph /\ E =/= C ) /\ q e. P ) /\ ( q e. ( ( ( S ` C ) ` Y ) I C ) /\ q e. ( A I B ) ) ) -> ( ( S ` X ) ` A ) = B )
198 1 2 3 4 5 54 61 68 70 72 194 197 miduniq 
 |-  ( ( ( ( ph /\ E =/= C ) /\ q e. P ) /\ ( q e. ( ( ( S ` C ) ` Y ) I C ) /\ q e. ( A I B ) ) ) -> q = X )
199 198 oveq1d 
 |-  ( ( ( ( ph /\ E =/= C ) /\ q e. P ) /\ ( q e. ( ( ( S ` C ) ` Y ) I C ) /\ q e. ( A I B ) ) ) -> ( q I Y ) = ( X I Y ) )
200 67 199 eleqtrd 
 |-  ( ( ( ( ph /\ E =/= C ) /\ q e. P ) /\ ( q e. ( ( ( S ` C ) ` Y ) I C ) /\ q e. ( A I B ) ) ) -> C e. ( X I Y ) )
201 1 2 3 4 5 53 58 8 74 mirbtwn 
 |-  ( ( ph /\ E =/= C ) -> Y e. ( ( N ` E ) I E ) )
202 153 oveq1d 
 |-  ( ( ph /\ E =/= C ) -> ( F I E ) = ( ( N ` E ) I E ) )
203 201 202 eleqtrrd 
 |-  ( ( ph /\ E =/= C ) -> Y e. ( F I E ) )
204 1 2 3 53 76 58 74 203 tgbtwncom 
 |-  ( ( ph /\ E =/= C ) -> Y e. ( E I F ) )
205 1 2 3 4 5 53 55 56 74 58 76 204 mirbtwni 
 |-  ( ( ph /\ E =/= C ) -> ( ( S ` C ) ` Y ) e. ( ( ( S ` C ) ` E ) I ( ( S ` C ) ` F ) ) )
206 1 2 3 53 75 69 55 77 71 59 102 142 205 tgtrisegint 
 |-  ( ( ph /\ E =/= C ) -> E. q e. P ( q e. ( ( ( S ` C ) ` Y ) I C ) /\ q e. ( A I B ) ) )
207 200 206 r19.29a 
 |-  ( ( ph /\ E =/= C ) -> C e. ( X I Y ) )
208 52 207 pm2.61dane 
 |-  ( ph -> C e. ( X I Y ) )