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={\mathrm{Base}}_G$$
	mirval.d	$$⊢\underset{\dot{}}{-}=\mathrm{dist}\left(G\right)$$
	mirval.i	$$⊢I=\mathrm{Itv}\left(G\right)$$
	mirval.l	$$⊢L={Line}_{𝒢}\left(G\right)$$
	mirval.s	$$⊢S={pInv}_{𝒢}\left(G\right)$$
	mirval.g	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}$$
	miduniq2.a	$$⊢\phi \to A\in P$$
	miduniq2.b	$$⊢\phi \to B\in P$$
	miduniq2.x	$$⊢\phi \to X\in P$$
	miduniq2.e	$$⊢\phi \to S\left(A\right)\left(S\left(B\right)\left(X\right)\right)=S\left(B\right)\left(S\left(A\right)\left(X\right)\right)$$
Assertion	miduniq2	$$⊢\phi \to A=B$$

Proof

Step	Hyp	Ref	Expression
1		mirval.p	$$⊢P={\mathrm{Base}}_G$$
2		mirval.d	$$⊢\underset{\dot{}}{-}=\mathrm{dist}\left(G\right)$$
3		mirval.i	$$⊢I=\mathrm{Itv}\left(G\right)$$
4		mirval.l	$$⊢L={Line}_{𝒢}\left(G\right)$$
5		mirval.s	$$⊢S={pInv}_{𝒢}\left(G\right)$$
6		mirval.g	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}$$
7		miduniq2.a	$$⊢\phi \to A\in P$$
8		miduniq2.b	$$⊢\phi \to B\in P$$
9		miduniq2.x	$$⊢\phi \to X\in P$$
10		miduniq2.e	$$⊢\phi \to S\left(A\right)\left(S\left(B\right)\left(X\right)\right)=S\left(B\right)\left(S\left(A\right)\left(X\right)\right)$$
11		eqid	$$⊢S\left(B\right)=S\left(B\right)$$
12	1 2 3 4 5 6 8 11	mirf	$$⊢\phi \to S\left(B\right):P⟶P$$
13	12 7	ffvelcdmd	$$⊢\phi \to S\left(B\right)\left(A\right)\in P$$
14		eqid	$$⊢S\left(B\right)\left(A\right)=S\left(B\right)\left(A\right)$$
15		eqid	$$⊢S\left(B\right)\left(S\left(B\right)\left(X\right)\right)=S\left(B\right)\left(S\left(B\right)\left(X\right)\right)$$
16		eqid	$$⊢S\left(B\right)\left(S\left(B\right)\left(S\left(A\right)\left(X\right)\right)\right)=S\left(B\right)\left(S\left(B\right)\left(S\left(A\right)\left(X\right)\right)\right)$$
17	12 9	ffvelcdmd	$$⊢\phi \to S\left(B\right)\left(X\right)\in P$$
18		eqid	$$⊢S\left(A\right)=S\left(A\right)$$
19	1 2 3 4 5 6 7 18 9	mircl	$$⊢\phi \to S\left(A\right)\left(X\right)\in P$$
20	12 19	ffvelcdmd	$$⊢\phi \to S\left(B\right)\left(S\left(A\right)\left(X\right)\right)\in P$$
21	1 2 3 4 5 6 11 14 15 16 8 7 17 20 10	mirauto	$$⊢\phi \to S\left(S\left(B\right)\left(A\right)\right)\left(S\left(B\right)\left(S\left(B\right)\left(X\right)\right)\right)=S\left(B\right)\left(S\left(B\right)\left(S\left(A\right)\left(X\right)\right)\right)$$
22	1 2 3 4 5 6 8 11 9	mirmir	$$⊢\phi \to S\left(B\right)\left(S\left(B\right)\left(X\right)\right)=X$$
23	22	fveq2d	$$⊢\phi \to S\left(S\left(B\right)\left(A\right)\right)\left(S\left(B\right)\left(S\left(B\right)\left(X\right)\right)\right)=S\left(S\left(B\right)\left(A\right)\right)\left(X\right)$$
24	1 2 3 4 5 6 8 11 19	mirmir	$$⊢\phi \to S\left(B\right)\left(S\left(B\right)\left(S\left(A\right)\left(X\right)\right)\right)=S\left(A\right)\left(X\right)$$
25	21 23 24	3eqtr3d	$$⊢\phi \to S\left(S\left(B\right)\left(A\right)\right)\left(X\right)=S\left(A\right)\left(X\right)$$
26	1 2 3 4 5 6 13 7 9 25	miduniq1	$$⊢\phi \to S\left(B\right)\left(A\right)=A$$
27	1 2 3 4 5 6 8 11 7	mirinv	$$⊢\phi \to \left(S\left(B\right)\left(A\right)=A\leftrightarrow B=A\right)$$
28	26 27	mpbid	$$⊢\phi \to B=A$$
29	28	eqcomd	$$⊢\phi \to A=B$$