Metamath Proof Explorer

Theorem zrhpsgnmhm

Description: Embedding of permutation signs into an arbitrary ring is a homomorphism. (Contributed by SO, 9-Jul-2018)

Ref Expression
Assertion zrhpsgnmhm ⊢ R ∈ Ring ∧ A ∈ Fin → ℤRHom ⁡ R ∘ pmSgn ⁡ A ∈ SymGrp ⁡ A MndHom mulGrp R

Proof

Step Hyp Ref Expression
1 eqid ⊢ ℤRHom ⁡ R = ℤRHom ⁡ R
2 1 zrhrhm ⊢ R ∈ Ring → ℤRHom ⁡ R ∈ ℤ ring RingHom R
3 eqid ⊢ mulGrp ℤ ring = mulGrp ℤ ring
4 eqid ⊢ mulGrp R = mulGrp R
5 3 4 rhmmhm ⊢ ℤRHom ⁡ R ∈ ℤ ring RingHom R → ℤRHom ⁡ R ∈ mulGrp ℤ ring MndHom mulGrp R
6 2 5 syl ⊢ R ∈ Ring → ℤRHom ⁡ R ∈ mulGrp ℤ ring MndHom mulGrp R
7 eqid ⊢ SymGrp ⁡ A = SymGrp ⁡ A
8 eqid ⊢ pmSgn ⁡ A = pmSgn ⁡ A
9 eqid ⊢ mulGrp ℂ fld ↾ 𝑠 1 − 1 = mulGrp ℂ fld ↾ 𝑠 1 − 1
10 7 8 9 psgnghm2 ⊢ A ∈ Fin → pmSgn ⁡ A ∈ SymGrp ⁡ A GrpHom mulGrp ℂ fld ↾ 𝑠 1 − 1
11 ghmmhm ⊢ pmSgn ⁡ A ∈ SymGrp ⁡ A GrpHom mulGrp ℂ fld ↾ 𝑠 1 − 1 → pmSgn ⁡ A ∈ SymGrp ⁡ A MndHom mulGrp ℂ fld ↾ 𝑠 1 − 1
12 10 11 syl ⊢ A ∈ Fin → pmSgn ⁡ A ∈ SymGrp ⁡ A MndHom mulGrp ℂ fld ↾ 𝑠 1 − 1
13 eqid ⊢ mulGrp ℂ fld ↾ 𝑠 ℂ ∖ 0 = mulGrp ℂ fld ↾ 𝑠 ℂ ∖ 0
14 13 cnmsgnsubg ⊢ 1 − 1 ∈ SubGrp ⁡ mulGrp ℂ fld ↾ 𝑠 ℂ ∖ 0
15 subgsubm ⊢ 1 − 1 ∈ SubGrp ⁡ mulGrp ℂ fld ↾ 𝑠 ℂ ∖ 0 → 1 − 1 ∈ SubMnd ⁡ mulGrp ℂ fld ↾ 𝑠 ℂ ∖ 0
16 14 15 ax-mp ⊢ 1 − 1 ∈ SubMnd ⁡ mulGrp ℂ fld ↾ 𝑠 ℂ ∖ 0
17 cnring ⊢ ℂ fld ∈ Ring
18 cnfldbas ⊢ ℂ = Base ℂ fld
19 cnfld0 ⊢ 0 = 0 ℂ fld
20 cndrng ⊢ ℂ fld ∈ DivRing
21 18 19 20 drngui ⊢ ℂ ∖ 0 = Unit ⁡ ℂ fld
22 eqid ⊢ mulGrp ℂ fld = mulGrp ℂ fld
23 21 22 unitsubm ⊢ ℂ fld ∈ Ring → ℂ ∖ 0 ∈ SubMnd ⁡ mulGrp ℂ fld
24 13 subsubm ⊢ ℂ ∖ 0 ∈ SubMnd ⁡ mulGrp ℂ fld → 1 − 1 ∈ SubMnd ⁡ mulGrp ℂ fld ↾ 𝑠 ℂ ∖ 0 ↔ 1 − 1 ∈ SubMnd ⁡ mulGrp ℂ fld ∧ 1 − 1 ⊆ ℂ ∖ 0
25 17 23 24 mp2b ⊢ 1 − 1 ∈ SubMnd ⁡ mulGrp ℂ fld ↾ 𝑠 ℂ ∖ 0 ↔ 1 − 1 ∈ SubMnd ⁡ mulGrp ℂ fld ∧ 1 − 1 ⊆ ℂ ∖ 0
26 16 25 mpbi ⊢ 1 − 1 ∈ SubMnd ⁡ mulGrp ℂ fld ∧ 1 − 1 ⊆ ℂ ∖ 0
27 26 simpli ⊢ 1 − 1 ∈ SubMnd ⁡ mulGrp ℂ fld
28 1z ⊢ 1 ∈ ℤ
29 neg1z ⊢ − 1 ∈ ℤ
30 prssi ⊢ 1 ∈ ℤ ∧ − 1 ∈ ℤ → 1 − 1 ⊆ ℤ
31 28 29 30 mp2an ⊢ 1 − 1 ⊆ ℤ
32 zsubrg ⊢ ℤ ∈ SubRing ⁡ ℂ fld
33 22 subrgsubm ⊢ ℤ ∈ SubRing ⁡ ℂ fld → ℤ ∈ SubMnd ⁡ mulGrp ℂ fld
34 zringmpg ⊢ mulGrp ℂ fld ↾ 𝑠 ℤ = mulGrp ℤ ring
35 34 eqcomi ⊢ mulGrp ℤ ring = mulGrp ℂ fld ↾ 𝑠 ℤ
36 35 subsubm ⊢ ℤ ∈ SubMnd ⁡ mulGrp ℂ fld → 1 − 1 ∈ SubMnd ⁡ mulGrp ℤ ring ↔ 1 − 1 ∈ SubMnd ⁡ mulGrp ℂ fld ∧ 1 − 1 ⊆ ℤ
37 32 33 36 mp2b ⊢ 1 − 1 ∈ SubMnd ⁡ mulGrp ℤ ring ↔ 1 − 1 ∈ SubMnd ⁡ mulGrp ℂ fld ∧ 1 − 1 ⊆ ℤ
38 27 31 37 mpbir2an ⊢ 1 − 1 ∈ SubMnd ⁡ mulGrp ℤ ring
39 zex ⊢ ℤ ∈ V
40 ressabs ⊢ ℤ ∈ V ∧ 1 − 1 ⊆ ℤ → mulGrp ℂ fld ↾ 𝑠 ℤ ↾ 𝑠 1 − 1 = mulGrp ℂ fld ↾ 𝑠 1 − 1
41 39 31 40 mp2an ⊢ mulGrp ℂ fld ↾ 𝑠 ℤ ↾ 𝑠 1 − 1 = mulGrp ℂ fld ↾ 𝑠 1 − 1
42 34 oveq1i ⊢ mulGrp ℂ fld ↾ 𝑠 ℤ ↾ 𝑠 1 − 1 = mulGrp ℤ ring ↾ 𝑠 1 − 1
43 41 42 eqtr3i ⊢ mulGrp ℂ fld ↾ 𝑠 1 − 1 = mulGrp ℤ ring ↾ 𝑠 1 − 1
44 43 resmhm2 ⊢ pmSgn ⁡ A ∈ SymGrp ⁡ A MndHom mulGrp ℂ fld ↾ 𝑠 1 − 1 ∧ 1 − 1 ∈ SubMnd ⁡ mulGrp ℤ ring → pmSgn ⁡ A ∈ SymGrp ⁡ A MndHom mulGrp ℤ ring
45 12 38 44 sylancl ⊢ A ∈ Fin → pmSgn ⁡ A ∈ SymGrp ⁡ A MndHom mulGrp ℤ ring
46 mhmco ⊢ ℤRHom ⁡ R ∈ mulGrp ℤ ring MndHom mulGrp R ∧ pmSgn ⁡ A ∈ SymGrp ⁡ A MndHom mulGrp ℤ ring → ℤRHom ⁡ R ∘ pmSgn ⁡ A ∈ SymGrp ⁡ A MndHom mulGrp R
47 6 45 46 syl2an ⊢ R ∈ Ring ∧ A ∈ Fin → ℤRHom ⁡ R ∘ pmSgn ⁡ A ∈ SymGrp ⁡ A MndHom mulGrp R