MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  trgcopy Structured version   Unicode version

Theorem trgcopy 24838
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.)
Hypotheses
Ref Expression
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
Ref Expression
trgcopy  |-  ( ph  ->  E. f  e.  P  ( <" A B C "> (cgrG `  G ) <" D E f ">  /\  f ( (hpG `  G ) `  ( D L E ) ) F ) )
Distinct variable groups:    .- , f    A, f    B, f    C, f    D, f    f, E    f, F    f, G    f, I    f, L    P, f    ph, f    f, K

Proof of Theorem trgcopy
Dummy variables  j 
k  l  q  v  w  x  y  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 trgcopy.p . . . . . . 7  |-  P  =  ( Base `  G
)
2 trgcopy.m . . . . . . 7  |-  .-  =  ( dist `  G )
3 eqid 2423 . . . . . . 7  |-  (cgrG `  G )  =  (cgrG `  G )
4 trgcopy.g . . . . . . . . . . 11  |-  ( ph  ->  G  e. TarskiG )
54ad2antrr 731 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G ) ( A L B ) )  ->  G  e. TarskiG )
65ad2antrr 731 . . . . . . . . 9  |-  ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G
) ( A L B ) )  /\  y  e.  P )  /\  <" A B x "> (cgrG `  G ) <" D E y "> )  ->  G  e. TarskiG )
76ad2antrr 731 . . . . . . . 8  |-  ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G ) ( A L B ) )  /\  y  e.  P
)  /\  <" A B x "> (cgrG `  G ) <" D E y "> )  /\  q  e.  P )  /\  ( ( D L E ) (⟂G `  G
) ( q L y )  /\  q
( (hpG `  G
) `  ( D L E ) ) F ) )  ->  G  e. TarskiG )
87adantr 467 . . . . . . 7  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  y  e.  P )  /\  <" A B x "> (cgrG `  G
) <" D E y "> )  /\  q  e.  P
)  /\  ( ( D L E ) (⟂G `  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 )
9 trgcopy.a . . . . . . . . . 10  |-  ( ph  ->  A  e.  P )
109ad2antrr 731 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G ) ( A L B ) )  ->  A  e.  P
)
1110ad2antrr 731 . . . . . . . 8  |-  ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G
) ( A L B ) )  /\  y  e.  P )  /\  <" A B x "> (cgrG `  G ) <" D E y "> )  ->  A  e.  P
)
1211ad3antrrr 735 . . . . . . 7  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  y  e.  P )  /\  <" A B x "> (cgrG `  G
) <" D E y "> )  /\  q  e.  P
)  /\  ( ( D L E ) (⟂G `  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 )
13 trgcopy.b . . . . . . . . . 10  |-  ( ph  ->  B  e.  P )
1413ad2antrr 731 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G ) ( A L B ) )  ->  B  e.  P
)
1514ad2antrr 731 . . . . . . . 8  |-  ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G
) ( A L B ) )  /\  y  e.  P )  /\  <" A B x "> (cgrG `  G ) <" D E y "> )  ->  B  e.  P
)
1615ad3antrrr 735 . . . . . . 7  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  y  e.  P )  /\  <" A B x "> (cgrG `  G
) <" D E y "> )  /\  q  e.  P
)  /\  ( ( D L E ) (⟂G `  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 )
17 trgcopy.c . . . . . . . . 9  |-  ( ph  ->  C  e.  P )
1817ad6antr 741 . . . . . . . 8  |-  ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G ) ( A L B ) )  /\  y  e.  P
)  /\  <" A B x "> (cgrG `  G ) <" D E y "> )  /\  q  e.  P )  /\  ( ( D L E ) (⟂G `  G
) ( q L y )  /\  q
( (hpG `  G
) `  ( D L E ) ) F ) )  ->  C  e.  P )
1918adantr 467 . . . . . . 7  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  y  e.  P )  /\  <" A B x "> (cgrG `  G
) <" D E y "> )  /\  q  e.  P
)  /\  ( ( D L E ) (⟂G `  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 )
20 trgcopy.d . . . . . . . . . 10  |-  ( ph  ->  D  e.  P )
2120ad2antrr 731 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G ) ( A L B ) )  ->  D  e.  P
)
2221ad2antrr 731 . . . . . . . 8  |-  ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G
) ( A L B ) )  /\  y  e.  P )  /\  <" A B x "> (cgrG `  G ) <" D E y "> )  ->  D  e.  P
)
2322ad3antrrr 735 . . . . . . 7  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  y  e.  P )  /\  <" A B x "> (cgrG `  G
) <" D E y "> )  /\  q  e.  P
)  /\  ( ( D L E ) (⟂G `  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 )
24 trgcopy.e . . . . . . . . . 10  |-  ( ph  ->  E  e.  P )
2524ad2antrr 731 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G ) ( A L B ) )  ->  E  e.  P
)
2625ad2antrr 731 . . . . . . . 8  |-  ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G
) ( A L B ) )  /\  y  e.  P )  /\  <" A B x "> (cgrG `  G ) <" D E y "> )  ->  E  e.  P
)
2726ad3antrrr 735 . . . . . . 7  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  y  e.  P )  /\  <" A B x "> (cgrG `  G
) <" D E y "> )  /\  q  e.  P
)  /\  ( ( D L E ) (⟂G `  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 )
28 simprl 763 . . . . . . 7  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  y  e.  P )  /\  <" A B x "> (cgrG `  G
) <" D E y "> )  /\  q  e.  P
)  /\  ( ( D L E ) (⟂G `  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 )
29 trgcopy.3 . . . . . . . . 9  |-  ( ph  ->  ( A  .-  B
)  =  ( D 
.-  E ) )
3029ad2antrr 731 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G ) ( A L B ) )  ->  ( A  .-  B )  =  ( D  .-  E ) )
3130ad5antr 739 . . . . . . 7  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  y  e.  P )  /\  <" A B x "> (cgrG `  G
) <" D E y "> )  /\  q  e.  P
)  /\  ( ( D L E ) (⟂G `  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 ) )
32 trgcopy.i . . . . . . . 8  |-  I  =  (Itv `  G )
33 trgcopy.l . . . . . . . . . . 11  |-  L  =  (LineG `  G )
34 trgcopy.1 . . . . . . . . . . 11  |-  ( ph  ->  -.  ( A  e.  ( B L C )  \/  B  =  C ) )
351, 33, 32, 4, 13, 17, 9, 34ncoltgdim2 24602 . . . . . . . . . 10  |-  ( ph  ->  GDimTarskiG 2 )
3635ad4antr 737 . . . . . . . . 9  |-  ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G
) ( A L B ) )  /\  y  e.  P )  /\  <" A B x "> (cgrG `  G ) <" D E y "> )  ->  GDimTarskiG 2 )
3736ad3antrrr 735 . . . . . . . 8  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  y  e.  P )  /\  <" A B x "> (cgrG `  G
) <" D E y "> )  /\  q  e.  P
)  /\  ( ( D L E ) (⟂G `  G ) ( q L y )  /\  q ( (hpG `  G ) `  ( D L E ) ) F ) )  /\  ( f  e.  P  /\  ( f ( K `
 y ) q  /\  ( y  .-  f )  =  ( x  .-  C ) ) ) )  ->  GDimTarskiG 2 )
