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 ) ) |