Metamath Proof Explorer

Theorem footex

Description: From a point C outside of a line A , there exists a point x on A such that ( C L x ) is perpendicular to A . This point is unique, see foot . (Contributed by Thierry Arnoux, 19-Oct-2019) (Revised by Thierry Arnoux, 1-Jul-2023)

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 footex 
|- ( 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 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 ) ) ) -> 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 ) ) ) /\ p e. P ) /\ C = ( ( ( pInvG ` G ) ` p ) ` y ) ) -> 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 ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) -> 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 ) ) ) /\ q e. P ) /\ ( y e. ( p I q ) /\ ( y .- q ) = ( y .- a ) ) ) -> 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 ) ) ) /\ d e. P ) /\ ( y e. ( ( ( ( pInvG ` G ) ` z ) ` q ) I d ) /\ ( y .- d ) = ( y .- C ) ) ) -> G e. TarskiG )
15 eqid 
 |-  ( ( pInvG ` G ) ` x ) = ( ( pInvG ` G ) ` x )
16 7 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 ) ) ) -> C e. P )
17 16 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 )
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 ) ) ) /\ 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 )
19 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 )
20 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 )
21 20 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 )
22 21 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 )
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 ) ) ) /\ 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 )
24 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 ) )
25 24 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 ) )
26 1 2 3 4 9 14 15 18 19 23 25 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 ) )
27 12 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 ) ) ) /\ 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 )
28 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 )
29 28 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 )
30 18 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 )
31 8 ad3antrrr 
 |-  ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) -> -. C e. A )
32 31 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 )
33 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 ) ) ) -> -. C e. A )
34 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 ) ) -> a e. P )
35 34 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 )
36 35 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 ) ) ) /\ 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 )
37 simplr 
 |-  ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) -> b e. P )
38 37 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 )
39 38 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 ) ) ) -> b e. P )
40 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 )
41 40 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 ) ) ) /\ 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 )
42 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 )
43 21 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 ) ) ) /\ 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 )
44 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 ) ) ) /\ ( x e. P /\ d = ( ( ( pInvG ` G ) ` x ) ` C ) ) ) -> z e. P )
45 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 )
46 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 ) )
47 46 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 ) )
48 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 = ( a L b ) )
49 46 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 )
50 49 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 =/= b )
51 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 ) ) )
52 51 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 ) )
53 52 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. ( b I y ) )
54 51 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 ) )
55 54 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 ) )
56 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 ) )
57 56 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 ) )
58 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 ) ) )
59 58 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 ) )
60 59 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 ) )
61 58 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 ) )
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 ) ) ) -> ( y .- z ) = ( y .- p ) )
63 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 ) ) ) /\ ( x e. P /\ d = ( ( ( pInvG ` G ) ` x ) ` C ) ) ) -> q e. P )
64 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 ) ) )
65 64 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 ) )
66 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 e. ( p I q ) )
67 64 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 ) )
68 67 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 .- a ) )
69 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 ) )
70 24 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 .- d ) = ( y .- C ) )
71 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 ) )
72 1 2 3 4 27 29 30 33 36 39 41 42 43 44 45 48 50 53 55 57 60 62 63 66 68 69 70 71 footexlem1 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 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 )
73 1 2 3 4 27 29 30 33 36 39 41 42 43 44 45 48 50 53 55 57 60 62 63 66 68 69 70 71 footexlem2 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 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 )
74 26 72 73 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 )
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 ) ) ) -> z e. P )
76 eqid 
 |-  ( ( pInvG ` G ) ` z ) = ( ( pInvG ` G ) ` z )
77 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 )
78 1 2 3 4 9 13 75 76 77 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 )
79 1 2 3 13 78 22 22 17 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 ) ) )
80 74 79 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 )
81 1 2 3 12 40 21 21 35 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 ) ) )
82 80 81 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 )
83 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 )
84 1 2 3 11 34 20 20 83 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 ) ) )
85 82 84 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 )
86 eqid 
 |-  ( ( pInvG ` G ) ` p ) = ( ( pInvG ` G ) ` p )
87 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 )
88 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 ) ) ) -> a e. P )
89 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 ) )
90 1 2 3 4 9 10 86 87 16 88 89 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 ) )
91 85 90 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 )
92 5 ad3antrrr 
 |-  ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) -> G e. TarskiG )
93 simpllr 
 |-  ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) -> a e. P )
94 7 ad3antrrr 
 |-  ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) -> C e. P )
95 1 2 3 92 37 93 93 94 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 ) ) )
96 91 95 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 )
97 1 3 4 5 6 tgisline 
 |-  ( ph -> E. a e. P E. b e. P ( A = ( a L b ) /\ a =/= b ) )
98 96 97 r19.29vva 
 |-  ( ph -> E. x e. A ( C L x ) ( perpG ` G ) A )