Metamath Proof Explorer

Theorem trgcopy

Description: Triangle construction: a copy of a given triangle can always be constructed in such a way that one side is lying on a half-line, and the third vertex is on a given half-plane: existence part. First part of Theorem 10.16 of Schwabhauser p. 92. (Contributed by Thierry Arnoux, 4-Aug-2020)

Ref Expression
Hypotheses trgcopy.p 
|- P = ( Base ` G )
trgcopy.m 
|- .- = ( dist ` G )
trgcopy.i 
|- I = ( Itv ` G )
trgcopy.l 
|- L = ( LineG ` G )
trgcopy.k 
|- K = ( hlG ` G )
trgcopy.g 
|- ( ph -> G e. TarskiG )
trgcopy.a 
|- ( ph -> A e. P )
trgcopy.b 
|- ( ph -> B e. P )
trgcopy.c 
|- ( ph -> C e. P )
trgcopy.d 
|- ( ph -> D e. P )
trgcopy.e 
|- ( ph -> E e. P )
trgcopy.f 
|- ( ph -> F e. P )
trgcopy.1 
|- ( ph -> -. ( A e. ( B L C ) \/ B = C ) )
trgcopy.2 
|- ( ph -> -. ( D e. ( E L F ) \/ E = F ) )
trgcopy.3 
|- ( ph -> ( A .- B ) = ( D .- E ) )
Assertion trgcopy 
|- ( ph -> E. f e. P ( <" A B C "> ( cgrG ` G ) <" D E f "> /\ f ( ( hpG ` G ) ` ( D L E ) ) F ) )

Proof

Step Hyp Ref Expression
1 trgcopy.p 
 |-  P = ( Base ` G )
2 trgcopy.m 
 |-  .- = ( dist ` G )
3 trgcopy.i 
 |-  I = ( Itv ` G )
4 trgcopy.l 
 |-  L = ( LineG ` G )
5 trgcopy.k 
 |-  K = ( hlG ` G )
6 trgcopy.g 
 |-  ( ph -> G e. TarskiG )
7 trgcopy.a 
 |-  ( ph -> A e. P )
8 trgcopy.b 
 |-  ( ph -> B e. P )
9 trgcopy.c 
 |-  ( ph -> C e. P )
10 trgcopy.d 
 |-  ( ph -> D e. P )
11 trgcopy.e 
 |-  ( ph -> E e. P )
12 trgcopy.f 
 |-  ( ph -> F e. P )
13 trgcopy.1 
 |-  ( ph -> -. ( A e. ( B L C ) \/ B = C ) )
14 trgcopy.2 
 |-  ( ph -> -. ( D e. ( E L F ) \/ E = F ) )
15 trgcopy.3 
 |-  ( ph -> ( A .- B ) = ( D .- E ) )
16 eqid 
 |-  ( cgrG ` G ) = ( cgrG ` G )
17 6 ad2antrr 
 |-  ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) -> G e. TarskiG )
18 17 ad2antrr 
 |-  ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ y e. P ) /\ <" A B x "> ( cgrG ` G ) <" D E y "> ) -> G e. TarskiG )
19 18 ad2antrr 
 |-  ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ y e. P ) /\ <" A B x "> ( cgrG ` G ) <" D E y "> ) /\ q e. P ) /\ ( ( D L E ) ( perpG ` G ) ( q L y ) /\ q ( ( hpG ` G ) ` ( D L E ) ) F ) ) -> G e. TarskiG )
20 19 adantr 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ y e. P ) /\ <" A B x "> ( cgrG ` G ) <" D E y "> ) /\ q e. P ) /\ ( ( D L E ) ( perpG ` G ) ( q L y ) /\ q ( ( hpG ` G ) ` ( D L E ) ) F ) ) /\ ( f e. P /\ ( f ( K ` y ) q /\ ( y .- f ) = ( x .- C ) ) ) ) -> G e. TarskiG )
21 7 ad2antrr 
 |-  ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) -> A e. P )
22 21 ad2antrr 
 |-  ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ y e. P ) /\ <" A B x "> ( cgrG ` G ) <" D E y "> ) -> A e. P )
23 22 ad3antrrr 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ y e. P ) /\ <" A B x "> ( cgrG ` G ) <" D E y "> ) /\ q e. P ) /\ ( ( D L E ) ( perpG ` G ) ( q L y ) /\ q ( ( hpG ` G ) ` ( D L E ) ) F ) ) /\ ( f e. P /\ ( f ( K ` y ) q /\ ( y .- f ) = ( x .- C ) ) ) ) -> A e. P )
24 8 ad2antrr 
 |-  ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) -> B e. P )
25 24 ad2antrr 
 |-  ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ y e. P ) /\ <" A B x "> ( cgrG ` G ) <" D E y "> ) -> B e. P )
26 25 ad3antrrr 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ y e. P ) /\ <" A B x "> ( cgrG ` G ) <" D E y "> ) /\ q e. P ) /\ ( ( D L E ) ( perpG ` G ) ( q L y ) /\ q ( ( hpG ` G ) ` ( D L E ) ) F ) ) /\ ( f e. P /\ ( f ( K ` y ) q /\ ( y .- f ) = ( x .- C ) ) ) ) -> B e. P )
27 9 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ y e. P ) /\ <" A B x "> ( cgrG ` G ) <" D E y "> ) /\ q e. P ) /\ ( ( D L E ) ( perpG ` G ) ( q L y ) /\ q ( ( hpG ` G ) ` ( D L E ) ) F ) ) -> C e. P )
28 27 adantr 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ y e. P ) /\ <" A B x "> ( cgrG ` G ) <" D E y "> ) /\ q e. P ) /\ ( ( D L E ) ( perpG ` G ) ( q L y ) /\ q ( ( hpG ` G ) ` ( D L E ) ) F ) ) /\ ( f e. P /\ ( f ( K ` y ) q /\ ( y .- f ) = ( x .- C ) ) ) ) -> C e. P )
29 10 ad2antrr 
 |-  ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) -> D e. P )
30 29 ad2antrr 
 |-  ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ y e. P ) /\ <" A B x "> ( cgrG ` G ) <" D E y "> ) -> D e. P )
31 30 ad3antrrr 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ y e. P ) /\ <" A B x "> ( cgrG ` G ) <" D E y "> ) /\ q e. P ) /\ ( ( D L E ) ( perpG ` G ) ( q L y ) /\ q ( ( hpG ` G ) ` ( D L E ) ) F ) ) /\ ( f e. P /\ ( f ( K ` y ) q /\ ( y .- f ) = ( x .- C ) ) ) ) -> D e. P )
32 11 ad2antrr 
 |-  ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) -> E e. P )
33 32 ad2antrr 
 |-  ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ y e. P ) /\ <" A B x "> ( cgrG ` G ) <" D E y "> ) -> E e. P )
34 33 ad3antrrr 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ y e. P ) /\ <" A B x "> ( cgrG ` G ) <" D E y "> ) /\ q e. P ) /\ ( ( D L E ) ( perpG ` G ) ( q L y ) /\ q ( ( hpG ` G ) ` ( D L E ) ) F ) ) /\ ( f e. P /\ ( f ( K ` y ) q /\ ( y .- f ) = ( x .- C ) ) ) ) -> E e. P )
35 simprl 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ y e. P ) /\ <" A B x "> ( cgrG ` G ) <" D E y "> ) /\ q e. P ) /\ ( ( D L E ) ( perpG ` G ) ( q L y ) /\ q ( ( hpG ` G ) ` ( D L E ) ) F ) ) /\ ( f e. P /\ ( f ( K ` y ) q /\ ( y .- f ) = ( x .- C ) ) ) ) -> f e. P )
36 15 ad2antrr 
 |-  ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) -> ( A .- B ) = ( D .- E ) )
37 36 ad5antr 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ y e. P ) /\ <" A B x "> ( cgrG ` G ) <" D E y "> ) /\ q e. P ) /\ ( ( D L E ) ( perpG ` G ) ( q L y ) /\ q ( ( hpG ` G ) ` ( D L E ) ) F ) ) /\ ( f e. P /\ ( f ( K ` y ) q /\ ( y .- f ) = ( x .- C ) ) ) ) -> ( A .- B ) = ( D .- E ) )
38 1 4 3 6 8 9 7 13 ncoltgdim2 
 |-  ( ph -> G TarskiGDim>= 2 )
