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 )  /\  (