Metamath Proof Explorer


Theorem mirconn

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

Ref Expression
Hypotheses mirval.p 𝑃 = ( Base ‘ 𝐺 )
mirval.d = ( dist ‘ 𝐺 )
mirval.i 𝐼 = ( Itv ‘ 𝐺 )
mirval.l 𝐿 = ( LineG ‘ 𝐺 )
mirval.s 𝑆 = ( pInvG ‘ 𝐺 )
mirval.g ( 𝜑𝐺 ∈ TarskiG )
mirconn.m 𝑀 = ( 𝑆𝐴 )
mirconn.a ( 𝜑𝐴𝑃 )
mirconn.x ( 𝜑𝑋𝑃 )
mirconn.y ( 𝜑𝑌𝑃 )
mirconn.1 ( 𝜑 → ( 𝑋 ∈ ( 𝐴 𝐼 𝑌 ) ∨ 𝑌 ∈ ( 𝐴 𝐼 𝑋 ) ) )
Assertion mirconn ( 𝜑𝐴 ∈ ( 𝑋 𝐼 ( 𝑀𝑌 ) ) )

Proof

Step Hyp Ref Expression
1 mirval.p 𝑃 = ( Base ‘ 𝐺 )
2 mirval.d = ( dist ‘ 𝐺 )
3 mirval.i 𝐼 = ( Itv ‘ 𝐺 )
4 mirval.l 𝐿 = ( LineG ‘ 𝐺 )
5 mirval.s 𝑆 = ( pInvG ‘ 𝐺 )
6 mirval.g ( 𝜑𝐺 ∈ TarskiG )
7 mirconn.m 𝑀 = ( 𝑆𝐴 )
8 mirconn.a ( 𝜑𝐴𝑃 )
9 mirconn.x ( 𝜑𝑋𝑃 )
10 mirconn.y ( 𝜑𝑌𝑃 )
11 mirconn.1 ( 𝜑 → ( 𝑋 ∈ ( 𝐴 𝐼 𝑌 ) ∨ 𝑌 ∈ ( 𝐴 𝐼 𝑋 ) ) )
12 6 adantr ( ( 𝜑𝑋 ∈ ( 𝐴 𝐼 𝑌 ) ) → 𝐺 ∈ TarskiG )
13 9 adantr ( ( 𝜑𝑋 ∈ ( 𝐴 𝐼 𝑌 ) ) → 𝑋𝑃 )
14 8 adantr ( ( 𝜑𝑋 ∈ ( 𝐴 𝐼 𝑌 ) ) → 𝐴𝑃 )
15 1 2 3 4 5 6 8 7 10 mircl ( 𝜑 → ( 𝑀𝑌 ) ∈ 𝑃 )
16 15 adantr ( ( 𝜑𝑋 ∈ ( 𝐴 𝐼 𝑌 ) ) → ( 𝑀𝑌 ) ∈ 𝑃 )
17 10 adantr ( ( 𝜑𝑋 ∈ ( 𝐴 𝐼 𝑌 ) ) → 𝑌𝑃 )
18 simpr ( ( 𝜑𝑋 ∈ ( 𝐴 𝐼 𝑌 ) ) → 𝑋 ∈ ( 𝐴 𝐼 𝑌 ) )
19 1 2 3 4 5 6 8 7 10 mirbtwn ( 𝜑𝐴 ∈ ( ( 𝑀𝑌 ) 𝐼 𝑌 ) )
20 19 adantr ( ( 𝜑𝑋 ∈ ( 𝐴 𝐼 𝑌 ) ) → 𝐴 ∈ ( ( 𝑀𝑌 ) 𝐼 𝑌 ) )
21 1 2 3 12 13 14 16 17 18 20 tgbtwnintr ( ( 𝜑𝑋 ∈ ( 𝐴 𝐼 𝑌 ) ) → 𝐴 ∈ ( 𝑋 𝐼 ( 𝑀𝑌 ) ) )
22 1 2 3 6 9 8 tgbtwntriv2 ( 𝜑𝐴 ∈ ( 𝑋 𝐼 𝐴 ) )
23 22 adantr ( ( 𝜑𝑌 = 𝐴 ) → 𝐴 ∈ ( 𝑋 𝐼 𝐴 ) )
24 simpr ( ( 𝜑𝑌 = 𝐴 ) → 𝑌 = 𝐴 )
25 24 fveq2d ( ( 𝜑𝑌 = 𝐴 ) → ( 𝑀𝑌 ) = ( 𝑀𝐴 ) )
26 1 2 3 4 5 6 8 7 mircinv ( 𝜑 → ( 𝑀𝐴 ) = 𝐴 )
27 26 adantr ( ( 𝜑𝑌 = 𝐴 ) → ( 𝑀𝐴 ) = 𝐴 )
28 25 27 eqtrd ( ( 𝜑𝑌 = 𝐴 ) → ( 𝑀𝑌 ) = 𝐴 )
29 28 oveq2d ( ( 𝜑𝑌 = 𝐴 ) → ( 𝑋 𝐼 ( 𝑀𝑌 ) ) = ( 𝑋 𝐼 𝐴 ) )
30 23 29 eleqtrrd ( ( 𝜑𝑌 = 𝐴 ) → 𝐴 ∈ ( 𝑋 𝐼 ( 𝑀𝑌 ) ) )
31 30 adantlr ( ( ( 𝜑𝑌 ∈ ( 𝐴 𝐼 𝑋 ) ) ∧ 𝑌 = 𝐴 ) → 𝐴 ∈ ( 𝑋 𝐼 ( 𝑀𝑌 ) ) )
32 6 ad2antrr ( ( ( 𝜑𝑌 ∈ ( 𝐴 𝐼 𝑋 ) ) ∧ 𝑌𝐴 ) → 𝐺 ∈ TarskiG )
33 9 ad2antrr ( ( ( 𝜑𝑌 ∈ ( 𝐴 𝐼 𝑋 ) ) ∧ 𝑌𝐴 ) → 𝑋𝑃 )
34 10 ad2antrr ( ( ( 𝜑𝑌 ∈ ( 𝐴 𝐼 𝑋 ) ) ∧ 𝑌𝐴 ) → 𝑌𝑃 )
35 8 ad2antrr ( ( ( 𝜑𝑌 ∈ ( 𝐴 𝐼 𝑋 ) ) ∧ 𝑌𝐴 ) → 𝐴𝑃 )
36 15 ad2antrr ( ( ( 𝜑𝑌 ∈ ( 𝐴 𝐼 𝑋 ) ) ∧ 𝑌𝐴 ) → ( 𝑀𝑌 ) ∈ 𝑃 )
37 simpr ( ( ( 𝜑𝑌 ∈ ( 𝐴 𝐼 𝑋 ) ) ∧ 𝑌𝐴 ) → 𝑌𝐴 )
38 simplr ( ( ( 𝜑𝑌 ∈ ( 𝐴 𝐼 𝑋 ) ) ∧ 𝑌𝐴 ) → 𝑌 ∈ ( 𝐴 𝐼 𝑋 ) )
39 1 2 3 32 35 34 33 38 tgbtwncom ( ( ( 𝜑𝑌 ∈ ( 𝐴 𝐼 𝑋 ) ) ∧ 𝑌𝐴 ) → 𝑌 ∈ ( 𝑋 𝐼 𝐴 ) )
40 1 2 3 6 15 8 10 19 tgbtwncom ( 𝜑𝐴 ∈ ( 𝑌 𝐼 ( 𝑀𝑌 ) ) )
41 40 ad2antrr ( ( ( 𝜑𝑌 ∈ ( 𝐴 𝐼 𝑋 ) ) ∧ 𝑌𝐴 ) → 𝐴 ∈ ( 𝑌 𝐼 ( 𝑀𝑌 ) ) )
42 1 2 3 32 33 34 35 36 37 39 41 tgbtwnouttr2 ( ( ( 𝜑𝑌 ∈ ( 𝐴 𝐼 𝑋 ) ) ∧ 𝑌𝐴 ) → 𝐴 ∈ ( 𝑋 𝐼 ( 𝑀𝑌 ) ) )
43 31 42 pm2.61dane ( ( 𝜑𝑌 ∈ ( 𝐴 𝐼 𝑋 ) ) → 𝐴 ∈ ( 𝑋 𝐼 ( 𝑀𝑌 ) ) )
44 21 43 11 mpjaodan ( 𝜑𝐴 ∈ ( 𝑋 𝐼 ( 𝑀𝑌 ) ) )