Users' Mathboxes Mathbox for Frédéric Liné < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  pdiveql Unicode version

Theorem pdiveql 26271
Description: The plane is divided into two equivalence classes by a line 
M. (For my private use only. Don't use.) (Contributed by FL, 14-Jul-2016.)
Hypotheses
Ref Expression
isside.1  |-  P  =  (PPoints `  G )
isside.2  |-  L  =  (PLines `  G )
isside.3  |-  .~  =  ( (ss `  G ) `
 M )
isside.4  |-  ( ph  ->  G  e. Ibg )
isside.5  |-  ( ph  ->  M  e.  L )
pdiveql.1  |-  ( ph  ->  A  e.  ( P 
\  M ) )
Assertion
Ref Expression
pdiveql  |-  ( ph  ->  ( B  e.  ( ( P  \  M
) /.  .~  )  <->  ( B  =  [ A ]  .~  \/  B  =  ( ( P  \  M )  \  [ A ]  .~  )
) ) )

Proof of Theorem pdiveql
Dummy variables  a  x  b  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elqsg 6727 . . . . 5  |-  ( B  e.  ( ( P 
\  M ) /.  .~  )  ->  ( B  e.  ( ( P  \  M ) /.  .~  ) 
<->  E. x  e.  ( P  \  M ) B  =  [ x ]  .~  ) )
2 exmid 404 . . . . . . 7  |-  ( ( ( A ( seg `  G ) x )  i^i  M )  =  (/)  \/  -.  ( ( A ( seg `  G
) x )  i^i 
M )  =  (/) )
3 isside.1 . . . . . . . . . . . . . . . 16  |-  P  =  (PPoints `  G )
4 isside.2 . . . . . . . . . . . . . . . 16  |-  L  =  (PLines `  G )
5 isside.3 . . . . . . . . . . . . . . . 16  |-  .~  =  ( (ss `  G ) `
 M )
6 isside.4 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  G  e. Ibg )
763ad2ant1 976 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( P  \  M )  /\  ( ( A ( seg `  G
) x )  i^i 
M )  =  (/) )  ->  G  e. Ibg )
8 isside.5 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  M  e.  L )
983ad2ant1 976 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( P  \  M )  /\  ( ( A ( seg `  G
) x )  i^i 
M )  =  (/) )  ->  M  e.  L
)
103, 4, 5, 7, 9bosser 26270 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  ( P  \  M )  /\  ( ( A ( seg `  G
) x )  i^i 
M )  =  (/) )  ->  .~  Er  ( P  \  M ) )
11 eqid 2296 . . . . . . . . . . . . . . . . . . . 20  |-  ( seg `  G )  =  ( seg `  G )
126adantr 451 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  ( P  \  M ) )  ->  G  e. Ibg )
13 pdiveql.1 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  A  e.  ( P 
\  M ) )
14 eldifi 3311 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( A  e.  ( P  \  M )  ->  A  e.  P )
1513, 14syl 15 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  A  e.  P )
1615adantr 451 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  ( P  \  M ) )  ->  A  e.  P )
17 eldifi 3311 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  e.  ( P  \  M )  ->  x  e.  P )
1817adantl 452 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  ( P  \  M ) )  ->  x  e.  P )
193, 11, 12, 16, 18xsyysx 26248 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  ( P  \  M ) )  ->  ( A
( seg `  G
) x )  =  ( x ( seg `  G ) A ) )
2019ineq1d 3382 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  ( P  \  M ) )  ->  ( ( A ( seg `  G
) x )  i^i 
M )  =  ( ( x ( seg `  G ) A )  i^i  M ) )
2120eqeq1d 2304 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  ( P  \  M ) )  ->  ( (
( A ( seg `  G ) x )  i^i  M )  =  (/) 
<->  ( ( x ( seg `  G ) A )  i^i  M
)  =  (/) ) )
2221biimp3a 1281 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( P  \  M )  /\  ( ( A ( seg `  G
) x )  i^i 
M )  =  (/) )  ->  ( ( x ( seg `  G
) A )  i^i 
M )  =  (/) )
23 simp2 956 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  ( P  \  M )  /\  ( ( A ( seg `  G
) x )  i^i 
M )  =  (/) )  ->  x  e.  ( P  \  M ) )
24133ad2ant1 976 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  ( P  \  M )  /\  ( ( A ( seg `  G
) x )  i^i 
M )  =  (/) )  ->  A  e.  ( P  \  M ) )
253, 4, 5, 7, 9, 11, 23, 24isside 26269 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( P  \  M )  /\  ( ( A ( seg `  G
) x )  i^i 
M )  =  (/) )  ->  ( x  .~  A 
<->  ( ( x ( seg `  G ) A )  i^i  M
)  =  (/) ) )
2622, 25mpbird 223 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  ( P  \  M )  /\  ( ( A ( seg `  G
) x )  i^i 
M )  =  (/) )  ->  x  .~  A
)
2710, 26erthi 6722 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( P  \  M )  /\  ( ( A ( seg `  G
) x )  i^i 
M )  =  (/) )  ->  [ x ]  .~  =  [ A ]  .~  )
28273exp 1150 . . . . . . . . . . . . 13  |-  ( ph  ->  ( x  e.  ( P  \  M )  ->  ( ( ( A ( seg `  G
) x )  i^i 
M )  =  (/)  ->  [ x ]  .~  =  [ A ]  .~  ) ) )
29 eqeq1 2302 . . . . . . . . . . . . . . 15  |-  ( B  =  [ x ]  .~  ->  ( B  =  [ A ]  .~  <->  [ x ]  .~  =  [ A ]  .~  )
)
3029imbi2d 307 . . . . . . . . . . . . . 14  |-  ( B  =  [ x ]  .~  ->  ( ( ( ( A ( seg `  G ) x )  i^i  M )  =  (/)  ->  B  =  [ A ]  .~  )  <->  ( ( ( A ( seg `  G ) x )  i^i  M
)  =  (/)  ->  [ x ]  .~  =  [ A ]  .~  ) ) )
3130imbi2d 307 . . . . . . . . . . . . 13  |-  ( B  =  [ x ]  .~  ->  ( ( x  e.  ( P  \  M )  ->  (
( ( A ( seg `  G ) x )  i^i  M
)  =  (/)  ->  B  =  [ A ]  .~  ) )  <->  ( x  e.  ( P  \  M
)  ->  ( (
( A ( seg `  G ) x )  i^i  M )  =  (/)  ->  [ x ]  .~  =  [ A ]  .~  ) ) ) )
3228, 31syl5ibr 212 . . . . . . . . . . . 12  |-  ( B  =  [ x ]  .~  ->  ( ph  ->  ( x  e.  ( P 
\  M )  -> 
( ( ( A ( seg `  G
) x )  i^i 
M )  =  (/)  ->  B  =  [ A ]  .~  ) ) ) )
3332com3l 75 . . . . . . . . . . 11  |-  ( ph  ->  ( x  e.  ( P  \  M )  ->  ( B  =  [ x ]  .~  ->  ( ( ( A ( seg `  G
) x )  i^i 
M )  =  (/)  ->  B  =  [ A ]  .~  ) ) ) )
34333imp 1145 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( P  \  M )  /\  B  =  [
x ]  .~  )  ->  ( ( ( A ( seg `  G
) x )  i^i 
M )  =  (/)  ->  B  =  [ A ]  .~  ) )
35 vex 2804 . . . . . . . . . . . . . . . . . . 19  |-  y  e. 
_V
36 vex 2804 . . . . . . . . . . . . . . . . . . 19  |-  x  e. 
_V
3735, 36pm3.2i 441 . . . . . . . . . . . . . . . . . 18  |-  ( y  e.  _V  /\  x  e.  _V )
38 elecg 6714 . . . . . . . . . . . . . . . . . 18  |-  ( ( y  e.  _V  /\  x  e.  _V )  ->  ( y  e.  [
x ]  .~  <->  x  .~  y ) )
3937, 38mp1i 11 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  ( P  \  M )  /\  -.  ( ( A ( seg `  G
) x )  i^i 
M )  =  (/) )  ->  ( y  e. 
[ x ]  .~  <->  x  .~  y ) )
4063ad2ant1 976 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  ( P  \  M )  /\  -.  ( ( A ( seg `  G
) x )  i^i 
M )  =  (/) )  ->  G  e. Ibg )
4183ad2ant1 976 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  ( P  \  M )  /\  -.  ( ( A ( seg `  G
) x )  i^i 
M )  =  (/) )  ->  M  e.  L
)
4236a1i 10 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  ( P  \  M )  /\  -.  ( ( A ( seg `  G
) x )  i^i 
M )  =  (/) )  ->  x  e.  _V )
4335a1i 10 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  ( P  \  M )  /\  -.  ( ( A ( seg `  G
) x )  i^i 
M )  =  (/) )  ->  y  e.  _V )
443, 4, 5, 40, 41, 11, 42, 43isside1 26268 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  ( P  \  M )  /\  -.  ( ( A ( seg `  G
) x )  i^i 
M )  =  (/) )  ->  ( x  .~  y 
<->  ( x  e.  ( P  \  M )  /\  y  e.  ( P  \  M )  /\  ( ( x ( seg `  G
) y )  i^i 
M )  =  (/) ) ) )
45 simpr2 962 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  x  e.  ( P  \  M
)  /\  -.  (
( A ( seg `  G ) x )  i^i  M )  =  (/) )  /\  (
x  e.  ( P 
\  M )  /\  y  e.  ( P  \  M )  /\  (
( x ( seg `  G ) y )  i^i  M )  =  (/) ) )  ->  y  e.  ( P  \  M
) )
4663ad2ant1 976 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  x  e.  ( P  \  M )  /\  ( x  e.  ( P  \  M
)  /\  y  e.  ( P  \  M )  /\  ( ( x ( seg `  G
) y )  i^i 
M )  =  (/) ) )  ->  G  e. Ibg )
4746adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  x  e.  ( P  \  M
)  /\  ( x  e.  ( P  \  M
)  /\  y  e.  ( P  \  M )  /\  ( ( x ( seg `  G
) y )  i^i 
M )  =  (/) ) )  /\  A  .~  y )  ->  G  e. Ibg )
4883ad2ant1 976 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  x  e.  ( P  \  M )  /\  ( x  e.  ( P  \  M
)  /\  y  e.  ( P  \  M )  /\  ( ( x ( seg `  G
) y )  i^i 
M )  =  (/) ) )  ->  M  e.  L )
4948adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  x  e.  ( P  \  M
)  /\  ( x  e.  ( P  \  M
)  /\  y  e.  ( P  \  M )  /\  ( ( x ( seg `  G
) y )  i^i 
M )  =  (/) ) )  /\  A  .~  y )  ->  M  e.  L )
50133ad2ant1 976 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  x  e.  ( P  \  M )  /\  ( x  e.  ( P  \  M
)  /\  y  e.  ( P  \  M )  /\  ( ( x ( seg `  G
) y )  i^i 
M )  =  (/) ) )  ->  A  e.  ( P  \  M
) )
5150adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  x  e.  ( P  \  M
)  /\  ( x  e.  ( P  \  M
)  /\  y  e.  ( P  \  M )  /\  ( ( x ( seg `  G
) y )  i^i 
M )  =  (/) ) )  /\  A  .~  y )  ->  A  e.  ( P  \  M
) )
52 simp32 992 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  x  e.  ( P  \  M )  /\  ( x  e.  ( P  \  M
)  /\  y  e.  ( P  \  M )  /\  ( ( x ( seg `  G
) y )  i^i 
M )  =  (/) ) )  ->  y  e.  ( P  \  M
) )
5352adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  x  e.  ( P  \  M
)  /\  ( x  e.  ( P  \  M
)  /\  y  e.  ( P  \  M )  /\  ( ( x ( seg `  G
) y )  i^i 
M )  =  (/) ) )  /\  A  .~  y )  ->  y  e.  ( P  \  M
) )
54 simpl2 959 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  x  e.  ( P  \  M
)  /\  ( x  e.  ( P  \  M
)  /\  y  e.  ( P  \  M )  /\  ( ( x ( seg `  G
) y )  i^i 
M )  =  (/) ) )  /\  A  .~  y )  ->  x  e.  ( P  \  M
) )
553, 4, 5, 46, 48, 11, 50, 52isside 26269 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  x  e.  ( P  \  M )  /\  ( x  e.  ( P  \  M
)  /\  y  e.  ( P  \  M )  /\  ( ( x ( seg `  G
) y )  i^i 
M )  =  (/) ) )  ->  ( A  .~  y  <->  ( ( A ( seg `  G
) y )  i^i 
M )  =  (/) ) )
5655biimpa 470 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  x  e.  ( P  \  M
)  /\  ( x  e.  ( P  \  M
)  /\  y  e.  ( P  \  M )  /\  ( ( x ( seg `  G
) y )  i^i 
M )  =  (/) ) )  /\  A  .~  y )  ->  (
( A ( seg `  G ) y )  i^i  M )  =  (/) )
5763ad2ant1 976 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( (
ph  /\  x  e.  ( P  \  M )  /\  y  e.  ( P  \  M ) )  ->  G  e. Ibg )
58173ad2ant2 977 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( (
ph  /\  x  e.  ( P  \  M )  /\  y  e.  ( P  \  M ) )  ->  x  e.  P )
59 eldifi 3311 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( y  e.  ( P  \  M )  ->  y  e.  P )
60593ad2ant3 978 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( (
ph  /\  x  e.  ( P  \  M )  /\  y  e.  ( P  \  M ) )  ->  y  e.  P )
613, 11, 57, 58, 60xsyysx 26248 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( (
ph  /\  x  e.  ( P  \  M )  /\  y  e.  ( P  \  M ) )  ->  ( x
( seg `  G
) y )  =  ( y ( seg `  G ) x ) )
6261ineq1d 3382 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
ph  /\  x  e.  ( P  \  M )  /\  y  e.  ( P  \  M ) )  ->  ( (
x ( seg `  G
) y )  i^i 
M )  =  ( ( y ( seg `  G ) x )  i^i  M ) )
6362eqeq1d 2304 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( (
ph  /\  x  e.  ( P  \  M )  /\  y  e.  ( P  \  M ) )  ->  ( (
( x ( seg `  G ) y )  i^i  M )  =  (/) 
<->  ( ( y ( seg `  G ) x )  i^i  M
)  =  (/) ) )
6463biimpd 198 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
ph  /\  x  e.  ( P  \  M )  /\  y  e.  ( P  \  M ) )  ->  ( (
( x ( seg `  G ) y )  i^i  M )  =  (/)  ->  ( ( y ( seg `  G
) x )  i^i 
M )  =  (/) ) )
65643exp 1150 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ph  ->  ( x  e.  ( P  \  M )  ->  ( y  e.  ( P  \  M
)  ->  ( (
( x ( seg `  G ) y )  i^i  M )  =  (/)  ->  ( ( y ( seg `  G
) x )  i^i 
M )  =  (/) ) ) ) )
66653imp2 1166 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  ( x  e.  ( P  \  M
)  /\  y  e.  ( P  \  M )  /\  ( ( x ( seg `  G
) y )  i^i 
M )  =  (/) ) )  ->  (
( y ( seg `  G ) x )  i^i  M )  =  (/) )
67663adant2 974 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  x  e.  ( P  \  M )  /\  ( x  e.  ( P  \  M
)  /\  y  e.  ( P  \  M )  /\  ( ( x ( seg `  G
) y )  i^i 
M )  =  (/) ) )  ->  (
( y ( seg `  G ) x )  i^i  M )  =  (/) )
6867adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  x  e.  ( P  \  M
)  /\  ( x  e.  ( P  \  M
)  /\  y  e.  ( P  \  M )  /\  ( ( x ( seg `  G
) y )  i^i 
M )  =  (/) ) )  /\  A  .~  y )  ->  (
( y ( seg `  G ) x )  i^i  M )  =  (/) )
693, 4, 11, 47, 49, 51, 53, 54, 56, 68bsstrs 26249 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  x  e.  ( P  \  M
)  /\  ( x  e.  ( P  \  M
)  /\  y  e.  ( P  \  M )  /\  ( ( x ( seg `  G
) y )  i^i 
M )  =  (/) ) )  /\  A  .~  y )  ->  (
( A ( seg `  G ) x )  i^i  M )  =  (/) )
7069ex 423 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  x  e.  ( P  \  M )  /\  ( x  e.  ( P  \  M
)  /\  y  e.  ( P  \  M )  /\  ( ( x ( seg `  G
) y )  i^i 
M )  =  (/) ) )  ->  ( A  .~  y  ->  (
( A ( seg `  G ) x )  i^i  M )  =  (/) ) )
7170con3d 125 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  x  e.  ( P  \  M )  /\  ( x  e.  ( P  \  M
)  /\  y  e.  ( P  \  M )  /\  ( ( x ( seg `  G
) y )  i^i 
M )  =  (/) ) )  ->  ( -.  ( ( A ( seg `  G ) x )  i^i  M
)  =  (/)  ->  -.  A  .~  y ) )
72713exp 1150 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( x  e.  ( P  \  M )  ->  ( ( x  e.  ( P  \  M )  /\  y  e.  ( P  \  M
)  /\  ( (
x ( seg `  G
) y )  i^i 
M )  =  (/) )  ->  ( -.  (
( A ( seg `  G ) x )  i^i  M )  =  (/)  ->  -.  A  .~  y ) ) ) )
7372com34 77 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( x  e.  ( P  \  M )  ->  ( -.  (
( A ( seg `  G ) x )  i^i  M )  =  (/)  ->  ( ( x  e.  ( P  \  M )  /\  y  e.  ( P  \  M
)  /\  ( (
x ( seg `  G
) y )  i^i 
M )  =  (/) )  ->  -.  A  .~  y ) ) ) )
74733imp1 1164 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  x  e.  ( P  \  M
)  /\  -.  (
( A ( seg `  G ) x )  i^i  M )  =  (/) )  /\  (
x  e.  ( P 
\  M )  /\  y  e.  ( P  \  M )  /\  (
( x ( seg `  G ) y )  i^i  M )  =  (/) ) )  ->  -.  A  .~  y )
7545, 74jca 518 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  x  e.  ( P  \  M
)  /\  -.  (
( A ( seg `  G ) x )  i^i  M )  =  (/) )  /\  (
x  e.  ( P 
\  M )  /\  y  e.  ( P  \  M )  /\  (
( x ( seg `  G ) y )  i^i  M )  =  (/) ) )  ->  (
y  e.  ( P 
\  M )  /\  -.  A  .~  y
) )
76 simpl2 959 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  x  e.  ( P  \  M
)  /\  -.  (
( A ( seg `  G ) x )  i^i  M )  =  (/) )  /\  (
y  e.  ( P 
\  M )  /\  -.  A  .~  y
) )  ->  x  e.  ( P  \  M
) )
77 simprl 732 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  x  e.  ( P  \  M
)  /\  -.  (
( A ( seg `  G ) x )  i^i  M )  =  (/) )  /\  (
y  e.  ( P 
\  M )  /\  -.  A  .~  y
) )  ->  y  e.  ( P  \  M
) )
7840adantl 452 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( y  e.  ( P 
\  M )  /\  ( ph  /\  x  e.  ( P  \  M
)  /\  -.  (
( A ( seg `  G ) x )  i^i  M )  =  (/) ) )  ->  G  e. Ibg )
7941adantl 452 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( y  e.  ( P 
\  M )  /\  ( ph  /\  x  e.  ( P  \  M
)  /\  -.  (
( A ( seg `  G ) x )  i^i  M )  =  (/) ) )  ->  M  e.  L )
80133ad2ant1 976 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  x  e.  ( P  \  M )  /\  -.  ( ( A ( seg `  G
) x )  i^i 
M )  =  (/) )  ->  A  e.  ( P  \  M ) )
8180adantl 452 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( y  e.  ( P 
\  M )  /\  ( ph  /\  x  e.  ( P  \  M
)  /\  -.  (
( A ( seg `  G ) x )  i^i  M )  =  (/) ) )  ->  A  e.  ( P  \  M
) )
82 simpl 443 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( y  e.  ( P 
\  M )  /\  ( ph  /\  x  e.  ( P  \  M
)  /\  -.  (
( A ( seg `  G ) x )  i^i  M )  =  (/) ) )  ->  y  e.  ( P  \  M
) )
833, 4, 5, 78, 79, 11, 81, 82isside 26269 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( y  e.  ( P 
\  M )  /\  ( ph  /\  x  e.  ( P  \  M
)  /\  -.  (
( A ( seg `  G ) x )  i^i  M )  =  (/) ) )  ->  ( A  .~  y  <->  ( ( A ( seg `  G
) y )  i^i 
M )  =  (/) ) )
8483notbid 285 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( y  e.  ( P 
\  M )  /\  ( ph  /\  x  e.  ( P  \  M
)  /\  -.  (
( A ( seg `  G ) x )  i^i  M )  =  (/) ) )  ->  ( -.  A  .~  y  <->  -.  ( ( A ( seg `  G ) y )  i^i  M
)  =  (/) ) )
8540ad2antll 709 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( -.  ( ( A ( seg `  G
) y )  i^i 
M )  =  (/)  /\  ( y  e.  ( P  \  M )  /\  ( ph  /\  x  e.  ( P  \  M )  /\  -.  ( ( A ( seg `  G ) x )  i^i  M
)  =  (/) ) ) )  ->  G  e. Ibg )
8641ad2antll 709 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( -.  ( ( A ( seg `  G
) y )  i^i 
M )  =  (/)  /\  ( y  e.  ( P  \  M )  /\  ( ph  /\  x  e.  ( P  \  M )  /\  -.  ( ( A ( seg `  G ) x )  i^i  M
)  =  (/) ) ) )  ->  M  e.  L )
87 simp2 956 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  x  e.  ( P  \  M )  /\  -.  ( ( A ( seg `  G
) x )  i^i 
M )  =  (/) )  ->  x  e.  ( P  \  M ) )
8887ad2antll 709 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( -.  ( ( A ( seg `  G
) y )  i^i 
M )  =  (/)  /\  ( y  e.  ( P  \  M )  /\  ( ph  /\  x  e.  ( P  \  M )  /\  -.  ( ( A ( seg `  G ) x )  i^i  M
)  =  (/) ) ) )  ->  x  e.  ( P  \  M ) )
8980ad2antll 709 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( -.  ( ( A ( seg `  G
) y )  i^i 
M )  =  (/)  /\  ( y  e.  ( P  \  M )  /\  ( ph  /\  x  e.  ( P  \  M )  /\  -.  ( ( A ( seg `  G ) x )  i^i  M
)  =  (/) ) ) )  ->  A  e.  ( P  \  M ) )
90 simprl 732 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( -.  ( ( A ( seg `  G
) y )  i^i 
M )  =  (/)  /\  ( y  e.  ( P  \  M )  /\  ( ph  /\  x  e.  ( P  \  M )  /\  -.  ( ( A ( seg `  G ) x )  i^i  M
)  =  (/) ) ) )  ->  y  e.  ( P  \  M ) )
9121notbid 285 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  x  e.  ( P  \  M ) )  ->  ( -.  ( ( A ( seg `  G ) x )  i^i  M
)  =  (/)  <->  -.  (
( x ( seg `  G ) A )  i^i  M )  =  (/) ) )
9291biimp3a 1281 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  x  e.  ( P  \  M )  /\  -.  ( ( A ( seg `  G
) x )  i^i 
M )  =  (/) )  ->  -.  ( (
x ( seg `  G
) A )  i^i 
M )  =  (/) )
93 df-ne 2461 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( x ( seg `  G ) A )  i^i  M )  =/=  (/) 
<->  -.  ( ( x ( seg `  G
) A )  i^i 
M )  =  (/) )
9492, 93sylibr 203 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  x  e.  ( P  \  M )  /\  -.  ( ( A ( seg `  G
) x )  i^i 
M )  =  (/) )  ->  ( ( x ( seg `  G
) A )  i^i 
M )  =/=  (/) )
9594ad2antll 709 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( -.  ( ( A ( seg `  G
) y )  i^i 
M )  =  (/)  /\  ( y  e.  ( P  \  M )  /\  ( ph  /\  x  e.  ( P  \  M )  /\  -.  ( ( A ( seg `  G ) x )  i^i  M
)  =  (/) ) ) )  ->  ( (
x ( seg `  G
) A )  i^i 
M )  =/=  (/) )
96 df-ne 2461 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( A ( seg `  G ) y )  i^i  M )  =/=  (/) 
<->  -.  ( ( A ( seg `  G
) y )  i^i 
M )  =  (/) )
9796biimpri 197 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( -.  ( ( A ( seg `  G ) y )  i^i  M
)  =  (/)  ->  (
( A ( seg `  G ) y )  i^i  M )  =/=  (/) )
9897adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( -.  ( ( A ( seg `  G
) y )  i^i 
M )  =  (/)  /\  ( y  e.  ( P  \  M )  /\  ( ph  /\  x  e.  ( P  \  M )  /\  -.  ( ( A ( seg `  G ) x )  i^i  M
)  =  (/) ) ) )  ->  ( ( A ( seg `  G
) y )  i^i 
M )  =/=  (/) )
993, 4, 11, 85, 86, 88, 89, 90, 95, 98nbssntrs 26250 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( -.  ( ( A ( seg `  G
) y )  i^i 
M )  =  (/)  /\  ( y  e.  ( P  \  M )  /\  ( ph  /\  x  e.  ( P  \  M )  /\  -.  ( ( A ( seg `  G ) x )  i^i  M
)  =  (/) ) ) )  ->  ( (
x ( seg `  G
) y )  i^i 
M )  =  (/) )
10099ex 423 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( -.  ( ( A ( seg `  G ) y )  i^i  M
)  =  (/)  ->  (
( y  e.  ( P  \  M )  /\  ( ph  /\  x  e.  ( P  \  M )  /\  -.  ( ( A ( seg `  G ) x )  i^i  M
)  =  (/) ) )  ->  ( ( x ( seg `  G
) y )  i^i 
M )  =  (/) ) )
10184, 100syl6bi 219 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( y  e.  ( P 
\  M )  /\  ( ph  /\  x  e.  ( P  \  M
)  /\  -.  (
( A ( seg `  G ) x )  i^i  M )  =  (/) ) )  ->  ( -.  A  .~  y  ->  ( ( y  e.  ( P  \  M
)  /\  ( ph  /\  x  e.  ( P 
\  M )  /\  -.  ( ( A ( seg `  G ) x )  i^i  M
)  =  (/) ) )  ->  ( ( x ( seg `  G
) y )  i^i 
M )  =  (/) ) ) )
102101pm2.43a 45 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( y  e.  ( P 
\  M )  /\  ( ph  /\  x  e.  ( P  \  M
)  /\  -.  (
( A ( seg `  G ) x )  i^i  M )  =  (/) ) )  ->  ( -.  A  .~  y  ->  ( ( x ( seg `  G ) y )  i^i  M
)  =  (/) ) )
103102impancom 427 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( y  e.  ( P 
\  M )  /\  -.  A  .~  y
)  ->  ( ( ph  /\  x  e.  ( P  \  M )  /\  -.  ( ( A ( seg `  G
) x )  i^i 
M )  =  (/) )  ->  ( ( x ( seg `  G
) y )  i^i 
M )  =  (/) ) )
104103impcom 419 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  x  e.  ( P  \  M
)  /\  -.  (
( A ( seg `  G ) x )  i^i  M )  =  (/) )  /\  (
y  e.  ( P 
\  M )  /\  -.  A  .~  y
) )  ->  (
( x ( seg `  G ) y )  i^i  M )  =  (/) )
10576, 77, 1043jca 1132 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  x  e.  ( P  \  M
)  /\  -.  (
( A ( seg `  G ) x )  i^i  M )  =  (/) )  /\  (
y  e.  ( P 
\  M )  /\  -.  A  .~  y
) )  ->  (
x  e.  ( P 
\  M )  /\  y  e.  ( P  \  M )  /\  (
( x ( seg `  G ) y )  i^i  M )  =  (/) ) )
10675, 105impbida 805 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  ( P  \  M )  /\  -.  ( ( A ( seg `  G
) x )  i^i 
M )  =  (/) )  ->  ( ( x  e.  ( P  \  M )  /\  y  e.  ( P  \  M
)  /\  ( (
x ( seg `  G
) y )  i^i 
M )  =  (/) ) 
<->  ( y  e.  ( P  \  M )  /\  -.  A  .~  y ) ) )
10744, 106bitrd 244 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  ( P  \  M )  /\  -.  ( ( A ( seg `  G
) x )  i^i 
M )  =  (/) )  ->  ( x  .~  y 
<->  ( y  e.  ( P  \  M )  /\  -.  A  .~  y ) ) )
108 elecg 6714 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( y  e.  _V  /\  A  e.  ( P  \  M ) )  -> 
( y  e.  [ A ]  .~  <->  A  .~  y ) )
10935, 80, 108sylancr 644 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  ( P  \  M )  /\  -.  ( ( A ( seg `  G
) x )  i^i 
M )  =  (/) )  ->  ( y  e. 
[ A ]  .~  <->  A  .~  y ) )
110109bicomd 192 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  ( P  \  M )  /\  -.  ( ( A ( seg `  G
) x )  i^i 
M )  =  (/) )  ->  ( A  .~  y 
<->  y  e.  [ A ]  .~  ) )
111110notbid 285 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  ( P  \  M )  /\  -.  ( ( A ( seg `  G
) x )  i^i 
M )  =  (/) )  ->  ( -.  A  .~  y  <->  -.  y  e.  [ A ]  .~  )
)
112111anbi2d 684 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  ( P  \  M )  /\  -.  ( ( A ( seg `  G
) x )  i^i 
M )  =  (/) )  ->  ( ( y  e.  ( P  \  M )  /\  -.  A  .~  y )  <->  ( y  e.  ( P  \  M
)  /\  -.  y  e.  [ A ]  .~  ) ) )
11339, 107, 1123bitrd 270 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( P  \  M )  /\  -.  ( ( A ( seg `  G
) x )  i^i 
M )  =  (/) )  ->  ( y  e. 
[ x ]  .~  <->  ( y  e.  ( P 
\  M )  /\  -.  y  e.  [ A ]  .~  ) ) )
114 eldif 3175 . . . . . . . . . . . . . . . 16  |-  ( y  e.  ( ( P 
\  M )  \  [ A ]  .~  )  <->  ( y  e.  ( P 
\  M )  /\  -.  y  e.  [ A ]  .~  ) )
115113, 114syl6bbr 254 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  ( P  \  M )  /\  -.  ( ( A ( seg `  G
) x )  i^i 
M )  =  (/) )  ->  ( y  e. 
[ x ]  .~  <->  y  e.  ( ( P 
\  M )  \  [ A ]  .~  )
) )
116115eqrdv 2294 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( P  \  M )  /\  -.  ( ( A ( seg `  G
) x )  i^i 
M )  =  (/) )  ->  [ x ]  .~  =  ( ( P  \  M )  \  [ A ]  .~  )
)
1171163exp 1150 . . . . . . . . . . . . 13  |-  ( ph  ->  ( x  e.  ( P  \  M )  ->  ( -.  (
( A ( seg `  G ) x )  i^i  M )  =  (/)  ->  [ x ]  .~  =  ( ( P  \  M )  \  [ A ]  .~  )
) ) )
118 eqeq1 2302 . . . . . . . . . . . . . . 15  |-  ( B  =  [ x ]  .~  ->  ( B  =  ( ( P  \  M )  \  [ A ]  .~  )  <->  [ x ]  .~  =  ( ( P  \  M )  \  [ A ]  .~  )
) )
119118imbi2d 307 . . . . . . . . . . . . . 14  |-  ( B  =  [ x ]  .~  ->  ( ( -.  ( ( A ( seg `  G ) x )  i^i  M
)  =  (/)  ->  B  =  ( ( P 
\  M )  \  [ A ]  .~  )
)  <->  ( -.  (
( A ( seg `  G ) x )  i^i  M )  =  (/)  ->  [ x ]  .~  =  ( ( P  \  M )  \  [ A ]  .~  )
) ) )
120119imbi2d 307 . . . . . . . . . . . . 13  |-  ( B  =  [ x ]  .~  ->  ( ( x  e.  ( P  \  M )  ->  ( -.  ( ( A ( seg `  G ) x )  i^i  M
)  =  (/)  ->  B  =  ( ( P 
\  M )  \  [ A ]  .~  )
) )  <->  ( x  e.  ( P  \  M
)  ->  ( -.  ( ( A ( seg `  G ) x )  i^i  M
)  =  (/)  ->  [ x ]  .~  =  ( ( P  \  M ) 
\  [ A ]  .~  ) ) ) ) )
121117, 120syl5ibr 212 . . . . . . . . . . . 12  |-  ( B  =  [ x ]  .~  ->  ( ph  ->  ( x  e.  ( P 
\  M )  -> 
( -.  ( ( A ( seg `  G
) x )  i^i 
M )  =  (/)  ->  B  =  ( ( P  \  M ) 
\  [ A ]  .~  ) ) ) ) )
122121com3l 75 . . . . . . . . . . 11  |-  ( ph  ->  ( x  e.  ( P  \  M )  ->  ( B  =  [ x ]  .~  ->  ( -.  ( ( A ( seg `  G
) x )  i^i 
M )  =  (/)  ->  B  =  ( ( P  \  M ) 
\  [ A ]  .~  ) ) ) ) )
1231223imp 1145 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( P  \  M )  /\  B  =  [
x ]  .~  )  ->  ( -.  ( ( A ( seg `  G
) x )  i^i 
M )  =  (/)  ->  B  =  ( ( P  \  M ) 
\  [ A ]  .~  ) ) )
12434, 123orim12d 811 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( P  \  M )  /\  B  =  [
x ]  .~  )  ->  ( ( ( ( A ( seg `  G
) x )  i^i 
M )  =  (/)  \/ 
-.  ( ( A ( seg `  G
) x )  i^i 
M )  =  (/) )  ->  ( B  =  [ A ]  .~  \/  B  =  (
( P  \  M
)  \  [ A ]  .~  ) ) ) )
1251243exp 1150 . . . . . . . 8  |-  ( ph  ->  ( x  e.  ( P  \  M )  ->  ( B  =  [ x ]  .~  ->  ( ( ( ( A ( seg `  G
) x )  i^i 
M )  =  (/)  \/ 
-.  ( ( A ( seg `  G
) x )  i^i 
M )  =  (/) )  ->  ( B  =  [ A ]  .~  \/  B  =  (
( P  \  M
)  \  [ A ]  .~  ) ) ) ) ) )
126125com14 82 . . . . . . 7  |-  ( ( ( ( A ( seg `  G ) x )  i^i  M
)  =  (/)  \/  -.  ( ( A ( seg `  G ) x )  i^i  M
)  =  (/) )  -> 
( x  e.  ( P  \  M )  ->  ( B  =  [ x ]  .~  ->  ( ph  ->  ( B  =  [ A ]  .~  \/  B  =  ( ( P  \  M )  \  [ A ]  .~  )
) ) ) ) )
1272, 126ax-mp 8 . . . . . 6  |-  ( x  e.  ( P  \  M )  ->  ( B  =  [ x ]  .~  ->  ( ph  ->  ( B  =  [ A ]  .~  \/  B  =  ( ( P 
\  M )  \  [ A ]  .~  )
) ) ) )
128127rexlimiv 2674 . . . . 5  |-  ( E. x  e.  ( P 
\  M ) B  =  [ x ]  .~  ->  ( ph  ->  ( B  =  [ A ]  .~  \/  B  =  ( ( P  \  M )  \  [ A ]  .~  )
) ) )
1291, 128syl6bi 219 . . . 4  |-  ( B  e.  ( ( P 
\  M ) /.  .~  )  ->  ( B  e.  ( ( P  \  M ) /.  .~  )  ->  ( ph  ->  ( B  =  [ A ]  .~  \/  B  =  ( ( P  \  M )  \  [ A ]  .~  )
) ) ) )
130129pm2.43i 43 . . 3  |-  ( B  e.  ( ( P 
\  M ) /.  .~  )  ->  ( ph  ->  ( B  =  [ A ]  .~  \/  B  =  ( ( P 
\  M )  \  [ A ]  .~  )
) ) )
131130com12 27 . 2  |-  ( ph  ->  ( B  e.  ( ( P  \  M
) /.  .~  )  ->  ( B  =  [ A ]  .~  \/  B  =  ( ( P 
\  M )  \  [ A ]  .~  )
) ) )
132 eqid 2296 . . . . . . 7  |-  [ A ]  .~  =  [ A ]  .~
133 eceq1 6712 . . . . . . . . 9  |-  ( a  =  A  ->  [ a ]  .~  =  [ A ]  .~  )
134133eqeq2d 2307 . . . . . . . 8  |-  ( a  =  A  ->  ( [ A ]  .~  =  [ a ]  .~  <->  [ A ]  .~  =  [ A ]  .~  )
)
135134rspcev 2897 . . . . . . 7  |-  ( ( A  e.  ( P 
\  M )  /\  [ A ]  .~  =  [ A ]  .~  )  ->  E. a  e.  ( P  \  M ) [ A ]  .~  =  [ a ]  .~  )
13613, 132, 135sylancl 643 . . . . . 6  |-  ( ph  ->  E. a  e.  ( P  \  M ) [ A ]  .~  =  [ a ]  .~  )
137 eceq2 6713 . . . . . . . . 9  |-  (  .~  =  ( (ss `  G ) `  M
)  ->  [ A ]  .~  =  [ A ] ( (ss `  G ) `  M
) )
1385, 137ax-mp 8 . . . . . . . 8  |-  [ A ]  .~  =  [ A ] ( (ss `  G ) `  M
)
139 fvex 5555 . . . . . . . . 9  |-  ( (ss
`  G ) `  M )  e.  _V
140 ecexg 6680 . . . . . . . . 9  |-  ( ( (ss `  G ) `
 M )  e. 
_V  ->  [ A ]
( (ss `  G
) `  M )  e.  _V )
141139, 140ax-mp 8 . . . . . . . 8  |-  [ A ] ( (ss `  G ) `  M
)  e.  _V
142138, 141eqeltri 2366 . . . . . . 7  |-  [ A ]  .~  e.  _V
143 elqsg 6727 . . . . . . 7  |-  ( [ A ]  .~  e.  _V  ->  ( [ A ]  .~  e.  ( ( P  \  M ) /.  .~  )  <->  E. a  e.  ( P  \  M
) [ A ]  .~  =  [ a ]  .~  ) )
144142, 143mp1i 11 . . . . . 6  |-  ( ph  ->  ( [ A ]  .~  e.  ( ( P 
\  M ) /.  .~  )  <->  E. a  e.  ( P  \  M ) [ A ]  .~  =  [ a ]  .~  ) )
145136, 144mpbird 223 . . . . 5  |-  ( ph  ->  [ A ]  .~  e.  ( ( P  \  M ) /.  .~  ) )
146 eleq1 2356 . . . . 5  |-  ( B  =  [ A ]  .~  ->  ( B  e.  ( ( P  \  M ) /.  .~  ) 
<->  [ A ]  .~  e.  ( ( P  \  M ) /.  .~  ) ) )
147145, 146syl5ibr 212 . . . 4  |-  ( B  =  [ A ]  .~  ->  ( ph  ->  B  e.  ( ( P 
\  M ) /.  .~  ) ) )
1483, 4, 11, 6, 13, 8lppotos 26247 . . . . . . 7  |-  ( ph  ->  E. b  e.  ( P  \  M ) ( ( A ( seg `  G ) b )  i^i  M
)  =/=  (/) )
149 eldif 3175 . . . . . . . . . . . 12  |-  ( x  e.  ( ( P 
\  M )  \  [ A ]  .~  )  <->  ( x  e.  ( P 
\  M )  /\  -.  x  e.  [ A ]  .~  ) )
150149a1i 10 . . . . . . . . . . 11  |-  ( ( ( ph  /\  b  e.  ( P  \  M
) )  /\  (
( A ( seg `  G ) b )  i^i  M )  =/=  (/) )  ->  ( x  e.  ( ( P 
\  M )  \  [ A ]  .~  )  <->  ( x  e.  ( P 
\  M )  /\  -.  x  e.  [ A ]  .~  ) ) )
151 simpllr 735 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  b  e.  ( P  \  M ) )  /\  ( ( A ( seg `  G ) b )  i^i  M
)  =/=  (/) )  /\  ( x  e.  ( P  \  M )  /\  -.  A  .~  x
) )  ->  b  e.  ( P  \  M
) )
152 simprl 732 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  b  e.  ( P  \  M ) )  /\  ( ( A ( seg `  G ) b )  i^i  M
)  =/=  (/) )  /\  ( x  e.  ( P  \  M )  /\  -.  A  .~  x
) )  ->  x  e.  ( P  \  M
) )
1536adantr 451 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  b  e.  ( P  \  M ) )  ->  G  e. Ibg )
154153adantr 451 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  b  e.  ( P  \  M
) )  /\  (
( A ( seg `  G ) b )  i^i  M )  =/=  (/) )  ->  G  e. Ibg )
155154adantl 452 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( x  e.  ( P 
\  M )  /\  ( ( ph  /\  b  e.  ( P  \  M ) )  /\  ( ( A ( seg `  G ) b )  i^i  M
)  =/=  (/) ) )  ->  G  e. Ibg )
1568adantr 451 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  b  e.  ( P  \  M ) )  ->  M  e.  L )
157156adantr 451 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  b  e.  ( P  \  M
) )  /\  (
( A ( seg `  G ) b )  i^i  M )  =/=  (/) )  ->  M  e.  L )
158157adantl 452 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( x  e.  ( P 
\  M )  /\  ( ( ph  /\  b  e.  ( P  \  M ) )  /\  ( ( A ( seg `  G ) b )  i^i  M
)  =/=  (/) ) )  ->  M  e.  L
)
15913adantr 451 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  b  e.  ( P  \  M ) )  ->  A  e.  ( P  \  M ) )
160159adantr 451 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  b  e.  ( P  \  M
) )  /\  (
( A ( seg `  G ) b )  i^i  M )  =/=  (/) )  ->  A  e.  ( P  \  M
) )
161160adantl 452 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( x  e.  ( P 
\  M )  /\  ( ( ph  /\  b  e.  ( P  \  M ) )  /\  ( ( A ( seg `  G ) b )  i^i  M
)  =/=  (/) ) )  ->  A  e.  ( P  \  M ) )
162 simpl 443 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( x  e.  ( P 
\  M )  /\  ( ( ph  /\  b  e.  ( P  \  M ) )  /\  ( ( A ( seg `  G ) b )  i^i  M
)  =/=  (/) ) )  ->  x  e.  ( P  \  M ) )
1633, 4, 5, 155, 158, 11, 161, 162isside1 26268 . . . . . . . . . . . . . . . . . . 19  |-  ( ( x  e.  ( P 
\  M )  /\  ( ( ph  /\  b  e.  ( P  \  M ) )  /\  ( ( A ( seg `  G ) b )  i^i  M
)  =/=  (/) ) )  ->  ( A  .~  x 
<->  ( A  e.  ( P  \  M )  /\  x  e.  ( P  \  M )  /\  ( ( A ( seg `  G
) x )  i^i 
M )  =  (/) ) ) )
164163notbid 285 . . . . . . . . . . . . . . . . . 18  |-  ( ( x  e.  ( P 
\  M )  /\  ( ( ph  /\  b  e.  ( P  \  M ) )  /\  ( ( A ( seg `  G ) b )  i^i  M
)  =/=  (/) ) )  ->  ( -.  A  .~  x  <->  -.  ( A  e.  ( P  \  M
)  /\  x  e.  ( P  \  M )  /\  ( ( A ( seg `  G
) x )  i^i 
M )  =  (/) ) ) )
165 3ianor 949 . . . . . . . . . . . . . . . . . . 19  |-  ( -.  ( A  e.  ( P  \  M )  /\  x  e.  ( P  \  M )  /\  ( ( A ( seg `  G
) x )  i^i 
M )  =  (/) ) 
<->  ( -.  A  e.  ( P  \  M
)  \/  -.  x  e.  ( P  \  M
)  \/  -.  (
( A ( seg `  G ) x )  i^i  M )  =  (/) ) )
166 pm2.24 101 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( A  e.  ( P  \  M )  ->  ( -.  A  e.  ( P  \  M )  -> 
( ( b ( seg `  G ) x )  i^i  M
)  =  (/) ) )
16713, 166syl 15 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  ( -.  A  e.  ( P  \  M
)  ->  ( (
b ( seg `  G
) x )  i^i 
M )  =  (/) ) )
168167adantr 451 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  b  e.  ( P  \  M ) )  ->  ( -.  A  e.  ( P  \  M )  ->  (
( b ( seg `  G ) x )  i^i  M )  =  (/) ) )
169168adantr 451 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  b  e.  ( P  \  M
) )  /\  (
( A ( seg `  G ) b )  i^i  M )  =/=  (/) )  ->  ( -.  A  e.  ( P 
\  M )  -> 
( ( b ( seg `  G ) x )  i^i  M
)  =  (/) ) )
170169adantl 452 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( x  e.  ( P 
\  M )  /\  ( ( ph  /\  b  e.  ( P  \  M ) )  /\  ( ( A ( seg `  G ) b )  i^i  M
)  =/=  (/) ) )  ->  ( -.  A  e.  ( P  \  M
)  ->  ( (
b ( seg `  G
) x )  i^i 
M )  =  (/) ) )
171170com12 27 . . . . . . . . . . . . . . . . . . . 20  |-  ( -.  A  e.  ( P 
\  M )  -> 
( ( x  e.  ( P  \  M
)  /\  ( ( ph  /\  b  e.  ( P  \  M ) )  /\  ( ( A ( seg `  G
) b )  i^i 
M )  =/=  (/) ) )  ->  ( ( b ( seg `  G
) x )  i^i 
M )  =  (/) ) )
172 pm2.24 101 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  e.  ( P  \  M )  ->  ( -.  x  e.  ( P  \  M )  -> 
( ( b ( seg `  G ) x )  i^i  M
)  =  (/) ) )
173172adantr 451 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( x  e.  ( P 
\  M )  /\  ( ( ph  /\  b  e.  ( P  \  M ) )  /\  ( ( A ( seg `  G ) b )  i^i  M
)  =/=  (/) ) )  ->  ( -.  x  e.  ( P  \  M
)  ->  ( (
b ( seg `  G
) x )  i^i 
M )  =  (/) ) )
174173com12 27 . . . . . . . . . . . . . . . . . . . 20  |-  ( -.  x  e.  ( P 
\  M )  -> 
( ( x  e.  ( P  \  M
)  /\  ( ( ph  /\  b  e.  ( P  \  M ) )  /\  ( ( A ( seg `  G
) b )  i^i 
M )  =/=  (/) ) )  ->  ( ( b ( seg `  G
) x )  i^i 
M )  =  (/) ) )
175 oveq2 5882 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( x  =  b  ->  (
b ( seg `  G
) x )  =  ( b ( seg `  G ) b ) )
176175equcoms 1666 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( b  =  x  ->  (
b ( seg `  G
) x )  =  ( b ( seg `  G ) b ) )
177176adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( b  =  x  /\  ( -.  ( ( A ( seg `  G
) x )  i^i 
M )  =  (/)  /\  ( x  e.  ( P  \  M )  /\  ( ( ph  /\  b  e.  ( P 
\  M ) )  /\  ( ( A ( seg `  G
) b )  i^i 
M )  =/=  (/) ) ) ) )  ->  (
b ( seg `  G
) x )  =  ( b ( seg `  G ) b ) )
178155ad2antll 709 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( b  =  x  /\  ( -.  ( ( A ( seg `  G
) x )  i^i 
M )  =  (/)  /\  ( x  e.  ( P  \  M )  /\  ( ( ph  /\  b  e.  ( P 
\  M ) )  /\  ( ( A ( seg `  G
) b )  i^i 
M )  =/=  (/) ) ) ) )  ->  G  e. Ibg )
179 eldifi 3311 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( b  e.  ( P  \  M )  ->  b  e.  P )
180179ad2antlr 707 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ph  /\  b  e.  ( P  \  M
) )  /\  (
( A ( seg `  G ) b )  i^i  M )  =/=  (/) )  ->  b  e.  P )
181180adantl 452 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( x  e.  ( P 
\  M )  /\  ( ( ph  /\  b  e.  ( P  \  M ) )  /\  ( ( A ( seg `  G ) b )  i^i  M
)  =/=  (/) ) )  ->  b  e.  P
)
182181ad2antll 709 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( b  =  x  /\  ( -.  ( ( A ( seg `  G
) x )  i^i 
M )  =  (/)  /\  ( x  e.  ( P  \  M )  /\  ( ( ph  /\  b  e.  ( P 
\  M ) )  /\  ( ( A ( seg `  G
) b )  i^i 
M )  =/=  (/) ) ) ) )  ->  b  e.  P )
1833, 11, 178, 182sgplpte22 26241 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( b  =  x  /\  ( -.  ( ( A ( seg `  G
) x )  i^i 
M )  =  (/)  /\  ( x  e.  ( P  \  M )  /\  ( ( ph  /\  b  e.  ( P 
\  M ) )  /\  ( ( A ( seg `  G
) b )  i^i 
M )  =/=  (/) ) ) ) )  ->  (
b ( seg `  G
) b )  =  { b } )
184177, 183eqtrd 2328 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( b  =  x  /\  ( -.  ( ( A ( seg `  G
) x )  i^i 
M )  =  (/)  /\  ( x  e.  ( P  \  M )  /\  ( ( ph  /\  b  e.  ( P 
\  M ) )  /\  ( ( A ( seg `  G
) b )  i^i 
M )  =/=  (/) ) ) ) )  ->  (
b ( seg `  G
) x )  =  { b } )
185184ineq1d 3382 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( b  =  x  /\  ( -.  ( ( A ( seg `  G
) x )  i^i 
M )  =  (/)  /\  ( x  e.  ( P  \  M )  /\  ( ( ph  /\  b  e.  ( P 
\  M ) )  /\  ( ( A ( seg `  G
) b )  i^i 
M )  =/=  (/) ) ) ) )  ->  (
( b ( seg `  G ) x )  i^i  M )  =  ( { b }  i^i  M ) )
186 incom 3374 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( { b }  i^i  M
)  =  ( M  i^i  { b } )
187 eldifn 3312 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( b  e.  ( P  \  M )  ->  -.  b  e.  M )
188187ad2antlr 707 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  b  e.  ( P  \  M
) )  /\  (
( A ( seg `  G ) b )  i^i  M )  =/=  (/) )  ->  -.  b  e.  M )
189188adantl 452 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( x  e.  ( P 
\  M )  /\  ( ( ph  /\  b  e.  ( P  \  M ) )  /\  ( ( A ( seg `  G ) b )  i^i  M
)  =/=  (/) ) )  ->  -.  b  e.  M )
190189ad2antll 709 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( b  =  x  /\  ( -.  ( ( A ( seg `  G
) x )  i^i 
M )  =  (/)  /\  ( x  e.  ( P  \  M )  /\  ( ( ph  /\  b  e.  ( P 
\  M ) )  /\  ( ( A ( seg `  G
) b )  i^i 
M )  =/=  (/) ) ) ) )  ->  -.  b  e.  M )
191 disjsn 3706 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( M  i^i  { b } )  =  (/)  <->  -.  b  e.  M )
192190, 191sylibr 203 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( b  =  x  /\  ( -.  ( ( A ( seg `  G
) x )  i^i 
M )  =  (/)  /\  ( x  e.  ( P  \  M )  /\  ( ( ph  /\  b  e.  ( P 
\  M ) )  /\  ( ( A ( seg `  G
) b )  i^i 
M )  =/=  (/) ) ) ) )  ->  ( M  i^i  { b } )  =  (/) )
193186, 192syl5eq 2340 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( b  =  x  /\  ( -.  ( ( A ( seg `  G
) x )  i^i 
M )  =  (/)  /\  ( x  e.  ( P  \  M )  /\  ( ( ph  /\  b  e.  ( P 
\  M ) )  /\  ( ( A ( seg `  G
) b )  i^i 
M )  =/=  (/) ) ) ) )  ->  ( { b }  i^i  M )  =  (/) )
194185, 193eqtrd 2328 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( b  =  x  /\  ( -.  ( ( A ( seg `  G
) x )  i^i 
M )  =  (/)  /\  ( x  e.  ( P  \  M )  /\  ( ( ph  /\  b  e.  ( P 
\  M ) )  /\  ( ( A ( seg `  G
) b )  i^i 
M )  =/=  (/) ) ) ) )  ->  (
( b ( seg `  G ) x )  i^i  M )  =  (/) )
195155ad2antll 709 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( -.  b  =  x  /\  ( -.  (
( A ( seg `  G ) x )  i^i  M )  =  (/)  /\  ( x  e.  ( P  \  M
)  /\  ( ( ph  /\  b  e.  ( P  \  M ) )  /\  ( ( A ( seg `  G
) b )  i^i 
M )  =/=  (/) ) ) ) )  ->  G  e. Ibg )
196158ad2antll 709 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( -.  b  =  x  /\  ( -.  (
( A ( seg `  G ) x )  i^i  M )  =  (/)  /\  ( x  e.  ( P  \  M
)  /\  ( ( ph  /\  b  e.  ( P  \  M ) )  /\  ( ( A ( seg `  G
) b )  i^i 
M )  =/=  (/) ) ) ) )  ->  M  e.  L )
197 simprlr 739 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( x  e.  ( P 
\  M )  /\  ( ( ph  /\  b  e.  ( P  \  M ) )  /\  ( ( A ( seg `  G ) b )  i^i  M
)  =/=  (/) ) )  ->  b  e.  ( P  \  M ) )
198197ad2antll 709 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( -.  b  =  x  /\  ( -.  (
( A ( seg `  G ) x )  i^i  M )  =  (/)  /\  ( x  e.  ( P  \  M
)  /\  ( ( ph  /\  b  e.  ( P  \  M ) )  /\  ( ( A ( seg `  G
) b )  i^i 
M )  =/=  (/) ) ) ) )  ->  b  e.  ( P  \  M
) )
199161ad2antll 709 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( -.  b  =  x  /\  ( -.  (
( A ( seg `  G ) x )  i^i  M )  =  (/)  /\  ( x  e.  ( P  \  M
)  /\  ( ( ph  /\  b  e.  ( P  \  M ) )  /\  ( ( A ( seg `  G
) b )  i^i 
M )  =/=  (/) ) ) ) )  ->  A  e.  ( P  \  M
) )
200 simprl 732 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( -.  ( ( A ( seg `  G
) x )  i^i 
M )  =  (/)  /\  ( x  e.  ( P  \  M )  /\  ( ( ph  /\  b  e.  ( P 
\  M ) )  /\  ( ( A ( seg `  G
) b )  i^i 
M )  =/=  (/) ) ) )  ->  x  e.  ( P  \  M ) )
201200adantl 452 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( -.  b  =  x  /\  ( -.  (
( A ( seg `  G ) x )  i^i  M )  =  (/)  /\  ( x  e.  ( P  \  M
)  /\  ( ( ph  /\  b  e.  ( P  \  M ) )  /\  ( ( A ( seg `  G
) b )  i^i 
M )  =/=  (/) ) ) ) )  ->  x  e.  ( P  \  M
) )
20215adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  b  e.  ( P  \  M ) )  ->  A  e.  P )
203179adantl 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  b  e.  ( P  \  M ) )  ->  b  e.  P )
2043, 11, 153, 202, 203xsyysx 26248 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  b  e.  ( P  \  M ) )  ->  ( A
( seg `  G
) b )  =  ( b ( seg `  G ) A ) )
205204ineq1d 3382 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  b  e.  ( P  \  M ) )  ->  ( ( A ( seg `  G
) b )  i^i 
M )  =  ( ( b ( seg `  G ) A )  i^i  M ) )
206205neeq1d 2472 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  b  e.  ( P  \  M ) )  ->  ( (
( A ( seg `  G ) b )  i^i  M )  =/=  (/) 
<->  ( ( b ( seg `  G ) A )  i^i  M
)  =/=  (/) ) )
207206biimpa 470 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  b  e.  ( P  \  M
) )  /\  (
( A ( seg `  G ) b )  i^i  M )  =/=  (/) )  ->  ( ( b ( seg `  G
) A )  i^i 
M )  =/=  (/) )
208207adantl 452 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( x  e.  ( P 
\  M )  /\  ( ( ph  /\  b  e.  ( P  \  M ) )  /\  ( ( A ( seg `  G ) b )  i^i  M
)  =/=  (/) ) )  ->  ( ( b ( seg `  G
) A )  i^i 
M )  =/=  (/) )
209208ad2antll 709 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( -.  b  =  x  /\  ( -.  (
( A ( seg `  G ) x )  i^i  M )  =  (/)  /\  ( x  e.  ( P  \  M
)  /\  ( ( ph  /\  b  e.  ( P  \  M ) )  /\  ( ( A ( seg `  G
) b )  i^i 
M )  =/=  (/) ) ) ) )  ->  (
( b ( seg `  G ) A )  i^i  M )  =/=  (/) )
210 simprl 732 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( -.  b  =  x  /\  ( -.  (
( A ( seg `  G ) x )  i^i  M )  =  (/)  /\  ( x  e.  ( P  \  M
)  /\  ( ( ph  /\  b  e.  ( P  \  M ) )  /\  ( ( A ( seg `  G
) b )  i^i 
M )  =/=  (/) ) ) ) )  ->  -.  ( ( A ( seg `  G ) x )  i^i  M
)  =  (/) )
211 df-ne 2461 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( A ( seg `  G ) x )  i^i  M )  =/=  (/) 
<->  -.  ( ( A ( seg `  G
) x )  i^i 
M )  =  (/) )
212210, 211sylibr 203 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( -.  b  =  x  /\  ( -.  (
( A ( seg `  G ) x )  i^i  M )  =  (/)  /\  ( x  e.  ( P  \  M
)  /\  ( ( ph  /\  b  e.  ( P  \  M ) )  /\  ( ( A ( seg `  G
) b )  i^i 
M )  =/=  (/) ) ) ) )  ->  (
( A ( seg `  G ) x )  i^i  M )  =/=  (/) )
2133, 4, 11, 195, 196, 198, 199, 201, 209, 212nbssntrs 26250 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( -.  b  =  x  /\  ( -.  (
( A ( seg `  G ) x )  i^i  M )  =  (/)  /\  ( x  e.  ( P  \  M
)  /\  ( ( ph  /\  b  e.  ( P  \  M ) )  /\  ( ( A ( seg `  G
) b )  i^i 
M )  =/=  (/) ) ) ) )  ->  (
( b ( seg `  G ) x )  i^i  M )  =  (/) )
214194, 213pm2.61ian 765 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( -.  ( ( A ( seg `  G
) x )  i^i 
M )  =  (/)  /\  ( x  e.  ( P  \  M )  /\  ( ( ph  /\  b  e.  ( P 
\  M ) )  /\  ( ( A ( seg `  G
) b )  i^i 
M )  =/=  (/) ) ) )  ->  ( (
b ( seg `  G
) x )  i^i 
M )  =  (/) )
215214ex 423 . . . . . . . . . . . . . . . . . . . 20  |-  ( -.  ( ( A ( seg `  G ) x )  i^i  M
)  =  (/)  ->  (
( x  e.  ( P  \  M )  /\  ( ( ph  /\  b  e.  ( P 
\  M ) )  /\  ( ( A ( seg `  G
) b )  i^i 
M )  =/=  (/) ) )  ->  ( ( b ( seg `  G
) x )  i^i 
M )  =  (/) ) )
216171, 174, 2153jaoi 1245 . . . . . . . . . . . . . . . . . . 19  |-  ( ( -.  A  e.  ( P  \  M )  \/  -.  x  e.  ( P  \  M
)  \/  -.  (
( A ( seg `  G ) x )  i^i  M )  =  (/) )  ->  ( ( x  e.  ( P 
\  M )  /\  ( ( ph  /\  b  e.  ( P  \  M ) )  /\  ( ( A ( seg `  G ) b )  i^i  M
)  =/=  (/) ) )  ->  ( ( b ( seg `  G
) x )  i^i 
M )  =  (/) ) )
217165, 216sylbi 187 . . . . . . . . . . . . . . . . . 18  |-  ( -.  ( A  e.  ( P  \  M )  /\  x  e.  ( P  \  M )  /\  ( ( A ( seg `  G
) x )  i^i 
M )  =  (/) )  ->  ( ( x  e.  ( P  \  M )  /\  (
( ph  /\  b  e.  ( P  \  M
) )  /\  (
( A ( seg `  G ) b )  i^i  M )  =/=  (/) ) )  ->  (
( b ( seg `  G ) x )  i^i  M )  =  (/) ) )
218164, 217syl6bi 219 . . . . . . . . . . . . . . . . 17  |-  ( ( x  e.  ( P 
\  M )  /\  ( ( ph  /\  b  e.  ( P  \  M ) )  /\  ( ( A ( seg `  G ) b )  i^i  M
)  =/=  (/) ) )  ->  ( -.  A  .~  x  ->  ( ( x  e.  ( P 
\  M )  /\  ( ( ph  /\  b  e.  ( P  \  M ) )  /\  ( ( A ( seg `  G ) b )  i^i  M
)  =/=  (/) ) )  ->  ( ( b ( seg `  G
) x )  i^i 
M )  =  (/) ) ) )
219218pm2.43a 45 . . . . . . . . . . . . . . . 16  |-  ( ( x  e.  ( P 
\  M )  /\  ( ( ph  /\  b  e.  ( P  \  M ) )  /\  ( ( A ( seg `  G ) b )  i^i  M
)  =/=  (/) ) )  ->  ( -.  A  .~  x  ->  ( ( b ( seg `  G
) x )  i^i 
M )  =  (/) ) )
220219impancom 427 . . . . . . . . . . . . . . 15  |-  ( ( x  e.  ( P 
\  M )  /\  -.  A  .~  x
)  ->  ( (
( ph  /\  b  e.  ( P  \  M
) )  /\  (
( A ( seg `  G ) b )  i^i  M )  =/=  (/) )  ->  ( ( b ( seg `  G
) x )  i^i 
M )  =  (/) ) )
221220impcom 419 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  b  e.  ( P  \  M ) )  /\  ( ( A ( seg `  G ) b )  i^i  M
)  =/=  (/) )  /\  ( x  e.  ( P  \  M )  /\  -.  A  .~  x
) )  ->  (
( b ( seg `  G ) x )  i^i  M )  =  (/) )
222151, 152, 2213jca 1132 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  b  e.  ( P  \  M ) )  /\  ( ( A ( seg `  G ) b )  i^i  M
)  =/=  (/) )  /\  ( x  e.  ( P  \  M )  /\  -.  A  .~  x
) )  ->  (
b  e.  ( P 
\  M )  /\  x  e.  ( P  \  M )  /\  (
( b ( seg `  G ) x )  i^i  M )  =  (/) ) )
223 simpr2 962 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  b  e.  ( P  \  M ) )  /\  ( ( A ( seg `  G ) b )  i^i  M
)  =/=  (/) )  /\  ( b  e.  ( P  \  M )  /\  x  e.  ( P  \  M )  /\  ( ( b ( seg `  G
) x )  i^i 
M )  =  (/) ) )  ->  x  e.  ( P  \  M
) )
224 df-ne 2461 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( A ( seg `  G ) b )  i^i  M )  =/=  (/) 
<->  -.  ( ( A ( seg `  G
) b )  i^i 
M )  =  (/) )
225153ad2antlr 707 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( b  e.  ( P  \  M
)  /\  x  e.  ( P  \  M )  /\  ( ( b ( seg `  G
) x )  i^i 
M )  =  (/) )  /\  ( ph  /\  b  e.  ( P  \  M ) ) )  /\  ( ( A ( seg `  G
) x )  i^i 
M )  =  (/) )  ->  G  e. Ibg )
226156ad2antlr 707 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( b  e.  ( P  \  M
)  /\  x  e.  ( P  \  M )  /\  ( ( b ( seg `  G
) x )  i^i 
M )  =  (/) )  /\  ( ph  /\  b  e.  ( P  \  M ) ) )  /\  ( ( A ( seg `  G
) x )  i^i 
M )  =  (/) )  ->  M  e.  L
)
227159ad2antlr 707 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( b  e.  ( P  \  M
)  /\  x  e.  ( P  \  M )  /\  ( ( b ( seg `  G
) x )  i^i 
M )  =  (/) )  /\  ( ph  /\  b  e.  ( P  \  M ) ) )  /\  ( ( A ( seg `  G
) x )  i^i 
M )  =  (/) )  ->  A  e.  ( P  \  M ) )
228 simpl2 959 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( b  e.  ( P  \  M )  /\  x  e.  ( P  \  M )  /\  ( ( b ( seg `  G
) x )  i^i 
M )  =  (/) )  /\  ( ph  /\  b  e.  ( P  \  M ) ) )  ->  x  e.  ( P  \  M ) )
229228adantr 451 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( b  e.  ( P  \  M
)  /\  x  e.  ( P  \  M )  /\  ( ( b ( seg `  G
) x )  i^i 
M )  =  (/) )  /\  ( ph  /\  b  e.  ( P  \  M ) ) )  /\  ( ( A ( seg `  G
) x )  i^i 
M )  =  (/) )  ->  x  e.  ( P  \  M ) )
230 simplrr 737 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( b  e.  ( P  \  M
)  /\  x  e.  ( P  \  M )  /\  ( ( b ( seg `  G
) x )  i^i 
M )  =  (/) )  /\  ( ph  /\  b  e.  ( P  \  M ) ) )  /\  ( ( A ( seg `  G
) x )  i^i 
M )  =  (/) )  ->  b  e.  ( P  \  M ) )
231 simpr 447 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( b  e.  ( P  \  M
)  /\  x  e.  ( P  \  M )  /\  ( ( b ( seg `  G
) x )  i^i 
M )  =  (/) )  /\  ( ph  /\  b  e.  ( P  \  M ) ) )  /\  ( ( A ( seg `  G
) x )  i^i 
M )  =  (/) )  ->  ( ( A ( seg `  G
) x )  i^i 
M )  =  (/) )
2321533ad2ant3 978 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( b  e.  ( P 
\  M )  /\  x  e.  ( P  \  M )  /\  ( ph  /\  b  e.  ( P  \  M ) ) )  ->  G  e. Ibg )
2331793ad2ant1 976 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( b  e.  ( P 
\  M )  /\  x  e.  ( P  \  M )  /\  ( ph  /\  b  e.  ( P  \  M ) ) )  ->  b  e.  P )
234173ad2ant2 977 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( b  e.  ( P 
\  M )  /\  x  e.  ( P  \  M )  /\  ( ph  /\  b  e.  ( P  \  M ) ) )  ->  x  e.  P )
2353, 11, 232, 233, 234xsyysx 26248 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( b  e.  ( P 
\  M )  /\  x  e.  ( P  \  M )  /\  ( ph  /\  b  e.  ( P  \  M ) ) )  ->  (
b ( seg `  G
) x )  =  ( x ( seg `  G ) b ) )
236235ineq1d 3382 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( b  e.  ( P 
\  M )  /\  x  e.  ( P  \  M )  /\  ( ph  /\  b  e.  ( P  \  M ) ) )  ->  (
( b ( seg `  G ) x )  i^i  M )  =  ( ( x ( seg `  G ) b )  i^i  M
) )
237236eqeq1d 2304 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( b  e.  ( P 
\  M )  /\  x  e.  ( P  \  M )  /\  ( ph  /\  b  e.  ( P  \  M ) ) )  ->  (
( ( b ( seg `  G ) x )  i^i  M
)  =  (/)  <->  ( (
x ( seg `  G
) b )  i^i 
M )  =  (/) ) )
238237biimpd 198 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( b  e.  ( P 
\  M )  /\  x  e.  ( P  \  M )  /\  ( ph  /\  b  e.  ( P  \  M ) ) )  ->  (
( ( b ( seg `  G ) x )  i^i  M
)  =  (/)  ->  (
( x ( seg `  G ) b )  i^i  M )  =  (/) ) )
2392383exp 1150 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( b  e.  ( P  \  M )  ->  (
x  e.  ( P 
\  M )  -> 
( ( ph  /\  b  e.  ( P  \  M ) )  -> 
( ( ( b ( seg `  G
) x )  i^i 
M )  =  (/)  ->  ( ( x ( seg `  G ) b )  i^i  M
)  =  (/) ) ) ) )
240239com34 77 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( b  e.  ( P  \  M )  ->  (
x  e.  ( P 
\  M )  -> 
( ( ( b ( seg `  G
) x )  i^i 
M )  =  (/)  ->  ( ( ph  /\  b  e.  ( P  \  M ) )  -> 
( ( x ( seg `  G ) b )  i^i  M
)  =  (/) ) ) ) )
2412403imp1 1164 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( b  e.  ( P  \  M )  /\  x  e.  ( P  \  M )  /\  ( ( b ( seg `  G
) x )  i^i 
M )  =  (/) )  /\  ( ph  /\  b  e.  ( P  \  M ) ) )  ->  ( ( x ( seg `  G
) b )  i^i 
M )  =  (/) )
242241adantr 451 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( b  e.  ( P  \  M
)  /\  x  e.  ( P  \  M )  /\  ( ( b ( seg `  G
) x )  i^i 
M )  =  (/) )  /\  ( ph  /\  b  e.  ( P  \  M ) ) )  /\  ( ( A ( seg `  G
) x )  i^i 
M )  =  (/) )  ->  ( ( x ( seg `  G
) b )  i^i 
M )  =  (/) )
2433, 4, 11, 225, 226, 227, 229, 230, 231, 242bsstrs 26249 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( b  e.  ( P  \  M
)  /\  x  e.  ( P  \  M )  /\  ( ( b ( seg `  G
) x )  i^i 
M )  =  (/) )  /\  ( ph  /\  b  e.  ( P  \  M ) ) )  /\  ( ( A ( seg `  G
) x )  i^i 
M )  =  (/) )  ->  ( ( A ( seg `  G
) b )  i^i 
M )  =  (/) )
244243ex 423 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( b  e.  ( P  \  M )  /\  x  e.  ( P  \  M )  /\  ( ( b ( seg `  G
) x )  i^i 
M )  =  (/) )  /\  ( ph  /\  b  e.  ( P  \  M ) ) )  ->  ( ( ( A ( seg `  G
) x )  i^i 
M )  =  (/)  ->  ( ( A ( seg `  G ) b )  i^i  M
)  =  (/) ) )
245244con3d 125 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( b  e.  ( P  \  M )  /\  x  e.  ( P  \  M )  /\  ( ( b ( seg `  G
) x )  i^i 
M )  =  (/) )  /\  ( ph  /\  b  e.  ( P  \  M ) ) )  ->  ( -.  (
( A ( seg `  G ) b )  i^i  M )  =  (/)  ->  -.  ( ( A ( seg `  G
) x )  i^i 
M )  =  (/) ) )
246245ex 423 . . . . . . . . . . . . . . . . . . 19  |-  ( ( b  e.  ( P 
\  M )  /\  x  e.  ( P  \  M )  /\  (
( b ( seg `  G ) x )  i^i  M )  =  (/) )  ->  ( (
ph  /\  b  e.  ( P  \  M ) )  ->  ( -.  ( ( A ( seg `  G ) b )  i^i  M
)  =  (/)  ->  -.  ( ( A ( seg `  G ) x )  i^i  M
)  =  (/) ) ) )
247246com13 74 . . . . . . . . . . . . . . . . . 18  |-  ( -.  ( ( A ( seg `  G ) b )  i^i  M
)  =  (/)  ->  (
( ph  /\  b  e.  ( P  \  M
) )  ->  (
( b  e.  ( P  \  M )  /\  x  e.  ( P  \  M )  /\  ( ( b ( seg `  G
) x )  i^i 
M )  =  (/) )  ->  -.  ( ( A ( seg `  G
) x )  i^i 
M )  =  (/) ) ) )
248224, 247sylbi 187 . . . . . . . . . . . . . . . . 17  |-  ( ( ( A ( seg `  G ) b )  i^i  M )  =/=  (/)  ->  ( ( ph  /\  b  e.  ( P 
\  M ) )  ->  ( ( b  e.  ( P  \  M )  /\  x  e.  ( P  \  M
)  /\  ( (
b ( seg `  G
) x )  i^i 
M )  =  (/) )  ->  -.  ( ( A ( seg `  G
) x )  i^i 
M )  =  (/) ) ) )
249248impcom 419 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  b  e.  ( P  \  M
) )  /\  (
( A ( seg `  G ) b )  i^i  M )  =/=  (/) )  ->  ( ( b  e.  ( P 
\  M )  /\  x  e.  ( P  \  M )  /\  (
( b ( seg `  G ) x )  i^i  M )  =  (/) )  ->  -.  (
( A ( seg `  G ) x )  i^i  M )  =  (/) ) )
250249imp 418 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  b  e.  ( P  \  M ) )  /\  ( ( A ( seg `  G ) b )  i^i  M
)  =/=  (/) )  /\  ( b  e.  ( P  \  M )  /\  x  e.  ( P  \  M )  /\  ( ( b ( seg `  G
) x )  i^i 
M )  =  (/) ) )  ->  -.  ( ( A ( seg `  G ) x )  i^i  M
)  =  (/) )
251154adantr 451 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  b  e.  ( P  \  M ) )  /\  ( ( A ( seg `  G ) b )  i^i  M
)  =/=  (/) )  /\  ( b  e.  ( P  \  M )  /\  x  e.  ( P  \  M )  /\  ( ( b ( seg `  G
) x )  i^i 
M )  =  (/) ) )  ->  G  e. Ibg )
252157adantr 451 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  b  e.  ( P  \  M ) )  /\  ( ( A ( seg `  G ) b )  i^i  M
)  =/=  (/) )  /\  ( b  e.  ( P  \  M )  /\  x  e.  ( P  \  M )  /\  ( ( b ( seg `  G
) x )  i^i 
M )  =  (/) ) )  ->  M  e.  L )
253160adantr 451 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  b  e.  ( P  \  M ) )  /\  ( ( A ( seg `  G ) b )  i^i  M
)  =/=  (/) )  /\  ( b  e.  ( P  \  M )  /\  x  e.  ( P  \  M )  /\  ( ( b ( seg `  G
) x )  i^i 
M )  =  (/) ) )  ->  A  e.  ( P  \  M
) )
2543, 4, 5, 251, 252, 11, 253, 223isside 26269 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  b  e.  ( P  \  M ) )  /\  ( ( A ( seg `  G ) b )  i^i  M
)  =/=  (/) )  /\  ( b  e.  ( P  \  M )  /\  x  e.  ( P  \  M )  /\  ( ( b ( seg `  G
) x )  i^i 
M )  =  (/) ) )  ->  ( A  .~  x  <->  ( ( A ( seg `  G
) x )  i^i 
M )  =  (/) ) )
255250, 254mtbird 292 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  b  e.  ( P  \  M ) )  /\  ( ( A ( seg `  G ) b )  i^i  M
)  =/=  (/) )  /\  ( b  e.  ( P  \  M )  /\  x  e.  ( P  \  M )  /\  ( ( b ( seg `  G
) x )  i^i 
M )  =  (/) ) )  ->  -.  A  .~  x )
256223, 255jca 518 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  b  e.  ( P  \  M ) )  /\  ( ( A ( seg `  G ) b )  i^i  M
)  =/=  (/) )  /\  ( b  e.  ( P  \  M )  /\  x  e.  ( P  \  M )  /\  ( ( b ( seg `  G
) x )  i^i 
M )  =  (/) ) )  ->  (
x  e.  ( P 
\  M )  /\  -.  A  .~  x
) )
257222, 256impbida 805 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  b  e.  ( P  \  M
) )  /\  (
( A ( seg `  G ) b )  i^i  M )  =/=  (/) )  ->  ( ( x  e.  ( P 
\  M )  /\  -.  A  .~  x
)  <->  ( b  e.  ( P  \  M
)  /\  x  e.  ( P  \  M )  /\  ( ( b ( seg `  G
) x )  i^i 
M )  =  (/) ) ) )
258 elecg 6714 . . . . . . . . . . . . . . 15  |-  ( ( x  e.  _V  /\  A  e.  ( P  \  M ) )  -> 
( x  e.  [ A ]  .~  <->  A  .~  x ) )
25936, 160, 258sylancr 644 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  b  e.  ( P  \  M
) )  /\  (
( A ( seg `  G ) b )  i^i  M )  =/=  (/) )  ->  ( x  e.  [ A ]  .~ 
<->  A  .~  x ) )
260259notbid 285 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  b  e.  ( P  \  M
) )  /\  (
( A ( seg `  G ) b )  i^i  M )  =/=  (/) )  ->  ( -.  x  e.  [ A ]  .~  <->  -.  A  .~  x ) )
261260anbi2d 684 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  b  e.  ( P  \  M
) )  /\  (
( A ( seg `  G ) b )  i^i  M )  =/=  (/) )  ->  ( ( x  e.  ( P 
\  M )  /\  -.  x  e.  [ A ]  .~  )  <->  ( x  e.  ( P  \  M
)  /\  -.  A  .~  x ) ) )
262 vex 2804 . . . . . . . . . . . . . . . 16  |-  b  e. 
_V
263262a1i 10 . . . . . . . . . . . . . . 15  |-  ( ph  ->  b  e.  _V )
26436a1i 10 . . . . . . . . . . . . . . 15  |-  ( ph  ->  x  e.  _V )
2653, 4, 5, 6, 8, 11, 263, 264isside1 26268 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( b  .~  x  <->  ( b  e.  ( P 
\  M )  /\  x  e.  ( P  \  M )  /\  (
( b ( seg `  G ) x )  i^i  M )  =  (/) ) ) )
266265adantr 451 . . . . . . . . . . . . 13  |-  ( (
ph  /\  b  e.  ( P  \  M ) )  ->  ( b  .~  x  <->  ( b  e.  ( P  \  M
)  /\  x  e.  ( P  \  M )  /\  ( ( b ( seg `  G
) x )  i^i 
M )  =  (/) ) ) )
267266adantr 451 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  b  e.  ( P  \  M
) )  /\  (
( A ( seg `  G ) b )  i^i  M )  =/=  (/) )  ->  ( b  .~  x  <->  ( b  e.  ( P  \  M
)  /\  x  e.  ( P  \  M )  /\  ( ( b ( seg `  G
) x )  i^i 
M )  =  (/) ) ) )
268257, 261, 2673bitr4d 276 . . . . . . . . . . 11  |-  ( ( ( ph  /\  b  e.  ( P  \  M
) )  /\  (
( A ( seg `  G ) b )  i^i  M )  =/=  (/) )  ->  ( ( x  e.  ( P 
\  M )  /\  -.  x  e.  [ A ]  .~  )  <->  b  .~  x ) )
26936, 262pm3.2i 441 . . . . . . . . . . . 12  |-  ( x  e.  _V  /\  b  e.  _V )
270 elecg 6714 . . . . . . . . . . . . 13  |-  ( ( x  e.  _V  /\  b  e.  _V )  ->  ( x  e.  [
b ]  .~  <->  b  .~  x ) )
271270bicomd 192 . . . . . . . . . . . 12  |-  ( ( x  e.  _V  /\  b  e.  _V )  ->  ( b  .~  x  <->  x  e.  [ b ]  .~  ) )
272269, 271mp1i 11 . . . . . . . . . . 11  |-  ( ( ( ph  /\  b  e.  ( P  \  M
) )  /\  (
( A ( seg `  G ) b )  i^i  M )  =/=  (/) )  ->  ( b  .~  x  <->  x  e.  [ b ]  .~  )
)
273150, 268, 2723bitrd 270 . . . . . . . . . 10  |-  ( ( ( ph  /\  b  e.  ( P  \  M
) )  /\  (
( A ( seg `  G ) b )  i^i  M )  =/=  (/) )  ->  ( x  e.  ( ( P 
\  M )  \  [ A ]  .~  )  <->  x  e.  [ b ]  .~  ) )
274273eqrdv 2294 . . . . . . . . 9  |-  ( ( ( ph  /\  b  e.  ( P  \  M
) )  /\  (
( A ( seg `  G ) b )  i^i  M )  =/=  (/) )  ->  ( ( P  \  M ) 
\  [ A ]  .~  )  =  [
b ]  .~  )
275274ex 423 . . . . . . . 8  |-  ( (
ph  /\  b  e.  ( P  \  M ) )  ->  ( (
( A ( seg `  G ) b )  i^i  M )  =/=  (/)  ->  ( ( P 
\  M )  \  [ A ]  .~  )  =  [ b ]  .~  ) )
276275reximdva 2668 . . . . . . 7  |-  ( ph  ->  ( E. b  e.  ( P  \  M
) ( ( A ( seg `  G
) b )  i^i 
M )  =/=  (/)  ->  E. b  e.  ( P  \  M
) ( ( P 
\  M )  \  [ A ]  .~  )  =  [ b ]  .~  ) )
277148, 276mpd 14 . . . . . 6  |-  ( ph  ->  E. b  e.  ( P  \  M ) ( ( P  \  M )  \  [ A ]  .~  )  =  [ b ]  .~  )
278 fvex 5555 . . . . . . . . 9  |-  (PPoints `  G
)  e.  _V
2793, 278eqeltri 2366 . . . . . . . 8  |-  P  e. 
_V
280 difexg 4178 . . . . . . . 8  |-  ( P  e.  _V  ->  ( P  \  M )  e. 
_V )
281279, 280ax-mp 8 . . . . . . 7  |-  ( P 
\  M )  e. 
_V
282 difexg 4178 . . . . . . 7  |-  ( ( P  \  M )  e.  _V  ->  (
( P  \  M
)  \  [ A ]  .~  )  e.  _V )
283 elqsg 6727 . . . . . . 7  |-  ( ( ( P  \  M
)  \  [ A ]  .~  )  e.  _V  ->  ( ( ( P 
\  M )  \  [ A ]  .~  )  e.  ( ( P  \  M ) /.  .~  ) 
<->  E. b  e.  ( P  \  M ) ( ( P  \  M )  \  [ A ]  .~  )  =  [ b ]  .~  ) )
284281, 282, 283mp2b 9 . . . . . 6  |-  ( ( ( P  \  M
)  \  [ A ]  .~  )  e.  ( ( P  \  M
) /.  .~  )  <->  E. b  e.  ( P 
\  M ) ( ( P  \  M
)  \  [ A ]  .~  )  =  [
b ]  .~  )
285277, 284sylibr 203 . . . . 5  |-  ( ph  ->  ( ( P  \  M )  \  [ A ]  .~  )  e.  ( ( P  \  M ) /.  .~  ) )
286 eleq1 2356 . . . . 5  |-  ( B  =  ( ( P 
\  M )  \  [ A ]  .~  )  ->  ( B  e.  ( ( P  \  M
) /.  .~  )  <->  ( ( P  \  M
)  \  [ A ]  .~  )  e.  ( ( P  \  M
) /.  .~  )
) )
287285, 286syl5ibr 212 . . . 4  |-  ( B  =  ( ( P 
\  M )  \  [ A ]  .~  )  ->  ( ph  ->  B  e.  ( ( P  \  M ) /.  .~  ) ) )
288147, 287jaoi 368 . . 3  |-  ( ( B  =  [ A ]  .~  \/  B  =  ( ( P  \  M )  \  [ A ]  .~  )
)  ->  ( ph  ->  B  e.  ( ( P  \  M ) /.  .~  ) ) )
289288com12 27 . 2  |-  ( ph  ->  ( ( B  =  [ A ]  .~  \/  B  =  (
( P  \  M
)  \  [ A ]  .~  ) )  ->  B  e.  ( ( P  \  M ) /.  .~  ) ) )
290131, 289impbid 183 1  |-  ( ph  ->  ( B  e.  ( ( P  \  M
) /.  .~  )  <->  ( B  =  [ A ]  .~  \/  B  =  ( ( P  \  M )  \  [ A ]  .~  )
) ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 176    \/ wo 357    /\ wa 358    \/ w3o 933    /\ w3a 934    = wceq 1632    e. wcel 1696    =/= wne 2459   E.wrex 2557   _Vcvv 2801    \ cdif 3162    i^i cin 3164   (/)c0 3468   {csn 3653   class class class wbr 4039   ` cfv 5271  (class class class)co 5874   [cec 6674   /.cqs 6675  PPointscpoints 26159  PLinescplines 26161  Ibgcibg 26210   segcseg 26233  sscsas 26265
This theorem is referenced by:  abhp  26276  abhp1  26277
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-13 1698  ax-14 1700  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-rep 4147  ax-sep 4157  ax-nul 4165  ax-pow 4204  ax-pr 4230  ax-un 4528
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-eu 2160  df-mo 2161  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ne 2461  df-nel 2462  df-ral 2561  df-rex 2562  df-reu 2563  df-rab 2565  df-v 2803  df-sbc 3005  df-csb 3095  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3469  df-if 3579  df-pw 3640  df-sn 3659  df-pr 3660  df-tp 3661  df-op 3662  df-uni 3844  df-iun 3923  df-br 4040  df-opab 4094  df-mpt 4095  df-id 4325  df-xp 4711  df-rel 4712  df-cnv 4713  df-co 4714  df-dm 4715  df-rn 4716  df-res 4717  df-ima 4718  df-iota 5235  df-fun 5273  df-fn 5274  df-f 5275  df-f1 5276  df-fo 5277  df-f1o 5278  df-fv 5279  df-ov 5877  df-oprab 5878  df-mpt2 5879  df-1st 6138  df-2nd 6139  df-riota 6320  df-er 6676  df-ec 6678  df-qs 6682  df-ig2 26164  df-li 26180  df-col 26194  df-ibg2 26212  df-seg2 26234  df-sside 26266
  Copyright terms: Public domain W3C validator