![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > zrhpsgnmhm | Structured version Visualization version GIF version |
Description: Embedding of permutation signs into an arbitrary ring is a homomorphism. (Contributed by SO, 9-Jul-2018.) |
Ref | Expression |
---|---|
zrhpsgnmhm | ⊢ ((𝑅 ∈ Ring ∧ 𝐴 ∈ Fin) → ((ℤRHom‘𝑅) ∘ (pmSgn‘𝐴)) ∈ ((SymGrp‘𝐴) MndHom (mulGrp‘𝑅))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid 2761 | . . . 4 ⊢ (ℤRHom‘𝑅) = (ℤRHom‘𝑅) | |
2 | 1 | zrhrhm 20083 | . . 3 ⊢ (𝑅 ∈ Ring → (ℤRHom‘𝑅) ∈ (ℤring RingHom 𝑅)) |
3 | eqid 2761 | . . . 4 ⊢ (mulGrp‘ℤring) = (mulGrp‘ℤring) | |
4 | eqid 2761 | . . . 4 ⊢ (mulGrp‘𝑅) = (mulGrp‘𝑅) | |
5 | 3, 4 | rhmmhm 18945 | . . 3 ⊢ ((ℤRHom‘𝑅) ∈ (ℤring RingHom 𝑅) → (ℤRHom‘𝑅) ∈ ((mulGrp‘ℤring) MndHom (mulGrp‘𝑅))) |
6 | 2, 5 | syl 17 | . 2 ⊢ (𝑅 ∈ Ring → (ℤRHom‘𝑅) ∈ ((mulGrp‘ℤring) MndHom (mulGrp‘𝑅))) |
7 | eqid 2761 | . . . . 5 ⊢ (SymGrp‘𝐴) = (SymGrp‘𝐴) | |
8 | eqid 2761 | . . . . 5 ⊢ (pmSgn‘𝐴) = (pmSgn‘𝐴) | |
9 | eqid 2761 | . . . . 5 ⊢ ((mulGrp‘ℂfld) ↾s {1, -1}) = ((mulGrp‘ℂfld) ↾s {1, -1}) | |
10 | 7, 8, 9 | psgnghm2 20150 | . . . 4 ⊢ (𝐴 ∈ Fin → (pmSgn‘𝐴) ∈ ((SymGrp‘𝐴) GrpHom ((mulGrp‘ℂfld) ↾s {1, -1}))) |
11 | ghmmhm 17892 | . . . 4 ⊢ ((pmSgn‘𝐴) ∈ ((SymGrp‘𝐴) GrpHom ((mulGrp‘ℂfld) ↾s {1, -1})) → (pmSgn‘𝐴) ∈ ((SymGrp‘𝐴) MndHom ((mulGrp‘ℂfld) ↾s {1, -1}))) | |
12 | 10, 11 | syl 17 | . . 3 ⊢ (𝐴 ∈ Fin → (pmSgn‘𝐴) ∈ ((SymGrp‘𝐴) MndHom ((mulGrp‘ℂfld) ↾s {1, -1}))) |
13 | eqid 2761 | . . . . . . . 8 ⊢ ((mulGrp‘ℂfld) ↾s (ℂ ∖ {0})) = ((mulGrp‘ℂfld) ↾s (ℂ ∖ {0})) | |
14 | 13 | cnmsgnsubg 20146 | . . . . . . 7 ⊢ {1, -1} ∈ (SubGrp‘((mulGrp‘ℂfld) ↾s (ℂ ∖ {0}))) |
15 | subgsubm 17838 | . . . . . . 7 ⊢ ({1, -1} ∈ (SubGrp‘((mulGrp‘ℂfld) ↾s (ℂ ∖ {0}))) → {1, -1} ∈ (SubMnd‘((mulGrp‘ℂfld) ↾s (ℂ ∖ {0})))) | |
16 | 14, 15 | ax-mp 5 | . . . . . 6 ⊢ {1, -1} ∈ (SubMnd‘((mulGrp‘ℂfld) ↾s (ℂ ∖ {0}))) |
17 | cnring 19991 | . . . . . . 7 ⊢ ℂfld ∈ Ring | |
18 | cnfldbas 19973 | . . . . . . . . 9 ⊢ ℂ = (Base‘ℂfld) | |
19 | cnfld0 19993 | . . . . . . . . 9 ⊢ 0 = (0g‘ℂfld) | |
20 | cndrng 19998 | . . . . . . . . 9 ⊢ ℂfld ∈ DivRing | |
21 | 18, 19, 20 | drngui 18976 | . . . . . . . 8 ⊢ (ℂ ∖ {0}) = (Unit‘ℂfld) |
22 | eqid 2761 | . . . . . . . 8 ⊢ (mulGrp‘ℂfld) = (mulGrp‘ℂfld) | |
23 | 21, 22 | unitsubm 18891 | . . . . . . 7 ⊢ (ℂfld ∈ Ring → (ℂ ∖ {0}) ∈ (SubMnd‘(mulGrp‘ℂfld))) |
24 | 13 | subsubm 17579 | . . . . . . 7 ⊢ ((ℂ ∖ {0}) ∈ (SubMnd‘(mulGrp‘ℂfld)) → ({1, -1} ∈ (SubMnd‘((mulGrp‘ℂfld) ↾s (ℂ ∖ {0}))) ↔ ({1, -1} ∈ (SubMnd‘(mulGrp‘ℂfld)) ∧ {1, -1} ⊆ (ℂ ∖ {0})))) |
25 | 17, 23, 24 | mp2b 10 | . . . . . 6 ⊢ ({1, -1} ∈ (SubMnd‘((mulGrp‘ℂfld) ↾s (ℂ ∖ {0}))) ↔ ({1, -1} ∈ (SubMnd‘(mulGrp‘ℂfld)) ∧ {1, -1} ⊆ (ℂ ∖ {0}))) |
26 | 16, 25 | mpbi 220 | . . . . 5 ⊢ ({1, -1} ∈ (SubMnd‘(mulGrp‘ℂfld)) ∧ {1, -1} ⊆ (ℂ ∖ {0})) |
27 | 26 | simpli 476 | . . . 4 ⊢ {1, -1} ∈ (SubMnd‘(mulGrp‘ℂfld)) |
28 | 1z 11620 | . . . . 5 ⊢ 1 ∈ ℤ | |
29 | neg1z 11626 | . . . . 5 ⊢ -1 ∈ ℤ | |
30 | prssi 4499 | . . . . 5 ⊢ ((1 ∈ ℤ ∧ -1 ∈ ℤ) → {1, -1} ⊆ ℤ) | |
31 | 28, 29, 30 | mp2an 710 | . . . 4 ⊢ {1, -1} ⊆ ℤ |
32 | zsubrg 20022 | . . . . 5 ⊢ ℤ ∈ (SubRing‘ℂfld) | |
33 | 22 | subrgsubm 19016 | . . . . 5 ⊢ (ℤ ∈ (SubRing‘ℂfld) → ℤ ∈ (SubMnd‘(mulGrp‘ℂfld))) |
34 | zringmpg 20063 | . . . . . . 7 ⊢ ((mulGrp‘ℂfld) ↾s ℤ) = (mulGrp‘ℤring) | |
35 | 34 | eqcomi 2770 | . . . . . 6 ⊢ (mulGrp‘ℤring) = ((mulGrp‘ℂfld) ↾s ℤ) |
36 | 35 | subsubm 17579 | . . . . 5 ⊢ (ℤ ∈ (SubMnd‘(mulGrp‘ℂfld)) → ({1, -1} ∈ (SubMnd‘(mulGrp‘ℤring)) ↔ ({1, -1} ∈ (SubMnd‘(mulGrp‘ℂfld)) ∧ {1, -1} ⊆ ℤ))) |
37 | 32, 33, 36 | mp2b 10 | . . . 4 ⊢ ({1, -1} ∈ (SubMnd‘(mulGrp‘ℤring)) ↔ ({1, -1} ∈ (SubMnd‘(mulGrp‘ℂfld)) ∧ {1, -1} ⊆ ℤ)) |
38 | 27, 31, 37 | mpbir2an 993 | . . 3 ⊢ {1, -1} ∈ (SubMnd‘(mulGrp‘ℤring)) |
39 | zex 11599 | . . . . . 6 ⊢ ℤ ∈ V | |
40 | ressabs 16162 | . . . . . 6 ⊢ ((ℤ ∈ V ∧ {1, -1} ⊆ ℤ) → (((mulGrp‘ℂfld) ↾s ℤ) ↾s {1, -1}) = ((mulGrp‘ℂfld) ↾s {1, -1})) | |
41 | 39, 31, 40 | mp2an 710 | . . . . 5 ⊢ (((mulGrp‘ℂfld) ↾s ℤ) ↾s {1, -1}) = ((mulGrp‘ℂfld) ↾s {1, -1}) |
42 | 34 | oveq1i 6825 | . . . . 5 ⊢ (((mulGrp‘ℂfld) ↾s ℤ) ↾s {1, -1}) = ((mulGrp‘ℤring) ↾s {1, -1}) |
43 | 41, 42 | eqtr3i 2785 | . . . 4 ⊢ ((mulGrp‘ℂfld) ↾s {1, -1}) = ((mulGrp‘ℤring) ↾s {1, -1}) |
44 | 43 | resmhm2 17582 | . . 3 ⊢ (((pmSgn‘𝐴) ∈ ((SymGrp‘𝐴) MndHom ((mulGrp‘ℂfld) ↾s {1, -1})) ∧ {1, -1} ∈ (SubMnd‘(mulGrp‘ℤring))) → (pmSgn‘𝐴) ∈ ((SymGrp‘𝐴) MndHom (mulGrp‘ℤring))) |
45 | 12, 38, 44 | sylancl 697 | . 2 ⊢ (𝐴 ∈ Fin → (pmSgn‘𝐴) ∈ ((SymGrp‘𝐴) MndHom (mulGrp‘ℤring))) |
46 | mhmco 17584 | . 2 ⊢ (((ℤRHom‘𝑅) ∈ ((mulGrp‘ℤring) MndHom (mulGrp‘𝑅)) ∧ (pmSgn‘𝐴) ∈ ((SymGrp‘𝐴) MndHom (mulGrp‘ℤring))) → ((ℤRHom‘𝑅) ∘ (pmSgn‘𝐴)) ∈ ((SymGrp‘𝐴) MndHom (mulGrp‘𝑅))) | |
47 | 6, 45, 46 | syl2an 495 | 1 ⊢ ((𝑅 ∈ Ring ∧ 𝐴 ∈ Fin) → ((ℤRHom‘𝑅) ∘ (pmSgn‘𝐴)) ∈ ((SymGrp‘𝐴) MndHom (mulGrp‘𝑅))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 196 ∧ wa 383 = wceq 1632 ∈ wcel 2140 Vcvv 3341 ∖ cdif 3713 ⊆ wss 3716 {csn 4322 {cpr 4324 ∘ ccom 5271 ‘cfv 6050 (class class class)co 6815 Fincfn 8124 ℂcc 10147 0cc0 10149 1c1 10150 -cneg 10480 ℤcz 11590 ↾s cress 16081 MndHom cmhm 17555 SubMndcsubmnd 17556 SubGrpcsubg 17810 GrpHom cghm 17879 SymGrpcsymg 18018 pmSgncpsgn 18130 mulGrpcmgp 18710 Ringcrg 18768 RingHom crh 18935 SubRingcsubrg 18999 ℂfldccnfld 19969 ℤringzring 20041 ℤRHomczrh 20071 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1871 ax-4 1886 ax-5 1989 ax-6 2055 ax-7 2091 ax-8 2142 ax-9 2149 ax-10 2169 ax-11 2184 ax-12 2197 ax-13 2392 ax-ext 2741 ax-rep 4924 ax-sep 4934 ax-nul 4942 ax-pow 4993 ax-pr 5056 ax-un 7116 ax-inf2 8714 ax-cnex 10205 ax-resscn 10206 ax-1cn 10207 ax-icn 10208 ax-addcl 10209 ax-addrcl 10210 ax-mulcl 10211 ax-mulrcl 10212 ax-mulcom 10213 ax-addass 10214 ax-mulass 10215 ax-distr 10216 ax-i2m1 10217 ax-1ne0 10218 ax-1rid 10219 ax-rnegex 10220 ax-rrecex 10221 ax-cnre 10222 ax-pre-lttri 10223 ax-pre-lttrn 10224 ax-pre-ltadd 10225 ax-pre-mulgt0 10226 ax-addf 10228 ax-mulf 10229 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3or 1073 df-3an 1074 df-xor 1614 df-tru 1635 df-ex 1854 df-nf 1859 df-sb 2048 df-eu 2612 df-mo 2613 df-clab 2748 df-cleq 2754 df-clel 2757 df-nfc 2892 df-ne 2934 df-nel 3037 df-ral 3056 df-rex 3057 df-reu 3058 df-rmo 3059 df-rab 3060 df-v 3343 df-sbc 3578 df-csb 3676 df-dif 3719 df-un 3721 df-in 3723 df-ss 3730 df-pss 3732 df-nul 4060 df-if 4232 df-pw 4305 df-sn 4323 df-pr 4325 df-tp 4327 df-op 4329 df-ot 4331 df-uni 4590 df-int 4629 df-iun 4675 df-iin 4676 df-br 4806 df-opab 4866 df-mpt 4883 df-tr 4906 df-id 5175 df-eprel 5180 df-po 5188 df-so 5189 df-fr 5226 df-se 5227 df-we 5228 df-xp 5273 df-rel 5274 df-cnv 5275 df-co 5276 df-dm 5277 df-rn 5278 df-res 5279 df-ima 5280 df-pred 5842 df-ord 5888 df-on 5889 df-lim 5890 df-suc 5891 df-iota 6013 df-fun 6052 df-fn 6053 df-f 6054 df-f1 6055 df-fo 6056 df-f1o 6057 df-fv 6058 df-isom 6059 df-riota 6776 df-ov 6818 df-oprab 6819 df-mpt2 6820 df-om 7233 df-1st 7335 df-2nd 7336 df-tpos 7523 df-wrecs 7578 df-recs 7639 df-rdg 7677 df-1o 7731 df-2o 7732 df-oadd 7735 df-er 7914 df-map 8028 df-en 8125 df-dom 8126 df-sdom 8127 df-fin 8128 df-card 8976 df-pnf 10289 df-mnf 10290 df-xr 10291 df-ltxr 10292 df-le 10293 df-sub 10481 df-neg 10482 df-div 10898 df-nn 11234 df-2 11292 df-3 11293 df-4 11294 df-5 11295 df-6 11296 df-7 11297 df-8 11298 df-9 11299 df-n0 11506 df-xnn0 11577 df-z 11591 df-dec 11707 df-uz 11901 df-rp 12047 df-fz 12541 df-fzo 12681 df-seq 13017 df-exp 13076 df-hash 13333 df-word 13506 df-lsw 13507 df-concat 13508 df-s1 13509 df-substr 13510 df-splice 13511 df-reverse 13512 df-s2 13814 df-struct 16082 df-ndx 16083 df-slot 16084 df-base 16086 df-sets 16087 df-ress 16088 df-plusg 16177 df-mulr 16178 df-starv 16179 df-tset 16183 df-ple 16184 df-ds 16187 df-unif 16188 df-0g 16325 df-gsum 16326 df-mre 16469 df-mrc 16470 df-acs 16472 df-mgm 17464 df-sgrp 17506 df-mnd 17517 df-mhm 17557 df-submnd 17558 df-grp 17647 df-minusg 17648 df-mulg 17763 df-subg 17813 df-ghm 17880 df-gim 17923 df-oppg 17997 df-symg 18019 df-pmtr 18083 df-psgn 18132 df-cmn 18416 df-abl 18417 df-mgp 18711 df-ur 18723 df-ring 18770 df-cring 18771 df-oppr 18844 df-dvdsr 18862 df-unit 18863 df-invr 18893 df-dvr 18904 df-rnghom 18938 df-drng 18972 df-subrg 19001 df-cnfld 19970 df-zring 20042 df-zrh 20075 |
This theorem is referenced by: madetsumid 20490 mdetleib2 20617 mdetf 20624 mdetdiaglem 20627 mdetrlin 20631 mdetrsca 20632 mdetralt 20637 mdetunilem7 20647 mdetunilem8 20648 |
Copyright terms: Public domain | W3C validator |