381, 32, 33, 4, 9, 13, 17, 34ncolne1 24662 . . . . . . . . . . . . . 14  |-  ( ph  ->  A  =/=  B )
391, 32, 33, 4, 9, 13, 38tgelrnln 24667 . . . . . . . . . . . . 13  |-  ( ph  ->  ( A L B )  e.  ran  L
)
4039ad2antrr 731 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G ) ( A L B ) )  ->  ( A L B )  e.  ran  L )
41 simplr 761 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G ) ( A L B ) )  ->  x  e.  ( A L B ) )
421, 33, 32, 5, 40, 41tglnpt 24586 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G ) ( A L B ) )  ->  x  e.  P
)
4342ad2antrr 731 . . . . . . . . . 10  |-  ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G
) ( A L B ) )  /\  y  e.  P )  /\  <" A B x "> (cgrG `  G ) <" D E y "> )  ->  x  e.  P
)
4443ad2antrr 731 . . . . . . . . 9  |-  ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G ) ( A L B ) )  /\  y  e.  P
)  /\  <" A B x "> (cgrG `  G ) <" D E y "> )  /\  q  e.  P )  /\  ( ( D L E ) (⟂G `  G
) ( q L y )  /\  q
( (hpG `  G
) `  ( D L E ) ) F ) )  ->  x  e.  P )
4544adantr 467 . . . . . . . 8  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  y  e.  P )  /\  <" A B x "> (cgrG `  G
) <" D E y "> )  /\  q  e.  P
)  /\  ( ( D L E ) (⟂G `  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 )
46 simplr 761 . . . . . . . . . 10  |-  ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G
) ( A L B ) )  /\  y  e.  P )  /\  <" A B x "> (cgrG `  G ) <" D E y "> )  ->  y  e.  P
)
4746ad2antrr 731 . . . . . . . . 9  |-  ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G ) ( A L B ) )  /\  y  e.  P
)  /\  <" A B x "> (cgrG `  G ) <" D E y "> )  /\  q  e.  P )  /\  ( ( D L E ) (⟂G `  G
) ( q L y )  /\  q
( (hpG `  G
) `  ( D L E ) ) F ) )  ->  y  e.  P )
4847adantr 467 . . . . . . . 8  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  y  e.  P )  /\  <" A B x "> (cgrG `  G
) <" D E y "> )  /\  q  e.  P
)  /\  ( ( D L E ) (⟂G `  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 )
4941ad5antr 739 . . . . . . . . . 10  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  y  e.  P )  /\  <" A B x "> (cgrG `  G
) <" D E y "> )  /\  q  e.  P
)  /\  ( ( D L E ) (⟂G `  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 ) )
5038ad7antr 743 . . . . . . . . . . 11  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  y  e.  P )  /\  <" A B x "> (cgrG `  G
) <" D E y "> )  /\  q  e.  P
)  /\  ( ( D L E ) (⟂G `  G ) ( q L y )  /\  q ( (hpG `  G ) `  ( D L E ) ) F ) )  /\  ( f  e.  P  /\  ( f ( K `
 y ) q  /\  ( y  .-  f )  =  ( x  .-  C ) ) ) )  ->  A  =/=  B )
511, 32, 33, 8, 12, 16, 50tglinecom 24672 . . . . . . . . . 10  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  y  e.  P )  /\  <" A B x "> (cgrG `  G
) <" D E y "> )  /\  q  e.  P
)  /\  ( ( D L E ) (⟂G `  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 ) )
5249, 51eleqtrd 2513 . . . . . . . . 9  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  y  e.  P )  /\  <" A B x "> (cgrG `  G
) <" D E y "> )  /\  q  e.  P
)  /\  ( ( D L E ) (⟂G `  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 ) )
53 simp-6r 780 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  y  e.  P )  /\  <" A B x "> (cgrG `  G
) <" D E y "> )  /\  q  e.  P
)  /\  ( ( D L E ) (⟂G `  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 ) (⟂G `  G
) ( A L B ) )
5433, 8, 53perpln1 24747 . . . . . . . . . . 11  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  y  e.  P )  /\  <" A B x "> (cgrG `  G
) <" D E y "> )  /\  q  e.  P
)  /\  ( ( D L E ) (⟂G `  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
)
5540ad5antr 739 . . . . . . . . . . 11  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  y  e.  P )  /\  <" A B x "> (cgrG `  G
) <" D E y "> )  /\  q  e.  P
)  /\  ( ( D L E ) (⟂G `  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
)
561, 2, 32, 33, 8, 54, 55, 53perpcom 24750 . . . . . . . . . 10  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  y  e.  P )  /\  <" A B x "> (cgrG `  G
) <" D E y "> )  /\  q  e.  P
)  /\  ( ( D L E ) (⟂G `  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 ) (⟂G `  G
) ( C L x ) )
571, 33, 32, 4, 13, 17, 9, 34ncolrot2 24600 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  -.  ( C  e.  ( A L B )  \/  A  =  B ) )
58 ioran 493 . . . . . . . . . . . . . . . . . 18  |-  ( -.  ( C  e.  ( A L B )  \/  A  =  B )  <->  ( -.  C  e.  ( A L B )  /\  -.  A  =  B ) )
5957, 58sylib 200 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( -.  C  e.  ( A L B )  /\  -.  A  =  B ) )
6059simpld 461 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  -.  C  e.  ( A L B ) )
6160ad2antrr 731 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G ) ( A L B ) )  ->  -.  C  e.  ( A L B ) )
62 nelne2 2755 . . . . . . . . . . . . . . 15  |-  ( ( x  e.  ( A L B )  /\  -.  C  e.  ( A L B ) )  ->  x  =/=  C
)
6341, 61, 62syl2anc 666 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G ) ( A L B ) )  ->  x  =/=  C
)
6463ad4antr 737 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G ) ( A L B ) )  /\  y  e.  P
)  /\  <" A B x "> (cgrG `  G ) <" D E y "> )  /\  q  e.  P )  /\  ( ( D L E ) (⟂G `  G
) ( q L y )  /\  q
( (hpG `  G
) `  ( D L E ) ) F ) )  ->  x  =/=  C )
6564adantr 467 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  y  e.  P )  /\  <" A B x "> (cgrG `  G
) <" D E y "> )  /\  q  e.  P
)  /\  ( ( D L E ) (⟂G `  G ) ( q L y )  /\  q ( (hpG `  G ) `  ( D L E ) ) F ) )  /\  ( f  e.  P  /\  ( f ( K `
 y ) q  /\  ( y  .-  f )  =  ( x  .-  C ) ) ) )  ->  x  =/=  C )
