MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  footex Structured version   Visualization version   Unicode version
Theorem footex 25613
Description: Lemma for foot 25614: existence part. (Contributed by Thierry Arnoux, 19-Oct-2019.)
Hypotheses
Ref Expression
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
Ref Expression
footex |- ( ph -> E. x e. A ( C L x ) (⟂G ` G ) A )
Distinct variable groups:   x, A   x, G   ph, x   x, C   x, I   x, .-   x, L   x, P
Proof of Theorem footex
Dummy variables a b d p q y z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 isperp.p . . . . . . . . 9 |- P = ( Base ` G )
2 isperp.d . . . . . . . . 9 |- .- = ( dist ` G )
3 isperp.i . . . . . . . . 9 |- I = (Itv ` G )
4 isperp.l . . . . . . . . 9 |- L = (LineG ` G )
5 eqid 2622 . . . . . . . . 9 |- (pInvG ` G ) = (pInvG ` G )
6 isperp.g . . . . . . . . . . . . . . 15 |- ( ph -> G e. TarskiG )
76ad3antrrr 766 . . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) -> G e. TarskiG )
87ad2antrr 762 . . . . . . . . . . . . 13 |- ( ( ( ( ( ( ph /\ 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 )
98ad2antrr 762 . . . . . . . . . . . 12 |- ( ( ( ( ( ( ( ( ph /\ 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 )
109ad2antrr 762 . . . . . . . . . . 11 |- ( ( ( ( ( ( ( ( ( ( ph /\ 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 )
1110ad2antrr 762 . . . . . . . . . 10 |- ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 )
1211ad2antrr 762 . . . . . . . . 9 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 )
13 eqid 2622 . . . . . . . . 9 |- ( (pInvG ` G ) ` x ) = ( (pInvG ` G ) ` x )
14 foot.x . . . . . . . . . . . . 13 |- ( ph -> C e. P )
1514ad3antrrr 766 . . . . . . . . . . . 12 |- ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) -> C e. P )
1615ad2antrr 762 . . . . . . . . . . 11 |- ( ( ( ( ( ( ph /\ 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 )
1716ad6antr 772 . . . . . . . . . 10 |- ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 )
1817ad2antrr 762 . . . . . . . . 9 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 792 . . . . . . . . 9 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 807 . . . . . . . . . . . 12 |- ( ( ( ( ( ( ( ( ph /\ 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 )
2120ad2antrr 762 . . . . . . . . . . 11 |- ( ( ( ( ( ( ( ( ( ( ph /\ 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 )
2221ad2antrr 762 . . . . . . . . . 10 |- ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 )
2322ad2antrr 762 . . . . . . . . 9 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 796 . . . . . . . . . 10 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 ) )
2524eqcomd 2628 . . . . . . . . 9 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 ) )
261, 2, 3, 4, 5, 12, 13, 18, 19, 23, 25midexlem 25587 . . . . . . . 8 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 ) )
2712adantr 481 . . . . . . . . . . . . 13 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 )
2823adantr 481 . . . . . . . . . . . . 13 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 )
29 simp-6r 811 . . . . . . . . . . . . . 14 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 )
3029adantr 481 . . . . . . . . . . . . 13 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 )
31 simprl 794 . . . . . . . . . . . . 13 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 )
32 simp-4r 807 . . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ( ( ( ( ( ph /\ 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 )
3332ad4antr 768 . . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 )
3433adantr 481 . . . . . . . . . . . . . 14 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 )
35 simp-5r 809 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 ) ) )
3635simprd 479 . . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 ) )
3736eqcomd 2628 . . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 ) )
3837adantr 481 . . . . . . . . . . . . . 14 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 ) )
39 simp-7r 813 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 ) )
4039adantr 481 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 ) )
41 simpllr 799 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) -> a e. P )
4241ad2antrr 762 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ( ( ph /\ 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 )
4342ad2antrr 762 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ( ( ( ( ph /\ 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 )
4443ad2antrr 762 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ( ( ( ( ( ( ph /\ 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 )
4544ad4antr 768 . . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 )
46 simplr 792 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) -> b e. P )
4746ad10antr 780 . . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 )
48 simp-11r 821 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 ) )
4948simprd 479 . . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 )
5049necomd 2849 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 )
51 simp-9r 817 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 ) ) )
5251simpld 475 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 ) )
531, 3, 4, 12, 47, 45, 23, 50, 52btwnlng3 25516 . . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 ) )
541, 3, 4, 12, 45, 47, 23, 49, 53lncom 25517 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 ) )
5548simpld 475 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 ) )
5654, 55eleqtrrd 2704 . . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 )
5756adantr 481 . . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 )
58 foot.y . . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> -. C e. A )
5958ad3antrrr 766 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) -> -. C e. A )
6059ad10antr 780 . . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 )
6160adantr 481 . . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 )
62 nelne2 2891 . . . . . . . . . . . . . . . . . . 19 |- ( ( y e. A /\ -. C e. A ) -> y =/= C )
6357, 61, 62syl2anc 693 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 )
6463necomd 2849 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 )
6540, 64eqnetrrd 2862 . . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 )
66 eqid 2622 . . . . . . . . . . . . . . . . . 18 |- ( (pInvG ` G ) ` p ) = ( (pInvG ` G ) ` p )
671, 2, 3, 4, 5, 27, 34, 66, 28mirinv 25561 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 ) )
6867necon3bid 2838 . . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 ) )
6965, 68mpbid 222 . . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 )
7069necomd 2849 . . . . . . . . . . . . . 14 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 )
711, 2, 3, 27, 28, 34, 28, 30, 38, 70tgcgrneq 25378 . . . . . . . . . . . . 13 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 )
7271necomd 2849 . . . . . . . . . . . . . 14 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 )
73 eqid 2622 . . . . . . . . . . . . . . 15 |- ( (pInvG ` G ) ` z ) = ( (pInvG ` G ) ` z )
74 simp-4r 807 . . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 )
7574adantr 481 . . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 )
76 simp-4r 807 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 )
77 simplr 792 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 )
781, 2, 3, 4, 5, 11, 76, 73, 77mircl 25556 . . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 )
7978ad3antrrr 766 . . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 )
8018adantr 481 . . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 )
81 simpllr 799 . . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 )
821, 2, 3, 4, 5, 27, 34, 66, 28mirbtwn 25553 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 ) )
8340oveq1d 6665 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 ) )
8482, 83eleqtrrd 2704 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 ) )
85 simpllr 799 . . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 ) ) )
8685simpld 475 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 ) )
8786adantr 481 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 ) )
881, 2, 3, 27, 80, 34, 28, 75, 69, 84, 87tgbtwnouttr2 25390 . . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 ) )
891, 2, 3, 27, 80, 28, 75, 88tgbtwncom 25383 . . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 ) )
90 simplrl 800 . . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 ) )
91 eqid 2622 . . . . . . . . . . . . . . . . . . 19 |- (cgrG ` G ) = (cgrG ` G )
9251simprd 479 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 ) )
9339oveq2d 6666 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 ) ) )
9492, 93eqtrd 2656 . . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 ) ) )
951, 2, 3, 4, 5, 12, 45, 33, 23israg 25592 . . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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. (∟G ` G ) <-> ( a .- y ) = ( a .- ( ( (pInvG ` G ) ` p ) ` y ) ) ) )
9694, 95mpbird 247 . . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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. (∟G ` G ) )
9785simprd 479 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 ) )
981, 2, 3, 12, 45, 23, 45, 18, 92tgcgrcomlr 25375 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 ) )
9997, 98eqtr2d 2657 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 ) )
1001, 3, 4, 12, 45, 47, 49tglinerflx1 25528 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 ) )
101100, 55eleqtrrd 2704 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 )
102 nelne2 2891 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( a e. A /\ -. C e. A ) -> a =/= C )
103101, 60, 102syl2anc 693 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 )
104103necomd 2849 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 )
1051, 2, 3, 12, 18, 45, 23, 74, 99, 104tgcgrneq 25378 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 )
106105necomd 2849 . . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 )
1071, 2, 3, 12, 33, 23, 74, 86tgbtwncom 25383 . . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 ) )
10835simpld 475 . . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 ) )
1091, 2, 3, 12, 23, 74, 23, 45, 97tgcgrcomlr 25375 . . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 ) )
1101, 2, 3, 12, 74, 45axtgcgrrflx 25361 . . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 ) )
11197eqcomd 2628 . . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 ) )
1121, 2, 3, 12, 74, 23, 33, 45, 23, 29, 45, 74, 106, 107, 108, 109, 37, 110, 111axtg5seg 25364 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 ) )
1131, 2, 3, 12, 33, 45, 29, 74, 112tgcgrcomlr 25375 . . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 ) )
1141, 2, 3, 12, 23, 33, 23, 29, 37tgcgrcomlr 25375 . . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 ) )
1151, 2, 91, 12, 45, 33, 23, 74, 29, 23, 113, 114, 111trgcgr 25411 . . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 "> )
1161, 2, 3, 4, 5, 12, 45, 33, 23, 91, 74, 29, 23, 96, 115ragcgr 25602 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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. (∟G ` G ) )
1171, 2, 3, 4, 5, 12, 74, 29, 23, 116ragcom 25593 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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. (∟G ` G ) )
1181, 2, 3, 4, 5, 12, 23, 29, 74israg 25592 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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. (∟G ` G ) <-> ( y .- q ) = ( y .- ( ( (pInvG ` G ) ` z ) ` q ) ) ) )
119117, 118mpbid 222 . . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 ) ) )
120119adantr 481 . . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 ) ) )
12125adantr 481 . . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 ) )
122 eqidd 2623 . . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 ) )
123 simprr 796 . . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 ) )
1241, 2, 3, 4, 5, 27, 73, 13, 75, 79, 28, 80, 81, 30, 31, 89, 90, 120, 121, 122, 123krippen 25586 . . . . . . . . . . . . . 14 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 ) )
1251, 3, 4, 27, 30, 28, 31, 72, 124btwnlng3 25516 . . . . . . . . . . . . 13 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 ) )
1261, 3, 4, 27, 28, 30, 31, 71, 125lncom 25517 . . . . . . . . . . . 12 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 ) )
127 isperp.a . . . . . . . . . . . . . . 15 |- ( ph -> A e. ran L )
128127ad5antr 770 . . . . . . . . . . . . . 14 |- ( ( ( ( ( ( ph /\ 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 )
129128ad9antr 778 . . . . . . . . . . . . 13 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 )
13045adantr 481 . . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 )
13192adantr 481 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 ) )
132131eqcomd 2628 . . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 ) )
133103adantr 481 . . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 )
1341, 2, 3, 27, 130, 80, 130, 28, 132, 133tgcgrneq 25378 . . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 )
135108adantr 481 . . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 ) )
1361, 3, 4, 27, 130, 28, 30, 134, 135btwnlng3 25516 . . . . . . . . . . . . . 14 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 ) )
137101adantr 481 . . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 )
1381, 3, 4, 27, 130, 28, 134, 134, 129, 137, 57tglinethru 25531 . . . . . . . . . . . . . 14 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 ) )
139136, 138eleqtrrd 2704 . . . . . . . . . . . . 13 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 )
1401, 3, 4, 27, 28, 30, 71, 71, 129, 57, 139tglinethru 25531 . . . . . . . . . . . 12 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 ) )
141126, 140eleqtrrd 2704 . . . . . . . . . . 11 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 2891 . . . . . . . . . . . . . . 15 |- ( ( x e. A /\ -. C e. A ) -> x =/= C )
143141, 61, 142syl2anc 693 . . . . . . . . . . . . . 14 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 )
144143necomd 2849 . . . . . . . . . . . . 13 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 )
1451, 3, 4, 27, 80, 31, 144tgelrnln 25525 . . . . . . . . . . . 12 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 )
1461, 3, 4, 27, 80, 31, 144tglinerflx2 25529 . . . . . . . . . . . . 13 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 ) )
147146, 141elind 3798 . . . . . . . . . . . 12 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 ) )
1481, 3, 4, 27, 80, 31, 144tglinerflx1 25528 . . . . . . . . . . . 12 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 ) )
14927adantr 481 . . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 )
150130adantr 481 . . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 )
15128adantr 481 . . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 )
15234adantr 481 . . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 )
15380adantr 481 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 2623 . . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 477 . . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 2623 . . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 )
157154, 155, 156s3eqd 13609 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 "> )
15831adantr 481 . . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 )
15930adantr 481 . . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 )
160106adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 )
1611, 2, 3, 27, 28, 75, 28, 79, 120tgcgrcomlr 25375 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 ) )
1621, 2, 3, 4, 5, 27, 30, 73, 75mircgr 25552 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 ) )
163162eqcomd 2628 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 ) ) )
1641, 2, 3, 27, 30, 75, 30, 79, 163tgcgrcomlr 25375 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 2623 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 ) )
1661, 2, 3, 27, 75, 28, 80, 79, 28, 81, 30, 30, 160, 89, 90, 161, 121, 164, 165axtg5seg 25364 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 ) )
1671, 2, 3, 27, 80, 30, 81, 30, 166tgcgrcomlr 25375 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 ) )
168123oveq2d 6666 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 ) ) )
169167, 168eqtrd 2656 . . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 ) ) )
1701, 2, 3, 4, 5, 27, 30, 31, 80israg 25592 . . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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. (∟G ` G ) <-> ( z .- C ) = ( z .- ( ( (pInvG ` G ) ` x ) ` C ) ) ) )
171169, 170mpbird 247 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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. (∟G ` G ) )
172171adantr 481 . . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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. (∟G ` G ) )
17372adantr 481 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 )
174173, 155neeqtrd 2863 . . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 )
175132adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 ) )
176133adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 )
1771, 2, 3, 149, 150, 153, 150, 151, 175, 176tgcgrneq 25378 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 )
178177necomd 2849 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 )
179136adantr 481 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 ) )
1801, 3, 4, 149, 151, 150, 159, 178, 179lncom 25517 . . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 ) )
181155oveq1d 6665 . . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 ) )
182180, 181eleqtrd 2703 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 ) )
183182orcd 407 . . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 ) )
1841, 2, 3, 4, 5, 149, 159, 158, 153, 150, 172, 174, 183ragcol 25594 . . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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. (∟G ` G ) )
1851, 2, 3, 4, 5, 149, 150, 158, 153, 184ragcom 25593 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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. (∟G ` G ) )
186157, 185eqeltrd 2701 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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. (∟G ` G ) )
18764adantr 481 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 )
1881, 2, 3, 27, 80, 34, 28, 84tgbtwncom 25383 . . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 ) )
1891, 4, 3, 27, 28, 34, 80, 188btwncolg3 25452 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 ) )
190189adantr 481 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 ) )
1911, 2, 3, 4, 5, 149, 153, 151, 150, 152, 186, 187, 190ragcol 25594 . . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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. (∟G ` G ) )
1921, 2, 3, 4, 5, 149, 152, 151, 150, 191ragcom 25593 . . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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. (∟G ` G ) )
19396ad2antrr 762 . . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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. (∟G ` G ) )
1941, 2, 3, 4, 5, 149, 150, 151, 152, 192, 193ragflat 25599 . . . . . . . . . . . . . 14 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 )
19570adantr 481 . . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 )
196195neneqd 2799 . . . . . . . . . . . . . 14 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 )
197194, 196pm2.65da 600 . . . . . . . . . . . . 13 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 )
198197neqned 2801 . . . . . . . . . . . 12 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 )
199123oveq2d 6666 . . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 ) ) )
200121, 199eqtrd 2656 . . . . . . . . . . . . . 14 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 ) ) )
2011, 2, 3, 4, 5, 27, 28, 31, 80israg 25592 . . . . . . . . . . . . . 14 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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. (∟G ` G ) <-> ( y .- C ) = ( y .- ( ( (pInvG ` G ) ` x ) ` C ) ) ) )
202200, 201mpbird 247 . . . . . . . . . . . . 13 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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. (∟G ` G ) )
2031, 2, 3, 4, 5, 27, 28, 31, 80, 202ragcom 25593 . . . . . . . . . . . 12 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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. (∟G ` G ) )
2041, 2, 3, 4, 27, 145, 129, 147, 148, 57, 144, 198, 203ragperp 25612 . . . . . . . . . . 11 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 ) (⟂G ` G ) A )
205141, 204jca 554 . . . . . . . . . 10 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 /\ ( C L x ) (⟂G ` G ) A ) )
206205ex 450 . . . . . . . . 9 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 /\ ( C L x ) (⟂G ` G ) A ) ) )
207206reximdv2 3014 . . . . . . . 8 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 ) -> E. x e. A ( C L x ) (⟂G ` G ) A ) )
20826, 207mpd 15 . . . . . . 7 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 ) (⟂G ` G ) A )
2091, 2, 3, 11, 78, 22, 22, 17axtgsegcon 25363 . . . . . . 7 |- ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 ) ) )
210208, 209r19.29a 3078 . . . . . 6 |- ( ( ( ( ( ( ( ( ( ( ( ( ph /\ 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 ) (⟂G ` G ) A )
2111, 2, 3, 10, 32, 21, 21, 44axtgsegcon 25363 . . . . . 6 |- ( ( ( ( ( ( ( ( ( ( ph /\ 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 ) ) )
212210, 211r19.29a 3078 . . . . 5 |- ( ( ( ( ( ( ( ( ( ( ph /\ 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 ) (⟂G ` G ) A )
213 simplr 792 . . . . . 6 |- ( ( ( ( ( ( ( ( ph /\ 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 )
2141, 2, 3, 9, 43, 20, 20, 213axtgsegcon 25363 . . . . 5 |- ( ( ( ( ( ( ( ( ph /\ 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 ) ) )
215212, 214r19.29a 3078 . . . 4 |- ( ( ( ( ( ( ( ( ph /\ 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 ) (⟂G ` G ) A )
216 simplr 792 . . . . 5 |- ( ( ( ( ( ( ph /\ 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 )
217 simprr 796 . . . . 5 |- ( ( ( ( ( ( ph /\ 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 ) )
2181, 2, 3, 4, 5, 8, 66, 216, 16, 42, 217midexlem 25587 . . . 4 |- ( ( ( ( ( ( ph /\ 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 ) )
219215, 218r19.29a 3078 . . 3 |- ( ( ( ( ( ( ph /\ 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 ) (⟂G ` G ) A )
2201, 2, 3, 7, 46, 41, 41, 15axtgsegcon 25363 . . 3 |- ( ( ( ( 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 ) ) )
221219, 220r19.29a 3078 . 2 |- ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) -> E. x e. A ( C L x ) (⟂G ` G ) A )
2221, 3, 4, 6, 127tgisline 25522 . 2 |- ( ph -> E. a e. P E. b e. P ( A = ( a L b ) /\ a =/= b ) )
223221, 222r19.29vva 3081 1 |- ( ph -> E. x e. A ( C L x ) (⟂G ` G ) A )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3   -> wi 4   \/ wo 383   /\ wa 384   = wceq 1483   e. wcel 1990   =/= wne 2794   E.wrex 2913   class class class wbr 4653   ran crn 5115   ` cfv 5888  (class class class)co 6650   <"cs3 13587   Basecbs 15857   distcds 15950  TarskiGcstrkg 25329  Itvcitv 25335  LineGclng 25336  cgrGccgrg 25405  pInvGcmir 25547  ∟Gcrag 25588  ⟂Gcperpg 25590
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-cnex 9992  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012  ax-pre-mulgt0 10013
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-int 4476  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-om 7066  df-1st 7168  df-2nd 7169  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-1o 7560  df-oadd 7564  df-er 7742  df-map 7859  df-pm 7860  df-en 7956  df-dom 7957  df-sdom 7958  df-fin 7959  df-card 8765  df-cda 8990  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-sub 10268  df-neg 10269  df-nn 11021  df-2 11079  df-3 11080  df-n0 11293  df-xnn0 11364  df-z 11378  df-uz 11688  df-fz 12327  df-fzo 12466  df-hash 13118  df-word 13299  df-concat 13301  df-s1 13302  df-s2 13593  df-s3 13594  df-trkgc 25347  df-trkgb 25348  df-trkgcb 25349  df-trkg 25352  df-cgrg 25406  df-leg 25478  df-mir 25548  df-rag 25589  df-perpg 25591
This theorem is referenced by:  foot  25614  colperpexlem3  25624  opphl  25646  lmieu  25676  trgcopy  25696
  Copyright terms: Public domain W3C validator