![]() |
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 19094 | . . 3 ⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → 𝑆 ∈ Grp) | |
2 | 1 | grpmndd 18832 | . 2 ⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → 𝑆 ∈ Mnd) |
3 | ghmgrp2 19095 | . . 3 ⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → 𝑇 ∈ Grp) | |
4 | 3 | grpmndd 18832 | . 2 ⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → 𝑇 ∈ Mnd) |
5 | eqid 2733 | . . . 4 ⊢ (Base‘𝑆) = (Base‘𝑆) | |
6 | eqid 2733 | . . . 4 ⊢ (Base‘𝑇) = (Base‘𝑇) | |
7 | 5, 6 | ghmf 19096 | . . 3 ⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → 𝐹:(Base‘𝑆)⟶(Base‘𝑇)) |
8 | eqid 2733 | . . . . . 6 ⊢ (+g‘𝑆) = (+g‘𝑆) | |
9 | eqid 2733 | . . . . . 6 ⊢ (+g‘𝑇) = (+g‘𝑇) | |
10 | 5, 8, 9 | ghmlin 19097 | . . . . 5 ⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆)) → (𝐹‘(𝑥(+g‘𝑆)𝑦)) = ((𝐹‘𝑥)(+g‘𝑇)(𝐹‘𝑦))) |
11 | 10 | 3expb 1121 | . . . 4 ⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆))) → (𝐹‘(𝑥(+g‘𝑆)𝑦)) = ((𝐹‘𝑥)(+g‘𝑇)(𝐹‘𝑦))) |
12 | 11 | ralrimivva 3201 | . . 3 ⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → ∀𝑥 ∈ (Base‘𝑆)∀𝑦 ∈ (Base‘𝑆)(𝐹‘(𝑥(+g‘𝑆)𝑦)) = ((𝐹‘𝑥)(+g‘𝑇)(𝐹‘𝑦))) |
13 | eqid 2733 | . . . 4 ⊢ (0g‘𝑆) = (0g‘𝑆) | |
14 | eqid 2733 | . . . 4 ⊢ (0g‘𝑇) = (0g‘𝑇) | |
15 | 13, 14 | ghmid 19098 | . . 3 ⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → (𝐹‘(0g‘𝑆)) = (0g‘𝑇)) |
16 | 7, 12, 15 | 3jca 1129 | . 2 ⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → (𝐹:(Base‘𝑆)⟶(Base‘𝑇) ∧ ∀𝑥 ∈ (Base‘𝑆)∀𝑦 ∈ (Base‘𝑆)(𝐹‘(𝑥(+g‘𝑆)𝑦)) = ((𝐹‘𝑥)(+g‘𝑇)(𝐹‘𝑦)) ∧ (𝐹‘(0g‘𝑆)) = (0g‘𝑇))) |
17 | 5, 6, 8, 9, 13, 14 | ismhm 18673 | . 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 1088 = wceq 1542 ∈ wcel 2107 ∀wral 3062 ⟶wf 6540 ‘cfv 6544 (class class class)co 7409 Basecbs 17144 +gcplusg 17197 0gc0g 17385 Mndcmnd 18625 MndHom cmhm 18669 GrpHom cghm 19089 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2704 ax-rep 5286 ax-sep 5300 ax-nul 5307 ax-pow 5364 ax-pr 5428 ax-un 7725 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2535 df-eu 2564 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2886 df-ne 2942 df-ral 3063 df-rex 3072 df-rmo 3377 df-reu 3378 df-rab 3434 df-v 3477 df-sbc 3779 df-csb 3895 df-dif 3952 df-un 3954 df-in 3956 df-ss 3966 df-nul 4324 df-if 4530 df-pw 4605 df-sn 4630 df-pr 4632 df-op 4636 df-uni 4910 df-iun 5000 df-br 5150 df-opab 5212 df-mpt 5233 df-id 5575 df-xp 5683 df-rel 5684 df-cnv 5685 df-co 5686 df-dm 5687 df-rn 5688 df-res 5689 df-ima 5690 df-iota 6496 df-fun 6546 df-fn 6547 df-f 6548 df-f1 6549 df-fo 6550 df-f1o 6551 df-fv 6552 df-riota 7365 df-ov 7412 df-oprab 7413 df-mpo 7414 df-map 8822 df-0g 17387 df-mgm 18561 df-sgrp 18610 df-mnd 18626 df-mhm 18671 df-grp 18822 df-ghm 19090 |
This theorem is referenced by: ghmmhmb 19103 ghmmulg 19104 resghm2 19109 ghmco 19112 ghmeql 19115 symgtrinv 19340 frgpup3lem 19645 gsummulglem 19809 gsumzinv 19813 gsuminv 19814 gsummulc1OLD 20126 gsummulc2OLD 20127 gsummulc1 20128 gsummulc2 20129 pwsco2rhm 20278 gsumvsmul 20536 zrhpsgnmhm 21137 evlslem2 21642 evlsgsumadd 21654 evls1gsumadd 21843 mat2pmatmul 22233 pm2mp 22327 cayhamlem4 22390 tsmsinv 23652 plypf1 25726 amgmlem 26494 lgseisenlem4 26881 gsumvsmul1 32203 rhmpreimaidl 32537 rhmcomulmpl 41124 rhmmpl 41125 selvcllem4 41153 selvvvval 41157 evlselv 41159 selvadd 41160 selvmul 41161 mendring 41934 amgmwlem 47849 amgmlemALT 47850 |
Copyright terms: Public domain | W3C validator |