Theorem ragflat3

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

	Ref	Expression
Hypotheses	israg.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
	israg.d	⊢ − = ( dist ‘ 𝐺 )
	israg.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
	israg.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
	israg.s	⊢ 𝑆 = ( pInvG ‘ 𝐺 )
	israg.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
	israg.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
	israg.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
	israg.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
	ragflat3.1	⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
	ragflat3.2	⊢ ( 𝜑 → ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) )
Assertion	ragflat3	⊢ ( 𝜑 → ( 𝐴 = 𝐵 ∨ 𝐶 = 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		israg.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
2		israg.d	⊢ − = ( dist ‘ 𝐺 )
3		israg.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
4		israg.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
5		israg.s	⊢ 𝑆 = ( pInvG ‘ 𝐺 )
6		israg.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
7		israg.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
8		israg.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
9		israg.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
10		ragflat3.1	⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
11		ragflat3.2	⊢ ( 𝜑 → ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) )
12	6	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝐴 = 𝐵 ) → 𝐺 ∈ TarskiG )
13	9	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝐴 = 𝐵 ) → 𝐶 ∈ 𝑃 )
14	8	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝐴 = 𝐵 ) → 𝐵 ∈ 𝑃 )
15	7	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝐴 = 𝐵 ) → 𝐴 ∈ 𝑃 )
16	10	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝐴 = 𝐵 ) → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
17		simpr	⊢ ( ( 𝜑 ∧ ¬ 𝐴 = 𝐵 ) → ¬ 𝐴 = 𝐵 )
18	17	neqned	⊢ ( ( 𝜑 ∧ ¬ 𝐴 = 𝐵 ) → 𝐴 ≠ 𝐵 )
19	11	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝐴 = 𝐵 ) → ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) )
20	1 4 3 12 15 14 13 19	colrot1	⊢ ( ( 𝜑 ∧ ¬ 𝐴 = 𝐵 ) → ( 𝐴 ∈ ( 𝐵 𝐿 𝐶 ) ∨ 𝐵 = 𝐶 ) )
21	1 2 3 4 5 12 15 14 13 13 16 18 20	ragcol	⊢ ( ( 𝜑 ∧ ¬ 𝐴 = 𝐵 ) → ⟨“ 𝐶 𝐵 𝐶 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
22	1 2 3 4 5 12 13 14 15 21	ragtriva	⊢ ( ( 𝜑 ∧ ¬ 𝐴 = 𝐵 ) → 𝐶 = 𝐵 )
23	22	ex	⊢ ( 𝜑 → ( ¬ 𝐴 = 𝐵 → 𝐶 = 𝐵 ) )
24	23	orrd	⊢ ( 𝜑 → ( 𝐴 = 𝐵 ∨ 𝐶 = 𝐵 ) )