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

Theorem ismhm 16535
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 16533 . . 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 6525 . 2  |-  ( F  e.  ( S MndHom  T
)  ->  ( S  e.  Mnd  /\  T  e. 
Mnd ) )
3 fveq2 5881 . . . . . . . 8  |-  ( t  =  T  ->  ( Base `  t )  =  ( Base `  T
) )
4 ismhm.c . . . . . . . 8  |-  C  =  ( Base `  T
)
53, 4syl6eqr 2488 . . . . . . 7  |-  ( t  =  T  ->  ( Base `  t )  =  C )
6 fveq2 5881 . . . . . . . 8  |-  ( s  =  S  ->  ( Base `  s )  =  ( Base `  S
) )
7 ismhm.b . . . . . . . 8  |-  B  =  ( Base `  S
)
86, 7syl6eqr 2488 . . . . . . 7  |-  ( s  =  S  ->  ( Base `  s )  =  B )
95, 8oveqan12rd 6325 . . . . . 6  |-  ( ( s  =  S  /\  t  =  T )  ->  ( ( Base `  t
)  ^m  ( Base `  s ) )  =  ( C  ^m  B
) )
108adantr 466 . . . . . . . 8  |-  ( ( s  =  S  /\  t  =  T )  ->  ( Base `  s
)  =  B )
11 fveq2 5881 . . . . . . . . . . . . 13  |-  ( s  =  S  ->  ( +g  `  s )  =  ( +g  `  S
) )
12 ismhm.p . . . . . . . . . . . . 13  |-  .+  =  ( +g  `  S )
1311, 12syl6eqr 2488 . . . . . . . . . . . 12  |-  ( s  =  S  ->  ( +g  `  s )  = 
.+  )
1413oveqd 6322 . . . . . . . . . . 11  |-  ( s  =  S  ->  (
x ( +g  `  s
) y )  =  ( x  .+  y
) )
1514fveq2d 5885 . . . . . . . . . 10  |-  ( s  =  S  ->  (
f `  ( x
( +g  `  s ) y ) )  =  ( f `  (
x  .+  y )
) )
16 fveq2 5881 . . . . . . . . . . . 12  |-  ( t  =  T  ->  ( +g  `  t )  =  ( +g  `  T
) )
17 ismhm.q . . . . . . . . . . . 12  |-  .+^  =  ( +g  `  T )
1816, 17syl6eqr 2488 . . . . . . . . . . 11  |-  ( t  =  T  ->  ( +g  `  t )  = 
.+^  )
1918oveqd 6322 . . . . . . . . . 10  |-  ( t  =  T  ->  (
( f `  x
) ( +g  `  t
) ( f `  y ) )  =  ( ( f `  x )  .+^  ( f `
 y ) ) )
