Theorem ply1asclzrhval

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

	Ref	Expression
Hypotheses	ply1asclzrhval.1	|- W = ( Poly1 ` R )
	ply1asclzrhval.2	|- A = ( algSc ` W )
	ply1asclzrhval.3	|- B = ( ZRHom ` W )
	ply1asclzrhval.4	|- C = ( ZRHom ` R )
	ply1asclzrhval.5	|- ( ph -> R e. CRing )
	ply1asclzrhval.6	|- ( ph -> X e. ZZ )
Assertion	ply1asclzrhval	|- ( ph -> ( A ` ( C ` X ) ) = ( B ` X ) )

Proof

Step	Hyp	Ref	Expression
1		ply1asclzrhval.1	|- W = ( Poly1 ` R )
2		ply1asclzrhval.2	|- A = ( algSc ` W )
3		ply1asclzrhval.3	|- B = ( ZRHom ` W )
4		ply1asclzrhval.4	|- C = ( ZRHom ` R )
5		ply1asclzrhval.5	|- ( ph -> R e. CRing )
6		ply1asclzrhval.6	|- ( ph -> X e. ZZ )
7		eqid	|- ( Poly1 ` R ) = ( Poly1 ` R )
8	7	ply1assa	|- ( R e. CRing -> ( Poly1 ` R ) e. AssAlg )
9	5 8	syl	|- ( ph -> ( Poly1 ` R ) e. AssAlg )
10	1 9	eqeltrid	|- ( ph -> W e. AssAlg )
11		eqid	|- ( Scalar ` W ) = ( Scalar ` W )
12	2 11	asclrhm	|- ( W e. AssAlg -> A e. ( ( Scalar ` W ) RingHom W ) )
13	10 12	syl	|- ( ph -> A e. ( ( Scalar ` W ) RingHom W ) )
14	5	crngringd	|- ( ph -> R e. Ring )
15	1	ply1sca	|- ( R e. Ring -> R = ( Scalar ` W ) )
16	14 15	syl	|- ( ph -> R = ( Scalar ` W ) )
17	16	eqcomd	|- ( ph -> ( Scalar ` W ) = R )
18	17	oveq1d	|- ( ph -> ( ( Scalar ` W ) RingHom W ) = ( R RingHom W ) )
19	13 18	eleqtrd	|- ( ph -> A e. ( R RingHom W ) )
20	19 6 4 3	rhmzrhval	|- ( ph -> ( A ` ( C ` X ) ) = ( B ` X ) )