6665necomd 2696 . . . . . . . . . . 11  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  y  e.  P )  /\  <" A B x "> (cgrG `  G
) <" D E y "> )  /\  q  e.  P
)  /\  ( ( D L E ) (⟂G `  G ) ( q L y )  /\  q ( (hpG `  G ) `  ( D L E ) ) F ) )  /\  ( f  e.  P  /\  ( f ( K `
 y ) q  /\  ( y  .-  f )  =  ( x  .-  C ) ) ) )  ->  C  =/=  x )
671, 32, 33, 8, 19, 45, 66tglinecom 24672 . . . . . . . . . 10  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  y  e.  P )  /\  <" A B x "> (cgrG `  G
) <" D E y "> )  /\  q  e.  P
)  /\  ( ( D L E ) (⟂G `  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 ) )
6856, 51, 673brtr3d 4451 . . . . . . . . 9  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  y  e.  P )  /\  <" A B x "> (cgrG `  G
) <" D E y "> )  /\  q  e.  P
)  /\  ( ( D L E ) (⟂G `  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 ) (⟂G `  G
) ( x L C ) )
691, 2, 32, 33, 8, 16, 12, 52, 19, 68perprag 24760 . . . . . . . 8  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  y  e.  P )  /\  <" A B x "> (cgrG `  G
) <" D E y "> )  /\  q  e.  P
)  /\  ( ( D L E ) (⟂G `  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.  (∟G `  G ) )
701, 2, 32, 4, 9, 13, 20, 24, 29, 38tgcgrneq 24519 . . . . . . . . . . . 12  |-  ( ph  ->  D  =/=  E )
7170necomd 2696 . . . . . . . . . . 11  |-  ( ph  ->  E  =/=  D )
7271ad7antr 743 . . . . . . . . . 10  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  y  e.  P )  /\  <" A B x "> (cgrG `  G
) <" D E y "> )  /\  q  e.  P
)  /\  ( ( D L E ) (⟂G `  G ) ( q L y )  /\  q ( (hpG `  G ) `  ( D L E ) ) F ) )  /\  ( f  e.  P  /\  ( f ( K `
 y ) q  /\  ( y  .-  f )  =  ( x  .-  C ) ) ) )  ->  E  =/=  D )
