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={\mathrm{Base}}_G$$
	israg.d	$$⊢\underset{\dot{}}{-}=\mathrm{dist}\left(G\right)$$
	israg.i	$$⊢I=\mathrm{Itv}\left(G\right)$$
	israg.l	$$⊢L={Line}_{𝒢}\left(G\right)$$
	israg.s	$$⊢S={pInv}_{𝒢}\left(G\right)$$
	israg.g	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}$$
	israg.a	$$⊢\phi \to A\in P$$
	israg.b	$$⊢\phi \to B\in P$$
	israg.c	$$⊢\phi \to C\in P$$
	ragcol.d	$$⊢\phi \to D\in P$$
	ragcol.1	$$⊢\phi \to ⟨“ABC”⟩\in {∟}_{𝒢}\left(G\right)$$
	ragcol.2	$$⊢\phi \to A\ne B$$
	ragcol.3	$$⊢\phi \to \left(A\in \left(BLD\right)\vee B=D\right)$$
Assertion	ragcol	$$⊢\phi \to ⟨“DBC”⟩\in {∟}_{𝒢}\left(G\right)$$

Proof

Step	Hyp	Ref	Expression
1		israg.p	$$⊢P={\mathrm{Base}}_G$$
2		israg.d	$$⊢\underset{\dot{}}{-}=\mathrm{dist}\left(G\right)$$
3		israg.i	$$⊢I=\mathrm{Itv}\left(G\right)$$
4		israg.l	$$⊢L={Line}_{𝒢}\left(G\right)$$
5		israg.s	$$⊢S={pInv}_{𝒢}\left(G\right)$$
6		israg.g	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}$$
7		israg.a	$$⊢\phi \to A\in P$$
8		israg.b	$$⊢\phi \to B\in P$$
9		israg.c	$$⊢\phi \to C\in P$$
10		ragcol.d	$$⊢\phi \to D\in P$$
11		ragcol.1	$$⊢\phi \to ⟨“ABC”⟩\in {∟}_{𝒢}\left(G\right)$$
12		ragcol.2	$$⊢\phi \to A\ne B$$
13		ragcol.3	$$⊢\phi \to \left(A\in \left(BLD\right)\vee B=D\right)$$
14		eqid	$$⊢{\sim }_{𝒢}\left(G\right)={\sim }_{𝒢}\left(G\right)$$
15		eqid	$$⊢S\left(B\right)=S\left(B\right)$$
16	1 2 3 4 5 6 8 15 9	mircl	$$⊢\phi \to S\left(B\right)\left(C\right)\in P$$
17	12	necomd	$$⊢\phi \to B\ne A$$
18	1 2 3 4 5 6 8 15 9	mircgr	$$⊢\phi \to B\underset{\dot{}}{-}S\left(B\right)\left(C\right)=B\underset{\dot{}}{-}C$$
19	18	eqcomd	$$⊢\phi \to B\underset{\dot{}}{-}C=B\underset{\dot{}}{-}S\left(B\right)\left(C\right)$$
20	1 2 3 4 5 6 7 8 9	israg	$$⊢\phi \to \left(⟨“ABC”⟩\in {∟}_{𝒢}\left(G\right)\leftrightarrow A\underset{\dot{}}{-}C=A\underset{\dot{}}{-}S\left(B\right)\left(C\right)\right)$$
21	11 20	mpbid	$$⊢\phi \to A\underset{\dot{}}{-}C=A\underset{\dot{}}{-}S\left(B\right)\left(C\right)$$
22	1 4 3 6 8 7 10 14 9 16 2 17 13 19 21	lncgr	$$⊢\phi \to D\underset{\dot{}}{-}C=D\underset{\dot{}}{-}S\left(B\right)\left(C\right)$$
23	1 2 3 4 5 6 10 8 9	israg	$$⊢\phi \to \left(⟨“DBC”⟩\in {∟}_{𝒢}\left(G\right)\leftrightarrow D\underset{\dot{}}{-}C=D\underset{\dot{}}{-}S\left(B\right)\left(C\right)\right)$$
24	22 23	mpbird	$$⊢\phi \to ⟨“DBC”⟩\in {∟}_{𝒢}\left(G\right)$$