Theorem mireq

Description: Equality deduction for point inversion. Theorem 7.9 of Schwabhauser p. 50. (Contributed by Thierry Arnoux, 30-May-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}}$$
	mirval.a	$$⊢\phi \to A\in P$$
	mirfv.m	$$⊢M=S\left(A\right)$$
	mirmir.b	$$⊢\phi \to B\in P$$
	mireq.c	$$⊢\phi \to C\in P$$
	mireq.d	$$⊢\phi \to M\left(B\right)=M\left(C\right)$$
Assertion	mireq	$$⊢\phi \to B=C$$

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		mirval.a	$$⊢\phi \to A\in P$$
8		mirfv.m	$$⊢M=S\left(A\right)$$
9		mirmir.b	$$⊢\phi \to B\in P$$
10		mireq.c	$$⊢\phi \to C\in P$$
11		mireq.d	$$⊢\phi \to M\left(B\right)=M\left(C\right)$$
12	1 2 3 4 5 6 7 8 10	mircl	$$⊢\phi \to M\left(C\right)\in P$$
13	1 2 3 4 5 6 7 8 9	mirfv	$$⊢\phi \to M\left(B\right)=\left(\iota z\in P|\left(A\underset{\dot{}}{-}z=A\underset{\dot{}}{-}B\wedge A\in \left(zIB\right)\right)\right)$$
14	13 11	eqtr3d	$$⊢\phi \to \left(\iota z\in P|\left(A\underset{\dot{}}{-}z=A\underset{\dot{}}{-}B\wedge A\in \left(zIB\right)\right)\right)=M\left(C\right)$$
15	1 2 3 6 9 7	mirreu3	$$⊢\phi \to \exists !z\in P\left(A\underset{\dot{}}{-}z=A\underset{\dot{}}{-}B\wedge A\in \left(zIB\right)\right)$$
16		oveq2	$$⊢z=M\left(C\right)\to A\underset{\dot{}}{-}z=A\underset{\dot{}}{-}M\left(C\right)$$
17	16	eqeq1d	$$⊢z=M\left(C\right)\to \left(A\underset{\dot{}}{-}z=A\underset{\dot{}}{-}B\leftrightarrow A\underset{\dot{}}{-}M\left(C\right)=A\underset{\dot{}}{-}B\right)$$
18		oveq1	$$⊢z=M\left(C\right)\to zIB=M\left(C\right)IB$$
19	18	eleq2d	$$⊢z=M\left(C\right)\to \left(A\in \left(zIB\right)\leftrightarrow A\in \left(M\left(C\right)IB\right)\right)$$
20	17 19	anbi12d	$$⊢z=M\left(C\right)\to \left(\left(A\underset{\dot{}}{-}z=A\underset{\dot{}}{-}B\wedge A\in \left(zIB\right)\right)\leftrightarrow \left(A\underset{\dot{}}{-}M\left(C\right)=A\underset{\dot{}}{-}B\wedge A\in \left(M\left(C\right)IB\right)\right)\right)$$
21	20	riota2	$$⊢\left(M\left(C\right)\in P\wedge \exists !z\in P\left(A\underset{\dot{}}{-}z=A\underset{\dot{}}{-}B\wedge A\in \left(zIB\right)\right)\right)\to \left(\left(A\underset{\dot{}}{-}M\left(C\right)=A\underset{\dot{}}{-}B\wedge A\in \left(M\left(C\right)IB\right)\right)\leftrightarrow \left(\iota z\in P|\left(A\underset{\dot{}}{-}z=A\underset{\dot{}}{-}B\wedge A\in \left(zIB\right)\right)\right)=M\left(C\right)\right)$$
22	12 15 21	syl2anc	$$⊢\phi \to \left(\left(A\underset{\dot{}}{-}M\left(C\right)=A\underset{\dot{}}{-}B\wedge A\in \left(M\left(C\right)IB\right)\right)\leftrightarrow \left(\iota z\in P|\left(A\underset{\dot{}}{-}z=A\underset{\dot{}}{-}B\wedge A\in \left(zIB\right)\right)\right)=M\left(C\right)\right)$$
23	14 22	mpbird	$$⊢\phi \to \left(A\underset{\dot{}}{-}M\left(C\right)=A\underset{\dot{}}{-}B\wedge A\in \left(M\left(C\right)IB\right)\right)$$
24	23	simpld	$$⊢\phi \to A\underset{\dot{}}{-}M\left(C\right)=A\underset{\dot{}}{-}B$$
25	24	eqcomd	$$⊢\phi \to A\underset{\dot{}}{-}B=A\underset{\dot{}}{-}M\left(C\right)$$
26	23	simprd	$$⊢\phi \to A\in \left(M\left(C\right)IB\right)$$
27	1 2 3 6 12 7 9 26	tgbtwncom	$$⊢\phi \to A\in \left(BIM\left(C\right)\right)$$
28	1 2 3 4 5 6 7 8 12 9 25 27	ismir	$$⊢\phi \to B=M\left(M\left(C\right)\right)$$
29	1 2 3 4 5 6 7 8 10	mirmir	$$⊢\phi \to M\left(M\left(C\right)\right)=C$$
30	28 29	eqtrd	$$⊢\phi \to B=C$$