Metamath Proof Explorer

Theorem ragncol

Description: Right angle implies non-colinearity. A consequence of theorem 8.9 of Schwabhauser p. 58. (Contributed by Thierry Arnoux, 1-Dec-2019)

Ref Expression
Hypotheses israg.p ⊢ P = Base G
israg.d ⊢ - ˙ = dist ⁡ G
israg.i ⊢ I = Itv ⁡ G
israg.l ⊢ L = Line 𝒢 ⁡ G
israg.s ⊢ S = pInv 𝒢 ⁡ G
israg.g ⊢ φ → G ∈ 𝒢 Tarski
israg.a ⊢ φ → A ∈ P
israg.b ⊢ φ → B ∈ P
israg.c ⊢ φ → C ∈ P
ragncol.1 ⊢ φ → ⟨“ ABC ”⟩ ∈ ∟ 𝒢 ⁡ G
ragncol.2 ⊢ φ → A ≠ B
ragncol.3 ⊢ φ → C ≠ B
Assertion ragncol ⊢ φ → ¬ C ∈ A L B ∨ A = B

Proof

Step Hyp Ref Expression
1 israg.p ⊢ P = Base G
2 israg.d ⊢ - ˙ = dist ⁡ G
3 israg.i ⊢ I = Itv ⁡ G
4 israg.l ⊢ L = Line 𝒢 ⁡ G
5 israg.s ⊢ S = pInv 𝒢 ⁡ G
6 israg.g ⊢ φ → G ∈ 𝒢 Tarski
7 israg.a ⊢ φ → A ∈ P
8 israg.b ⊢ φ → B ∈ P
9 israg.c ⊢ φ → C ∈ P
10 ragncol.1 ⊢ φ → ⟨“ ABC ”⟩ ∈ ∟ 𝒢 ⁡ G
11 ragncol.2 ⊢ φ → A ≠ B
12 ragncol.3 ⊢ φ → C ≠ B
13 11 neneqd ⊢ φ → ¬ A = B
14 12 neneqd ⊢ φ → ¬ C = B
15 ioran ⊢ ¬ A = B ∨ C = B ↔ ¬ A = B ∧ ¬ C = B
16 13 14 15 sylanbrc ⊢ φ → ¬ A = B ∨ C = B
17 6 adantr ⊢ φ ∧ C ∈ A L B ∨ A = B → G ∈ 𝒢 Tarski
18 7 adantr ⊢ φ ∧ C ∈ A L B ∨ A = B → A ∈ P
19 8 adantr ⊢ φ ∧ C ∈ A L B ∨ A = B → B ∈ P
20 9 adantr ⊢ φ ∧ C ∈ A L B ∨ A = B → C ∈ P
21 10 adantr ⊢ φ ∧ C ∈ A L B ∨ A = B → ⟨“ ABC ”⟩ ∈ ∟ 𝒢 ⁡ G
22 simpr ⊢ φ ∧ C ∈ A L B ∨ A = B → C ∈ A L B ∨ A = B
23 1 2 3 4 5 17 18 19 20 21 22 ragflat3 ⊢ φ ∧ C ∈ A L B ∨ A = B → A = B ∨ C = B
24 16 23 mtand ⊢ φ → ¬ C ∈ A L B ∨ A = B