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 |
|
mirhl.m |
|- M = ( S ` A ) |
8 |
|
mirhl.k |
|- K = ( hlG ` G ) |
9 |
|
mirhl.a |
|- ( ph -> A e. P ) |
10 |
|
mirhl.x |
|- ( ph -> X e. P ) |
11 |
|
mirhl.y |
|- ( ph -> Y e. P ) |
12 |
|
mirhl.z |
|- ( ph -> Z e. P ) |
13 |
|
mirbtwnhl.1 |
|- ( ph -> X =/= A ) |
14 |
|
mirbtwnhl.2 |
|- ( ph -> Y =/= A ) |
15 |
|
mirbtwnhl.3 |
|- ( ph -> A e. ( X I Y ) ) |
16 |
|
simpr |
|- ( ( ph /\ Z = A ) -> Z = A ) |
17 |
1 3 8 9 10 9 6
|
hleqnid |
|- ( ph -> -. A ( K ` A ) X ) |
18 |
17
|
adantr |
|- ( ( ph /\ Z = A ) -> -. A ( K ` A ) X ) |
19 |
16 18
|
eqnbrtrd |
|- ( ( ph /\ Z = A ) -> -. Z ( K ` A ) X ) |
20 |
16
|
fveq2d |
|- ( ( ph /\ Z = A ) -> ( M ` Z ) = ( M ` A ) ) |
21 |
1 2 3 4 5 6 9 7
|
mircinv |
|- ( ph -> ( M ` A ) = A ) |
22 |
21
|
adantr |
|- ( ( ph /\ Z = A ) -> ( M ` A ) = A ) |
23 |
20 22
|
eqtrd |
|- ( ( ph /\ Z = A ) -> ( M ` Z ) = A ) |
24 |
1 3 8 9 11 9 6
|
hleqnid |
|- ( ph -> -. A ( K ` A ) Y ) |
25 |
24
|
adantr |
|- ( ( ph /\ Z = A ) -> -. A ( K ` A ) Y ) |
26 |
23 25
|
eqnbrtrd |
|- ( ( ph /\ Z = A ) -> -. ( M ` Z ) ( K ` A ) Y ) |
27 |
19 26
|
2falsed |
|- ( ( ph /\ Z = A ) -> ( Z ( K ` A ) X <-> ( M ` Z ) ( K ` A ) Y ) ) |
28 |
|
simplr |
|- ( ( ( ph /\ Z =/= A ) /\ Z ( K ` A ) X ) -> Z =/= A ) |
29 |
28
|
neneqd |
|- ( ( ( ph /\ Z =/= A ) /\ Z ( K ` A ) X ) -> -. Z = A ) |
30 |
6
|
ad3antrrr |
|- ( ( ( ( ph /\ Z =/= A ) /\ Z ( K ` A ) X ) /\ ( M ` Z ) = A ) -> G e. TarskiG ) |
31 |
9
|
ad3antrrr |
|- ( ( ( ( ph /\ Z =/= A ) /\ Z ( K ` A ) X ) /\ ( M ` Z ) = A ) -> A e. P ) |
32 |
12
|
ad3antrrr |
|- ( ( ( ( ph /\ Z =/= A ) /\ Z ( K ` A ) X ) /\ ( M ` Z ) = A ) -> Z e. P ) |
33 |
|
simpr |
|- ( ( ( ( ph /\ Z =/= A ) /\ Z ( K ` A ) X ) /\ ( M ` Z ) = A ) -> ( M ` Z ) = A ) |
34 |
21
|
ad3antrrr |
|- ( ( ( ( ph /\ Z =/= A ) /\ Z ( K ` A ) X ) /\ ( M ` Z ) = A ) -> ( M ` A ) = A ) |
35 |
33 34
|
eqtr4d |
|- ( ( ( ( ph /\ Z =/= A ) /\ Z ( K ` A ) X ) /\ ( M ` Z ) = A ) -> ( M ` Z ) = ( M ` A ) ) |
36 |
1 2 3 4 5 30 31 7 32 31 35
|
mireq |
|- ( ( ( ( ph /\ Z =/= A ) /\ Z ( K ` A ) X ) /\ ( M ` Z ) = A ) -> Z = A ) |
37 |
29 36
|
mtand |
|- ( ( ( ph /\ Z =/= A ) /\ Z ( K ` A ) X ) -> -. ( M ` Z ) = A ) |
38 |
37
|
neqned |
|- ( ( ( ph /\ Z =/= A ) /\ Z ( K ` A ) X ) -> ( M ` Z ) =/= A ) |
39 |
14
|
ad2antrr |
|- ( ( ( ph /\ Z =/= A ) /\ Z ( K ` A ) X ) -> Y =/= A ) |
40 |
6
|
ad2antrr |
|- ( ( ( ph /\ Z =/= A ) /\ Z ( K ` A ) X ) -> G e. TarskiG ) |
41 |
10
|
ad2antrr |
|- ( ( ( ph /\ Z =/= A ) /\ Z ( K ` A ) X ) -> X e. P ) |
42 |
9
|
ad2antrr |
|- ( ( ( ph /\ Z =/= A ) /\ Z ( K ` A ) X ) -> A e. P ) |
43 |
1 2 3 4 5 6 9 7 12
|
mircl |
|- ( ph -> ( M ` Z ) e. P ) |
44 |
43
|
ad2antrr |
|- ( ( ( ph /\ Z =/= A ) /\ Z ( K ` A ) X ) -> ( M ` Z ) e. P ) |
45 |
11
|
ad2antrr |
|- ( ( ( ph /\ Z =/= A ) /\ Z ( K ` A ) X ) -> Y e. P ) |
46 |
13
|
ad2antrr |
|- ( ( ( ph /\ Z =/= A ) /\ Z ( K ` A ) X ) -> X =/= A ) |
47 |
12
|
ad2antrr |
|- ( ( ( ph /\ Z =/= A ) /\ Z ( K ` A ) X ) -> Z e. P ) |
48 |
1 3 8 12 10 9 6
|
ishlg |
|- ( ph -> ( Z ( K ` A ) X <-> ( Z =/= A /\ X =/= A /\ ( Z e. ( A I X ) \/ X e. ( A I Z ) ) ) ) ) |
49 |
48
|
adantr |
|- ( ( ph /\ Z =/= A ) -> ( Z ( K ` A ) X <-> ( Z =/= A /\ X =/= A /\ ( Z e. ( A I X ) \/ X e. ( A I Z ) ) ) ) ) |
50 |
49
|
biimpa |
|- ( ( ( ph /\ Z =/= A ) /\ Z ( K ` A ) X ) -> ( Z =/= A /\ X =/= A /\ ( Z e. ( A I X ) \/ X e. ( A I Z ) ) ) ) |
51 |
50
|
simp3d |
|- ( ( ( ph /\ Z =/= A ) /\ Z ( K ` A ) X ) -> ( Z e. ( A I X ) \/ X e. ( A I Z ) ) ) |
52 |
51
|
orcomd |
|- ( ( ( ph /\ Z =/= A ) /\ Z ( K ` A ) X ) -> ( X e. ( A I Z ) \/ Z e. ( A I X ) ) ) |
53 |
1 2 3 4 5 40 7 42 41 47 52
|
mirconn |
|- ( ( ( ph /\ Z =/= A ) /\ Z ( K ` A ) X ) -> A e. ( X I ( M ` Z ) ) ) |
54 |
15
|
ad2antrr |
|- ( ( ( ph /\ Z =/= A ) /\ Z ( K ` A ) X ) -> A e. ( X I Y ) ) |
55 |
1 3 40 41 42 44 45 46 53 54
|
tgbtwnconn2 |
|- ( ( ( ph /\ Z =/= A ) /\ Z ( K ` A ) X ) -> ( ( M ` Z ) e. ( A I Y ) \/ Y e. ( A I ( M ` Z ) ) ) ) |
56 |
1 3 8 43 11 9 6
|
ishlg |
|- ( ph -> ( ( M ` Z ) ( K ` A ) Y <-> ( ( M ` Z ) =/= A /\ Y =/= A /\ ( ( M ` Z ) e. ( A I Y ) \/ Y e. ( A I ( M ` Z ) ) ) ) ) ) |
57 |
56
|
adantr |
|- ( ( ph /\ Z =/= A ) -> ( ( M ` Z ) ( K ` A ) Y <-> ( ( M ` Z ) =/= A /\ Y =/= A /\ ( ( M ` Z ) e. ( A I Y ) \/ Y e. ( A I ( M ` Z ) ) ) ) ) ) |
58 |
57
|
adantr |
|- ( ( ( ph /\ Z =/= A ) /\ Z ( K ` A ) X ) -> ( ( M ` Z ) ( K ` A ) Y <-> ( ( M ` Z ) =/= A /\ Y =/= A /\ ( ( M ` Z ) e. ( A I Y ) \/ Y e. ( A I ( M ` Z ) ) ) ) ) ) |
59 |
38 39 55 58
|
mpbir3and |
|- ( ( ( ph /\ Z =/= A ) /\ Z ( K ` A ) X ) -> ( M ` Z ) ( K ` A ) Y ) |
60 |
|
simplr |
|- ( ( ( ph /\ Z =/= A ) /\ ( M ` Z ) ( K ` A ) Y ) -> Z =/= A ) |
61 |
13
|
ad2antrr |
|- ( ( ( ph /\ Z =/= A ) /\ ( M ` Z ) ( K ` A ) Y ) -> X =/= A ) |
62 |
6
|
ad2antrr |
|- ( ( ( ph /\ Z =/= A ) /\ ( M ` Z ) ( K ` A ) Y ) -> G e. TarskiG ) |
63 |
11
|
ad2antrr |
|- ( ( ( ph /\ Z =/= A ) /\ ( M ` Z ) ( K ` A ) Y ) -> Y e. P ) |
64 |
9
|
ad2antrr |
|- ( ( ( ph /\ Z =/= A ) /\ ( M ` Z ) ( K ` A ) Y ) -> A e. P ) |
65 |
12
|
ad2antrr |
|- ( ( ( ph /\ Z =/= A ) /\ ( M ` Z ) ( K ` A ) Y ) -> Z e. P ) |
66 |
10
|
ad2antrr |
|- ( ( ( ph /\ Z =/= A ) /\ ( M ` Z ) ( K ` A ) Y ) -> X e. P ) |
67 |
14
|
ad2antrr |
|- ( ( ( ph /\ Z =/= A ) /\ ( M ` Z ) ( K ` A ) Y ) -> Y =/= A ) |
68 |
21
|
ad2antrr |
|- ( ( ( ph /\ Z =/= A ) /\ ( M ` Z ) ( K ` A ) Y ) -> ( M ` A ) = A ) |
69 |
43
|
ad2antrr |
|- ( ( ( ph /\ Z =/= A ) /\ ( M ` Z ) ( K ` A ) Y ) -> ( M ` Z ) e. P ) |
70 |
1 2 3 4 5 62 64 7 63
|
mircl |
|- ( ( ( ph /\ Z =/= A ) /\ ( M ` Z ) ( K ` A ) Y ) -> ( M ` Y ) e. P ) |
71 |
57
|
biimpa |
|- ( ( ( ph /\ Z =/= A ) /\ ( M ` Z ) ( K ` A ) Y ) -> ( ( M ` Z ) =/= A /\ Y =/= A /\ ( ( M ` Z ) e. ( A I Y ) \/ Y e. ( A I ( M ` Z ) ) ) ) ) |
72 |
71
|
simp3d |
|- ( ( ( ph /\ Z =/= A ) /\ ( M ` Z ) ( K ` A ) Y ) -> ( ( M ` Z ) e. ( A I Y ) \/ Y e. ( A I ( M ` Z ) ) ) ) |
73 |
1 2 3 4 5 62 7 64 69 63 72
|
mirconn |
|- ( ( ( ph /\ Z =/= A ) /\ ( M ` Z ) ( K ` A ) Y ) -> A e. ( ( M ` Z ) I ( M ` Y ) ) ) |
74 |
1 2 3 62 69 64 70 73
|
tgbtwncom |
|- ( ( ( ph /\ Z =/= A ) /\ ( M ` Z ) ( K ` A ) Y ) -> A e. ( ( M ` Y ) I ( M ` Z ) ) ) |
75 |
68 74
|
eqeltrd |
|- ( ( ( ph /\ Z =/= A ) /\ ( M ` Z ) ( K ` A ) Y ) -> ( M ` A ) e. ( ( M ` Y ) I ( M ` Z ) ) ) |
76 |
1 2 3 4 5 62 64 7 63 64 65
|
mirbtwnb |
|- ( ( ( ph /\ Z =/= A ) /\ ( M ` Z ) ( K ` A ) Y ) -> ( A e. ( Y I Z ) <-> ( M ` A ) e. ( ( M ` Y ) I ( M ` Z ) ) ) ) |
77 |
75 76
|
mpbird |
|- ( ( ( ph /\ Z =/= A ) /\ ( M ` Z ) ( K ` A ) Y ) -> A e. ( Y I Z ) ) |
78 |
1 2 3 6 10 9 11 15
|
tgbtwncom |
|- ( ph -> A e. ( Y I X ) ) |
79 |
78
|
ad2antrr |
|- ( ( ( ph /\ Z =/= A ) /\ ( M ` Z ) ( K ` A ) Y ) -> A e. ( Y I X ) ) |
80 |
1 3 62 63 64 65 66 67 77 79
|
tgbtwnconn2 |
|- ( ( ( ph /\ Z =/= A ) /\ ( M ` Z ) ( K ` A ) Y ) -> ( Z e. ( A I X ) \/ X e. ( A I Z ) ) ) |
81 |
49
|
adantr |
|- ( ( ( ph /\ Z =/= A ) /\ ( M ` Z ) ( K ` A ) Y ) -> ( Z ( K ` A ) X <-> ( Z =/= A /\ X =/= A /\ ( Z e. ( A I X ) \/ X e. ( A I Z ) ) ) ) ) |
82 |
60 61 80 81
|
mpbir3and |
|- ( ( ( ph /\ Z =/= A ) /\ ( M ` Z ) ( K ` A ) Y ) -> Z ( K ` A ) X ) |
83 |
59 82
|
impbida |
|- ( ( ph /\ Z =/= A ) -> ( Z ( K ` A ) X <-> ( M ` Z ) ( K ` A ) Y ) ) |
84 |
27 83
|
pm2.61dane |
|- ( ph -> ( Z ( K ` A ) X <-> ( M ` Z ) ( K ` A ) Y ) ) |