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	$⊢ Y = ℤRHom (R)$
	zrhpsgnevpm.s	$⊢ S = pmSgn (N)$
	zrhpsgnevpm.o	$⊢ \underset{˙}{1} = 1_{R}$
	zrhpsgnodpm.p	$⊢ P = {Base}_{SymGrp (N)}$
	zrhpsgnodpm.i	$⊢ I = {inv}_{g} (R)$
Assertion	zrhpsgnodpm	$⊢ (R \in Ring \land N \in Fin \land F \in (P ∖ pmEven (N))) \to (Y \circ S) (F) = I (\underset{˙}{1})$

Proof

Step	Hyp	Ref	Expression
1		zrhpsgnevpm.y	$⊢ Y = ℤRHom (R)$
2		zrhpsgnevpm.s	$⊢ S = pmSgn (N)$
3		zrhpsgnevpm.o	$⊢ \underset{˙}{1} = 1_{R}$
4		zrhpsgnodpm.p	$⊢ P = {Base}_{SymGrp (N)}$
5		zrhpsgnodpm.i	$⊢ I = {inv}_{g} (R)$
6		eqid	$⊢ SymGrp (N) = SymGrp (N)$
7		eqid	$⊢ {mulGrp}_{ℂ_{fld}} ↾_{𝑠} \{1, - 1\} = {mulGrp}_{ℂ_{fld}} ↾_{𝑠} \{1, - 1\}$
8	6 2 7	psgnghm2	$⊢ N \in Fin \to S \in (SymGrp (N) GrpHom ({mulGrp}_{ℂ_{fld}} ↾_{𝑠} \{1, - 1\}))$
9		eqid	$⊢ {Base}_{({mulGrp}_{ℂ_{fld}} ↾_{𝑠} \{1, - 1\})} = {Base}_{({mulGrp}_{ℂ_{fld}} ↾_{𝑠} \{1, - 1\})}$
10	4 9	ghmf	$⊢ S \in (SymGrp (N) GrpHom ({mulGrp}_{ℂ_{fld}} ↾_{𝑠} \{1, - 1\})) \to S : P ⟶ {Base}_{({mulGrp}_{ℂ_{fld}} ↾_{𝑠} \{1, - 1\})}$
11	8 10	syl	$⊢ N \in Fin \to S : P ⟶ {Base}_{({mulGrp}_{ℂ_{fld}} ↾_{𝑠} \{1, - 1\})}$
12	11	3ad2ant2	$⊢ (R \in Ring \land N \in Fin \land F \in (P ∖ pmEven (N))) \to S : P ⟶ {Base}_{({mulGrp}_{ℂ_{fld}} ↾_{𝑠} \{1, - 1\})}$
13		eldifi	$⊢ F \in (P ∖ pmEven (N)) \to F \in P$
14	13	3ad2ant3	$⊢ (R \in Ring \land N \in Fin \land F \in (P ∖ pmEven (N))) \to F \in P$
15		fvco3	$⊢ (S : P ⟶ {Base}_{({mulGrp}_{ℂ_{fld}} ↾_{𝑠} \{1, - 1\})} \land F \in P) \to (Y \circ S) (F) = Y (S (F))$
16	12 14 15	syl2anc	$⊢ (R \in Ring \land N \in Fin \land F \in (P ∖ pmEven (N))) \to (Y \circ S) (F) = Y (S (F))$
17	6 4 2	psgnodpm	$⊢ (N \in Fin \land F \in (P ∖ pmEven (N))) \to S (F) = - 1$
18	17	3adant1	$⊢ (R \in Ring \land N \in Fin \land F \in (P ∖ pmEven (N))) \to S (F) = - 1$
19	18	fveq2d	$⊢ (R \in Ring \land N \in Fin \land F \in (P ∖ pmEven (N))) \to Y (S (F)) = Y (- 1)$
20	1	zrhrhm	$⊢ R \in Ring \to Y \in (ℤ_{ring} RingHom R)$
21		rhmghm	$⊢ Y \in (ℤ_{ring} RingHom R) \to Y \in (ℤ_{ring} GrpHom R)$
22	20 21	syl	$⊢ R \in Ring \to Y \in (ℤ_{ring} GrpHom R)$
23		1z	$⊢ 1 \in ℤ$
24	23	a1i	$⊢ R \in Ring \to 1 \in ℤ$
25		zringbas	$⊢ ℤ = {Base}_{ℤ_{ring}}$
26		eqid	$⊢ {inv}_{g} (ℤ_{ring}) = {inv}_{g} (ℤ_{ring})$
27	25 26 5	ghminv	$⊢ (Y \in (ℤ_{ring} GrpHom R) \land 1 \in ℤ) \to Y ({inv}_{g} (ℤ_{ring}) (1)) = I (Y (1))$
28	22 24 27	syl2anc	$⊢ R \in Ring \to Y ({inv}_{g} (ℤ_{ring}) (1)) = I (Y (1))$
29		zringinvg	$⊢ 1 \in ℤ \to - 1 = {inv}_{g} (ℤ_{ring}) (1)$
30	23 29	ax-mp	$⊢ - 1 = {inv}_{g} (ℤ_{ring}) (1)$
31	30	eqcomi	$⊢ {inv}_{g} (ℤ_{ring}) (1) = - 1$
32	31	fveq2i	$⊢ Y ({inv}_{g} (ℤ_{ring}) (1)) = Y (- 1)$
33	32	a1i	$⊢ R \in Ring \to Y ({inv}_{g} (ℤ_{ring}) (1)) = Y (- 1)$
34	1 3	zrh1	$⊢ R \in Ring \to Y (1) = \underset{˙}{1}$
35	34	fveq2d	$⊢ R \in Ring \to I (Y (1)) = I (\underset{˙}{1})$
36	28 33 35	3eqtr3d	$⊢ R \in Ring \to Y (- 1) = I (\underset{˙}{1})$
37	36	3ad2ant1	$⊢ (R \in Ring \land N \in Fin \land F \in (P ∖ pmEven (N))) \to Y (- 1) = I (\underset{˙}{1})$
38	16 19 37	3eqtrd	$⊢ (R \in Ring \land N \in Fin \land F \in (P ∖ pmEven (N))) \to (Y \circ S) (F) = I (\underset{˙}{1})$

Metamath Proof Explorer

Theorem zrhpsgnodpm

Proof