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 ⊢ ( 𝜑 → 𝐴 ∈ ( 𝑋 𝐼 ( 𝑀 ‘ 𝑌 ) ) )