39 38 ad4antr 
 |-  ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ y e. P ) /\ <" A B x "> ( cgrG ` G ) <" D E y "> ) -> G TarskiGDim>= 2 )
40 39 ad3antrrr 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ y e. P ) /\ <" A B x "> ( cgrG ` G ) <" D E y "> ) /\ q e. P ) /\ ( ( D L E ) ( perpG ` G ) ( q L y ) /\ q ( ( hpG ` G ) ` ( D L E ) ) F ) ) /\ ( f e. P /\ ( f ( K ` y ) q /\ ( y .- f ) = ( x .- C ) ) ) ) -> G TarskiGDim>= 2 )
41 1 3 4 6 7 8 9 13 ncolne1 
 |-  ( ph -> A =/= B )
42 1 3 4 6 7 8 41 tgelrnln 
 |-  ( ph -> ( A L B ) e. ran L )
43 42 ad2antrr 
 |-  ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) -> ( A L B ) e. ran L )
44 simplr 
 |-  ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) -> x e. ( A L B ) )
45 1 4 3 17 43 44 tglnpt 
 |-  ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) -> x e. P )
46 45 ad2antrr 
 |-  ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ y e. P ) /\ <" A B x "> ( cgrG ` G ) <" D E y "> ) -> x e. P )
47 46 ad2antrr 
 |-  ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ y e. P ) /\ <" A B x "> ( cgrG ` G ) <" D E y "> ) /\ q e. P ) /\ ( ( D L E ) ( perpG ` G ) ( q L y ) /\ q ( ( hpG ` G ) ` ( D L E ) ) F ) ) -> x e. P )
48 47 adantr 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ y e. P ) /\ <" A B x "> ( cgrG ` G ) <" D E y "> ) /\ q e. P ) /\ ( ( D L E ) ( perpG ` G ) ( q L y ) /\ q ( ( hpG ` G ) ` ( D L E ) ) F ) ) /\ ( f e. P /\ ( f ( K ` y ) q /\ ( y .- f ) = ( x .- C ) ) ) ) -> x e. P )
49 simplr 
 |-  ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ y e. P ) /\ <" A B x "> ( cgrG ` G ) <" D E y "> ) -> y e. P )
50 49 ad2antrr 
 |-  ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ y e. P ) /\ <" A B x "> ( cgrG ` G ) <" D E y "> ) /\ q e. P ) /\ ( ( D L E ) ( perpG ` G ) ( q L y ) /\ q ( ( hpG ` G ) ` ( D L E ) ) F ) ) -> y e. P )
51 50 adantr 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ y e. P ) /\ <" A B x "> ( cgrG ` G ) <" D E y "> ) /\ q e. P ) /\ ( ( D L E ) ( perpG ` G ) ( q L y ) /\ q ( ( hpG ` G ) ` ( D L E ) ) F ) ) /\ ( f e. P /\ ( f ( K ` y ) q /\ ( y .- f ) = ( x .- C ) ) ) ) -> y e. P )
52 44 ad5antr 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ y e. P ) /\ <" A B x "> ( cgrG ` G ) <" D E y "> ) /\ q e. P ) /\ ( ( D L E ) ( perpG ` G ) ( q L y ) /\ q ( ( hpG ` G ) ` ( D L E ) ) F ) ) /\ ( f e. P /\ ( f ( K ` y ) q /\ ( y .- f ) = ( x .- C ) ) ) ) -> x e. ( A L B ) )
53 41 ad7antr 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ y e. P ) /\ <" A B x "> ( cgrG ` G ) <" D E y "> ) /\ q e. P ) /\ ( ( D L E ) ( perpG ` G ) ( q L y ) /\ q ( ( hpG ` G ) ` ( D L E ) ) F ) ) /\ ( f e. P /\ ( f ( K ` y ) q /\ ( y .- f ) = ( x .- C ) ) ) ) -> A =/= B )
54 1 3 4 20 23 26 53 tglinecom 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ y e. P ) /\ <" A B x "> ( cgrG ` G ) <" D E y "> ) /\ q e. P ) /\ ( ( D L E ) ( perpG ` G ) ( q L y ) /\ q ( ( hpG ` G ) ` ( D L E ) ) F ) ) /\ ( f e. P /\ ( f ( K ` y ) q /\ ( y .- f ) = ( x .- C ) ) ) ) -> ( A L B ) = ( B L A ) )
55 52 54 eleqtrd 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ y e. P ) /\ <" A B x "> ( cgrG ` G ) <" D E y "> ) /\ q e. P ) /\ ( ( D L E ) ( perpG ` G ) ( q L y ) /\ q ( ( hpG ` G ) ` ( D L E ) ) F ) ) /\ ( f e. P /\ ( f ( K ` y ) q /\ ( y .- f ) = ( x .- C ) ) ) ) -> x e. ( B L A ) )
56 simp-6r 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ y e. P ) /\ <" A B x "> ( cgrG ` G ) <" D E y "> ) /\ q e. P ) /\ ( ( D L E ) ( perpG ` G ) ( q L y ) /\ q ( ( hpG ` G ) ` ( D L E ) ) F ) ) /\ ( f e. P /\ ( f ( K ` y ) q /\ ( y .- f ) = ( x .- C ) ) ) ) -> ( C L x ) ( perpG ` G ) ( A L B ) )
57 4 20 56 perpln1 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ y e. P ) /\ <" A B x "> ( cgrG ` G ) <" D E y "> ) /\ q e. P ) /\ ( ( D L E ) ( perpG ` G ) ( q L y ) /\ q ( ( hpG ` G ) ` ( D L E ) ) F ) ) /\ ( f e. P /\ ( f ( K ` y ) q /\ ( y .- f ) = ( x .- C ) ) ) ) -> ( C L x ) e. ran L )
58 43 ad5antr 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ y e. P ) /\ <" A B x "> ( cgrG ` G ) <" D E y "> ) /\ q e. P ) /\ ( ( D L E ) ( perpG ` G ) ( q L y ) /\ q ( ( hpG ` G ) ` ( D L E ) ) F ) ) /\ ( f e. P /\ ( f ( K ` y ) q /\ ( y .- f ) = ( x .- C ) ) ) ) -> ( A L B ) e. ran L )
59 1 2 3 4 20 57 58 56 perpcom 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ y e. P ) /\ <" A B x "> ( cgrG ` G ) <" D E y "> ) /\ q e. P ) /\ ( ( D L E ) ( perpG ` G ) ( q L y ) /\ q ( ( hpG ` G ) ` ( D L E ) ) F ) ) /\ ( f e. P /\ ( f ( K ` y ) q /\ ( y .- f ) = ( x .- C ) ) ) ) -> ( A L B ) ( perpG ` G ) ( C L x ) )
60 1 4 3 6 8 9 7 13 ncolrot2 
 |-  ( ph -> -. ( C e. ( A L B ) \/ A = B ) )
61 ioran 
 |-  ( -. ( C e. ( A L B ) \/ A = B ) <-> ( -. C e. ( A L B ) /\ -. A = B ) )
62 60 61 sylib 
 |-  ( ph -> ( -. C e. ( A L B ) /\ -. A = B ) )
63 62 simpld 
 |-  ( ph -> -. C e. ( A L B ) )
64 63 ad2antrr 
 |-  ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) -> -. C e. ( A L B ) )
