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	⊢ 𝑃 = ( Base ‘ ( SymGrp ‘ 𝑁 ) )
	zrhpsgnelbas.s	⊢ 𝑆 = ( pmSgn ‘ 𝑁 )
	zrhpsgnelbas.y	⊢ 𝑌 = ( ℤRHom ‘ 𝑅 )
Assertion	zrhcopsgnelbas	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ∧ 𝑄 ∈ 𝑃 ) → ( ( 𝑌 ∘ 𝑆 ) ‘ 𝑄 ) ∈ ( Base ‘ 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		zrhpsgnelbas.p	⊢ 𝑃 = ( Base ‘ ( SymGrp ‘ 𝑁 ) )
2		zrhpsgnelbas.s	⊢ 𝑆 = ( pmSgn ‘ 𝑁 )
3		zrhpsgnelbas.y	⊢ 𝑌 = ( ℤRHom ‘ 𝑅 )
4	1 2	cofipsgn	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑄 ∈ 𝑃 ) → ( ( 𝑌 ∘ 𝑆 ) ‘ 𝑄 ) = ( 𝑌 ‘ ( 𝑆 ‘ 𝑄 ) ) )
5	4	3adant1	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ∧ 𝑄 ∈ 𝑃 ) → ( ( 𝑌 ∘ 𝑆 ) ‘ 𝑄 ) = ( 𝑌 ‘ ( 𝑆 ‘ 𝑄 ) ) )
6	1 2 3	zrhpsgnelbas	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ∧ 𝑄 ∈ 𝑃 ) → ( 𝑌 ‘ ( 𝑆 ‘ 𝑄 ) ) ∈ ( Base ‘ 𝑅 ) )
7	5 6	eqeltrd	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ∧ 𝑄 ∈ 𝑃 ) → ( ( 𝑌 ∘ 𝑆 ) ‘ 𝑄 ) ∈ ( Base ‘ 𝑅 ) )