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.

Step	Hyp	Ref	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 )
5	4	ad2antrr 731	. . . . . . . . . 10 |- ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) (⟂G ` G ) ( A L B ) ) -> G e. TarskiG )
6	5	ad2antrr 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 )
7	6	ad2antrr 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 )
8	7	adantr 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 )
10	9	ad2antrr 731	. . . . . . . . 9 |- ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) (⟂G ` G ) ( A L B ) ) -> A e. P )
11	10	ad2antrr 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 )
12	11	ad3antrrr 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 )
14	13	ad2antrr 731	. . . . . . . . 9 |- ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) (⟂G ` G ) ( A L B ) ) -> B e. P )
15	14	ad2antrr 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 )
16	15	ad3antrrr 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 )
18	17	ad6antr 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 )
19	18	adantr 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 )
21	20	ad2antrr 731	. . . . . . . . 9 |- ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) (⟂G ` G ) ( A L B ) ) -> D e. P )
22	21	ad2antrr 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 )
23	22	ad3antrrr 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 )
25	24	ad2antrr 731	. . . . . . . . 9 |- ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) (⟂G ` G ) ( A L B ) ) -> E e. P )
26	25	ad2antrr 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 )
27	26	ad3antrrr 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 ) )
30	29	ad2antrr 731	. . . . . . . 8 |- ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) (⟂G ` G ) ( A L B ) ) -> ( A .- B ) = ( D .- E ) )
31	30	ad5antr 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 ) )
35	1, 33, 32, 4, 13, 17, 9, 34	ncoltgdim2 24602	. . . . . . . . . 10 |- ( ph -> GDimTarskiG≥ 2 )
36	35	ad4antr 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 )
37	36	ad3antrrr 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 )
38	1, 32, 33, 4, 9, 13, 17, 34	ncolne1 24662	. . . . . . . . . . . . . 14 |- ( ph -> A =/= B )
39	1, 32, 33, 4, 9, 13, 38	tgelrnln 24667	. . . . . . . . . . . . 13 |- ( ph -> ( A L B ) e. ran L )
40	39	ad2antrr 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 ) )
42	1, 33, 32, 5, 40, 41	tglnpt 24586	. . . . . . . . . . 11 |- ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) (⟂G ` G ) ( A L B ) ) -> x e. P )
43	42	ad2antrr 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 )
44	43	ad2antrr 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 )
45	44	adantr 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 )
47	46	ad2antrr 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 )
48	47	adantr 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 )
49	41	ad5antr 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 ) )
50	38	ad7antr 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 )
51	1, 32, 33, 8, 12, 16, 50	tglinecom 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 ) )
52	49, 51	eleqtrd 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 ) )
54	33, 8, 53	perpln1 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 )
55	40	ad5antr 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 )
56	1, 2, 32, 33, 8, 54, 55, 53	perpcom 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 ) )
57	1, 33, 32, 4, 13, 17, 9, 34	ncolrot2 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 ) )
59	57, 58	sylib 200	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( -. C e. ( A L B ) /\ -. A = B ) )
60	59	simpld 461	. . . . . . . . . . . . . . . 16 |- ( ph -> -. C e. ( A L B ) )
61	60	ad2antrr 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 )
63	41, 61, 62	syl2anc 666	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) (⟂G ` G ) ( A L B ) ) -> x =/= C )
64	63	ad4antr 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 )
65	64	adantr 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 )
66	65	necomd 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 )
67	1, 32, 33, 8, 19, 45, 66	tglinecom 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 ) )
68	56, 51, 67	3brtr3d 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 ) )
69	1, 2, 32, 33, 8, 16, 12, 52, 19, 68	perprag 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 ) )
70	1, 2, 32, 4, 9, 13, 20, 24, 29, 38	tgcgrneq 24519	. . . . . . . . . . . 12 |- ( ph -> D =/= E )
71	70	necomd 2696	. . . . . . . . . . 11 |- ( ph -> E =/= D )
72	71	ad7antr 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 )
73	70	ad4antr 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 )
74	73	neneqd 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 )
75	41	orcd 394	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) (⟂G ` G ) ( A L B ) ) -> ( x e. ( A L B ) \/ A = B ) )
76	1, 33, 32, 5, 10, 14, 42, 75	colrot2 24597	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) (⟂G ` G ) ( A L B ) ) -> ( B e. ( x L A ) \/ x = A ) )
77	1, 33, 32, 5, 42, 10, 14, 76	colcom 24595	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) (⟂G ` G ) ( A L B ) ) -> ( B e. ( A L x ) \/ A = x ) )
78	77	ad2antrr 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 "> )
80	1, 33, 32, 6, 11, 15, 43, 3, 22, 26, 46, 78, 79	lnxfr 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 ) )
81	1, 33, 32, 6, 22, 46, 26, 80	colrot2 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 ) )
82	1, 33, 32, 6, 26, 22, 46, 81	colcom 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 ) )
83	82	orcomd 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 ) ) )
84	83	ord 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 ) ) )
85	74, 84	mpd 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 ) )
86	85	ad3antrrr 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 ) )
87	1, 32, 33, 8, 27, 23, 48, 72, 86	lncom 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 ) )
89	88	eqcomd 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 ) )
90	1, 2, 32, 8, 45, 19, 48, 28, 89, 65	tgcgrneq 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 )
91	1, 32, 33, 8, 48, 28, 90	tgelrnln 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 )
92	1, 32, 33, 8, 27, 23, 72	tgelrnln 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 ) )
96	33, 7, 95	perpln2 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 )
97	1, 32, 33, 7, 94, 47, 96	tglnne 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 )
98	97	adantr 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 )
99	98	necomd 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 )
100	1, 32, 33, 8, 48, 93, 99	tgelrnln 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 )
101	95	adantr 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 ) )
102	1, 32, 33, 8, 27, 23, 72	tglinecom 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 ) )
103	1, 32, 33, 8, 48, 93, 100	tglnne 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 )
104	1, 32, 33, 8, 48, 93, 103	tglinecom 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 ) )
105	101, 102, 104	3brtr4d 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 ) )
106	1, 2, 32, 33, 8, 92, 100, 105	perpcom 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 )
109	1, 32, 107, 28, 93, 48, 8, 33, 108	hlln 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 ) )
110	1, 32, 33, 8, 48, 93, 28, 99, 109	lncom 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 ) )
111	110	orcd 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 ) )
112	1, 2, 32, 33, 8, 48, 93, 28, 106, 111, 90	colperp 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 ) )
113	1, 2, 32, 33, 8, 91, 92, 112	perpcom 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 ) )
114	1, 2, 32, 33, 8, 27, 23, 87, 28, 113	perprag 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 ) )
115	79	ad3antrrr 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 "> )
116	1, 2, 32, 3, 8, 12, 16, 45, 23, 27, 48, 115	cgr3simp2 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 ) )
117	1, 2, 32, 8, 37, 16, 45, 19, 27, 48, 28, 69, 114, 116, 89	hypcgr 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 )
119	51, 68	eqbrtrd 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 ) )
120	1, 2, 32, 33, 8, 12, 16, 49, 19, 119	perprag 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 ) )
121	1, 2, 32, 33, 118, 8, 12, 45, 19, 120	ragcom 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 ) )
122	102, 113	eqbrtrrd 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 ) )
123	1, 2, 32, 33, 8, 23, 27, 86, 28, 122	perprag 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 ) )
124	1, 2, 32, 33, 118, 8, 23, 48, 28, 123	ragcom 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 ) )
125	1, 2, 32, 8, 45, 19, 48, 28, 89	tgcgrcomlr 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 ) )
126	1, 2, 32, 3, 8, 12, 16, 45, 23, 27, 48, 115	cgr3simp3 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 ) )
127	1, 2, 32, 8, 37, 19, 45, 12, 28, 48, 23, 121, 124, 125, 126	hypcgr 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 ) )
128	1, 2, 3, 8, 12, 16, 19, 23, 27, 28, 31, 117, 127	trgcgr 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 "> )
129	1, 32, 33, 4, 20, 24, 70	tgelrnln 24667	. . . . . . . . 9 |- ( ph -> ( D L E ) e. ran L )
130	129	ad4antr 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 )
131	130	ad3antrrr 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 ) ) )
134	132, 133	eleq12d 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 )
136	135, 133	eleq12d 2505	. . . . . . . . . 10 |- ( ( w = k /\ v = l ) -> ( v e. ( P \ ( D L E ) ) <-> l e. ( P \ ( D L E ) ) ) )
137	134, 136	anbi12d 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 )
141	139, 140	oveq12d 6321	. . . . . . . . . . 11 |- ( ( ( w = k /\ v = l ) /\ z = j ) -> ( w I v ) = ( k I l ) )
142	138, 141	eleq12d 2505	. . . . . . . . . 10 |- ( ( ( w = k /\ v = l ) /\ z = j ) -> ( z e. ( w I v ) <-> j e. ( k I l ) ) )
143	142	cbvrexdva 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 ) ) )
144	137, 143	anbi12d 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 ) ) ) )
145	144	cbvopabv 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 ) ) }
146	8	adantr 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 )
147	19	adantr 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 )
148	16	adantr 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 )
149	12	adantr 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 )
150	23	adantr 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 )
151	27	adantr 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 )
152	28	adantr 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 )
153	71	ad8antr 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 ) )
155	1, 32, 33, 146, 151, 150, 152, 153, 154	lncom 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 ) )
156	155	orcd 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 ) )
157	1, 33, 32, 146, 151, 150, 152, 156	colrot1 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 ) )
158	128	adantr 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 "> )
159	1, 2, 32, 3, 146, 149, 148, 147, 150, 151, 152, 158	trgcgrcom 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 "> )
160	1, 33, 32, 146, 150, 151, 152, 3, 149, 148, 147, 157, 159	lnxfr 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 ) )
161	1, 33, 32, 146, 149, 147, 148, 160	colrot1 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 ) )
162	1, 33, 32, 146, 147, 148, 149, 161	colcom 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 ) )
163	34	ad8antr 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 ) )
164	162, 163	pm2.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 ) )
165	108, 164	jca 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 ) ) )
166	109	orcd 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 ) )
167	1, 33, 32, 8, 93, 48, 28, 166	colrot2 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 ) )
168	1, 32, 33, 8, 131, 28, 145, 93, 86, 167, 107	colhp 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 ) ) ) )
169	165, 168	mpbird 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 )
171	170	ad4antr 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 )
172	171	ad2antrr 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 )
173	172	adantr 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 )
175	1, 32, 33, 8, 131, 28, 145, 93, 169, 173, 174	hpgtr 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 )
176	128, 175	jca 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 ) )
177	1, 32, 107, 47, 44, 18, 7, 94, 2, 97, 64	hlcgrex 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 ) ) )
178	176, 177	reximddv 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