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

Theorem mplsubglem 16453
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 3388 . . 3  |-  { g  e.  B  |  ( `' g " ( _V  \  {  .0.  }
) )  e.  A }  C_  B
31, 2syl6eqss 3358 . 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 16413 . . . 4  |-  ( ph  ->  ( D  X.  {  .0.  } )  e.  B
)
11 eqid 2404 . . . . . . . . 9  |-  ( Base `  R )  =  (
Base `  R )
1211, 8grpidcl 14788 . . . . . . . 8  |-  ( R  e.  Grp  ->  .0.  e.  ( Base `  R
) )
13 fconst6g 5591 . . . . . . . 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 3429 . . . . . . . . 9  |-  ( u  e.  ( D  \  (/) )  ->  u  e.  D )
16 fvex 5701 . . . . . . . . . . 11  |-  ( 0g
`  R )  e. 
_V
178, 16eqeltri 2474 . . . . . . . . . 10  |-  .0.  e.  _V
1817fvconst2 5906 . . . . . . . . 9  |-  ( u  e.  D  ->  (
( D  X.  {  .0.  } ) `  u
)  =  .0.  )
1915, 18syl 16 . . . . . . . 8  |-  ( u  e.  ( D  \  (/) )  ->  ( ( D  X.  {  .0.  }
) `  u )  =  .0.  )
2019adantl 453 . . . . . . 7  |-  ( (
ph  /\  u  e.  ( D  \  (/) ) )  ->  ( ( D  X.  {  .0.  }
) `  u )  =  .0.  )
2114, 20suppss 5822 . . . . . 6  |-  ( ph  ->  ( `' ( D  X.  {  .0.  }
) " ( _V 
\  {  .0.  }
) )  C_  (/) )
22 ss0 3618 . . . . . 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 2478 . . . 4  |-  ( ph  ->  ( `' ( D  X.  {  .0.  }
) " ( _V 
\  {  .0.  }
) )  e.  A
)
261eleq2d 2471 . . . . 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 2470 . . . . . 6  |-  ( g  =  ( D  X.  {  .0.  } )  -> 
( ( `' g
" ( _V  \  {  .0.  } ) )  e.  A  <->  ( `' ( D  X.  {  .0.  } ) " ( _V 
\  {  .0.  }
) )  e.  A
) )
3029elrab 3052 . . . . 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 253 . . . 4  |-  ( ph  ->  ( ( D  X.  {  .0.  } )  e.  U  <->  ( ( D  X.  {  .0.  }
)  e.  B  /\  ( `' ( D  X.  {  .0.  } ) "
( _V  \  {  .0.  } ) )  e.  A ) ) )
3210, 25, 31mpbir2and 889 . . 3  |-  ( ph  ->  ( D  X.  {  .0.  } )  e.  U
)
33 ne0i 3594 . . 3  |-  ( ( D  X.  {  .0.  } )  e.  U  ->  U  =/=  (/) )
3432, 33syl 16 . 2  |-  ( ph  ->  U  =/=  (/) )
35 eqid 2404 . . . . . . 7  |-  ( +g  `  S )  =  ( +g  `  S )
366ad2antrr 707 . . . . . . 7  |-  ( ( ( ph  /\  u  e.  U )  /\  v  e.  U )  ->  R  e.  Grp )
371eleq2d 2471 . . . . . . . . . . 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 2470 . . . . . . . . . . . 12  |-  ( g  =  u  ->  (
( `' g "
( _V  \  {  .0.  } ) )  e.  A  <->  ( `' u " ( _V  \  {  .0.  } ) )  e.  A ) )
4140elrab 3052 . . . . . . . . . . 11  |-  ( u  e.  { g  e.  B  |  ( `' g " ( _V 
\  {  .0.  }
) )  e.  A } 
<->  ( u  e.  B  /\  ( `' u "
( _V  \  {  .0.  } ) )  e.  A ) )
4237, 41syl6bb 253 . . . . . . . . . 10  |-  ( ph  ->  ( u  e.  U  <->  ( u  e.  B  /\  ( `' u " ( _V 
\  {  .0.  }
) )  e.  A
) ) )
4342biimpa 471 . . . . . . . . 9  |-  ( (
ph  /\  u  e.  U )  ->  (
u  e.  B  /\  ( `' u " ( _V 
\  {  .0.  }
) )  e.  A
) )
4443simpld 446 . . . . . . . 8  |-  ( (
ph  /\  u  e.  U )  ->  u  e.  B )
4544adantr 452 . . . . . . 7  |-  ( ( ( ph  /\  u  e.  U )  /\  v  e.  U )  ->  u  e.  B )
461adantr 452 . . . . . . . . . . 11  |-  ( (
ph  /\  u  e.  U )  ->  U  =  { g  e.  B  |  ( `' g
" ( _V  \  {  .0.  } ) )  e.  A } )
4746eleq2d 2471 . . . . . . . . . 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 2470 . . . . . . . . . . 11  |-  ( g  =  v  ->  (
( `' g "
( _V  \  {  .0.  } ) )  e.  A  <->  ( `' v
" ( _V  \  {  .0.  } ) )  e.  A ) )
5150elrab 3052 . . . . . . . . . 10  |-  ( v  e.  { g  e.  B  |  ( `' g " ( _V 
\  {  .0.  }
) )  e.  A } 
<->  ( v  e.  B  /\  ( `' v "
( _V  \  {  .0.  } ) )  e.  A ) )
5247, 51syl6bb 253 . . . . . . . . 9  |-  ( (
ph  /\  u  e.  U )  ->  (
v  e.  U  <->  ( v  e.  B  /\  ( `' v " ( _V  \  {  .0.  }
) )  e.  A
) ) )
5352biimpa 471 . . . . . . . 8  |-  ( ( ( ph  /\  u  e.  U )  /\  v  e.  U )  ->  (
v  e.  B  /\  ( `' v " ( _V  \  {  .0.  }
) )  e.  A
) )
5453simpld 446 . . . . . . 7  |-  ( ( ( ph  /\  u  e.  U )  /\  v  e.  U )  ->  v  e.  B )
554, 9, 35, 36, 45, 54psraddcl 16402 . . . . . 6  |-  ( ( ( ph  /\  u  e.  U )  /\  v  e.  U )  ->  (
u ( +g  `  S
) v )  e.  B )
5643simprd 450 . . . . . . . . . 10  |-  ( (
ph  /\  u  e.  U )  ->  ( `' u " ( _V 
\  {  .0.  }
) )  e.  A
)
5756adantr 452 . . . . . . . . 9  |-  ( ( ( ph  /\  u  e.  U )  /\  v  e.  U )  ->  ( `' u " ( _V 
\  {  .0.  }
) )  e.  A
)
5853simprd 450 . . . . . . . . 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 2758 . . . . . . . . . 10  |-  ( ph  ->  A. x  e.  A  A. y  e.  A  ( x  u.  y
)  e.  A )
6160ad2antrr 707 . . . . . . . . 9  |-  ( ( ( ph  /\  u  e.  U )  /\  v  e.  U )  ->  A. x  e.  A  A. y  e.  A  ( x  u.  y )  e.  A
)
62 uneq1 3454 . . . . . . . . . . 11  |-  ( x  =  ( `' u " ( _V  \  {  .0.  } ) )  -> 
( x  u.  y
)  =  ( ( `' u " ( _V 
\  {  .0.  }
) )  u.  y
) )
6362eleq1d 2470 . . . . . . . . . 10  |-  ( x  =  ( `' u " ( _V  \  {  .0.  } ) )  -> 
( ( x  u.  y )  e.  A  <->  ( ( `' u "
( _V  \  {  .0.  } ) )  u.  y )  e.  A
) )
64 uneq2 3455 . . . . . . . . . . 11  |-  ( y  =  ( `' v
" ( _V  \  {  .0.  } ) )  ->  ( ( `' u " ( _V 
\  {  .0.  }
) )  u.  y
)  =  ( ( `' u " ( _V 
\  {  .0.  }
) )  u.  ( `' v " ( _V  \  {  .0.  }
) ) ) )
6564eleq1d 2470 . . . . . . . . . 10  |-  ( y  =  ( `' v
" ( _V  \  {  .0.  } ) )  ->  ( ( ( `' u " ( _V 
\  {  .0.  }
) )  u.  y
)  e.  A  <->  ( ( `' u " ( _V 
\  {  .0.  }
) )  u.  ( `' v " ( _V  \  {  .0.  }
) ) )  e.  A ) )
6663, 65rspc2va 3019 . . . . . . . . 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 1183 . . . . . . . 8  |-  ( ( ( ph  /\  u  e.  U )  /\  v  e.  U )  ->  (
( `' u "
( _V  \  {  .0.  } ) )  u.  ( `' v "
( _V  \  {  .0.  } ) ) )  e.  A )
684, 11, 7, 9, 55psrelbas 16399 . . . . . . . . 9  |-  ( ( ( ph  /\  u  e.  U )  /\  v  e.  U )  ->  (
u ( +g  `  S
) v ) : D --> ( Base `  R
) )
69 eqid 2404 . . . . . . . . . . . . 13  |-  ( +g  `  R )  =  ( +g  `  R )
704, 9, 69, 35, 45, 54psradd 16401 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  u  e.  U )  /\  v  e.  U )  ->  (
u ( +g  `  S
) v )  =  ( u  o F ( +g  `  R
) v ) )
7170fveq1d 5689 . . . . . . . . . . 11  |-  ( ( ( ph  /\  u  e.  U )  /\  v  e.  U )  ->  (
( u ( +g  `  S ) v ) `
 k )  =  ( ( u  o F ( +g  `  R
) v ) `  k ) )
7271adantr 452 . . . . . . . . . 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 3429 . . . . . . . . . . 11  |-  ( k  e.  ( D  \ 
( ( `' u " ( _V  \  {  .0.  } ) )  u.  ( `' v "
( _V  \  {  .0.  } ) ) ) )  ->  k  e.  D )
744, 11, 7, 9, 44psrelbas 16399 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  u  e.  U )  ->  u : D --> ( Base `  R
) )
7574adantr 452 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  u  e.  U )  /\  v  e.  U )  ->  u : D --> ( Base `  R
) )
76 ffn 5550 . . . . . . . . . . . . 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 16399 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  u  e.  U )  /\  v  e.  U )  ->  v : D --> ( Base `  R
) )
79 ffn 5550 . . . . . . . . . . . . 13  |-  ( v : D --> ( Base `  R )  ->  v  Fn  D )
8078, 79syl 16 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  u  e.  U )  /\  v  e.  U )  ->  v  Fn  D )
81 ovex 6065 . . . . . . . . . . . . . . 15  |-  ( NN0 
^m  I )  e. 
_V
8281rabex 4314 . . . . . . . . . . . . . 14  |-  { f  e.  ( NN0  ^m  I )  |  ( `' f " NN )  e.  Fin }  e.  _V
837, 82eqeltri 2474 . . . . . . . . . . . . 13  |-  D  e. 
_V
8483a1i 11 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  u  e.  U )  /\  v  e.  U )  ->  D  e.  _V )
85 inidm 3510 . . . . . . . . . . . 12  |-  ( D  i^i  D )  =  D
86 eqidd 2405 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  u  e.  U )  /\  v  e.  U
)  /\  k  e.  D )  ->  (
u `  k )  =  ( u `  k ) )
87 eqidd 2405 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  u  e.  U )  /\  v  e.  U
)  /\  k  e.  D )  ->  (
v `  k )  =  ( v `  k ) )
8877, 80, 84, 84, 85, 86, 87ofval 6273 . . . . . . . . . . 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 461 . . . . . . . . . 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 3470 . . . . . . . . . . . . . . 15  |-  ( `' u " ( _V 
\  {  .0.  }
) )  C_  (
( `' u "
( _V  \  {  .0.  } ) )  u.  ( `' v "
( _V  \  {  .0.  } ) ) )
91 sscon 3441 . . . . . . . . . . . . . . 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 3304 . . . . . . . . . . . . 13  |-  ( k  e.  ( D  \ 
( ( `' u " ( _V  \  {  .0.  } ) )  u.  ( `' v "
( _V  \  {  .0.  } ) ) ) )  ->  k  e.  ( D  \  ( `' u " ( _V 
\  {  .0.  }
) ) ) )
94 ssid 3327 . . . . . . . . . . . . . . . 16  |-  ( `' u " ( _V 
\  {  .0.  }
) )  C_  ( `' u " ( _V 
\  {  .0.  }
) )
9594a1i 11 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  u  e.  U )  ->  ( `' u " ( _V 
\  {  .0.  }
) )  C_  ( `' u " ( _V 
\  {  .0.  }
) ) )
9674, 95suppssr 5823 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  u  e.  U )  /\  k  e.  ( D  \  ( `' u " ( _V 
\  {  .0.  }
) ) ) )  ->  ( u `  k )  =  .0.  )
9796adantlr 696 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  u  e.  U )  /\  v  e.  U
)  /\  k  e.  ( D  \  ( `' u " ( _V 
\  {  .0.  }
) ) ) )  ->  ( u `  k )  =  .0.  )
9893, 97sylan2 461 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  u  e.  U )  /\  v  e.  U
)  /\  k  e.  ( D  \  (
( `' u "
( _V  \  {  .0.  } ) )  u.  ( `' v "
( _V  \  {  .0.  } ) ) ) ) )  ->  (
u `  k )  =  .0.  )
99 ssun2 3471 . . . . . . . . . . . . . . 15  |-  ( `' v " ( _V 
\  {  .0.  }
) )  C_  (
( `' u "
( _V  \  {  .0.  } ) )  u.  ( `' v "
( _V  \  {  .0.  } ) ) )
100 sscon 3441 . . . . . . . . . . . . . . 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 3304 . . . . . . . . . . . . 13  |-  ( k  e.  ( D  \ 
( ( `' u " ( _V  \  {  .0.  } ) )  u.  ( `' v "
( _V  \  {  .0.  } ) ) ) )  ->  k  e.  ( D  \  ( `' v " ( _V  \  {  .0.  }
) ) ) )
103 ssid 3327 . . . . . . . . . . . . . . 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 5823 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  u  e.  U )  /\  v  e.  U
)  /\  k  e.  ( D  \  ( `' v " ( _V  \  {  .0.  }
) ) ) )  ->  ( v `  k )  =  .0.  )
106102, 105sylan2 461 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  u  e.  U )  /\  v  e.  U
)  /\  k  e.  ( D  \  (
( `' u "
( _V  \  {  .0.  } ) )  u.  ( `' v "
( _V  \  {  .0.  } ) ) ) ) )  ->  (
v `  k )  =  .0.  )
10798, 106oveq12d 6058 . . . . . . . . . . 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 14790 . . . . . . . . . . . . . 14  |-  ( ( R  e.  Grp  /\  .0.  e.  ( Base `  R
) )  ->  (  .0.  ( +g  `  R
)  .0.  )  =  .0.  )
10912, 108mpdan 650 . . . . . . . . . . . . 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 452 . . . . . . . . . . 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 2436 . . . . . . . . . 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 2440 . . . . . . . . 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 5822 . . . . . . . 8  |-  ( ( ( ph  /\  u  e.  U )  /\  v  e.  U )  ->  ( `' ( u ( +g  `  S ) v ) " ( _V  \  {  .0.  }
) )  C_  (
( `' u "
( _V  \  {  .0.  } ) )  u.  ( `' v "
( _V  \  {  .0.  } ) ) ) )
11567, 114ssexd 4310 . . . . . . 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 599 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  A )  ->  (
y  C_  x  ->  y  e.  A ) )
118117alrimiv 1638 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  A )  ->  A. y
( y  C_  x  ->  y  e.  A ) )
119118ralrimiva 2749 . . . . . . . . 9  |-  ( ph  ->  A. x  e.  A  A. y ( y  C_  x  ->  y  e.  A
) )
120119ad2antrr 707 . . . . . . . 8  |-  ( ( ( ph  /\  u  e.  U )  /\  v  e.  U )  ->  A. x  e.  A  A. y
( y  C_  x  ->  y  e.  A ) )
121 sseq2 3330 . . . . . . . . . . 11  |-  ( x  =  ( ( `' u " ( _V 
\  {  .0.  }
) )  u.  ( `' v " ( _V  \  {  .0.  }
) ) )  -> 
( y  C_  x  <->  y 
C_  ( ( `' u " ( _V 
\  {  .0.  }
) )  u.  ( `' v " ( _V  \  {  .0.  }
) ) ) ) )
122121imbi1d 309 . . . . . . . . . 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 1632 . . . . . . . . 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 3008 . . . . . . . 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 58 . . . . . . 7  |-  ( ( ( ph  /\  u  e.  U )  /\  v  e.  U )  ->  A. y
( y  C_  (
( `' u "
( _V  \  {  .0.  } ) )  u.  ( `' v "
( _V  \  {  .0.  } ) ) )  ->  y  e.  A
) )
126 sseq1 3329 . . . . . . . . 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 2464 . . . . . . . . 9  |-  ( y  =  ( `' ( u ( +g  `  S
) v ) "
( _V  \  {  .0.  } ) )  -> 
( y  e.  A  <->  ( `' ( u ( +g  `  S ) v ) " ( _V  \  {  .0.  }
) )  e.  A
) )
128126, 127imbi12d 312 . . . . . . . 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 2996 . . . . . . 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 59 . . . . . 6  |-  ( ( ( ph  /\  u  e.  U )  /\  v  e.  U )  ->  ( `' ( u ( +g  `  S ) v ) " ( _V  \  {  .0.  }
) )  e.  A
)
1311ad2antrr 707 . . . . . . . 8  |-  ( ( ( ph  /\  u  e.  U )  /\  v  e.  U )  ->  U  =  { g  e.  B  |  ( `' g
" ( _V  \  {  .0.  } ) )  e.  A } )
132131eleq2d 2471 . . . . . . 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 2470 . . . . . . . 8  |-  ( g  =  ( u ( +g  `  S ) v )  ->  (
( `' g "
( _V  \  {  .0.  } ) )  e.  A  <->  ( `' ( u ( +g  `  S
) v ) "
( _V  \  {  .0.  } ) )  e.  A ) )
136135elrab 3052 . . . . . . 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 253 . . . . . 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 889 . . . . 5  |-  ( ( ( ph  /\  u  e.  U )  /\  v  e.  U )  ->  (
u ( +g  `  S
) v )  e.  U )
139138ralrimiva 2749 . . . 4  |-  ( (
ph  /\  u  e.  U )  ->  A. v  e.  U  ( u
( +g  `  S ) v )  e.  U
)
1404, 5, 6psrgrp 16417 . . . . . . 7  |-  ( ph  ->  S  e.  Grp )
141 eqid 2404 . . . . . . . 8  |-  ( inv g `  S )  =  ( inv g `  S )
1429, 141grpinvcl 14805 . . . . . . 7  |-  ( ( S  e.  Grp  /\  u  e.  B )  ->  ( ( inv g `  S ) `  u
)  e.  B )
143140, 142sylan 458 . . . . . 6  |-  ( (
ph  /\  u  e.  B )  ->  (
( inv g `  S ) `  u
)  e.  B )
14444, 143syldan 457 . . . . 5  |-  ( (
ph  /\  u  e.  U )  ->  (
( inv g `  S ) `  u
)  e.  B )
1454, 11, 7, 9, 144psrelbas 16399 . . . . . . . 8  |-  ( (
ph  /\  u  e.  U )  ->  (
( inv g `  S ) `  u
) : D --> ( Base `  R ) )
1465adantr 452 . . . . . . . . . . . 12  |-  ( (
ph  /\  u  e.  U )  ->  I  e.  W )
1476adantr 452 . . . . . . . . . . . 12  |-  ( (
ph  /\  u  e.  U )  ->  R  e.  Grp )
148 eqid 2404 . . . . . . . . . . . 12  |-  ( inv g `  R )  =  ( inv g `  R )
1494, 146, 147, 7, 148, 9, 141, 44psrneg 16419 . . . . . . . . . . 11  |-  ( (
ph  /\  u  e.  U )  ->  (
( inv g `  S ) `  u
)  =  ( ( inv g `  R
)  o.  u ) )
150149adantr 452 . . . . . . . . . 10  |-  ( ( ( ph  /\  u  e.  U )  /\  k  e.  ( D  \  ( `' u " ( _V 
\  {  .0.  }
) ) ) )  ->  ( ( inv g `  S ) `
 u )  =  ( ( inv g `  R )  o.  u
) )
151150fveq1d 5689 . . . . . . . . 9  |-  ( ( ( ph  /\  u  e.  U )  /\  k  e.  ( D  \  ( `' u " ( _V 
\  {  .0.  }
) ) ) )  ->  ( ( ( inv g `  S
) `  u ) `  k )  =  ( ( ( inv g `  R )  o.  u
) `  k )
)
152 eldifi 3429 . . . . . . . . . 10  |-  ( k  e.  ( D  \ 
( `' u "
( _V  \  {  .0.  } ) ) )  ->  k  e.  D
)
153 fvco3 5759 . . . . . . . . . 10  |-  ( ( u : D --> ( Base `  R )  /\  k  e.  D )  ->  (
( ( inv g `  R )  o.  u
) `  k )  =  ( ( inv g `  R ) `
 ( u `  k ) ) )
15474, 152, 153syl2an 464 . . . . . . . . 9  |-  ( ( ( ph  /\  u  e.  U )  /\  k  e.  ( D  \  ( `' u " ( _V 
\  {  .0.  }
) ) ) )  ->  ( ( ( inv g `  R
)  o.  u ) `
 k )  =  ( ( inv g `  R ) `  (
u `  k )
) )
15596fveq2d 5691 . . . . . . . . . 10  |-  ( ( ( ph  /\  u  e.  U )  /\  k  e.  ( D  \  ( `' u " ( _V 
\  {  .0.  }
) ) ) )  ->  ( ( inv g `  R ) `
 ( u `  k ) )  =  ( ( inv g `  R ) `  .0.  ) )
1568, 148grpinvid 14811 . . . . . . . . . . . 12  |-  ( R  e.  Grp  ->  (
( inv g `  R ) `  .0.  )  =  .0.  )
157147, 156syl 16 . . . . . . . . . . 11  |-  ( (
ph  /\  u  e.  U )  ->  (
( inv g `  R ) `  .0.  )  =  .0.  )
158157adantr 452 . . . . . . . . . 10  |-  ( ( ( ph  /\  u  e.  U )  /\  k  e.  ( D  \  ( `' u " ( _V 
\  {  .0.  }
) ) ) )  ->  ( ( inv g `  R ) `
 .0.  )  =  .0.  )
159155, 158eqtrd 2436 . . . . . . . . 9  |-  ( ( ( ph  /\  u  e.  U )  /\  k  e.  ( D  \  ( `' u " ( _V 
\  {  .0.  }
) ) ) )  ->  ( ( inv g `  R ) `
 ( u `  k ) )  =  .0.  )
160151, 154, 1593eqtrd 2440 . . . . . . . 8  |-  ( ( ( ph  /\  u  e.  U )  /\  k  e.  ( D  \  ( `' u " ( _V 
\  {  .0.  }
) ) ) )  ->  ( ( ( inv g `  S
) `  u ) `  k )  =  .0.  )
161145, 160suppss 5822 . . . . . . 7  |-  ( (
ph  /\  u  e.  U )  ->  ( `' ( ( inv g `  S ) `
 u ) "
( _V  \  {  .0.  } ) )  C_  ( `' u " ( _V 
\  {  .0.  }
) ) )
16256, 161ssexd 4310 . . . . . 6  |-  ( (
ph  /\  u  e.  U )  ->  ( `' ( ( inv g `  S ) `
 u ) "
( _V  \  {  .0.  } ) )  e. 
_V )
163119adantr 452 . . . . . . 7  |-  ( (
ph  /\  u  e.  U )  ->  A. x  e.  A  A. y
( y  C_  x  ->  y  e.  A ) )
164 sseq2 3330 . . . . . . . . . 10  |-  ( x  =  ( `' u " ( _V  \  {  .0.  } ) )  -> 
( y  C_  x  <->  y 
C_  ( `' u " ( _V  \  {  .0.  } ) ) ) )
165164imbi1d 309 . . . . . . . . 9  |-  ( x  =  ( `' u " ( _V  \  {  .0.  } ) )  -> 
( ( y  C_  x  ->  y  e.  A
)  <->  ( y  C_  ( `' u " ( _V 
\  {  .0.  }
) )  ->  y  e.  A ) ) )
166165albidv 1632 . . . . . . . 8  |-  ( x  =  ( `' u " ( _V  \  {  .0.  } ) )  -> 
( A. y ( y  C_  x  ->  y  e.  A )  <->  A. y
( y  C_  ( `' u " ( _V 
\  {  .0.  }
) )  ->  y  e.  A ) ) )
167166rspcv 3008 . . . . . . 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 58 . . . . . 6  |-  ( (
ph  /\  u  e.  U )  ->  A. y
( y  C_  ( `' u " ( _V 
\  {  .0.  }
) )  ->  y  e.  A ) )
169 sseq1 3329 . . . . . . . 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 2464 . . . . . . . 8  |-  ( y  =  ( `' ( ( inv g `  S ) `  u
) " ( _V 
\  {  .0.  }
) )  ->  (
y  e.  A  <->  ( `' ( ( inv g `  S ) `  u
) " ( _V 
\  {  .0.  }
) )  e.  A
) )
171169, 170imbi12d 312 . . . . . . 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 2996 . . . . . 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 59 . . . . 5  |-  ( (
ph  /\  u  e.  U )  ->  ( `' ( ( inv g `  S ) `
 u ) "
( _V  \  {  .0.  } ) )  e.  A )
17446eleq2d 2471 . . . . . 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 5005 . . . . . . . . 9  |-  ( g  =  ( ( inv g `  S ) `
 u )  ->  `' g  =  `' ( ( inv g `  S ) `  u
) )
176175imaeq1d 5161 . . . . . . . 8  |-  ( g  =  ( ( inv g `  S ) `
 u )  -> 
( `' g "
( _V  \  {  .0.  } ) )  =  ( `' ( ( inv g `  S
) `  u ) " ( _V  \  {  .0.  } ) ) )
177176eleq1d 2470 . . . . . . 7  |-  ( g  =  ( ( inv g `  S ) `
 u )  -> 
( ( `' g
" ( _V  \  {  .0.  } ) )  e.  A  <->  ( `' ( ( inv g `  S ) `  u
) " ( _V 
\  {  .0.  }
) )  e.  A
) )
178177elrab 3052 . . . . . 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 253 . . . . 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 889 . . . 4  |-  ( (
ph  /\  u  e.  U )  ->  (
( inv g `  S ) `  u
)  e.  U )
181139, 180jca 519 . . 3  |-  ( (
ph  /\  u  e.  U )  ->  ( A. v  e.  U  ( u ( +g  `  S ) v )  e.  U  /\  (
( inv g `  S ) `  u
)  e.  U ) )
182181ralrimiva 2749 . 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 14914 . . 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 1137 1  |-  ( ph  ->  U  e.  (SubGrp `  S ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359    /\ w3a 936   A.wal 1546    = wceq 1649    e. wcel 1721    =/= wne 2567   A.wral 2666   {crab 2670   _Vcvv 2916    \ cdif 3277    u. cun 3278    C_ wss 3280   (/)c0 3588   {csn 3774    X. cxp 4835   `'ccnv 4836   "cima 4840    o. ccom 4841    Fn wfn 5408   -->wf 5409   ` cfv 5413  (class class class)co 6040    o Fcof 6262    ^m cmap 6977   Fincfn 7068   NNcn 9956   NN0cn0 10177   Basecbs 13424   +g cplusg 13484   0gc0g 13678   Grpcgrp 14640   inv gcminusg 14641  SubGrpcsubg 14893   mPwSer cmps 16361
This theorem is referenced by:  mpllsslem  16454  mplsubg  16455
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-rep 4280  ax-sep 4290  ax-nul 4298  ax-pow 4337  ax-pr 4363  ax-un 4660  ax-cnex 9002  ax-resscn 9003  ax-1cn 9004  ax-icn 9005  ax-addcl 9006  ax-addrcl 9007  ax-mulcl 9008  ax-mulrcl 9009  ax-mulcom 9010  ax-addass 9011  ax-mulass 9012  ax-distr 9013  ax-i2m1 9014  ax-1ne0 9015  ax-1rid 9016  ax-rnegex 9017  ax-rrecex 9018  ax-cnre 9019  ax-pre-lttri 9020  ax-pre-lttrn 9021  ax-pre-ltadd 9022  ax-pre-mulgt0 9023
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-nel 2570  df-ral 2671  df-rex 2672  df-reu 2673  df-rmo 2674  df-rab 2675  df-v 2918  df-sbc 3122  df-csb 3212  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-pss 3296  df-nul 3589  df-if 3700  df-pw 3761  df-sn 3780  df-pr 3781  df-tp 3782  df-op 3783  df-uni 3976  df-int 4011  df-iun 4055  df-br 4173  df-opab 4227  df-mpt 4228  df-tr 4263  df-eprel 4454  df-id 4458  df-po 4463  df-so 4464  df-fr 4501  df-we 4503  df-ord 4544  df-on 4545  df-lim 4546  df-suc 4547  df-om 4805  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-iota 5377  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-ov 6043  df-oprab 6044  df-mpt2 6045  df-of 6264  df-1st 6308  df-2nd 6309  df-riota 6508  df-recs 6592  df-rdg 6627  df-1o 6683  df-oadd 6687  df-er 6864  df-map 6979  df-en 7069  df-dom 7070  df-sdom 7071  df-fin 7072  df-pnf 9078  df-mnf 9079  df-xr 9080  df-ltxr 9081  df-le 9082  df-sub 9249  df-neg 9250  df-nn 9957  df-2 10014  df-3 10015  df-4 10016  df-5 10017  df-6 10018  df-7 10019  df-8 10020  df-9 10021  df-n0 10178  df-z 10239  df-uz 10445  df-fz 11000  df-struct 13426  df-ndx 13427  df-slot 13428  df-base 13429  df-sets 13430  df-ress 13431  df-plusg 13497  df-mulr 13498  df-sca 13500  df-vsca 13501  df-tset 13503  df-0g 13682  df-mnd 14645  df-grp 14767  df-minusg 14768  df-subg 14896  df-psr 16372
  Copyright terms: Public domain W3C validator