7370ad4antr 737 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G
) ( A L B ) )  /\  y  e.  P )  /\  <" A B x "> (cgrG `  G ) <" D E y "> )  ->  D  =/=  E
)
7473neneqd 2626 . . . . . . . . . . . 12  |-  ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G
) ( A L B ) )  /\  y  e.  P )  /\  <" A B x "> (cgrG `  G ) <" D E y "> )  ->  -.  D  =  E )
7541orcd 394 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G ) ( A L B ) )  ->  ( x  e.  ( A L B )  \/  A  =  B ) )
761, 33, 32, 5, 10, 14, 42, 75colrot2 24597 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G ) ( A L B ) )  ->  ( B  e.  ( x L A )  \/  x  =  A ) )
771, 33, 32, 5, 42, 10, 14, 76colcom 24595 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G ) ( A L B ) )  ->  ( B  e.  ( A L x )  \/  A  =  x ) )
7877ad2antrr 731 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G
) ( A L B ) )  /\  y  e.  P )  /\  <" A B x "> (cgrG `  G ) <" D E y "> )  ->  ( B  e.  ( A L x )  \/  A  =  x ) )
79 simpr 463 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G
) ( A L B ) )  /\  y  e.  P )  /\  <" A B x "> (cgrG `  G ) <" D E y "> )  ->  <" A B x "> (cgrG `  G ) <" D E y "> )
801, 33, 32, 6, 11, 15, 43, 3, 22, 26, 46, 78, 79lnxfr 24603 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G
) ( A L B ) )  /\  y  e.  P )  /\  <" A B x "> (cgrG `  G ) <" D E y "> )  ->  ( E  e.  ( D L y )  \/  D  =  y ) )
811, 33, 32, 6, 22, 46, 26, 80colrot2 24597 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G
) ( A L B ) )  /\  y  e.  P )  /\  <" A B x "> (cgrG `  G ) <" D E y "> )  ->  ( y  e.  ( E L D )  \/  E  =  D ) )
821, 33, 32, 6, 26, 22, 46, 81colcom 24595 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G
) ( A L B ) )  /\  y  e.  P )  /\  <" A B x "> (cgrG `  G ) <" D E y "> )  ->  ( y  e.  ( D L E )  \/  D  =  E ) )
8382orcomd 390 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G
) ( A L B ) )  /\  y  e.  P )  /\  <" A B x "> (cgrG `  G ) <" D E y "> )  ->  ( D  =  E  \/  y  e.  ( D L E ) ) )
8483ord 379 . . . . . . . . . . . 12  |-  ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G
) ( A L B ) )  /\  y  e.  P )  /\  <" A B x "> (cgrG `  G ) <" D E y "> )  ->  ( -.  D  =  E  ->  y  e.  ( D L E ) ) )
8574, 84mpd 15 . . . . . . . . . . 11  |-  ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G
) ( A L B ) )  /\  y  e.  P )  /\  <" A B x "> (cgrG `  G ) <" D E y "> )  ->  y  e.  ( D L E ) )
8685ad3antrrr 735 . . . . . . . . . 10  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  y  e.  P )  /\  <" A B x "> (cgrG `  G
) <" D E y "> )  /\  q  e.  P
)  /\  ( ( D L E ) (⟂G `  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 ) )
871, 32, 33, 8, 27, 23, 48, 72, 86lncom 24659 . . . . . . . . 9  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  y  e.  P )  /\  <" A B x "> (cgrG `  G
) <" D E y "> )  /\  q  e.  P
)  /\  ( ( D L E ) (⟂G `  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 ) )
88 simprrr 774 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  y  e.  P )  /\  <" A B x "> (cgrG `  G
) <" D E y "> )  /\  q  e.  P
)  /\  ( ( D L E ) (⟂G `  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 ) )
8988eqcomd 2431 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  y  e.  P )  /\  <" A B x "> (cgrG `  G
) <" D E y "> )  /\  q  e.  P
)  /\  ( ( D L E ) (⟂G `  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 ) )
901, 2, 32, 8, 45, 19, 48, 28, 89, 65tgcgrneq 24519 . . . . . . . . . . 11  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  y  e.  P )  /\  <" A B x "> (cgrG `  G
) <" D E y "> )  /\  q  e.  P
)  /\  ( ( D L E ) (⟂G `  G ) ( q L y )  /\  q ( (hpG `  G ) `  ( D L E ) ) F ) )  /\  ( f  e.  P  /\  ( f ( K `
 y ) q  /\  ( y  .-  f )  =  ( x  .-  C ) ) ) )  -> 
y  =/=  f )
911, 32, 33, 8, 48, 28, 90tgelrnln 24667 . . . . . . . . . 10  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  y  e.  P )  /\  <" A B x "> (cgrG `  G
) <" D E y "> )  /\  q  e.  P
)  /\  ( ( D L E ) (⟂G `  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
)
921, 32, 33, 8, 27, 23, 72tgelrnln 24667 . . . . . . . . . 10  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  y  e.  P )  /\  <" A B x "> (cgrG `  G
) <" D E y "> )  /\  q  e.  P
)  /\  ( ( D L E ) (⟂G `  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
)
93 simpllr 768 . . . . . . . . . . 11  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  y  e.  P )  /\  <" A B x "> (cgrG `  G
) <" D E y "> )  /\  q  e.  P
)  /\  ( ( D L E ) (⟂G `  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 )
94 simplr 761 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G ) ( A L B ) )  /\  y  e.  P
)  /\  <" A B x "> (cgrG `  G ) <" D E y "> )  /\  q  e.  P )  /\  ( ( D L E ) (⟂G `  G
) ( q L y )  /\  q
( (hpG `  G
) `  ( D L E ) ) F ) )  ->  q  e.  P )
95 simprl 763 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G ) ( A L B ) )  /\  y  e.  P
)  /\  <" A B x "> (cgrG `  G ) <" D E y "> )  /\  q  e.  P )  /\  ( ( D L E ) (⟂G `  G
) ( q L y )  /\  q
( (hpG `  G
) `  ( D L E ) ) F ) )  ->  ( D L E ) (⟂G `  G ) ( q L y ) )
9633, 7, 95perpln2 24748 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G ) ( A L B ) )  /\  y  e.  P
)  /\  <" A B x "> (cgrG `  G ) <" D E y "> )  /\  q  e.  P )  /\  ( ( D L E ) (⟂G `  G
) ( q L y )  /\  q
( (hpG `  G
) `  ( D L E ) ) F ) )  ->  (
q L y )  e.  ran  L )
971, 32, 33, 7, 94, 47, 96tglnne 24665 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G ) ( A L B ) )  /\  y  e.  P
)  /\  <" A B x "> (cgrG `  G ) <" D E y "> )  /\  q  e.  P )  /\  ( ( D L E ) (⟂G `  G
) ( q L y )  /\  q
( (hpG `  G
) `  ( D L E ) ) F ) )  ->  q  =/=  y )
9897adantr 467 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  y  e.  P )  /\  <" A B x "> (cgrG `  G
) <" D E y "> )  /\  q  e.  P
)  /\  ( ( D L E ) (⟂G `  G ) ( q L y )  /\  q ( (hpG `  G ) `  ( D L E ) ) F ) )  /\  ( f  e.  P  /\  ( f ( K `
 y ) q  /\  ( y  .-  f )  =  ( x  .-  C ) ) ) )  -> 
