Theorem colperp

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

	Ref	Expression
Hypotheses	colperpex.p	|- P = ( Base ` G )
	colperpex.d	|- .- = ( dist ` G )
	colperpex.i	|- I = ( Itv ` G )
	colperpex.l	|- L = ( LineG ` G )
	colperpex.g	|- ( ph -> G e. TarskiG )
	colperp.a	|- ( ph -> A e. P )
	colperp.b	|- ( ph -> B e. P )
	colperp.c	|- ( ph -> C e. P )
	colperp.1	|- ( ph -> ( A L B ) ( perpG ` G ) D )
	colperp.2	|- ( ph -> ( C e. ( A L B ) \/ A = B ) )
	colperp.3	|- ( ph -> A =/= C )
Assertion	colperp	|- ( ph -> ( A L C ) ( perpG ` G ) D )

Proof

Step	Hyp	Ref	Expression
1		colperpex.p	|- P = ( Base ` G )
2		colperpex.d	|- .- = ( dist ` G )
3		colperpex.i	|- I = ( Itv ` G )
4		colperpex.l	|- L = ( LineG ` G )
5		colperpex.g	|- ( ph -> G e. TarskiG )
6		colperp.a	|- ( ph -> A e. P )
7		colperp.b	|- ( ph -> B e. P )
8		colperp.c	|- ( ph -> C e. P )
9		colperp.1	|- ( ph -> ( A L B ) ( perpG ` G ) D )
10		colperp.2	|- ( ph -> ( C e. ( A L B ) \/ A = B ) )
11		colperp.3	|- ( ph -> A =/= C )
12	4 5 9	perpln1	|- ( ph -> ( A L B ) e. ran L )
13	1 3 4 5 6 7 12	tglnne	|- ( ph -> A =/= B )
14	1 3 4 5 6 7 13	tglinerflx1	|- ( ph -> A e. ( A L B ) )
15	13	neneqd	|- ( ph -> -. A = B )
16	10	orcomd	|- ( ph -> ( A = B \/ C e. ( A L B ) ) )
17	16	ord	|- ( ph -> ( -. A = B -> C e. ( A L B ) ) )
18	15 17	mpd	|- ( ph -> C e. ( A L B ) )
19	1 3 4 5 6 8 11 11 12 14 18	tglinethru	|- ( ph -> ( A L B ) = ( A L C ) )
20	19 9	eqbrtrrd	|- ( ph -> ( A L C ) ( perpG ` G ) D )