65 nelne2 
 |-  ( ( x e. ( A L B ) /\ -. C e. ( A L B ) ) -> x =/= C )
66 44 64 65 syl2anc 
 |-  ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) -> x =/= C )
67 66 ad4antr 
 |-  ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ y e. P ) /\ <" A B x "> ( cgrG ` G ) <" D E y "> ) /\ q e. P ) /\ ( ( D L E ) ( perpG ` G ) ( q L y ) /\ q ( ( hpG ` G ) ` ( D L E ) ) F ) ) -> x =/= C )
68 67 adantr 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ y e. P ) /\ <" A B x "> ( cgrG ` G ) <" D E y "> ) /\ q e. P ) /\ ( ( D L E ) ( perpG ` G ) ( q L y ) /\ q ( ( hpG ` G ) ` ( D L E ) ) F ) ) /\ ( f e. P /\ ( f ( K ` y ) q /\ ( y .- f ) = ( x .- C ) ) ) ) -> x =/= C )
69 68 necomd 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ y e. P ) /\ <" A B x "> ( cgrG ` G ) <" D E y "> ) /\ q e. P ) /\ ( ( D L E ) ( perpG ` G ) ( q L y ) /\ q ( ( hpG ` G ) ` ( D L E ) ) F ) ) /\ ( f e. P /\ ( f ( K ` y ) q /\ ( y .- f ) = ( x .- C ) ) ) ) -> C =/= x )
70 1 3 4 20 28 48 69 tglinecom 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ y e. P ) /\ <" A B x "> ( cgrG ` G ) <" D E y "> ) /\ q e. P ) /\ ( ( D L E ) ( perpG ` G ) ( q L y ) /\ q ( ( hpG ` G ) ` ( D L E ) ) F ) ) /\ ( f e. P /\ ( f ( K ` y ) q /\ ( y .- f ) = ( x .- C ) ) ) ) -> ( C L x ) = ( x L C ) )
71 59 54 70 3brtr3d 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ y e. P ) /\ <" A B x "> ( cgrG ` G ) <" D E y "> ) /\ q e. P ) /\ ( ( D L E ) ( perpG ` G ) ( q L y ) /\ q ( ( hpG ` G ) ` ( D L E ) ) F ) ) /\ ( f e. P /\ ( f ( K ` y ) q /\ ( y .- f ) = ( x .- C ) ) ) ) -> ( B L A ) ( perpG ` G ) ( x L C ) )
72 1 2 3 4 20 26 23 55 28 71 perprag 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ y e. P ) /\ <" A B x "> ( cgrG ` G ) <" D E y "> ) /\ q e. P ) /\ ( ( D L E ) ( perpG ` G ) ( q L y ) /\ q ( ( hpG ` G ) ` ( D L E ) ) F ) ) /\ ( f e. P /\ ( f ( K ` y ) q /\ ( y .- f ) = ( x .- C ) ) ) ) -> <" B x C "> e. ( raG ` G ) )
73 1 3 4 6 10 11 12 14 ncolne1 
 |-  ( ph -> D =/= E )
74 73 necomd 
 |-  ( ph -> E =/= D )
75 74 ad7antr 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ y e. P ) /\ <" A B x "> ( cgrG ` G ) <" D E y "> ) /\ q e. P ) /\ ( ( D L E ) ( perpG ` G ) ( q L y ) /\ q ( ( hpG ` G ) ` ( D L E ) ) F ) ) /\ ( f e. P /\ ( f ( K ` y ) q /\ ( y .- f ) = ( x .- C ) ) ) ) -> E =/= D )
76 73 ad4antr 
 |-  ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ y e. P ) /\ <" A B x "> ( cgrG ` G ) <" D E y "> ) -> D =/= E )
77 76 neneqd 
 |-  ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ y e. P ) /\ <" A B x "> ( cgrG ` G ) <" D E y "> ) -> -. D = E )
78 44 orcd 
 |-  ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) -> ( x e. ( A L B ) \/ A = B ) )
79 1 4 3 17 21 24 45 78 colrot2 
 |-  ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) -> ( B e. ( x L A ) \/ x = A ) )
80 1 4 3 17 45 21 24 79 colcom 
 |-  ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) -> ( B e. ( A L x ) \/ A = x ) )
81 80 ad2antrr 
 |-  ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ y e. P ) /\ <" A B x "> ( cgrG ` G ) <" D E y "> ) -> ( B e. ( A L x ) \/ A = x ) )
82 simpr 
 |-  ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ y e. P ) /\ <" A B x "> ( cgrG ` G ) <" D E y "> ) -> <" A B x "> ( cgrG ` G ) <" D E y "> )
83 1 4 3 18 22 25 46 16 30 33 49 81 82 lnxfr 
 |-  ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ y e. P ) /\ <" A B x "> ( cgrG ` G ) <" D E y "> ) -> ( E e. ( D L y ) \/ D = y ) )
84 1 4 3 18 30 49 33 83 colrot2 
 |-  ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ y e. P ) /\ <" A B x "> ( cgrG ` G ) <" D E y "> ) -> ( y e. ( E L D ) \/ E = D ) )
85 1 4 3 18 33 30 49 84 colcom 
 |-  ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ y e. P ) /\ <" A B x "> ( cgrG ` G ) <" D E y "> ) -> ( y e. ( D L E ) \/ D = E ) )
86 85 orcomd 
 |-  ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ y e. P ) /\ <" A B x "> ( cgrG ` G ) <" D E y "> ) -> ( D = E \/ y e. ( D L E ) ) )
87 86 ord 
 |-  ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ y e. P ) /\ <" A B x "> ( cgrG ` G ) <" D E y "> ) -> ( -. D = E -> y e. ( D L E ) ) )
