| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > ghmmhm | Structured version Visualization version GIF version | ||
| Description: A group homomorphism is a monoid homomorphism. (Contributed by Stefan O'Rear, 7-Mar-2015.) |
| Ref | Expression |
|---|---|
| ghmmhm | ⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → 𝐹 ∈ (𝑆 MndHom 𝑇)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ghmgrp1 19133 | . . 3 ⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → 𝑆 ∈ Grp) | |
| 2 | 1 | grpmndd 18861 | . 2 ⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → 𝑆 ∈ Mnd) |
| 3 | ghmgrp2 19134 | . . 3 ⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → 𝑇 ∈ Grp) | |
| 4 | 3 | grpmndd 18861 | . 2 ⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → 𝑇 ∈ Mnd) |
| 5 | eqid 2729 | . . . 4 ⊢ (Base‘𝑆) = (Base‘𝑆) | |
| 6 | eqid 2729 | . . . 4 ⊢ (Base‘𝑇) = (Base‘𝑇) | |
| 7 | 5, 6 | ghmf 19135 | . . 3 ⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → 𝐹:(Base‘𝑆)⟶(Base‘𝑇)) |
| 8 | eqid 2729 | . . . . . 6 ⊢ (+g‘𝑆) = (+g‘𝑆) | |
| 9 | eqid 2729 | . . . . . 6 ⊢ (+g‘𝑇) = (+g‘𝑇) | |
| 10 | 5, 8, 9 | ghmlin 19136 | . . . . 5 ⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆)) → (𝐹‘(𝑥(+g‘𝑆)𝑦)) = ((𝐹‘𝑥)(+g‘𝑇)(𝐹‘𝑦))) |
| 11 | 10 | 3expb 1120 | . . . 4 ⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆))) → (𝐹‘(𝑥(+g‘𝑆)𝑦)) = ((𝐹‘𝑥)(+g‘𝑇)(𝐹‘𝑦))) |
| 12 | 11 | ralrimivva 3178 | . . 3 ⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → ∀𝑥 ∈ (Base‘𝑆)∀𝑦 ∈ (Base‘𝑆)(𝐹‘(𝑥(+g‘𝑆)𝑦)) = ((𝐹‘𝑥)(+g‘𝑇)(𝐹‘𝑦))) |
| 13 | eqid 2729 | . . . 4 ⊢ (0g‘𝑆) = (0g‘𝑆) | |
| 14 | eqid 2729 | . . . 4 ⊢ (0g‘𝑇) = (0g‘𝑇) | |
| 15 | 13, 14 | ghmid 19137 | . . 3 ⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → (𝐹‘(0g‘𝑆)) = (0g‘𝑇)) |
| 16 | 7, 12, 15 | 3jca 1128 | . 2 ⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → (𝐹:(Base‘𝑆)⟶(Base‘𝑇) ∧ ∀𝑥 ∈ (Base‘𝑆)∀𝑦 ∈ (Base‘𝑆)(𝐹‘(𝑥(+g‘𝑆)𝑦)) = ((𝐹‘𝑥)(+g‘𝑇)(𝐹‘𝑦)) ∧ (𝐹‘(0g‘𝑆)) = (0g‘𝑇))) |
| 17 | 5, 6, 8, 9, 13, 14 | ismhm 18695 | . 2 ⊢ (𝐹 ∈ (𝑆 MndHom 𝑇) ↔ ((𝑆 ∈ Mnd ∧ 𝑇 ∈ Mnd) ∧ (𝐹:(Base‘𝑆)⟶(Base‘𝑇) ∧ ∀𝑥 ∈ (Base‘𝑆)∀𝑦 ∈ (Base‘𝑆)(𝐹‘(𝑥(+g‘𝑆)𝑦)) = ((𝐹‘𝑥)(+g‘𝑇)(𝐹‘𝑦)) ∧ (𝐹‘(0g‘𝑆)) = (0g‘𝑇)))) |
| 18 | 2, 4, 16, 17 | syl21anbrc 1345 | 1 ⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → 𝐹 ∈ (𝑆 MndHom 𝑇)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ w3a 1086 = wceq 1540 ∈ wcel 2109 ∀wral 3044 ⟶wf 6495 ‘cfv 6499 (class class class)co 7369 Basecbs 17156 +gcplusg 17197 0gc0g 17379 Mndcmnd 18644 MndHom cmhm 18691 GrpHom cghm 19127 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-sep 5246 ax-nul 5256 ax-pow 5315 ax-pr 5382 ax-un 7691 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-ral 3045 df-rex 3054 df-rmo 3351 df-reu 3352 df-rab 3403 df-v 3446 df-sbc 3751 df-csb 3860 df-dif 3914 df-un 3916 df-in 3918 df-ss 3928 df-nul 4293 df-if 4485 df-pw 4561 df-sn 4586 df-pr 4588 df-op 4592 df-uni 4868 df-iun 4953 df-br 5103 df-opab 5165 df-mpt 5184 df-id 5526 df-xp 5637 df-rel 5638 df-cnv 5639 df-co 5640 df-dm 5641 df-rn 5642 df-res 5643 df-ima 5644 df-iota 6452 df-fun 6501 df-fn 6502 df-f 6503 df-fv 6507 df-riota 7326 df-ov 7372 df-oprab 7373 df-mpo 7374 df-1st 7947 df-2nd 7948 df-map 8778 df-0g 17381 df-mgm 18550 df-sgrp 18629 df-mnd 18645 df-mhm 18693 df-grp 18851 df-ghm 19128 |
| This theorem is referenced by: ghmmhmb 19142 ghmmulg 19143 resghm2 19148 ghmco 19151 ghmeql 19154 symgtrinv 19387 frgpup3lem 19692 gsummulglem 19856 gsumzinv 19860 gsuminv 19861 gsummulc1OLD 20235 gsummulc2OLD 20236 gsummulc1 20237 gsummulc2 20238 pwsco2rhm 20424 gsumvsmul 20865 rhmpreimaidl 21220 zrhpsgnmhm 21527 evlslem2 22020 evlsgsumadd 22032 evls1gsumadd 22245 rhmcomulmpl 22303 rhmmpl 22304 rhmply1vsca 22309 mat2pmatmul 22652 pm2mp 22746 cayhamlem4 22809 tsmsinv 24069 plypf1 26151 amgmlem 26934 lgseisenlem4 27323 gsumvsmul1 33035 gsummulgc2 33044 algextdeglem8 33708 rhmcomulpsr 42533 rhmpsr 42534 selvcllem4 42563 selvvvval 42567 evlselv 42569 selvadd 42570 selvmul 42571 mendring 43171 amgmwlem 49785 amgmlemALT 49786 |
| Copyright terms: Public domain | W3C validator |