zrhpsgnelbas

Description: Embedding of permutation signs into a ring results in an element of the ring. (Contributed by AV, 1-Jan-2019)

	Ref	Expression
Hypotheses	zrhpsgnelbas.p	$⊢ P = {Base}_{SymGrp (N)}$
	zrhpsgnelbas.s	$⊢ S = pmSgn (N)$
	zrhpsgnelbas.y	$⊢ Y = ℤRHom (R)$
Assertion	zrhpsgnelbas	$⊢ (R \in Ring \land N \in Fin \land Q \in P) \to Y (S (Q)) \in {Base}_{R}$

Proof

Step	Hyp	Ref	Expression
1		zrhpsgnelbas.p	$⊢ P = {Base}_{SymGrp (N)}$
2		zrhpsgnelbas.s	$⊢ S = pmSgn (N)$
3		zrhpsgnelbas.y	$⊢ Y = ℤRHom (R)$
4	1 2	psgnran	$⊢ (N \in Fin \land Q \in P) \to S (Q) \in \{1, - 1\}$
5	4	3adant1	$⊢ (R \in Ring \land N \in Fin \land Q \in P) \to S (Q) \in \{1, - 1\}$
6		elpri	$⊢ S (Q) \in \{1, - 1\} \to (S (Q) = 1 \lor S (Q) = - 1)$
7		eqid	$⊢ 1_{R} = 1_{R}$
8	3 7	zrh1	$⊢ R \in Ring \to Y (1) = 1_{R}$
9		eqid	$⊢ {Base}_{R} = {Base}_{R}$
10	9 7	ringidcl	$⊢ R \in Ring \to 1_{R} \in {Base}_{R}$
11	8 10	eqeltrd	$⊢ R \in Ring \to Y (1) \in {Base}_{R}$
12	11	3ad2ant1	$⊢ (R \in Ring \land N \in Fin \land Q \in P) \to Y (1) \in {Base}_{R}$
13		fveq2	$⊢ S (Q) = 1 \to Y (S (Q)) = Y (1)$
14	13	eleq1d	$⊢ S (Q) = 1 \to (Y (S (Q)) \in {Base}_{R} \leftrightarrow Y (1) \in {Base}_{R})$
15	12 14	imbitrrid	$⊢ S (Q) = 1 \to ((R \in Ring \land N \in Fin \land Q \in P) \to Y (S (Q)) \in {Base}_{R})$
16		neg1z	$⊢ - 1 \in ℤ$
17		eqid	$⊢ \cdot_{R} = \cdot_{R}$
18	3 17 7	zrhmulg	$⊢ (R \in Ring \land - 1 \in ℤ) \to Y (- 1) = -1 \cdot_{R} 1_{R}$
19	16 18	mpan2	$⊢ R \in Ring \to Y (- 1) = -1 \cdot_{R} 1_{R}$
20		ringgrp	$⊢ R \in Ring \to R \in Grp$
21	16	a1i	$⊢ R \in Ring \to - 1 \in ℤ$
22	9 17 20 21 10	mulgcld	$⊢ R \in Ring \to -1 \cdot_{R} 1_{R} \in {Base}_{R}$
23	19 22	eqeltrd	$⊢ R \in Ring \to Y (- 1) \in {Base}_{R}$
24	23	3ad2ant1	$⊢ (R \in Ring \land N \in Fin \land Q \in P) \to Y (- 1) \in {Base}_{R}$
25		fveq2	$⊢ S (Q) = - 1 \to Y (S (Q)) = Y (- 1)$
26	25	eleq1d	$⊢ S (Q) = - 1 \to (Y (S (Q)) \in {Base}_{R} \leftrightarrow Y (- 1) \in {Base}_{R})$
27	24 26	imbitrrid	$⊢ S (Q) = - 1 \to ((R \in Ring \land N \in Fin \land Q \in P) \to Y (S (Q)) \in {Base}_{R})$
28	15 27	jaoi	$⊢ (S (Q) = 1 \lor S (Q) = - 1) \to ((R \in Ring \land N \in Fin \land Q \in P) \to Y (S (Q)) \in {Base}_{R})$
29	6 28	syl	$⊢ S (Q) \in \{1, - 1\} \to ((R \in Ring \land N \in Fin \land Q \in P) \to Y (S (Q)) \in {Base}_{R})$
30	5 29	mpcom	$⊢ (R \in Ring \land N \in Fin \land Q \in P) \to Y (S (Q)) \in {Base}_{R}$

Metamath Proof Explorer

Theorem zrhpsgnelbas

Proof