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
|- P = ( Base ` G )
mirval.d
|- .- = ( dist ` G )
mirval.i
|- I = ( Itv ` G )
mirval.l
|- L = ( LineG ` G )
mirval.s
|- S = ( pInvG ` G )
mirval.g
|- ( ph -> G e. TarskiG )
miduniq2.a
|- ( ph -> A e. P )
miduniq2.b
|- ( ph -> B e. P )
miduniq2.x
|- ( ph -> X e. P )
miduniq2.e
|- ( ph -> ( ( S ` A ) ` ( ( S ` B ) ` X ) ) = ( ( S ` B ) ` ( ( S ` A ) ` X ) ) )
Assertion miduniq2
|- ( ph -> A = B )

Proof

Step Hyp Ref Expression
1 mirval.p
 |-  P = ( Base ` G )
2 mirval.d
 |-  .- = ( dist ` G )
3 mirval.i
 |-  I = ( Itv ` G )
4 mirval.l
 |-  L = ( LineG ` G )
5 mirval.s
 |-  S = ( pInvG ` G )
6 mirval.g
 |-  ( ph -> G e. TarskiG )
7 miduniq2.a
 |-  ( ph -> A e. P )
8 miduniq2.b
 |-  ( ph -> B e. P )
9 miduniq2.x
 |-  ( ph -> X e. P )
10 miduniq2.e
 |-  ( ph -> ( ( S ` A ) ` ( ( S ` B ) ` X ) ) = ( ( S ` B ) ` ( ( S ` A ) ` X ) ) )
11 eqid
 |-  ( S ` B ) = ( S ` B )
12 1 2 3 4 5 6 8 11 mirf
 |-  ( ph -> ( S ` B ) : P --> P )
13 12 7 ffvelrnd
 |-  ( ph -> ( ( S ` B ) ` A ) e. P )
14 eqid
 |-  ( ( S ` B ) ` A ) = ( ( S ` B ) ` A )
15 eqid
 |-  ( ( S ` B ) ` ( ( S ` B ) ` X ) ) = ( ( S ` B ) ` ( ( S ` B ) ` X ) )
16 eqid
 |-  ( ( S ` B ) ` ( ( S ` B ) ` ( ( S ` A ) ` X ) ) ) = ( ( S ` B ) ` ( ( S ` B ) ` ( ( S ` A ) ` X ) ) )
17 12 9 ffvelrnd
 |-  ( ph -> ( ( S ` B ) ` X ) e. P )
18 eqid
 |-  ( S ` A ) = ( S ` A )
19 1 2 3 4 5 6 7 18 9 mircl
 |-  ( ph -> ( ( S ` A ) ` X ) e. P )
20 12 19 ffvelrnd
 |-  ( ph -> ( ( S ` B ) ` ( ( S ` A ) ` X ) ) e. P )
21 1 2 3 4 5 6 11 14 15 16 8 7 17 20 10 mirauto
 |-  ( ph -> ( ( S ` ( ( S ` B ) ` A ) ) ` ( ( S ` B ) ` ( ( S ` B ) ` X ) ) ) = ( ( S ` B ) ` ( ( S ` B ) ` ( ( S ` A ) ` X ) ) ) )
22 1 2 3 4 5 6 8 11 9 mirmir
 |-  ( ph -> ( ( S ` B ) ` ( ( S ` B ) ` X ) ) = X )
23 22 fveq2d
 |-  ( ph -> ( ( S ` ( ( S ` B ) ` A ) ) ` ( ( S ` B ) ` ( ( S ` B ) ` X ) ) ) = ( ( S ` ( ( S ` B ) ` A ) ) ` X ) )
24 1 2 3 4 5 6 8 11 19 mirmir
 |-  ( ph -> ( ( S ` B ) ` ( ( S ` B ) ` ( ( S ` A ) ` X ) ) ) = ( ( S ` A ) ` X ) )
25 21 23 24 3eqtr3d
 |-  ( ph -> ( ( S ` ( ( S ` B ) ` A ) ) ` X ) = ( ( S ` A ) ` X ) )
26 1 2 3 4 5 6 13 7 9 25 miduniq1
 |-  ( ph -> ( ( S ` B ) ` A ) = A )
27 1 2 3 4 5 6 8 11 7 mirinv
 |-  ( ph -> ( ( ( S ` B ) ` A ) = A <-> B = A ) )
28 26 27 mpbid
 |-  ( ph -> B = A )
29 28 eqcomd
 |-  ( ph -> A = B )