q  =/=  y )
9998necomd 2696 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  y  e.  P )  /\  <" A B x "> (cgrG `  G
) <" D E y "> )  /\  q  e.  P
)  /\  ( ( D L E ) (⟂G `  G ) ( q L y )  /\  q ( (hpG `  G ) `  ( D L E ) ) F ) )  /\  ( f  e.  P  /\  ( f ( K `
 y ) q  /\  ( y  .-  f )  =  ( x  .-  C ) ) ) )  -> 
y  =/=  q )
1001, 32, 33, 8, 48, 93, 99tgelrnln 24667 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  y  e.  P )  /\  <" A B x "> (cgrG `  G
) <" D E y "> )  /\  q  e.  P
)  /\  ( ( D L E ) (⟂G `  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
)
10195adantr 467 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  y  e.  P )  /\  <" A B x "> (cgrG `  G
) <" D E y "> )  /\  q  e.  P
)  /\  ( ( D L E ) (⟂G `  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 ) (⟂G `  G
) ( q L y ) )
1021, 32, 33, 8, 27, 23, 72tglinecom 24672 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  y  e.  P )  /\  <" A B x "> (cgrG `  G
) <" D E y "> )  /\  q  e.  P
)  /\  ( ( D L E ) (⟂G `  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 ) )
1031, 32, 33, 8, 48, 93, 100tglnne 24665 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  y  e.  P )  /\  <" A B x "> (cgrG `  G
) <" D E y "> )  /\  q  e.  P
)  /\  ( ( D L E ) (⟂G `  G ) ( q L y )  /\  q ( (hpG `  G ) `  ( D L E ) ) F ) )  /\  ( f  e.  P  /\  ( f ( K `
 y ) q  /\  ( y  .-  f )  =  ( x  .-  C ) ) ) )  -> 
y  =/=  q )
1041, 32, 33, 8, 48, 93, 103tglinecom 24672 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  y  e.  P )  /\  <" A B x "> (cgrG `  G
) <" D E y "> )  /\  q  e.  P
)  /\  ( ( D L E ) (⟂G `  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 ) )
105101, 102, 1043brtr4d 4452 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  y  e.  P )  /\  <" A B x "> (cgrG `  G
) <" D E y "> )  /\  q  e.  P
)  /\  ( ( D L E ) (⟂G `  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 ) (⟂G `  G
) ( y L q ) )
1061, 2, 32, 33, 8, 92, 100, 105perpcom 24750 . . . . . . . . . . 11  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  y  e.  P )  /\  <" A B x "> (cgrG `  G
) <" D E y "> )  /\  q  e.  P
)  /\  ( ( D L E ) (⟂G `  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 ) (⟂G `  G
) ( E L D ) )
107 trgcopy.k . . . . . . . . . . . . . 14  |-  K  =  (hlG `  G )
108 simprrl 773 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  y  e.  P )  /\  <" A B x "> (cgrG `  G
) <" D E y "> )  /\  q  e.  P
)  /\  ( ( D L E ) (⟂G `  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 )
1091, 32, 107, 28, 93, 48, 8, 33, 108hlln 24644 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  y  e.  P )  /\  <" A B x "> (cgrG `  G
) <" D E y "> )  /\  q  e.  P
)  /\  ( ( D L E ) (⟂G `  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 ) )
1101, 32, 33, 8, 48, 93, 28, 99, 109lncom 24659 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  y  e.  P )  /\  <" A B x "> (cgrG `  G
) <" D E y "> )  /\  q  e.  P
)  /\  ( ( D L E ) (⟂G `  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 ) )
111110orcd 394 . . . . . . . . . . 11  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  y  e.  P )  /\  <" A B x "> (cgrG `  G
) <" D E y "> )  /\  q  e.  P
)  /\  ( ( D L E ) (⟂G `  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 ) )
1121, 2, 32, 33, 8, 48, 93, 28, 106, 111, 90colperp 24763 . . . . . . . . . 10  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  y  e.  P )  /\  <" A B x "> (cgrG `  G
) <" D E y "> )  /\  q  e.  P
)  /\  ( ( D L E ) (⟂G `  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 ) (⟂G `  G
) ( E L D ) )
1131, 2, 32, 33, 8, 91, 92, 112perpcom 24750 . . . . . . . . 9  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  y  e.  P )  /\  <" A B x "> (cgrG `  G
) <" D E y "> )  /\  q  e.  P
)  /\  ( ( D L E ) (⟂G `  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 ) (⟂G `  G
) ( y L f ) )
1141, 2, 32, 33, 8, 27, 23, 87, 28, 113perprag 24760 . . . . . . . 8  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  y  e.  P )  /\  <" A B x "> (cgrG `  G
) <" D E y "> )  /\  q  e.  P
)  /\  ( ( D L E ) (⟂G `  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.  (∟G `  G ) )
11579ad3antrrr 735 . . . . . . . . 9  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  y  e.  P )  /\  <" A B x "> (cgrG `  G
) <" D E y "> )  /\  q  e.  P
)  /\  ( ( D L E ) (⟂G `  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 "> )
1161, 2, 32, 3, 8, 12, 16, 45, 23, 27, 48, 115cgr3simp2 24558 . . . . . . . 8  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  y  e.  P )  /\  <" A B x "> (cgrG `  G
) <" D E y "> )  /\  q  e.  P
)  /\  ( ( D L E ) (⟂G `  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 ) )
1171, 2, 32, 8, 37, 16, 45, 19, 27, 48, 28, 69, 114, 116, 89hypcgr 24835 . . . . . . 7  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  y  e.  P )  /\  <" A B x "> (cgrG `  G
) <" D E y "> )  /\  q  e.  P
)  /\  ( ( D L E ) (⟂G `  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 ) )
118 eqid 2423 . . . . . . . . 9  |-  (pInvG `  G )  =  (pInvG `  G )
11951, 68eqbrtrd 4442 . . . . . . . . . 10  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  y  e.  P )  /\  <" A B x "> (cgrG `  G
) <" D E y "> )  /\  q  e.  P
)  /\  ( ( D L E ) (⟂G `  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 ) (⟂G `  G
) ( x L C ) )
1201, 2, 32, 33, 8, 12, 16, 49, 19, 119perprag 24760 . . . . . . . . 9  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  y  e.  P )  /\  <" A B x "> (cgrG `  G
) <" D E y "> )  /\  q  e.  P
)  /\  ( ( D L E ) (⟂G `  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.  (∟G `  G ) )
1211, 2, 32, 33, 118, 8, 12, 45, 19, 120ragcom 24735 . . . . . . . 8  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  y  e.  P )  /\  <" A B x "> (cgrG `  G
) <" D E y "> )  /\  q  e.  P
)  /\  ( ( D L E ) (⟂G `  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.  (∟G `  G ) )
122102, 113eqbrtrrd 4444 . . . . . . . . . 10  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  y  e.  P )  /\  <" A B x "> (cgrG `  G
) <" D E y "> )  /\  q  e.  P
)  /\  ( ( D L E ) (⟂G `  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 ) (⟂G `  G
) ( y L f ) )
1231, 2, 32, 33, 8, 23, 27, 86, 28, 122perprag 24760 . . . . . . . . 9  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  y  e.  P )  /\  <" A B x "> (cgrG `  G
) <" D E y "> )  /\  q  e.  P
)  /\  ( ( D L E ) (⟂G `  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.  (∟G `  G ) )
1241, 2, 32, 33, 118, 8, 23, 48, 28, 123ragcom 24735 . . . . . . . 8  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  y  e.  P )  /\  <" A B x "> (cgrG `  G
) <" D E y "> )  /\  q  e.  P
)  /\  ( ( D L E ) (⟂G `  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.  (∟G `  G ) )
1251, 2, 32, 8, 45, 19, 48, 28, 89tgcgrcomlr 24516 . . . . . . . 8  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  y  e.  P )  /\  <" A B x "> (cgrG `  G
) <" D E y "> )  /\  q  e.  P
)  /\  ( ( D L E ) (⟂G `  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 ) )
1261, 2, 32, 3, 8, 12, 16, 45, 23, 27, 48, 115cgr3simp3 24559 . . . . . . . 8  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  y  e.  P )  /\  <" A B x "> (cgrG `  G
) <" D E y "> )  /\  q  e.  P
)  /\  ( ( D L E ) (⟂G `  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 ) )
1271, 2, 32, 8, 37, 19, 45, 12, 28, 48, 23, 121, 124, 125, 126hypcgr 24835 . . . . . . 7  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  y  e.  P )  /\  <" A B x "> (cgrG `  G
) <" D E y "> )  /\  q  e.  P
)  /\  ( ( D L E ) (⟂G `  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 ) )
1281, 2, 3, 8, 12, 16, 19, 23, 27, 28, 31, 117, 127trgcgr 24553 . . . . . 6  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  y  e.  P )  /\  <" A B x "> (cgrG `  G
) <" D E y "> )  /\  q  e.  P
)  /\  ( ( D L E ) (⟂G `  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 "> )
1291, 32, 33, 4, 20, 24, 70tgelrnln 24667 . . . . . . . . 9  |-  ( ph  ->  ( D L E )  e.  ran  L
)
130129ad4antr 737 . . . . . . . 8  |-  ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G
) ( A L B ) )  /\  y  e.  P )  /\  <" A B x "> (cgrG `  G ) <" D E y "> )  ->  ( D L E )  e.  ran  L )
131130ad3antrrr 735 . . . . . . 7  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  y  e.  P )  /\  <" A B x "> (cgrG `  G
) <" D E y "> )  /\  q  e.  P
)  /\  ( ( D L E ) (⟂G `  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
)
132 simpl 459 . . . . . . . . . . 11  |-  ( ( w  =  k  /\  v  =  l )  ->  w  =  k )
133 eqidd 2424 . . . . . . . . . . 11  |-  ( ( w  =  k  /\  v  =  l )  ->  ( P  \  ( D L E ) )  =  ( P  \ 
( D L E ) ) )
134132, 133eleq12d 2505 . . . . . . . . . 10  |-  ( ( w  =  k  /\  v  =  l )  ->  ( w  e.  ( P  \  ( D L E ) )  <-> 
k  e.  ( P 
\  ( D L E ) ) ) )
135 simpr 463 . . . . . . . . . . 11  |-  ( ( w  =  k  /\  v  =  l )  ->  v  =  l )
136135, 133eleq12d 2505 . . . . . . . . . 10  |-  ( ( w  =  k  /\  v  =  l )  ->  ( v  e.  ( P  \  ( D L E ) )  <-> 
l  e.  ( P 
\  ( D L E ) ) ) )
137134, 136anbi12d 716 . . . . . . . . 9  |-  ( ( 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 463 . . . . . . . . . . 11  |-  ( ( ( w  =  k  /\  v  =  l )  /\  z  =  j )  ->  z  =  j )
139 simpll 759 . . . . . . . . . . . 12  |-  ( ( ( w  =  k  /\  v  =  l )  /\  z  =  j )  ->  w  =  k )
140 simplr 761 . . . . . . . . . . . 12  |-  ( ( ( w  =  k  /\  v  =  l )  /\  z  =  j )  ->  v  =  l )
141139, 140oveq12d 6321 . . . . . . . . . . 11  |-  ( ( ( w  =  k  /\  v  =  l )  /\  z  =  j )  ->  (
w I v )  =  ( k I l ) )
142138, 141eleq12d 2505 . . . . . . . . . 10  |-  ( ( ( w  =  k  /\  v  =  l )  /\  z  =  j )  ->  (
z  e.  ( w I v )  <->  j  e.  ( k I l ) ) )
143142cbvrexdva 3063 . . . . . . . . 9  |-  ( ( 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 ) ) )
144137, 143anbi12d 716 . . . . . . . 8  |-  ( ( 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 ) ) ) )
145144cbvopabv 4491 . . . . . . 7  |-  { <. 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 ) ) }
1468adantr 467 . . . . . . . . . . 11  |-  ( ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G
) ( A L B ) )  /\  y  e.  P )  /\  <" A B x "> (cgrG `  G ) <" D E y "> )  /\  q  e.  P
)  /\  ( ( D L E ) (⟂G `  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 )
14719adantr 467 . . . . . . . . . . 11  |-  ( ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G
) ( A L B ) )  /\  y  e.  P )  /\  <" A B x "> (cgrG `  G ) <" D E y "> )  /\  q  e.  P
)  /\  ( ( D L E ) (⟂G `  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 )
14816adantr 467 . . . . . . . . . . 11  |-  ( ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G
) ( A L B ) )  /\  y  e.  P )  /\  <" A B x "> (cgrG `  G ) <" D E y "> )  /\  q  e.  P
)  /\  ( ( D L E ) (⟂G `  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 )
14912adantr 467 . . . . . . . . . . 11  |-  ( ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G
) ( A L B ) )  /\  y  e.  P )  /\  <" A B x "> (cgrG `  G ) <" D E y "> )  /\  q  e.  P
)  /\  ( ( D L E ) (⟂G `  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 )
15023adantr 467 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G
) ( A L B ) )  /\  y  e.  P )  /\  <" A B x "> (cgrG `  G ) <" D E y "> )  /\  q  e.  P
)  /\  ( ( D L E ) (⟂G `  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 )
15127adantr 467 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G
) ( A L B ) )  /\  y  e.  P )  /\  <" A B x "> (cgrG `  G ) <" D E y "> )  /\  q  e.  P
)  /\  ( ( D L E ) (⟂G `  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 )
15228adantr 467 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G
) ( A L B ) )  /\  y  e.  P )  /\  <" A B x "> (cgrG `  G ) <" D E y "> )  /\  q  e.  P
)  /\  ( ( D L E ) (⟂G `  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 )
15371ad8antr 745 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G
) ( A L B ) )  /\  y  e.  P )  /\  <" A B x "> (cgrG `  G ) <" D E y "> )  /\  q  e.  P
)  /\  ( ( D L E ) (⟂G `  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 463 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G
) ( A L B ) )  /\  y  e.  P )  /\  <" A B x "> (cgrG `  G ) <" D E y "> )  /\  q  e.  P
)  /\  ( ( D L E ) (⟂G `  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 ) )
1551, 32, 33, 146, 151, 150, 152, 153, 154lncom 24659 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G
) ( A L B ) )  /\  y  e.  P )  /\  <" A B x "> (cgrG `  G ) <" D E y "> )  /\  q  e.  P
)  /\  ( ( D L E ) (⟂G `  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 ) )
156155orcd 394 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G
) ( A L B ) )  /\  y  e.  P )  /\  <" A B x "> (cgrG `  G ) <" D E y "> )  /\  q  e.  P
)  /\  ( ( D L E ) (⟂G `  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 ) )
1571, 33, 32, 146, 151, 150, 152, 156colrot1 24596 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G
) ( A L B ) )  /\  y  e.  P )  /\  <" A B x "> (cgrG `  G ) <" D E y "> )  /\  q  e.  P
)  /\  ( ( D L E ) (⟂G `  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 ) )
158128adantr 467 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G
) ( A L B ) )  /\  y  e.  P )  /\  <" A B x "> (cgrG `  G ) <" D E y "> )  /\  q  e.  P
)  /\  ( ( D L E ) (⟂G `  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 "> )
1591, 2, 32, 3, 146, 149, 148, 147, 150, 151, 152, 158trgcgrcom 24565 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G
) ( A L B ) )  /\  y  e.  P )  /\  <" A B x "> (cgrG `  G ) <" D E y "> )  /\  q  e.  P
)  /\  ( ( D L E ) (⟂G `  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 "> )
1601, 33, 32, 146, 150, 151, 152, 3, 149, 148, 147, 157, 159lnxfr 24603 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G
) ( A L B ) )  /\  y  e.  P )  /\  <" A B x "> (cgrG `  G ) <" D E y "> )  /\  q  e.  P
)  /\  ( ( D L E ) (⟂G `  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 ) )
1611, 33, 32, 146, 149, 147, 148, 160colrot1 24596 . . . . . . . . . . 11  |-  ( ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G
) ( A L B ) )  /\  y  e.  P )  /\  <" A B x "> (cgrG `  G ) <" D E y "> )  /\  q  e.  P
)  /\  ( ( D L E ) (⟂G `  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 ) )
1621, 33, 32, 146, 147, 148, 149, 161colcom 24595 . . . . . . . . . 10  |-  ( ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G
) ( A L B ) )  /\  y  e.  P )  /\  <" A B x "> (cgrG `  G ) <" D E y "> )  /\  q  e.  P
)  /\  ( ( D L E ) (⟂G `  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 ) )
16334ad8antr 745 . . . . . . . . . 10  |-  ( ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G
) ( A L B ) )  /\  y  e.  P )  /\  <" A B x "> (cgrG `  G ) <" D E y "> )  /\  q  e.  P
)  /\  ( ( D L E ) (⟂G `  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 ) )
164162, 163pm2.65da 579 . . . . . . . . 9  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  y  e.  P )  /\  <" A B x "> (cgrG `  G
) <" D E y "> )  /\  q  e.  P
)  /\  ( ( D L E ) (⟂G `  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 ) )
165108, 164jca 535 . . . . . . . 8  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  y  e.  P )  /\  <" A B x "> (cgrG `  G
) <" D E y "> )  /\  q  e.  P
)  /\  ( ( D L E ) (⟂G `  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  /\  -.  f  e.  ( D L E ) ) )
166109orcd 394 . . . . . . . . . 10  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  y  e.  P )  /\  <" A B x "> (cgrG `  G
) <" D E y "> )  /\  q  e.  P
)  /\  ( ( D L E ) (⟂G `  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 )  \/  q  =  y ) )
1671, 33, 32, 8, 93, 48, 28, 166colrot2 24597 . . . . . . . . 9  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  y  e.  P )  /\  <" A B x "> (cgrG `  G
) <" D E y "> )  /\  q  e.  P
)  /\  ( ( D L E ) (⟂G `  G ) ( q L y )  /\  q ( (hpG `  G ) `  ( D L E ) ) F ) )  /\  ( f  e.  P  /\  ( f ( K `
 y ) q  /\  ( y  .-  f )  =  ( x  .-  C ) ) ) )  -> 
( y  e.  ( f L q )  \/  f  =  q ) )
1681, 32, 33, 8, 131, 28, 145, 93, 86, 167, 107colhp 24804 . . . . . . . 8  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  y  e.  P )  /\  <" A B x "> (cgrG `  G
) <" D E y "> )  /\  q  e.  P
)  /\  ( ( D L E ) (⟂G `  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  <->  ( f
( K `  y
) q  /\  -.  f  e.  ( D L E ) ) ) )
169165, 168mpbird 236 . . . . . . 7  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  y  e.  P )  /\  <" A B x "> (cgrG `  G
) <" D E y "> )  /\  q  e.  P
)  /\  ( ( D L E ) (⟂G `  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 )
170 trgcopy.f . . . . . . . . . 10  |-  ( ph  ->  F  e.  P )
171170ad4antr 737 . . . . . . . . 9  |-  ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G
) ( A L B ) )  /\  y  e.  P )  /\  <" A B x "> (cgrG `  G ) <" D E y "> )  ->  F  e.  P
)
172171ad2antrr 731 . . . . . . . 8  |-  ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G ) ( A L B ) )  /\  y  e.  P
)  /\  <" A B x "> (cgrG `  G ) <" D E y "> )  /\  q  e.  P )  /\  ( ( D L E ) (⟂G `  G
) ( q L y )  /\  q
( (hpG `  G
) `  ( D L E ) ) F ) )  ->  F  e.  P )
173172adantr 467 . . . . . . 7  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  y  e.  P )  /\  <" A B x "> (cgrG `  G
) <" D E y "> )  /\  q  e.  P
)  /\  ( ( D L E ) (⟂G `  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 )
174 simplrr 770 . . . . . . 7  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  y  e.  P )  /\  <" A B x "> (cgrG `  G
) <" D E y "> )  /\  q  e.  P
)  /\  ( ( D L E ) (⟂G `  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 )
1751, 32, 33, 8, 131, 28, 145, 93, 169, 173, 174hpgtr 24802 . . . . . 6  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  y  e.  P )  /\  <" A B x "> (cgrG `  G
) <" D E y "> )  /\  q  e.  P
)  /\  ( ( D L E ) (⟂G `  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 )
176128, 175jca 535 . . . . 5  |-  ( ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G )
( A L B ) )  /\  y  e.  P )  /\  <" A B x "> (cgrG `  G
) <" D E y "> )  /\  q  e.  P
)  /\  ( ( D L E ) (⟂G `  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 ) )
1771, 32, 107, 47, 44, 18, 7, 94, 2, 97, 64hlcgrex 24653 . . . . 5  |-  ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G ) ( A L B ) )  /\  y  e.  P
)  /\  <" A B x "> (cgrG `  G ) <" D E y "> )  /\  q  e.  P )  /\  ( ( D L E ) (⟂G `  G
) ( q L y )  /\  q
( (hpG `  G
) `  ( D L E ) ) F ) )  ->  E. f  e.  P  ( f
( K `  y
) q  /\  (
y  .-  f )  =  ( x  .-  C ) ) )
178176, 177reximddv 2902 . . . 4  |-  ( ( ( ( ( ( ( ph  /\  x  e.  ( A L B ) )  /\  ( C L x ) (⟂G `  G ) ( A L B ) )  /\  y  e.  P
)  /\  <" A B x "> (cgrG `  G ) <" D E