Metamath Proof Explorer


Theorem mirconn

Description: Point inversion of connectedness. (Contributed by Thierry Arnoux, 2-Mar-2020)

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 )
mirconn.m
|- M = ( S ` A )
mirconn.a
|- ( ph -> A e. P )
mirconn.x
|- ( ph -> X e. P )
mirconn.y
|- ( ph -> Y e. P )
mirconn.1
|- ( ph -> ( X e. ( A I Y ) \/ Y e. ( A I X ) ) )
Assertion mirconn
|- ( ph -> A e. ( X I ( M ` 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 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 ) ) )