2015, 19eqeqan12d 2452 . . . . . . . . 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 3046 . . . . . . . 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 3046 . . . . . . 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 5881 . . . . . . . . . 10  |-  ( s  =  S  ->  ( 0g `  s )  =  ( 0g `  S
) )
24 ismhm.z . . . . . . . . . 10  |-  .0.  =  ( 0g `  S )
2523, 24syl6eqr 2488 . . . . . . . . 9  |-  ( s  =  S  ->  ( 0g `  s )  =  .0.  )
2625fveq2d 5885 . . . . . . . 8  |-  ( s  =  S  ->  (
f `  ( 0g `  s ) )  =  ( f `  .0.  ) )
27 fveq2 5881 . . . . . . . . 9  |-  ( t  =  T  ->  ( 0g `  t )  =  ( 0g `  T
) )
28 ismhm.y . . . . . . . . 9  |-  Y  =  ( 0g `  T
)
2927, 28syl6eqr 2488 . . . . . . . 8  |-  ( t  =  T  ->  ( 0g `  t )  =  Y )
3026, 29eqeqan12d 2452 . . . . . . 7  |-  ( ( s  =  S  /\  t  =  T )  ->  ( ( f `  ( 0g `  s ) )  =  ( 0g
`  t )  <->  ( f `  .0.  )  =  Y ) )
3122, 30anbi12d 715 . . . . . 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 3082 . . . . 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 6333 . . . . . 6  |-  ( C  ^m  B )  e. 
_V
3433rabex 4576 . . . . 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 6441 . . . 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 2499 . . 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 5891 . . . . . . 7  |-  ( Base `  T )  e.  _V
384, 37eqeltri 2513 . . . . . 6  |-  C  e. 
_V
39 fvex 5891 . . . . . . 7  |-  ( Base `  S )  e.  _V
407, 39eqeltri 2513 . . . . . 6  |-  B  e. 
_V
4138, 40elmap 7508 . . . . 5  |-  ( F  e.  ( C  ^m  B )  <->  F : B
--> C )
4241anbi1i 699 . . . 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 5880 . . . . . . . 8  |-  ( f  =  F  ->  (
f `  ( x  .+  y ) )  =  ( F `  (
x  .+  y )
) )
44 fveq1 5880 . . . . . . . . 9  |-  ( f  =  F  ->  (
f `  x )  =  ( F `  x ) )
45 fveq1 5880 . . . . . . . . 9  |-  ( f  =  F  ->  (
f `  y )  =  ( F `  y ) )
4644, 45oveq12d 6323 . . . . . . . 8  |-  ( f  =  F  ->  (
( f `  x
)  .+^  ( f `  y ) )  =  ( ( F `  x )  .+^  ( F `
 y ) ) )
4743, 46eqeq12d 2451 . . . . . . 7  |-  ( f  =  F  ->  (
( f `  (
x  .+  y )
)  =  ( ( f `  x ) 
.+^  ( f `  y ) )  <->  ( F `  ( x  .+  y
) )  =  ( ( F `  x
)  .+^  ( F `  y ) ) ) )
48472ralbidv 2876 . . . . . 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 5880 . . . . . . 7  |-  ( f  =  F  ->  (
f `  .0.  )  =  ( F `  .0.  ) )
5049eqeq1d 2431 . . . . . 6  |-  ( f  =  F  ->  (
( f `  .0.  )  =  Y  <->  ( F `  .0.  )  =  Y ) )
5148, 50anbi12d 715 . . . . 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 3235 . . . 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 986 . . . 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 280 . . 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 264 . 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 646 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 setvar class
Syntax hints:    <-> wb 187    /\ wa 370    /\ w3a 982    = wceq 1437    e. wcel 1870   A.wral 2782   {crab 2786   _Vcvv 3087   -->wf 5597   ` cfv 5601  (class class class)co 6305    ^m cmap 7480   Basecbs 15084   +g cplusg 15152   0gc0g 15297   Mndcmnd 16486   MndHom cmhm 16531
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-8 1872  ax-9 1874  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407  ax-sep 4548  ax-nul 4556  ax-pow 4603  ax-pr 4661  ax-un 6597
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-eu 2270  df-mo 2271  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-ne 2627  df-ral 2787  df-rex 2788  df-rab 2791  df-v 3089  df-sbc 3306  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-nul 3768  df-if 3916  df-pw 3987  df-sn 4003  df-pr 4005  df-op 4009  df-uni 4223  df-br 4427  df-opab 4485  df-id 4769  df-xp 4860  df-rel 4861  df-cnv 4862  df-co 4863  df-dm 4864  df-rn 4865  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-fv 5609  df-ov 6308  df-oprab 6309  df-mpt2 6310  df-map 7482  df-mhm 16533
This theorem is referenced by:  mhmf  16538  mhmpropd  16539  mhmlin  16540  mhm0  16541  idmhm  16542  mhmf1o  16543  0mhm  16556  resmhm  16557  resmhm2  16558  resmhm2b  16559  mhmco  16560  prdspjmhm  16565  pwsdiagmhm  16567  pwsco1mhm  16568  pwsco2mhm  16569  frmdup1  16599  mhmfmhm  16760  ghmmhm  16844  frgpmhm  17350  mulgmhm  17403  srglmhm  17703  srgrmhm  17704  dfrhm2  17880  isrhm2d  17891  expmhm  18970  mat1mhm  19440  scmatmhm  19490  mat2pmatmhm  19688  pm2mpmhm  19775  dchrelbas3  24029  xrge0iifmhm  28584  esumcocn  28740  elmrsubrn  29946  deg1mhm  35783  ismhm0  38572  mhmismgmhm  38573  c0mhm  38677
  Copyright terms: Public domain W3C validator