Theorem colperp

Description: Deduce a perpendicularity from perpendicularity and colinearity. (Contributed by Thierry Arnoux, 8-Dec-2019)

	Ref	Expression
Hypotheses	colperpex.p	$$⊢P={\mathrm{Base}}_G$$
	colperpex.d	$$⊢\underset{\dot{}}{-}=\mathrm{dist}\left(G\right)$$
	colperpex.i	$$⊢I=\mathrm{Itv}\left(G\right)$$
	colperpex.l	$$⊢L={Line}_{𝒢}\left(G\right)$$
	colperpex.g	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}$$
	colperp.a	$$⊢\phi \to A\in P$$
	colperp.b	$$⊢\phi \to B\in P$$
	colperp.c	$$⊢\phi \to C\in P$$
	colperp.1	$$⊢\phi \to \left(ALB\right){⟂}_{𝒢}\left(G\right)D$$
	colperp.2	$$⊢\phi \to \left(C\in \left(ALB\right)\vee A=B\right)$$
	colperp.3	$$⊢\phi \to A\ne C$$
Assertion	colperp	$$⊢\phi \to \left(ALC\right){⟂}_{𝒢}\left(G\right)D$$

Proof

Step	Hyp	Ref	Expression
1		colperpex.p	$$⊢P={\mathrm{Base}}_G$$
2		colperpex.d	$$⊢\underset{\dot{}}{-}=\mathrm{dist}\left(G\right)$$
3		colperpex.i	$$⊢I=\mathrm{Itv}\left(G\right)$$
4		colperpex.l	$$⊢L={Line}_{𝒢}\left(G\right)$$
5		colperpex.g	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}$$
6		colperp.a	$$⊢\phi \to A\in P$$
7		colperp.b	$$⊢\phi \to B\in P$$
8		colperp.c	$$⊢\phi \to C\in P$$
9		colperp.1	$$⊢\phi \to \left(ALB\right){⟂}_{𝒢}\left(G\right)D$$
10		colperp.2	$$⊢\phi \to \left(C\in \left(ALB\right)\vee A=B\right)$$
11		colperp.3	$$⊢\phi \to A\ne C$$
12	4 5 9	perpln1	$$⊢\phi \to ALB\in \mathrm{ran}L$$
13	1 3 4 5 6 7 12	tglnne	$$⊢\phi \to A\ne B$$
14	1 3 4 5 6 7 13	tglinerflx1	$$⊢\phi \to A\in \left(ALB\right)$$
15	13	neneqd	$$⊢\phi \to \neg A=B$$
16	10	orcomd	$$⊢\phi \to \left(A=B\vee C\in \left(ALB\right)\right)$$
17	16	ord	$$⊢\phi \to \left(\neg A=B\to C\in \left(ALB\right)\right)$$
18	15 17	mpd	$$⊢\phi \to C\in \left(ALB\right)$$
19	1 3 4 5 6 8 11 11 12 14 18	tglinethru	$$⊢\phi \to ALB=ALC$$
20	19 9	eqbrtrrd	$$⊢\phi \to \left(ALC\right){⟂}_{𝒢}\left(G\right)D$$