This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem zrhpsgnodpm

Description: The sign of an odd permutation embedded into a ring is the additive inverse of the unity element of the ring. (Contributed by SO, 9-Jul-2018)

Ref Expression
Hypotheses zrhpsgnevpm.y ⊢ 𝑌 = ( ℤRHom ‘ 𝑅 )
zrhpsgnevpm.s ⊢ 𝑆 = ( pmSgn ‘ 𝑁 )
zrhpsgnevpm.o ⊢ 1 = ( 1r ‘ 𝑅 )
zrhpsgnodpm.p ⊢ 𝑃 = ( Base ‘ ( SymGrp ‘ 𝑁 ) )
zrhpsgnodpm.i ⊢ 𝐼 = ( invg ‘ 𝑅 )
Assertion zrhpsgnodpm ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ∧ 𝐹 ∈ ( 𝑃 ∖ ( pmEven ‘ 𝑁 ) ) ) → ( ( 𝑌 ∘ 𝑆 ) ‘ 𝐹 ) = ( 𝐼 ‘ 1 ) )

Proof

Step Hyp Ref Expression
1 zrhpsgnevpm.y ⊢ 𝑌 = ( ℤRHom ‘ 𝑅 )
2 zrhpsgnevpm.s ⊢ 𝑆 = ( pmSgn ‘ 𝑁 )
3 zrhpsgnevpm.o ⊢ 1 = ( 1r ‘ 𝑅 )
4 zrhpsgnodpm.p ⊢ 𝑃 = ( Base ‘ ( SymGrp ‘ 𝑁 ) )
5 zrhpsgnodpm.i ⊢ 𝐼 = ( invg ‘ 𝑅 )
6 eqid ⊢ ( SymGrp ‘ 𝑁 ) = ( SymGrp ‘ 𝑁 )
7 eqid ⊢ ( ( mulGrp ‘ ℂfld ) ↾s { 1 , - 1 } ) = ( ( mulGrp ‘ ℂfld ) ↾s { 1 , - 1 } )
8 6 2 7 psgnghm2 ⊢ ( 𝑁 ∈ Fin → 𝑆 ∈ ( ( SymGrp ‘ 𝑁 ) GrpHom ( ( mulGrp ‘ ℂfld ) ↾s { 1 , - 1 } ) ) )
9 eqid ⊢ ( Base ‘ ( ( mulGrp ‘ ℂfld ) ↾s { 1 , - 1 } ) ) = ( Base ‘ ( ( mulGrp ‘ ℂfld ) ↾s { 1 , - 1 } ) )
10 4 9 ghmf ⊢ ( 𝑆 ∈ ( ( SymGrp ‘ 𝑁 ) GrpHom ( ( mulGrp ‘ ℂfld ) ↾s { 1 , - 1 } ) ) → 𝑆 : 𝑃 ⟶ ( Base ‘ ( ( mulGrp ‘ ℂfld ) ↾s { 1 , - 1 } ) ) )
11 8 10 syl ⊢ ( 𝑁 ∈ Fin → 𝑆 : 𝑃 ⟶ ( Base ‘ ( ( mulGrp ‘ ℂfld ) ↾s { 1 , - 1 } ) ) )
12 11 3ad2ant2 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ∧ 𝐹 ∈ ( 𝑃 ∖ ( pmEven ‘ 𝑁 ) ) ) → 𝑆 : 𝑃 ⟶ ( Base ‘ ( ( mulGrp ‘ ℂfld ) ↾s { 1 , - 1 } ) ) )
13 eldifi ⊢ ( 𝐹 ∈ ( 𝑃 ∖ ( pmEven ‘ 𝑁 ) ) → 𝐹 ∈ 𝑃 )
14 13 3ad2ant3 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ∧ 𝐹 ∈ ( 𝑃 ∖ ( pmEven ‘ 𝑁 ) ) ) → 𝐹 ∈ 𝑃 )
15 fvco3 ⊢ ( ( 𝑆 : 𝑃 ⟶ ( Base ‘ ( ( mulGrp ‘ ℂfld ) ↾s { 1 , - 1 } ) ) ∧ 𝐹 ∈ 𝑃 ) → ( ( 𝑌 ∘ 𝑆 ) ‘ 𝐹 ) = ( 𝑌 ‘ ( 𝑆 ‘ 𝐹 ) ) )
16 12 14 15 syl2anc ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ∧ 𝐹 ∈ ( 𝑃 ∖ ( pmEven ‘ 𝑁 ) ) ) → ( ( 𝑌 ∘ 𝑆 ) ‘ 𝐹 ) = ( 𝑌 ‘ ( 𝑆 ‘ 𝐹 ) ) )
17 6 4 2 psgnodpm ⊢ ( ( 𝑁 ∈ Fin ∧ 𝐹 ∈ ( 𝑃 ∖ ( pmEven ‘ 𝑁 ) ) ) → ( 𝑆 ‘ 𝐹 ) = - 1 )
18 17 3adant1 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ∧ 𝐹 ∈ ( 𝑃 ∖ ( pmEven ‘ 𝑁 ) ) ) → ( 𝑆 ‘ 𝐹 ) = - 1 )
19 18 fveq2d ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ∧ 𝐹 ∈ ( 𝑃 ∖ ( pmEven ‘ 𝑁 ) ) ) → ( 𝑌 ‘ ( 𝑆 ‘ 𝐹 ) ) = ( 𝑌 ‘ - 1 ) )
20 1 zrhrhm ⊢ ( 𝑅 ∈ Ring → 𝑌 ∈ ( ℤring RingHom 𝑅 ) )
21 rhmghm ⊢ ( 𝑌 ∈ ( ℤring RingHom 𝑅 ) → 𝑌 ∈ ( ℤring GrpHom 𝑅 ) )
22 20 21 syl ⊢ ( 𝑅 ∈ Ring → 𝑌 ∈ ( ℤring GrpHom 𝑅 ) )
23 1z ⊢ 1 ∈ ℤ
24 23 a1i ⊢ ( 𝑅 ∈ Ring → 1 ∈ ℤ )
25 zringbas ⊢ ℤ = ( Base ‘ ℤring )
26 eqid ⊢ ( invg ‘ ℤring ) = ( invg ‘ ℤring )
27 25 26 5 ghminv ⊢ ( ( 𝑌 ∈ ( ℤring GrpHom 𝑅 ) ∧ 1 ∈ ℤ ) → ( 𝑌 ‘ ( ( invg ‘ ℤring ) ‘ 1 ) ) = ( 𝐼 ‘ ( 𝑌 ‘ 1 ) ) )
28 22 24 27 syl2anc ⊢ ( 𝑅 ∈ Ring → ( 𝑌 ‘ ( ( invg ‘ ℤring ) ‘ 1 ) ) = ( 𝐼 ‘ ( 𝑌 ‘ 1 ) ) )
29 zringinvg ⊢ ( 1 ∈ ℤ → - 1 = ( ( invg ‘ ℤring ) ‘ 1 ) )
30 23 29 ax-mp ⊢ - 1 = ( ( invg ‘ ℤring ) ‘ 1 )
31 30 eqcomi ⊢ ( ( invg ‘ ℤring ) ‘ 1 ) = - 1
32 31 fveq2i ⊢ ( 𝑌 ‘ ( ( invg ‘ ℤring ) ‘ 1 ) ) = ( 𝑌 ‘ - 1 )
33 32 a1i ⊢ ( 𝑅 ∈ Ring → ( 𝑌 ‘ ( ( invg ‘ ℤring ) ‘ 1 ) ) = ( 𝑌 ‘ - 1 ) )
34 1 3 zrh1 ⊢ ( 𝑅 ∈ Ring → ( 𝑌 ‘ 1 ) = 1 )
35 34 fveq2d ⊢ ( 𝑅 ∈ Ring → ( 𝐼 ‘ ( 𝑌 ‘ 1 ) ) = ( 𝐼 ‘ 1 ) )
36 28 33 35 3eqtr3d ⊢ ( 𝑅 ∈ Ring → ( 𝑌 ‘ - 1 ) = ( 𝐼 ‘ 1 ) )
37 36 3ad2ant1 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ∧ 𝐹 ∈ ( 𝑃 ∖ ( pmEven ‘ 𝑁 ) ) ) → ( 𝑌 ‘ - 1 ) = ( 𝐼 ‘ 1 ) )
38 16 19 37 3eqtrd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ∧ 𝐹 ∈ ( 𝑃 ∖ ( pmEven ‘ 𝑁 ) ) ) → ( ( 𝑌 ∘ 𝑆 ) ‘ 𝐹 ) = ( 𝐼 ‘ 1 ) )