cgrane1

Description: Angles imply inequality. (Contributed by Thierry Arnoux, 1-Aug-2020)

	Ref	Expression
Hypotheses	iscgra.p	$⊢ P = {Base}_{G}$
	iscgra.i	$⊢ I = Itv (G)$
	iscgra.k	$⊢ K = {hl}_{𝒢} (G)$
	iscgra.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	iscgra.a	$⊢ φ \to A \in P$
	iscgra.b	$⊢ φ \to B \in P$
	iscgra.c	$⊢ φ \to C \in P$
	iscgra.d	$⊢ φ \to D \in P$
	iscgra.e	$⊢ φ \to E \in P$
	iscgra.f	$⊢ φ \to F \in P$
	cgrahl1.2	$⊢ φ \to ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩$
Assertion	cgrane1	$⊢ φ \to A \neq B$

Proof

Step	Hyp	Ref	Expression
1		iscgra.p	$⊢ P = {Base}_{G}$
2		iscgra.i	$⊢ I = Itv (G)$
3		iscgra.k	$⊢ K = {hl}_{𝒢} (G)$
4		iscgra.g	$⊢ φ \to G \in 𝒢_{Tarski}$
5		iscgra.a	$⊢ φ \to A \in P$
6		iscgra.b	$⊢ φ \to B \in P$
7		iscgra.c	$⊢ φ \to C \in P$
8		iscgra.d	$⊢ φ \to D \in P$
9		iscgra.e	$⊢ φ \to E \in P$
10		iscgra.f	$⊢ φ \to F \in P$
11		cgrahl1.2	$⊢ φ \to ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩$
12		eqid	$⊢ dist (G) = dist (G)$
13	4	ad3antrrr	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x K (E) D \land y K (E) F)) \to G \in 𝒢_{Tarski}$
14		simpllr	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x K (E) D \land y K (E) F)) \to x \in P$
15	9	ad3antrrr	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x K (E) D \land y K (E) F)) \to E \in P$
16	5	ad3antrrr	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x K (E) D \land y K (E) F)) \to A \in P$
17	6	ad3antrrr	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x K (E) D \land y K (E) F)) \to B \in P$
18		eqid	$⊢ \sim_{𝒢} (G) = \sim_{𝒢} (G)$
19	7	ad3antrrr	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x K (E) D \land y K (E) F)) \to C \in P$
20		simplr	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x K (E) D \land y K (E) F)) \to y \in P$
21		simpr1	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x K (E) D \land y K (E) F)) \to ⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩$
22	1 12 2 18 13 16 17 19 14 15 20 21	cgr3simp1	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x K (E) D \land y K (E) F)) \to A dist (G) B = x dist (G) E$
23	22	eqcomd	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x K (E) D \land y K (E) F)) \to x dist (G) E = A dist (G) B$
24	8	ad3antrrr	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x K (E) D \land y K (E) F)) \to D \in P$
25		simpr2	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x K (E) D \land y K (E) F)) \to x K (E) D$
26	1 2 3 14 24 15 13 25	hlne1	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x K (E) D \land y K (E) F)) \to x \neq E$
27	1 12 2 13 14 15 16 17 23 26	tgcgrneq	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x K (E) D \land y K (E) F)) \to A \neq B$
28	1 2 3 4 5 6 7 8 9 10	iscgra	$⊢ φ \to (⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩ \leftrightarrow \exists x \in P \exists y \in P (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x K (E) D \land y K (E) F))$
29	11 28	mpbid	$⊢ φ \to \exists x \in P \exists y \in P (⟨“ A B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x K (E) D \land y K (E) F)$
30	27 29	r19.29vva	$⊢ φ \to A \neq B$

Metamath Proof Explorer

Theorem cgrane1

Proof