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

Theorem issubm 14425
Description: Expand definition of a submonoid. (Contributed by Mario Carneiro, 7-Mar-2015.)
Hypotheses
Ref Expression
issubm.b  |-  B  =  ( Base `  M
)
issubm.z  |-  .0.  =  ( 0g `  M )
issubm.p  |-  .+  =  ( +g  `  M )
Assertion
Ref Expression
issubm  |-  ( M  e.  Mnd  ->  ( S  e.  (SubMnd `  M
)  <->  ( S  C_  B  /\  .0.  e.  S  /\  A. x  e.  S  A. y  e.  S  ( x  .+  y )  e.  S ) ) )
Distinct variable groups:    x, M, y    x, S, y
Allowed substitution hints:    B( x, y)    .+ ( x, y)    .0. ( x, y)

Proof of Theorem issubm
Dummy variables  m  t are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fveq2 5525 . . . . . 6  |-  ( m  =  M  ->  ( Base `  m )  =  ( Base `  M
) )
21pweqd 3630 . . . . 5  |-  ( m  =  M  ->  ~P ( Base `  m )  =  ~P ( Base `  M
) )
3 fveq2 5525 . . . . . . 7  |-  ( m  =  M  ->  ( 0g `  m )  =  ( 0g `  M
) )
43eleq1d 2349 . . . . . 6  |-  ( m  =  M  ->  (
( 0g `  m
)  e.  t  <->  ( 0g `  M )  e.  t ) )
5 fveq2 5525 . . . . . . . . 9  |-  ( m  =  M  ->  ( +g  `  m )  =  ( +g  `  M
) )
65oveqd 5875 . . . . . . . 8  |-  ( m  =  M  ->  (
x ( +g  `  m
) y )  =  ( x ( +g  `  M ) y ) )
76eleq1d 2349 . . . . . . 7  |-  ( m  =  M  ->  (
( x ( +g  `  m ) y )  e.  t  <->  ( x
( +g  `  M ) y )  e.  t ) )
872ralbidv 2585 . . . . . 6  |-  ( m  =  M  ->  ( A. x  e.  t  A. y  e.  t 
( x ( +g  `  m ) y )  e.  t  <->  A. x  e.  t  A. y  e.  t  ( x
( +g  `  M ) y )  e.  t ) )
94, 8anbi12d 691 . . . . 5  |-  ( m  =  M  ->  (
( ( 0g `  m )  e.  t  /\  A. x  e.  t  A. y  e.  t  ( x ( +g  `  m ) y )  e.  t )  <->  ( ( 0g
`  M )  e.  t  /\  A. x  e.  t  A. y  e.  t  ( x
( +g  `  M ) y )  e.  t ) ) )
102, 9rabeqbidv 2783 . . . 4  |-  ( m  =  M  ->  { t  e.  ~P ( Base `  m )  |  ( ( 0g `  m
)  e.  t  /\  A. x  e.  t  A. y  e.  t  (
x ( +g  `  m
) y )  e.  t ) }  =  { t  e.  ~P ( Base `  M )  |  ( ( 0g
`  M )  e.  t  /\  A. x  e.  t  A. y  e.  t  ( x
( +g  `  M ) y )  e.  t ) } )
11 df-submnd 14416 . . . 4  |- SubMnd  =  ( m  e.  Mnd  |->  { t  e.  ~P ( Base `  m )  |  ( ( 0g `  m )  e.  t  /\  A. x  e.  t  A. y  e.  t  ( x ( +g  `  m ) y )  e.  t ) } )
12 fvex 5539 . . . . . 6  |-  ( Base `  M )  e.  _V
1312pwex 4193 . . . . 5  |-  ~P ( Base `  M )  e. 
_V
1413rabex 4165 . . . 4  |-  { t  e.  ~P ( Base `  M )  |  ( ( 0g `  M
)  e.  t  /\  A. x  e.  t  A. y  e.  t  (
x ( +g  `  M
) y )  e.  t ) }  e.  _V
1510, 11, 14fvmpt 5602 . . 3  |-  ( M  e.  Mnd  ->  (SubMnd `  M )  =  {
t  e.  ~P ( Base `  M )  |  ( ( 0g `  M )  e.  t  /\  A. x  e.  t  A. y  e.  t  ( x ( +g  `  M ) y )  e.  t ) } )
1615eleq2d 2350 . 2  |-  ( M  e.  Mnd  ->  ( S  e.  (SubMnd `  M
)  <->  S  e.  { t  e.  ~P ( Base `  M )  |  ( ( 0g `  M
)  e.  t  /\  A. x  e.  t  A. y  e.  t  (
x ( +g  `  M
) y )  e.  t ) } ) )
17 eleq2 2344 . . . . 5  |-  ( t  =  S  ->  (
( 0g `  M
)  e.  t  <->  ( 0g `  M )  e.  S
) )
18 eleq2 2344 . . . . . . 7  |-  ( t  =  S  ->  (
( x ( +g  `  M ) y )  e.  t  <->  ( x
( +g  `  M ) y )  e.  S
) )
1918raleqbi1dv 2744 . . . . . 6  |-  ( t  =  S  ->  ( A. y  e.  t 
( x ( +g  `  M ) y )  e.  t  <->  A. y  e.  S  ( x
( +g  `  M ) y )  e.  S
) )
2019raleqbi1dv 2744 . . . . 5  |-  ( t  =  S  ->  ( A. x  e.  t  A. y  e.  t 
( x ( +g  `  M ) y )  e.  t  <->  A. x  e.  S  A. y  e.  S  ( x
( +g  `  M ) y )  e.  S
) )
2117, 20anbi12d 691 . . . 4  |-  ( t  =  S  ->  (
( ( 0g `  M )  e.  t  /\  A. x  e.  t  A. y  e.  t  ( x ( +g  `  M ) y )  e.  t )  <->  ( ( 0g
`  M )  e.  S  /\  A. x  e.  S  A. y  e.  S  ( x
( +g  `  M ) y )  e.  S
) ) )
2221elrab 2923 . . 3  |-  ( S  e.  { t  e. 
~P ( Base `  M
)  |  ( ( 0g `  M )  e.  t  /\  A. x  e.  t  A. y  e.  t  (
x ( +g  `  M
) y )  e.  t ) }  <->  ( S  e.  ~P ( Base `  M
)  /\  ( ( 0g `  M )  e.  S  /\  A. x  e.  S  A. y  e.  S  ( x
( +g  `  M ) y )  e.  S
) ) )
23 issubm.b . . . . . 6  |-  B  =  ( Base `  M
)
2423sseq2i 3203 . . . . 5  |-  ( S 
C_  B  <->  S  C_  ( Base `  M ) )
25 issubm.z . . . . . . 7  |-  .0.  =  ( 0g `  M )
2625eleq1i 2346 . . . . . 6  |-  (  .0. 
e.  S  <->  ( 0g `  M )  e.  S
)
27 issubm.p . . . . . . . . 9  |-  .+  =  ( +g  `  M )
2827oveqi 5871 . . . . . . . 8  |-  ( x 
.+  y )  =  ( x ( +g  `  M ) y )
2928eleq1i 2346 . . . . . . 7  |-  ( ( x  .+  y )  e.  S  <->  ( x
( +g  `  M ) y )  e.  S
)
30292ralbii 2569 . . . . . 6  |-  ( A. x  e.  S  A. y  e.  S  (
x  .+  y )  e.  S  <->  A. x  e.  S  A. y  e.  S  ( x ( +g  `  M ) y )  e.  S )
3126, 30anbi12i 678 . . . . 5  |-  ( (  .0.  e.  S  /\  A. x  e.  S  A. y  e.  S  (
x  .+  y )  e.  S )  <->  ( ( 0g `  M )  e.  S  /\  A. x  e.  S  A. y  e.  S  ( x
( +g  `  M ) y )  e.  S
) )
3224, 31anbi12i 678 . . . 4  |-  ( ( S  C_  B  /\  (  .0.  e.  S  /\  A. x  e.  S  A. y  e.  S  (
x  .+  y )  e.  S ) )  <->  ( S  C_  ( Base `  M
)  /\  ( ( 0g `  M )  e.  S  /\  A. x  e.  S  A. y  e.  S  ( x
( +g  `  M ) y )  e.  S
) ) )
33 3anass 938 . . . 4  |-  ( ( S  C_  B  /\  .0.  e.  S  /\  A. x  e.  S  A. y  e.  S  (
x  .+  y )  e.  S )  <->  ( S  C_  B  /\  (  .0. 
e.  S  /\  A. x  e.  S  A. y  e.  S  (
x  .+  y )  e.  S ) ) )
3412elpw2 4175 . . . . 5  |-  ( S  e.  ~P ( Base `  M )  <->  S  C_  ( Base `  M ) )
3534anbi1i 676 . . . 4  |-  ( ( S  e.  ~P ( Base `  M )  /\  ( ( 0g `  M )  e.  S  /\  A. x  e.  S  A. y  e.  S  ( x ( +g  `  M ) y )  e.  S ) )  <-> 
( S  C_  ( Base `  M )  /\  ( ( 0g `  M )  e.  S  /\  A. x  e.  S  A. y  e.  S  ( x ( +g  `  M ) y )  e.  S ) ) )
3632, 33, 353bitr4ri 269 . . 3  |-  ( ( S  e.  ~P ( Base `  M )  /\  ( ( 0g `  M )  e.  S  /\  A. x  e.  S  A. y  e.  S  ( x ( +g  `  M ) y )  e.  S ) )  <-> 
( S  C_  B  /\  .0.  e.  S  /\  A. x  e.  S  A. y  e.  S  (
x  .+  y )  e.  S ) )
3722, 36bitri 240 . 2  |-  ( S  e.  { t  e. 
~P ( Base `  M
)  |  ( ( 0g `  M )  e.  t  /\  A. x  e.  t  A. y  e.  t  (
x ( +g  `  M
) y )  e.  t ) }  <->  ( S  C_  B  /\  .0.  e.  S  /\  A. x  e.  S  A. y  e.  S  ( x  .+  y )  e.  S
) )
3816, 37syl6bb 252 1  |-  ( M  e.  Mnd  ->  ( S  e.  (SubMnd `  M
)  <->  ( S  C_  B  /\  .0.  e.  S  /\  A. x  e.  S  A. y  e.  S  ( x  .+  y )  e.  S ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358    /\ w3a 934    = wceq 1623    e. wcel 1684   A.wral 2543   {crab 2547    C_ wss 3152   ~Pcpw 3625   ` cfv 5255  (class class class)co 5858   Basecbs 13148   +g cplusg 13208   0gc0g 13400   Mndcmnd 14361  SubMndcsubmnd 14414
This theorem is referenced by:  issubm2  14426  submcl  14430  mhmima  14440  mhmeql  14441  submacs  14442  gsumwspan  14468  frmdsssubm  14483  issubg3  14637  cntzsubm  14811  oppgsubm  14835  lsmsubm  14964  issubrg3  15573  xrge0subm  16412  cnsubmlem  16419  iistmd  23286  issubmd  27383  isdomn3  27523  mon1psubm  27525
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141  ax-nul 4149  ax-pow 4188  ax-pr 4214
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-mo 2148  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-ral 2548  df-rex 2549  df-rab 2552  df-v 2790  df-sbc 2992  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-pw 3627  df-sn 3646  df-pr 3647  df-op 3649  df-uni 3828  df-br 4024  df-opab 4078  df-mpt 4079  df-id 4309  df-xp 4695  df-rel 4696  df-cnv 4697  df-co 4698  df-dm 4699  df-iota 5219  df-fun 5257  df-fv 5263  df-ov 5861  df-submnd 14416
  Copyright terms: Public domain W3C validator