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

Theorem mplsubglemOLD 18222
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 18220 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 3581 . . 3  |-  { g  e.  B  |  ( `' g " ( _V  \  {  .0.  }
) )  e.  A }  C_  B
31, 2syl6eqss 3549 . 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 18174 . . . 4  |-  ( ph  ->  ( D  X.  {  .0.  } )  e.  B
)
11 eqid 2457 . . . . . . . . 9  |-  ( Base `  R )  =  (
Base `  R )
1211, 8grpidcl 16205 . . . . . . . 8  |-  ( R  e.  Grp  ->  .0.  e.  ( Base `  R
) )
13 fconst6g 5780 . . . . . . . 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 3622 . . . . . . . . 9  |-  ( u  e.  ( D  \  (/) )  ->  u  e.  D )
16 fvex 5882 . . . . . . . . . . 11  |-  ( 0g
`  R )  e. 
_V
178, 16eqeltri 2541 . . . . . . . . . 10  |-  .0.  e.  _V
1817fvconst2 6128 . . . . . . . . 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 6021 . . . . . 6  |-  ( ph  ->  ( `' ( D  X.  {  .0.  }
) " ( _V 
\  {  .0.  }
) )  C_  (/) )
22 ss0 3825 . . . . . 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 2545 . . . 4  |-  ( ph  ->  ( `' ( D  X.  {  .0.  }
) " ( _V 
\  {  .0.  }
) )  e.  A
)
261eleq2d 2527 . . . . 5  |-  ( ph  ->  ( ( D  X.  {  .0.  } )  e.  U  <->  ( D  X.  {  .0.  } )  e. 
{ g  e.  B  |  ( `' g
" ( _V  \  {  .0.  } ) )  e.  A } ) )
27 cnveq 5186 . . . . . . . 8  |-  ( g  =  ( D  X.  {  .0.  } )  ->  `' g  =  `' ( D  X.  {  .0.  } ) )
2827imaeq1d 5346 . . . . . . 7  |-  ( g  =  ( D  X.  {  .0.  } )  -> 
( `' g "
( _V  \  {  .0.  } ) )  =  ( `' ( D  X.  {  .0.  }
) " ( _V 
\  {  .0.  }
) ) )
2928eleq1d 2526 . . . . . 6  |-  ( g  =  ( D  X.  {  .0.  } )  -> 
( ( `' g
" ( _V  \  {  .0.  } ) )  e.  A  <->  ( `' ( D  X.  {  .0.  } ) " ( _V 
\  {  .0.  }
) )  e.  A
) )
3029elrab 3257 . . . . 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 922 . . 3  |-  ( ph  ->  ( D  X.  {  .0.  } )  e.  U
)
33 ne0i 3799 . . 3  |-  ( ( D  X.  {  .0.  } )  e.  U  ->  U  =/=  (/) )
3432, 33syl 16 . 2  |-  ( ph  ->  U  =/=  (/) )
35 eqid 2457 . . . . . . 7  |-  ( +g  `  S )  =  ( +g  `  S )
366ad2antrr 725 . . . . . . 7  |-  ( ( ( ph  /\  u  e.  U )  /\  v  e.  U )  ->  R  e.  Grp )
371eleq2d 2527 . . . . . . . . . . 11  |-  ( ph  ->  ( u  e.  U  <->  u  e.  { g  e.  B  |  ( `' g " ( _V 
\  {  .0.  }
) )  e.  A } ) )
38 cnveq 5186 . . . . . . . . . . . . . 14  |-  ( g  =  u  ->  `' g  =  `' u
)
3938imaeq1d 5346 . . . . . . . . . . . . 13  |-  ( g  =  u  ->  ( `' g " ( _V  \  {  .0.  }
) )  =  ( `' u " ( _V 
\  {  .0.  }
) ) )
4039eleq1d 2526 . . . . . . . . . . . 12  |-  ( g  =  u  ->  (
( `' g "
( _V  \  {  .0.  } ) )  e.  A  <->  ( `' u " ( _V  \  {  .0.  } ) )  e.  A ) )
4140elrab 3257 . . . . . . . . . . 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 2527 . . . . . . . . . 10  |-  ( (
ph  /\  u  e.  U )  ->  (
v  e.  U  <->  v  e.  { g  e.  B  | 
( `' g "
( _V  \  {  .0.  } ) )  e.  A } ) )
48 cnveq 5186 . . . . . . . . . . . . 13  |-  ( g  =  v  ->  `' g  =  `' v
)
4948imaeq1d 5346 . . . . . . . . . . . 12  |-  ( g  =  v  ->  ( `' g " ( _V  \  {  .0.  }
) )  =  ( `' v " ( _V  \  {  .0.  }
) ) )
5049eleq1d 2526 . . . . . . . . . . 11  |-  ( g  =  v  ->  (
( `' g "
( _V  \  {  .0.  } ) )  e.  A  <->  ( `' v
" ( _V  \  {  .0.  } ) )  e.  A ) )
5150elrab 3257 . . . . . . . . . 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 18163 . . . . . 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 3647 . . . . . . . . . . 11  |-  ( x  =  ( `' u " ( _V  \  {  .0.  } ) )  -> 
( x  u.  y
)  =  ( ( `' u " ( _V 
\  {  .0.  }
) )  u.  y
) )
6362eleq1d 2526 . . . . . . . . . 10  |-  ( x  =  ( `' u " ( _V  \  {  .0.  } ) )  -> 
( ( x  u.  y )  e.  A  <->  ( ( `' u "
( _V  \  {  .0.  } ) )  u.  y )  e.  A
) )
64 uneq2 3648 . . . . . . . . . . 11  |-  ( y  =  ( `' v
" ( _V  \  {  .0.  } ) )  ->  ( ( `' u " ( _V 
\  {  .0.  }
) )  u.  y
)  =  ( ( `' u " ( _V 
\  {  .0.  }
) )  u.  ( `' v " ( _V  \  {  .0.  }
) ) ) )
6564eleq1d 2526 . . . . . . . . . 10  |-  ( y  =  ( `' v
" ( _V  \  {  .0.  } ) )  ->  ( ( ( `' u " ( _V 
\  {  .0.  }
) )  u.  y
)  e.  A  <->  ( ( `' u " ( _V 
\  {  .0.  }
) )  u.  ( `' v " ( _V  \  {  .0.  }
) ) )  e.  A ) )
6663, 65rspc2va 3220 . . . . . . . . 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 1227 . . . . . . . 8  |-  ( ( ( ph  /\  u  e.  U )  /\  v  e.  U )  ->  (
( `' u "
( _V  \  {  .0.  } ) )  u.  ( `' v "
( _V  \  {  .0.  } ) ) )  e.  A )
684, 11, 7, 9, 55psrelbas 18159 . . . . . . . . 9  |-  ( ( ( ph  /\  u  e.  U )  /\  v  e.  U )  ->  (
u ( +g  `  S
) v ) : D --> ( Base `  R
) )
69 eqid 2457 . . . . . . . . . . . . 13  |-  ( +g  `  R )  =  ( +g  `  R )
704, 9, 69, 35, 45, 54psradd 18162 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  u  e.  U )  /\  v  e.  U )  ->  (
u ( +g  `  S
) v )  =  ( u  oF ( +g  `  R
) v ) )
7170fveq1d 5874 . . . . . . . . . . 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 3622 . . . . . . . . . . 11  |-  ( k  e.  ( D  \ 
( ( `' u " ( _V  \  {  .0.  } ) )  u.  ( `' v "
( _V  \  {  .0.  } ) ) ) )  ->  k  e.  D )
744, 11, 7, 9, 44psrelbas 18159 . . . . . . . . . . . . . 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 5737 . . . . . . . . . . . . 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 18159 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  u  e.  U )  /\  v  e.  U )  ->  v : D --> ( Base `  R
) )
79 ffn 5737 . . . . . . . . . . . . 13  |-  ( v : D --> ( Base `  R )  ->  v  Fn  D )
8078, 79syl 16 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  u  e.  U )  /\  v  e.  U )  ->  v  Fn  D )
81 ovex 6324 . . . . . . . . . . . . . . 15  |-  ( NN0 
^m  I )  e. 
_V
8281rabex 4607 . . . . . . . . . . . . . 14  |-  { f  e.  ( NN0  ^m  I )  |  ( `' f " NN )  e.  Fin }  e.  _V
837, 82eqeltri 2541 . . . . . . . . . . . . 13  |-  D  e. 
_V
8483a1i 11 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  u  e.  U )  /\  v  e.  U )  ->  D  e.  _V )
85 inidm 3703 . . . . . . . . . . . 12  |-  ( D  i^i  D )  =  D
86 eqidd 2458 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  u  e.  U )  /\  v  e.  U
)  /\  k  e.  D )  ->  (
u `  k )  =  ( u `  k ) )
87 eqidd 2458 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  u  e.  U )  /\  v  e.  U
)  /\  k  e.  D )  ->  (
v `  k )  =  ( v `  k ) )
8877, 80, 84, 84, 85, 86, 87ofval 6548 . . . . . . . . . . 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 3663 . . . . . . . . . . . . . . 15  |-  ( `' u " ( _V 
\  {  .0.  }
) )  C_  (
( `' u "
( _V  \  {  .0.  } ) )  u.  ( `' v "
( _V  \  {  .0.  } ) ) )
91 sscon 3634 . . . . . . . . . . . . . . 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 3495 . . . . . . . . . . . . 13  |-  ( k  e.  ( D  \ 
( ( `' u " ( _V  \  {  .0.  } ) )  u.  ( `' v "
( _V  \  {  .0.  } ) ) ) )  ->  k  e.  ( D  \  ( `' u " ( _V 
\  {  .0.  }
) ) ) )
94 ssid 3518 . . . . . . . . . . . . . . . 16  |-  ( `' u " ( _V 
\  {  .0.  }
) )  C_  ( `' u " ( _V 
\  {  .0.  }
) )
9594a1i 11 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  u  e.  U )  ->  ( `' u " ( _V 
\  {  .0.  }
) )  C_  ( `' u " ( _V 
\  {  .0.  }
) ) )
9674, 95suppssrOLD 6022 . . . . . . . . . . . . . 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 3664 . . . . . . . . . . . . . . 15  |-  ( `' v " ( _V 
\  {  .0.  }
) )  C_  (
( `' u "
( _V  \  {  .0.  } ) )  u.  ( `' v "
( _V  \  {  .0.  } ) ) )
100 sscon 3634 . . . . . . . . . . . . . . 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 3495 . . . . . . . . . . . . 13  |-  ( k  e.  ( D  \ 
( ( `' u " ( _V  \  {  .0.  } ) )  u.  ( `' v "
( _V  \  {  .0.  } ) ) ) )  ->  k  e.  ( D  \  ( `' v " ( _V  \  {  .0.  }
) ) ) )
103 ssid 3518 . . . . . . . . . . . . . . 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 6022 . . . . . . . . . . . . 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 6314 . . . . . . . . . . 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 16207 . . . . . . . . . . . . . 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 2498 . . . . . . . . . 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 2502 . . . . . . . . 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 6021 . . . . . . . 8  |-  ( ( ( ph  /\  u  e.  U )  /\  v  e.  U )  ->  ( `' ( u ( +g  `  S ) v ) " ( _V  \  {  .0.  }
) )  C_  (
( `' u "
( _V  \  {  .0.  } ) )  u.  ( `' v "
( _V  \  {  .0.  } ) ) ) )
11567, 114ssexd 4603 . . . . . . 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 1720 . . . . . . . . . 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 3521 . . . . . . . . . . 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 1714 . . . . . . . . 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 3206 . . . . . . . 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 3520 . . . . . . . . 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 2529 . . . . . . . . 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 3194 . . . . . . 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 2527 . . . . . . 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 5186 . . . . . . . . . 10  |-  ( g  =  ( u ( +g  `  S ) v )  ->  `' g  =  `' (
u ( +g  `  S
) v ) )
134133imaeq1d 5346 . . . . . . . . 9  |-  ( g  =  ( u ( +g  `  S ) v )  ->  ( `' g " ( _V  \  {  .0.  }
) )  =  ( `' ( u ( +g  `  S ) v ) " ( _V  \  {  .0.  }
) ) )
135134eleq1d 2526 . . . . . . . 8  |-  ( g  =  ( u ( +g  `  S ) v )  ->  (
( `' g "
( _V  \  {  .0.  } ) )  e.  A  <->  ( `' ( u ( +g  `  S
) v ) "
( _V  \  {  .0.  } ) )  e.  A ) )
136135elrab 3257 . . . . . . 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 922 . . . . 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 18178 . . . . . . 7  |-  ( ph  ->  S  e.  Grp )
141 eqid 2457 . . . . . . . 8  |-  ( invg `  S )  =  ( invg `  S )
1429, 141grpinvcl 16222 . . . . . . 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 18159 . . . . . . . 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 2457 . . . . . . . . . . . 12  |-  ( invg `  R )  =  ( invg `  R )
1494, 146, 147, 7, 148, 9, 141, 44psrneg 18180 . . . . . . . . . . 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 5874 . . . . . . . . 9  |-  ( ( ( ph  /\  u  e.  U )  /\  k  e.  ( D  \  ( `' u " ( _V 
\  {  .0.  }
) ) ) )  ->  ( ( ( invg `  S
) `  u ) `  k )  =  ( ( ( invg `  R )  o.  u
) `  k )
)
152 eldifi 3622 . . . . . . . . . 10  |-  ( k  e.  ( D  \ 
( `' u "
( _V  \  {  .0.  } ) ) )  ->  k  e.  D
)
153 fvco3 5950 . . . . . . . . . 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 5876 . . . . . . . . . 10  |-  ( ( ( ph  /\  u  e.  U )  /\  k  e.  ( D  \  ( `' u " ( _V 
\  {  .0.  }
) ) ) )  ->  ( ( invg `  R ) `
 ( u `  k ) )  =  ( ( invg `  R ) `  .0.  ) )
1568, 148grpinvid 16228 . . . . . . . . . . . 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 2498 . . . . . . . . 9  |-  ( ( ( ph  /\  u  e.  U )  /\  k  e.  ( D  \  ( `' u " ( _V 
\  {  .0.  }
) ) ) )  ->  ( ( invg `  R ) `
 ( u `  k ) )  =  .0.  )
160151, 154, 1593eqtrd 2502 . . . . . . . 8  |-  ( ( ( ph  /\  u  e.  U )  /\  k  e.  ( D  \  ( `' u " ( _V 
\  {  .0.  }
) ) ) )  ->  ( ( ( invg `  S
) `  u ) `  k )  =  .0.  )
161145, 160suppssOLD 6021 . . . . . . 7  |-  ( (
ph  /\  u  e.  U )  ->  ( `' ( ( invg `  S ) `
 u ) "
( _V  \  {  .0.  } ) )  C_  ( `' u " ( _V 
\  {  .0.  }
) ) )
16256, 161ssexd 4603 . . . . . 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 3521 . . . . . . . . . 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 1714 . . . . . . . 8  |-  ( x  =  ( `' u " ( _V  \  {  .0.  } ) )  -> 
( A. y ( y  C_  x  ->  y  e.  A )  <->  A. y
( y  C_  ( `' u " ( _V 
\  {  .0.  }
) )  ->  y  e.  A ) ) )
167166rspcv 3206 . . . . . . 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 3520 . . . . . . . 8  |-  ( y  =  ( `' ( ( invg `  S ) `  u
) " ( _V 
\  {  .0.  }
) )  ->  (
y  C_  ( `' u " ( _V  \  {  .0.  } ) )  <-> 
( `' ( ( invg `  S
) `  u ) " ( _V  \  {  .0.  } ) ) 
C_  ( `' u " ( _V  \  {  .0.  } ) ) ) )
170 eleq1 2529 . . . . . . . 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 3194 . . . . . 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 2527 . . . . . 6  |-  ( (
ph  /\  u  e.  U )  ->  (
( ( invg `  S ) `  u
)  e.  U  <->  ( ( invg `  S ) `
 u )  e. 
{ g  e.  B  |  ( `' g
" ( _V  \  {  .0.  } ) )  e.  A } ) )
175 cnveq 5186 . . . . . . . . 9  |-  ( g  =  ( ( invg `  S ) `
 u )  ->  `' g  =  `' ( ( invg `  S ) `  u
) )
176175imaeq1d 5346 . . . . . . . 8  |-  ( g  =  ( ( invg `  S ) `
 u )  -> 
( `' g "
( _V  \  {  .0.  } ) )  =  ( `' ( ( invg `  S
) `  u ) " ( _V  \  {  .0.  } ) ) )
177176eleq1d 2526 . . . . . . 7  |-  ( g  =  ( ( invg `  S ) `
 u )  -> 
( ( `' g
" ( _V  \  {  .0.  } ) )  e.  A  <->  ( `' ( ( invg `  S ) `  u
) " ( _V 
\  {  .0.  }
) )  e.  A
) )
178177elrab 3257 . . . . . 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 922 . . . 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 16343 . . 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 1179 1  |-  ( ph  ->  U  e.  (SubGrp `  S ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    /\ w3a 973   A.wal 1393    = wceq 1395    e. wcel 1819    =/= wne 2652   A.wral 2807   {crab 2811   _Vcvv 3109    \ cdif 3468    u. cun 3469    C_ wss 3471   (/)c0 3793   {csn 4032    X. cxp 5006   `'ccnv 5007   "cima 5011    o. ccom 5012    Fn wfn 5589   -->wf 5590   ` cfv 5594  (class class class)co 6296    oFcof 6537    ^m cmap 7438   Fincfn 7535   NNcn 10556   NN0cn0 10816   Basecbs 14644   +g cplusg 14712   0gc0g 14857   Grpcgrp 16180   invgcminusg 16181  SubGrpcsubg 16322   mPwSer cmps 18127
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-8 1821  ax-9 1823  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435  ax-rep 4568  ax-sep 4578  ax-nul 4586  ax-pow 4634  ax-pr 4695  ax-un 6591  ax-cnex 9565  ax-resscn 9566  ax-1cn 9567  ax-icn 9568  ax-addcl 9569  ax-addrcl 9570  ax-mulcl 9571  ax-mulrcl 9572  ax-mulcom 9573  ax-addass 9574  ax-mulass 9575  ax-distr 9576  ax-i2m1 9577  ax-1ne0 9578  ax-1rid 9579  ax-rnegex 9580  ax-rrecex 9581  ax-cnre 9582  ax-pre-lttri 9583  ax-pre-lttrn 9584  ax-pre-ltadd 9585  ax-pre-mulgt0 9586
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-eu 2287  df-mo 2288  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-nel 2655  df-ral 2812  df-rex 2813  df-reu 2814  df-rmo 2815  df-rab 2816  df-v 3111  df-sbc 3328  df-csb 3431  df-dif 3474  df-un 3476  df-in 3478  df-ss 3485  df-pss 3487  df-nul 3794  df-if 3945  df-pw 4017  df-sn 4033  df-pr 4035  df-tp 4037  df-op 4039  df-uni 4252  df-int 4289  df-iun 4334  df-br 4457  df-opab 4516  df-mpt 4517  df-tr 4551  df-eprel 4800  df-id 4804  df-po 4809  df-so 4810  df-fr 4847  df-we 4849  df-ord 4890  df-on 4891  df-lim 4892  df-suc 4893  df-xp 5014  df-rel 5015  df-cnv 5016  df-co 5017  df-dm 5018  df-rn 5019  df-res 5020  df-ima 5021  df-iota 5557  df-fun 5596  df-fn 5597  df-f 5598  df-f1 5599  df-fo 5600  df-f1o 5601  df-fv 5602  df-riota 6258  df-ov 6299  df-oprab 6300  df-mpt2 6301  df-of 6539  df-om 6700  df-1st 6799  df-2nd 6800  df-supp 6918  df-recs 7060  df-rdg 7094  df-1o 7148  df-oadd 7152  df-er 7329  df-map 7440  df-en 7536  df-dom 7537  df-sdom 7538  df-fin 7539  df-fsupp 7848  df-pnf 9647  df-mnf 9648  df-xr 9649  df-ltxr 9650  df-le 9651  df-sub 9826  df-neg 9827  df-nn 10557  df-2 10615  df-3 10616  df-4 10617  df-5 10618  df-6 10619  df-7 10620  df-8 10621  df-9 10622  df-n0 10817  df-z 10886  df-uz 11107  df-fz 11698  df-struct 14646  df-ndx 14647  df-slot 14648  df-base 14649  df-sets 14650  df-ress 14651  df-plusg 14725  df-mulr 14726  df-sca 14728  df-vsca 14729  df-tset 14731  df-0g 14859  df-mgm 15999  df-sgrp 16038  df-mnd 16048  df-grp 16184  df-minusg 16185  df-subg 16325  df-psr 18132
This theorem is referenced by:  mpllsslemOLD  18223
  Copyright terms: Public domain W3C validator