Theorem trgcopy 25696

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 2622	. . . . . . 7 |- (cgrG ` G ) = (cgrG ` G )
4		trgcopy.g	. . . . . . . . . . 11 |- ( ph -> G e. TarskiG )
5	4	ad2antrr 762	. . . . . . . . . 10 |- ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) (⟂G ` G ) ( A L B ) ) -> G e. TarskiG )
6	5	ad2antrr 762	. . . . . . . . 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 762	. . . . . . . 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 481	. . . . . . 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 762	. . . . . . . . 9 |- ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) (⟂G ` G ) ( A L B ) ) -> A e. P )
11	10	ad2antrr 762	. . . . . . . 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 766	. . . . . . 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 762	. . . . . . . . 9 |- ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) (⟂G ` G ) ( A L B ) ) -> B e. P )
15	14	ad2antrr 762	. . . . . . . 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 766	. . . . . . 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 772	. . . . . . . 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 481	. . . . . . 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 762	. . . . . . . . 9 |- ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) (⟂G ` G ) ( A L B ) ) -> D e. P )
22	21	ad2antrr 762	. . . . . . . 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 766	. . . . . . 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 762	. . . . . . . . 9 |- ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) (⟂G ` G ) ( A L B ) ) -> E e. P )
26	25	ad2antrr 762	. . . . . . . 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 766	. . . . . . 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 794	. . . . . . 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 762	. . . . . . . 8 |- ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) (⟂G ` G ) ( A L B ) ) -> ( A .- B ) = ( D .- E ) )
31	30	ad5antr 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 ) ) ) ) -> ( 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 25460	. . . . . . . . . 10 |- ( ph -> GDimTarskiG≥ 2 )
36	35	ad4antr 768	. . . . . . . . 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 766	. . . . . . . 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 25520	. . . . . . . . . . . . . 14 |- ( ph -> A =/= B )
39	1, 32, 33, 4, 9, 13, 38	tgelrnln 25525	. . . . . . . . . . . . 13 |- ( ph -> ( A L B ) e. ran L )
40	39	ad2antrr 762	. . . . . . . . . . . 12 |- ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) (⟂G ` G ) ( A L B ) ) -> ( A L B ) e. ran L )
41		simplr 792	. . . . . . . . . . . 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 25444	. . . . . . . . . . 11 |- ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) (⟂G ` G ) ( A L B ) ) -> x e. P )
43	42	ad2antrr 762	. . . . . . . . . 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 762	. . . . . . . . 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 481	. . . . . . . 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 792	. . . . . . . . . 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 762	. . . . . . . . 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 481	. . . . . . . 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 770	. . . . . . . . . 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 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 ) ) ) ) -> A =/= B )
51	1, 32, 33, 8, 12, 16, 50	tglinecom 25530	. . . . . . . . . 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 2703	. . . . . . . . 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 811	. . . . . . . . . . . 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 25605	. . . . . . . . . . 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 770	. . . . . . . . . . 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 25608	. . . . . . . . . 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 25458	. . . . . . . . . . . . . . . . . 18 |- ( ph -> -. ( C e. ( A L B ) \/ A = B ) )
58		ioran 511	. . . . . . . . . . . . . . . . . 18 |- ( -. ( C e. ( A L B ) \/ A = B ) <-> ( -. C e. ( A L B ) /\ -. A = B ) )
59	57, 58	sylib 208	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( -. C e. ( A L B ) /\ -. A = B ) )
60	59	simpld 475	. . . . . . . . . . . . . . . 16 |- ( ph -> -. C e. ( A L B ) )
61	60	ad2antrr 762	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) (⟂G ` G ) ( A L B ) ) -> -. C e. ( A L B ) )
62		nelne2 2891	. . . . . . . . . . . . . . 15 |- ( ( x e. ( A L B ) /\ -. C e. ( A L B ) ) -> x =/= C )
63	41, 61, 62	syl2anc 693	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) (⟂G ` G ) ( A L B ) ) -> x =/= C )
64	63	ad4antr 768	. . . . . . . . . . . . 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 481	. . . . . . . . . . . 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 2849	. . . . . . . . . . 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 25530	. . . . . . . . . 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 4684	. . . . . . . . 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 25618	. . . . . . . 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 25378	. . . . . . . . . . . 12 |- ( ph -> D =/= E )
71	70	necomd 2849	. . . . . . . . . . 11 |- ( ph -> E =/= D )
72	71	ad7antr 774	. . . . . . . . . 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 768	. . . . . . . . . . . . 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 2799	. . . . . . . . . . . 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 407	. . . . . . . . . . . . . . . . . . . 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 25455	. . . . . . . . . . . . . . . . . . 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 25453	. . . . . . . . . . . . . . . . . 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 762	. . . . . . . . . . . . . . . . 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 477	. . . . . . . . . . . . . . . . 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 25461	. . . . . . . . . . . . . . . 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 25455	. . . . . . . . . . . . . . 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 25453	. . . . . . . . . . . . . 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 403	. . . . . . . . . . . . 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 392	. . . . . . . . . . . 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 766	. . . . . . . . . 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 25517	. . . . . . . . 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 805	. . . . . . . . . . . . 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 2628	. . . . . . . . . . . 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 25378	. . . . . . . . . . 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 25525	. . . . . . . . . 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 25525	. . . . . . . . . 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 799	. . . . . . . . . . 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 792	. . . . . . . . . . . . . . . 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 794	. . . . . . . . . . . . . . . . 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 25606	. . . . . . . . . . . . . . . 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 25523	. . . . . . . . . . . . . . 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 481	. . . . . . . . . . . . . 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 2849	. . . . . . . . . . . . 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 25525	. . . . . . . . . . . 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 481	. . . . . . . . . . . . 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 25530	. . . . . . . . . . . . 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 25523	. . . . . . . . . . . . . 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 25530	. . . . . . . . . . . . 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 4685	. . . . . . . . . . . 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 25608	. . . . . . . . . . 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 804	. . . . . . . . . . . . . 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 25502	. . . . . . . . . . . . 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 25517	. . . . . . . . . . . 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 407	. . . . . . . . . . 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 25621	. . . . . . . . . 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 25608	. . . . . . . . 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 25618	. . . . . . . 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 766	. . . . . . . . 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 25416	. . . . . . . 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 25693	. . . . . . 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 2622	. . . . . . . . 9 |- (pInvG ` G ) = (pInvG ` G )
119	51, 68	eqbrtrd 4675	. . . . . . . . . 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 25618	. . . . . . . . 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 25593	. . . . . . . 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 4677	. . . . . . . . . 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 25618	. . . . . . . . 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 25593	. . . . . . . 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 25375	. . . . . . . 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 25417	. . . . . . . 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 25693	. . . . . . 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 25411	. . . . . 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 25525	. . . . . . . . 9 |- ( ph -> ( D L E ) e. ran L )
130	129	ad4antr 768	. . . . . . . 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 766	. . . . . . 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 473	. . . . . . . . . . 11 |- ( ( w = k /\ v = l ) -> w = k )
133		eqidd 2623	. . . . . . . . . . 11 |- ( ( w = k /\ v = l ) -> ( P \ ( D L E ) ) = ( P \ ( D L E ) ) )
134	132, 133	eleq12d 2695	. . . . . . . . . 10 |- ( ( w = k /\ v = l ) -> ( w e. ( P \ ( D L E ) ) <-> k e. ( P \ ( D L E ) ) ) )
135		simpr 477	. . . . . . . . . . 11 |- ( ( w = k /\ v = l ) -> v = l )
136	135, 133	eleq12d 2695	. . . . . . . . . 10 |- ( ( w = k /\ v = l ) -> ( v e. ( P \ ( D L E ) ) <-> l e. ( P \ ( D L E ) ) ) )
137	134, 136	anbi12d 747	. . . . . . . . 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 477	. . . . . . . . . . 11 |- ( ( ( w = k /\ v = l ) /\ z = j ) -> z = j )
139		simpll 790	. . . . . . . . . . . 12 |- ( ( ( w = k /\ v = l ) /\ z = j ) -> w = k )
140		simplr 792	. . . . . . . . . . . 12 |- ( ( ( w = k /\ v = l ) /\ z = j ) -> v = l )
141	139, 140	oveq12d 6668	. . . . . . . . . . 11 |- ( ( ( w = k /\ v = l ) /\ z = j ) -> ( w I v ) = ( k I l ) )
142	138, 141	eleq12d 2695	. . . . . . . . . 10 |- ( ( ( w = k /\ v = l ) /\ z = j ) -> ( z e. ( w I v ) <-> j e. ( k I l ) ) )
143	142	cbvrexdva 3178	. . . . . . . . 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 747	. . . . . . . 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 4722	. . . . . . 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 481	. . . . . . . . . . 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 481	. . . . . . . . . . 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 481	. . . . . . . . . . 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 481	. . . . . . . . . . 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 481	. . . . . . . . . . . . 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 481	. . . . . . . . . . . . 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 481	. . . . . . . . . . . . 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 776	. . . . . . . . . . . . . . . 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 477	. . . . . . . . . . . . . . . 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 25517	. . . . . . . . . . . . . . 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 407	. . . . . . . . . . . . . 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 25454	. . . . . . . . . . . . 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 481	. . . . . . . . . . . . . 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 25423	. . . . . . . . . . . . 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 25461	. . . . . . . . . . . 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 25454	. . . . . . . . . . 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 25453	. . . . . . . . . 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 776	. . . . . . . . . 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 600	. . . . . . . . 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 554	. . . . . . . 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 407	. . . . . . . . . 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 25455	. . . . . . . . 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 25662	. . . . . . . 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 247	. . . . . . 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 768	. . . . . . . . 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 762	. . . . . . . 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 481	. . . . . . 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 801	. . . . . . 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 25660	. . . . . 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 554	. . . . 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 25511	. . . . 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 3018	. . . 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 y "> ) /\ q e. P ) /\ ( ( D L E ) (⟂G ` G ) ( q L y ) /\ q ( (hpG ` G ) ` ( D L E ) ) F ) ) -> E. f e. P ( <" A B C "> (cgrG ` G ) <" D E f "> /\ f ( (hpG ` G ) ` ( D L E ) ) F ) )
179		trgcopy.2	. . . . . . . . 9 |- ( ph -> -. ( D e. ( E L F ) \/ E = F ) )
180	1, 33, 32, 4, 24, 170, 20, 179	ncolrot2 25458	. . . . . . . 8 |- ( ph -> -. ( F e. ( D L E ) \/ D = E ) )
181		ioran 511	. . . . . . . 8 |- ( -. ( F e. ( D L E ) \/ D = E ) <-> ( -. F e. ( D L E ) /\ -. D = E ) )
182	180, 181	sylib 208	. . . . . . 7 |- ( ph -> ( -. F e. ( D L E ) /\ -. D = E ) )
183	182	simpld 475	. . . . . 6 |- ( ph -> -. F e. ( D L E ) )
184	183	ad4antr 768	. . . . 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 "> ) -> -. F e. ( D L E ) )
185	1, 2, 32, 33, 6, 36, 130, 145, 85, 171, 184	lnperpex 25695	. . . 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 y "> ) -> E. q e. P ( ( D L E ) (⟂G ` G ) ( q L y ) /\ q ( (hpG ` G ) ` ( D L E ) ) F ) )
186	178, 185	r19.29a 3078	. . 3 |- ( ( ( ( ( ph /\ 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. f e. P ( <" A B C "> (cgrG ` G ) <" D E f "> /\ f ( (hpG ` G ) ` ( D L E ) ) F ) )
187	1, 33, 32, 5, 10, 14, 42, 3, 21, 25, 2, 77, 30	lnext 25462	. . 3 |- ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) (⟂G ` G ) ( A L B ) ) -> E. y e. P <" A B x "> (cgrG ` G ) <" D E y "> )
188	186, 187	r19.29a 3078	. 2 |- ( ( ( ph /\ x e. ( A L B ) ) /\ ( C L x ) (⟂G ` G ) ( A L B ) ) -> E. f e. P ( <" A B C "> (cgrG ` G ) <" D E f "> /\ f ( (hpG ` G ) ` ( D L E ) ) F ) )
189	1, 2, 32, 33, 4, 39, 17, 60	footex 25613	. 2 |- ( ph -> E. x e. ( A L B ) ( C L x ) (⟂G ` G ) ( A L B ) )
190	188, 189	r19.29a 3078	1 |- ( ph -> E. f e. P ( <" A B C "> (cgrG ` G ) <" D E f "> /\ f ( (hpG ` G ) ` ( D L E ) ) F ) )

Syntax hints:   -. wn 3   -> wi 4   \/ wo 383   /\ wa 384   = wceq 1483   e. wcel 1990   =/= wne 2794   E.wrex 2913   \ cdif 3571   class class class wbr 4653   {copab 4712   ran crn 5115   ` cfv 5888  (class class class)co 6650   2c2 11070   <"cs3 13587   Basecbs 15857   distcds 15950  TarskiGcstrkg 25329  Dim_TarskiG≥cstrkgld 25333  Itvcitv 25335  LineGclng 25336  cgrGccgrg 25405  hlGchlg 25495  pInvGcmir 25547  ⟂Gcperpg 25590  hpGchpg 25649

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-cnex 9992  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012  ax-pre-mulgt0 10013

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-fal 1489  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-int 4476  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-om 7066  df-1st 7168  df-2nd 7169  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-1o 7560  df-oadd 7564  df-er 7742  df-map 7859  df-pm 7860  df-en 7956  df-dom 7957  df-sdom 7958  df-fin 7959  df-card 8765  df-cda 8990  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-sub 10268  df-neg 10269  df-nn 11021  df-2 11079  df-3 11080  df-n0 11293  df-xnn0 11364  df-z 11378  df-uz 11688  df-fz 12327  df-fzo 12466  df-hash 13118  df-word 13299  df-concat 13301  df-s1 13302  df-s2 13593  df-s3 13594  df-trkgc 25347  df-trkgb 25348  df-trkgcb 25349  df-trkgld 25351  df-trkg 25352  df-cgrg 25406  df-ismt 25428  df-leg 25478  df-hlg 25496  df-mir 25548  df-rag 25589  df-perpg 25591  df-hpg 25650  df-mid 25666  df-lmi 25667

This theorem is referenced by:  trgcopyeu  25698  acopy  25724  cgrg3col4  25734