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	$⊢ \underset{˙}{-} = dist (G)$
	israg.i	$⊢ I = Itv (G)$
	israg.l	$⊢ L = {Line}_{𝒢} (G)$
	israg.s	$⊢ S = {pInv}_{𝒢} (G)$
	israg.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	israg.a	$⊢ φ \to A \in P$
	israg.b	$⊢ φ \to B \in P$
	israg.c	$⊢ φ \to C \in P$
	ragcol.d	$⊢ φ \to D \in P$
	ragcol.1	$⊢ φ \to ⟨“ A B C ”⟩ \in ∟_{𝒢} (G)$
	ragcol.2	$⊢ φ \to A \neq B$
	ragcol.3	$⊢ φ \to (A \in (B L D) \lor B = D)$
Assertion	ragcol	$⊢ φ \to ⟨“ D B C ”⟩ \in ∟_{𝒢} (G)$

Proof

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		ragcol.d	$⊢ φ \to D \in P$
11		ragcol.1	$⊢ φ \to ⟨“ A B C ”⟩ \in ∟_{𝒢} (G)$
12		ragcol.2	$⊢ φ \to A \neq B$
13		ragcol.3	$⊢ φ \to (A \in (B L D) \lor B = D)$
14		eqid	$⊢ \sim_{𝒢} (G) = \sim_{𝒢} (G)$
15		eqid	$⊢ S (B) = S (B)$
16	1 2 3 4 5 6 8 15 9	mircl	$⊢ φ \to S (B) (C) \in P$
17	12	necomd	$⊢ φ \to B \neq A$
18	1 2 3 4 5 6 8 15 9	mircgr	$⊢ φ \to B \underset{˙}{-} S (B) (C) = B \underset{˙}{-} C$
19	18	eqcomd	$⊢ φ \to B \underset{˙}{-} C = B \underset{˙}{-} S (B) (C)$
20	1 2 3 4 5 6 7 8 9	israg	$⊢ φ \to (⟨“ A B C ”⟩ \in ∟_{𝒢} (G) \leftrightarrow A \underset{˙}{-} C = A \underset{˙}{-} S (B) (C))$
21	11 20	mpbid	$⊢ φ \to A \underset{˙}{-} C = A \underset{˙}{-} S (B) (C)$
22	1 4 3 6 8 7 10 14 9 16 2 17 13 19 21	lncgr	$⊢ φ \to D \underset{˙}{-} C = D \underset{˙}{-} S (B) (C)$
23	1 2 3 4 5 6 10 8 9	israg	$⊢ φ \to (⟨“ D B C ”⟩ \in ∟_{𝒢} (G) \leftrightarrow D \underset{˙}{-} C = D \underset{˙}{-} S (B) (C))$
24	22 23	mpbird	$⊢ φ \to ⟨“ D B C ”⟩ \in ∟_{𝒢} (G)$

Metamath Proof Explorer

Theorem ragcol

Proof