Metamath Proof Explorer

Theorem zrhpsgnevpm

Description: The sign of an even permutation embedded into a ring is the multiplicative neutral element of the ring. (Contributed by SO, 9-Jul-2018)

Ref Expression
Hypotheses zrhpsgnevpm.y ⊢ Y = ℤRHom ⁡ R
zrhpsgnevpm.s ⊢ S = pmSgn ⁡ N
zrhpsgnevpm.o ⊢ 1 ˙ = 1 R
Assertion zrhpsgnevpm ⊢ R ∈ Ring ∧ N ∈ Fin ∧ F ∈ pmEven ⁡ N → Y ∘ S ⁡ F = 1 ˙

Proof

Step Hyp Ref Expression
1 zrhpsgnevpm.y ⊢ Y = ℤRHom ⁡ R
2 zrhpsgnevpm.s ⊢ S = pmSgn ⁡ N
3 zrhpsgnevpm.o ⊢ 1 ˙ = 1 R
4 eqid ⊢ SymGrp ⁡ N = SymGrp ⁡ N
5 eqid ⊢ mulGrp ℂ fld ↾ 𝑠 1 − 1 = mulGrp ℂ fld ↾ 𝑠 1 − 1
6 4 2 5 psgnghm2 ⊢ N ∈ Fin → S ∈ SymGrp ⁡ N GrpHom mulGrp ℂ fld ↾ 𝑠 1 − 1
7 eqid ⊢ Base SymGrp ⁡ N = Base SymGrp ⁡ N
8 eqid ⊢ Base mulGrp ℂ fld ↾ 𝑠 1 − 1 = Base mulGrp ℂ fld ↾ 𝑠 1 − 1
9 7 8 ghmf ⊢ S ∈ SymGrp ⁡ N GrpHom mulGrp ℂ fld ↾ 𝑠 1 − 1 → S : Base SymGrp ⁡ N ⟶ Base mulGrp ℂ fld ↾ 𝑠 1 − 1
10 6 9 syl ⊢ N ∈ Fin → S : Base SymGrp ⁡ N ⟶ Base mulGrp ℂ fld ↾ 𝑠 1 − 1
11 10 3ad2ant2 ⊢ R ∈ Ring ∧ N ∈ Fin ∧ F ∈ pmEven ⁡ N → S : Base SymGrp ⁡ N ⟶ Base mulGrp ℂ fld ↾ 𝑠 1 − 1
12 4 7 evpmss ⊢ pmEven ⁡ N ⊆ Base SymGrp ⁡ N
13 12 sseli ⊢ F ∈ pmEven ⁡ N → F ∈ Base SymGrp ⁡ N
14 13 3ad2ant3 ⊢ R ∈ Ring ∧ N ∈ Fin ∧ F ∈ pmEven ⁡ N → F ∈ Base SymGrp ⁡ N
15 fvco3 ⊢ S : Base SymGrp ⁡ N ⟶ Base mulGrp ℂ fld ↾ 𝑠 1 − 1 ∧ F ∈ Base SymGrp ⁡ N → Y ∘ S ⁡ F = Y ⁡ S ⁡ F
16 11 14 15 syl2anc ⊢ R ∈ Ring ∧ N ∈ Fin ∧ F ∈ pmEven ⁡ N → Y ∘ S ⁡ F = Y ⁡ S ⁡ F
17 4 7 2 psgnevpm ⊢ N ∈ Fin ∧ F ∈ pmEven ⁡ N → S ⁡ F = 1
18 17 3adant1 ⊢ R ∈ Ring ∧ N ∈ Fin ∧ F ∈ pmEven ⁡ N → S ⁡ F = 1
19 18 fveq2d ⊢ R ∈ Ring ∧ N ∈ Fin ∧ F ∈ pmEven ⁡ N → Y ⁡ S ⁡ F = Y ⁡ 1
20 1 3 zrh1 ⊢ R ∈ Ring → Y ⁡ 1 = 1 ˙
21 20 3ad2ant1 ⊢ R ∈ Ring ∧ N ∈ Fin ∧ F ∈ pmEven ⁡ N → Y ⁡ 1 = 1 ˙
22 16 19 21 3eqtrd ⊢ R ∈ Ring ∧ N ∈ Fin ∧ F ∈ pmEven ⁡ N → Y ∘ S ⁡ F = 1 ˙