Metamath Proof Explorer

Theorem mirmir2

Description: Point inversion of a point inversion through another point. (Contributed by Thierry Arnoux, 3-Nov-2019)

Ref Expression
Hypotheses mirval.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
mirval.d ⊢ − = ( dist ‘ 𝐺 )
mirval.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
mirval.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
mirval.s ⊢ 𝑆 = ( pInvG ‘ 𝐺 )
mirval.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
mirval.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
mirfv.m ⊢ 𝑀 = ( 𝑆 ‘ 𝐴 )
miriso.1 ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
miriso.2 ⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
Assertion mirmir2 ( 𝜑 → ( 𝑀 ‘ ( ( 𝑆 ‘ 𝑌 ) ‘ 𝑋 ) ) = ( ( 𝑆 ‘ ( 𝑀 ‘ 𝑌 ) ) ‘ ( 𝑀 ‘ 𝑋 ) ) )

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 mirval.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
8 mirfv.m ⊢ 𝑀 = ( 𝑆 ‘ 𝐴 )
9 miriso.1 ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
10 miriso.2 ⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
11 1 2 3 4 5 6 7 8 10 mircl ⊢ ( 𝜑 → ( 𝑀 ‘ 𝑌 ) ∈ 𝑃 )
12 eqid ⊢ ( 𝑆 ‘ ( 𝑀 ‘ 𝑌 ) ) = ( 𝑆 ‘ ( 𝑀 ‘ 𝑌 ) )
13 1 2 3 4 5 6 7 8 9 mircl ⊢ ( 𝜑 → ( 𝑀 ‘ 𝑋 ) ∈ 𝑃 )
14 eqid ⊢ ( 𝑆 ‘ 𝑌 ) = ( 𝑆 ‘ 𝑌 )
15 1 2 3 4 5 6 10 14 9 mircl ⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝑌 ) ‘ 𝑋 ) ∈ 𝑃 )
16 1 2 3 4 5 6 7 8 15 mircl ⊢ ( 𝜑 → ( 𝑀 ‘ ( ( 𝑆 ‘ 𝑌 ) ‘ 𝑋 ) ) ∈ 𝑃 )
17 1 2 3 4 5 6 10 14 9 mircgr ⊢ ( 𝜑 → ( 𝑌 − ( ( 𝑆 ‘ 𝑌 ) ‘ 𝑋 ) ) = ( 𝑌 − 𝑋 ) )
18 1 2 3 4 5 6 7 8 10 15 10 9 17 mircgrs ⊢ ( 𝜑 → ( ( 𝑀 ‘ 𝑌 ) − ( 𝑀 ‘ ( ( 𝑆 ‘ 𝑌 ) ‘ 𝑋 ) ) ) = ( ( 𝑀 ‘ 𝑌 ) − ( 𝑀 ‘ 𝑋 ) ) )
19 1 2 3 4 5 6 10 14 9 mirbtwn ⊢ ( 𝜑 → 𝑌 ∈ ( ( ( 𝑆 ‘ 𝑌 ) ‘ 𝑋 ) 𝐼 𝑋 ) )
20 1 2 3 4 5 6 7 8 15 10 9 19 mirbtwni ⊢ ( 𝜑 → ( 𝑀 ‘ 𝑌 ) ∈ ( ( 𝑀 ‘ ( ( 𝑆 ‘ 𝑌 ) ‘ 𝑋 ) ) 𝐼 ( 𝑀 ‘ 𝑋 ) ) )
21 1 2 3 4 5 6 11 12 13 16 18 20 ismir ⊢ ( 𝜑 → ( 𝑀 ‘ ( ( 𝑆 ‘ 𝑌 ) ‘ 𝑋 ) ) = ( ( 𝑆 ‘ ( 𝑀 ‘ 𝑌 ) ) ‘ ( 𝑀 ‘ 𝑋 ) ) )