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	ffvelcdmd	\|- ( 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	ffvelcdmd	\|- ( 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	ffvelcdmd	\|- ( 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 )

Metamath Proof Explorer

Theorem miduniq2

Proof