Theorem footexALT

Description: Alternative version of footex which minimization requires a notably long time. (Contributed by Thierry Arnoux, 19-Oct-2019) (New usage is discouraged.) (Proof modification is discouraged.)

	Ref	Expression
Hypotheses	isperp.p	|- P = ( Base ` G )
	isperp.d	|- .- = ( dist ` G )
	isperp.i	|- I = ( Itv ` G )
	isperp.l	|- L = ( LineG ` G )
	isperp.g	|- ( ph -> G e. TarskiG )
	isperp.a	|- ( ph -> A e. ran L )
	foot.x	|- ( ph -> C e. P )
	foot.y	|- ( ph -> -. C e. A )
Assertion	footexALT	|- ( ph -> E. x e. A ( C L x ) ( perpG ` G ) A )

Proof

Step	Hyp	Ref	Expression
1		isperp.p	|- P = ( Base ` G )
2		isperp.d	|- .- = ( dist ` G )
3		isperp.i	|- I = ( Itv ` G )
4		isperp.l	|- L = ( LineG ` G )
5		isperp.g	|- ( ph -> G e. TarskiG )
6		isperp.a	|- ( ph -> A e. ran L )
7		foot.x	|- ( ph -> C e. P )
8		foot.y	|- ( ph -> -. C e. A )
9		eqid	|- ( pInvG ` G ) = ( pInvG ` G )
10	5	ad3antrrr	|- ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) -> G e. TarskiG )
11	10	ad2antrr	|- ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) -> G e. TarskiG )
12	11	ad2antrr	|- ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) -> G e. TarskiG )
13	12	ad2antrr	|- ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) -> G e. TarskiG )
14	13	ad2antrr	|- ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) -> G e. TarskiG )
15	14	ad2antrr	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) -> G e. TarskiG )
16		eqid	|- ( ( pInvG ` G ) ` x ) = ( ( pInvG ` G ) ` x )
17	7	ad3antrrr	|- ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) -> C e. P )
18	17	ad2antrr	|- ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) -> C e. P )
19	18	ad6antr	|- ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) -> C e. P )
20	19	ad2antrr	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) -> C e. P )
21		simplr	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) -> d e. P )
22		simp-4r	|- ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) -> y e. P )
23	22	ad2antrr	|- ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) -> y e. P )
24	23	ad2antrr	|- ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) -> y e. P )
25	24	ad2antrr	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) -> y e. P )
26		simprr	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) -> ( y .- d ) = ( y .- C ) )
27	26	eqcomd	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) -> ( y .- C ) = ( y .- d ) )
28	1 2 3 4 9 15 16 20 21 25 27	midexlem	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) -> E. x e. P d = ( ( ( pInvG ` G ) ` x ) ` C ) )
29	15	adantr	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) /\ ( x e. P /\ d = ( ( ( pInvG ` G ) ` x ) ` C ) ) ) -> G e. TarskiG )
30	25	adantr	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) /\ ( x e. P /\ d = ( ( ( pInvG ` G ) ` x ) ` C ) ) ) -> y e. P )
31		simp-6r	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) -> z e. P )
32	31	adantr	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) /\ ( x e. P /\ d = ( ( ( pInvG ` G ) ` x ) ` C ) ) ) -> z e. P )
33		simprl	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) /\ ( x e. P /\ d = ( ( ( pInvG ` G ) ` x ) ` C ) ) ) -> x e. P )
34		simp-4r	|- ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) -> p e. P )
35	34	ad4antr	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) -> p e. P )
36	35	adantr	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) /\ ( x e. P /\ d = ( ( ( pInvG ` G ) ` x ) ` C ) ) ) -> p e. P )
37		simp-5r	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) -> ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) )
38	37	simprd	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) -> ( y .- z ) = ( y .- p ) )
39	38	eqcomd	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) -> ( y .- p ) = ( y .- z ) )
40	39	adantr	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) /\ ( x e. P /\ d = ( ( ( pInvG ` G ) ` x ) ` C ) ) ) -> ( y .- p ) = ( y .- z ) )
41		simp-7r	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) -> C = ( ( ( pInvG ` G ) ` p ) ` y ) )
42	41	adantr	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) /\ ( x e. P /\ d = ( ( ( pInvG ` G ) ` x ) ` C ) ) ) -> C = ( ( ( pInvG ` G ) ` p ) ` y ) )
43		simpllr	|- ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) -> a e. P )
44	43	ad2antrr	|- ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) -> a e. P )
45	44	ad2antrr	|- ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) -> a e. P )
46	45	ad2antrr	|- ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) -> a e. P )
47	46	ad4antr	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) -> a e. P )
48		simplr	|- ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) -> b e. P )
49	48	ad10antr	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) -> b e. P )
50		simp-11r	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) -> ( A = ( a L b ) /\ a =/= b ) )
51	50	simprd	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) -> a =/= b )
52	51	necomd	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) -> b =/= a )
53		simp-9r	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) -> ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) )
54	53	simpld	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) -> a e. ( b I y ) )
55	1 3 4 15 49 47 25 52 54	btwnlng3	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) -> y e. ( b L a ) )
56	1 3 4 15 47 49 25 51 55	lncom	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) -> y e. ( a L b ) )
57	50	simpld	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) -> A = ( a L b ) )
58	56 57	eleqtrrd	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) -> y e. A )
59	58	adantr	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) /\ ( x e. P /\ d = ( ( ( pInvG ` G ) ` x ) ` C ) ) ) -> y e. A )
60	8	ad3antrrr	|- ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) -> -. C e. A )
61	60	ad10antr	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) -> -. C e. A )
62	61	adantr	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) /\ ( x e. P /\ d = ( ( ( pInvG ` G ) ` x ) ` C ) ) ) -> -. C e. A )
63		nelne2	|- ( ( y e. A /\ -. C e. A ) -> y =/= C )
64	59 62 63	syl2anc	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) /\ ( x e. P /\ d = ( ( ( pInvG ` G ) ` x ) ` C ) ) ) -> y =/= C )
65	64	necomd	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) /\ ( x e. P /\ d = ( ( ( pInvG ` G ) ` x ) ` C ) ) ) -> C =/= y )
66	42 65	eqnetrrd	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) /\ ( x e. P /\ d = ( ( ( pInvG ` G ) ` x ) ` C ) ) ) -> ( ( ( pInvG ` G ) ` p ) ` y ) =/= y )
67		eqid	|- ( ( pInvG ` G ) ` p ) = ( ( pInvG ` G ) ` p )
68	1 2 3 4 9 29 36 67 30	mirinv	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) /\ ( x e. P /\ d = ( ( ( pInvG ` G ) ` x ) ` C ) ) ) -> ( ( ( ( pInvG ` G ) ` p ) ` y ) = y <-> p = y ) )
69	68	necon3bid	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) /\ ( x e. P /\ d = ( ( ( pInvG ` G ) ` x ) ` C ) ) ) -> ( ( ( ( pInvG ` G ) ` p ) ` y ) =/= y <-> p =/= y ) )
70	66 69	mpbid	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) /\ ( x e. P /\ d = ( ( ( pInvG ` G ) ` x ) ` C ) ) ) -> p =/= y )
71	70	necomd	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) /\ ( x e. P /\ d = ( ( ( pInvG ` G ) ` x ) ` C ) ) ) -> y =/= p )
72	1 2 3 29 30 36 30 32 40 71	tgcgrneq	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) /\ ( x e. P /\ d = ( ( ( pInvG ` G ) ` x ) ` C ) ) ) -> y =/= z )
73	72	necomd	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) /\ ( x e. P /\ d = ( ( ( pInvG ` G ) ` x ) ` C ) ) ) -> z =/= y )
74		eqid	|- ( ( pInvG ` G ) ` z ) = ( ( pInvG ` G ) ` z )
75		simp-4r	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) -> q e. P )
76	75	adantr	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) /\ ( x e. P /\ d = ( ( ( pInvG ` G ) ` x ) ` C ) ) ) -> q e. P )
77		simp-4r	|- ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) -> z e. P )
78		simplr	|- ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) -> q e. P )
79	1 2 3 4 9 14 77 74 78	mircl	|- ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) -> ( ( ( pInvG ` G ) ` z ) ` q ) e. P )
80	79	ad3antrrr	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) /\ ( x e. P /\ d = ( ( ( pInvG ` G ) ` x ) ` C ) ) ) -> ( ( ( pInvG ` G ) ` z ) ` q ) e. P )
81	20	adantr	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) /\ ( x e. P /\ d = ( ( ( pInvG ` G ) ` x ) ` C ) ) ) -> C e. P )
82		simpllr	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) /\ ( x e. P /\ d = ( ( ( pInvG ` G ) ` x ) ` C ) ) ) -> d e. P )
83	1 2 3 4 9 29 36 67 30	mirbtwn	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) /\ ( x e. P /\ d = ( ( ( pInvG ` G ) ` x ) ` C ) ) ) -> p e. ( ( ( ( pInvG ` G ) ` p ) ` y ) I y ) )
84	42	oveq1d	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) /\ ( x e. P /\ d = ( ( ( pInvG ` G ) ` x ) ` C ) ) ) -> ( C I y ) = ( ( ( ( pInvG ` G ) ` p ) ` y ) I y ) )
85	83 84	eleqtrrd	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) /\ ( x e. P /\ d = ( ( ( pInvG ` G ) ` x ) ` C ) ) ) -> p e. ( C I y ) )
86		simpllr	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) -> ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) )
87	86	simpld	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) -> y e. ( p I q ) )
88	87	adantr	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) /\ ( x e. P /\ d = ( ( ( pInvG ` G ) ` x ) ` C ) ) ) -> y e. ( p I q ) )
89	1 2 3 29 81 36 30 76 70 85 88	tgbtwnouttr2	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) /\ ( x e. P /\ d = ( ( ( pInvG ` G ) ` x ) ` C ) ) ) -> y e. ( C I q ) )
90	1 2 3 29 81 30 76 89	tgbtwncom	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) /\ ( x e. P /\ d = ( ( ( pInvG ` G ) ` x ) ` C ) ) ) -> y e. ( q I C ) )
91		simplrl	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) /\ ( x e. P /\ d = ( ( ( pInvG ` G ) ` x ) ` C ) ) ) -> y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) )
92		eqid	|- ( cgrG ` G ) = ( cgrG ` G )
93	53	simprd	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) -> ( a .- y ) = ( a .- C ) )
94	41	oveq2d	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) -> ( a .- C ) = ( a .- ( ( ( pInvG ` G ) ` p ) ` y ) ) )
95	93 94	eqtrd	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) -> ( a .- y ) = ( a .- ( ( ( pInvG ` G ) ` p ) ` y ) ) )
96	1 2 3 4 9 15 47 35 25	israg	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) -> ( <" a p y "> e. ( raG ` G ) <-> ( a .- y ) = ( a .- ( ( ( pInvG ` G ) ` p ) ` y ) ) ) )
97	95 96	mpbird	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) -> <" a p y "> e. ( raG ` G ) )
98	86	simprd	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) -> ( y .- q ) = ( y .- a ) )
99	1 2 3 15 47 25 47 20 93	tgcgrcomlr	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) -> ( y .- a ) = ( C .- a ) )
100	98 99	eqtr2d	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) -> ( C .- a ) = ( y .- q ) )
101	1 3 4 15 47 49 51	tglinerflx1	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) -> a e. ( a L b ) )
102	101 57	eleqtrrd	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) -> a e. A )
103		nelne2	|- ( ( a e. A /\ -. C e. A ) -> a =/= C )
104	102 61 103	syl2anc	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) -> a =/= C )
105	104	necomd	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) -> C =/= a )
106	1 2 3 15 20 47 25 75 100 105	tgcgrneq	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) -> y =/= q )
107	106	necomd	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) -> q =/= y )
108	1 2 3 15 35 25 75 87	tgbtwncom	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) -> y e. ( q I p ) )
109	37	simpld	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) -> y e. ( a I z ) )
110	1 2 3 15 25 75 25 47 98	tgcgrcomlr	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) -> ( q .- y ) = ( a .- y ) )
111	1 2 3 15 75 47	axtgcgrrflx	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) -> ( q .- a ) = ( a .- q ) )
112	98	eqcomd	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) -> ( y .- a ) = ( y .- q ) )
113	1 2 3 15 75 25 35 47 25 31 47 75 107 108 109 110 39 111 112	axtg5seg	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) -> ( p .- a ) = ( z .- q ) )
114	1 2 3 15 35 47 31 75 113	tgcgrcomlr	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) -> ( a .- p ) = ( q .- z ) )
115	1 2 3 15 25 35 25 31 39	tgcgrcomlr	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) -> ( p .- y ) = ( z .- y ) )
116	1 2 92 15 47 35 25 75 31 25 114 115 112	trgcgr	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) -> <" a p y "> ( cgrG ` G ) <" q z y "> )
117	1 2 3 4 9 15 47 35 25 92 75 31 25 97 116	ragcgr	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) -> <" q z y "> e. ( raG ` G ) )
118	1 2 3 4 9 15 75 31 25 117	ragcom	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) -> <" y z q "> e. ( raG ` G ) )
119	1 2 3 4 9 15 25 31 75	israg	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) -> ( <" y z q "> e. ( raG ` G ) <-> ( y .- q ) = ( y .- ( ( ( pInvG ` G ) ` z ) ` q ) ) ) )
120	118 119	mpbid	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) -> ( y .- q ) = ( y .- ( ( ( pInvG ` G ) ` z ) ` q ) ) )
121	120	adantr	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) /\ ( x e. P /\ d = ( ( ( pInvG ` G ) ` x ) ` C ) ) ) -> ( y .- q ) = ( y .- ( ( ( pInvG ` G ) ` z ) ` q ) ) )
122	27	adantr	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) /\ ( x e. P /\ d = ( ( ( pInvG ` G ) ` x ) ` C ) ) ) -> ( y .- C ) = ( y .- d ) )
123		eqidd	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) /\ ( x e. P /\ d = ( ( ( pInvG ` G ) ` x ) ` C ) ) ) -> ( ( ( pInvG ` G ) ` z ) ` q ) = ( ( ( pInvG ` G ) ` z ) ` q ) )
124		simprr	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) /\ ( x e. P /\ d = ( ( ( pInvG ` G ) ` x ) ` C ) ) ) -> d = ( ( ( pInvG ` G ) ` x ) ` C ) )
125	1 2 3 4 9 29 74 16 76 80 30 81 82 32 33 90 91 121 122 123 124	krippen	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) /\ ( x e. P /\ d = ( ( ( pInvG ` G ) ` x ) ` C ) ) ) -> y e. ( z I x ) )
126	1 3 4 29 32 30 33 73 125	btwnlng3	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) /\ ( x e. P /\ d = ( ( ( pInvG ` G ) ` x ) ` C ) ) ) -> x e. ( z L y ) )
127	1 3 4 29 30 32 33 72 126	lncom	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) /\ ( x e. P /\ d = ( ( ( pInvG ` G ) ` x ) ` C ) ) ) -> x e. ( y L z ) )
128	6	ad5antr	|- ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) -> A e. ran L )
129	128	ad9antr	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) /\ ( x e. P /\ d = ( ( ( pInvG ` G ) ` x ) ` C ) ) ) -> A e. ran L )
130	47	adantr	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) /\ ( x e. P /\ d = ( ( ( pInvG ` G ) ` x ) ` C ) ) ) -> a e. P )
131	93	adantr	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) /\ ( x e. P /\ d = ( ( ( pInvG ` G ) ` x ) ` C ) ) ) -> ( a .- y ) = ( a .- C ) )
132	131	eqcomd	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) /\ ( x e. P /\ d = ( ( ( pInvG ` G ) ` x ) ` C ) ) ) -> ( a .- C ) = ( a .- y ) )
133	104	adantr	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) /\ ( x e. P /\ d = ( ( ( pInvG ` G ) ` x ) ` C ) ) ) -> a =/= C )
134	1 2 3 29 130 81 130 30 132 133	tgcgrneq	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) /\ ( x e. P /\ d = ( ( ( pInvG ` G ) ` x ) ` C ) ) ) -> a =/= y )
135	109	adantr	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) /\ ( x e. P /\ d = ( ( ( pInvG ` G ) ` x ) ` C ) ) ) -> y e. ( a I z ) )
136	1 3 4 29 130 30 32 134 135	btwnlng3	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) /\ ( x e. P /\ d = ( ( ( pInvG ` G ) ` x ) ` C ) ) ) -> z e. ( a L y ) )
137	102	adantr	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) /\ ( x e. P /\ d = ( ( ( pInvG ` G ) ` x ) ` C ) ) ) -> a e. A )
138	1 3 4 29 130 30 134 134 129 137 59	tglinethru	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) /\ ( x e. P /\ d = ( ( ( pInvG ` G ) ` x ) ` C ) ) ) -> A = ( a L y ) )
139	136 138	eleqtrrd	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) /\ ( x e. P /\ d = ( ( ( pInvG ` G ) ` x ) ` C ) ) ) -> z e. A )
140	1 3 4 29 30 32 72 72 129 59 139	tglinethru	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) /\ ( x e. P /\ d = ( ( ( pInvG ` G ) ` x ) ` C ) ) ) -> A = ( y L z ) )
141	127 140	eleqtrrd	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) /\ ( x e. P /\ d = ( ( ( pInvG ` G ) ` x ) ` C ) ) ) -> x e. A )
142		nelne2	|- ( ( x e. A /\ -. C e. A ) -> x =/= C )
143	141 62 142	syl2anc	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) /\ ( x e. P /\ d = ( ( ( pInvG ` G ) ` x ) ` C ) ) ) -> x =/= C )
144	143	necomd	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) /\ ( x e. P /\ d = ( ( ( pInvG ` G ) ` x ) ` C ) ) ) -> C =/= x )
145	1 3 4 29 81 33 144	tgelrnln	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) /\ ( x e. P /\ d = ( ( ( pInvG ` G ) ` x ) ` C ) ) ) -> ( C L x ) e. ran L )
146	1 3 4 29 81 33 144	tglinerflx2	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) /\ ( x e. P /\ d = ( ( ( pInvG ` G ) ` x ) ` C ) ) ) -> x e. ( C L x ) )
147	146 141	elind	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) /\ ( x e. P /\ d = ( ( ( pInvG ` G ) ` x ) ` C ) ) ) -> x e. ( ( C L x ) i^i A ) )
148	1 3 4 29 81 33 144	tglinerflx1	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) /\ ( x e. P /\ d = ( ( ( pInvG ` G ) ` x ) ` C ) ) ) -> C e. ( C L x ) )
149	29	adantr	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) /\ ( x e. P /\ d = ( ( ( pInvG ` G ) ` x ) ` C ) ) ) /\ y = x ) -> G e. TarskiG )
150	130	adantr	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) /\ ( x e. P /\ d = ( ( ( pInvG ` G ) ` x ) ` C ) ) ) /\ y = x ) -> a e. P )
151	30	adantr	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) /\ ( x e. P /\ d = ( ( ( pInvG ` G ) ` x ) ` C ) ) ) /\ y = x ) -> y e. P )
152	36	adantr	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) /\ ( x e. P /\ d = ( ( ( pInvG ` G ) ` x ) ` C ) ) ) /\ y = x ) -> p e. P )
153	81	adantr	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) /\ ( x e. P /\ d = ( ( ( pInvG ` G ) ` x ) ` C ) ) ) /\ y = x ) -> C e. P )
154		eqidd	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) /\ ( x e. P /\ d = ( ( ( pInvG ` G ) ` x ) ` C ) ) ) /\ y = x ) -> C = C )
155		simpr	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) /\ ( x e. P /\ d = ( ( ( pInvG ` G ) ` x ) ` C ) ) ) /\ y = x ) -> y = x )
156		eqidd	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) /\ ( x e. P /\ d = ( ( ( pInvG ` G ) ` x ) ` C ) ) ) /\ y = x ) -> a = a )
157	154 155 156	s3eqd	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) /\ ( x e. P /\ d = ( ( ( pInvG ` G ) ` x ) ` C ) ) ) /\ y = x ) -> <" C y a "> = <" C x a "> )
158	33	adantr	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) /\ ( x e. P /\ d = ( ( ( pInvG ` G ) ` x ) ` C ) ) ) /\ y = x ) -> x e. P )
159	32	adantr	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) /\ ( x e. P /\ d = ( ( ( pInvG ` G ) ` x ) ` C ) ) ) /\ y = x ) -> z e. P )
160	107	adantr	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) /\ ( x e. P /\ d = ( ( ( pInvG ` G ) ` x ) ` C ) ) ) -> q =/= y )
161	1 2 3 29 30 76 30 80 121	tgcgrcomlr	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) /\ ( x e. P /\ d = ( ( ( pInvG ` G ) ` x ) ` C ) ) ) -> ( q .- y ) = ( ( ( ( pInvG ` G ) ` z ) ` q ) .- y ) )
162	1 2 3 4 9 29 32 74 76	mircgr	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) /\ ( x e. P /\ d = ( ( ( pInvG ` G ) ` x ) ` C ) ) ) -> ( z .- ( ( ( pInvG ` G ) ` z ) ` q ) ) = ( z .- q ) )
163	162	eqcomd	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) /\ ( x e. P /\ d = ( ( ( pInvG ` G ) ` x ) ` C ) ) ) -> ( z .- q ) = ( z .- ( ( ( pInvG ` G ) ` z ) ` q ) ) )
164	1 2 3 29 32 76 32 80 163	tgcgrcomlr	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) /\ ( x e. P /\ d = ( ( ( pInvG ` G ) ` x ) ` C ) ) ) -> ( q .- z ) = ( ( ( ( pInvG ` G ) ` z ) ` q ) .- z ) )
165		eqidd	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) /\ ( x e. P /\ d = ( ( ( pInvG ` G ) ` x ) ` C ) ) ) -> ( y .- z ) = ( y .- z ) )
166	1 2 3 29 76 30 81 80 30 82 32 32 160 90 91 161 122 164 165	axtg5seg	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) /\ ( x e. P /\ d = ( ( ( pInvG ` G ) ` x ) ` C ) ) ) -> ( C .- z ) = ( d .- z ) )
167	1 2 3 29 81 32 82 32 166	tgcgrcomlr	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) /\ ( x e. P /\ d = ( ( ( pInvG ` G ) ` x ) ` C ) ) ) -> ( z .- C ) = ( z .- d ) )
168	124	oveq2d	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) /\ ( x e. P /\ d = ( ( ( pInvG ` G ) ` x ) ` C ) ) ) -> ( z .- d ) = ( z .- ( ( ( pInvG ` G ) ` x ) ` C ) ) )
169	167 168	eqtrd	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) /\ ( x e. P /\ d = ( ( ( pInvG ` G ) ` x ) ` C ) ) ) -> ( z .- C ) = ( z .- ( ( ( pInvG ` G ) ` x ) ` C ) ) )
170	1 2 3 4 9 29 32 33 81	israg	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) /\ ( x e. P /\ d = ( ( ( pInvG ` G ) ` x ) ` C ) ) ) -> ( <" z x C "> e. ( raG ` G ) <-> ( z .- C ) = ( z .- ( ( ( pInvG ` G ) ` x ) ` C ) ) ) )
171	169 170	mpbird	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) /\ ( x e. P /\ d = ( ( ( pInvG ` G ) ` x ) ` C ) ) ) -> <" z x C "> e. ( raG ` G ) )
172	171	adantr	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) /\ ( x e. P /\ d = ( ( ( pInvG ` G ) ` x ) ` C ) ) ) /\ y = x ) -> <" z x C "> e. ( raG ` G ) )
173	73	adantr	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) /\ ( x e. P /\ d = ( ( ( pInvG ` G ) ` x ) ` C ) ) ) /\ y = x ) -> z =/= y )
174	173 155	neeqtrd	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) /\ ( x e. P /\ d = ( ( ( pInvG ` G ) ` x ) ` C ) ) ) /\ y = x ) -> z =/= x )
175	132	adantr	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) /\ ( x e. P /\ d = ( ( ( pInvG ` G ) ` x ) ` C ) ) ) /\ y = x ) -> ( a .- C ) = ( a .- y ) )
176	133	adantr	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) /\ ( x e. P /\ d = ( ( ( pInvG ` G ) ` x ) ` C ) ) ) /\ y = x ) -> a =/= C )
177	1 2 3 149 150 153 150 151 175 176	tgcgrneq	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) /\ ( x e. P /\ d = ( ( ( pInvG ` G ) ` x ) ` C ) ) ) /\ y = x ) -> a =/= y )
178	177	necomd	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) /\ ( x e. P /\ d = ( ( ( pInvG ` G ) ` x ) ` C ) ) ) /\ y = x ) -> y =/= a )
179	136	adantr	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) /\ ( x e. P /\ d = ( ( ( pInvG ` G ) ` x ) ` C ) ) ) /\ y = x ) -> z e. ( a L y ) )
180	1 3 4 149 151 150 159 178 179	lncom	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) /\ ( x e. P /\ d = ( ( ( pInvG ` G ) ` x ) ` C ) ) ) /\ y = x ) -> z e. ( y L a ) )
181	155	oveq1d	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) /\ ( x e. P /\ d = ( ( ( pInvG ` G ) ` x ) ` C ) ) ) /\ y = x ) -> ( y L a ) = ( x L a ) )
182	180 181	eleqtrd	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) /\ ( x e. P /\ d = ( ( ( pInvG ` G ) ` x ) ` C ) ) ) /\ y = x ) -> z e. ( x L a ) )
183	182	orcd	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) /\ ( x e. P /\ d = ( ( ( pInvG ` G ) ` x ) ` C ) ) ) /\ y = x ) -> ( z e. ( x L a ) \/ x = a ) )
184	1 2 3 4 9 149 159 158 153 150 172 174 183	ragcol	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) /\ ( x e. P /\ d = ( ( ( pInvG ` G ) ` x ) ` C ) ) ) /\ y = x ) -> <" a x C "> e. ( raG ` G ) )
185	1 2 3 4 9 149 150 158 153 184	ragcom	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) /\ ( x e. P /\ d = ( ( ( pInvG ` G ) ` x ) ` C ) ) ) /\ y = x ) -> <" C x a "> e. ( raG ` G ) )
186	157 185	eqeltrd	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) /\ ( x e. P /\ d = ( ( ( pInvG ` G ) ` x ) ` C ) ) ) /\ y = x ) -> <" C y a "> e. ( raG ` G ) )
187	65	adantr	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) /\ ( x e. P /\ d = ( ( ( pInvG ` G ) ` x ) ` C ) ) ) /\ y = x ) -> C =/= y )
188	1 2 3 29 81 36 30 85	tgbtwncom	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) /\ ( x e. P /\ d = ( ( ( pInvG ` G ) ` x ) ` C ) ) ) -> p e. ( y I C ) )
189	1 4 3 29 30 36 81 188	btwncolg3	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) /\ ( x e. P /\ d = ( ( ( pInvG ` G ) ` x ) ` C ) ) ) -> ( C e. ( y L p ) \/ y = p ) )
190	189	adantr	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) /\ ( x e. P /\ d = ( ( ( pInvG ` G ) ` x ) ` C ) ) ) /\ y = x ) -> ( C e. ( y L p ) \/ y = p ) )
191	1 2 3 4 9 149 153 151 150 152 186 187 190	ragcol	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) /\ ( x e. P /\ d = ( ( ( pInvG ` G ) ` x ) ` C ) ) ) /\ y = x ) -> <" p y a "> e. ( raG ` G ) )
192	1 2 3 4 9 149 152 151 150 191	ragcom	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) /\ ( x e. P /\ d = ( ( ( pInvG ` G ) ` x ) ` C ) ) ) /\ y = x ) -> <" a y p "> e. ( raG ` G ) )
193	97	ad2antrr	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) /\ ( x e. P /\ d = ( ( ( pInvG ` G ) ` x ) ` C ) ) ) /\ y = x ) -> <" a p y "> e. ( raG ` G ) )
194	1 2 3 4 9 149 150 151 152 192 193	ragflat	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) /\ ( x e. P /\ d = ( ( ( pInvG ` G ) ` x ) ` C ) ) ) /\ y = x ) -> y = p )
195	71	adantr	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) /\ ( x e. P /\ d = ( ( ( pInvG ` G ) ` x ) ` C ) ) ) /\ y = x ) -> y =/= p )
196	195	neneqd	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) /\ ( x e. P /\ d = ( ( ( pInvG ` G ) ` x ) ` C ) ) ) /\ y = x ) -> -. y = p )
197	194 196	pm2.65da	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) /\ ( x e. P /\ d = ( ( ( pInvG ` G ) ` x ) ` C ) ) ) -> -. y = x )
198	197	neqned	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) /\ ( x e. P /\ d = ( ( ( pInvG ` G ) ` x ) ` C ) ) ) -> y =/= x )
199	124	oveq2d	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) /\ ( x e. P /\ d = ( ( ( pInvG ` G ) ` x ) ` C ) ) ) -> ( y .- d ) = ( y .- ( ( ( pInvG ` G ) ` x ) ` C ) ) )
200	122 199	eqtrd	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) /\ ( x e. P /\ d = ( ( ( pInvG ` G ) ` x ) ` C ) ) ) -> ( y .- C ) = ( y .- ( ( ( pInvG ` G ) ` x ) ` C ) ) )
201	1 2 3 4 9 29 30 33 81	israg	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) /\ ( x e. P /\ d = ( ( ( pInvG ` G ) ` x ) ` C ) ) ) -> ( <" y x C "> e. ( raG ` G ) <-> ( y .- C ) = ( y .- ( ( ( pInvG ` G ) ` x ) ` C ) ) ) )
202	200 201	mpbird	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) /\ ( x e. P /\ d = ( ( ( pInvG ` G ) ` x ) ` C ) ) ) -> <" y x C "> e. ( raG ` G ) )
203	1 2 3 4 9 29 30 33 81 202	ragcom	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) /\ ( x e. P /\ d = ( ( ( pInvG ` G ) ` x ) ` C ) ) ) -> <" C x y "> e. ( raG ` G ) )
204	1 2 3 4 29 145 129 147 148 59 144 198 203	ragperp	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) /\ ( x e. P /\ d = ( ( ( pInvG ` G ) ` x ) ` C ) ) ) -> ( C L x ) ( perpG ` G ) A )
205	28 141 204	reximssdv	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) -> E. x e. A ( C L x ) ( perpG ` G ) A )
206	1 2 3 14 79 24 24 19	axtgsegcon	|- ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) -> E. d e. P ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) )
207	205 206	r19.29a	|- ( ( ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) -> E. x e. A ( C L x ) ( perpG ` G ) A )
208	1 2 3 13 34 23 23 46	axtgsegcon	|- ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) -> E. q e. P ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) )
209	207 208	r19.29a	|- ( ( ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) -> E. x e. A ( C L x ) ( perpG ` G ) A )
210		simplr	|- ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) -> p e. P )
211	1 2 3 12 45 22 22 210	axtgsegcon	|- ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) -> E. z e. P ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) )
212	209 211	r19.29a	|- ( ( ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) -> E. x e. A ( C L x ) ( perpG ` G ) A )
213		simplr	|- ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) -> y e. P )
214		simprr	|- ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) -> ( a .- y ) = ( a .- C ) )
215	1 2 3 4 9 11 67 213 18 44 214	midexlem	|- ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) -> E. p e. P C = ( ( ( pInvG ` G ) ` p ) ` y ) )
216	212 215	r19.29a	|- ( ( ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) /\ y e. P ) /\ ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) ) -> E. x e. A ( C L x ) ( perpG ` G ) A )
217	1 2 3 10 48 43 43 17	axtgsegcon	|- ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) -> E. y e. P ( a e. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) )
218	216 217	r19.29a	|- ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) -> E. x e. A ( C L x ) ( perpG ` G ) A )
219	1 3 4 5 6	tgisline	|- ( ph -> E. a e. P E. b e. P ( A = ( a L b ) /\ a =/= b ) )
220	218 219	r19.29vva	|- ( ph -> E. x e. A ( C L x ) ( perpG ` G ) A )