MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  footex Structured version   Unicode version
Theorem footex 23249
Description: Lemma for foot 23250: 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 2452 . . . . . . . . 9 |- (pInvG ` G ) = (pInvG ` G )
6 isperp.g . . . . . . . . . . . . . . 15 |- ( ph -> G e. TarskiG )
76ad3antrrr 729 . . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) -> G e. TarskiG )
87ad2antrr 725 . . . . . . . . . . . . 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 725 . . . . . . . . . . . 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 725 . . . . . . . . . . 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 725 . . . . . . . . . 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 725 . . . . . . . . 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 2452 . . . . . . . . 9 |- ( (pInvG ` G ) ` x ) = ( (pInvG ` G ) ` x )
14 foot.x . . . . . . . . . . . . 13 |- ( ph -> C e. P )
1514ad3antrrr 729 . . . . . . . . . . . 12 |- ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) -> C e. P )
1615ad2antrr 725 . . . . . . . . . . 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 735 . . . . . . . . . 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 725 . . . . . . . . 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 754 . . . . . . . . 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 simplr 754 . . . . . . . . . . . . 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 ) ) ) -> y e. P )
2120ad2antrr 725 . . . . . . . . . . . 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 )
2221ad2antrr 725 . . . . . . . . . . 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 )
2322ad2antrr 725 . . . . . . . . . 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 )
2423ad2antrr 725 . . . . . . . . 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 )
25 simprr 756 . . . . . . . . . 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 ) )
2625eqcomd 2460 . . . . . . . . 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 ) )
271, 2, 3, 4, 5, 12, 13, 18, 19, 24, 26midexlem 23224 . . . . . . . 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 ) )
2812adantr 465 . . . . . . . . . . . . 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 )
2924adantr 465 . . . . . . . . . . . . 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 )
30 simp-6r 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 ) ) ) /\ p e. P ) /\ C = ( ( (pInvG ` G ) ` p ) ` y ) ) /\ z e. P ) /\ ( y e. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) ) /\ q e. P ) /\ ( 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 )
3130adantr 465 . . . . . . . . . . . . 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 )
32 simprl 755 . . . . . . . . . . . . 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 )
33 simplr 754 . . . . . . . . . . . . . . . . . . 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 ) ) -> p e. P )
3433ad2antrr 725 . . . . . . . . . . . . . . . . . 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 ) ) ) -> p e. P )
3534ad4antr 731 . . . . . . . . . . . . . . . . 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 ) ) ) -> p e. P )
3635adantr 465 . . . . . . . . . . . . . . . 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 ) ) ) -> p e. P )
37 simp-5r 768 . . . . . . . . . . . . . . . . . . 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. ( a I z ) /\ ( y .- z ) = ( y .- p ) ) )
3837simprd 463 . . . . . . . . . . . . . . . . . 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 .- z ) = ( y .- p ) )
3938eqcomd 2460 . . . . . . . . . . . . . . . . 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 .- p ) = ( y .- z ) )
4039adantr 465 . . . . . . . . . . . . . . . 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 .- p ) = ( y .- z ) )
41 simp-7r 772 . . . . . . . . . . . . . . . . . . . 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 = ( ( (pInvG ` G ) ` p ) ` y ) )
4241adantr 465 . . . . . . . . . . . . . . . . . . 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 = ( ( (pInvG ` G ) ` p ) ` y ) )
43 simpllr 758 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) -> a e. P )
4443ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) -> a e. P )
4544ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) -> a e. P )
4645ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) -> a e. P )
4746ad4antr 731 . . . . . . . . . . . . . . . . . . . . . . . 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. P )
48 simplr 754 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) -> b e. P )
4948ad10antr 743 . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) -> b e. P )
50 simp-11r 780 . . . . . . . . . . . . . . . . . . . . . . . . 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 = ( a L b ) /\ a =/= b ) )
5150simprd 463 . . . . . . . . . . . . . . . . . . . . . . . 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 =/= b )
5251necomd 2720 . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) -> b =/= a )
53 simp-9r 776 . . . . . . . . . . . . . . . . . . . . . . . . . 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. ( b I y ) /\ ( a .- y ) = ( a .- C ) ) )
5453simpld 459 . . . . . . . . . . . . . . . . . . . . . . . . 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 e. ( b I y ) )
551, 3, 4, 12, 49, 47, 24, 52, 54btwnlng3 23161 . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) -> y e. ( b L a ) )
561, 3, 4, 12, 47, 49, 24, 51, 55lncom 23162 . . . . . . . . . . . . . . . . . . . . . . 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 e. ( a L b ) )
5750simpld 459 . . . . . . . . . . . . . . . . . . . . . . 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 ) )
5856, 57eleqtrrd 2543 . . . . . . . . . . . . . . . . . . . . . 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 )
5958adantr 465 . . . . . . . . . . . . . . . . . . . . 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 e. A )
60 foot.y . . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ph -> -. C e. A )
6160ad3antrrr 729 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ph /\ a e. P ) /\ b e. P ) /\ ( A = ( a L b ) /\ a =/= b ) ) -> -. C e. A )
6261ad10antr 743 . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) -> -. C e. A )
6362adantr 465 . . . . . . . . . . . . . . . . . . . . 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 ) ) ) -> -. C e. A )
64 nelne2 2779 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( y e. A /\ -. C e. A ) -> y =/= C )
6559, 63, 64syl2anc 661 . . . . . . . . . . . . . . . . . . . 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 =/= C )
6665necomd 2720 . . . . . . . . . . . . . . . . . . 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 =/= y )
6742, 66eqnetrrd 2743 . . . . . . . . . . . . . . . . . 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 ) ) ) -> ( ( (pInvG ` G ) ` p ) ` y ) =/= y )
68 eqid 2452 . . . . . . . . . . . . . . . . . . . 20 |- ( (pInvG ` G ) ` p ) = ( (pInvG ` G ) ` p )
691, 2, 3, 4, 5, 28, 36, 68, 29mirinv 23208 . . . . . . . . . . . . . . . . . . 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 ) ) ) -> ( ( ( (pInvG ` G ) ` p ) ` y ) = y <-> p = y ) )
7069necon3bid 2707 . . . . . . . . . . . . . . . . . 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 ) ) ) -> ( ( ( (pInvG ` G ) ` p ) ` y ) =/= y <-> p =/= y ) )
7167, 70mpbid 210 . . . . . . . . . . . . . . . . 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 =/= y )
7271necomd 2720 . . . . . . . . . . . . . . . 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 =/= p )
731, 2, 3, 28, 29, 36, 29, 31, 40, 72tgcgrneq 23066 . . . . . . . . . . . . . . 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 =/= z )
7473necomd 2720 . . . . . . . . . . . . . 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 )
7574necomd 2720 . . . . . . . . . . . . 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 )
76 eqid 2452 . . . . . . . . . . . . . . 15 |- ( (pInvG ` G ) ` z ) = ( (pInvG ` G ) ` z )
77 simp-4r 766 . . . . . . . . . . . . . . . 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 )
7877adantr 465 . . . . . . . . . . . . . . 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 )
79 simp-4r 766 . . . . . . . . . . . . . . . . 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 )
80 simplr 754 . . . . . . . . . . . . . . . . 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 )
811, 2, 3, 4, 5, 11, 79, 76, 80mircl 23203 . . . . . . . . . . . . . . . 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 )
8281ad3antrrr 729 . . . . . . . . . . . . . . 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 )
8318adantr 465 . . . . . . . . . . . . . . 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 )
8419adantr 465 . . . . . . . . . . . . . . 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 )
851, 2, 3, 4, 5, 28, 36, 68, 29mirbtwn 23200 . . . . . . . . . . . . . . . . . 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 ) )
8642oveq1d 6210 . . . . . . . . . . . . . . . . . 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 ) )
8785, 86eleqtrrd 2543 . . . . . . . . . . . . . . . . 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 ) )
88 simpllr 758 . . . . . . . . . . . . . . . . . . 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 ) ) )
8988simpld 459 . . . . . . . . . . . . . . . . . 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 ) )
9089adantr 465 . . . . . . . . . . . . . . . . 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 ) )
911, 2, 3, 28, 83, 36, 29, 78, 71, 87, 90tgbtwnouttr2 23078 . . . . . . . . . . . . . . . 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 ) )
921, 2, 3, 28, 83, 29, 78, 91tgbtwncom 23071 . . . . . . . . . . . . . . 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 ) )
93 simplrl 759 . . . . . . . . . . . . . . 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 ) )
94 eqid 2452 . . . . . . . . . . . . . . . . . . 19 |- (cgrG ` G ) = (cgrG ` G )
9553simprd 463 . . . . . . . . . . . . . . . . . . . . 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 ) )
9641oveq2d 6211 . . . . . . . . . . . . . . . . . . . . 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 ) ) )
9795, 96eqtrd 2493 . . . . . . . . . . . . . . . . . . . 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 ) ) )
981, 2, 3, 4, 5, 12, 47, 35, 24israg 23229 . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
9997, 98mpbird 232 . . . . . . . . . . . . . . . . . . 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 ) )
10088simprd 463 . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
1011, 2, 3, 12, 47, 24, 47, 18, 95tgcgrcomlr 23063 . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
102100, 101eqtr2d 2494 . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
1031, 3, 4, 12, 47, 49, 51tglinerflx1 23173 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
104103, 57eleqtrrd 2543 . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
105 nelne2 2779 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( a e. A /\ -. C e. A ) -> a =/= C )
106104, 62, 105syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . . 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 )
107106necomd 2720 . . . . . . . . . . . . . . . . . . . . . . . 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 )
1081, 2, 3, 12, 18, 47, 24, 77, 102, 107tgcgrneq 23066 . . . . . . . . . . . . . . . . . . . . . . 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 )
109108necomd 2720 . . . . . . . . . . . . . . . . . . . . . 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 )
1101, 2, 3, 12, 35, 24, 77, 89tgbtwncom 23071 . . . . . . . . . . . . . . . . . . . . . 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 ) )
11137simpld 459 . . . . . . . . . . . . . . . . . . . . . 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 ) /\ (