Metamath Proof Explorer

Theorem ragcol

Description: The right angle property is independent of the choice of point on one side. Theorem 8.3 of Schwabhauser p. 58. (Contributed by Thierry Arnoux, 25-Aug-2019)

Ref Expression
Hypotheses israg.p $⊢ P = Base G$
israg.d
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$
ragcol.d $⊢ φ → D ∈ P$
ragcol.1 $⊢ φ → ⟨“ ABC ”⟩ ∈ ∟ 𝒢 ⁡ G$
ragcol.2 $⊢ φ → A ≠ B$
ragcol.3 $⊢ φ → A ∈ B L D ∨ B = D$
Assertion ragcol $⊢ φ → ⟨“ DBC ”⟩ ∈ ∟ 𝒢 ⁡ G$

Proof

Step Hyp Ref Expression
1 israg.p $⊢ P = Base G$
2 israg.d
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 ragcol.d $⊢ φ → D ∈ P$
11 ragcol.1 $⊢ φ → ⟨“ ABC ”⟩ ∈ ∟ 𝒢 ⁡ G$
12 ragcol.2 $⊢ φ → A ≠ B$
13 ragcol.3 $⊢ φ → A ∈ B L D ∨ B = D$
14 eqid $⊢ ∼ 𝒢 ⁡ G = ∼ 𝒢 ⁡ G$
15 eqid $⊢ S ⁡ B = S ⁡ B$
16 1 2 3 4 5 6 8 15 9 mircl $⊢ φ → S ⁡ B ⁡ C ∈ P$
17 12 necomd $⊢ φ → B ≠ A$
18 1 2 3 4 5 6 8 15 9 mircgr
19 18 eqcomd
20 1 2 3 4 5 6 7 8 9 israg
21 11 20 mpbid
22 1 4 3 6 8 7 10 14 9 16 2 17 13 19 21 lncgr
23 1 2 3 4 5 6 10 8 9 israg
24 22 23 mpbird $⊢ φ → ⟨“ DBC ”⟩ ∈ ∟ 𝒢 ⁡ G$