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

Theorem ismhm 17538
Description: Property of a monoid homomorphism. (Contributed by Mario Carneiro, 7-Mar-2015.)
Hypotheses
Ref Expression
ismhm.b 𝐵 = (Base‘𝑆)
ismhm.c 𝐶 = (Base‘𝑇)
ismhm.p + = (+g𝑆)
ismhm.q = (+g𝑇)
ismhm.z 0 = (0g𝑆)
ismhm.y 𝑌 = (0g𝑇)
Assertion
Ref Expression
ismhm (𝐹 ∈ (𝑆 MndHom 𝑇) ↔ ((𝑆 ∈ Mnd ∧ 𝑇 ∈ Mnd) ∧ (𝐹:𝐵𝐶 ∧ ∀𝑥𝐵𝑦𝐵 (𝐹‘(𝑥 + 𝑦)) = ((𝐹𝑥) (𝐹𝑦)) ∧ (𝐹0 ) = 𝑌)))
Distinct variable groups:   𝑥,𝑦,𝐵   𝑥,𝑆,𝑦   𝑥,𝑇,𝑦   𝑥,𝐹,𝑦
Allowed substitution hints:   𝐶(𝑥,𝑦)   + (𝑥,𝑦)   (𝑥,𝑦)   𝑌(𝑥,𝑦)   0 (𝑥,𝑦)

