MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  trgcopy Structured version   Visualization version   Unicode version
Theorem trgcopy 24894
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 2461 . . . . . . 7 |- (cgrG ` G ) = (cgrG ` G )
4 trgcopy.g . . . . . . . . . . 11 |- ( ph -> G e. TarskiG )
54ad2antrr 737 . . . . . . . . . 10 |- ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) (⟂G ` G ) ( A L B ) ) -> G e. TarskiG )
65ad2antrr 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 "> ) -> G e. TarskiG )
76ad2antrr 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 "> ) /\ q e. P ) /\ ( ( D L E ) (⟂G ` G ) ( q L y ) /\ q ( (hpG ` G ) ` ( D L E ) ) F ) ) -> G e. TarskiG )
87adantr 471 . . . . . . 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 737 . . . . . . . . 9 |- ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) (⟂G ` G ) ( A L B ) ) -> A e. P )
1110ad2antrr 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 "> ) -> A e. P )
1211ad3antrrr 741 . . . . . . 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 737 . . . . . . . . 9 |- ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) (⟂G ` G ) ( A L B ) ) -> B e. P )
1514ad2antrr 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 "> ) -> B e. P )
1615ad3antrrr 741 . . . . . . 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 747 . . . . . . . 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 471 . . . . . . 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 737 . . . . . . . . 9 |- ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) (⟂G ` G ) ( A L B ) ) -> D e. P )
2221ad2antrr 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 e. P )
2322ad3antrrr 741 . . . . . . 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 737 . . . . . . . . 9 |- ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) (⟂G ` G ) ( A L B ) ) -> E e. P )
2625ad2antrr 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 "> ) -> E e. P )
2726ad3antrrr 741 . . . . . . 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 769 . . . . . . 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 737 . . . . . . . 8 |- ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) (⟂G ` G ) ( A L B ) ) -> ( A .- B ) = ( D .- E ) )
3130ad5antr 745 . . . . . . 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 24658 . . . . . . . . . 10 |- ( ph -> GDimTarskiG≥ 2 )
3635ad4antr 743 . . . . . . . . 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 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 ) ) /\ ( f e. P /\ ( f ( K ` y ) q /\ ( y .- f ) = ( x .- C ) ) ) ) -> GDimTarskiG≥ 2 )
381, 32, 33, 4, 9, 13, 17, 34ncolne1 24718 . . . . . . . . . . . . . 14 |- ( ph -> A =/= B )
391, 32, 33, 4, 9, 13, 38tgelrnln 24723 . . . . . . . . . . . . 13 |- ( ph -> ( A L B ) e. ran L )
4039ad2antrr 737 . . . . . . . . . . . 12 |- ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) (⟂G ` G ) ( A L B ) ) -> ( A L B ) e. ran L )
41 simplr 767 . . . . . . . . . . . 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 24642 . . . . . . . . . . 11 |- ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) (⟂G ` G ) ( A L B ) ) -> x e. P )
4342ad2antrr 737 . . . . . . . . . 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 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 "> ) /\ q e. P ) /\ ( ( D L E ) (⟂G ` G ) ( q L y ) /\ q ( (hpG ` G ) ` ( D L E ) ) F ) ) -> x e. P )
4544adantr 471 . . . . . . . 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 767 . . . . . . . . . 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 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 "> ) /\ q e. P ) /\ ( ( D L E ) (⟂G ` G ) ( q L y ) /\ q ( (hpG ` G ) ` ( D L E ) ) F ) ) -> y e. P )
4847adantr 471 . . . . . . . 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 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 ) ) ) ) -> x e. ( A L B ) )
5038ad7antr 749 . . . . . . . . . . 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 24728 . . . . . . . . . 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 2541 . . . . . . . . 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 786 . . . . . . . . . . . 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 24803 . . . . . . . . . . 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 745 . . . . . . . . . . 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 24806 . . . . . . . . . 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 24656 . . . . . . . . . . . . . . . . . 18 |- ( ph -> -. ( C e. ( A L B ) \/ A = B ) )
58 ioran 497 . . . . . . . . . . . . . . . . . 18 |- ( -. ( C e. ( A L B ) \/ A = B ) <-> ( -. C e. ( A L B ) /\ -. A = B ) )
5957, 58sylib 201 . . . . . . . . . . . . . . . . 17 |- ( ph -> ( -. C e. ( A L B ) /\ -. A = B ) )
6059simpld 465 . . . . . . . . . . . . . . . 16 |- ( ph -> -. C e. ( A L B ) )
6160ad2antrr 737 . . . . . . . . . . . . . . 15 |- ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) (⟂G ` G ) ( A L B ) ) -> -. C e. ( A L B ) )
62 nelne2 2732 . . . . . . . . . . . . . . 15 |- ( ( x e. ( A L B ) /\ -. C e. ( A L B ) ) -> x =/= C )
6341, 61, 62syl2anc 671 . . . . . . . . . . . . . 14 |- ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) (⟂G ` G ) ( A L B ) ) -> x =/= C )
6463ad4antr 743 . . . . . . . . . . . . 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 471 . . . . . . . . . . . 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 2690 . . . . . . . . . . 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 24728 . . . . . . . . . 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 4445 . . . . . . . . 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 24816 . . . . . . . 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 24575 . . . . . . . . . . . 12 |- ( ph -> D =/= E )
7170necomd 2690 . . . . . . . . . . 11 |- ( ph -> E =/= D )
7271ad7antr 749 . . . . . . . . . 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 743 . . . . . . . . . . . . 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 2639 . . . . . . . . . . . 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 398 . . . . . . . . . . . . . . . . . . . 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 24653 . . . . . . . . . . . . . . . . . . 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 24651 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) (⟂G ` G ) ( A L B ) ) -> ( B e. ( A L x ) \/ A = x ) )
7877ad2antrr 737 . . . . . . . . . . . . . . . . 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 467 . . . . . . . . . . . . . . . . 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 24659 . . . . . . . . . . . . . . . 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 24653 . . . . . . . . . . . . . . 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 24651 . . . . . . . . . . . . . 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 394 . . . . . . . . . . . . 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 383 . . . . . . . . . . . 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 741 . . . . . . . . . 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 24715 . . . . . . . . 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 780 . . . . . . . . . . . . 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 2467 . . . . . . . . . . . 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 24575 . . . . . . . . . . 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 24723 . . . . . . . . . 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 24723 . . . . . . . . . 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 774 . . . . . . . . . . 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 767 . . . . . . . . . . . . . . . 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 769 . . . . . . . . . . . . . . . . 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 24804 . . . . . . . . . . . . . . . 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 24721 . . . . . . . . . . . . . . 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 471 . . . . . . . . . . . . . 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 2690 . . . . . . . . . . . . 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 24723 . . . . . . . . . . . 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 471 . . . . . . . . . . . . 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 24728 . . . . . . . . . . . . 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 24721 . . . . . . . . . . . . . 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 24728 . . . . . . . . . . . . 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 4446 . . . . . . . . . . . 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 24806 . . . . . . . . . . 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 779 . . . . . . . . . . . . . 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 24700 . . . . . . . . . . . . 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 24715 . . . . . . . . . . . 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 398 . . . . . . . . . . 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 24819 . . . . . . . . . 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 24806 . . . . . . . . 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 24816 . . . . . . . 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 741 . . . . . . . . 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 24614 . . . . . . . 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 24891 . . . . . . 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 2461 . . . . . . . . 9 |- (pInvG ` G ) = (pInvG ` G )
11951, 68eqbrtrd 4436 . . . . . . . . . 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 24816 . . . . . . . . 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 24791 . . . . . . . 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 4438 . . . . . . . . . 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 24816 . . . . . . . . 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 24791 . . . . . . . 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 24572 . . . . . . . 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 24615 . . . . . . . 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 24891 . . . . . . 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 24609 . . . . . 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 24723 . . . . . . . . 9 |- ( ph -> ( D L E ) e. ran L )
130129ad4antr 743 . . . . . . . 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 741 . . . . . . 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 463 . . . . . . . . . . 11 |- ( ( w = k /\ v = l ) -> w = k )
133 eqidd 2462 . . . . . . . . . . 11 |- ( ( w = k /\ v = l ) -> ( P \ ( D L E ) ) = ( P \ ( D L E ) ) )
134132, 133eleq12d 2533 . . . . . . . . . 10 |- ( ( w = k /\ v = l ) -> ( w e. ( P \ ( D L E ) ) <-> k e. ( P \ ( D L E ) ) ) )
135 simpr 467 . . . . . . . . . . 11 |- ( ( w = k /\ v = l ) -> v = l )
136135, 133eleq12d 2533 . . . . . . . . . 10 |- ( ( w = k /\ v = l ) -> ( v e. ( P \ ( D L E ) ) <-> l e. ( P \ ( D L E ) ) ) )
137134, 136anbi12d 722 . . . . . . . . 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 467 . . . . . . . . . . 11 |- ( ( ( w = k /\ v = l ) /\ z = j ) -> z = j )
139 simpll 765 . . . . . . . . . . . 12 |- ( ( ( w = k /\ v = l ) /\ z = j ) -> w = k )
140 simplr 767 . . . . . . . . . . . 12 |- ( ( ( w = k /\ v = l ) /\ z = j ) -> v = l )
141139, 140oveq12d 6332 . . . . . . . . . . 11 |- ( ( ( w = k /\ v = l ) /\ z = j ) -> ( w I v ) = ( k I l ) )
142138, 141eleq12d 2533 . . . . . . . . . 10 |- ( ( ( w = k /\ v = l ) /\ z = j ) -> ( z e. ( w I v ) <-> j e. ( k I l ) ) )
143142cbvrexdva 3037 . . . . . . . . 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 722 . . . . . . . 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 4485 . . . . . . 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 471 . . . . . . . . . . 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 471 . . . . . . . . . . 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 471 . . . . . . . . . . 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 471 . . . . . . . . . . 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 471 . . . . . . . . . . . . 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 471 . . . . . . . . . . . . 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 471 . . . . . . . . . . . . 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 751 . . . . . . . . . . . . . . . 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 467 . . . . . . . . . . . . . . . 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 24715 . . . . . . . . . . . . . . 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 398 . . . . . . . . . . . . . 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 24652 . . . . . . . . . . . . 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 471 . . . . . . . . . . . . . 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 24621 . . . . . . . . . . . . 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 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. ( D L E ) ) -> ( B e. ( A L C ) \/ A = C ) )
1611, 33, 32, 146, 149, 147, 148, 160colrot1 24652 . . . . . . . . . . 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 24651 . . . . . . . . . 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 751 . . . . . . . . . 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 584 . . . . . . . . 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 539 . . . . . . . 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 398 . . . . . . . . . 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 24653 . . . . . . . . 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 24860 . . . . . . . 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 240 . . . . . . 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 743 . . . . . . . . 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 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 "> ) /\ q e. P ) /\ ( ( D L E ) (⟂G ` G ) ( q L y ) /\ q ( (hpG ` G ) ` ( D L E ) ) F ) ) -> F e. P )
173172adantr 471 . . . . . . 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 776 . . . . . . 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 24858 . . . . . 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 539 . . . . 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 24709 . . . . 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 2874 . . . 4 |- ( ( ( ( ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) (⟂G ` G ) ( A L B ) ) /\ y e. P ) /\ <" A B x "> (cgrG ` G ) <" D