MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mplsubglemOLD Structured version   Unicode version

Theorem mplsubglemOLD 17859
Description: If  A is an ideal of sets (a nonempty collection closed under subset and binary union) of the set  D of finite bags (the primary applications being  A  =  Fin and  A  =  ~P B for some  B), then the set of all power series whose coefficient functions are supported on an element of  A is a subgroup of the set of all power series. (Contributed by Mario Carneiro, 12-Jan-2015.) Obsolete version of mplsubglem 17857 as of 16-Jul-2019. (New usage is discouraged.) (Proof modification is discouraged.)
Hypotheses
Ref Expression
mplsubglemOLD.s  |-  S  =  ( I mPwSer  R )
mplsubglemOLD.b  |-  B  =  ( Base `  S
)
mplsubglemOLD.z  |-  .0.  =  ( 0g `  R )
mplsubglemOLD.d  |-  D  =  { f  e.  ( NN0  ^m  I )  |  ( `' f
" NN )  e. 
Fin }
mplsubglemOLD.i  |-  ( ph  ->  I  e.  W )
mplsubglemOLD.0  |-  ( ph  -> 
(/)  e.  A )
mplsubgOLD.a  |-  ( (
ph  /\  ( x  e.  A  /\  y  e.  A ) )  -> 
( x  u.  y
)  e.  A )
mplsubglemOLD.y  |-  ( (
ph  /\  ( x  e.  A  /\  y  C_  x ) )  -> 
y  e.  A )
mplsubglemOLD.u  |-  ( ph  ->  U  =  { g  e.  B  |  ( `' g " ( _V  \  {  .0.  }
) )  e.  A } )
mplsubglemOLD.r  |-  ( ph  ->  R  e.  Grp )
Assertion
Ref Expression
mplsubglemOLD  |-  ( ph  ->  U  e.  (SubGrp `  S ) )
Distinct variable groups:    f, g, x, y,  .0.    A, f, g, x, y    B, f, g    D, g    f, I    ph, x, y    S, f, g, y
Allowed substitution hints:    ph( f, g)    B( x, y)    D( x, y, f)    R( x, y, f, g)    S( x)    U( x, y, f, g)    I( x, y, g)    W( x, y, f, g)

Proof of Theorem mplsubglemOLD
Dummy variables  k  u  v are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 mplsubglemOLD.u . . 3  |-  ( ph  ->  U  =  { g  e.  B  |  ( `' g " ( _V  \  {  .0.  }
) )  e.  A } )
2 ssrab2 3578 . . 3  |-  { g  e.  B  |  ( `' g " ( _V  \  {  .0.  }
) )  e.  A }  C_  B
31, 2syl6eqss 3547 . 2  |-  ( ph  ->  U  C_  B )
4 mplsubglemOLD.s . . . . 5  |-  S  =  ( I mPwSer  R )
5 mplsubglemOLD.i . . . . 5  |-  ( ph  ->  I  e.  W )
6 mplsubglemOLD.r . . . . 5  |-  ( ph  ->  R  e.  Grp )
7 mplsubglemOLD.d . . . . 5  |-  D  =  { f  e.  ( NN0  ^m  I )  |  ( `' f
" NN )  e. 
Fin }
8 mplsubglemOLD.z . . . . 5  |-  .0.  =  ( 0g `  R )
9 mplsubglemOLD.b . . . . 5  |-  B  =  ( Base `  S
)
104, 5, 6, 7, 8, 9psr0cl 17811 . . . 4  |-  ( ph  ->  ( D  X.  {  .0.  } )  e.  B
)
11 eqid 2460 . . . . . . . . 9  |-  ( Base `  R )  =  (
Base `  R )
1211, 8grpidcl 15872 . . . . . . . 8  |-  ( R  e.  Grp  ->  .0.  e.  ( Base `  R
) )
13 fconst6g 5765 . . . . . . . 8  |-  (  .0. 
e.  ( Base `  R
)  ->  ( D  X.  {  .0.  } ) : D --> ( Base `  R ) )
146, 12, 133syl 20 . . . . . . 7  |-  ( ph  ->  ( D  X.  {  .0.  } ) : D --> ( Base `  R )
)
15 eldifi 3619 . . . . . . . . 9  |-  ( u  e.  ( D  \  (/) )  ->  u  e.  D )
16 fvex 5867 . . . . . . . . . . 11  |-  ( 0g
`  R )  e. 
_V
178, 16eqeltri 2544 . . . . . . . . . 10  |-  .0.  e.  _V
1817fvconst2 6107 . . . . . . . . 9  |-  ( u  e.  D  ->  (
( D  X.  {  .0.  } ) `  u
)  =  .0.  )
1915, 18syl 16 . . . . . . . 8  |-  ( u  e.  ( D  \  (/) )  ->  ( ( D  X.  {  .0.  }
) `  u )  =  .0.  )
2019adantl 466 . . . . . . 7  |-  ( (
ph  /\  u  e.  ( D  \  (/) ) )  ->  ( ( D  X.  {  .0.  }
) `  u )  =  .0.  )
2114, 20suppssOLD 6005 . . . . . 6  |-  ( ph  ->  ( `' ( D  X.  {  .0.  }
) " ( _V 
\  {  .0.  }
) )  C_  (/) )
22 ss0 3809 . . . . . 6  |-  ( ( `' ( D  X.  {  .0.  } ) "
( _V  \  {  .0.  } ) )  C_  (/) 
->  ( `' ( D  X.  {  .0.  }
) " ( _V 
\  {  .0.  }
) )  =  (/) )
2321, 22syl 16 . . . . 5  |-  ( ph  ->  ( `' ( D  X.  {  .0.  }
) " ( _V 
\  {  .0.  }
) )  =  (/) )
24 mplsubglemOLD.0 . . . . 5  |-  ( ph  -> 
(/)  e.  A )
2523, 24eqeltrd 2548 . . . 4  |-  ( ph  ->  ( `' ( D  X.  {  .0.  }
) " ( _V 
\  {  .0.  }
) )  e.  A
)
261eleq2d 2530 . . . . 5  |-  ( ph  ->  ( ( D  X.  {  .0.  } )  e.  U  <->  ( D  X.  {  .0.  } )  e. 
{ g  e.  B  |  ( `' g
" ( _V  \  {  .0.  } ) )  e.  A } ) )
27 cnveq 5167 . . . . . . . 8  |-  ( g  =  ( D  X.  {  .0.  } )  ->  `' g  =  `' ( D  X.  {  .0.  } ) )
2827imaeq1d 5327 . . . . . . 7  |-  ( g  =  ( D  X.  {  .0.  } )  -> 
( `' g "
( _V  \  {  .0.  } ) )  =  ( `' ( D  X.  {  .0.  }
) " ( _V 
\  {  .0.  }
) ) )
2928eleq1d 2529 . . . . . 6  |-  ( g  =  ( D  X.  {  .0.  } )  -> 
( ( `' g
" ( _V  \  {  .0.  } ) )  e.  A  <->  ( `' ( D  X.  {  .0.  } ) " ( _V 
\  {  .0.  }
) )  e.  A
) )
3029elrab 3254 . . . . 5  |-  ( ( D  X.  {  .0.  } )  e.  { g  e.  B  |  ( `' g " ( _V  \  {  .0.  }
) )  e.  A } 
<->  ( ( D  X.  {  .0.  } )  e.  B  /\  ( `' ( D  X.  {  .0.  } ) " ( _V  \  {  .0.  }
) )  e.  A
) )
3126, 30syl6bb 261 . . . 4  |-  ( ph  ->  ( ( D  X.  {  .0.  } )  e.  U  <->  ( ( D  X.  {  .0.  }
)  e.  B  /\  ( `' ( D  X.  {  .0.  } ) "
( _V  \  {  .0.  } ) )  e.  A ) ) )
3210, 25, 31mpbir2and 915 . . 3  |-  ( ph  ->  ( D  X.  {  .0.  } )  e.  U
)
33 ne0i 3784 . . 3  |-  ( ( D  X.  {  .0.  } )  e.  U  ->  U  =/=  (/) )
3432, 33syl 16 . 2  |-  ( ph  ->  U  =/=  (/) )
35 eqid 2460 . . . . . . 7  |-  ( +g  `  S )  =  ( +g  `  S )
366ad2antrr 725 . . . . . . 7  |-  ( ( ( ph  /\  u  e.  U )  /\  v  e.  U )  ->  R  e.  Grp )
371eleq2d 2530 . . . . . . . . . . 11  |-  ( ph  ->  ( u  e.  U  <->  u  e.  { g  e.  B  |  ( `' g " ( _V 
\  {  .0.  }
) )  e.  A } ) )
38 cnveq 5167 . . . . . . . . . . . . . 14  |-  ( g  =  u  ->  `' g  =  `' u
)
3938imaeq1d 5327 . . . . . . . . . . . . 13  |-  ( g  =  u  ->  ( `' g " ( _V  \  {  .0.  }
) )  =  ( `' u " ( _V 
\  {  .0.  }
) ) )
4039eleq1d 2529 . . . . . . . . . . . 12  |-  ( g  =  u  ->  (
( `' g "
( _V  \  {  .0.  } ) )  e.  A  <->  ( `' u " ( _V  \  {  .0.  } ) )  e.  A ) )
4140elrab 3254 . . . . . . . . . . 11  |-  ( u  e.  { g  e.  B  |  ( `' g " ( _V 
\  {  .0.  }
) )  e.  A } 
<->  ( u  e.  B  /\  ( `' u "
( _V  \  {  .0.  } ) )  e.  A ) )
4237, 41syl6bb 261 . . . . . . . . . 10  |-  ( ph  ->  ( u  e.  U  <->  ( u  e.  B  /\  ( `' u " ( _V 
\  {  .0.  }
) )  e.  A
) ) )
4342biimpa 484 . . . . . . . . 9  |-  ( (
ph  /\  u  e.  U )  ->  (
u  e.  B  /\  ( `' u " ( _V 
\  {  .0.  }
) )  e.  A
) )
4443simpld 459 . . . . . . . 8  |-  ( (
ph  /\  u  e.  U )  ->  u  e.  B )
4544adantr 465 . . . . . . 7  |-  ( ( ( ph  /\  u  e.  U )  /\  v  e.  U )  ->  u  e.  B )
461adantr 465 . . . . . . . . . . 11  |-  ( (
ph  /\  u  e.  U )  ->  U  =  { g  e.  B  |  ( `' g
" ( _V  \  {  .0.  } ) )  e.  A } )
4746eleq2d 2530 . . . . . . . . . 10  |-  ( (
ph  /\  u  e.  U )  ->  (
v  e.  U  <->  v  e.  { g  e.  B  | 
( `' g "
( _V  \  {  .0.  } ) )  e.  A } ) )
48 cnveq 5167 . . . . . . . . . . . . 13  |-  ( g  =  v  ->  `' g  =  `' v
)
4948imaeq1d 5327 . . . . . . . . . . . 12  |-  ( g  =  v  ->  ( `' g " ( _V  \  {  .0.  }
) )  =  ( `' v " ( _V  \  {  .0.  }
) ) )
5049eleq1d 2529 . . . . . . . . . . 11  |-  ( g  =  v  ->  (
( `' g "
( _V  \  {  .0.  } ) )  e.  A  <->  ( `' v
" ( _V  \  {  .0.  } ) )  e.  A ) )
5150elrab 3254 . . . . . . . . . 10  |-  ( v  e.  { g  e.  B  |  ( `' g " ( _V 
\  {  .0.  }
) )  e.  A } 
<->  ( v  e.  B  /\  ( `' v "
( _V  \  {  .0.  } ) )  e.  A ) )
5247, 51syl6bb 261 . . . . . . . . 9  |-  ( (
ph  /\  u  e.  U )  ->  (
v  e.  U  <->  ( v  e.  B  /\  ( `' v " ( _V  \  {  .0.  }
) )  e.  A
) ) )
5352biimpa 484 . . . . . . . 8  |-  ( ( ( ph  /\  u  e.  U )  /\  v  e.  U )  ->  (
v  e.  B  /\  ( `' v " ( _V  \  {  .0.  }
) )  e.  A
) )
5453simpld 459 . . . . . . 7  |-  ( ( ( ph  /\  u  e.  U )  /\  v  e.  U )  ->  v  e.  B )
554, 9, 35, 36, 45, 54psraddcl 17800 . . . . . 6  |-  ( ( ( ph  /\  u  e.  U )  /\  v  e.  U )  ->  (
u ( +g  `  S
) v )  e.  B )
5643simprd 463 . . . . . . . . . 10  |-  ( (
ph  /\  u  e.  U )  ->  ( `' u " ( _V 
\  {  .0.  }
) )  e.  A
)
5756adantr 465 . . . . . . . . 9  |-  ( ( ( ph  /\  u  e.  U )  /\  v  e.  U )  ->  ( `' u " ( _V 
\  {  .0.  }
) )  e.  A
)
5853simprd 463 . . . . . . . . 9  |-  ( ( ( ph  /\  u  e.  U )  /\  v  e.  U )  ->  ( `' v " ( _V  \  {  .0.  }
) )  e.  A
)
59 mplsubgOLD.a . . . . . . . . . . 11  |-  ( (
ph  /\  ( x  e.  A  /\  y  e.  A ) )  -> 
( x  u.  y
)  e.  A )
6059ralrimivva 2878 . . . . . . . . . 10  |-  ( ph  ->  A. x  e.  A  A. y  e.  A  ( x  u.  y
)  e.  A )
6160ad2antrr 725 . . . . . . . . 9  |-  ( ( ( ph  /\  u  e.  U )  /\  v  e.  U )  ->  A. x  e.  A  A. y  e.  A  ( x  u.  y )  e.  A
)
62 uneq1 3644 . . . . . . . . . . 11  |-  ( x  =  ( `' u " ( _V  \  {  .0.  } ) )  -> 
( x  u.  y
)  =  ( ( `' u " ( _V 
\  {  .0.  }
) )  u.  y
) )
6362eleq1d 2529 . . . . . . . . . 10  |-  ( x  =  ( `' u " ( _V  \  {  .0.  } ) )  -> 
( ( x  u.  y )  e.  A  <->  ( ( `' u "
( _V  \  {  .0.  } ) )  u.  y )  e.  A
) )
64 uneq2 3645 . . . . . . . . . . 11  |-  ( y  =  ( `' v
" ( _V  \  {  .0.  } ) )  ->  ( ( `' u " ( _V 
\  {  .0.  }
) )  u.  y
)  =  ( ( `' u " ( _V 
\  {  .0.  }
) )  u.  ( `' v " ( _V  \  {  .0.  }
) ) ) )
6564eleq1d 2529 . . . . . . . . . 10  |-  ( y  =  ( `' v
" ( _V  \  {  .0.  } ) )  ->  ( ( ( `' u " ( _V 
\  {  .0.  }
) )  u.  y
)  e.  A  <->  ( ( `' u " ( _V 
\  {  .0.  }
) )  u.  ( `' v " ( _V  \  {  .0.  }
) ) )  e.  A ) )
6663, 65rspc2va 3217 . . . . . . . . 9  |-  ( ( ( ( `' u " ( _V  \  {  .0.  } ) )  e.  A  /\  ( `' v " ( _V 
\  {  .0.  }
) )  e.  A
)  /\  A. x  e.  A  A. y  e.  A  ( x  u.  y )  e.  A
)  ->  ( ( `' u " ( _V 
\  {  .0.  }
) )  u.  ( `' v " ( _V  \  {  .0.  }
) ) )  e.  A )
6757, 58, 61, 66syl21anc 1222 . . . . . . . 8  |-  ( ( ( ph  /\  u  e.  U )  /\  v  e.  U )  ->  (
( `' u "
( _V  \  {  .0.  } ) )  u.  ( `' v "
( _V  \  {  .0.  } ) ) )  e.  A )
684, 11, 7, 9, 55psrelbas 17796 . . . . . . . . 9  |-  ( ( ( ph  /\  u  e.  U )  /\  v  e.  U )  ->  (
u ( +g  `  S
) v ) : D --> ( Base `  R
) )
69 eqid 2460 . . . . . . . . . . . . 13  |-  ( +g  `  R )  =  ( +g  `  R )
704, 9, 69, 35, 45, 54psradd 17799 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  u  e.  U )  /\  v  e.  U )  ->  (
u ( +g  `  S
) v )  =  ( u  oF ( +g  `  R
) v ) )
7170fveq1d 5859 . . . . . . . . . . 11  |-  ( ( ( ph  /\  u  e.  U )  /\  v  e.  U )  ->  (
( u ( +g  `  S ) v ) `
 k )  =  ( ( u  oF ( +g  `  R
) v ) `  k ) )
7271adantr 465 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  u  e.  U )  /\  v  e.  U
)  /\  k  e.  ( D  \  (
( `' u "
( _V  \  {  .0.  } ) )  u.  ( `' v "
( _V  \  {  .0.  } ) ) ) ) )  ->  (
( u ( +g  `  S ) v ) `
 k )  =  ( ( u  oF ( +g  `  R
) v ) `  k ) )
73 eldifi 3619 . . . . . . . . . . 11  |-  ( k  e.  ( D  \ 
( ( `' u " ( _V  \  {  .0.  } ) )  u.  ( `' v "
( _V  \  {  .0.  } ) ) ) )  ->  k  e.  D )
744, 11, 7, 9, 44psrelbas 17796 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  u  e.  U )  ->  u : D --> ( Base `  R
) )
7574adantr 465 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  u  e.  U )  /\  v  e.  U )  ->  u : D --> ( Base `  R
) )
76 ffn 5722 . . . . . . . . . . . . 13  |-  ( u : D --> ( Base `  R )  ->  u  Fn  D )
7775, 76syl 16 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  u  e.  U )  /\  v  e.  U )  ->  u  Fn  D )
784, 11, 7, 9, 54psrelbas 17796 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  u  e.  U )  /\  v  e.  U )  ->  v : D --> ( Base `  R
) )
79 ffn 5722 . . . . . . . . . . . . 13  |-  ( v : D --> ( Base `  R )  ->  v  Fn  D )
8078, 79syl 16 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  u  e.  U )  /\  v  e.  U )  ->  v  Fn  D )
81 ovex 6300 . . . . . . . . . . . . . . 15  |-  ( NN0 
^m  I )  e. 
_V
8281rabex 4591 . . . . . . . . . . . . . 14  |-  { f  e.  ( NN0  ^m  I )  |  ( `' f " NN )  e.  Fin }  e.  _V
837, 82eqeltri 2544 . . . . . . . . . . . . 13  |-  D  e. 
_V
8483a1i 11 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  u  e.  U )  /\  v  e.  U )  ->  D  e.  _V )
85 inidm 3700 . . . . . . . . . . . 12  |-  ( D  i^i  D )  =  D
86 eqidd 2461 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  u  e.  U )  /\  v  e.  U
)  /\  k  e.  D )  ->  (
u `  k )  =  ( u `  k ) )
87 eqidd 2461 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  u  e.  U )  /\  v  e.  U
)  /\  k  e.  D )  ->  (
v `  k )  =  ( v `  k ) )
8877, 80, 84, 84, 85, 86, 87ofval 6524 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  u  e.  U )  /\  v  e.  U
)  /\  k  e.  D )  ->  (
( u  oF ( +g  `  R
) v ) `  k )  =  ( ( u `  k
) ( +g  `  R
) ( v `  k ) ) )
8973, 88sylan2 474 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  u  e.  U )  /\  v  e.  U
)  /\  k  e.  ( D  \  (
( `' u "
( _V  \  {  .0.  } ) )  u.  ( `' v "
( _V  \  {  .0.  } ) ) ) ) )  ->  (
( u  oF ( +g  `  R
) v ) `  k )  =  ( ( u `  k
) ( +g  `  R
) ( v `  k ) ) )
90 ssun1 3660 . . . . . . . . . . . . . . 15  |-  ( `' u " ( _V 
\  {  .0.  }
) )  C_  (
( `' u "
( _V  \  {  .0.  } ) )  u.  ( `' v "
( _V  \  {  .0.  } ) ) )
91 sscon 3631 . . . . . . . . . . . . . . 15  |-  ( ( `' u " ( _V 
\  {  .0.  }
) )  C_  (
( `' u "
( _V  \  {  .0.  } ) )  u.  ( `' v "
( _V  \  {  .0.  } ) ) )  ->  ( D  \ 
( ( `' u " ( _V  \  {  .0.  } ) )  u.  ( `' v "
( _V  \  {  .0.  } ) ) ) )  C_  ( D  \  ( `' u "
( _V  \  {  .0.  } ) ) ) )
9290, 91ax-mp 5 . . . . . . . . . . . . . 14  |-  ( D 
\  ( ( `' u " ( _V 
\  {  .0.  }
) )  u.  ( `' v " ( _V  \  {  .0.  }
) ) ) ) 
C_  ( D  \ 
( `' u "
( _V  \  {  .0.  } ) ) )
9392sseli 3493 . . . . . . . . . . . . 13  |-  ( k  e.  ( D  \ 
( ( `' u " ( _V  \  {  .0.  } ) )  u.  ( `' v "
( _V  \  {  .0.  } ) ) ) )  ->  k  e.  ( D  \  ( `' u " ( _V 
\  {  .0.  }
) ) ) )
94 ssid 3516 . . . . . . . . . . . . . . . 16  |-  ( `' u " ( _V 
\  {  .0.  }
) )  C_  ( `' u " ( _V 
\  {  .0.  }
) )
9594a1i 11 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  u  e.  U )  ->  ( `' u " ( _V 
\  {  .0.  }
) )  C_  ( `' u " ( _V 
\  {  .0.  }
) ) )
9674, 95suppssrOLD 6006 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  u  e.  U )  /\  k  e.  ( D  \  ( `' u " ( _V 
\  {  .0.  }
) ) ) )  ->  ( u `  k )  =  .0.  )
9796adantlr 714 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  u  e.  U )  /\  v  e.  U
)  /\  k  e.  ( D  \  ( `' u " ( _V 
\  {  .0.  }
) ) ) )  ->  ( u `  k )  =  .0.  )
9893, 97sylan2 474 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  u  e.  U )  /\  v  e.  U
)  /\  k  e.  ( D  \  (
( `' u "
( _V  \  {  .0.  } ) )  u.  ( `' v "
( _V  \  {  .0.  } ) ) ) ) )  ->  (
u `  k )  =  .0.  )
99 ssun2 3661 . . . . . . . . . . . . . . 15  |-  ( `' v " ( _V 
\  {  .0.  }
) )  C_  (
( `' u "
( _V  \  {  .0.  } ) )  u.  ( `' v "
( _V  \  {  .0.  } ) ) )
100 sscon 3631 . . . . . . . . . . . . . . 15  |-  ( ( `' v " ( _V  \  {  .0.  }
) )  C_  (
( `' u "
( _V  \  {  .0.  } ) )  u.  ( `' v "
( _V  \  {  .0.  } ) ) )  ->  ( D  \ 
( ( `' u " ( _V  \  {  .0.  } ) )  u.  ( `' v "
( _V  \  {  .0.  } ) ) ) )  C_  ( D  \  ( `' v "
( _V  \  {  .0.  } ) ) ) )
10199, 100ax-mp 5 . . . . . . . . . . . . . 14  |-  ( D 
\  ( ( `' u " ( _V 
\  {  .0.  }
) )  u.  ( `' v " ( _V  \  {  .0.  }
) ) ) ) 
C_  ( D  \ 
( `' v "
( _V  \  {  .0.  } ) ) )
102101sseli 3493 . . . . . . . . . . . . 13  |-  ( k  e.  ( D  \ 
( ( `' u " ( _V  \  {  .0.  } ) )  u.  ( `' v "
( _V  \  {  .0.  } ) ) ) )  ->  k  e.  ( D  \  ( `' v " ( _V  \  {  .0.  }
) ) ) )
103 ssid 3516 . . . . . . . . . . . . . . 15  |-  ( `' v " ( _V 
\  {  .0.  }
) )  C_  ( `' v " ( _V  \  {  .0.  }
) )
104103a1i 11 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  u  e.  U )  /\  v  e.  U )  ->  ( `' v " ( _V  \  {  .0.  }
) )  C_  ( `' v " ( _V  \  {  .0.  }
) ) )
10578, 104suppssrOLD 6006 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  u  e.  U )  /\  v  e.  U
)  /\  k  e.  ( D  \  ( `' v " ( _V  \  {  .0.  }
) ) ) )  ->  ( v `  k )  =  .0.  )
106102, 105sylan2 474 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  u  e.  U )  /\  v  e.  U
)  /\  k  e.  ( D  \  (
( `' u "
( _V  \  {  .0.  } ) )  u.  ( `' v "
( _V  \  {  .0.  } ) ) ) ) )  ->  (
v `  k )  =  .0.  )
10798, 106oveq12d 6293 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  u  e.  U )  /\  v  e.  U
)  /\  k  e.  ( D  \  (
( `' u "
( _V  \  {  .0.  } ) )  u.  ( `' v "
( _V  \  {  .0.  } ) ) ) ) )  ->  (
( u `  k
) ( +g  `  R
) ( v `  k ) )  =  (  .0.  ( +g  `  R )  .0.  )
)
10811, 69, 8grplid 15874 . . . . . . . . . . . . . 14  |-  ( ( R  e.  Grp  /\  .0.  e.  ( Base `  R
) )  ->  (  .0.  ( +g  `  R
)  .0.  )  =  .0.  )
10912, 108mpdan 668 . . . . . . . . . . . . 13  |-  ( R  e.  Grp  ->  (  .0.  ( +g  `  R
)  .0.  )  =  .0.  )
11036, 109syl 16 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  u  e.  U )  /\  v  e.  U )  ->  (  .0.  ( +g  `  R
)  .0.  )  =  .0.  )
111110adantr 465 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  u  e.  U )  /\  v  e.  U
)  /\  k  e.  ( D  \  (
( `' u "
( _V  \  {  .0.  } ) )  u.  ( `' v "
( _V  \  {  .0.  } ) ) ) ) )  ->  (  .0.  ( +g  `  R
)  .0.  )  =  .0.  )
112107, 111eqtrd 2501 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  u  e.  U )  /\  v  e.  U
)  /\  k  e.  ( D  \  (
( `' u "
( _V  \  {  .0.  } ) )  u.  ( `' v "
( _V  \  {  .0.  } ) ) ) ) )  ->  (
( u `  k
) ( +g  `  R
) ( v `  k ) )  =  .0.  )
11372, 89, 1123eqtrd 2505 . . . . . . . . 9  |-  ( ( ( ( ph  /\  u  e.  U )  /\  v  e.  U
)  /\  k  e.  ( D  \  (
( `' u "
( _V  \  {  .0.  } ) )  u.  ( `' v "
( _V  \  {  .0.  } ) ) ) ) )  ->  (
( u ( +g  `  S ) v ) `
 k )  =  .0.  )
11468, 113suppssOLD 6005 . . . . . . . 8  |-  ( ( ( ph  /\  u  e.  U )  /\  v  e.  U )  ->  ( `' ( u ( +g  `  S ) v ) " ( _V  \  {  .0.  }
) )  C_  (
( `' u "
( _V  \  {  .0.  } ) )  u.  ( `' v "
( _V  \  {  .0.  } ) ) ) )
11567, 114ssexd 4587 . . . . . . 7  |-  ( ( ( ph  /\  u  e.  U )  /\  v  e.  U )  ->  ( `' ( u ( +g  `  S ) v ) " ( _V  \  {  .0.  }
) )  e.  _V )
116 mplsubglemOLD.y . . . . . . . . . . . 12  |-  ( (
ph  /\  ( x  e.  A  /\  y  C_  x ) )  -> 
y  e.  A )
117116expr 615 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  A )  ->  (
y  C_  x  ->  y  e.  A ) )
118117alrimiv 1690 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  A )  ->  A. y
( y  C_  x  ->  y  e.  A ) )
119118ralrimiva 2871 . . . . . . . . 9  |-  ( ph  ->  A. x  e.  A  A. y ( y  C_  x  ->  y  e.  A
) )
120119ad2antrr 725 . . . . . . . 8  |-  ( ( ( ph  /\  u  e.  U )  /\  v  e.  U )  ->  A. x  e.  A  A. y
( y  C_  x  ->  y  e.  A ) )
121 sseq2 3519 . . . . . . . . . . 11  |-  ( x  =  ( ( `' u " ( _V 
\  {  .0.  }
) )  u.  ( `' v " ( _V  \  {  .0.  }
) ) )  -> 
( y  C_  x  <->  y 
C_  ( ( `' u " ( _V 
\  {  .0.  }
) )  u.  ( `' v " ( _V  \  {  .0.  }
) ) ) ) )
122121imbi1d 317 . . . . . . . . . 10  |-  ( x  =  ( ( `' u " ( _V 
\  {  .0.  }
) )  u.  ( `' v " ( _V  \  {  .0.  }
) ) )  -> 
( ( y  C_  x  ->  y  e.  A
)  <->  ( y  C_  ( ( `' u " ( _V  \  {  .0.  } ) )  u.  ( `' v "
( _V  \  {  .0.  } ) ) )  ->  y  e.  A
) ) )
123122albidv 1684 . . . . . . . . 9  |-  ( x  =  ( ( `' u " ( _V 
\  {  .0.  }
) )  u.  ( `' v " ( _V  \  {  .0.  }
) ) )  -> 
( A. y ( y  C_  x  ->  y  e.  A )  <->  A. y
( y  C_  (
( `' u "
( _V  \  {  .0.  } ) )  u.  ( `' v "
( _V  \  {  .0.  } ) ) )  ->  y  e.  A
) ) )
124123rspcv 3203 . . . . . . . 8  |-  ( ( ( `' u "
( _V  \  {  .0.  } ) )  u.  ( `' v "
( _V  \  {  .0.  } ) ) )  e.  A  ->  ( A. x  e.  A  A. y ( y  C_  x  ->  y  e.  A
)  ->  A. y
( y  C_  (
( `' u "
( _V  \  {  .0.  } ) )  u.  ( `' v "
( _V  \  {  .0.  } ) ) )  ->  y  e.  A
) ) )
12567, 120, 124sylc 60 . . . . . . 7  |-  ( ( ( ph  /\  u  e.  U )  /\  v  e.  U )  ->  A. y
( y  C_  (
( `' u "
( _V  \  {  .0.  } ) )  u.  ( `' v "
( _V  \  {  .0.  } ) ) )  ->  y  e.  A
) )
126 sseq1 3518 . . . . . . . . 9  |-  ( y  =  ( `' ( u ( +g  `  S
) v ) "
( _V  \  {  .0.  } ) )  -> 
( y  C_  (
( `' u "
( _V  \  {  .0.  } ) )  u.  ( `' v "
( _V  \  {  .0.  } ) ) )  <-> 
( `' ( u ( +g  `  S
) v ) "
( _V  \  {  .0.  } ) )  C_  ( ( `' u " ( _V  \  {  .0.  } ) )  u.  ( `' v "
( _V  \  {  .0.  } ) ) ) ) )
127 eleq1 2532 . . . . . . . . 9  |-  ( y  =  ( `' ( u ( +g  `  S
) v ) "
( _V  \  {  .0.  } ) )  -> 
( y  e.  A  <->  ( `' ( u ( +g  `  S ) v ) " ( _V  \  {  .0.  }
) )  e.  A
) )
128126, 127imbi12d 320 . . . . . . . 8  |-  ( y  =  ( `' ( u ( +g  `  S
) v ) "
( _V  \  {  .0.  } ) )  -> 
( ( y  C_  ( ( `' u " ( _V  \  {  .0.  } ) )  u.  ( `' v "
( _V  \  {  .0.  } ) ) )  ->  y  e.  A
)  <->  ( ( `' ( u ( +g  `  S ) v )
" ( _V  \  {  .0.  } ) ) 
C_  ( ( `' u " ( _V 
\  {  .0.  }
) )  u.  ( `' v " ( _V  \  {  .0.  }
) ) )  -> 
( `' ( u ( +g  `  S
) v ) "
( _V  \  {  .0.  } ) )  e.  A ) ) )
129128spcgv 3191 . . . . . . 7  |-  ( ( `' ( u ( +g  `  S ) v ) " ( _V  \  {  .0.  }
) )  e.  _V  ->  ( A. y ( y  C_  ( ( `' u " ( _V 
\  {  .0.  }
) )  u.  ( `' v " ( _V  \  {  .0.  }
) ) )  -> 
y  e.  A )  ->  ( ( `' ( u ( +g  `  S ) v )
" ( _V  \  {  .0.  } ) ) 
C_  ( ( `' u " ( _V 
\  {  .0.  }
) )  u.  ( `' v " ( _V  \  {  .0.  }
) ) )  -> 
( `' ( u ( +g  `  S
) v ) "
( _V  \  {  .0.  } ) )  e.  A ) ) )
130115, 125, 114, 129syl3c 61 . . . . . 6  |-  ( ( ( ph  /\  u  e.  U )  /\  v  e.  U )  ->  ( `' ( u ( +g  `  S ) v ) " ( _V  \  {  .0.  }
) )  e.  A
)
1311ad2antrr 725 . . . . . . . 8  |-  ( ( ( ph  /\  u  e.  U )  /\  v  e.  U )  ->  U  =  { g  e.  B  |  ( `' g
" ( _V  \  {  .0.  } ) )  e.  A } )
132131eleq2d 2530 . . . . . . 7  |-  ( ( ( ph  /\  u  e.  U )  /\  v  e.  U )  ->  (
( u ( +g  `  S ) v )  e.  U  <->  ( u
( +g  `  S ) v )  e.  {
g  e.  B  | 
( `' g "
( _V  \  {  .0.  } ) )  e.  A } ) )
133 cnveq 5167 . . . . . . . . . 10  |-  ( g  =  ( u ( +g  `  S ) v )  ->  `' g  =  `' (
u ( +g  `  S
) v ) )
134133imaeq1d 5327 . . . . . . . . 9  |-  ( g  =  ( u ( +g  `  S ) v )  ->  ( `' g " ( _V  \  {  .0.  }
) )  =  ( `' ( u ( +g  `  S ) v ) " ( _V  \  {  .0.  }
) ) )
135134eleq1d 2529 . . . . . . . 8  |-  ( g  =  ( u ( +g  `  S ) v )  ->  (
( `' g "
( _V  \  {  .0.  } ) )  e.  A  <->  ( `' ( u ( +g  `  S
) v ) "
( _V  \  {  .0.  } ) )  e.  A ) )
136135elrab 3254 . . . . . . 7  |-  ( ( u ( +g  `  S
) v )  e. 
{ g  e.  B  |  ( `' g
" ( _V  \  {  .0.  } ) )  e.  A }  <->  ( (
u ( +g  `  S
) v )  e.  B  /\  ( `' ( u ( +g  `  S ) v )
" ( _V  \  {  .0.  } ) )  e.  A ) )
137132, 136syl6bb 261 . . . . . 6  |-  ( ( ( ph  /\  u  e.  U )  /\  v  e.  U )  ->  (
( u ( +g  `  S ) v )  e.  U  <->  ( (
u ( +g  `  S
) v )  e.  B  /\  ( `' ( u ( +g  `  S ) v )
" ( _V  \  {  .0.  } ) )  e.  A ) ) )
13855, 130, 137mpbir2and 915 . . . . 5  |-  ( ( ( ph  /\  u  e.  U )  /\  v  e.  U )  ->  (
u ( +g  `  S
) v )  e.  U )
139138ralrimiva 2871 . . . 4  |-  ( (
ph  /\  u  e.  U )  ->  A. v  e.  U  ( u
( +g  `  S ) v )  e.  U
)
1404, 5, 6psrgrp 17815 . . . . . . 7  |-  ( ph  ->  S  e.  Grp )
141 eqid 2460 . . . . . . . 8  |-  ( invg `  S )  =  ( invg `  S )
1429, 141grpinvcl 15889 . . . . . . 7  |-  ( ( S  e.  Grp  /\  u  e.  B )  ->  ( ( invg `  S ) `  u
)  e.  B )
143140, 142sylan 471 . . . . . 6  |-  ( (
ph  /\  u  e.  B )  ->  (
( invg `  S ) `  u
)  e.  B )
14444, 143syldan 470 . . . . 5  |-  ( (
ph  /\  u  e.  U )  ->  (
( invg `  S ) `  u
)  e.  B )
1454, 11, 7, 9, 144psrelbas 17796 . . . . . . . 8  |-  ( (
ph  /\  u  e.  U )  ->  (
( invg `  S ) `  u
) : D --> ( Base `  R ) )
1465adantr 465 . . . . . . . . . . . 12  |-  ( (
ph  /\  u  e.  U )  ->  I  e.  W )
1476adantr 465 . . . . . . . . . . . 12  |-  ( (
ph  /\  u  e.  U )  ->  R  e.  Grp )
148 eqid 2460 . . . . . . . . . . . 12  |-  ( invg `  R )  =  ( invg `  R )
1494, 146, 147, 7, 148, 9, 141, 44psrneg 17817 . . . . . . . . . . 11  |-  ( (
ph  /\  u  e.  U )  ->  (
( invg `  S ) `  u
)  =  ( ( invg `  R
)  o.  u ) )
150149adantr 465 . . . . . . . . . 10  |-  ( ( ( ph  /\  u  e.  U )  /\  k  e.  ( D  \  ( `' u " ( _V 
\  {  .0.  }
) ) ) )  ->  ( ( invg `  S ) `
 u )  =  ( ( invg `  R )  o.  u
) )
151150fveq1d 5859 . . . . . . . . 9  |-  ( ( ( ph  /\  u  e.  U )  /\  k  e.  ( D  \  ( `' u " ( _V 
\  {  .0.  }
) ) ) )  ->  ( ( ( invg `  S
) `  u ) `  k )  =  ( ( ( invg `  R )  o.  u
) `  k )
)
152 eldifi 3619 . . . . . . . . . 10  |-  ( k  e.  ( D  \ 
( `' u "
( _V  \  {  .0.  } ) ) )  ->  k  e.  D
)
153 fvco3 5935 . . . . . . . . . 10  |-  ( ( u : D --> ( Base `  R )  /\  k  e.  D )  ->  (
( ( invg `  R )  o.  u
) `  k )  =  ( ( invg `  R ) `
 ( u `  k ) ) )
15474, 152, 153syl2an 477 . . . . . . . . 9  |-  ( ( ( ph  /\  u  e.  U )  /\  k  e.  ( D  \  ( `' u " ( _V 
\  {  .0.  }
) ) ) )  ->  ( ( ( invg `  R
)  o.  u ) `
 k )  =  ( ( invg `  R ) `  (
u `  k )
) )
15596fveq2d 5861 . . . . . . . . . 10  |-  ( ( ( ph  /\  u  e.  U )  /\  k  e.  ( D  \  ( `' u " ( _V 
\  {  .0.  }
) ) ) )  ->  ( ( invg `  R ) `
 ( u `  k ) )  =  ( ( invg `  R ) `  .0.  ) )
1568, 148grpinvid 15895 . . . . . . . . . . . 12  |-  ( R  e.  Grp  ->  (
( invg `  R ) `  .0.  )  =  .0.  )
157147, 156syl 16 . . . . . . . . . . 11  |-  ( (
ph  /\  u  e.  U )  ->  (
( invg `  R ) `  .0.  )  =  .0.  )
158157adantr 465 . . . . . . . . . 10  |-  ( ( ( ph  /\  u  e.  U )  /\  k  e.  ( D  \  ( `' u " ( _V 
\  {  .0.  }
) ) ) )  ->  ( ( invg `  R ) `
 .0.  )  =  .0.  )
159155, 158eqtrd 2501 . . . . . . . . 9  |-  ( ( ( ph  /\  u  e.  U )  /\  k  e.  ( D  \  ( `' u " ( _V 
\  {  .0.  }
) ) ) )  ->  ( ( invg `  R ) `
 ( u `  k ) )  =  .0.  )
160151, 154, 1593eqtrd 2505 . . . . . . . 8  |-  ( ( ( ph  /\  u  e.  U )  /\  k  e.  ( D  \  ( `' u " ( _V 
\  {  .0.  }
) ) ) )  ->  ( ( ( invg `  S
) `  u ) `  k )  =  .0.  )
161145, 160suppssOLD 6005 . . . . . . 7  |-  ( (
ph  /\  u  e.  U )  ->  ( `' ( ( invg `  S ) `
 u ) "
( _V  \  {  .0.  } ) )  C_  ( `' u " ( _V 
\  {  .0.  }
) ) )
16256, 161ssexd 4587 . . . . . 6  |-  ( (
ph  /\  u  e.  U )  ->  ( `' ( ( invg `  S ) `
 u ) "
( _V  \  {  .0.  } ) )  e. 
_V )
163119adantr 465 . . . . . . 7  |-  ( (
ph  /\  u  e.  U )  ->  A. x  e.  A  A. y
( y  C_  x  ->  y  e.  A ) )
164 sseq2 3519 . . . . . . . . . 10  |-  ( x  =  ( `' u " ( _V  \  {  .0.  } ) )  -> 
( y  C_  x  <->  y 
C_  ( `' u " ( _V  \  {  .0.  } ) ) ) )
165164imbi1d 317 . . . . . . . . 9  |-  ( x  =  ( `' u " ( _V  \  {  .0.  } ) )  -> 
( ( y  C_  x  ->  y  e.  A
)  <->  ( y  C_  ( `' u " ( _V 
\  {  .0.  }
) )  ->  y  e.  A ) ) )
166165albidv 1684 . . . . . . . 8  |-  ( x  =  ( `' u " ( _V  \  {  .0.  } ) )  -> 
( A. y ( y  C_  x  ->  y  e.  A )  <->  A. y
( y  C_  ( `' u " ( _V 
\  {  .0.  }
) )  ->  y  e.  A ) ) )
167166rspcv 3203 . . . . . . 7  |-  ( ( `' u " ( _V 
\  {  .0.  }
) )  e.  A  ->  ( A. x  e.  A  A. y ( y  C_  x  ->  y  e.  A )  ->  A. y ( y  C_  ( `' u " ( _V 
\  {  .0.  }
) )  ->  y  e.  A ) ) )
16856, 163, 167sylc 60 . . . . . 6  |-  ( (
ph  /\  u  e.  U )  ->  A. y
( y  C_  ( `' u " ( _V 
\  {  .0.  }
) )  ->  y  e.  A ) )
169 sseq1 3518 . . . . . . . 8  |-  ( y  =  ( `' ( ( invg `  S ) `  u
) " ( _V 
\  {  .0.  }
) )  ->  (
y  C_  ( `' u " ( _V  \  {  .0.  } ) )  <-> 
( `' ( ( invg `  S
) `  u ) " ( _V  \  {  .0.  } ) ) 
C_  ( `' u " ( _V  \  {  .0.  } ) ) ) )
170 eleq1 2532 . . . . . . . 8  |-  ( y  =  ( `' ( ( invg `  S ) `  u
) " ( _V 
\  {  .0.  }
) )  ->  (
y  e.  A  <->  ( `' ( ( invg `  S ) `  u
) " ( _V 
\  {  .0.  }
) )  e.  A
) )
171169, 170imbi12d 320 . . . . . . 7  |-  ( y  =  ( `' ( ( invg `  S ) `  u
) " ( _V 
\  {  .0.  }
) )  ->  (
( y  C_  ( `' u " ( _V 
\  {  .0.  }
) )  ->  y  e.  A )  <->  ( ( `' ( ( invg `  S ) `
 u ) "
( _V  \  {  .0.  } ) )  C_  ( `' u " ( _V 
\  {  .0.  }
) )  ->  ( `' ( ( invg `  S ) `
 u ) "
( _V  \  {  .0.  } ) )  e.  A ) ) )
172171spcgv 3191 . . . . . 6  |-  ( ( `' ( ( invg `  S ) `
 u ) "
( _V  \  {  .0.  } ) )  e. 
_V  ->  ( A. y
( y  C_  ( `' u " ( _V 
\  {  .0.  }
) )  ->  y  e.  A )  ->  (
( `' ( ( invg `  S
) `  u ) " ( _V  \  {  .0.  } ) ) 
C_  ( `' u " ( _V  \  {  .0.  } ) )  -> 
( `' ( ( invg `  S
) `  u ) " ( _V  \  {  .0.  } ) )  e.  A ) ) )
173162, 168, 161, 172syl3c 61 . . . . 5  |-  ( (
ph  /\  u  e.  U )  ->  ( `' ( ( invg `  S ) `
 u ) "
( _V  \  {  .0.  } ) )  e.  A )
17446eleq2d 2530 . . . . . 6  |-  ( (
ph  /\  u  e.  U )  ->  (
( ( invg `  S ) `  u
)  e.  U  <->  ( ( invg `  S ) `
 u )  e. 
{ g  e.  B  |  ( `' g
" ( _V  \  {  .0.  } ) )  e.  A } ) )
175 cnveq 5167 . . . . . . . . 9  |-  ( g  =  ( ( invg `  S ) `
 u )  ->  `' g  =  `' ( ( invg `  S ) `  u
) )
176175imaeq1d 5327 . . . . . . . 8  |-  ( g  =  ( ( invg `  S ) `
 u )  -> 
( `' g "
( _V  \  {  .0.  } ) )  =  ( `' ( ( invg `  S
) `  u ) " ( _V  \  {  .0.  } ) ) )
177176eleq1d 2529 . . . . . . 7  |-  ( g  =  ( ( invg `  S ) `
 u )  -> 
( ( `' g
" ( _V  \  {  .0.  } ) )  e.  A  <->  ( `' ( ( invg `  S ) `  u
) " ( _V 
\  {  .0.  }
) )  e.  A
) )
178177elrab 3254 . . . . . 6  |-  ( ( ( invg `  S ) `  u
)  e.  { g  e.  B  |  ( `' g " ( _V  \  {  .0.  }
) )  e.  A } 
<->  ( ( ( invg `  S ) `
 u )  e.  B  /\  ( `' ( ( invg `  S ) `  u
) " ( _V 
\  {  .0.  }
) )  e.  A
) )
179174, 178syl6bb 261 . . . . 5  |-  ( (
ph  /\  u  e.  U )  ->  (
( ( invg `  S ) `  u
)  e.  U  <->  ( (
( invg `  S ) `  u
)  e.  B  /\  ( `' ( ( invg `  S ) `
 u ) "
( _V  \  {  .0.  } ) )  e.  A ) ) )
180144, 173, 179mpbir2and 915 . . . 4  |-  ( (
ph  /\  u  e.  U )  ->  (
( invg `  S ) `  u
)  e.  U )
181139, 180jca 532 . . 3  |-  ( (
ph  /\  u  e.  U )  ->  ( A. v  e.  U  ( u ( +g  `  S ) v )  e.  U  /\  (
( invg `  S ) `  u
)  e.  U ) )
182181ralrimiva 2871 . 2  |-  ( ph  ->  A. u  e.  U  ( A. v  e.  U  ( u ( +g  `  S ) v )  e.  U  /\  (
( invg `  S ) `  u
)  e.  U ) )
1839, 35, 141issubg2 16004 . . 3  |-  ( S  e.  Grp  ->  ( U  e.  (SubGrp `  S
)  <->  ( U  C_  B  /\  U  =/=  (/)  /\  A. u  e.  U  ( A. v  e.  U  ( u ( +g  `  S ) v )  e.  U  /\  (
( invg `  S ) `  u
)  e.  U ) ) ) )
184140, 183syl 16 . 2  |-  ( ph  ->  ( U  e.  (SubGrp `  S )  <->  ( U  C_  B  /\  U  =/=  (/)  /\  A. u  e.  U  ( A. v  e.  U  ( u
( +g  `  S ) v )  e.  U  /\  ( ( invg `  S ) `  u
)  e.  U ) ) ) )
1853, 34, 182, 184mpbir3and 1174 1  |-  ( ph  ->  U  e.  (SubGrp `  S ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    /\ w3a 968   A.wal 1372    = wceq 1374    e. wcel 1762    =/= wne 2655   A.wral 2807   {crab 2811   _Vcvv 3106    \ cdif 3466    u. cun 3467    C_ wss 3469   (/)c0 3778   {csn 4020    X. cxp 4990   `'ccnv 4991   "cima 4995    o. ccom 4996    Fn wfn 5574   -->wf 5575   ` cfv 5579  (class class class)co 6275    oFcof 6513    ^m cmap 7410   Fincfn 7506   NNcn 10525   NN0cn0 10784   Basecbs 14479   +g cplusg 14544   0gc0g 14684   Grpcgrp 15716   invgcminusg 15717  SubGrpcsubg 15983   mPwSer cmps 17764
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-8 1764  ax-9 1766  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438  ax-rep 4551  ax-sep 4561  ax-nul 4569  ax-pow 4618  ax-pr 4679  ax-un 6567  ax-cnex 9537  ax-resscn 9538  ax-1cn 9539  ax-icn 9540  ax-addcl 9541  ax-addrcl 9542  ax-mulcl 9543  ax-mulrcl 9544  ax-mulcom 9545  ax-addass 9546  ax-mulass 9547  ax-distr 9548  ax-i2m1 9549  ax-1ne0 9550  ax-1rid 9551  ax-rnegex 9552  ax-rrecex 9553  ax-cnre 9554  ax-pre-lttri 9555  ax-pre-lttrn 9556  ax-pre-ltadd 9557  ax-pre-mulgt0 9558
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 969  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-eu 2272  df-mo 2273  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-ne 2657  df-nel 2658  df-ral 2812  df-rex 2813  df-reu 2814  df-rmo 2815  df-rab 2816  df-v 3108  df-sbc 3325  df-csb 3429  df-dif 3472  df-un 3474  df-in 3476  df-ss 3483  df-pss 3485  df-nul 3779  df-if 3933  df-pw 4005  df-sn 4021  df-pr 4023  df-tp 4025  df-op 4027  df-uni 4239  df-int 4276  df-iun 4320  df-br 4441  df-opab 4499  df-mpt 4500  df-tr 4534  df-eprel 4784  df-id 4788  df-po 4793  df-so 4794  df-fr 4831  df-we 4833  df-ord 4874  df-on 4875  df-lim 4876  df-suc 4877  df-xp 4998  df-rel 4999  df-cnv 5000  df-co 5001  df-dm 5002  df-rn 5003  df-res 5004  df-ima 5005  df-iota 5542  df-fun 5581  df-fn 5582  df-f 5583  df-f1 5584  df-fo 5585  df-f1o 5586  df-fv 5587  df-riota 6236  df-ov 6278  df-oprab 6279  df-mpt2 6280  df-of 6515  df-om 6672  df-1st 6774  df-2nd 6775  df-supp 6892  df-recs 7032  df-rdg 7066  df-1o 7120  df-oadd 7124  df-er 7301  df-map 7412  df-en 7507  df-dom 7508  df-sdom 7509  df-fin 7510  df-fsupp 7819  df-pnf 9619  df-mnf 9620  df-xr 9621  df-ltxr 9622  df-le 9623  df-sub 9796  df-neg 9797  df-nn 10526  df-2 10583  df-3 10584  df-4 10585  df-5 10586  df-6 10587  df-7 10588  df-8 10589  df-9 10590  df-n0 10785  df-z 10854  df-uz 11072  df-fz 11662  df-struct 14481  df-ndx 14482  df-slot 14483  df-base 14484  df-sets 14485  df-ress 14486  df-plusg 14557  df-mulr 14558  df-sca 14560  df-vsca 14561  df-tset 14563  df-0g 14686  df-mnd 15721  df-grp 15851  df-minusg 15852  df-subg 15986  df-psr 17769
This theorem is referenced by:  mpllsslemOLD  17860
  Copyright terms: Public domain W3C validator