88 77 87 mpd 
 |-  ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ y e. P ) /\ <" A B x "> ( cgrG ` G ) <" D E y "> ) -> y e. ( D L E ) )
89 88 ad3antrrr 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ y e. P ) /\ <" A B x "> ( cgrG ` G ) <" D E y "> ) /\ q e. P ) /\ ( ( D L E ) ( perpG ` G ) ( q L y ) /\ q ( ( hpG ` G ) ` ( D L E ) ) F ) ) /\ ( f e. P /\ ( f ( K ` y ) q /\ ( y .- f ) = ( x .- C ) ) ) ) -> y e. ( D L E ) )
90 1 3 4 20 34 31 51 75 89 lncom 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ y e. P ) /\ <" A B x "> ( cgrG ` G ) <" D E y "> ) /\ q e. P ) /\ ( ( D L E ) ( perpG ` G ) ( q L y ) /\ q ( ( hpG ` G ) ` ( D L E ) ) F ) ) /\ ( f e. P /\ ( f ( K ` y ) q /\ ( y .- f ) = ( x .- C ) ) ) ) -> y e. ( E L D ) )
91 simprrr 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ y e. P ) /\ <" A B x "> ( cgrG ` G ) <" D E y "> ) /\ q e. P ) /\ ( ( D L E ) ( perpG ` G ) ( q L y ) /\ q ( ( hpG ` G ) ` ( D L E ) ) F ) ) /\ ( f e. P /\ ( f ( K ` y ) q /\ ( y .- f ) = ( x .- C ) ) ) ) -> ( y .- f ) = ( x .- C ) )
92 91 eqcomd 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ y e. P ) /\ <" A B x "> ( cgrG ` G ) <" D E y "> ) /\ q e. P ) /\ ( ( D L E ) ( perpG ` G ) ( q L y ) /\ q ( ( hpG ` G ) ` ( D L E ) ) F ) ) /\ ( f e. P /\ ( f ( K ` y ) q /\ ( y .- f ) = ( x .- C ) ) ) ) -> ( x .- C ) = ( y .- f ) )
93 1 2 3 20 48 28 51 35 92 68 tgcgrneq 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ y e. P ) /\ <" A B x "> ( cgrG ` G ) <" D E y "> ) /\ q e. P ) /\ ( ( D L E ) ( perpG ` G ) ( q L y ) /\ q ( ( hpG ` G ) ` ( D L E ) ) F ) ) /\ ( f e. P /\ ( f ( K ` y ) q /\ ( y .- f ) = ( x .- C ) ) ) ) -> y =/= f )
94 1 3 4 20 51 35 93 tgelrnln 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ y e. P ) /\ <" A B x "> ( cgrG ` G ) <" D E y "> ) /\ q e. P ) /\ ( ( D L E ) ( perpG ` G ) ( q L y ) /\ q ( ( hpG ` G ) ` ( D L E ) ) F ) ) /\ ( f e. P /\ ( f ( K ` y ) q /\ ( y .- f ) = ( x .- C ) ) ) ) -> ( y L f ) e. ran L )
95 1 3 4 20 34 31 75 tgelrnln 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ y e. P ) /\ <" A B x "> ( cgrG ` G ) <" D E y "> ) /\ q e. P ) /\ ( ( D L E ) ( perpG ` G ) ( q L y ) /\ q ( ( hpG ` G ) ` ( D L E ) ) F ) ) /\ ( f e. P /\ ( f ( K ` y ) q /\ ( y .- f ) = ( x .- C ) ) ) ) -> ( E L D ) e. ran L )
96 simpllr 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ y e. P ) /\ <" A B x "> ( cgrG ` G ) <" D E y "> ) /\ q e. P ) /\ ( ( D L E ) ( perpG ` G ) ( q L y ) /\ q ( ( hpG ` G ) ` ( D L E ) ) F ) ) /\ ( f e. P /\ ( f ( K ` y ) q /\ ( y .- f ) = ( x .- C ) ) ) ) -> q e. P )
97 simplr 
 |-  ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ y e. P ) /\ <" A B x "> ( cgrG ` G ) <" D E y "> ) /\ q e. P ) /\ ( ( D L E ) ( perpG ` G ) ( q L y ) /\ q ( ( hpG ` G ) ` ( D L E ) ) F ) ) -> q e. P )
98 simprl 
 |-  ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ y e. P ) /\ <" A B x "> ( cgrG ` G ) <" D E y "> ) /\ q e. P ) /\ ( ( D L E ) ( perpG ` G ) ( q L y ) /\ q ( ( hpG ` G ) ` ( D L E ) ) F ) ) -> ( D L E ) ( perpG ` G ) ( q L y ) )
99 4 19 98 perpln2 
 |-  ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ y e. P ) /\ <" A B x "> ( cgrG ` G ) <" D E y "> ) /\ q e. P ) /\ ( ( D L E ) ( perpG ` G ) ( q L y ) /\ q ( ( hpG ` G ) ` ( D L E ) ) F ) ) -> ( q L y ) e. ran L )
100 1 3 4 19 97 50 99 tglnne 
 |-  ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ y e. P ) /\ <" A B x "> ( cgrG ` G ) <" D E y "> ) /\ q e. P ) /\ ( ( D L E ) ( perpG ` G ) ( q L y ) /\ q ( ( hpG ` G ) ` ( D L E ) ) F ) ) -> q =/= y )
