ragflat3

Description: Right angle and colinearity. Theorem 8.9 of Schwabhauser p. 58. (Contributed by Thierry Arnoux, 4-Sep-2019)

Step	Hyp	Ref	Expression
1		israg.p	$⊢ P = {Base}_{G}$
2		israg.d	$⊢ \underset{˙}{-} = dist (G)$
3		israg.i	$⊢ I = Itv (G)$
4		israg.l	$⊢ L = {Line}_{𝒢} (G)$
5		israg.s	$⊢ S = {pInv}_{𝒢} (G)$
6		israg.g	$⊢ φ \to G \in 𝒢_{Tarski}$
7		israg.a	$⊢ φ \to A \in P$
8		israg.b	$⊢ φ \to B \in P$
9		israg.c	$⊢ φ \to C \in P$
10		ragflat3.1	$⊢ φ \to ⟨“ A B C ”⟩ \in ∟_{𝒢} (G)$
11		ragflat3.2	$⊢ φ \to (C \in (A L B) \lor A = B)$
12	6	adantr	$⊢ (φ \land \neg A = B) \to G \in 𝒢_{Tarski}$
13	9	adantr	$⊢ (φ \land \neg A = B) \to C \in P$
14	8	adantr	$⊢ (φ \land \neg A = B) \to B \in P$
15	7	adantr	$⊢ (φ \land \neg A = B) \to A \in P$
16	10	adantr	$⊢ (φ \land \neg A = B) \to ⟨“ A B C ”⟩ \in ∟_{𝒢} (G)$
17		simpr	$⊢ (φ \land \neg A = B) \to \neg A = B$
18	17	neqned	$⊢ (φ \land \neg A = B) \to A \neq B$
19	11	adantr	$⊢ (φ \land \neg A = B) \to (C \in (A L B) \lor A = B)$
20	1 4 3 12 15 14 13 19	colrot1	$⊢ (φ \land \neg A = B) \to (A \in (B L C) \lor B = C)$
21	1 2 3 4 5 12 15 14 13 13 16 18 20	ragcol	$⊢ (φ \land \neg A = B) \to ⟨“ C B C ”⟩ \in ∟_{𝒢} (G)$
22	1 2 3 4 5 12 13 14 15 21	ragtriva	$⊢ (φ \land \neg A = B) \to C = B$
23	22	ex	$⊢ φ \to (\neg A = B \to C = B)$
24	23	orrd	$⊢ φ \to (A = B \lor C = B)$

Metamath Proof Explorer