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

Theorem ismhm 14699
Description: Property of a monoid homomorphism. (Contributed by Mario Carneiro, 7-Mar-2015.)
Hypotheses
Ref Expression
ismhm.b  |-  B  =  ( Base `  S
)
ismhm.c  |-  C  =  ( Base `  T
)
ismhm.p  |-  .+  =  ( +g  `  S )
ismhm.q  |-  .+^  =  ( +g  `  T )
ismhm.z  |-  .0.  =  ( 0g `  S )
ismhm.y  |-  Y  =  ( 0g `  T
)
Assertion
Ref Expression
ismhm  |-  ( F  e.  ( S MndHom  T
)  <->  ( ( S  e.  Mnd  /\  T  e.  Mnd )  /\  ( F : B --> C  /\  A. x  e.  B  A. y  e.  B  ( F `  ( x  .+  y ) )  =  ( ( F `  x )  .+^  ( F `
 y ) )  /\  ( F `  .0.  )  =  Y
) ) )
Distinct variable groups:    x, y, B    x, S, y    x, T, y    x, F, y
Allowed substitution hints:    C( x, y)    .+ ( x, y)    .+^ ( x, y)    Y( x, y)    .0. ( x, y)

Proof of Theorem ismhm
Dummy variables  f 
s  t are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-mhm 14697 . . 3  |- MndHom  =  ( s  e.  Mnd , 
t  e.  Mnd  |->  { f  e.  ( (
Base `  t )  ^m  ( Base `  s
) )  |  ( A. x  e.  (
Base `  s ) A. y  e.  ( Base `  s ) ( f `  ( x ( +g  `  s
) y ) )  =  ( ( f `
 x ) ( +g  `  t ) ( f `  y
) )  /\  (
f `  ( 0g `  s ) )  =  ( 0g `  t
) ) } )
21elmpt2cl 6251 . 2  |-  ( F  e.  ( S MndHom  T
)  ->  ( S  e.  Mnd  /\  T  e. 
Mnd ) )
3 fveq2 5691 . . . . . . . 8  |-  ( t  =  T  ->  ( Base `  t )  =  ( Base `  T
) )
4 ismhm.c . . . . . . . 8  |-  C  =  ( Base `  T
)
53, 4syl6eqr 2458 . . . . . . 7  |-  ( t  =  T  ->  ( Base `  t )  =  C )
6 fveq2 5691 . . . . . . . 8  |-  ( s  =  S  ->  ( Base `  s )  =  ( Base `  S
) )
7 ismhm.b . . . . . . . 8  |-  B  =  ( Base `  S
)
86, 7syl6eqr 2458 . . . . . . 7  |-  ( s  =  S  ->  ( Base `  s )  =  B )
95, 8oveqan12rd 6064 . . . . . 6  |-  ( ( s  =  S  /\  t  =  T )  ->  ( ( Base `  t
)  ^m  ( Base `  s ) )  =  ( C  ^m  B
) )
108adantr 452 . . . . . . . 8  |-  ( ( s  =  S  /\  t  =  T )  ->  ( Base `  s
)  =  B )
11 fveq2 5691 . . . . . . . . . . . . 13  |-  ( s  =  S  ->  ( +g  `  s )  =  ( +g  `  S
) )
12 ismhm.p . . . . . . . . . . . . 13  |-  .+  =  ( +g  `  S )
1311, 12syl6eqr 2458 . . . . . . . . . . . 12  |-  ( s  =  S  ->  ( +g  `  s )  = 
.+  )
1413oveqd 6061 . . . . . . . . . . 11  |-  ( s  =  S  ->  (
x ( +g  `  s
) y )  =  ( x  .+  y
) )
1514fveq2d 5695 . . . . . . . . . 10  |-  ( s  =  S  ->  (
f `  ( x
( +g  `  s ) y ) )  =  ( f `  (
x  .+  y )
) )
16 fveq2 5691 . . . . . . . . . . . 12  |-  ( t  =  T  ->  ( +g  `  t )  =  ( +g  `  T
) )
17 ismhm.q . . . . . . . . . . . 12  |-  .+^  =  ( +g  `  T )
1816, 17syl6eqr 2458 . . . . . . . . . . 11  |-  ( t  =  T  ->  ( +g  `  t )  = 
.+^  )
1918oveqd 6061 . . . . . . . . . 10  |-  ( t  =  T  ->  (
( f `  x
) ( +g  `  t
) ( f `  y ) )  =  ( ( f `  x )  .+^  ( f `
 y ) ) )
