Theorem cgrancol

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

	Ref	Expression
Hypotheses	cgracol.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
	cgracol.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
	cgracol.m	⊢ − = ( dist ‘ 𝐺 )
	cgracol.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
	cgracol.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
	cgracol.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
	cgracol.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
	cgracol.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
	cgracol.e	⊢ ( 𝜑 → 𝐸 ∈ 𝑃 )
	cgracol.f	⊢ ( 𝜑 → 𝐹 ∈ 𝑃 )
	cgracol.1	⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ )
	cgrancol.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
	cgrancol.2	⊢ ( 𝜑 → ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) )
Assertion	cgrancol	⊢ ( 𝜑 → ¬ ( 𝐹 ∈ ( 𝐷 𝐿 𝐸 ) ∨ 𝐷 = 𝐸 ) )

Proof

Step	Hyp	Ref	Expression
1		cgracol.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
2		cgracol.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
3		cgracol.m	⊢ − = ( dist ‘ 𝐺 )
4		cgracol.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
5		cgracol.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
6		cgracol.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
7		cgracol.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
8		cgracol.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
9		cgracol.e	⊢ ( 𝜑 → 𝐸 ∈ 𝑃 )
10		cgracol.f	⊢ ( 𝜑 → 𝐹 ∈ 𝑃 )
11		cgracol.1	⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ )
12		cgrancol.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
13		cgrancol.2	⊢ ( 𝜑 → ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) )
14	4	adantr	⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( 𝐷 𝐿 𝐸 ) ∨ 𝐷 = 𝐸 ) ) → 𝐺 ∈ TarskiG )
15	8	adantr	⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( 𝐷 𝐿 𝐸 ) ∨ 𝐷 = 𝐸 ) ) → 𝐷 ∈ 𝑃 )
16	9	adantr	⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( 𝐷 𝐿 𝐸 ) ∨ 𝐷 = 𝐸 ) ) → 𝐸 ∈ 𝑃 )
17	10	adantr	⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( 𝐷 𝐿 𝐸 ) ∨ 𝐷 = 𝐸 ) ) → 𝐹 ∈ 𝑃 )
18	5	adantr	⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( 𝐷 𝐿 𝐸 ) ∨ 𝐷 = 𝐸 ) ) → 𝐴 ∈ 𝑃 )
19	6	adantr	⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( 𝐷 𝐿 𝐸 ) ∨ 𝐷 = 𝐸 ) ) → 𝐵 ∈ 𝑃 )
20	7	adantr	⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( 𝐷 𝐿 𝐸 ) ∨ 𝐷 = 𝐸 ) ) → 𝐶 ∈ 𝑃 )
21		eqid	⊢ ( hlG ‘ 𝐺 ) = ( hlG ‘ 𝐺 )
22	11	adantr	⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( 𝐷 𝐿 𝐸 ) ∨ 𝐷 = 𝐸 ) ) → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ )
23	1 2 14 21 18 19 20 15 16 17 22	cgracom	⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( 𝐷 𝐿 𝐸 ) ∨ 𝐷 = 𝐸 ) ) → ⟨“ 𝐷 𝐸 𝐹 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐴 𝐵 𝐶 ”⟩ )
24		simpr	⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( 𝐷 𝐿 𝐸 ) ∨ 𝐷 = 𝐸 ) ) → ( 𝐹 ∈ ( 𝐷 𝐿 𝐸 ) ∨ 𝐷 = 𝐸 ) )
25	1 2 3 14 15 16 17 18 19 20 23 12 24	cgracol	⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( 𝐷 𝐿 𝐸 ) ∨ 𝐷 = 𝐸 ) ) → ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) )
26	13 25	mtand	⊢ ( 𝜑 → ¬ ( 𝐹 ∈ ( 𝐷 𝐿 𝐸 ) ∨ 𝐷 = 𝐸 ) )