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

Theorem mplsubglem 16500
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.)
Hypotheses
Ref Expression
mplsubglem.s  |-  S  =  ( I mPwSer  R )
mplsubglem.b  |-  B  =  ( Base `  S
)
mplsubglem.z  |-  .0.  =  ( 0g `  R )
mplsubglem.d  |-  D  =  { f  e.  ( NN0  ^m  I )  |  ( `' f
" NN )  e. 
Fin }
mplsubglem.i  |-  ( ph  ->  I  e.  W )
mplsubglem.0  |-  ( ph  -> 
(/)  e.  A )
mplsubglem.a  |-  ( (
ph  /\  ( x  e.  A  /\  y  e.  A ) )  -> 
( x  u.  y
)  e.  A )
mplsubglem.y  |-  ( (
ph  /\  ( x  e.  A  /\  y  C_  x ) )  -> 
y  e.  A )
mplsubglem.u  |-  ( ph  ->  U  =  { g  e.  B  |  ( `' g " ( _V  \  {  .0.  }
) )  e.  A } )
mplsubglem.r  |-  ( ph  ->  R  e.  Grp )
Assertion
Ref Expression
mplsubglem  |-  ( 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 mplsubglem
Dummy variables  k  u  v are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 mplsubglem.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 3400 . 2  |-  ( ph  ->  U  C_  B )
4 mplsubglem.s . . . . 5  |-  S  =  ( I mPwSer  R )
5 mplsubglem.i . . . . 5  |-  ( ph  ->  I  e.  W )
6 mplsubglem.r . . . . 5  |-  ( ph  ->  R  e.  Grp )
7 mplsubglem.d . . . . 5  |-  D  =  { f  e.  ( NN0  ^m  I )  |  ( `' f
" NN )  e. 
Fin }
8 mplsubglem.z . . . . 5  |-  .0.  =  ( 0g `  R )
9 mplsubglem.b . . . . 5  |-  B  =  ( Base `  S
)
104, 5, 6, 7, 8, 9psr0cl 16460 . . . 4  |-  ( ph  ->  ( D  X.  {  .0.  } )  e.  B
)
11 eqid 2438 . . . . . . . . 9  |-  ( Base `  R )  =  (
Base `  R )
1211, 8grpidcl 14835 . . . . . . . 8  |-  ( R  e.  Grp  ->  .0.  e.  ( Base `  R
) )
13 fconst6g 5634 . . . . . . . 8  |-  (  .0. 
e.  ( Base `  R
)  ->  ( D  X.  {  .0.  } ) : D --> ( Base `  R ) )
146, 12, 133syl 19 . . . . . . 7  |-  ( ph  ->  ( D  X.  {  .0.  } ) : D --> ( Base `  R )
)
15 eldifi 3471 . . . . . . . . 9  |-  ( u  e.  ( D  \  (/) )  ->  u  e.  D )
16 fvex 5744 . . . . . . . . . . 11  |-  ( 0g
`  R )  e. 
_V
178, 16eqeltri 2508 . . . . . . . . . 10  |-  .0.  e.  _V
1817fvconst2 5949 . . . . . . . . 9  |-  ( u  e.  D  ->  (
( D  X.  {  .0.  } ) `  u
)  =  .0.  )
1915, 18syl 16 . . . . . . . 8  |-  ( u  e.  ( D  \  (/) )  ->  ( ( D  X.  {  .0.  }
) `  u )  =  .0.  )
2019adantl 454 . . . . . . 7  |-  ( (
ph  /\  u  e.  ( D  \  (/) ) )  ->  ( ( D  X.  {  .0.  }
) `  u )  =  .0.  )
2114, 20suppss 5865 . . . . . 6  |-  ( ph  ->  ( `' ( D  X.  {  .0.  }
) " ( _V 
\  {  .0.  }
) )  C_  (/) )
22 ss0 3660 . . . . . 6  |-  ( ( `' ( D  X.  {  .0.  } ) "
( _V  \  {  .0.  } ) )  C_  (/) 
->  ( `' ( D  X.  {  .0.  }
) " ( _V 
\  {  .0.  }
) )  =  (/) )
2321, 22syl 16 . . . . 5  |-  ( ph  ->  ( `' ( D  X.  {  .0.  }
) " ( _V 
\  {  .0.  }
) )  =  (/) )
24 mplsubglem.0 . . . . 5  |-  ( ph  -> 
(/)  e.  A )
2523, 24eqeltrd 2512 . . . 4  |-  ( ph  ->  ( `' ( D  X.  {  .0.  }
) " ( _V 
\  {  .0.  }
) )  e.  A
)
261eleq2d 2505 . . . . 5  |-  ( ph  ->  ( ( D  X.  {  .0.  } )  e.  U  <->  ( D  X.  {  .0.  } )  e. 
{ g  e.  B  |  ( `' g
" ( _V  \  {  .0.  } ) )  e.  A } ) )
27 cnveq 5048 . . . . . . . 8  |-  ( g  =  ( D  X.  {  .0.  } )  ->  `' g  =  `' ( D  X.  {  .0.  } ) )
2827imaeq1d 5204 . . . . . . 7  |-  ( g  =  ( D  X.  {  .0.  } )  -> 
( `' g "
( _V  \  {  .0.  } ) )  =  ( `' ( D  X.  {  .0.  }
) " ( _V 
\  {  .0.  }
) ) )
2928eleq1d 2504 . . . . . 6  |-  ( g  =  ( D  X.  {  .0.  } )  -> 
( ( `' g
" ( _V  \  {  .0.  } ) )  e.  A  <->  ( `' ( D  X.  {  .0.  } ) " ( _V 
\  {  .0.  }
) )  e.  A
) )
3029elrab 3094 . . . . 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 254 . . . 4  |-  ( ph  ->  ( ( D  X.  {  .0.  } )  e.  U  <->  ( ( D  X.  {  .0.  }
)  e.  B  /\  ( `' ( D  X.  {  .0.  } ) "
( _V  \  {  .0.  } ) )  e.  A ) ) )
3210, 25, 31mpbir2and 890 . . 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 2438 . . . . . . 7  |-  ( +g  `  S )  =  ( +g  `  S )
366ad2antrr 708 . . . . . . 7  |-  ( ( ( ph  /\  u  e.  U )  /\  v  e.  U )  ->  R  e.  Grp )
371eleq2d 2505 . . . . . . . . . . 11  |-  ( ph  ->  ( u  e.  U  <->  u  e.  { g  e.  B  |  ( `' g " ( _V 
\  {  .0.  }
) )  e.  A } ) )
38 cnveq 5048 . . . . . . . . . . . . . 14  |-  ( g  =  u  ->  `' g  =  `' u
)
3938imaeq1d 5204 . . . . . . . . . . . . 13  |-  ( g  =  u  ->  ( `' g " ( _V  \  {  .0.  }
) )  =  ( `' u " ( _V 
\  {  .0.  }
) ) )
4039eleq1d 2504 . . . . . . . . . . . 12  |-  ( g  =  u  ->  (
( `' g "
( _V  \  {  .0.  } ) )  e.  A  <->  ( `' u " ( _V  \  {  .0.  } ) )  e.  A ) )
4140elrab 3094 . . . . . . . . . . 11  |-  ( u  e.  { g  e.  B  |  ( `' g " ( _V 
\  {  .0.  }
) )  e.  A } 
<->  ( u  e.  B  /\  ( `' u "
( _V  \  {  .0.  } ) )  e.  A ) )
4237, 41syl6bb 254 . . . . . . . . . 10  |-  ( ph  ->  ( u  e.  U  <->  ( u  e.  B  /\  ( `' u " ( _V 
\  {  .0.  }
) )  e.  A
) ) )
4342biimpa 472 . . . . . . . . 9  |-  ( (
ph  /\  u  e.  U )  ->  (
u  e.  B  /\  ( `' u " ( _V 
\  {  .0.  }
) )  e.  A
) )
4443simpld 447 . . . . . . . 8  |-  ( (
ph  /\  u  e.  U )  ->  u  e.  B )
4544adantr 453 . . . . . . 7  |-  ( ( ( ph  /\  u  e.  U )  /\  v  e.  U )  ->  u  e.  B )
461adantr 453 . . . . . . . . . . 11  |-  ( (
ph  /\  u  e.  U )  ->  U  =  { g  e.  B  |  ( `' g
" ( _V  \  {  .0.  } ) )  e.  A } )
4746eleq2d 2505 . . . . . . . . . 10  |-  ( (
ph  /\  u  e.  U )  ->  (
v  e.  U  <->  v  e.  { g  e.  B  | 
( `' g "
( _V  \  {  .0.  } ) )  e.  A } ) )
48 cnveq 5048 . . . . . . . . . . . . 13  |-  ( g  =  v  ->  `' g  =  `' v
)
4948imaeq1d 5204 . . . . . . . . . . . 12  |-  ( g  =  v  ->  ( `' g " ( _V  \  {  .0.  }
) )  =  ( `' v " ( _V  \  {  .0.  }
) ) )
5049eleq1d 2504 . . . . . . . . . . 11  |-  ( g  =  v  ->  (
( `' g "
( _V  \  {  .0.  } ) )  e.  A  <->  ( `' v
" ( _V  \  {  .0.  } ) )  e.  A ) )
5150elrab 3094 . . . . . . . . . 10  |-  ( v  e.  { g  e.  B  |  ( `' g " ( _V 
\  {  .0.  }
) )  e.  A } 
<->  ( v  e.  B  /\  ( `' v "
( _V  \  {  .0.  } ) )  e.  A ) )
5247, 51syl6bb 254 . . . . . . . . 9  |-  ( (
ph  /\  u  e.  U )  ->  (
v  e.  U  <->  ( v  e.  B  /\  ( `' v " ( _V  \  {  .0.  }
) )  e.  A
) ) )
5352biimpa 472 . . . . . . . 8  |-  ( ( ( ph  /\  u  e.  U )  /\  v  e.  U )  ->  (
v  e.  B  /\  ( `' v " ( _V  \  {  .0.  }
) )  e.  A
) )
5453simpld 447 . . . . . . 7  |-  ( ( ( ph  /\  u  e.  U )  /\  v  e.  U )  ->  v  e.  B )
554, 9, 35, 36, 45, 54psraddcl 16449 . . . . . 6  |-  ( ( ( ph  /\  u  e.  U )  /\  v  e.  U )  ->  (
u ( +g  `  S
) v )  e.  B )
5643simprd 451 . . . . . . . . . 10  |-  ( (
ph  /\  u  e.  U )  ->  ( `' u " ( _V 
\  {  .0.  }
) )  e.  A
)
5756adantr 453 . . . . . . . . 9  |-  ( ( ( ph  /\  u  e.  U )  /\  v  e.  U )  ->  ( `' u " ( _V 
\  {  .0.  }
) )  e.  A
)
5853simprd 451 . . . . . . . . 9  |-  ( ( ( ph  /\  u  e.  U )  /\  v  e.  U )  ->  ( `' v " ( _V  \  {  .0.  }
) )  e.  A
)
59 mplsubglem.a . . . . . . . . . . 11  |-  ( (
ph  /\  ( x  e.  A  /\  y  e.  A ) )  -> 
( x  u.  y
)  e.  A )
6059ralrimivva 2800 . . . . . . . . . 10  |-  ( ph  ->  A. x  e.  A  A. y  e.  A  ( x  u.  y
)  e.  A )
6160ad2antrr 708 . . . . . . . . 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 2504 . . . . . . . . . 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 2504 . . . . . . . . . 10  |-  ( y  =  ( `' v
" ( _V  \  {  .0.  } ) )  ->  ( ( ( `' u " ( _V 
\  {  .0.  }
) )  u.  y
)  e.  A  <->  ( ( `' u " ( _V 
\  {  .0.  }
) )  u.  ( `' v " ( _V  \  {  .0.  }
) ) )  e.  A ) )
6663, 65rspc2va 3061 . . . . . . . . 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 1184 . . . . . . . 8  |-  ( ( ( ph  /\  u  e.  U )  /\  v  e.  U )  ->  (
( `' u "
( _V  \  {  .0.  } ) )  u.  ( `' v "
( _V  \  {  .0.  } ) ) )  e.  A )
684, 11, 7, 9, 55psrelbas 16446 . . . . . . . . 9  |-  ( ( ( ph  /\  u  e.  U )  /\  v  e.  U )  ->  (
u ( +g  `  S
) v ) : D --> ( Base `  R
) )
69 eqid 2438 . . . . . . . . . . . . 13  |-  ( +g  `  R )  =  ( +g  `  R )
704, 9, 69, 35, 45, 54psradd 16448 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  u  e.  U )  /\  v  e.  U )  ->  (
u ( +g  `  S
) v )  =  ( u  o F ( +g  `  R
) v ) )
7170fveq1d 5732 . . . . . . . . . . 11  |-  ( ( ( ph  /\  u  e.  U )  /\  v  e.  U )  ->  (
( u ( +g  `  S ) v ) `
 k )  =  ( ( u  o F ( +g  `  R
) v ) `  k ) )
7271adantr 453 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  u  e.  U )  /\  v  e.  U
)  /\  k  e.  ( D  \  (
( `' u "
( _V  \  {  .0.  } ) )  u.  ( `' v "
( _V  \  {  .0.  } ) ) ) ) )  ->  (
( u ( +g  `  S ) v ) `
 k )  =  ( ( u  o F ( +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 16446 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  u  e.  U )  ->  u : D --> ( Base `  R
) )
7574adantr 453 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  u  e.  U )  /\  v  e.  U )  ->  u : D --> ( Base `  R
) )
76 ffn 5593 . . . . . . . . . . . . 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 16446 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  u  e.  U )  /\  v  e.  U )  ->  v : D --> ( Base `  R
) )
79 ffn 5593 . . . . . . . . . . . . 13  |-  ( v : D --> ( Base `  R )  ->  v  Fn  D )
8078, 79syl 16 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  u  e.  U )  /\  v  e.  U )  ->  v  Fn  D )
81 ovex 6108 . . . . . . . . . . . . . . 15  |-  ( NN0 
^m  I )  e. 
_V
8281rabex 4356 . . . . . . . . . . . . . 14  |-  { f  e.  ( NN0  ^m  I )  |  ( `' f " NN )  e.  Fin }  e.  _V
837, 82eqeltri 2508 . . . . . . . . . . . . 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 2439 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  u  e.  U )  /\  v  e.  U
)  /\  k  e.  D )  ->  (
u `  k )  =  ( u `  k ) )
87 eqidd 2439 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  u  e.  U )  /\  v  e.  U
)  /\  k  e.  D )  ->  (
v `  k )  =  ( v `  k ) )
8877, 80, 84, 84, 85, 86, 87ofval 6316 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  u  e.  U )  /\  v  e.  U
)  /\  k  e.  D )  ->  (
( u  o F ( +g  `  R
) v ) `  k )  =  ( ( u `  k
) ( +g  `  R
) ( v `  k ) ) )
8973, 88sylan2 462 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  u  e.  U )  /\  v  e.  U
)  /\  k  e.  ( D  \  (
( `' u "
( _V  \  {  .0.  } ) )  u.  ( `' v "
( _V  \  {  .0.  } ) ) ) ) )  ->  (
( u  o F ( +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 8 . . . . . . . . . . . . . 14  |-  ( D 
\  ( ( `' u " ( _V 
\  {  .0.  }
) )  u.  ( `' v " ( _V  \  {  .0.  }
) ) ) ) 
C_  ( D  \ 
( `' u "
( _V  \  {  .0.  } ) ) )
9392sseli 3346 . . . . . . . . . . . . 13  |-  ( k  e.  ( D  \ 
( ( `' u " ( _V  \  {  .0.  } ) )  u.  ( `' v "
( _V  \  {  .0.  } ) ) ) )  ->  k  e.  ( D  \  ( `' u " ( _V 
\  {  .0.  }
) ) ) )
94 ssid 3369 . . . . . . . . . . . . . . . 16  |-  ( `' u " ( _V 
\  {  .0.  }
) )  C_  ( `' u " ( _V 
\  {  .0.  }
) )
9594a1i 11 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  u  e.  U )  ->  ( `' u " ( _V 
\  {  .0.  }
) )  C_  ( `' u " ( _V 
\  {  .0.  }
) ) )
9674, 95suppssr 5866 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  u  e.  U )  /\  k  e.  ( D  \  ( `' u " ( _V 
\  {  .0.  }
) ) ) )  ->  ( u `  k )  =  .0.  )
9796adantlr 697 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  u  e.  U )  /\  v  e.  U
)  /\  k  e.  ( D  \  ( `' u " ( _V 
\  {  .0.  }
) ) ) )  ->  ( u `  k )  =  .0.  )
9893, 97sylan2 462 . . . . . . . . . . . 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 8 . . . . . . . . . . . . . 14  |-  ( D 
\  ( ( `' u " ( _V 
\  {  .0.  }
) )  u.  ( `' v " ( _V  \  {  .0.  }
) ) ) ) 
C_  ( D  \ 
( `' v "
( _V  \  {  .0.  } ) ) )
102101sseli 3346 . . . . . . . . . . . . 13  |-  ( k  e.  ( D  \ 
( ( `' u " ( _V  \  {  .0.  } ) )  u.  ( `' v "
( _V  \  {  .0.  } ) ) ) )  ->  k  e.  ( D  \  ( `' v " ( _V  \  {  .0.  }
) ) ) )
103 ssid 3369 . . . . . . . . . . . . . . 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, 104suppssr 5866 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  u  e.  U )  /\  v  e.  U
)  /\  k  e.  ( D  \  ( `' v " ( _V  \  {  .0.  }
) ) ) )  ->  ( v `  k )  =  .0.  )
106102, 105sylan2 462 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  u  e.  U )  /\  v  e.  U
)  /\  k  e.  ( D  \  (
( `' u "
( _V  \  {  .0.  } ) )  u.  ( `' v "
( _V  \  {  .0.  } ) ) ) ) )  ->  (
v `  k )  =  .0.  )
10798, 106oveq12d 6101 . . . . . . . . . . 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 14837 . . . . . . . . . . . . . 14  |-  ( ( R  e.  Grp  /\  .0.  e.  ( Base `  R
) )  ->  (  .0.  ( +g  `  R
)  .0.  )  =  .0.  )
10912, 108mpdan 651 . . . . . . . . . . . . 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 453 . . . . . . . . . . 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 2470 . . . . . . . . . 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 2474 . . . . . . . . 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, 113suppss 5865 . . . . . . . 8  |-  ( ( ( ph  /\  u  e.  U )  /\  v  e.  U )  ->  ( `' ( u ( +g  `  S ) v ) " ( _V  \  {  .0.  }
) )  C_  (
( `' u "
( _V  \  {  .0.  } ) )  u.  ( `' v "
( _V  \  {  .0.  } ) ) ) )
11567, 114ssexd 4352 . . . . . . 7  |-  ( ( ( ph  /\  u  e.  U )  /\  v  e.  U )  ->  ( `' ( u ( +g  `  S ) v ) " ( _V  \  {  .0.  }
) )  e.  _V )
116 mplsubglem.y . . . . . . . . . . . 12  |-  ( (
ph  /\  ( x  e.  A  /\  y  C_  x ) )  -> 
y  e.  A )
117116expr 600 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  A )  ->  (
y  C_  x  ->  y  e.  A ) )
118117alrimiv 1642 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  A )  ->  A. y
( y  C_  x  ->  y  e.  A ) )
119118ralrimiva 2791 . . . . . . . . 9  |-  ( ph  ->  A. x  e.  A  A. y ( y  C_  x  ->  y  e.  A
) )
120119ad2antrr 708 . . . . . . . 8  |-  ( ( ( ph  /\  u  e.  U )  /\  v  e.  U )  ->  A. x  e.  A  A. y
( y  C_  x  ->  y  e.  A ) )
121 sseq2 3372 . . . . . . . . . . 11  |-  ( x  =  ( ( `' u " ( _V 
\  {  .0.  }
) )  u.  ( `' v " ( _V  \  {  .0.  }
) ) )  -> 
( y  C_  x  <->  y 
C_  ( ( `' u " ( _V 
\  {  .0.  }
) )  u.  ( `' v " ( _V  \  {  .0.  }
) ) ) ) )
122121imbi1d 310 . . . . . . . . . 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 1636 . . . . . . . . 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 3050 . . . . . . . 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 59 . . . . . . 7  |-  ( ( ( ph  /\  u  e.  U )  /\  v  e.  U )  ->  A. y
( y  C_  (
( `' u "
( _V  \  {  .0.  } ) )  u.  ( `' v "
( _V  \  {  .0.  } ) ) )  ->  y  e.  A
) )
126 sseq1 3371 . . . . . . . . 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 2498 . . . . . . . . 9  |-  ( y  =  ( `' ( u ( +g  `  S
) v ) "
( _V  \  {  .0.  } ) )  -> 
( y  e.  A  <->  ( `' ( u ( +g  `  S ) v ) " ( _V  \  {  .0.  }
) )  e.  A
) )
128126, 127imbi12d 313 . . . . . . . 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 3038 . . . . . . 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 60 . . . . . 6  |-  ( ( ( ph  /\  u  e.  U )  /\  v  e.  U )  ->  ( `' ( u ( +g  `  S ) v ) " ( _V  \  {  .0.  }
) )  e.  A
)
1311ad2antrr 708 . . . . . . . 8  |-  ( ( ( ph  /\  u  e.  U )  /\  v  e.  U )  ->  U  =  { g  e.  B  |  ( `' g
" ( _V  \  {  .0.  } ) )  e.  A } )
132131eleq2d 2505 . . . . . . 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 5048 . . . . . . . . . 10  |-  ( g  =  ( u ( +g  `  S ) v )  ->  `' g  =  `' (
u ( +g  `  S
) v ) )
134133imaeq1d 5204 . . . . . . . . 9  |-  ( g  =  ( u ( +g  `  S ) v )  ->  ( `' g " ( _V  \  {  .0.  }
) )  =  ( `' ( u ( +g  `  S ) v ) " ( _V  \  {  .0.  }
) ) )
135134eleq1d 2504 . . . . . . . 8  |-  ( g  =  ( u ( +g  `  S ) v )  ->  (
( `' g "
( _V  \  {  .0.  } ) )  e.  A  <->  ( `' ( u ( +g  `  S
) v ) "
( _V  \  {  .0.  } ) )  e.  A ) )
136135elrab 3094 . . . . . . 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 254 . . . . . 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 890 . . . . 5  |-  ( ( ( ph  /\  u  e.  U )  /\  v  e.  U )  ->  (
u ( +g  `  S
) v )  e.  U )
139138ralrimiva 2791 . . . 4  |-  ( (
ph  /\  u  e.  U )  ->  A. v  e.  U  ( u
( +g  `  S ) v )  e.  U
)
1404, 5, 6psrgrp 16464 . . . . . . 7  |-  ( ph  ->  S  e.  Grp )
141 eqid 2438 . . . . . . . 8  |-  ( inv g `  S )  =  ( inv g `  S )
1429, 141grpinvcl 14852 . . . . . . 7  |-  ( ( S  e.  Grp  /\  u  e.  B )  ->  ( ( inv g `  S ) `  u
)  e.  B )
143140, 142sylan 459 . . . . . 6  |-  ( (
ph  /\  u  e.  B )  ->  (
( inv g `  S ) `  u
)  e.  B )
14444, 143syldan 458 . . . . 5  |-  ( (
ph  /\  u  e.  U )  ->  (
( inv g `  S ) `  u
)  e.  B )
1454, 11, 7, 9, 144psrelbas 16446 . . . . . . . 8  |-  ( (
ph  /\  u  e.  U )  ->  (
( inv g `  S ) `  u
) : D --> ( Base `  R ) )
1465adantr 453 . . . . . . . . . . . 12  |-  ( (
ph  /\  u  e.  U )  ->  I  e.  W )
1476adantr 453 . . . . . . . . . . . 12  |-  ( (
ph  /\  u  e.  U )  ->  R  e.  Grp )
148 eqid 2438 . . . . . . . . . . . 12  |-  ( inv g `  R )  =  ( inv g `  R )
1494, 146, 147, 7, 148, 9, 141, 44psrneg 16466 . . . . . . . . . . 11  |-  ( (
ph  /\  u  e.  U )  ->  (
( inv g `  S ) `  u
)  =  ( ( inv g `  R
)  o.  u ) )
150149adantr 453 . . . . . . . . . 10  |-  ( ( ( ph  /\  u  e.  U )  /\  k  e.  ( D  \  ( `' u " ( _V 
\  {  .0.  }
) ) ) )  ->  ( ( inv g `  S ) `
 u )  =  ( ( inv g `  R )  o.  u
) )
151150fveq1d 5732 . . . . . . . . 9  |-  ( ( ( ph  /\  u  e.  U )  /\  k  e.  ( D  \  ( `' u " ( _V 
\  {  .0.  }
) ) ) )  ->  ( ( ( inv g `  S
) `  u ) `  k )  =  ( ( ( inv g `  R )  o.  u
) `  k )
)
152 eldifi 3471 . . . . . . . . . 10  |-  ( k  e.  ( D  \ 
( `' u "
( _V  \  {  .0.  } ) ) )  ->  k  e.  D
)
153 fvco3 5802 . . . . . . . . . 10  |-  ( ( u : D --> ( Base `  R )  /\  k  e.  D )  ->  (
( ( inv g `  R )  o.  u
) `  k )  =  ( ( inv g `  R ) `
 ( u `  k ) ) )
15474, 152, 153syl2an 465 . . . . . . . . 9  |-  ( ( ( ph  /\  u  e.  U )  /\  k  e.  ( D  \  ( `' u " ( _V 
\  {  .0.  }
) ) ) )  ->  ( ( ( inv g `  R
)  o.  u ) `
 k )  =  ( ( inv g `  R ) `  (
u `  k )
) )
15596fveq2d 5734 . . . . . . . . . 10  |-  ( ( ( ph  /\  u  e.  U )  /\  k  e.  ( D  \  ( `' u " ( _V 
\  {  .0.  }
) ) ) )  ->  ( ( inv g `  R ) `
 ( u `  k ) )  =  ( ( inv g `  R ) `  .0.  ) )
1568, 148grpinvid 14858 . . . . . . . . . . . 12  |-  ( R  e.  Grp  ->  (
( inv g `  R ) `  .0.  )  =  .0.  )
157147, 156syl 16 . . . . . . . . . . 11  |-  ( (
ph  /\  u  e.  U )  ->  (
( inv g `  R ) `  .0.  )  =  .0.  )
158157adantr 453 . . . . . . . . . 10  |-  ( ( ( ph  /\  u  e.  U )  /\  k  e.  ( D  \  ( `' u " ( _V 
\  {  .0.  }
) ) ) )  ->  ( ( inv g `  R ) `
 .0.  )  =  .0.  )
159155, 158eqtrd 2470 . . . . . . . . 9  |-  ( ( ( ph  /\  u  e.  U )  /\  k  e.  ( D  \  ( `' u " ( _V 
\  {  .0.  }
) ) ) )  ->  ( ( inv g `  R ) `
 ( u `  k ) )  =  .0.  )
160151, 154, 1593eqtrd 2474 . . . . . . . 8  |-  ( ( ( ph  /\  u  e.  U )  /\  k  e.  ( D  \  ( `' u " ( _V 
\  {  .0.  }
) ) ) )  ->  ( ( ( inv g `  S
) `  u ) `  k )  =  .0.  )
161145, 160suppss 5865 . . . . . . 7  |-  ( (
ph  /\  u  e.  U )  ->  ( `' ( ( inv g `  S ) `
 u ) "
( _V  \  {  .0.  } ) )  C_  ( `' u " ( _V 
\  {  .0.  }
) ) )
16256, 161ssexd 4352 . . . . . 6  |-  ( (
ph  /\  u  e.  U )  ->  ( `' ( ( inv g `  S ) `
 u ) "
( _V  \  {  .0.  } ) )  e. 
_V )
163119adantr 453 . . . . . . 7  |-  ( (
ph  /\  u  e.  U )  ->  A. x  e.  A  A. y
( y  C_  x  ->  y  e.  A ) )
164 sseq2 3372 . . . . . . . . . 10  |-  ( x  =  ( `' u " ( _V  \  {  .0.  } ) )  -> 
( y  C_  x  <->  y 
C_  ( `' u " ( _V  \  {  .0.  } ) ) ) )
165164imbi1d 310 . . . . . . . . 9  |-  ( x  =  ( `' u " ( _V  \  {  .0.  } ) )  -> 
( ( y  C_  x  ->  y  e.  A
)  <->  ( y  C_  ( `' u " ( _V 
\  {  .0.  }
) )  ->  y  e.  A ) ) )
166165albidv 1636 . . . . . . . 8  |-  ( x  =  ( `' u " ( _V  \  {  .0.  } ) )  -> 
( A. y ( y  C_  x  ->  y  e.  A )  <->  A. y
( y  C_  ( `' u " ( _V 
\  {  .0.  }
) )  ->  y  e.  A ) ) )
167166rspcv 3050 . . . . . . 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 59 . . . . . 6  |-  ( (
ph  /\  u  e.  U )  ->  A. y
( y  C_  ( `' u " ( _V 
\  {  .0.  }
) )  ->  y  e.  A ) )
169 sseq1 3371 . . . . . . . 8  |-  ( y  =  ( `' ( ( inv g `  S ) `  u
) " ( _V 
\  {  .0.  }
) )  ->  (
y  C_  ( `' u " ( _V  \  {  .0.  } ) )  <-> 
( `' ( ( inv g `  S
) `  u ) " ( _V  \  {  .0.  } ) ) 
C_  ( `' u " ( _V  \  {  .0.  } ) ) ) )
170 eleq1 2498 . . . . . . . 8  |-  ( y  =  ( `' ( ( inv g `  S ) `  u
) " ( _V 
\  {  .0.  }
) )  ->  (
y  e.  A  <->  ( `' ( ( inv g `  S ) `  u
) " ( _V 
\  {  .0.  }
) )  e.  A
) )
171169, 170imbi12d 313 . . . . . . 7  |-  ( y  =  ( `' ( ( inv g `  S ) `  u
) " ( _V 
\  {  .0.  }
) )  ->  (
( y  C_  ( `' u " ( _V 
\  {  .0.  }
) )  ->  y  e.  A )  <->  ( ( `' ( ( inv g `  S ) `
 u ) "
( _V  \  {  .0.  } ) )  C_  ( `' u " ( _V 
\  {  .0.  }
) )  ->  ( `' ( ( inv g `  S ) `
 u ) "
( _V  \  {  .0.  } ) )  e.  A ) ) )
172171spcgv 3038 . . . . . 6  |-  ( ( `' ( ( inv g `  S ) `
 u ) "
( _V  \  {  .0.  } ) )  e. 
_V  ->  ( A. y
( y  C_  ( `' u " ( _V 
\  {  .0.  }
) )  ->  y  e.  A )  ->  (
( `' ( ( inv g `  S
) `  u ) " ( _V  \  {  .0.  } ) ) 
C_  ( `' u " ( _V  \  {  .0.  } ) )  -> 
( `' ( ( inv g `  S
) `  u ) " ( _V  \  {  .0.  } ) )  e.  A ) ) )
173162, 168, 161, 172syl3c 60 . . . . 5  |-  ( (
ph  /\  u  e.  U )  ->  ( `' ( ( inv g `  S ) `
 u ) "
( _V  \  {  .0.  } ) )  e.  A )
17446eleq2d 2505 . . . . . 6  |-  ( (
ph  /\  u  e.  U )  ->  (
( ( inv g `  S ) `  u
)  e.  U  <->  ( ( inv g `  S ) `
 u )  e. 
{ g  e.  B  |  ( `' g
" ( _V  \  {  .0.  } ) )  e.  A } ) )
175 cnveq 5048 . . . . . . . . 9  |-  ( g  =  ( ( inv g `  S ) `
 u )  ->  `' g  =  `' ( ( inv g `  S ) `  u
) )
176175imaeq1d 5204 . . . . . . . 8  |-  ( g  =  ( ( inv g `  S ) `
 u )  -> 
( `' g "
( _V  \  {  .0.  } ) )  =  ( `' ( ( inv g `  S
) `  u ) " ( _V  \  {  .0.  } ) ) )
177176eleq1d 2504 . . . . . . 7  |-  ( g  =  ( ( inv g `  S ) `
 u )  -> 
( ( `' g
" ( _V  \  {  .0.  } ) )  e.  A  <->  ( `' ( ( inv g `  S ) `  u
) " ( _V 
\  {  .0.  }
) )  e.  A
) )
178177elrab 3094 . . . . . 6  |-  ( ( ( inv g `  S ) `  u
)  e.  { g  e.  B  |  ( `' g " ( _V  \  {  .0.  }
) )  e.  A } 
<->  ( ( ( inv g `  S ) `
 u )  e.  B  /\  ( `' ( ( inv g `  S ) `  u
) " ( _V 
\  {  .0.  }
) )  e.  A
) )
179174, 178syl6bb 254 . . . . 5  |-  ( (
ph  /\  u  e.  U )  ->  (
( ( inv g `  S ) `  u
)  e.  U  <->  ( (
( inv g `  S ) `  u
)  e.  B  /\  ( `' ( ( inv g `  S ) `
 u ) "
( _V  \  {  .0.  } ) )  e.  A ) ) )
180144, 173, 179mpbir2and 890 . . . 4  |-  ( (
ph  /\  u  e.  U )  ->  (
( inv g `  S ) `  u
)  e.  U )
181139, 180jca 520 . . 3  |-  ( (
ph  /\  u  e.  U )  ->  ( A. v  e.  U  ( u ( +g  `  S ) v )  e.  U  /\  (
( inv g `  S ) `  u
)  e.  U ) )
182181ralrimiva 2791 . 2  |-  ( ph  ->  A. u  e.  U  ( A. v  e.  U  ( u ( +g  `  S ) v )  e.  U  /\  (
( inv g `  S ) `  u
)  e.  U ) )
1839, 35, 141issubg2 14961 . . 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  /\  (
( inv g `  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  /\  ( ( inv g `  S ) `  u
)  e.  U ) ) ) )
1853, 34, 182, 184mpbir3and 1138 1  |-  ( ph  ->  U  e.  (SubGrp `  S ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178    /\ wa 360    /\ w3a 937   A.wal 1550    = wceq 1653    e. wcel 1726    =/= wne 2601   A.wral 2707   {crab 2711   _Vcvv 2958    \ cdif 3319    u. cun 3320    C_ wss 3322   (/)c0 3630   {csn 3816    X. cxp 4878   `'ccnv 4879   "cima 4883    o. ccom 4884    Fn wfn 5451   -->wf 5452   ` cfv 5456  (class class class)co 6083    o Fcof 6305    ^m cmap 7020   Fincfn 7111   NNcn 10002   NN0cn0 10223   Basecbs 13471   +g cplusg 13531   0gc0g 13725   Grpcgrp 14687   inv gcminusg 14688  SubGrpcsubg 14940   mPwSer cmps 16408
This theorem is referenced by:  mpllsslem  16501  mplsubg  16502
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-13 1728  ax-14 1730  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419  ax-rep 4322  ax-sep 4332  ax-nul 4340  ax-pow 4379  ax-pr 4405  ax-un 4703  ax-cnex 9048  ax-resscn 9049  ax-1cn 9050  ax-icn 9051  ax-addcl 9052  ax-addrcl 9053  ax-mulcl 9054  ax-mulrcl 9055  ax-mulcom 9056  ax-addass 9057  ax-mulass 9058  ax-distr 9059  ax-i2m1 9060  ax-1ne0 9061  ax-1rid 9062  ax-rnegex 9063  ax-rrecex 9064  ax-cnre 9065  ax-pre-lttri 9066  ax-pre-lttrn 9067  ax-pre-ltadd 9068  ax-pre-mulgt0 9069
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 938  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2287  df-mo 2288  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-nel 2604  df-ral 2712  df-rex 2713  df-reu 2714  df-rmo 2715  df-rab 2716  df-v 2960  df-sbc 3164  df-csb 3254  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-pss 3338  df-nul 3631  df-if 3742  df-pw 3803  df-sn 3822  df-pr 3823  df-tp 3824  df-op 3825  df-uni 4018  df-int 4053  df-iun 4097  df-br 4215  df-opab 4269  df-mpt 4270  df-tr 4305  df-eprel 4496  df-id 4500  df-po 4505  df-so 4506  df-fr 4543  df-we 4545  df-ord 4586  df-on 4587  df-lim 4588  df-suc 4589  df-om 4848  df-xp 4886  df-rel 4887  df-cnv 4888  df-co 4889  df-dm 4890  df-rn 4891  df-res 4892  df-ima 4893  df-iota 5420  df-fun 5458  df-fn 5459  df-f 5460  df-f1 5461  df-fo 5462  df-f1o 5463  df-fv 5464  df-ov 6086  df-oprab 6087  df-mpt2 6088  df-of 6307  df-1st 6351  df-2nd 6352  df-riota 6551  df-recs 6635  df-rdg 6670  df-1o 6726  df-oadd 6730  df-er 6907  df-map 7022  df-en 7112  df-dom 7113  df-sdom 7114  df-fin 7115  df-pnf 9124  df-mnf 9125  df-xr 9126  df-ltxr 9127  df-le 9128  df-sub 9295  df-neg 9296  df-nn 10003  df-2 10060  df-3 10061  df-4 10062  df-5 10063  df-6 10064  df-7 10065  df-8 10066  df-9 10067  df-n0 10224  df-z 10285  df-uz 10491  df-fz 11046  df-struct 13473  df-ndx 13474  df-slot 13475  df-base 13476  df-sets 13477  df-ress 13478  df-plusg 13544  df-mulr 13545  df-sca 13547  df-vsca 13548  df-tset 13550  df-0g 13729  df-mnd 14692  df-grp 14814  df-minusg 14815  df-subg 14943  df-psr 16419
  Copyright terms: Public domain W3C validator