2015, 19eqeqan12d 2423 . . . . . . . . 9  |-  ( ( s  =  S  /\  t  =  T )  ->  ( ( f `  ( x ( +g  `  s ) y ) )  =  ( ( f `  x ) ( +g  `  t
) ( f `  y ) )  <->  ( f `  ( x  .+  y
) )  =  ( ( f `  x
)  .+^  ( f `  y ) ) ) )
2110, 20raleqbidv 2880 . . . . . . . 8  |-  ( ( s  =  S  /\  t  =  T )  ->  ( A. y  e.  ( Base `  s
) ( f `  ( x ( +g  `  s ) y ) )  =  ( ( f `  x ) ( +g  `  t
) ( f `  y ) )  <->  A. y  e.  B  ( f `  ( x  .+  y
) )  =  ( ( f `  x
)  .+^  ( f `  y ) ) ) )
2210, 21raleqbidv 2880 . . . . . . 7  |-  ( ( s  =  S  /\  t  =  T )  ->  ( A. x  e.  ( Base `  s
) A. y  e.  ( Base `  s
) ( f `  ( x ( +g  `  s ) y ) )  =  ( ( f `  x ) ( +g  `  t
) ( f `  y ) )  <->  A. x  e.  B  A. y  e.  B  ( f `  ( x  .+  y
) )  =  ( ( f `  x
)  .+^  ( f `  y ) ) ) )
23 fveq2 5691 . . . . . . . . . 10  |-  ( s  =  S  ->  ( 0g `  s )  =  ( 0g `  S
) )
24 ismhm.z . . . . . . . . . 10  |-  .0.  =  ( 0g `  S )
2523, 24syl6eqr 2458 . . . . . . . . 9  |-  ( s  =  S  ->  ( 0g `  s )  =  .0.  )
2625fveq2d 5695 . . . . . . . 8  |-  ( s  =  S  ->  (
f `  ( 0g `  s ) )  =  ( f `  .0.  ) )
27 fveq2 5691 . . . . . . . . 9  |-  ( t  =  T  ->  ( 0g `  t )  =  ( 0g `  T
) )
28 ismhm.y . . . . . . . . 9  |-  Y  =  ( 0g `  T
)
2927, 28syl6eqr 2458 . . . . . . . 8  |-  ( t  =  T  ->  ( 0g `  t )  =  Y )
3026, 29eqeqan12d 2423 . . . . . . 7  |-  ( ( s  =  S  /\  t  =  T )  ->  ( ( f `  ( 0g `  s ) )  =  ( 0g
`  t )  <->  ( f `  .0.  )  =  Y ) )
3122, 30anbi12d 692 . . . . . 6  |-  ( ( s  =  S  /\  t  =  T )  ->  ( ( A. x  e.  ( Base `  s
) A. y  e.  ( Base `  s
) ( f `  ( x ( +g  `  s ) y ) )  =  ( ( f `  x ) ( +g  `  t
) ( f `  y ) )  /\  ( f `  ( 0g `  s ) )  =  ( 0g `  t ) )  <->  ( A. x  e.  B  A. y  e.  B  (
f `  ( x  .+  y ) )  =  ( ( f `  x )  .+^  ( f `
 y ) )  /\  ( f `  .0.  )  =  Y
) ) )
329, 31rabeqbidv 2915 . . . . 5  |-  ( ( s  =  S  /\  t  =  T )  ->  { f  e.  ( ( Base `  t
)  ^m  ( Base `  s ) )  |  ( A. x  e.  ( Base `  s
) A. y  e.  ( Base `  s
) ( f `  ( x ( +g  `  s ) y ) )  =  ( ( f `  x ) ( +g  `  t
) ( f `  y ) )  /\  ( f `  ( 0g `  s ) )  =  ( 0g `  t ) ) }  =  { f  e.  ( C  ^m  B
)  |  ( A. x  e.  B  A. y  e.  B  (
f `  ( x  .+  y ) )  =  ( ( f `  x )  .+^  ( f `
 y ) )  /\  ( f `  .0.  )  =  Y
) } )
33 ovex 6069 . . . . . 6  |-  ( C  ^m  B )  e. 
_V
3433rabex 4318 . . . . 5  |-  { f  e.  ( C  ^m  B )  |  ( A. x  e.  B  A. y  e.  B  ( f `  (
x  .+  y )
)  =  ( ( f `  x ) 
.+^  ( f `  y ) )  /\  ( f `  .0.  )  =  Y ) }  e.  _V
3532, 1, 34ovmpt2a 6167 . . . 4  |-  ( ( S  e.  Mnd  /\  T  e.  Mnd )  ->  ( S MndHom  T )  =  { f  e.  ( C  ^m  B
)  |  ( A. x  e.  B  A. y  e.  B  (
f `  ( x  .+  y ) )  =  ( ( f `  x )  .+^  ( f `
 y ) )  /\  ( f `  .0.  )  =  Y
) } )
3635eleq2d 2475 . . 3  |-  ( ( S  e.  Mnd  /\  T  e.  Mnd )  ->  ( F  e.  ( S MndHom  T )  <->  F  e.  { f  e.  ( C  ^m  B )  |  ( A. x  e.  B  A. y  e.  B  ( f `  ( x  .+  y ) )  =  ( ( f `  x ) 
.+^  ( f `  y ) )  /\  ( f `  .0.  )  =  Y ) } ) )
37 fvex 5705 . . . . . . 7  |-  ( Base `  T )  e.  _V
384, 37eqeltri 2478 . . . . . 6  |-  C  e. 
_V
39 fvex 5705 . . . . . . 7  |-  ( Base `  S )  e.  _V
407, 39eqeltri 2478 . . . . . 6  |-  B  e. 
_V
4138, 40elmap 7005 . . . . 5  |-  ( F  e.  ( C  ^m  B )  <->  F : B
--> C )
4241anbi1i 677 . . . 4  |-  ( ( F  e.  ( C  ^m  B )  /\  ( A. x  e.  B  A. y  e.  B  ( F `  ( x 
.+  y ) )  =  ( ( F `
 x )  .+^  ( F `  y ) )  /\  ( F `
 .0.  )  =  Y ) )  <->  ( F : B --> C  /\  ( A. x  e.  B  A. y  e.  B  ( F `  ( x 
.+  y ) )  =  ( ( F `
 x )  .+^  ( F `  y ) )  /\  ( F `
 .0.  )  =  Y ) ) )
43 fveq1 5690 . . . . . . . 8  |-  ( f  =  F  ->  (
f `  ( x  .+  y ) )  =  ( F `  (
x  .+  y )
) )
44 fveq1 5690 . . . . . . . . 9  |-  ( f  =  F  ->  (
f `  x )  =  ( F `  x ) )
45 fveq1 5690 . . . . . . . . 9  |-  ( f  =  F  ->  (
f `  y )  =  ( F `  y ) )
4644, 45oveq12d 6062 . . . . . . . 8  |-  ( f  =  F  ->  (
( f `  x
)  .+^  ( f `  y ) )  =  ( ( F `  x )  .+^  ( F `
 y ) ) )
4743, 46eqeq12d 2422 . . . . . . 7  |-  ( f  =  F  ->  (
( f `  (
x  .+  y )
)  =  ( ( f `  x ) 
.+^  ( f `  y ) )  <->  ( F `  ( x  .+  y
) )  =  ( ( F `  x
)  .+^  ( F `  y ) ) ) )
48472ralbidv 2712 . . . . . 6  |-  ( f  =  F  ->  ( A. x  e.  B  A. y  e.  B  ( f `  (
x  .+  y )
)  =  ( ( f `  x ) 
.+^  ( f `  y ) )  <->  A. x  e.  B  A. y  e.  B  ( F `  ( x  .+  y
) )  =  ( ( F `  x
)  .+^  ( F `  y ) ) ) )
49 fveq1 5690 . . . . . . 7  |-  ( f  =  F  ->  (
f `  .0.  )  =  ( F `  .0.  ) )
5049eqeq1d 2416 . . . . . 6  |-  ( f  =  F  ->  (
( f `  .0.  )  =  Y  <->  ( F `  .0.  )  =  Y ) )
5148, 50anbi12d 692 . . . . 5  |-  ( f  =  F  ->  (
( A. x  e.  B  A. y  e.  B  ( f `  ( x  .+  y ) )  =  ( ( f `  x ) 
.+^  ( f `  y ) )  /\  ( f `  .0.  )  =  Y )  <->  ( A. x  e.  B  A. y  e.  B  ( F `  ( x 
.+  y ) )  =  ( ( F `
 x )  .+^  ( F `  y ) )  /\  ( F `
 .0.  )  =  Y ) ) )
5251elrab 3056 . . . 4  |-  ( F  e.  { f  e.  ( C  ^m  B
)  |  ( A. x  e.  B  A. y  e.  B  (
f `  ( x  .+  y ) )  =  ( ( f `  x )  .+^  ( f `
 y ) )  /\  ( f `  .0.  )  =  Y
) }  <->  ( F  e.  ( C  ^m  B
)  /\  ( A. x  e.  B  A. y  e.  B  ( F `  ( x  .+  y ) )  =  ( ( F `  x )  .+^  ( F `
 y ) )  /\  ( F `  .0.  )  =  Y
) ) )
53 3anass 940 . . . 4  |-  ( ( F : B --> C  /\  A. x  e.  B  A. y  e.  B  ( F `  ( x  .+  y ) )  =  ( ( F `  x )  .+^  ( F `
 y ) )  /\  ( F `  .0.  )  =  Y
)  <->  ( F : B
--> C  /\  ( A. x  e.  B  A. y  e.  B  ( F `  ( x  .+  y ) )  =  ( ( F `  x )  .+^  ( F `
 y ) )  /\  ( F `  .0.  )  =  Y
) ) )
5442, 52, 533bitr4i 269 . . 3  |-  ( F  e.  { f  e.  ( C  ^m  B
)  |  ( A. x  e.  B  A. y  e.  B  (
f `  ( x  .+  y ) )  =  ( ( f `  x )  .+^  ( f `
 y ) )  /\  ( f `  .0.  )  =  Y
) }  <->  ( F : B --> C  /\  A. x  e.  B  A. y  e.  B  ( F `  ( x  .+  y ) )  =  ( ( F `  x )  .+^  ( F `
 y ) )  /\  ( F `  .0.  )  =  Y
) )
5536, 54syl6bb 253 . 2  |-  ( ( S  e.  Mnd  /\  T  e.  Mnd )  ->  ( F  e.  ( S MndHom  T )  <->  ( F : B --> C  /\  A. x  e.  B  A. y  e.  B  ( F `  ( x  .+  y ) )  =  ( ( F `  x )  .+^  ( F `
 y ) )  /\  ( F `  .0.  )  =  Y
) ) )
562, 55biadan2 624 1  |-  ( F  e.  ( S MndHom  T
)  <->  ( ( S  e.  Mnd  /\  T  e.  Mnd )  /\  ( F : B --> C  /\  A. x  e.  B  A. y  e.  B  ( F `  ( x  .+  y ) )  =  ( ( F `  x )  .+^  ( F `
 y ) )  /\  ( F `  .0.  )  =  Y
) ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 177    /\ wa 359    /\ w3a 936    = wceq 1649    e. wcel 1721   A.wral 2670   {crab 2674   _Vcvv 2920   -->wf 5413   ` cfv 5417  (class class class)co 6044    ^m cmap 6981   Basecbs 13428   +g cplusg 13488   0gc0g 13682   Mndcmnd 14643   MndHom cmhm 14695
This theorem is referenced by:  mhmf  14702  mhmpropd  14703  mhmlin  14704  mhm0  14705  0mhm  14717  resmhm  14718  resmhm2  14719  resmhm2b  14720  mhmco  14721  prdspjmhm  14725  pwsdiagmhm  14727  pwsco1mhm  14728  pwsco2mhm  14729  frmdup1  14768  ghmmhm  14975  frgpmhm  15356  mulgmhm  15409  dfrhm2  15780  isrhm2d  15788  expmhm  16735  dchrelbas3  20979  xrge0iifmhm  24282  esumcocn  24427  deg1mhm  27398
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 2389  ax-sep 4294  ax-nul 4302  ax-pow 4341  ax-pr 4367  ax-un 4664
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2262  df-mo 2263  df-clab 2395  df-cleq 2401  df-clel 2404  df-nfc 2533  df-ne 2573  df-ral 2675  df-rex 2676  df-rab 2679  df-v 2922  df-sbc 3126  df-dif 3287  df-un 3289  df-in 3291  df-ss 3298  df-nul 3593  df-if 3704  df-pw 3765  df-sn 3784  df-pr 3785  df-op 3787  df-uni 3980  df-br 4177  df-opab 4231  df-id 4462  df-xp 4847  df-rel 4848  df-cnv 4849  df-co 4850  df-dm 4851  df-rn 4852  df-iota 5381  df-fun 5419  df-fn 5420  df-f 5421  df-fv 5425  df-ov 6047  df-oprab 6048  df-mpt2 6049  df-map 6983  df-mhm 14697
  Copyright terms: Public domain W3C validator