101 100 adantr 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ y e. P ) /\ <" A B x "> ( cgrG ` G ) <" D E y "> ) /\ q e. P ) /\ ( ( D L E ) ( perpG ` G ) ( q L y ) /\ q ( ( hpG ` G ) ` ( D L E ) ) F ) ) /\ ( f e. P /\ ( f ( K ` y ) q /\ ( y .- f ) = ( x .- C ) ) ) ) -> q =/= y )
102 101 necomd 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ y e. P ) /\ <" A B x "> ( cgrG ` G ) <" D E y "> ) /\ q e. P ) /\ ( ( D L E ) ( perpG ` G ) ( q L y ) /\ q ( ( hpG ` G ) ` ( D L E ) ) F ) ) /\ ( f e. P /\ ( f ( K ` y ) q /\ ( y .- f ) = ( x .- C ) ) ) ) -> y =/= q )
103 1 3 4 20 51 96 102 tgelrnln 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ y e. P ) /\ <" A B x "> ( cgrG ` G ) <" D E y "> ) /\ q e. P ) /\ ( ( D L E ) ( perpG ` G ) ( q L y ) /\ q ( ( hpG ` G ) ` ( D L E ) ) F ) ) /\ ( f e. P /\ ( f ( K ` y ) q /\ ( y .- f ) = ( x .- C ) ) ) ) -> ( y L q ) e. ran L )
104 98 adantr 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ y e. P ) /\ <" A B x "> ( cgrG ` G ) <" D E y "> ) /\ q e. P ) /\ ( ( D L E ) ( perpG ` G ) ( q L y ) /\ q ( ( hpG ` G ) ` ( D L E ) ) F ) ) /\ ( f e. P /\ ( f ( K ` y ) q /\ ( y .- f ) = ( x .- C ) ) ) ) -> ( D L E ) ( perpG ` G ) ( q L y ) )
105 1 3 4 20 34 31 75 tglinecom 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ y e. P ) /\ <" A B x "> ( cgrG ` G ) <" D E y "> ) /\ q e. P ) /\ ( ( D L E ) ( perpG ` G ) ( q L y ) /\ q ( ( hpG ` G ) ` ( D L E ) ) F ) ) /\ ( f e. P /\ ( f ( K ` y ) q /\ ( y .- f ) = ( x .- C ) ) ) ) -> ( E L D ) = ( D L E ) )
106 1 3 4 20 51 96 102 tglinecom 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ y e. P ) /\ <" A B x "> ( cgrG ` G ) <" D E y "> ) /\ q e. P ) /\ ( ( D L E ) ( perpG ` G ) ( q L y ) /\ q ( ( hpG ` G ) ` ( D L E ) ) F ) ) /\ ( f e. P /\ ( f ( K ` y ) q /\ ( y .- f ) = ( x .- C ) ) ) ) -> ( y L q ) = ( q L y ) )
107 104 105 106 3brtr4d 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ y e. P ) /\ <" A B x "> ( cgrG ` G ) <" D E y "> ) /\ q e. P ) /\ ( ( D L E ) ( perpG ` G ) ( q L y ) /\ q ( ( hpG ` G ) ` ( D L E ) ) F ) ) /\ ( f e. P /\ ( f ( K ` y ) q /\ ( y .- f ) = ( x .- C ) ) ) ) -> ( E L D ) ( perpG ` G ) ( y L q ) )
108 1 2 3 4 20 95 103 107 perpcom 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ y e. P ) /\ <" A B x "> ( cgrG ` G ) <" D E y "> ) /\ q e. P ) /\ ( ( D L E ) ( perpG ` G ) ( q L y ) /\ q ( ( hpG ` G ) ` ( D L E ) ) F ) ) /\ ( f e. P /\ ( f ( K ` y ) q /\ ( y .- f ) = ( x .- C ) ) ) ) -> ( y L q ) ( perpG ` G ) ( E L D ) )
109 simprrl 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ y e. P ) /\ <" A B x "> ( cgrG ` G ) <" D E y "> ) /\ q e. P ) /\ ( ( D L E ) ( perpG ` G ) ( q L y ) /\ q ( ( hpG ` G ) ` ( D L E ) ) F ) ) /\ ( f e. P /\ ( f ( K ` y ) q /\ ( y .- f ) = ( x .- C ) ) ) ) -> f ( K ` y ) q )
110 1 3 5 35 96 51 20 4 109 hlln 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ y e. P ) /\ <" A B x "> ( cgrG ` G ) <" D E y "> ) /\ q e. P ) /\ ( ( D L E ) ( perpG ` G ) ( q L y ) /\ q ( ( hpG ` G ) ` ( D L E ) ) F ) ) /\ ( f e. P /\ ( f ( K ` y ) q /\ ( y .- f ) = ( x .- C ) ) ) ) -> f e. ( q L y ) )
111 1 3 4 20 51 96 35 102 110 lncom 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ y e. P ) /\ <" A B x "> ( cgrG ` G ) <" D E y "> ) /\ q e. P ) /\ ( ( D L E ) ( perpG ` G ) ( q L y ) /\ q ( ( hpG ` G ) ` ( D L E ) ) F ) ) /\ ( f e. P /\ ( f ( K ` y ) q /\ ( y .- f ) = ( x .- C ) ) ) ) -> f e. ( y L q ) )
112 111 orcd 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ y e. P ) /\ <" A B x "> ( cgrG ` G ) <" D E y "> ) /\ q e. P ) /\ ( ( D L E ) ( perpG ` G ) ( q L y ) /\ q ( ( hpG ` G ) ` ( D L E ) ) F ) ) /\ ( f e. P /\ ( f ( K ` y ) q /\ ( y .- f ) = ( x .- C ) ) ) ) -> ( f e. ( y L q ) \/ y = q ) )
113 1 2 3 4 20 51 96 35 108 112 93 colperp 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ y e. P ) /\ <" A B x "> ( cgrG ` G ) <" D E y "> ) /\ q e. P ) /\ ( ( D L E ) ( perpG ` G ) ( q L y ) /\ q ( ( hpG ` G ) ` ( D L E ) ) F ) ) /\ ( f e. P /\ ( f ( K ` y ) q /\ ( y .- f ) = ( x .- C ) ) ) ) -> ( y L f ) ( perpG ` G ) ( E L D ) )
114 1 2 3 4 20 94 95 113 perpcom 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ y e. P ) /\ <" A B x "> ( cgrG ` G ) <" D E y "> ) /\ q e. P ) /\ ( ( D L E ) ( perpG ` G ) ( q L y ) /\ q ( ( hpG ` G ) ` ( D L E ) ) F ) ) /\ ( f e. P /\ ( f ( K ` y ) q /\ ( y .- f ) = ( x .- C ) ) ) ) -> ( E L D ) ( perpG ` G ) ( y L f ) )
115 1 2 3 4 20 34 31 90 35 114 perprag 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ y e. P ) /\ <" A B x "> ( cgrG ` G ) <" D E y "> ) /\ q e. P ) /\ ( ( D L E ) ( perpG ` G ) ( q L y ) /\ q ( ( hpG ` G ) ` ( D L E ) ) F ) ) /\ ( f e. P /\ ( f ( K ` y ) q /\ ( y .- f ) = ( x .- C ) ) ) ) -> <" E y f "> e. ( raG ` G ) )
116 82 ad3antrrr 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ y e. P ) /\ <" A B x "> ( cgrG ` G ) <" D E y "> ) /\ q e. P ) /\ ( ( D L E ) ( perpG ` G ) ( q L y ) /\ q ( ( hpG ` G ) ` ( D L E ) ) F ) ) /\ ( f e. P /\ ( f ( K ` y ) q /\ ( y .- f ) = ( x .- C ) ) ) ) -> <" A B x "> ( cgrG ` G ) <" D E y "> )
117 1 2 3 16 20 23 26 48 31 34 51 116 cgr3simp2 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ y e. P ) /\ <" A B x "> ( cgrG ` G ) <" D E y "> ) /\ q e. P ) /\ ( ( D L E ) ( perpG ` G ) ( q L y ) /\ q ( ( hpG ` G ) ` ( D L E ) ) F ) ) /\ ( f e. P /\ ( f ( K ` y ) q /\ ( y .- f ) = ( x .- C ) ) ) ) -> ( B .- x ) = ( E .- y ) )
118 1 2 3 20 40 26 48 28 34 51 35 72 115 117 92 hypcgr 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ y e. P ) /\ <" A B x "> ( cgrG ` G ) <" D E y "> ) /\ q e. P ) /\ ( ( D L E ) ( perpG ` G ) ( q L y ) /\ q ( ( hpG ` G ) ` ( D L E ) ) F ) ) /\ ( f e. P /\ ( f ( K ` y ) q /\ ( y .- f ) = ( x .- C ) ) ) ) -> ( B .- C ) = ( E .- f ) )
119 eqid 
 |-  ( pInvG ` G ) = ( pInvG ` G )
