![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > mhmlin | Structured version Visualization version GIF version |
Description: A monoid homomorphism commutes with composition. (Contributed by Mario Carneiro, 7-Mar-2015.) |
Ref | Expression |
---|---|
mhmlin.b | ⊢ 𝐵 = (Base‘𝑆) |
mhmlin.p | ⊢ + = (+g‘𝑆) |
mhmlin.q | ⊢ ⨣ = (+g‘𝑇) |
Ref | Expression |
---|---|
mhmlin | ⊢ ((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝐹‘(𝑋 + 𝑌)) = ((𝐹‘𝑋) ⨣ (𝐹‘𝑌))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mhmlin.b | . . . . . 6 ⊢ 𝐵 = (Base‘𝑆) | |
2 | eqid 2738 | . . . . . 6 ⊢ (Base‘𝑇) = (Base‘𝑇) | |
3 | mhmlin.p | . . . . . 6 ⊢ + = (+g‘𝑆) | |
4 | mhmlin.q | . . . . . 6 ⊢ ⨣ = (+g‘𝑇) | |
5 | eqid 2738 | . . . . . 6 ⊢ (0g‘𝑆) = (0g‘𝑆) | |
6 | eqid 2738 | . . . . . 6 ⊢ (0g‘𝑇) = (0g‘𝑇) | |
7 | 1, 2, 3, 4, 5, 6 | ismhm 18563 | . . . . 5 ⊢ (𝐹 ∈ (𝑆 MndHom 𝑇) ↔ ((𝑆 ∈ Mnd ∧ 𝑇 ∈ Mnd) ∧ (𝐹:𝐵⟶(Base‘𝑇) ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) ⨣ (𝐹‘𝑦)) ∧ (𝐹‘(0g‘𝑆)) = (0g‘𝑇)))) |
8 | 7 | simprbi 498 | . . . 4 ⊢ (𝐹 ∈ (𝑆 MndHom 𝑇) → (𝐹:𝐵⟶(Base‘𝑇) ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) ⨣ (𝐹‘𝑦)) ∧ (𝐹‘(0g‘𝑆)) = (0g‘𝑇))) |
9 | 8 | simp2d 1144 | . . 3 ⊢ (𝐹 ∈ (𝑆 MndHom 𝑇) → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) ⨣ (𝐹‘𝑦))) |
10 | fvoveq1 7375 | . . . . 5 ⊢ (𝑥 = 𝑋 → (𝐹‘(𝑥 + 𝑦)) = (𝐹‘(𝑋 + 𝑦))) | |
11 | fveq2 6840 | . . . . . 6 ⊢ (𝑥 = 𝑋 → (𝐹‘𝑥) = (𝐹‘𝑋)) | |
12 | 11 | oveq1d 7367 | . . . . 5 ⊢ (𝑥 = 𝑋 → ((𝐹‘𝑥) ⨣ (𝐹‘𝑦)) = ((𝐹‘𝑋) ⨣ (𝐹‘𝑦))) |
13 | 10, 12 | eqeq12d 2754 | . . . 4 ⊢ (𝑥 = 𝑋 → ((𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) ⨣ (𝐹‘𝑦)) ↔ (𝐹‘(𝑋 + 𝑦)) = ((𝐹‘𝑋) ⨣ (𝐹‘𝑦)))) |
14 | oveq2 7360 | . . . . . 6 ⊢ (𝑦 = 𝑌 → (𝑋 + 𝑦) = (𝑋 + 𝑌)) | |
15 | 14 | fveq2d 6844 | . . . . 5 ⊢ (𝑦 = 𝑌 → (𝐹‘(𝑋 + 𝑦)) = (𝐹‘(𝑋 + 𝑌))) |
16 | fveq2 6840 | . . . . . 6 ⊢ (𝑦 = 𝑌 → (𝐹‘𝑦) = (𝐹‘𝑌)) | |
17 | 16 | oveq2d 7368 | . . . . 5 ⊢ (𝑦 = 𝑌 → ((𝐹‘𝑋) ⨣ (𝐹‘𝑦)) = ((𝐹‘𝑋) ⨣ (𝐹‘𝑌))) |
18 | 15, 17 | eqeq12d 2754 | . . . 4 ⊢ (𝑦 = 𝑌 → ((𝐹‘(𝑋 + 𝑦)) = ((𝐹‘𝑋) ⨣ (𝐹‘𝑦)) ↔ (𝐹‘(𝑋 + 𝑌)) = ((𝐹‘𝑋) ⨣ (𝐹‘𝑌)))) |
19 | 13, 18 | rspc2v 3589 | . . 3 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) ⨣ (𝐹‘𝑦)) → (𝐹‘(𝑋 + 𝑌)) = ((𝐹‘𝑋) ⨣ (𝐹‘𝑌)))) |
20 | 9, 19 | syl5com 31 | . 2 ⊢ (𝐹 ∈ (𝑆 MndHom 𝑇) → ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝐹‘(𝑋 + 𝑌)) = ((𝐹‘𝑋) ⨣ (𝐹‘𝑌)))) |
21 | 20 | 3impib 1117 | 1 ⊢ ((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝐹‘(𝑋 + 𝑌)) = ((𝐹‘𝑋) ⨣ (𝐹‘𝑌))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 397 ∧ w3a 1088 = wceq 1542 ∈ wcel 2107 ∀wral 3063 ⟶wf 6490 ‘cfv 6494 (class class class)co 7352 Basecbs 17043 +gcplusg 17093 0gc0g 17281 Mndcmnd 18516 MndHom cmhm 18559 |
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 2709 ax-sep 5255 ax-nul 5262 ax-pow 5319 ax-pr 5383 ax-un 7665 |
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 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2816 df-nfc 2888 df-ne 2943 df-ral 3064 df-rex 3073 df-rab 3407 df-v 3446 df-sbc 3739 df-dif 3912 df-un 3914 df-in 3916 df-ss 3926 df-nul 4282 df-if 4486 df-pw 4561 df-sn 4586 df-pr 4588 df-op 4592 df-uni 4865 df-br 5105 df-opab 5167 df-id 5530 df-xp 5638 df-rel 5639 df-cnv 5640 df-co 5641 df-dm 5642 df-rn 5643 df-iota 6446 df-fun 6496 df-fn 6497 df-f 6498 df-fv 6502 df-ov 7355 df-oprab 7356 df-mpo 7357 df-map 8726 df-mhm 18561 |
This theorem is referenced by: mhmf1o 18572 resmhm 18591 resmhm2 18592 resmhm2b 18593 mhmco 18594 mhmima 18595 mhmeql 18596 pwsco2mhm 18603 gsumwmhm 18615 mhmmulg 18876 ghmmhmb 18978 cntzmhm 19078 gsumzmhm 19673 rhmmul 20112 evlslem1 21444 mpfind 21469 mhmvlin 21698 mdetunilem7 21919 dchrzrhmul 26546 dchrmulcl 26549 dchrn0 26550 dchrinvcl 26553 dchrsum2 26568 sum2dchr 26574 mhmhmeotmd 32312 |
Copyright terms: Public domain | W3C validator |