Metamath Proof Explorer

Theorem miduniq2

Description: If two point inversions commute, they are identical. Theorem 7.19 of Schwabhauser p. 52. (Contributed by Thierry Arnoux, 30-Jul-2019)

Ref Expression
Hypotheses mirval.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
mirval.d ⊢ − = ( dist ‘ 𝐺 )
mirval.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
mirval.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
mirval.s ⊢ 𝑆 = ( pInvG ‘ 𝐺 )
mirval.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
miduniq2.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
miduniq2.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
miduniq2.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
miduniq2.e ⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝐴 ) ‘ ( ( 𝑆 ‘ 𝐵 ) ‘ 𝑋 ) ) = ( ( 𝑆 ‘ 𝐵 ) ‘ ( ( 𝑆 ‘ 𝐴 ) ‘ 𝑋 ) ) )
Assertion miduniq2 ( 𝜑 → 𝐴 = 𝐵 )

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 miduniq2.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
8 miduniq2.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
9 miduniq2.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
10 miduniq2.e ⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝐴 ) ‘ ( ( 𝑆 ‘ 𝐵 ) ‘ 𝑋 ) ) = ( ( 𝑆 ‘ 𝐵 ) ‘ ( ( 𝑆 ‘ 𝐴 ) ‘ 𝑋 ) ) )
11 eqid ⊢ ( 𝑆 ‘ 𝐵 ) = ( 𝑆 ‘ 𝐵 )
12 1 2 3 4 5 6 8 11 mirf ⊢ ( 𝜑 → ( 𝑆 ‘ 𝐵 ) : 𝑃 ⟶ 𝑃 )
13 12 7 ffvelrnd ⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝐵 ) ‘ 𝐴 ) ∈ 𝑃 )
14 eqid ⊢ ( ( 𝑆 ‘ 𝐵 ) ‘ 𝐴 ) = ( ( 𝑆 ‘ 𝐵 ) ‘ 𝐴 )
15 eqid ⊢ ( ( 𝑆 ‘ 𝐵 ) ‘ ( ( 𝑆 ‘ 𝐵 ) ‘ 𝑋 ) ) = ( ( 𝑆 ‘ 𝐵 ) ‘ ( ( 𝑆 ‘ 𝐵 ) ‘ 𝑋 ) )
16 eqid ⊢ ( ( 𝑆 ‘ 𝐵 ) ‘ ( ( 𝑆 ‘ 𝐵 ) ‘ ( ( 𝑆 ‘ 𝐴 ) ‘ 𝑋 ) ) ) = ( ( 𝑆 ‘ 𝐵 ) ‘ ( ( 𝑆 ‘ 𝐵 ) ‘ ( ( 𝑆 ‘ 𝐴 ) ‘ 𝑋 ) ) )
17 12 9 ffvelrnd ⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝐵 ) ‘ 𝑋 ) ∈ 𝑃 )
18 eqid ⊢ ( 𝑆 ‘ 𝐴 ) = ( 𝑆 ‘ 𝐴 )
19 1 2 3 4 5 6 7 18 9 mircl ⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝐴 ) ‘ 𝑋 ) ∈ 𝑃 )
20 12 19 ffvelrnd ⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝐵 ) ‘ ( ( 𝑆 ‘ 𝐴 ) ‘ 𝑋 ) ) ∈ 𝑃 )
21 1 2 3 4 5 6 11 14 15 16 8 7 17 20 10 mirauto ⊢ ( 𝜑 → ( ( 𝑆 ‘ ( ( 𝑆 ‘ 𝐵 ) ‘ 𝐴 ) ) ‘ ( ( 𝑆 ‘ 𝐵 ) ‘ ( ( 𝑆 ‘ 𝐵 ) ‘ 𝑋 ) ) ) = ( ( 𝑆 ‘ 𝐵 ) ‘ ( ( 𝑆 ‘ 𝐵 ) ‘ ( ( 𝑆 ‘ 𝐴 ) ‘ 𝑋 ) ) ) )
22 1 2 3 4 5 6 8 11 9 mirmir ⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝐵 ) ‘ ( ( 𝑆 ‘ 𝐵 ) ‘ 𝑋 ) ) = 𝑋 )
23 22 fveq2d ⊢ ( 𝜑 → ( ( 𝑆 ‘ ( ( 𝑆 ‘ 𝐵 ) ‘ 𝐴 ) ) ‘ ( ( 𝑆 ‘ 𝐵 ) ‘ ( ( 𝑆 ‘ 𝐵 ) ‘ 𝑋 ) ) ) = ( ( 𝑆 ‘ ( ( 𝑆 ‘ 𝐵 ) ‘ 𝐴 ) ) ‘ 𝑋 ) )
24 1 2 3 4 5 6 8 11 19 mirmir ⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝐵 ) ‘ ( ( 𝑆 ‘ 𝐵 ) ‘ ( ( 𝑆 ‘ 𝐴 ) ‘ 𝑋 ) ) ) = ( ( 𝑆 ‘ 𝐴 ) ‘ 𝑋 ) )
25 21 23 24 3eqtr3d ⊢ ( 𝜑 → ( ( 𝑆 ‘ ( ( 𝑆 ‘ 𝐵 ) ‘ 𝐴 ) ) ‘ 𝑋 ) = ( ( 𝑆 ‘ 𝐴 ) ‘ 𝑋 ) )
26 1 2 3 4 5 6 13 7 9 25 miduniq1 ⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝐵 ) ‘ 𝐴 ) = 𝐴 )
27 1 2 3 4 5 6 8 11 7 mirinv ⊢ ( 𝜑 → ( ( ( 𝑆 ‘ 𝐵 ) ‘ 𝐴 ) = 𝐴 ↔ 𝐵 = 𝐴 ) )
28 26 27 mpbid ⊢ ( 𝜑 → 𝐵 = 𝐴 )
29 28 eqcomd ⊢ ( 𝜑 → 𝐴 = 𝐵 )