Theorem ply1asclzrhval

Description: Transfer results from algebraic scalars and ZR ring homomorphisms. (Contributed by metakunt, 17-Jun-2025)

	Ref	Expression
Hypotheses	ply1asclzrhval.1	⊢ 𝑊 = ( Poly1 ‘ 𝑅 )
	ply1asclzrhval.2	⊢ 𝐴 = ( algSc ‘ 𝑊 )
	ply1asclzrhval.3	⊢ 𝐵 = ( ℤRHom ‘ 𝑊 )
	ply1asclzrhval.4	⊢ 𝐶 = ( ℤRHom ‘ 𝑅 )
	ply1asclzrhval.5	⊢ ( 𝜑 → 𝑅 ∈ CRing )
	ply1asclzrhval.6	⊢ ( 𝜑 → 𝑋 ∈ ℤ )
Assertion	ply1asclzrhval	⊢ ( 𝜑 → ( 𝐴 ‘ ( 𝐶 ‘ 𝑋 ) ) = ( 𝐵 ‘ 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		ply1asclzrhval.1	⊢ 𝑊 = ( Poly1 ‘ 𝑅 )
2		ply1asclzrhval.2	⊢ 𝐴 = ( algSc ‘ 𝑊 )
3		ply1asclzrhval.3	⊢ 𝐵 = ( ℤRHom ‘ 𝑊 )
4		ply1asclzrhval.4	⊢ 𝐶 = ( ℤRHom ‘ 𝑅 )
5		ply1asclzrhval.5	⊢ ( 𝜑 → 𝑅 ∈ CRing )
6		ply1asclzrhval.6	⊢ ( 𝜑 → 𝑋 ∈ ℤ )
7		eqid	⊢ ( Poly1 ‘ 𝑅 ) = ( Poly1 ‘ 𝑅 )
8	7	ply1assa	⊢ ( 𝑅 ∈ CRing → ( Poly1 ‘ 𝑅 ) ∈ AssAlg )
9	5 8	syl	⊢ ( 𝜑 → ( Poly1 ‘ 𝑅 ) ∈ AssAlg )
10	1 9	eqeltrid	⊢ ( 𝜑 → 𝑊 ∈ AssAlg )
11		eqid	⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
12	2 11	asclrhm	⊢ ( 𝑊 ∈ AssAlg → 𝐴 ∈ ( ( Scalar ‘ 𝑊 ) RingHom 𝑊 ) )
13	10 12	syl	⊢ ( 𝜑 → 𝐴 ∈ ( ( Scalar ‘ 𝑊 ) RingHom 𝑊 ) )
14	5	crngringd	⊢ ( 𝜑 → 𝑅 ∈ Ring )
15	1	ply1sca	⊢ ( 𝑅 ∈ Ring → 𝑅 = ( Scalar ‘ 𝑊 ) )
16	14 15	syl	⊢ ( 𝜑 → 𝑅 = ( Scalar ‘ 𝑊 ) )
17	16	eqcomd	⊢ ( 𝜑 → ( Scalar ‘ 𝑊 ) = 𝑅 )
18	17	oveq1d	⊢ ( 𝜑 → ( ( Scalar ‘ 𝑊 ) RingHom 𝑊 ) = ( 𝑅 RingHom 𝑊 ) )
19	13 18	eleqtrd	⊢ ( 𝜑 → 𝐴 ∈ ( 𝑅 RingHom 𝑊 ) )
20	19 6 4 3	rhmzrhval	⊢ ( 𝜑 → ( 𝐴 ‘ ( 𝐶 ‘ 𝑋 ) ) = ( 𝐵 ‘ 𝑋 ) )