leagne3

Description: Deduce inequality from the less-than angle relation. (Contributed by Thierry Arnoux, 25-Feb-2023)

	Ref	Expression
Hypotheses	isleag.p	$⊢ P = {Base}_{G}$
	isleag.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	isleag.a	$⊢ φ \to A \in P$
	isleag.b	$⊢ φ \to B \in P$
	isleag.c	$⊢ φ \to C \in P$
	isleag.d	$⊢ φ \to D \in P$
	isleag.e	$⊢ φ \to E \in P$
	isleag.f	$⊢ φ \to F \in P$
	leagne.1	$⊢ φ \to ⟨“ A B C ”⟩ \leq_{𝒢}^{∠} (G) ⟨“ D E F ”⟩$
Assertion	leagne3	$⊢ φ \to D \neq E$

Proof

Step	Hyp	Ref	Expression
1		isleag.p	$⊢ P = {Base}_{G}$
2		isleag.g	$⊢ φ \to G \in 𝒢_{Tarski}$
3		isleag.a	$⊢ φ \to A \in P$
4		isleag.b	$⊢ φ \to B \in P$
5		isleag.c	$⊢ φ \to C \in P$
6		isleag.d	$⊢ φ \to D \in P$
7		isleag.e	$⊢ φ \to E \in P$
8		isleag.f	$⊢ φ \to F \in P$
9		leagne.1	$⊢ φ \to ⟨“ A B C ”⟩ \leq_{𝒢}^{∠} (G) ⟨“ D E F ”⟩$
10		eqid	$⊢ Itv (G) = Itv (G)$
11		eqid	$⊢ {hl}_{𝒢} (G) = {hl}_{𝒢} (G)$
12	2	ad2antrr	$⊢ ((φ \land x \in P) \land (x \in_{𝒢}^{∠} (G) ⟨“ D E F ”⟩ \land ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E x ”⟩)) \to G \in 𝒢_{Tarski}$
13	3	ad2antrr	$⊢ ((φ \land x \in P) \land (x \in_{𝒢}^{∠} (G) ⟨“ D E F ”⟩ \land ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E x ”⟩)) \to A \in P$
14	4	ad2antrr	$⊢ ((φ \land x \in P) \land (x \in_{𝒢}^{∠} (G) ⟨“ D E F ”⟩ \land ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E x ”⟩)) \to B \in P$
15	5	ad2antrr	$⊢ ((φ \land x \in P) \land (x \in_{𝒢}^{∠} (G) ⟨“ D E F ”⟩ \land ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E x ”⟩)) \to C \in P$
16	6	ad2antrr	$⊢ ((φ \land x \in P) \land (x \in_{𝒢}^{∠} (G) ⟨“ D E F ”⟩ \land ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E x ”⟩)) \to D \in P$
17	7	ad2antrr	$⊢ ((φ \land x \in P) \land (x \in_{𝒢}^{∠} (G) ⟨“ D E F ”⟩ \land ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E x ”⟩)) \to E \in P$
18		simplr	$⊢ ((φ \land x \in P) \land (x \in_{𝒢}^{∠} (G) ⟨“ D E F ”⟩ \land ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E x ”⟩)) \to x \in P$
19		simprr	$⊢ ((φ \land x \in P) \land (x \in_{𝒢}^{∠} (G) ⟨“ D E F ”⟩ \land ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E x ”⟩)) \to ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E x ”⟩$
20	1 10 11 12 13 14 15 16 17 18 19	cgrane3	$⊢ ((φ \land x \in P) \land (x \in_{𝒢}^{∠} (G) ⟨“ D E F ”⟩ \land ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E x ”⟩)) \to E \neq D$
21	20	necomd	$⊢ ((φ \land x \in P) \land (x \in_{𝒢}^{∠} (G) ⟨“ D E F ”⟩ \land ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E x ”⟩)) \to D \neq E$
22	1 2 3 4 5 6 7 8	isleag	$⊢ φ \to (⟨“ A B C ”⟩ \leq_{𝒢}^{∠} (G) ⟨“ D E F ”⟩ \leftrightarrow \exists x \in P (x \in_{𝒢}^{∠} (G) ⟨“ D E F ”⟩ \land ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E x ”⟩))$
23	9 22	mpbid	$⊢ φ \to \exists x \in P (x \in_{𝒢}^{∠} (G) ⟨“ D E F ”⟩ \land ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E x ”⟩)$
24	21 23	r19.29a	$⊢ φ \to D \neq E$

Metamath Proof Explorer

Theorem leagne3

Proof