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 = ( ZRHom ` R )
	Assertion	zrhcopsgnelbas	\|- ( ( R e. Ring /\ N e. Fin /\ Q e. P ) -> ( ( Y o. S ) ` Q ) e. ( Base ` R ) )

Proof

Step	Hyp	Ref	Expression
1		zrhpsgnelbas.p	\|- P = ( Base ` ( SymGrp ` N ) )
2		zrhpsgnelbas.s	\|- S = ( pmSgn ` N )
3		zrhpsgnelbas.y	\|- Y = ( ZRHom ` R )
4	1 2	cofipsgn	\|- ( ( N e. Fin /\ Q e. P ) -> ( ( Y o. S ) ` Q ) = ( Y ` ( S ` Q ) ) )
5	4	3adant1	\|- ( ( R e. Ring /\ N e. Fin /\ Q e. P ) -> ( ( Y o. S ) ` Q ) = ( Y ` ( S ` Q ) ) )
6	1 2 3	zrhpsgnelbas	\|- ( ( R e. Ring /\ N e. Fin /\ Q e. P ) -> ( Y ` ( S ` Q ) ) e. ( Base ` R ) )
7	5 6	eqeltrd	\|- ( ( R e. Ring /\ N e. Fin /\ Q e. P ) -> ( ( Y o. S ) ` Q ) e. ( Base ` R ) )