zrhpsgnevpm

Description: The sign of an even permutation embedded into a ring is the unity 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}$
Assertion	zrhpsgnevpm	$⊢ (R \in Ring \land N \in Fin \land F \in pmEven (N)) \to (Y \circ S) (F) = \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		eqid	$⊢ SymGrp (N) = SymGrp (N)$
5		eqid	$⊢ {mulGrp}_{ℂ_{fld}} ↾_{𝑠} \{1, - 1\} = {mulGrp}_{ℂ_{fld}} ↾_{𝑠} \{1, - 1\}$
6	4 2 5	psgnghm2	$⊢ N \in Fin \to S \in (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 \in (SymGrp (N) GrpHom ({mulGrp}_{ℂ_{fld}} ↾_{𝑠} \{1, - 1\})) \to S : {Base}_{SymGrp (N)} ⟶ {Base}_{({mulGrp}_{ℂ_{fld}} ↾_{𝑠} \{1, - 1\})}$
10	6 9	syl	$⊢ N \in Fin \to S : {Base}_{SymGrp (N)} ⟶ {Base}_{({mulGrp}_{ℂ_{fld}} ↾_{𝑠} \{1, - 1\})}$
11	10	3ad2ant2	$⊢ (R \in Ring \land N \in Fin \land F \in pmEven (N)) \to S : {Base}_{SymGrp (N)} ⟶ {Base}_{({mulGrp}_{ℂ_{fld}} ↾_{𝑠} \{1, - 1\})}$
12	4 7	evpmss	$⊢ pmEven (N) \subseteq {Base}_{SymGrp (N)}$
13	12	sseli	$⊢ F \in pmEven (N) \to F \in {Base}_{SymGrp (N)}$
14	13	3ad2ant3	$⊢ (R \in Ring \land N \in Fin \land F \in pmEven (N)) \to F \in {Base}_{SymGrp (N)}$
15		fvco3	$⊢ (S : {Base}_{SymGrp (N)} ⟶ {Base}_{({mulGrp}_{ℂ_{fld}} ↾_{𝑠} \{1, - 1\})} \land F \in {Base}_{SymGrp (N)}) \to (Y \circ S) (F) = Y (S (F))$
16	11 14 15	syl2anc	$⊢ (R \in Ring \land N \in Fin \land F \in pmEven (N)) \to (Y \circ S) (F) = Y (S (F))$
17	4 7 2	psgnevpm	$⊢ (N \in Fin \land F \in pmEven (N)) \to S (F) = 1$
18	17	3adant1	$⊢ (R \in Ring \land N \in Fin \land F \in pmEven (N)) \to S (F) = 1$
19	18	fveq2d	$⊢ (R \in Ring \land N \in Fin \land F \in pmEven (N)) \to Y (S (F)) = Y (1)$
20	1 3	zrh1	$⊢ R \in Ring \to Y (1) = \underset{˙}{1}$
21	20	3ad2ant1	$⊢ (R \in Ring \land N \in Fin \land F \in pmEven (N)) \to Y (1) = \underset{˙}{1}$
22	16 19 21	3eqtrd	$⊢ (R \in Ring \land N \in Fin \land F \in pmEven (N)) \to (Y \circ S) (F) = \underset{˙}{1}$

Metamath Proof Explorer

Theorem zrhpsgnevpm

Proof