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

Theorem ismhm 17258
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 17256 . . 3 MndHom = (𝑠 ∈ Mnd, 𝑡 ∈ Mnd ↦ {𝑓 ∈ ((Base‘𝑡) ↑𝑚 (Base‘𝑠)) ∣ (∀𝑥 ∈ (Base‘𝑠)∀𝑦 ∈ (Base‘𝑠)(𝑓‘(𝑥(+g𝑠)𝑦)) = ((𝑓𝑥)(+g𝑡)(𝑓𝑦)) ∧ (𝑓‘(0g𝑠)) = (0g𝑡))})
21elmpt2cl 6829 . 2 (𝐹 ∈ (𝑆 MndHom 𝑇) → (𝑆 ∈ Mnd ∧ 𝑇 ∈ Mnd))
3 fveq2 6148 . . . . . . . 8 (𝑡 = 𝑇 → (Base‘𝑡) = (Base‘𝑇))
4 ismhm.c . . . . . . . 8 𝐶 = (Base‘𝑇)
53, 4syl6eqr 2673 . . . . . . 7 (𝑡 = 𝑇 → (Base‘𝑡) = 𝐶)
6 fveq2 6148 . . . . . . . 8 (𝑠 = 𝑆 → (Base‘𝑠) = (Base‘𝑆))
7 ismhm.b . . . . . . . 8 𝐵 = (Base‘𝑆)
86, 7syl6eqr 2673 . . . . . . 7 (𝑠 = 𝑆 → (Base‘𝑠) = 𝐵)
95, 8oveqan12rd 6624 . . . . . 6 ((𝑠 = 𝑆𝑡 = 𝑇) → ((Base‘𝑡) ↑𝑚 (Base‘𝑠)) = (𝐶𝑚 𝐵))
108adantr 481 . . . . . . . 8 ((𝑠 = 𝑆𝑡 = 𝑇) → (Base‘𝑠) = 𝐵)
11 fveq2 6148 . . . . . . . . . . . . 13 (𝑠 = 𝑆 → (+g𝑠) = (+g𝑆))
12 ismhm.p . . . . . . . . . . . . 13 + = (+g𝑆)
1311, 12syl6eqr 2673 . . . . . . . . . . . 12 (𝑠 = 𝑆 → (+g𝑠) = + )
1413oveqd 6621 . . . . . . . . . . 11 (𝑠 = 𝑆 → (𝑥(+g𝑠)𝑦) = (𝑥 + 𝑦))
1514fveq2d 6152 . . . . . . . . . 10 (𝑠 = 𝑆 → (𝑓‘(𝑥(+g𝑠)𝑦)) = (𝑓‘(𝑥 + 𝑦)))
16 fveq2 6148 . . . . . . . . . . . 12 (𝑡 = 𝑇 → (+g𝑡) = (+g𝑇))
17 ismhm.q . . . . . . . . . . . 12 = (+g𝑇)
1816, 17syl6eqr 2673 . . . . . . . . . . 11 (𝑡 = 𝑇 → (+g𝑡) = )
1918oveqd 6621 . . . . . . . . . 10 (𝑡 = 𝑇 → ((𝑓𝑥)(+g𝑡)(𝑓𝑦)) = ((𝑓𝑥) (𝑓𝑦)))
2015, 19eqeqan12d 2637 . . . . . . . . 9 ((𝑠 = 𝑆𝑡 = 𝑇) → ((𝑓‘(𝑥(+g𝑠)𝑦)) = ((𝑓𝑥)(+g𝑡)(𝑓𝑦)) ↔ (𝑓‘(𝑥 + 𝑦)) = ((𝑓𝑥) (𝑓𝑦))))
2110, 20raleqbidv 3141 . . . . . . . 8 ((𝑠 = 𝑆𝑡 = 𝑇) → (∀𝑦 ∈ (Base‘𝑠)(𝑓‘(𝑥(+g𝑠)𝑦)) = ((𝑓𝑥)(+g𝑡)(𝑓𝑦)) ↔ ∀𝑦𝐵 (𝑓‘(𝑥 + 𝑦)) = ((𝑓𝑥) (𝑓𝑦))))
2210, 21raleqbidv 3141 . . . . . . 7 ((𝑠 = 𝑆𝑡 = 𝑇) → (∀𝑥 ∈ (Base‘𝑠)∀𝑦 ∈ (Base‘𝑠)(𝑓‘(𝑥(+g𝑠)𝑦)) = ((𝑓𝑥)(+g𝑡)(𝑓𝑦)) ↔ ∀𝑥𝐵𝑦𝐵 (𝑓‘(𝑥 + 𝑦)) = ((𝑓𝑥) (𝑓𝑦))))
23 fveq2 6148 . . . . . . . . . 10 (𝑠 = 𝑆 → (0g𝑠) = (0g𝑆))
24 ismhm.z . . . . . . . . . 10 0 = (0g𝑆)
2523, 24syl6eqr 2673 . . . . . . . . 9 (𝑠 = 𝑆 → (0g𝑠) = 0 )
2625fveq2d 6152 . . . . . . . 8 (𝑠 = 𝑆 → (𝑓‘(0g𝑠)) = (𝑓0 ))
27 fveq2 6148 . . . . . . . . 9 (𝑡 = 𝑇 → (0g𝑡) = (0g𝑇))
28 ismhm.y . . . . . . . . 9 𝑌 = (0g𝑇)
2927, 28syl6eqr 2673 . . . . . . . 8 (𝑡 = 𝑇 → (0g𝑡) = 𝑌)
3026, 29eqeqan12d 2637 . . . . . . 7 ((𝑠 = 𝑆𝑡 = 𝑇) → ((𝑓‘(0g𝑠)) = (0g𝑡) ↔ (𝑓0 ) = 𝑌))
3122, 30anbi12d 746 . . . . . 6 ((𝑠 = 𝑆𝑡 = 𝑇) → ((∀𝑥 ∈ (Base‘𝑠)∀𝑦 ∈ (Base‘𝑠)(𝑓‘(𝑥(+g𝑠)𝑦)) = ((𝑓𝑥)(+g𝑡)(𝑓𝑦)) ∧ (𝑓‘(0g𝑠)) = (0g𝑡)) ↔ (∀𝑥𝐵𝑦𝐵 (𝑓‘(𝑥 + 𝑦)) = ((𝑓𝑥) (𝑓𝑦)) ∧ (𝑓0 ) = 𝑌)))
329, 31rabeqbidv 3181 . . . . 5 ((𝑠 = 𝑆𝑡 = 𝑇) → {𝑓 ∈ ((Base‘𝑡) ↑𝑚 (Base‘𝑠)) ∣ (∀𝑥 ∈ (Base‘𝑠)∀𝑦 ∈ (Base‘𝑠)(𝑓‘(𝑥(+g𝑠)𝑦)) = ((𝑓𝑥)(+g𝑡)(𝑓𝑦)) ∧ (𝑓‘(0g𝑠)) = (0g𝑡))} = {𝑓 ∈ (𝐶𝑚 𝐵) ∣ (∀𝑥𝐵𝑦𝐵 (𝑓‘(𝑥 + 𝑦)) = ((𝑓𝑥) (𝑓𝑦)) ∧ (𝑓0 ) = 𝑌)})
33 ovex 6632 . . . . . 6 (𝐶𝑚 𝐵) ∈ V
3433rabex 4773 . . . . 5 {𝑓 ∈ (𝐶𝑚 𝐵) ∣ (∀𝑥𝐵𝑦𝐵 (𝑓‘(𝑥 + 𝑦)) = ((𝑓𝑥) (𝑓𝑦)) ∧ (𝑓0 ) = 𝑌)} ∈ V
3532, 1, 34ovmpt2a 6744 . . . 4 ((𝑆 ∈ Mnd ∧ 𝑇 ∈ Mnd) → (𝑆 MndHom 𝑇) = {𝑓 ∈ (𝐶𝑚 𝐵) ∣ (∀𝑥𝐵𝑦𝐵 (𝑓‘(𝑥 + 𝑦)) = ((𝑓𝑥) (𝑓𝑦)) ∧ (𝑓0 ) = 𝑌)})
3635eleq2d 2684 . . 3 ((𝑆 ∈ Mnd ∧ 𝑇 ∈ Mnd) → (𝐹 ∈ (𝑆 MndHom 𝑇) ↔ 𝐹 ∈ {𝑓 ∈ (𝐶𝑚 𝐵) ∣ (∀𝑥𝐵𝑦𝐵 (𝑓‘(𝑥 + 𝑦)) = ((𝑓𝑥) (𝑓𝑦)) ∧ (𝑓0 ) = 𝑌)}))
37 fvex 6158 . . . . . . 7 (Base‘𝑇) ∈ V
384, 37eqeltri 2694 . . . . . 6 𝐶 ∈ V
39 fvex 6158 . . . . . . 7 (Base‘𝑆) ∈ V
407, 39eqeltri 2694 . . . . . 6 𝐵 ∈ V
4138, 40elmap 7830 . . . . 5 (𝐹 ∈ (𝐶𝑚 𝐵) ↔ 𝐹:𝐵𝐶)
4241anbi1i 730 . . . 4 ((𝐹 ∈ (𝐶𝑚 𝐵) ∧ (∀𝑥𝐵𝑦𝐵 (𝐹‘(𝑥 + 𝑦)) = ((𝐹𝑥) (𝐹𝑦)) ∧ (𝐹0 ) = 𝑌)) ↔ (𝐹:𝐵𝐶 ∧ (∀𝑥𝐵𝑦𝐵 (𝐹‘(𝑥 + 𝑦)) = ((𝐹𝑥) (𝐹𝑦)) ∧ (𝐹0 ) = 𝑌)))
43 fveq1 6147 . . . . . . . 8 (𝑓 = 𝐹 → (𝑓‘(𝑥 + 𝑦)) = (𝐹‘(𝑥 + 𝑦)))
44 fveq1 6147 . . . . . . . . 9 (𝑓 = 𝐹 → (𝑓𝑥) = (𝐹𝑥))
45 fveq1 6147 . . . . . . . . 9 (𝑓 = 𝐹 → (𝑓𝑦) = (𝐹𝑦))
4644, 45oveq12d 6622 . . . . . . . 8 (𝑓 = 𝐹 → ((𝑓𝑥) (𝑓𝑦)) = ((𝐹𝑥) (𝐹𝑦)))
4743, 46eqeq12d 2636 . . . . . . 7 (𝑓 = 𝐹 → ((𝑓‘(𝑥 + 𝑦)) = ((𝑓𝑥) (𝑓𝑦)) ↔ (𝐹‘(𝑥 + 𝑦)) = ((𝐹𝑥) (𝐹𝑦))))
48472ralbidv 2983 . . . . . 6 (𝑓 = 𝐹 → (∀𝑥𝐵𝑦𝐵 (𝑓‘(𝑥 + 𝑦)) = ((𝑓𝑥) (𝑓𝑦)) ↔ ∀𝑥𝐵𝑦𝐵 (𝐹‘(𝑥 + 𝑦)) = ((𝐹𝑥) (𝐹𝑦))))
49 fveq1 6147 . . . . . . 7 (𝑓 = 𝐹 → (𝑓0 ) = (𝐹0 ))
5049eqeq1d 2623 . . . . . 6 (𝑓 = 𝐹 → ((𝑓0 ) = 𝑌 ↔ (𝐹0 ) = 𝑌))
5148, 50anbi12d 746 . . . . 5 (𝑓 = 𝐹 → ((∀𝑥𝐵𝑦𝐵 (𝑓‘(𝑥 + 𝑦)) = ((𝑓𝑥) (𝑓𝑦)) ∧ (𝑓0 ) = 𝑌) ↔ (∀𝑥𝐵𝑦𝐵 (𝐹‘(𝑥 + 𝑦)) = ((𝐹𝑥) (𝐹𝑦)) ∧ (𝐹0 ) = 𝑌)))
5251elrab 3346 . . . 4 (𝐹 ∈ {𝑓 ∈ (𝐶𝑚 𝐵) ∣ (∀𝑥𝐵𝑦𝐵 (𝑓‘(𝑥 + 𝑦)) = ((𝑓𝑥) (𝑓𝑦)) ∧ (𝑓0 ) = 𝑌)} ↔ (𝐹 ∈ (𝐶𝑚 𝐵) ∧ (∀𝑥𝐵𝑦𝐵 (𝐹‘(𝑥 + 𝑦)) = ((𝐹𝑥) (𝐹𝑦)) ∧ (𝐹0 ) = 𝑌)))
53 3anass 1040 . . . 4 ((𝐹:𝐵𝐶 ∧ ∀𝑥𝐵𝑦𝐵 (𝐹‘(𝑥 + 𝑦)) = ((𝐹𝑥) (𝐹𝑦)) ∧ (𝐹0 ) = 𝑌) ↔ (𝐹:𝐵𝐶 ∧ (∀𝑥𝐵𝑦𝐵 (𝐹‘(𝑥 + 𝑦)) = ((𝐹𝑥) (𝐹𝑦)) ∧ (𝐹0 ) = 𝑌)))
5442, 52, 533bitr4i 292 . . 3 (𝐹 ∈ {𝑓 ∈ (𝐶𝑚 𝐵) ∣ (∀𝑥𝐵𝑦𝐵 (𝑓‘(𝑥 + 𝑦)) = ((𝑓𝑥) (𝑓𝑦)) ∧ (𝑓0 ) = 𝑌)} ↔ (𝐹:𝐵𝐶 ∧ ∀𝑥𝐵𝑦𝐵 (𝐹‘(𝑥 + 𝑦)) = ((𝐹𝑥) (𝐹𝑦)) ∧ (𝐹0 ) = 𝑌))
5536, 54syl6bb 276 . 2 ((𝑆 ∈ Mnd ∧ 𝑇 ∈ Mnd) → (𝐹 ∈ (𝑆 MndHom 𝑇) ↔ (𝐹:𝐵𝐶 ∧ ∀𝑥𝐵𝑦𝐵 (𝐹‘(𝑥 + 𝑦)) = ((𝐹𝑥) (𝐹𝑦)) ∧ (𝐹0 ) = 𝑌)))
562, 55biadan2 673 1 (𝐹 ∈ (𝑆 MndHom 𝑇) ↔ ((𝑆 ∈ Mnd ∧ 𝑇 ∈ Mnd) ∧ (𝐹:𝐵𝐶 ∧ ∀𝑥𝐵𝑦𝐵 (𝐹‘(𝑥 + 𝑦)) = ((𝐹𝑥) (𝐹𝑦)) ∧ (𝐹0 ) = 𝑌)))
Colors of variables: wff setvar class
Syntax hints:  wb 196  wa 384  w3a 1036   = wceq 1480  wcel 1987  wral 2907  {crab 2911  Vcvv 3186  wf 5843  cfv 5847  (class class class)co 6604  𝑚 cmap 7802  Basecbs 15781  +gcplusg 15862  0gc0g 16021  Mndcmnd 17215   MndHom cmhm 17254
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4741  ax-nul 4749  ax-pow 4803  ax-pr 4867  ax-un 6902
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2912  df-rex 2913  df-rab 2916  df-v 3188  df-sbc 3418  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-nul 3892  df-if 4059  df-pw 4132  df-sn 4149  df-pr 4151  df-op 4155  df-uni 4403  df-br 4614  df-opab 4674  df-id 4989  df-xp 5080  df-rel 5081  df-cnv 5082  df-co 5083  df-dm 5084  df-rn 5085  df-iota 5810  df-fun 5849  df-fn 5850  df-f 5851  df-fv 5855  df-ov 6607  df-oprab 6608  df-mpt2 6609  df-map 7804  df-mhm 17256
This theorem is referenced by:  mhmf  17261  mhmpropd  17262  mhmlin  17263  mhm0  17264  idmhm  17265  mhmf1o  17266  0mhm  17279  resmhm  17280  resmhm2  17281  resmhm2b  17282  mhmco  17283  prdspjmhm  17288  pwsdiagmhm  17290  pwsco1mhm  17291  pwsco2mhm  17292  frmdup1  17322  mhmfmhm  17459  ghmmhm  17591  frgpmhm  18099  mulgmhm  18154  srglmhm  18456  srgrmhm  18457  dfrhm2  18638  isrhm2d  18649  expmhm  19734  mat1mhm  20209  scmatmhm  20259  mat2pmatmhm  20457  pm2mpmhm  20544  dchrelbas3  24863  xrge0iifmhm  29767  esumcocn  29923  elmrsubrn  31125  deg1mhm  37266  ismhm0  41093  mhmismgmhm  41094  c0mhm  41198
  Copyright terms: Public domain W3C validator