120 54 71 eqbrtrd 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ y e. P ) /\ <" A B x "> ( cgrG ` G ) <" D E y "> ) /\ q e. P ) /\ ( ( D L E ) ( perpG ` G ) ( q L y ) /\ q ( ( hpG ` G ) ` ( D L E ) ) F ) ) /\ ( f e. P /\ ( f ( K ` y ) q /\ ( y .- f ) = ( x .- C ) ) ) ) -> ( A L B ) ( perpG ` G ) ( x L C ) )
121 1 2 3 4 20 23 26 52 28 120 perprag 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ y e. P ) /\ <" A B x "> ( cgrG ` G ) <" D E y "> ) /\ q e. P ) /\ ( ( D L E ) ( perpG ` G ) ( q L y ) /\ q ( ( hpG ` G ) ` ( D L E ) ) F ) ) /\ ( f e. P /\ ( f ( K ` y ) q /\ ( y .- f ) = ( x .- C ) ) ) ) -> <" A x C "> e. ( raG ` G ) )
122 1 2 3 4 119 20 23 48 28 121 ragcom 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ y e. P ) /\ <" A B x "> ( cgrG ` G ) <" D E y "> ) /\ q e. P ) /\ ( ( D L E ) ( perpG ` G ) ( q L y ) /\ q ( ( hpG ` G ) ` ( D L E ) ) F ) ) /\ ( f e. P /\ ( f ( K ` y ) q /\ ( y .- f ) = ( x .- C ) ) ) ) -> <" C x A "> e. ( raG ` G ) )
123 105 114 eqbrtrrd 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ y e. P ) /\ <" A B x "> ( cgrG ` G ) <" D E y "> ) /\ q e. P ) /\ ( ( D L E ) ( perpG ` G ) ( q L y ) /\ q ( ( hpG ` G ) ` ( D L E ) ) F ) ) /\ ( f e. P /\ ( f ( K ` y ) q /\ ( y .- f ) = ( x .- C ) ) ) ) -> ( D L E ) ( perpG ` G ) ( y L f ) )
124 1 2 3 4 20 31 34 89 35 123 perprag 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ y e. P ) /\ <" A B x "> ( cgrG ` G ) <" D E y "> ) /\ q e. P ) /\ ( ( D L E ) ( perpG ` G ) ( q L y ) /\ q ( ( hpG ` G ) ` ( D L E ) ) F ) ) /\ ( f e. P /\ ( f ( K ` y ) q /\ ( y .- f ) = ( x .- C ) ) ) ) -> <" D y f "> e. ( raG ` G ) )
125 1 2 3 4 119 20 31 51 35 124 ragcom 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ y e. P ) /\ <" A B x "> ( cgrG ` G ) <" D E y "> ) /\ q e. P ) /\ ( ( D L E ) ( perpG ` G ) ( q L y ) /\ q ( ( hpG ` G ) ` ( D L E ) ) F ) ) /\ ( f e. P /\ ( f ( K ` y ) q /\ ( y .- f ) = ( x .- C ) ) ) ) -> <" f y D "> e. ( raG ` G ) )
126 1 2 3 20 48 28 51 35 92 tgcgrcomlr 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ y e. P ) /\ <" A B x "> ( cgrG ` G ) <" D E y "> ) /\ q e. P ) /\ ( ( D L E ) ( perpG ` G ) ( q L y ) /\ q ( ( hpG ` G ) ` ( D L E ) ) F ) ) /\ ( f e. P /\ ( f ( K ` y ) q /\ ( y .- f ) = ( x .- C ) ) ) ) -> ( C .- x ) = ( f .- y ) )
127 1 2 3 16 20 23 26 48 31 34 51 116 cgr3simp3 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ y e. P ) /\ <" A B x "> ( cgrG ` G ) <" D E y "> ) /\ q e. P ) /\ ( ( D L E ) ( perpG ` G ) ( q L y ) /\ q ( ( hpG ` G ) ` ( D L E ) ) F ) ) /\ ( f e. P /\ ( f ( K ` y ) q /\ ( y .- f ) = ( x .- C ) ) ) ) -> ( x .- A ) = ( y .- D ) )
128 1 2 3 20 40 28 48 23 35 51 31 122 125 126 127 hypcgr 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ y e. P ) /\ <" A B x "> ( cgrG ` G ) <" D E y "> ) /\ q e. P ) /\ ( ( D L E ) ( perpG ` G ) ( q L y ) /\ q ( ( hpG ` G ) ` ( D L E ) ) F ) ) /\ ( f e. P /\ ( f ( K ` y ) q /\ ( y .- f ) = ( x .- C ) ) ) ) -> ( C .- A ) = ( f .- D ) )
129 1 2 16 20 23 26 28 31 34 35 37 118 128 trgcgr 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ y e. P ) /\ <" A B x "> ( cgrG ` G ) <" D E y "> ) /\ q e. P ) /\ ( ( D L E ) ( perpG ` G ) ( q L y ) /\ q ( ( hpG ` G ) ` ( D L E ) ) F ) ) /\ ( f e. P /\ ( f ( K ` y ) q /\ ( y .- f ) = ( x .- C ) ) ) ) -> <" A B C "> ( cgrG ` G ) <" D E f "> )
130 1 3 4 6 10 11 73 tgelrnln 
 |-  ( ph -> ( D L E ) e. ran L )
131 130 ad4antr 
 |-  ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ y e. P ) /\ <" A B x "> ( cgrG ` G ) <" D E y "> ) -> ( D L E ) e. ran L )
