Theorem colperpexlem2

Description: Lemma for colperpex . Second part of lemma 8.20 of Schwabhauser p. 62. (Contributed by Thierry Arnoux, 10-Nov-2019)

	Ref	Expression
Hypotheses	colperpex.p	$$⊢P={\mathrm{Base}}_G$$
	colperpex.d	$$⊢\underset{\dot{}}{-}=\mathrm{dist}\left(G\right)$$
	colperpex.i	$$⊢I=\mathrm{Itv}\left(G\right)$$
	colperpex.l	$$⊢L={Line}_{𝒢}\left(G\right)$$
	colperpex.g	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}$$
	colperpexlem.s	$$⊢S={pInv}_{𝒢}\left(G\right)$$
	colperpexlem.m	$$⊢M=S\left(A\right)$$
	colperpexlem.n	$$⊢N=S\left(B\right)$$
	colperpexlem.k	$$⊢K=S\left(Q\right)$$
	colperpexlem.a	$$⊢\phi \to A\in P$$
	colperpexlem.b	$$⊢\phi \to B\in P$$
	colperpexlem.c	$$⊢\phi \to C\in P$$
	colperpexlem.q	$$⊢\phi \to Q\in P$$
	colperpexlem.1	$$⊢\phi \to ⟨“ABC”⟩\in {∟}_{𝒢}\left(G\right)$$
	colperpexlem.2	$$⊢\phi \to K\left(M\left(C\right)\right)=N\left(C\right)$$
	colperpexlem2.e	$$⊢\phi \to B\ne C$$
Assertion	colperpexlem2	$$⊢\phi \to A\ne Q$$

Proof

Step	Hyp	Ref	Expression
1		colperpex.p	$$⊢P={\mathrm{Base}}_G$$
2		colperpex.d	$$⊢\underset{\dot{}}{-}=\mathrm{dist}\left(G\right)$$
3		colperpex.i	$$⊢I=\mathrm{Itv}\left(G\right)$$
4		colperpex.l	$$⊢L={Line}_{𝒢}\left(G\right)$$
5		colperpex.g	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}$$
6		colperpexlem.s	$$⊢S={pInv}_{𝒢}\left(G\right)$$
7		colperpexlem.m	$$⊢M=S\left(A\right)$$
8		colperpexlem.n	$$⊢N=S\left(B\right)$$
9		colperpexlem.k	$$⊢K=S\left(Q\right)$$
10		colperpexlem.a	$$⊢\phi \to A\in P$$
11		colperpexlem.b	$$⊢\phi \to B\in P$$
12		colperpexlem.c	$$⊢\phi \to C\in P$$
13		colperpexlem.q	$$⊢\phi \to Q\in P$$
14		colperpexlem.1	$$⊢\phi \to ⟨“ABC”⟩\in {∟}_{𝒢}\left(G\right)$$
15		colperpexlem.2	$$⊢\phi \to K\left(M\left(C\right)\right)=N\left(C\right)$$
16		colperpexlem2.e	$$⊢\phi \to B\ne C$$
17		simpr	$$⊢\left(\phi \wedge A=Q\right)\to A=Q$$
18	17	fveq2d	$$⊢\left(\phi \wedge A=Q\right)\to S\left(A\right)=S\left(Q\right)$$
19	18 7 9	3eqtr4g	$$⊢\left(\phi \wedge A=Q\right)\to M=K$$
20	19	fveq1d	$$⊢\left(\phi \wedge A=Q\right)\to M\left(M\left(C\right)\right)=K\left(M\left(C\right)\right)$$
21	1 2 3 4 6 5 10 7 12	mirmir	$$⊢\phi \to M\left(M\left(C\right)\right)=C$$
22	21	adantr	$$⊢\left(\phi \wedge A=Q\right)\to M\left(M\left(C\right)\right)=C$$
23	15	adantr	$$⊢\left(\phi \wedge A=Q\right)\to K\left(M\left(C\right)\right)=N\left(C\right)$$
24	20 22 23	3eqtr3rd	$$⊢\left(\phi \wedge A=Q\right)\to N\left(C\right)=C$$
25	1 2 3 4 6 5 11 8 12	mirinv	$$⊢\phi \to \left(N\left(C\right)=C\leftrightarrow B=C\right)$$
26	25	adantr	$$⊢\left(\phi \wedge A=Q\right)\to \left(N\left(C\right)=C\leftrightarrow B=C\right)$$
27	24 26	mpbid	$$⊢\left(\phi \wedge A=Q\right)\to B=C$$
28	27	ex	$$⊢\phi \to \left(A=Q\to B=C\right)$$
29	28	necon3ad	$$⊢\phi \to \left(B\ne C\to \neg A=Q\right)$$
30	16 29	mpd	$$⊢\phi \to \neg A=Q$$
31	30	neqned	$$⊢\phi \to A\ne Q$$