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 ⊢ 𝑌 = ( ℤRHom ‘ 𝑅 )
zrhpsgnevpm.s ⊢ 𝑆 = ( pmSgn ‘ 𝑁 )
zrhpsgnevpm.o ⊢ 1 = ( 1r ‘ 𝑅 )
Assertion zrhpsgnevpm ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ∧ 𝐹 ∈ ( pmEven ‘ 𝑁 ) ) → ( ( 𝑌 ∘ 𝑆 ) ‘ 𝐹 ) = 1 )

Proof

Step Hyp Ref Expression
1 zrhpsgnevpm.y ⊢ 𝑌 = ( ℤRHom ‘ 𝑅 )
2 zrhpsgnevpm.s ⊢ 𝑆 = ( pmSgn ‘ 𝑁 )
3 zrhpsgnevpm.o ⊢ 1 = ( 1r ‘ 𝑅 )
4 eqid ⊢ ( SymGrp ‘ 𝑁 ) = ( SymGrp ‘ 𝑁 )
5 eqid ⊢ ( ( mulGrp ‘ ℂfld ) ↾s { 1 , - 1 } ) = ( ( mulGrp ‘ ℂfld ) ↾s { 1 , - 1 } )
6 4 2 5 psgnghm2 ⊢ ( 𝑁 ∈ Fin → 𝑆 ∈ ( ( SymGrp ‘ 𝑁 ) GrpHom ( ( mulGrp ‘ ℂfld ) ↾s { 1 , - 1 } ) ) )
7 eqid ⊢ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) = ( Base ‘ ( SymGrp ‘ 𝑁 ) )
8 eqid ⊢ ( Base ‘ ( ( mulGrp ‘ ℂfld ) ↾s { 1 , - 1 } ) ) = ( Base ‘ ( ( mulGrp ‘ ℂfld ) ↾s { 1 , - 1 } ) )
9 7 8 ghmf ⊢ ( 𝑆 ∈ ( ( SymGrp ‘ 𝑁 ) GrpHom ( ( mulGrp ‘ ℂfld ) ↾s { 1 , - 1 } ) ) → 𝑆 : ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ⟶ ( Base ‘ ( ( mulGrp ‘ ℂfld ) ↾s { 1 , - 1 } ) ) )
10 6 9 syl ⊢ ( 𝑁 ∈ Fin → 𝑆 : ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ⟶ ( Base ‘ ( ( mulGrp ‘ ℂfld ) ↾s { 1 , - 1 } ) ) )
11 10 3ad2ant2 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ∧ 𝐹 ∈ ( pmEven ‘ 𝑁 ) ) → 𝑆 : ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ⟶ ( Base ‘ ( ( mulGrp ‘ ℂfld ) ↾s { 1 , - 1 } ) ) )
12 4 7 evpmss ⊢ ( pmEven ‘ 𝑁 ) ⊆ ( Base ‘ ( SymGrp ‘ 𝑁 ) )
13 12 sseli ⊢ ( 𝐹 ∈ ( pmEven ‘ 𝑁 ) → 𝐹 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) )
14 13 3ad2ant3 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ∧ 𝐹 ∈ ( pmEven ‘ 𝑁 ) ) → 𝐹 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) )
15 fvco3 ⊢ ( ( 𝑆 : ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ⟶ ( Base ‘ ( ( mulGrp ‘ ℂfld ) ↾s { 1 , - 1 } ) ) ∧ 𝐹 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ) → ( ( 𝑌 ∘ 𝑆 ) ‘ 𝐹 ) = ( 𝑌 ‘ ( 𝑆 ‘ 𝐹 ) ) )
16 11 14 15 syl2anc ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ∧ 𝐹 ∈ ( pmEven ‘ 𝑁 ) ) → ( ( 𝑌 ∘ 𝑆 ) ‘ 𝐹 ) = ( 𝑌 ‘ ( 𝑆 ‘ 𝐹 ) ) )
17 4 7 2 psgnevpm ⊢ ( ( 𝑁 ∈ Fin ∧ 𝐹 ∈ ( pmEven ‘ 𝑁 ) ) → ( 𝑆 ‘ 𝐹 ) = 1 )
18 17 3adant1 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ∧ 𝐹 ∈ ( pmEven ‘ 𝑁 ) ) → ( 𝑆 ‘ 𝐹 ) = 1 )
19 18 fveq2d ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ∧ 𝐹 ∈ ( pmEven ‘ 𝑁 ) ) → ( 𝑌 ‘ ( 𝑆 ‘ 𝐹 ) ) = ( 𝑌 ‘ 1 ) )
20 1 3 zrh1 ⊢ ( 𝑅 ∈ Ring → ( 𝑌 ‘ 1 ) = 1 )
21 20 3ad2ant1 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ∧ 𝐹 ∈ ( pmEven ‘ 𝑁 ) ) → ( 𝑌 ‘ 1 ) = 1 )
22 16 19 21 3eqtrd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ∧ 𝐹 ∈ ( pmEven ‘ 𝑁 ) ) → ( ( 𝑌 ∘ 𝑆 ) ‘ 𝐹 ) = 1 )