Theorem zrhpsgnodpm

Description: The sign of an odd permutation embedded into a ring is the additive inverse of 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 ‘ 𝑅 )
	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 ) )