132 131 ad3antrrr 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ y e. P ) /\ <" A B x "> ( cgrG ` G ) <" D E y "> ) /\ q e. P ) /\ ( ( D L E ) ( perpG ` G ) ( q L y ) /\ q ( ( hpG ` G ) ` ( D L E ) ) F ) ) /\ ( f e. P /\ ( f ( K ` y ) q /\ ( y .- f ) = ( x .- C ) ) ) ) -> ( D L E ) e. ran L )
133 simpl 
 |-  ( ( w = k /\ v = l ) -> w = k )
134 133 eleq1d 
 |-  ( ( w = k /\ v = l ) -> ( w e. ( P \ ( D L E ) ) <-> k e. ( P \ ( D L E ) ) ) )
135 simpr 
 |-  ( ( w = k /\ v = l ) -> v = l )
136 135 eleq1d 
 |-  ( ( w = k /\ v = l ) -> ( v e. ( P \ ( D L E ) ) <-> l e. ( P \ ( D L E ) ) ) )
137 134 136 anbi12d 
 |-  ( ( w = k /\ v = l ) -> ( ( w e. ( P \ ( D L E ) ) /\ v e. ( P \ ( D L E ) ) ) <-> ( k e. ( P \ ( D L E ) ) /\ l e. ( P \ ( D L E ) ) ) ) )
138 simpr 
 |-  ( ( ( w = k /\ v = l ) /\ z = j ) -> z = j )
139 simpll 
 |-  ( ( ( w = k /\ v = l ) /\ z = j ) -> w = k )
140 simplr 
 |-  ( ( ( w = k /\ v = l ) /\ z = j ) -> v = l )
141 139 140 oveq12d 
 |-  ( ( ( w = k /\ v = l ) /\ z = j ) -> ( w I v ) = ( k I l ) )
142 138 141 eleq12d 
 |-  ( ( ( w = k /\ v = l ) /\ z = j ) -> ( z e. ( w I v ) <-> j e. ( k I l ) ) )
143 142 cbvrexdva 
 |-  ( ( w = k /\ v = l ) -> ( E. z e. ( D L E ) z e. ( w I v ) <-> E. j e. ( D L E ) j e. ( k I l ) ) )
144 137 143 anbi12d 
 |-  ( ( w = k /\ v = l ) -> ( ( ( w e. ( P \ ( D L E ) ) /\ v e. ( P \ ( D L E ) ) ) /\ E. z e. ( D L E ) z e. ( w I v ) ) <-> ( ( k e. ( P \ ( D L E ) ) /\ l e. ( P \ ( D L E ) ) ) /\ E. j e. ( D L E ) j e. ( k I l ) ) ) )
145 144 cbvopabv 
 |-  { <. w , v >. | ( ( w e. ( P \ ( D L E ) ) /\ v e. ( P \ ( D L E ) ) ) /\ E. z e. ( D L E ) z e. ( w I v ) ) } = { <. k , l >. | ( ( k e. ( P \ ( D L E ) ) /\ l e. ( P \ ( D L E ) ) ) /\ E. j e. ( D L E ) j e. ( k I l ) ) }
146 20 adantr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ y e. P ) /\ <" A B x "> ( cgrG ` G ) <" D E y "> ) /\ q e. P ) /\ ( ( D L E ) ( perpG ` G ) ( q L y ) /\ q ( ( hpG ` G ) ` ( D L E ) ) F ) ) /\ ( f e. P /\ ( f ( K ` y ) q /\ ( y .- f ) = ( x .- C ) ) ) ) /\ f e. ( D L E ) ) -> G e. TarskiG )
147 28 adantr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ y e. P ) /\ <" A B x "> ( cgrG ` G ) <" D E y "> ) /\ q e. P ) /\ ( ( D L E ) ( perpG ` G ) ( q L y ) /\ q ( ( hpG ` G ) ` ( D L E ) ) F ) ) /\ ( f e. P /\ ( f ( K ` y ) q /\ ( y .- f ) = ( x .- C ) ) ) ) /\ f e. ( D L E ) ) -> C e. P )
148 26 adantr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ y e. P ) /\ <" A B x "> ( cgrG ` G ) <" D E y "> ) /\ q e. P ) /\ ( ( D L E ) ( perpG ` G ) ( q L y ) /\ q ( ( hpG ` G ) ` ( D L E ) ) F ) ) /\ ( f e. P /\ ( f ( K ` y ) q /\ ( y .- f ) = ( x .- C ) ) ) ) /\ f e. ( D L E ) ) -> B e. P )
149 23 adantr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ y e. P ) /\ <" A B x "> ( cgrG ` G ) <" D E y "> ) /\ q e. P ) /\ ( ( D L E ) ( perpG ` G ) ( q L y ) /\ q ( ( hpG ` G ) ` ( D L E ) ) F ) ) /\ ( f e. P /\ ( f ( K ` y ) q /\ ( y .- f ) = ( x .- C ) ) ) ) /\ f e. ( D L E ) ) -> A e. P )
150 31 adantr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ y e. P ) /\ <" A B x "> ( cgrG ` G ) <" D E y "> ) /\ q e. P ) /\ ( ( D L E ) ( perpG ` G ) ( q L y ) /\ q ( ( hpG ` G ) ` ( D L E ) ) F ) ) /\ ( f e. P /\ ( f ( K ` y ) q /\ ( y .- f ) = ( x .- C ) ) ) ) /\ f e. ( D L E ) ) -> D e. P )
151 34 adantr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ y e. P ) /\ <" A B x "> ( cgrG ` G ) <" D E y "> ) /\ q e. P ) /\ ( ( D L E ) ( perpG ` G ) ( q L y ) /\ q ( ( hpG ` G ) ` ( D L E ) ) F ) ) /\ ( f e. P /\ ( f ( K ` y ) q /\ ( y .- f ) = ( x .- C ) ) ) ) /\ f e. ( D L E ) ) -> E e. P )
152 35 adantr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ y e. P ) /\ <" A B x "> ( cgrG ` G ) <" D E y "> ) /\ q e. P ) /\ ( ( D L E ) ( perpG ` G ) ( q L y ) /\ q ( ( hpG ` G ) ` ( D L E ) ) F ) ) /\ ( f e. P /\ ( f ( K ` y ) q /\ ( y .- f ) = ( x .- C ) ) ) ) /\ f e. ( D L E ) ) -> f e. P )
153 74 ad8antr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ y e. P ) /\ <" A B x "> ( cgrG ` G ) <" D E y "> ) /\ q e. P ) /\ ( ( D L E ) ( perpG ` G ) ( q L y ) /\ q ( ( hpG ` G ) ` ( D L E ) ) F ) ) /\ ( f e. P /\ ( f ( K ` y ) q /\ ( y .- f ) = ( x .- C ) ) ) ) /\ f e. ( D L E ) ) -> E =/= D )
154 simpr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ y e. P ) /\ <" A B x "> ( cgrG ` G ) <" D E y "> ) /\ q e. P ) /\ ( ( D L E ) ( perpG ` G ) ( q L y ) /\ q ( ( hpG ` G ) ` ( D L E ) ) F ) ) /\ ( f e. P /\ ( f ( K ` y ) q /\ ( y .- f ) = ( x .- C ) ) ) ) /\ f e. ( D L E ) ) -> f e. ( D L E ) )
155 1 3 4 146 151 150 152 153 154 lncom 
 |-  ( ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ y e. P ) /\ <" A B x "> ( cgrG ` G ) <" D E y "> ) /\ q e. P ) /\ ( ( D L E ) ( perpG ` G ) ( q L y ) /\ q ( ( hpG ` G ) ` ( D L E ) ) F ) ) /\ ( f e. P /\ ( f ( K ` y ) q /\ ( y .- f ) = ( x .- C ) ) ) ) /\ f e. ( D L E ) ) -> f e. ( E L D ) )
156 155 orcd 
 |-  ( ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ y e. P ) /\ <" A B x "> ( cgrG ` G ) <" D E y "> ) /\ q e. P ) /\ ( ( D L E ) ( perpG ` G ) ( q L y ) /\ q ( ( hpG ` G ) ` ( D L E ) ) F ) ) /\ ( f e. P /\ ( f ( K ` y ) q /\ ( y .- f ) = ( x .- C ) ) ) ) /\ f e. ( D L E ) ) -> ( f e. ( E L D ) \/ E = D ) )
157 1 4 3 146 151 150 152 156 colrot1 
 |-  ( ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ y e. P ) /\ <" A B x "> ( cgrG ` G ) <" D E y "> ) /\ q e. P ) /\ ( ( D L E ) ( perpG ` G ) ( q L y ) /\ q ( ( hpG ` G ) ` ( D L E ) ) F ) ) /\ ( f e. P /\ ( f ( K ` y ) q /\ ( y .- f ) = ( x .- C ) ) ) ) /\ f e. ( D L E ) ) -> ( E e. ( D L f ) \/ D = f ) )
158 129 adantr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ y e. P ) /\ <" A B x "> ( cgrG ` G ) <" D E y "> ) /\ q e. P ) /\ ( ( D L E ) ( perpG ` G ) ( q L y ) /\ q ( ( hpG ` G ) ` ( D L E ) ) F ) ) /\ ( f e. P /\ ( f ( K ` y ) q /\ ( y .- f ) = ( x .- C ) ) ) ) /\ f e. ( D L E ) ) -> <" A B C "> ( cgrG ` G ) <" D E f "> )
159 1 2 3 16 146 149 148 147 150 151 152 158 trgcgrcom 
 |-  ( ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ y e. P ) /\ <" A B x "> ( cgrG ` G ) <" D E y "> ) /\ q e. P ) /\ ( ( D L E ) ( perpG ` G ) ( q L y ) /\ q ( ( hpG ` G ) ` ( D L E ) ) F ) ) /\ ( f e. P /\ ( f ( K ` y ) q /\ ( y .- f ) = ( x .- C ) ) ) ) /\ f e. ( D L E ) ) -> <" D E f "> ( cgrG ` G ) <" A B C "> )
160 1 4 3 146 150 151 152 16 149 148 147 157 159 lnxfr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ y e. P ) /\ <" A B x "> ( cgrG ` G ) <" D E y "> ) /\ q e. P ) /\ ( ( D L E ) ( perpG ` G ) ( q L y ) /\ q ( ( hpG ` G ) ` ( D L E ) ) F ) ) /\ ( f e. P /\ ( f ( K ` y ) q /\ ( y .- f ) = ( x .- C ) ) ) ) /\ f e. ( D L E ) ) -> ( B e. ( A L C ) \/ A = C ) )
161 1 4 3 146 149 147 148 160 colrot1 
 |-  ( ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ y e. P ) /\ <" A B x "> ( cgrG ` G ) <" D E y "> ) /\ q e. P ) /\ ( ( D L E ) ( perpG ` G ) ( q L y ) /\ q ( ( hpG ` G ) ` ( D L E ) ) F ) ) /\ ( f e. P /\ ( f ( K ` y ) q /\ ( y .- f ) = ( x .- C ) ) ) ) /\ f e. ( D L E ) ) -> ( A e. ( C L B ) \/ C = B ) )
162 1 4 3 146 147 148 149 161 colcom 
 |-  ( ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ y e. P ) /\ <" A B x "> ( cgrG ` G ) <" D E y "> ) /\ q e. P ) /\ ( ( D L E ) ( perpG ` G ) ( q L y ) /\ q ( ( hpG ` G ) ` ( D L E ) ) F ) ) /\ ( f e. P /\ ( f ( K ` y ) q /\ ( y .- f ) = ( x .- C ) ) ) ) /\ f e. ( D L E ) ) -> ( A e. ( B L C ) \/ B = C ) )
