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 ) )