cgrancol

Description: Angle congruence preserves non-colinearity. (Contributed by Thierry Arnoux, 9-Aug-2020)

	Ref	Expression
Hypotheses	cgracol.p	$⊢ P = {Base}_{G}$
	cgracol.i	$⊢ I = Itv (G)$
	cgracol.m	$⊢ \underset{˙}{-} = dist (G)$
	cgracol.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	cgracol.a	$⊢ φ \to A \in P$
	cgracol.b	$⊢ φ \to B \in P$
	cgracol.c	$⊢ φ \to C \in P$
	cgracol.d	$⊢ φ \to D \in P$
	cgracol.e	$⊢ φ \to E \in P$
	cgracol.f	$⊢ φ \to F \in P$
	cgracol.1	$⊢ φ \to ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩$
	cgrancol.l	$⊢ L = {Line}_{𝒢} (G)$
	cgrancol.2	$⊢ φ \to \neg (C \in (A L B) \lor A = B)$
Assertion	cgrancol	$⊢ φ \to \neg (F \in (D L E) \lor D = E)$

Proof

Step	Hyp	Ref	Expression
1		cgracol.p	$⊢ P = {Base}_{G}$
2		cgracol.i	$⊢ I = Itv (G)$
3		cgracol.m	$⊢ \underset{˙}{-} = dist (G)$
4		cgracol.g	$⊢ φ \to G \in 𝒢_{Tarski}$
5		cgracol.a	$⊢ φ \to A \in P$
6		cgracol.b	$⊢ φ \to B \in P$
7		cgracol.c	$⊢ φ \to C \in P$
8		cgracol.d	$⊢ φ \to D \in P$
9		cgracol.e	$⊢ φ \to E \in P$
10		cgracol.f	$⊢ φ \to F \in P$
11		cgracol.1	$⊢ φ \to ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩$
12		cgrancol.l	$⊢ L = {Line}_{𝒢} (G)$
13		cgrancol.2	$⊢ φ \to \neg (C \in (A L B) \lor A = B)$
14	4	adantr	$⊢ (φ \land (F \in (D L E) \lor D = E)) \to G \in 𝒢_{Tarski}$
15	8	adantr	$⊢ (φ \land (F \in (D L E) \lor D = E)) \to D \in P$
16	9	adantr	$⊢ (φ \land (F \in (D L E) \lor D = E)) \to E \in P$
17	10	adantr	$⊢ (φ \land (F \in (D L E) \lor D = E)) \to F \in P$
18	5	adantr	$⊢ (φ \land (F \in (D L E) \lor D = E)) \to A \in P$
19	6	adantr	$⊢ (φ \land (F \in (D L E) \lor D = E)) \to B \in P$
20	7	adantr	$⊢ (φ \land (F \in (D L E) \lor D = E)) \to C \in P$
21		eqid	$⊢ {hl}_{𝒢} (G) = {hl}_{𝒢} (G)$
22	11	adantr	$⊢ (φ \land (F \in (D L E) \lor D = E)) \to ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩$
23	1 2 14 21 18 19 20 15 16 17 22	cgracom	$⊢ (φ \land (F \in (D L E) \lor D = E)) \to ⟨“ D E F ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ A B C ”⟩$
24		simpr	$⊢ (φ \land (F \in (D L E) \lor D = E)) \to (F \in (D L E) \lor D = E)$
25	1 2 3 14 15 16 17 18 19 20 23 12 24	cgracol	$⊢ (φ \land (F \in (D L E) \lor D = E)) \to (C \in (A L B) \lor A = B)$
26	13 25	mtand	$⊢ φ \to \neg (F \in (D L E) \lor D = E)$

Metamath Proof Explorer

Theorem cgrancol

Proof