163 13 ad8antr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ y e. P ) /\ <" A B x "> ( cgrG ` G ) <" D E y "> ) /\ q e. P ) /\ ( ( D L E ) ( perpG ` G ) ( q L y ) /\ q ( ( hpG ` G ) ` ( D L E ) ) F ) ) /\ ( f e. P /\ ( f ( K ` y ) q /\ ( y .- f ) = ( x .- C ) ) ) ) /\ f e. ( D L E ) ) -> -. ( A e. ( B L C ) \/ B = C ) )
164 162 163 pm2.65da 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ y e. P ) /\ <" A B x "> ( cgrG ` G ) <" D E y "> ) /\ q e. P ) /\ ( ( D L E ) ( perpG ` G ) ( q L y ) /\ q ( ( hpG ` G ) ` ( D L E ) ) F ) ) /\ ( f e. P /\ ( f ( K ` y ) q /\ ( y .- f ) = ( x .- C ) ) ) ) -> -. f e. ( D L E ) )
165 1 3 4 20 132 51 145 5 89 35 96 164 109 hphl 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ y e. P ) /\ <" A B x "> ( cgrG ` G ) <" D E y "> ) /\ q e. P ) /\ ( ( D L E ) ( perpG ` G ) ( q L y ) /\ q ( ( hpG ` G ) ` ( D L E ) ) F ) ) /\ ( f e. P /\ ( f ( K ` y ) q /\ ( y .- f ) = ( x .- C ) ) ) ) -> f ( ( hpG ` G ) ` ( D L E ) ) q )
166 12 ad4antr 
 |-  ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ y e. P ) /\ <" A B x "> ( cgrG ` G ) <" D E y "> ) -> F e. P )
167 166 ad2antrr 
 |-  ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ y e. P ) /\ <" A B x "> ( cgrG ` G ) <" D E y "> ) /\ q e. P ) /\ ( ( D L E ) ( perpG ` G ) ( q L y ) /\ q ( ( hpG ` G ) ` ( D L E ) ) F ) ) -> F e. P )
168 167 adantr 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ y e. P ) /\ <" A B x "> ( cgrG ` G ) <" D E y "> ) /\ q e. P ) /\ ( ( D L E ) ( perpG ` G ) ( q L y ) /\ q ( ( hpG ` G ) ` ( D L E ) ) F ) ) /\ ( f e. P /\ ( f ( K ` y ) q /\ ( y .- f ) = ( x .- C ) ) ) ) -> F e. P )
169 simplrr 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ y e. P ) /\ <" A B x "> ( cgrG ` G ) <" D E y "> ) /\ q e. P ) /\ ( ( D L E ) ( perpG ` G ) ( q L y ) /\ q ( ( hpG ` G ) ` ( D L E ) ) F ) ) /\ ( f e. P /\ ( f ( K ` y ) q /\ ( y .- f ) = ( x .- C ) ) ) ) -> q ( ( hpG ` G ) ` ( D L E ) ) F )
170 1 3 4 20 132 35 145 96 165 168 169 hpgtr 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ y e. P ) /\ <" A B x "> ( cgrG ` G ) <" D E y "> ) /\ q e. P ) /\ ( ( D L E ) ( perpG ` G ) ( q L y ) /\ q ( ( hpG ` G ) ` ( D L E ) ) F ) ) /\ ( f e. P /\ ( f ( K ` y ) q /\ ( y .- f ) = ( x .- C ) ) ) ) -> f ( ( hpG ` G ) ` ( D L E ) ) F )
171 129 170 jca 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ y e. P ) /\ <" A B x "> ( cgrG ` G ) <" D E y "> ) /\ q e. P ) /\ ( ( D L E ) ( perpG ` G ) ( q L y ) /\ q ( ( hpG ` G ) ` ( D L E ) ) F ) ) /\ ( f e. P /\ ( f ( K ` y ) q /\ ( y .- f ) = ( x .- C ) ) ) ) -> ( <" A B C "> ( cgrG ` G ) <" D E f "> /\ f ( ( hpG ` G ) ` ( D L E ) ) F ) )
172 1 3 5 50 47 27 19 97 2 100 67 hlcgrex 
 |-  ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ y e. P ) /\ <" A B x "> ( cgrG ` G ) <" D E y "> ) /\ q e. P ) /\ ( ( D L E ) ( perpG ` G ) ( q L y ) /\ q ( ( hpG ` G ) ` ( D L E ) ) F ) ) -> E. f e. P ( f ( K ` y ) q /\ ( y .- f ) = ( x .- C ) ) )
173 171 172 reximddv 
 |-  ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ y e. P ) /\ <" A B x "> ( cgrG ` G ) <" D E y "> ) /\ q e. P ) /\ ( ( D L E ) ( perpG ` G ) ( q L y ) /\ q ( ( hpG ` G ) ` ( D L E ) ) F ) ) -> E. f e. P ( <" A B C "> ( cgrG ` G ) <" D E f "> /\ f ( ( hpG ` G ) ` ( D L E ) ) F ) )
174 1 4 3 6 11 12 10 14 ncolrot2 
 |-  ( ph -> -. ( F e. ( D L E ) \/ D = E ) )
175 ioran 
 |-  ( -. ( F e. ( D L E ) \/ D = E ) <-> ( -. F e. ( D L E ) /\ -. D = E ) )
176 174 175 sylib 
 |-  ( ph -> ( -. F e. ( D L E ) /\ -. D = E ) )
177 176 simpld 
 |-  ( ph -> -. F e. ( D L E ) )
178 177 ad4antr 
 |-  ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ y e. P ) /\ <" A B x "> ( cgrG ` G ) <" D E y "> ) -> -. F e. ( D L E ) )
179 1 2 3 4 18 39 131 145 88 166 178 lnperpex 
 |-  ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ y e. P ) /\ <" A B x "> ( cgrG ` G ) <" D E y "> ) -> E. q e. P ( ( D L E ) ( perpG ` G ) ( q L y ) /\ q ( ( hpG ` G ) ` ( D L E ) ) F ) )
180 173 179 r19.29a 
 |-  ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) /\ y e. P ) /\ <" A B x "> ( cgrG ` G ) <" D E y "> ) -> E. f e. P ( <" A B C "> ( cgrG ` G ) <" D E f "> /\ f ( ( hpG ` G ) ` ( D L E ) ) F ) )
181 1 4 3 17 21 24 45 16 29 32 2 80 36 lnext 
 |-  ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) -> E. y e. P <" A B x "> ( cgrG ` G ) <" D E y "> )
182 180 181 r19.29a 
 |-  ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) ( perpG ` G ) ( A L B ) ) -> E. f e. P ( <" A B C "> ( cgrG ` G ) <" D E f "> /\ f ( ( hpG ` G ) ` ( D L E ) ) F ) )
183 1 2 3 4 6 42 9 63 footex 
 |-  ( ph -> E. x e. ( A L B ) ( C L x ) ( perpG ` G ) ( A L B ) )
184 182 183 r19.29a 
 |-  ( ph -> E. f e. P ( <" A B C "> ( cgrG ` G ) <" D E f "> /\ f ( ( hpG ` G ) ` ( D L E ) ) F ) )