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

Metamath Proof Explorer

Theorem zrhcopsgnelbas

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

		Ref	Expression
	Hypotheses	zrhpsgnelbas.p	$⊢ P = {Base}_{SymGrp (N)}$
		zrhpsgnelbas.s	$⊢ S = pmSgn (N)$
		zrhpsgnelbas.y	$⊢ Y = ℤRHom (R)$
	Assertion	zrhcopsgnelbas	$⊢ (R \in Ring \land N \in Fin \land Q \in P) \to (Y \circ 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	cofipsgn	$⊢ (N \in Fin \land Q \in P) \to (Y \circ S) (Q) = Y (S (Q))$
5	4	3adant1	$⊢ (R \in Ring \land N \in Fin \land Q \in P) \to (Y \circ S) (Q) = Y (S (Q))$
6	1 2 3	zrhpsgnelbas	$⊢ (R \in Ring \land N \in Fin \land Q \in P) \to Y (S (Q)) \in {Base}_{R}$
7	5 6	eqeltrd	$⊢ (R \in Ring \land N \in Fin \land Q \in P) \to (Y \circ S) (Q) \in {Base}_{R}$