Proof of Theorem ismhm
Dummy variables 𝑓 𝑠 𝑡 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-mhm 17536 . . 3 MndHom = (𝑠 ∈ Mnd, 𝑡 ∈ Mnd ↦ {𝑓 ∈ ((Base‘𝑡) ↑𝑚 (Base‘𝑠)) ∣ (∀𝑥 ∈ (Base‘𝑠)∀𝑦 ∈ (Base‘𝑠)(𝑓‘(𝑥(+g𝑠)𝑦)) = ((𝑓𝑥)(+g𝑡)(𝑓𝑦)) ∧ (𝑓‘(0g𝑠)) = (0g𝑡))})
21elmpt2cl 7041 . 2 (𝐹 ∈ (𝑆 MndHom 𝑇) → (𝑆 ∈ Mnd ∧ 𝑇 ∈ Mnd))
3 fveq2 6352 . . . . . . . 8 (𝑡 = 𝑇 → (Base‘𝑡) = (Base‘𝑇))
4 ismhm.c . . . . . . . 8 𝐶 = (Base‘𝑇)
53, 4syl6eqr 2812 . . . . . . 7 (𝑡 = 𝑇 → (Base‘𝑡) = 𝐶)
6 fveq2 6352 . . . . . . . 8 (𝑠 = 𝑆 → (Base‘𝑠) = (Base‘𝑆))
7 ismhm.b . . . . . . . 8 𝐵 = (Base‘𝑆)
86, 7syl6eqr 2812 . . . . . . 7 (𝑠 = 𝑆 → (Base‘𝑠) = 𝐵)
95, 8oveqan12rd 6833 . . . . . 6 ((𝑠 = 𝑆𝑡 = 𝑇) → ((Base‘𝑡) ↑𝑚 (Base‘𝑠)) = (𝐶𝑚 𝐵))
108adantr 472 . . . . . . . 8 ((𝑠 = 𝑆𝑡 = 𝑇) → (Base‘𝑠) = 𝐵)
11 fveq2 6352 . . . . . . . . . . . . 13 (𝑠 = 𝑆 → (+g𝑠) = (+g𝑆))
12 ismhm.p . . . . . . . . . . . . 13 + = (+g𝑆)
1311, 12syl6eqr 2812 . . . . . . . . . . . 12 (𝑠 = 𝑆 → (+g𝑠) = + )
1413oveqd 6830 . . . . . . . . . . 11 (𝑠 = 𝑆 → (𝑥(+g𝑠)𝑦) = (𝑥 + 𝑦))
1514fveq2d 6356 . . . . . . . . . 10 (𝑠 = 𝑆 → (𝑓‘(𝑥(+g𝑠)𝑦)) = (𝑓‘(𝑥 + 𝑦)))
16 fveq2 6352 . . . . . . . . . . . 12 (𝑡 = 𝑇 → (+g𝑡) = (+g𝑇))
17 ismhm.q . . . . . . . . . . . 12 = (+g𝑇)
1816, 17syl6eqr 2812 . . . . . . . . . . 11 (𝑡 = 𝑇 → (+g𝑡) = )
1918oveqd 6830 . . . . . . . . . 10 (𝑡 = 𝑇 → ((𝑓𝑥)(+g𝑡)(𝑓𝑦)) = ((𝑓𝑥) (𝑓𝑦)))
2015, 19eqeqan12d 2776 . . . . . . . . 9 ((𝑠 = 𝑆𝑡 = 𝑇) → ((𝑓‘(𝑥(+g𝑠)𝑦)) = ((𝑓𝑥)(+g𝑡)(𝑓𝑦)) ↔ (𝑓‘(𝑥 + 𝑦)) = ((𝑓𝑥) (𝑓𝑦))))
2110, 20raleqbidv 3291 . . . . . . . 8 ((𝑠 = 𝑆𝑡 = 𝑇) → (∀𝑦 ∈ (Base‘𝑠)(𝑓‘(𝑥(+g𝑠)𝑦)) = ((𝑓𝑥)(+g𝑡)(𝑓𝑦)) ↔ ∀𝑦𝐵 (𝑓‘(𝑥 + 𝑦)) = ((𝑓𝑥) (𝑓𝑦))))
2210, 21raleqbidv 3291 . . . . . . 7 ((𝑠 = 𝑆𝑡 = 𝑇) → (∀𝑥 ∈ (Base‘𝑠)∀𝑦 ∈ (Base‘𝑠)(𝑓‘(𝑥(+g𝑠)𝑦)) = ((𝑓𝑥)(+g𝑡)(𝑓𝑦)) ↔ ∀𝑥𝐵𝑦𝐵 (𝑓‘(𝑥 + 𝑦)) = ((𝑓𝑥) (𝑓𝑦))))
23 fveq2 6352 . . . . . . . . . 10 (𝑠 = 𝑆 → (0g𝑠) = (0g𝑆))
24 ismhm.z . . . . . . . . . 10 0 = (0g𝑆)
2523, 24syl6eqr 2812 . . . . . . . . 9 (𝑠 = 𝑆 → (0g𝑠) = 0 )
2625fveq2d 6356 . . . . . . . 8 (𝑠 = 𝑆 → (𝑓‘(0g𝑠)) = (𝑓0 ))
27 fveq2 6352 . . . . . . . . 9 (𝑡 = 𝑇 → (0g𝑡) = (0g𝑇))
28 ismhm.y . . . . . . . . 9 𝑌 = (0g𝑇)
2927, 28syl6eqr 2812 . . . . . . . 8 (𝑡 = 𝑇 → (0g𝑡) = 𝑌)
3026, 29eqeqan12d 2776 . . . . . . 7 ((𝑠 = 𝑆𝑡 = 𝑇) → ((𝑓‘(0g𝑠)) = (0g𝑡) ↔ (𝑓0 ) = 𝑌))
3122, 30anbi12d 749 . . . . . 6 ((𝑠 = 𝑆𝑡 = 𝑇) → ((∀𝑥 ∈ (Base‘𝑠)∀𝑦 ∈ (Base‘𝑠)(𝑓‘(𝑥(+g𝑠)𝑦)) = ((𝑓𝑥)(+g𝑡)(𝑓𝑦)) ∧ (𝑓‘(0g𝑠)) = (0g𝑡)) ↔ (∀𝑥𝐵𝑦𝐵 (𝑓‘(𝑥 + 𝑦)) = ((𝑓𝑥) (𝑓𝑦)) ∧ (𝑓0 ) = 𝑌)))
329, 31rabeqbidv 3335 . . . . 5 ((𝑠 = 𝑆𝑡 = 𝑇) → {𝑓 ∈ ((Base‘𝑡) ↑𝑚 (Base‘𝑠)) ∣ (∀𝑥 ∈ (Base‘𝑠)∀𝑦 ∈ (Base‘𝑠)(𝑓‘(𝑥(+g𝑠)𝑦)) = ((𝑓𝑥)(+g𝑡)(𝑓𝑦)) ∧ (𝑓‘(0g𝑠)) = (0g𝑡))} = {𝑓 ∈ (𝐶𝑚 𝐵) ∣ (∀𝑥𝐵𝑦𝐵 (𝑓‘(𝑥 + 𝑦)) = ((𝑓𝑥) (𝑓𝑦)) ∧ (𝑓0 ) = 𝑌)})
33 ovex 6841 . . . . . 6 (𝐶𝑚 𝐵) ∈ V
3433rabex 4964 . . . . 5 {𝑓 ∈ (𝐶𝑚 𝐵) ∣ (∀𝑥𝐵𝑦𝐵 (𝑓‘(𝑥 + 𝑦)) = ((𝑓𝑥) (𝑓𝑦)) ∧ (𝑓0 ) = 𝑌)} ∈ V
3532, 1, 34ovmpt2a 6956 . . . 4 ((𝑆 ∈ Mnd ∧ 𝑇 ∈ Mnd) → (𝑆 MndHom 𝑇) = {𝑓 ∈ (𝐶𝑚 𝐵) ∣ (∀𝑥𝐵𝑦𝐵 (𝑓‘(𝑥 + 𝑦)) = ((𝑓𝑥) (𝑓𝑦)) ∧ (𝑓0 ) = 𝑌)})
3635eleq2d 2825 . . 3 ((𝑆 ∈ Mnd ∧ 𝑇 ∈ Mnd) → (𝐹 ∈ (𝑆 MndHom 𝑇) ↔ 𝐹 ∈ {𝑓 ∈ (𝐶𝑚 𝐵) ∣ (∀𝑥𝐵𝑦𝐵 (𝑓‘(𝑥 + 𝑦)) = ((𝑓𝑥) (𝑓𝑦)) ∧ (𝑓0 ) = 𝑌)}))
37 fvex 6362 . . . . . . 7 (Base‘𝑇) ∈ V
384, 37eqeltri 2835 . . . . . 6 𝐶 ∈ V
39 fvex 6362 . . . . . . 7 (Base‘𝑆) ∈ V
407, 39eqeltri 2835 . . . . . 6 𝐵 ∈ V
4138, 40elmap 8052 . . . . 5 (𝐹 ∈ (𝐶𝑚 𝐵) ↔ 𝐹:𝐵𝐶)
4241anbi1i 733 . . . 4 ((𝐹 ∈ (𝐶𝑚 𝐵) ∧ (∀𝑥𝐵𝑦𝐵 (𝐹‘(𝑥 + 𝑦)) = ((𝐹𝑥) (𝐹𝑦)) ∧ (𝐹0 ) = 𝑌)) ↔ (𝐹:𝐵𝐶 ∧ (∀𝑥𝐵𝑦𝐵 (𝐹‘(𝑥 + 𝑦)) = ((𝐹𝑥) (𝐹𝑦)) ∧ (𝐹0 ) = 𝑌)))
43 fveq1 6351 . . . . . . . 8 (𝑓 = 𝐹 → (𝑓‘(𝑥 + 𝑦)) = (𝐹‘(𝑥 + 𝑦)))
44 fveq1 6351 . . . . . . . . 9 (𝑓 = 𝐹 → (𝑓𝑥) = (𝐹𝑥))
45 fveq1 6351 . . . . . . . . 9 (𝑓 = 𝐹 → (𝑓𝑦) = (𝐹𝑦))
4644, 45oveq12d 6831 . . . . . . . 8 (𝑓 = 𝐹 → ((𝑓𝑥) (𝑓𝑦)) = ((𝐹𝑥) (𝐹𝑦)))
4743, 46eqeq12d 2775 . . . . . . 7 (𝑓 = 𝐹 → ((𝑓‘(𝑥 + 𝑦)) = ((𝑓𝑥) (𝑓𝑦)) ↔ (𝐹‘(𝑥 + 𝑦)) = ((𝐹𝑥) (𝐹𝑦))))
48472ralbidv 3127 . . . . . 6 (𝑓 = 𝐹 → (∀𝑥𝐵𝑦𝐵 (𝑓‘(𝑥 + 𝑦)) = ((𝑓𝑥) (𝑓𝑦)) ↔ ∀𝑥𝐵𝑦𝐵 (𝐹‘(𝑥 + 𝑦)) = ((𝐹𝑥) (𝐹𝑦))))
49 fveq1 6351 . . . . . . 7 (𝑓 = 𝐹 → (𝑓0 ) = (𝐹0 ))
5049eqeq1d 2762 . . . . . 6 (𝑓 = 𝐹 → ((𝑓0 ) = 𝑌 ↔ (𝐹0 ) = 𝑌))
5148, 50anbi12d 749 . . . . 5 (𝑓 = 𝐹 → ((∀𝑥𝐵𝑦𝐵 (𝑓‘(𝑥 + 𝑦)) = ((𝑓𝑥) (𝑓𝑦)) ∧ (𝑓0 ) = 𝑌) ↔ (∀𝑥𝐵𝑦𝐵 (𝐹‘(𝑥 + 𝑦)) = ((𝐹𝑥) (𝐹𝑦)) ∧ (𝐹0 ) = 𝑌)))
5251elrab 3504 . . . 4 (𝐹 ∈ {𝑓 ∈ (𝐶𝑚 𝐵) ∣ (∀𝑥𝐵𝑦𝐵 (𝑓‘(𝑥 + 𝑦)) = ((𝑓𝑥) (𝑓𝑦)) ∧ (𝑓0 ) = 𝑌)} ↔ (𝐹 ∈ (𝐶𝑚 𝐵) ∧ (∀𝑥𝐵𝑦𝐵 (𝐹‘(𝑥 + 𝑦)) = ((𝐹𝑥) (𝐹𝑦)) ∧ (𝐹0 ) = 𝑌)))
53 3anass 1081 . . . 4 ((𝐹:𝐵𝐶 ∧ ∀𝑥𝐵𝑦𝐵 (𝐹‘(𝑥 + 𝑦)) = ((𝐹𝑥) (𝐹𝑦)) ∧ (𝐹0 ) = 𝑌) ↔ (𝐹:𝐵𝐶 ∧ (∀𝑥𝐵𝑦𝐵 (𝐹‘(𝑥 + 𝑦)) = ((𝐹𝑥) (𝐹𝑦)) ∧ (𝐹0 ) = 𝑌)))
5442, 52, 533bitr4i 292 . . 3 (𝐹 ∈ {𝑓 ∈ (𝐶𝑚 𝐵) ∣ (∀𝑥𝐵𝑦𝐵 (𝑓‘(𝑥 + 𝑦)) = ((𝑓𝑥) (𝑓𝑦)) ∧ (𝑓0 ) = 𝑌)} ↔ (𝐹:𝐵𝐶 ∧ ∀𝑥𝐵𝑦𝐵 (𝐹‘(𝑥 + 𝑦)) = ((𝐹𝑥) (𝐹𝑦)) ∧ (𝐹0 ) = 𝑌))
5536, 54syl6bb 276 . 2 ((𝑆 ∈ Mnd ∧ 𝑇 ∈ Mnd) → (𝐹 ∈ (𝑆 MndHom 𝑇) ↔ (𝐹:𝐵𝐶 ∧ ∀𝑥𝐵𝑦𝐵 (𝐹‘(𝑥 + 𝑦)) = ((𝐹𝑥) (𝐹𝑦)) ∧ (𝐹0 ) = 𝑌)))
562, 55biadan2 677 1 (𝐹 ∈ (𝑆 MndHom 𝑇) ↔ ((𝑆 ∈ Mnd ∧ 𝑇 ∈ Mnd) ∧ (𝐹:𝐵𝐶 ∧ ∀𝑥𝐵𝑦𝐵 (𝐹‘(𝑥 + 𝑦)) = ((𝐹𝑥) (𝐹𝑦)) ∧ (𝐹0 ) = 𝑌)))
Colors of variables: wff setvar class
Syntax hints:  wb 196  wa 383  w3a 1072   = wceq 1632  wcel 2139  wral 3050  {crab 3054  Vcvv 3340  wf 6045  cfv 6049  (class class class)co 6813  𝑚 cmap 8023  Basecbs 16059  +gcplusg 16143  0gc0g 16302  Mndcmnd 17495   MndHom cmhm 17534
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7114
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-ral 3055  df-rex 3056  df-rab 3059  df-v 3342  df-sbc 3577  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-op 4328  df-uni 4589  df-br 4805  df-opab 4865  df-id 5174  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-fv 6057  df-ov 6816  df-oprab 6817  df-mpt2 6818  df-map 8025  df-mhm 17536
This theorem is referenced by:  mhmf  17541  mhmpropd  17542  mhmlin  17543  mhm0  17544  idmhm  17545  mhmf1o  17546  0mhm  17559  resmhm  17560  resmhm2  17561  resmhm2b  17562  mhmco  17563  prdspjmhm  17568  pwsdiagmhm  17570  pwsco1mhm  17571  pwsco2mhm  17572  frmdup1  17602  mhmfmhm  17739  ghmmhm  17871  frgpmhm  18378  mulgmhm  18433  srglmhm  18735  srgrmhm  18736  dfrhm2  18919  isrhm2d  18930  expmhm  20017  mat1mhm  20492  scmatmhm  20542  mat2pmatmhm  20740  pm2mpmhm  20827  dchrelbas3  25162  xrge0iifmhm  30294  esumcocn  30451  elmrsubrn  31724  deg1mhm  38287  ismhm0  42315  mhmismgmhm  42316  c0mhm  42420
  Copyright terms: Public domain W3C validator