Theorem ragtriva

Description: Trivial right angle. Theorem 8.8 of Schwabhauser p. 58. (Contributed by Thierry Arnoux, 3-Sep-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$$
	ragtriva.1	$$⊢\phi \to ⟨“ABA”⟩\in {∟}_{𝒢}\left(G\right)$$
Assertion	ragtriva	$$⊢\phi \to A=B$$

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		ragtriva.1	$$⊢\phi \to ⟨“ABA”⟩\in {∟}_{𝒢}\left(G\right)$$
11	1 2 3 4 5 6 8 7 9	ragtrivb	$$⊢\phi \to ⟨“BAA”⟩\in {∟}_{𝒢}\left(G\right)$$
12	1 2 3 4 5 6 8 7 7 11	ragcom	$$⊢\phi \to ⟨“AAB”⟩\in {∟}_{𝒢}\left(G\right)$$
13	1 2 3 4 5 6 7 7 8 12 10	ragflat	$$⊢\phi \to A=B$$