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 |
|
mirconn.m |
|- M = ( S ` A ) |
8 |
|
mirconn.a |
|- ( ph -> A e. P ) |
9 |
|
mirconn.x |
|- ( ph -> X e. P ) |
10 |
|
mirconn.y |
|- ( ph -> Y e. P ) |
11 |
|
mirconn.1 |
|- ( ph -> ( X e. ( A I Y ) \/ Y e. ( A I X ) ) ) |
12 |
6
|
adantr |
|- ( ( ph /\ X e. ( A I Y ) ) -> G e. TarskiG ) |
13 |
9
|
adantr |
|- ( ( ph /\ X e. ( A I Y ) ) -> X e. P ) |
14 |
8
|
adantr |
|- ( ( ph /\ X e. ( A I Y ) ) -> A e. P ) |
15 |
1 2 3 4 5 6 8 7 10
|
mircl |
|- ( ph -> ( M ` Y ) e. P ) |
16 |
15
|
adantr |
|- ( ( ph /\ X e. ( A I Y ) ) -> ( M ` Y ) e. P ) |
17 |
10
|
adantr |
|- ( ( ph /\ X e. ( A I Y ) ) -> Y e. P ) |
18 |
|
simpr |
|- ( ( ph /\ X e. ( A I Y ) ) -> X e. ( A I Y ) ) |
19 |
1 2 3 4 5 6 8 7 10
|
mirbtwn |
|- ( ph -> A e. ( ( M ` Y ) I Y ) ) |
20 |
19
|
adantr |
|- ( ( ph /\ X e. ( A I Y ) ) -> A e. ( ( M ` Y ) I Y ) ) |
21 |
1 2 3 12 13 14 16 17 18 20
|
tgbtwnintr |
|- ( ( ph /\ X e. ( A I Y ) ) -> A e. ( X I ( M ` Y ) ) ) |
22 |
1 2 3 6 9 8
|
tgbtwntriv2 |
|- ( ph -> A e. ( X I A ) ) |
23 |
22
|
adantr |
|- ( ( ph /\ Y = A ) -> A e. ( X I A ) ) |
24 |
|
simpr |
|- ( ( ph /\ Y = A ) -> Y = A ) |
25 |
24
|
fveq2d |
|- ( ( ph /\ Y = A ) -> ( M ` Y ) = ( M ` A ) ) |
26 |
1 2 3 4 5 6 8 7
|
mircinv |
|- ( ph -> ( M ` A ) = A ) |
27 |
26
|
adantr |
|- ( ( ph /\ Y = A ) -> ( M ` A ) = A ) |
28 |
25 27
|
eqtrd |
|- ( ( ph /\ Y = A ) -> ( M ` Y ) = A ) |
29 |
28
|
oveq2d |
|- ( ( ph /\ Y = A ) -> ( X I ( M ` Y ) ) = ( X I A ) ) |
30 |
23 29
|
eleqtrrd |
|- ( ( ph /\ Y = A ) -> A e. ( X I ( M ` Y ) ) ) |
31 |
30
|
adantlr |
|- ( ( ( ph /\ Y e. ( A I X ) ) /\ Y = A ) -> A e. ( X I ( M ` Y ) ) ) |
32 |
6
|
ad2antrr |
|- ( ( ( ph /\ Y e. ( A I X ) ) /\ Y =/= A ) -> G e. TarskiG ) |
33 |
9
|
ad2antrr |
|- ( ( ( ph /\ Y e. ( A I X ) ) /\ Y =/= A ) -> X e. P ) |
34 |
10
|
ad2antrr |
|- ( ( ( ph /\ Y e. ( A I X ) ) /\ Y =/= A ) -> Y e. P ) |
35 |
8
|
ad2antrr |
|- ( ( ( ph /\ Y e. ( A I X ) ) /\ Y =/= A ) -> A e. P ) |
36 |
15
|
ad2antrr |
|- ( ( ( ph /\ Y e. ( A I X ) ) /\ Y =/= A ) -> ( M ` Y ) e. P ) |
37 |
|
simpr |
|- ( ( ( ph /\ Y e. ( A I X ) ) /\ Y =/= A ) -> Y =/= A ) |
38 |
|
simplr |
|- ( ( ( ph /\ Y e. ( A I X ) ) /\ Y =/= A ) -> Y e. ( A I X ) ) |
39 |
1 2 3 32 35 34 33 38
|
tgbtwncom |
|- ( ( ( ph /\ Y e. ( A I X ) ) /\ Y =/= A ) -> Y e. ( X I A ) ) |
40 |
1 2 3 6 15 8 10 19
|
tgbtwncom |
|- ( ph -> A e. ( Y I ( M ` Y ) ) ) |
41 |
40
|
ad2antrr |
|- ( ( ( ph /\ Y e. ( A I X ) ) /\ Y =/= A ) -> A e. ( Y I ( M ` Y ) ) ) |
42 |
1 2 3 32 33 34 35 36 37 39 41
|
tgbtwnouttr2 |
|- ( ( ( ph /\ Y e. ( A I X ) ) /\ Y =/= A ) -> A e. ( X I ( M ` Y ) ) ) |
43 |
31 42
|
pm2.61dane |
|- ( ( ph /\ Y e. ( A I X ) ) -> A e. ( X I ( M ` Y ) ) ) |
44 |
21 43 11
|
mpjaodan |
|- ( ph -> A e. ( X I ( M ` Y ) ) ) |