Theorem inagne1

Description: Deduce inequality from the in-angle relation. (Contributed by Thierry Arnoux, 29-Oct-2021)

	Ref	Expression
Hypotheses	isinag.p	$$⊢P={\mathrm{Base}}_G$$
	isinag.i	$$⊢I=\mathrm{Itv}\left(G\right)$$
	isinag.k	$$⊢K={hl}_{𝒢}\left(G\right)$$
	isinag.x	$$⊢\phi \to X\in P$$
	isinag.a	$$⊢\phi \to A\in P$$
	isinag.b	$$⊢\phi \to B\in P$$
	isinag.c	$$⊢\phi \to C\in P$$
	inagflat.g	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}$$
	inagswap.1	$$⊢\phi \to X{\in }_{𝒢}^{\angle }\left(G\right)⟨“ABC”⟩$$
Assertion	inagne1	$$⊢\phi \to A\ne B$$

Proof

Step	Hyp	Ref	Expression
1		isinag.p	$$⊢P={\mathrm{Base}}_G$$
2		isinag.i	$$⊢I=\mathrm{Itv}\left(G\right)$$
3		isinag.k	$$⊢K={hl}_{𝒢}\left(G\right)$$
4		isinag.x	$$⊢\phi \to X\in P$$
5		isinag.a	$$⊢\phi \to A\in P$$
6		isinag.b	$$⊢\phi \to B\in P$$
7		isinag.c	$$⊢\phi \to C\in P$$
8		inagflat.g	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}$$
9		inagswap.1	$$⊢\phi \to X{\in }_{𝒢}^{\angle }\left(G\right)⟨“ABC”⟩$$
10	1 2 3 4 5 6 7 8	isinag	$$⊢\phi \to \left(X{\in }_{𝒢}^{\angle }\left(G\right)⟨“ABC”⟩\leftrightarrow \left(\left(A\ne B\wedge C\ne B\wedge X\ne B\right)\wedge \exists x\in P\left(x\in \left(AIC\right)\wedge \left(x=B\vee xK\left(B\right)X\right)\right)\right)\right)$$
11	9 10	mpbid	$$⊢\phi \to \left(\left(A\ne B\wedge C\ne B\wedge X\ne B\right)\wedge \exists x\in P\left(x\in \left(AIC\right)\wedge \left(x=B\vee xK\left(B\right)X\right)\right)\right)$$
12	11	simpld	$$⊢\phi \to \left(A\ne B\wedge C\ne B\wedge X\ne B\right)$$
13	12	simp1d	$$⊢\phi \to A\ne B$$