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

Theorem mplsubglemOLD 17486
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 17484 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 3430 . . 3  |-  { g  e.  B  |  ( `' g " ( _V  \  {  .0.  }
) )  e.  A }  C_  B
31, 2syl6eqss 3399 . 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 17439 . . . 4  |-  ( ph  ->  ( D  X.  {  .0.  } )  e.  B
)
11 eqid 2437 . . . . . . . . 9  |-  ( Base `  R )  =  (
Base `  R )
1211, 8grpidcl 15555 . . . . . . . 8  |-  ( R  e.  Grp  ->  .0.  e.  ( Base `  R
) )
13 fconst6g 5592 . . . . . . . 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 3471 . . . . . . . . 9  |-  ( u  e.  ( D  \  (/) )  ->  u  e.  D )
16 fvex 5694 . . . . . . . . . . 11  |-  ( 0g
`  R )  e. 
_V
178, 16eqeltri 2507 . . . . . . . . . 10  |-  .0.  e.  _V
1817fvconst2 5926 . . . . . . . . 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 5829 . . . . . 6  |-  ( ph  ->  ( `' ( D  X.  {  .0.  }
) " ( _V 
\  {  .0.  }
) )  C_  (/) )
22 ss0 3661 . . . . . 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 2511 . . . 4  |-  ( ph  ->  ( `' ( D  X.  {  .0.  }
) " ( _V 
\  {  .0.  }
) )  e.  A
)
261eleq2d 2504 . . . . 5  |-  ( ph  ->  ( ( D  X.  {  .0.  } )  e.  U  <->  ( D  X.  {  .0.  } )  e. 
{ g  e.  B  |  ( `' g
" ( _V  \  {  .0.  } ) )  e.  A } ) )
27 cnveq 5005 . . . . . . . 8  |-  ( g  =  ( D  X.  {  .0.  } )  ->  `' g  =  `' ( D  X.  {  .0.  } ) )
2827imaeq1d 5161 . . . . . . 7  |-  ( g  =  ( D  X.  {  .0.  } )  -> 
( `' g "
( _V  \  {  .0.  } ) )  =  ( `' ( D  X.  {  .0.  }
) " ( _V 
\  {  .0.  }
) ) )
2928eleq1d 2503 . . . . . 6  |-  ( g  =  ( D  X.  {  .0.  } )  -> 
( ( `' g
" ( _V  \  {  .0.  } ) )  e.  A  <->  ( `' ( D  X.  {  .0.  } ) " ( _V 
\  {  .0.  }
) )  e.  A
) )
3029elrab 3110 . . . . 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 913 . . 3  |-  ( ph  ->  ( D  X.  {  .0.  } )  e.  U
)
33 ne0i 3636 . . 3  |-  ( ( D  X.  {  .0.  } )  e.  U  ->  U  =/=  (/) )
3432, 33syl 16 . 2  |-  ( ph  ->  U  =/=  (/) )
35 eqid 2437 . . . . . . 7  |-  ( +g  `  S )  =  ( +g  `  S )
366ad2antrr 725 . . . . . . 7  |-  ( ( ( ph  /\  u  e.  U )  /\  v  e.  U )  ->  R  e.  Grp )
371eleq2d 2504 . . . . . . . . . . 11  |-  ( ph  ->  ( u  e.  U  <->  u  e.  { g  e.  B  |  ( `' g " ( _V 
\  {  .0.  }
) )  e.  A } ) )
38 cnveq 5005 . . . . . . . . . . . . . 14  |-  ( g  =  u  ->  `' g  =  `' u
)
3938imaeq1d 5161 . . . . . . . . . . . . 13  |-  ( g  =  u  ->  ( `' g " ( _V  \  {  .0.  }
) )  =  ( `' u " ( _V 
\  {  .0.  }
) ) )
4039eleq1d 2503 . . . . . . . . . . . 12  |-  ( g  =  u  ->  (
( `' g "
( _V  \  {  .0.  } ) )  e.  A  <->  ( `' u " ( _V  \  {  .0.  } ) )  e.  A ) )
4140elrab 3110 . . . . . . . . . . 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 2504 . . . . . . . . . 10  |-  ( (
ph  /\  u  e.  U )  ->  (
v  e.  U  <->  v  e.  { g  e.  B  | 
( `' g "
( _V  \  {  .0.  } ) )  e.  A } ) )
48 cnveq 5005 . . . . . . . . . . . . 13  |-  ( g  =  v  ->  `' g  =  `' v
)
4948imaeq1d 5161 . . . . . . . . . . . 12  |-  ( g  =  v  ->  ( `' g " ( _V  \  {  .0.  }
) )  =  ( `' v " ( _V  \  {  .0.  }
) ) )
5049eleq1d 2503 . . . . . . . . . . 11  |-  ( g  =  v  ->  (
( `' g "
( _V  \  {  .0.  } ) )  e.  A  <->  ( `' v
" ( _V  \  {  .0.  } ) )  e.  A ) )
5150elrab 3110 . . . . . . . . . 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 17428 . . . . . 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 2802 . . . . . . . . . 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 3496 . . . . . . . . . . 11  |-  ( x  =  ( `' u " ( _V  \  {  .0.  } ) )  -> 
( x  u.  y
)  =  ( ( `' u " ( _V 
\  {  .0.  }
) )  u.  y
) )
6362eleq1d 2503 . . . . . . . . . 10  |-  ( x  =  ( `' u " ( _V  \  {  .0.  } ) )  -> 
( ( x  u.  y )  e.  A  <->  ( ( `' u "
( _V  \  {  .0.  } ) )  u.  y )  e.  A
) )
64 uneq2 3497 . . . . . . . . . . 11  |-  ( y  =  ( `' v
" ( _V  \  {  .0.  } ) )  ->  ( ( `' u " ( _V 
\  {  .0.  }
) )  u.  y
)  =  ( ( `' u " ( _V 
\  {  .0.  }
) )  u.  ( `' v " ( _V  \  {  .0.  }
) ) ) )
6564eleq1d 2503 . . . . . . . . . 10  |-  ( y  =  ( `' v
" ( _V  \  {  .0.  } ) )  ->  ( ( ( `' u " ( _V 
\  {  .0.  }
) )  u.  y
)  e.  A  <->  ( ( `' u " ( _V 
\  {  .0.  }
) )  u.  ( `' v " ( _V  \  {  .0.  }
) ) )  e.  A ) )
6663, 65rspc2va 3073 . . . . . . . . 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 1217 . . . . . . . 8  |-  ( ( ( ph  /\  u  e.  U )  /\  v  e.  U )  ->  (
( `' u "
( _V  \  {  .0.  } ) )  u.  ( `' v "
( _V  \  {  .0.  } ) ) )  e.  A )
684, 11, 7, 9, 55psrelbas 17424 . . . . . . . . 9  |-  ( ( ( ph  /\  u  e.  U )  /\  v  e.  U )  ->  (
u ( +g  `  S
) v ) : D --> ( Base `  R
) )
69 eqid 2437 . . . . . . . . . . . . 13  |-  ( +g  `  R )  =  ( +g  `  R )
704, 9, 69, 35, 45, 54psradd 17427 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  u  e.  U )  /\  v  e.  U )  ->  (
u ( +g  `  S
) v )  =  ( u  oF ( +g  `  R
) v ) )
7170fveq1d 5686 . . . . . . . . . . 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 3471 . . . . . . . . . . 11  |-  ( k  e.  ( D  \ 
( ( `' u " ( _V  \  {  .0.  } ) )  u.  ( `' v "
( _V  \  {  .0.  } ) ) ) )  ->  k  e.  D )
744, 11, 7, 9, 44psrelbas 17424 . . . . . . . . . . . . . 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 5552 . . . . . . . . . . . . 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 17424 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  u  e.  U )  /\  v  e.  U )  ->  v : D --> ( Base `  R
) )
79 ffn 5552 . . . . . . . . . . . . 13  |-  ( v : D --> ( Base `  R )  ->  v  Fn  D )
8078, 79syl 16 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  u  e.  U )  /\  v  e.  U )  ->  v  Fn  D )
81 ovex 6111 . . . . . . . . . . . . . . 15  |-  ( NN0 
^m  I )  e. 
_V
8281rabex 4436 . . . . . . . . . . . . . 14  |-  { f  e.  ( NN0  ^m  I )  |  ( `' f " NN )  e.  Fin }  e.  _V
837, 82eqeltri 2507 . . . . . . . . . . . . 13  |-  D  e. 
_V
8483a1i 11 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  u  e.  U )  /\  v  e.  U )  ->  D  e.  _V )
85 inidm 3552 . . . . . . . . . . . 12  |-  ( D  i^i  D )  =  D
86 eqidd 2438 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  u  e.  U )  /\  v  e.  U
)  /\  k  e.  D )  ->  (
u `  k )  =  ( u `  k ) )
87 eqidd 2438 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  u  e.  U )  /\  v  e.  U
)  /\  k  e.  D )  ->  (
v `  k )  =  ( v `  k ) )
8877, 80, 84, 84, 85, 86, 87ofval 6324 . . . . . . . . . . 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 3512 . . . . . . . . . . . . . . 15  |-  ( `' u " ( _V 
\  {  .0.  }
) )  C_  (
( `' u "
( _V  \  {  .0.  } ) )  u.  ( `' v "
( _V  \  {  .0.  } ) ) )
91 sscon 3483 . . . . . . . . . . . . . . 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 3345 . . . . . . . . . . . . 13  |-  ( k  e.  ( D  \ 
( ( `' u " ( _V  \  {  .0.  } ) )  u.  ( `' v "
( _V  \  {  .0.  } ) ) ) )  ->  k  e.  ( D  \  ( `' u " ( _V 
\  {  .0.  }
) ) ) )
94 ssid 3368 . . . . . . . . . . . . . . . 16  |-  ( `' u " ( _V 
\  {  .0.  }
) )  C_  ( `' u " ( _V 
\  {  .0.  }
) )
9594a1i 11 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  u  e.  U )  ->  ( `' u " ( _V 
\  {  .0.  }
) )  C_  ( `' u " ( _V 
\  {  .0.  }
) ) )
9674, 95suppssrOLD 5830 . . . . . . . . . . . . . 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 3513 . . . . . . . . . . . . . . 15  |-  ( `' v " ( _V 
\  {  .0.  }
) )  C_  (
( `' u "
( _V  \  {  .0.  } ) )  u.  ( `' v "
( _V  \  {  .0.  } ) ) )
100 sscon 3483 . . . . . . . . . . . . . . 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 3345 . . . . . . . . . . . . 13  |-  ( k  e.  ( D  \ 
( ( `' u " ( _V  \  {  .0.  } ) )  u.  ( `' v "
( _V  \  {  .0.  } ) ) ) )  ->  k  e.  ( D  \  ( `' v " ( _V  \  {  .0.  }
) ) ) )
103 ssid 3368 . . . . . . . . . . . . . . 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 5830 . . . . . . . . . . . . 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 6104 . . . . . . . . . . 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 15557 . . . . . . . . . . . . . 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 2469 . . . . . . . . . 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 2473 . . . . . . . . 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 5829 . . . . . . . 8  |-  ( ( ( ph  /\  u  e.  U )  /\  v  e.  U )  ->  ( `' ( u ( +g  `  S ) v ) " ( _V  \  {  .0.  }
) )  C_  (
( `' u "
( _V  \  {  .0.  } ) )  u.  ( `' v "
( _V  \  {  .0.  } ) ) ) )
11567, 114ssexd 4432 . . . . . . 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 1685 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  A )  ->  A. y
( y  C_  x  ->  y  e.  A ) )
119118ralrimiva 2793 . . . . . . . . 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 3371 . . . . . . . . . . 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 1679 . . . . . . . . 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 3062 . . . . . . . 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 3370 . . . . . . . . 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 2497 . . . . . . . . 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 3050 . . . . . . 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 2504 . . . . . . 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 5005 . . . . . . . . . 10  |-  ( g  =  ( u ( +g  `  S ) v )  ->  `' g  =  `' (
u ( +g  `  S
) v ) )
134133imaeq1d 5161 . . . . . . . . 9  |-  ( g  =  ( u ( +g  `  S ) v )  ->  ( `' g " ( _V  \  {  .0.  }
) )  =  ( `' ( u ( +g  `  S ) v ) " ( _V  \  {  .0.  }
) ) )
135134eleq1d 2503 . . . . . . . 8  |-  ( g  =  ( u ( +g  `  S ) v )  ->  (
( `' g "
( _V  \  {  .0.  } ) )  e.  A  <->  ( `' ( u ( +g  `  S
) v ) "
( _V  \  {  .0.  } ) )  e.  A ) )
136135elrab 3110 . . . . . . 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 913 . . . . 5  |-  ( ( ( ph  /\  u  e.  U )  /\  v  e.  U )  ->  (
u ( +g  `  S
) v )  e.  U )
139138ralrimiva 2793 . . . 4  |-  ( (
ph  /\  u  e.  U )  ->  A. v  e.  U  ( u
( +g  `  S ) v )  e.  U
)
1404, 5, 6psrgrp 17443 . . . . . . 7  |-  ( ph  ->  S  e.  Grp )
141 eqid 2437 . . . . . . . 8  |-  ( invg `  S )  =  ( invg `  S )
1429, 141grpinvcl 15572 . . . . . . 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 17424 . . . . . . . 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 2437 . . . . . . . . . . . 12  |-  ( invg `  R )  =  ( invg `  R )
1494, 146, 147, 7, 148, 9, 141, 44psrneg 17445 . . . . . . . . . . 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 5686 . . . . . . . . 9  |-  ( ( ( ph  /\  u  e.  U )  /\  k  e.  ( D  \  ( `' u " ( _V 
\  {  .0.  }
) ) ) )  ->  ( ( ( invg `  S
) `  u ) `  k )  =  ( ( ( invg `  R )  o.  u
) `  k )
)
152 eldifi 3471 . . . . . . . . . 10  |-  ( k  e.  ( D  \ 
( `' u "
( _V  \  {  .0.  } ) ) )  ->  k  e.  D
)
153 fvco3 5761 . . . . . . . . . 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 5688 . . . . . . . . . 10  |-  ( ( ( ph  /\  u  e.  U )  /\  k  e.  ( D  \  ( `' u " ( _V 
\  {  .0.  }
) ) ) )  ->  ( ( invg `  R ) `
 ( u `  k ) )  =  ( ( invg `  R ) `  .0.  ) )
1568, 148grpinvid 15578 . . . . . . . . . . . 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 2469 . . . . . . . . 9  |-  ( ( ( ph  /\  u  e.  U )  /\  k  e.  ( D  \  ( `' u " ( _V 
\  {  .0.  }
) ) ) )  ->  ( ( invg `  R ) `
 ( u `  k ) )  =  .0.  )
160151, 154, 1593eqtrd 2473 . . . . . . . 8  |-  ( ( ( ph  /\  u  e.  U )  /\  k  e.  ( D  \  ( `' u " ( _V 
\  {  .0.  }
) ) ) )  ->  ( ( ( invg `  S
) `  u ) `  k )  =  .0.  )
161145, 160suppssOLD 5829 . . . . . . 7  |-  ( (
ph  /\  u  e.  U )  ->  ( `' ( ( invg `  S ) `
 u ) "
( _V  \  {  .0.  } ) )  C_  ( `' u " ( _V 
\  {  .0.  }
) ) )
16256, 161ssexd 4432 . . . . . 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 3371 . . . . . . . . . 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 1679 . . . . . . . 8  |-  ( x  =  ( `' u " ( _V  \  {  .0.  } ) )  -> 
( A. y ( y  C_  x  ->  y  e.  A )  <->  A. y
( y  C_  ( `' u " ( _V 
\  {  .0.  }
) )  ->  y  e.  A ) ) )
167166rspcv 3062 . . . . . . 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 3370 . . . . . . . 8  |-  ( y  =  ( `' ( ( invg `  S ) `  u
) " ( _V 
\  {  .0.  }
) )  ->  (
y  C_  ( `' u " ( _V  \  {  .0.  } ) )  <-> 
( `' ( ( invg `  S
) `  u ) " ( _V  \  {  .0.  } ) ) 
C_  ( `' u " ( _V  \  {  .0.  } ) ) ) )
170 eleq1 2497 . . . . . . . 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 3050 . . . . . 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 2504 . . . . . 6  |-  ( (
ph  /\  u  e.  U )  ->  (
( ( invg `  S ) `  u
)  e.  U  <->  ( ( invg `  S ) `
 u )  e. 
{ g  e.  B  |  ( `' g
" ( _V  \  {  .0.  } ) )  e.  A } ) )
175 cnveq 5005 . . . . . . . . 9  |-  ( g  =  ( ( invg `  S ) `
 u )  ->  `' g  =  `' ( ( invg `  S ) `  u
) )
176175imaeq1d 5161 . . . . . . . 8  |-  ( g  =  ( ( invg `  S ) `
 u )  -> 
( `' g "
( _V  \  {  .0.  } ) )  =  ( `' ( ( invg `  S
) `  u ) " ( _V  \  {  .0.  } ) ) )
177176eleq1d 2503 . . . . . . 7  |-  ( g  =  ( ( invg `  S ) `
 u )  -> 
( ( `' g
" ( _V  \  {  .0.  } ) )  e.  A  <->  ( `' ( ( invg `  S ) `  u
) " ( _V 
\  {  .0.  }
) )  e.  A
) )
178177elrab 3110 . . . . . 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 913 . . . 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 2793 . 2  |-  ( ph  ->  A. u  e.  U  ( A. v  e.  U  ( u ( +g  `  S ) v )  e.  U  /\  (
( invg `  S ) `  u
)  e.  U ) )
1839, 35, 141issubg2 15685 . . 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 1171 1  |-  ( ph  ->  U  e.  (SubGrp `  S ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    /\ w3a 965   A.wal 1367    = wceq 1369    e. wcel 1756    =/= wne 2600   A.wral 2709   {crab 2713   _Vcvv 2966    \ cdif 3318    u. cun 3319    C_ wss 3321   (/)c0 3630   {csn 3870    X. cxp 4830   `'ccnv 4831   "cima 4835    o. ccom 4836    Fn wfn 5406   -->wf 5407   ` cfv 5411  (class class class)co 6086    oFcof 6313    ^m cmap 7206   Fincfn 7302   NNcn 10314   NN0cn0 10571   Basecbs 14166   +g cplusg 14230   0gc0g 14370   Grpcgrp 15402   invgcminusg 15403  SubGrpcsubg 15664   mPwSer cmps 17392
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2418  ax-rep 4396  ax-sep 4406  ax-nul 4414  ax-pow 4463  ax-pr 4524  ax-un 6367  ax-cnex 9330  ax-resscn 9331  ax-1cn 9332  ax-icn 9333  ax-addcl 9334  ax-addrcl 9335  ax-mulcl 9336  ax-mulrcl 9337  ax-mulcom 9338  ax-addass 9339  ax-mulass 9340  ax-distr 9341  ax-i2m1 9342  ax-1ne0 9343  ax-1rid 9344  ax-rnegex 9345  ax-rrecex 9346  ax-cnre 9347  ax-pre-lttri 9348  ax-pre-lttrn 9349  ax-pre-ltadd 9350  ax-pre-mulgt0 9351
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2256  df-mo 2257  df-clab 2424  df-cleq 2430  df-clel 2433  df-nfc 2562  df-ne 2602  df-nel 2603  df-ral 2714  df-rex 2715  df-reu 2716  df-rmo 2717  df-rab 2718  df-v 2968  df-sbc 3180  df-csb 3282  df-dif 3324  df-un 3326  df-in 3328  df-ss 3335  df-pss 3337  df-nul 3631  df-if 3785  df-pw 3855  df-sn 3871  df-pr 3873  df-tp 3875  df-op 3877  df-uni 4085  df-int 4122  df-iun 4166  df-br 4286  df-opab 4344  df-mpt 4345  df-tr 4379  df-eprel 4624  df-id 4628  df-po 4633  df-so 4634  df-fr 4671  df-we 4673  df-ord 4714  df-on 4715  df-lim 4716  df-suc 4717  df-xp 4838  df-rel 4839  df-cnv 4840  df-co 4841  df-dm 4842  df-rn 4843  df-res 4844  df-ima 4845  df-iota 5374  df-fun 5413  df-fn 5414  df-f 5415  df-f1 5416  df-fo 5417  df-f1o 5418  df-fv 5419  df-riota 6045  df-ov 6089  df-oprab 6090  df-mpt2 6091  df-of 6315  df-om 6472  df-1st 6572  df-2nd 6573  df-supp 6686  df-recs 6824  df-rdg 6858  df-1o 6912  df-oadd 6916  df-er 7093  df-map 7208  df-en 7303  df-dom 7304  df-sdom 7305  df-fin 7306  df-fsupp 7613  df-pnf 9412  df-mnf 9413  df-xr 9414  df-ltxr 9415  df-le 9416  df-sub 9589  df-neg 9590  df-nn 10315  df-2 10372  df-3 10373  df-4 10374  df-5 10375  df-6 10376  df-7 10377  df-8 10378  df-9 10379  df-n0 10572  df-z 10639  df-uz 10854  df-fz 11430  df-struct 14168  df-ndx 14169  df-slot 14170  df-base 14171  df-sets 14172  df-ress 14173  df-plusg 14243  df-mulr 14244  df-sca 14246  df-vsca 14247  df-tset 14249  df-0g 14372  df-mnd 15407  df-grp 15534  df-minusg 15535  df-subg 15667  df-psr 17397
This theorem is referenced by:  mpllsslemOLD  17487
  Copyright terms: Public domain W3C validator