Theorem miduniq

Description: Uniqueness of the middle point, expressed with point inversion. Theorem 7.17 of Schwabhauser p. 51. (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}}$$
	miduniq.a	$$⊢\phi \to A\in P$$
	miduniq.b	$$⊢\phi \to B\in P$$
	miduniq.x	$$⊢\phi \to X\in P$$
	miduniq.y	$$⊢\phi \to Y\in P$$
	miduniq.e	$$⊢\phi \to S\left(A\right)\left(X\right)=Y$$
	miduniq.f	$$⊢\phi \to S\left(B\right)\left(X\right)=Y$$
Assertion	miduniq	$$⊢\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		miduniq.a	$$⊢\phi \to A\in P$$
8		miduniq.b	$$⊢\phi \to B\in P$$
9		miduniq.x	$$⊢\phi \to X\in P$$
10		miduniq.y	$$⊢\phi \to Y\in P$$
11		miduniq.e	$$⊢\phi \to S\left(A\right)\left(X\right)=Y$$
12		miduniq.f	$$⊢\phi \to S\left(B\right)\left(X\right)=Y$$
13		eqid	$$⊢{\sim }_{𝒢}\left(G\right)={\sim }_{𝒢}\left(G\right)$$
14		eqid	$$⊢S\left(A\right)=S\left(A\right)$$
15	1 2 3 4 5 6 7 14 8	mircl	$$⊢\phi \to S\left(A\right)\left(B\right)\in P$$
16		eqid	$$⊢S\left(B\right)=S\left(B\right)$$
17	1 2 3 4 5 6 8 16 9	mirbtwn	$$⊢\phi \to B\in \left(S\left(B\right)\left(X\right)IX\right)$$
18	12	oveq1d	$$⊢\phi \to S\left(B\right)\left(X\right)IX=YIX$$
19	17 18	eleqtrd	$$⊢\phi \to B\in \left(YIX\right)$$
20	1 2 3 6 10 8 9 19	tgbtwncom	$$⊢\phi \to B\in \left(XIY\right)$$
21	1 2 3 4 5 6 7 14 10 8	miriso	$$⊢\phi \to S\left(A\right)\left(Y\right)\underset{\dot{}}{-}S\left(A\right)\left(B\right)=Y\underset{\dot{}}{-}B$$
22	1 2 3 4 5 6 7 14 9 11	mircom	$$⊢\phi \to S\left(A\right)\left(Y\right)=X$$
23	22	oveq1d	$$⊢\phi \to S\left(A\right)\left(Y\right)\underset{\dot{}}{-}S\left(A\right)\left(B\right)=X\underset{\dot{}}{-}S\left(A\right)\left(B\right)$$
24	1 2 3 4 5 6 8 16 9	mircgr	$$⊢\phi \to B\underset{\dot{}}{-}S\left(B\right)\left(X\right)=B\underset{\dot{}}{-}X$$
25	12	oveq2d	$$⊢\phi \to B\underset{\dot{}}{-}S\left(B\right)\left(X\right)=B\underset{\dot{}}{-}Y$$
26	24 25	eqtr3d	$$⊢\phi \to B\underset{\dot{}}{-}X=B\underset{\dot{}}{-}Y$$
27	26	eqcomd	$$⊢\phi \to B\underset{\dot{}}{-}Y=B\underset{\dot{}}{-}X$$
28	1 2 3 6 8 10 8 9 27	tgcgrcomlr	$$⊢\phi \to Y\underset{\dot{}}{-}B=X\underset{\dot{}}{-}B$$
29	21 23 28	3eqtr3rd	$$⊢\phi \to X\underset{\dot{}}{-}B=X\underset{\dot{}}{-}S\left(A\right)\left(B\right)$$
30	1 2 3 4 5 6 7 14 9 8	miriso	$$⊢\phi \to S\left(A\right)\left(X\right)\underset{\dot{}}{-}S\left(A\right)\left(B\right)=X\underset{\dot{}}{-}B$$
31	11	oveq1d	$$⊢\phi \to S\left(A\right)\left(X\right)\underset{\dot{}}{-}S\left(A\right)\left(B\right)=Y\underset{\dot{}}{-}S\left(A\right)\left(B\right)$$
32	1 2 3 6 8 9 8 10 26	tgcgrcomlr	$$⊢\phi \to X\underset{\dot{}}{-}B=Y\underset{\dot{}}{-}B$$
33	30 31 32	3eqtr3rd	$$⊢\phi \to Y\underset{\dot{}}{-}B=Y\underset{\dot{}}{-}S\left(A\right)\left(B\right)$$
34	1 4 3 6 9 10 8 13 15 7 2 20 29 33	tgidinside	$$⊢\phi \to B=S\left(A\right)\left(B\right)$$
35	34	eqcomd	$$⊢\phi \to S\left(A\right)\left(B\right)=B$$
36	1 2 3 4 5 6 7 14 8	mirinv	$$⊢\phi \to \left(S\left(A\right)\left(B\right)=B\leftrightarrow A=B\right)$$
37	35 36	mpbid	$$⊢\phi \to A=B$$