Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > mulgghm2 | Structured version Visualization version GIF version |
Description: The powers of a group element give a homomorphism from ℤ to a group. (Contributed by Mario Carneiro, 13-Jun-2015.) (Revised by AV, 12-Jun-2019.) |
Ref | Expression |
---|---|
mulgghm2.m | ⊢ · = (.g‘𝑅) |
mulgghm2.f | ⊢ 𝐹 = (𝑛 ∈ ℤ ↦ (𝑛 · 1 )) |
mulgghm2.b | ⊢ 𝐵 = (Base‘𝑅) |
Ref | Expression |
---|---|
mulgghm2 | ⊢ ((𝑅 ∈ Grp ∧ 1 ∈ 𝐵) → 𝐹 ∈ (ℤring GrpHom 𝑅)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpl 483 | . . 3 ⊢ ((𝑅 ∈ Grp ∧ 1 ∈ 𝐵) → 𝑅 ∈ Grp) | |
2 | zringgrp 20738 | . . 3 ⊢ ℤring ∈ Grp | |
3 | 1, 2 | jctil 520 | . 2 ⊢ ((𝑅 ∈ Grp ∧ 1 ∈ 𝐵) → (ℤring ∈ Grp ∧ 𝑅 ∈ Grp)) |
4 | mulgghm2.b | . . . . . . 7 ⊢ 𝐵 = (Base‘𝑅) | |
5 | mulgghm2.m | . . . . . . 7 ⊢ · = (.g‘𝑅) | |
6 | 4, 5 | mulgcl 18780 | . . . . . 6 ⊢ ((𝑅 ∈ Grp ∧ 𝑛 ∈ ℤ ∧ 1 ∈ 𝐵) → (𝑛 · 1 ) ∈ 𝐵) |
7 | 6 | 3expa 1117 | . . . . 5 ⊢ (((𝑅 ∈ Grp ∧ 𝑛 ∈ ℤ) ∧ 1 ∈ 𝐵) → (𝑛 · 1 ) ∈ 𝐵) |
8 | 7 | an32s 649 | . . . 4 ⊢ (((𝑅 ∈ Grp ∧ 1 ∈ 𝐵) ∧ 𝑛 ∈ ℤ) → (𝑛 · 1 ) ∈ 𝐵) |
9 | mulgghm2.f | . . . 4 ⊢ 𝐹 = (𝑛 ∈ ℤ ↦ (𝑛 · 1 )) | |
10 | 8, 9 | fmptd 7020 | . . 3 ⊢ ((𝑅 ∈ Grp ∧ 1 ∈ 𝐵) → 𝐹:ℤ⟶𝐵) |
11 | eqid 2735 | . . . . . . . . 9 ⊢ (+g‘𝑅) = (+g‘𝑅) | |
12 | 4, 5, 11 | mulgdir 18794 | . . . . . . . 8 ⊢ ((𝑅 ∈ Grp ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ∧ 1 ∈ 𝐵)) → ((𝑥 + 𝑦) · 1 ) = ((𝑥 · 1 )(+g‘𝑅)(𝑦 · 1 ))) |
13 | 12 | 3exp2 1353 | . . . . . . 7 ⊢ (𝑅 ∈ Grp → (𝑥 ∈ ℤ → (𝑦 ∈ ℤ → ( 1 ∈ 𝐵 → ((𝑥 + 𝑦) · 1 ) = ((𝑥 · 1 )(+g‘𝑅)(𝑦 · 1 )))))) |
14 | 13 | imp42 427 | . . . . . 6 ⊢ (((𝑅 ∈ Grp ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ 1 ∈ 𝐵) → ((𝑥 + 𝑦) · 1 ) = ((𝑥 · 1 )(+g‘𝑅)(𝑦 · 1 ))) |
15 | 14 | an32s 649 | . . . . 5 ⊢ (((𝑅 ∈ Grp ∧ 1 ∈ 𝐵) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → ((𝑥 + 𝑦) · 1 ) = ((𝑥 · 1 )(+g‘𝑅)(𝑦 · 1 ))) |
16 | zaddcl 12420 | . . . . . . 7 ⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) → (𝑥 + 𝑦) ∈ ℤ) | |
17 | 16 | adantl 482 | . . . . . 6 ⊢ (((𝑅 ∈ Grp ∧ 1 ∈ 𝐵) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (𝑥 + 𝑦) ∈ ℤ) |
18 | oveq1 7315 | . . . . . . 7 ⊢ (𝑛 = (𝑥 + 𝑦) → (𝑛 · 1 ) = ((𝑥 + 𝑦) · 1 )) | |
19 | ovex 7341 | . . . . . . 7 ⊢ ((𝑥 + 𝑦) · 1 ) ∈ V | |
20 | 18, 9, 19 | fvmpt 6907 | . . . . . 6 ⊢ ((𝑥 + 𝑦) ∈ ℤ → (𝐹‘(𝑥 + 𝑦)) = ((𝑥 + 𝑦) · 1 )) |
21 | 17, 20 | syl 17 | . . . . 5 ⊢ (((𝑅 ∈ Grp ∧ 1 ∈ 𝐵) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (𝐹‘(𝑥 + 𝑦)) = ((𝑥 + 𝑦) · 1 )) |
22 | oveq1 7315 | . . . . . . . 8 ⊢ (𝑛 = 𝑥 → (𝑛 · 1 ) = (𝑥 · 1 )) | |
23 | ovex 7341 | . . . . . . . 8 ⊢ (𝑥 · 1 ) ∈ V | |
24 | 22, 9, 23 | fvmpt 6907 | . . . . . . 7 ⊢ (𝑥 ∈ ℤ → (𝐹‘𝑥) = (𝑥 · 1 )) |
25 | oveq1 7315 | . . . . . . . 8 ⊢ (𝑛 = 𝑦 → (𝑛 · 1 ) = (𝑦 · 1 )) | |
26 | ovex 7341 | . . . . . . . 8 ⊢ (𝑦 · 1 ) ∈ V | |
27 | 25, 9, 26 | fvmpt 6907 | . . . . . . 7 ⊢ (𝑦 ∈ ℤ → (𝐹‘𝑦) = (𝑦 · 1 )) |
28 | 24, 27 | oveqan12d 7327 | . . . . . 6 ⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) → ((𝐹‘𝑥)(+g‘𝑅)(𝐹‘𝑦)) = ((𝑥 · 1 )(+g‘𝑅)(𝑦 · 1 ))) |
29 | 28 | adantl 482 | . . . . 5 ⊢ (((𝑅 ∈ Grp ∧ 1 ∈ 𝐵) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → ((𝐹‘𝑥)(+g‘𝑅)(𝐹‘𝑦)) = ((𝑥 · 1 )(+g‘𝑅)(𝑦 · 1 ))) |
30 | 15, 21, 29 | 3eqtr4d 2785 | . . . 4 ⊢ (((𝑅 ∈ Grp ∧ 1 ∈ 𝐵) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥)(+g‘𝑅)(𝐹‘𝑦))) |
31 | 30 | ralrimivva 3192 | . . 3 ⊢ ((𝑅 ∈ Grp ∧ 1 ∈ 𝐵) → ∀𝑥 ∈ ℤ ∀𝑦 ∈ ℤ (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥)(+g‘𝑅)(𝐹‘𝑦))) |
32 | 10, 31 | jca 512 | . 2 ⊢ ((𝑅 ∈ Grp ∧ 1 ∈ 𝐵) → (𝐹:ℤ⟶𝐵 ∧ ∀𝑥 ∈ ℤ ∀𝑦 ∈ ℤ (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥)(+g‘𝑅)(𝐹‘𝑦)))) |
33 | zringbas 20739 | . . 3 ⊢ ℤ = (Base‘ℤring) | |
34 | zringplusg 20740 | . . 3 ⊢ + = (+g‘ℤring) | |
35 | 33, 4, 34, 11 | isghm 18893 | . 2 ⊢ (𝐹 ∈ (ℤring GrpHom 𝑅) ↔ ((ℤring ∈ Grp ∧ 𝑅 ∈ Grp) ∧ (𝐹:ℤ⟶𝐵 ∧ ∀𝑥 ∈ ℤ ∀𝑦 ∈ ℤ (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥)(+g‘𝑅)(𝐹‘𝑦))))) |
36 | 3, 32, 35 | sylanbrc 583 | 1 ⊢ ((𝑅 ∈ Grp ∧ 1 ∈ 𝐵) → 𝐹 ∈ (ℤring GrpHom 𝑅)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 = wceq 1538 ∈ wcel 2103 ∀wral 3060 ↦ cmpt 5163 ⟶wf 6454 ‘cfv 6458 (class class class)co 7308 + caddc 10934 ℤcz 12379 Basecbs 16971 +gcplusg 17021 Grpcgrp 18636 .gcmg 18759 GrpHom cghm 18890 ℤringczring 20733 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1910 ax-6 1968 ax-7 2008 ax-8 2105 ax-9 2113 ax-10 2134 ax-11 2151 ax-12 2168 ax-ext 2706 ax-rep 5217 ax-sep 5231 ax-nul 5238 ax-pow 5296 ax-pr 5360 ax-un 7621 ax-cnex 10987 ax-resscn 10988 ax-1cn 10989 ax-icn 10990 ax-addcl 10991 ax-addrcl 10992 ax-mulcl 10993 ax-mulrcl 10994 ax-mulcom 10995 ax-addass 10996 ax-mulass 10997 ax-distr 10998 ax-i2m1 10999 ax-1ne0 11000 ax-1rid 11001 ax-rnegex 11002 ax-rrecex 11003 ax-cnre 11004 ax-pre-lttri 11005 ax-pre-lttrn 11006 ax-pre-ltadd 11007 ax-pre-mulgt0 11008 ax-addf 11010 ax-mulf 11011 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3or 1087 df-3an 1088 df-tru 1541 df-fal 1551 df-ex 1779 df-nf 1783 df-sb 2065 df-mo 2537 df-eu 2566 df-clab 2713 df-cleq 2727 df-clel 2813 df-nfc 2885 df-ne 2940 df-nel 3046 df-ral 3061 df-rex 3070 df-rmo 3339 df-reu 3340 df-rab 3357 df-v 3438 df-sbc 3721 df-csb 3837 df-dif 3894 df-un 3896 df-in 3898 df-ss 3908 df-pss 3910 df-nul 4262 df-if 4465 df-pw 4540 df-sn 4565 df-pr 4567 df-tp 4569 df-op 4571 df-uni 4844 df-iun 4932 df-br 5081 df-opab 5143 df-mpt 5164 df-tr 5198 df-id 5500 df-eprel 5506 df-po 5514 df-so 5515 df-fr 5555 df-we 5557 df-xp 5606 df-rel 5607 df-cnv 5608 df-co 5609 df-dm 5610 df-rn 5611 df-res 5612 df-ima 5613 df-pred 6217 df-ord 6284 df-on 6285 df-lim 6286 df-suc 6287 df-iota 6410 df-fun 6460 df-fn 6461 df-f 6462 df-f1 6463 df-fo 6464 df-f1o 6465 df-fv 6466 df-riota 7265 df-ov 7311 df-oprab 7312 df-mpo 7313 df-om 7749 df-1st 7867 df-2nd 7868 df-frecs 8132 df-wrecs 8163 df-recs 8237 df-rdg 8276 df-1o 8332 df-er 8534 df-en 8770 df-dom 8771 df-sdom 8772 df-fin 8773 df-pnf 11071 df-mnf 11072 df-xr 11073 df-ltxr 11074 df-le 11075 df-sub 11267 df-neg 11268 df-nn 12034 df-2 12096 df-3 12097 df-4 12098 df-5 12099 df-6 12100 df-7 12101 df-8 12102 df-9 12103 df-n0 12294 df-z 12380 df-dec 12498 df-uz 12643 df-fz 13300 df-seq 13782 df-struct 16907 df-sets 16924 df-slot 16942 df-ndx 16954 df-base 16972 df-ress 17001 df-plusg 17034 df-mulr 17035 df-starv 17036 df-tset 17040 df-ple 17041 df-ds 17043 df-unif 17044 df-0g 17211 df-mgm 18385 df-sgrp 18434 df-mnd 18445 df-grp 18639 df-minusg 18640 df-mulg 18760 df-subg 18811 df-ghm 18891 df-cmn 19447 df-mgp 19780 df-ur 19797 df-ring 19844 df-cring 19845 df-subrg 20085 df-cnfld 20661 df-zring 20734 |
This theorem is referenced by: mulgrhm 20762 frgpcyg 20844 |
Copyright terms: Public domain | W3C validator |