Metamath Proof Explorer

Theorem mirmid

Description: Point inversion preserves midpoints. (Contributed by Thierry Arnoux, 12-Dec-2019)

Ref Expression
Hypotheses ismid.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
ismid.d ⊢ − = ( dist ‘ 𝐺 )
ismid.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
ismid.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
ismid.1 ⊢ ( 𝜑 → 𝐺 DimTarskiG≥ 2 )
midcl.1 ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
midcl.2 ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
mirmid.s ⊢ 𝑆 = ( ( pInvG ‘ 𝐺 ) ‘ 𝑀 )
mirmid.x ⊢ ( 𝜑 → 𝑀 ∈ 𝑃 )
Assertion mirmid ( 𝜑 → ( ( 𝑆 ‘ 𝐴 ) ( midG ‘ 𝐺 ) ( 𝑆 ‘ 𝐵 ) ) = ( 𝑆 ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 ismid.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 ismid.d ⊢ − = ( dist ‘ 𝐺 )
3 ismid.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
4 ismid.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
5 ismid.1 ⊢ ( 𝜑 → 𝐺 DimTarskiG≥ 2 )
6 midcl.1 ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
7 midcl.2 ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
8 mirmid.s ⊢ 𝑆 = ( ( pInvG ‘ 𝐺 ) ‘ 𝑀 )
9 mirmid.x ⊢ ( 𝜑 → 𝑀 ∈ 𝑃 )
10 eqidd ⊢ ( 𝜑 → ( 𝐴 ( midG ‘ 𝐺 ) 𝐵 ) = ( 𝐴 ( midG ‘ 𝐺 ) 𝐵 ) )
11 eqid ⊢ ( pInvG ‘ 𝐺 ) = ( pInvG ‘ 𝐺 )
12 1 2 3 4 5 6 7 midcl ⊢ ( 𝜑 → ( 𝐴 ( midG ‘ 𝐺 ) 𝐵 ) ∈ 𝑃 )
13 1 2 3 4 5 6 7 11 12 ismidb ⊢ ( 𝜑 → ( 𝐵 = ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐵 ) ) ‘ 𝐴 ) ↔ ( 𝐴 ( midG ‘ 𝐺 ) 𝐵 ) = ( 𝐴 ( midG ‘ 𝐺 ) 𝐵 ) ) )
14 10 13 mpbird ⊢ ( 𝜑 → 𝐵 = ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐵 ) ) ‘ 𝐴 ) )
15 14 fveq2d ⊢ ( 𝜑 → ( 𝑆 ‘ 𝐵 ) = ( 𝑆 ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐵 ) ) ‘ 𝐴 ) ) )
16 eqid ⊢ ( LineG ‘ 𝐺 ) = ( LineG ‘ 𝐺 )
17 1 2 3 16 11 4 9 8 6 12 mirmir2 ⊢ ( 𝜑 → ( 𝑆 ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐵 ) ) ‘ 𝐴 ) ) = ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑆 ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐵 ) ) ) ‘ ( 𝑆 ‘ 𝐴 ) ) )
18 15 17 eqtrd ⊢ ( 𝜑 → ( 𝑆 ‘ 𝐵 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑆 ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐵 ) ) ) ‘ ( 𝑆 ‘ 𝐴 ) ) )
19 1 2 3 16 11 4 9 8 6 mircl ⊢ ( 𝜑 → ( 𝑆 ‘ 𝐴 ) ∈ 𝑃 )
20 1 2 3 16 11 4 9 8 7 mircl ⊢ ( 𝜑 → ( 𝑆 ‘ 𝐵 ) ∈ 𝑃 )
21 1 2 3 16 11 4 9 8 12 mircl ⊢ ( 𝜑 → ( 𝑆 ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐵 ) ) ∈ 𝑃 )
22 1 2 3 4 5 19 20 11 21 ismidb ⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝐵 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑆 ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐵 ) ) ) ‘ ( 𝑆 ‘ 𝐴 ) ) ↔ ( ( 𝑆 ‘ 𝐴 ) ( midG ‘ 𝐺 ) ( 𝑆 ‘ 𝐵 ) ) = ( 𝑆 ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐵 ) ) ) )
23 18 22 mpbid ⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝐴 ) ( midG ‘ 𝐺 ) ( 𝑆 ‘ 𝐵 ) ) = ( 𝑆 ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐵 ) ) )