Theorem mirne

Description: Mirror of non-center point cannot be the center point. (Contributed by Thierry Arnoux, 27-Sep-2020)

	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)$$
	mirinv.b	$$⊢\phi \to B\in P$$
	mirne.1	$$⊢\phi \to B\ne A$$
Assertion	mirne	$$⊢\phi \to M\left(B\right)\ne A$$

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		mirinv.b	$$⊢\phi \to B\in P$$
10		mirne.1	$$⊢\phi \to B\ne A$$
11		simpr	$$⊢\left(\phi \wedge M\left(B\right)=A\right)\to M\left(B\right)=A$$
12	11	fveq2d	$$⊢\left(\phi \wedge M\left(B\right)=A\right)\to M\left(M\left(B\right)\right)=M\left(A\right)$$
13	1 2 3 4 5 6 7 8 9	mirmir	$$⊢\phi \to M\left(M\left(B\right)\right)=B$$
14	13	adantr	$$⊢\left(\phi \wedge M\left(B\right)=A\right)\to M\left(M\left(B\right)\right)=B$$
15		eqid	$$⊢A=A$$
16	1 2 3 4 5 6 7 8 7	mirinv	$$⊢\phi \to \left(M\left(A\right)=A\leftrightarrow A=A\right)$$
17	15 16	mpbiri	$$⊢\phi \to M\left(A\right)=A$$
18	17	adantr	$$⊢\left(\phi \wedge M\left(B\right)=A\right)\to M\left(A\right)=A$$
19	12 14 18	3eqtr3d	$$⊢\left(\phi \wedge M\left(B\right)=A\right)\to B=A$$
20	10	adantr	$$⊢\left(\phi \wedge M\left(B\right)=A\right)\to B\ne A$$
21	20	neneqd	$$⊢\left(\phi \wedge M\left(B\right)=A\right)\to \neg B=A$$
22	19 21	pm2.65da	$$⊢\phi \to \neg M\left(B\right)=A$$
23	22	neqned	$$⊢\phi \to M\left(B\right)\ne A$$