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