Theorem ply1asclzrhval

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

	Ref	Expression
Hypotheses	ply1asclzrhval.1	$$⊢W={\mathrm{Poly}}_1\left(R\right)$$
	ply1asclzrhval.2	$$⊢A=\mathrm{algSc}\left(W\right)$$
	ply1asclzrhval.3	$$⊢B=\mathrm{\mathbb{Z}RHom}\left(W\right)$$
	ply1asclzrhval.4	$$⊢C=\mathrm{\mathbb{Z}RHom}\left(R\right)$$
	ply1asclzrhval.5	$$⊢\phi \to R\in \mathrm{CRing}$$
	ply1asclzrhval.6	$$⊢\phi \to X\in \mathbb{Z}$$
Assertion	ply1asclzrhval	$$⊢\phi \to A\left(C\left(X\right)\right)=B\left(X\right)$$

Proof

Step	Hyp	Ref	Expression
1		ply1asclzrhval.1	$$⊢W={\mathrm{Poly}}_1\left(R\right)$$
2		ply1asclzrhval.2	$$⊢A=\mathrm{algSc}\left(W\right)$$
3		ply1asclzrhval.3	$$⊢B=\mathrm{\mathbb{Z}RHom}\left(W\right)$$
4		ply1asclzrhval.4	$$⊢C=\mathrm{\mathbb{Z}RHom}\left(R\right)$$
5		ply1asclzrhval.5	$$⊢\phi \to R\in \mathrm{CRing}$$
6		ply1asclzrhval.6	$$⊢\phi \to X\in \mathbb{Z}$$
7		eqid	$$⊢{\mathrm{Poly}}_1\left(R\right)={\mathrm{Poly}}_1\left(R\right)$$
8	7	ply1assa	$$⊢R\in \mathrm{CRing}\to {\mathrm{Poly}}_1\left(R\right)\in \mathrm{AssAlg}$$
9	5 8	syl	$$⊢\phi \to {\mathrm{Poly}}_1\left(R\right)\in \mathrm{AssAlg}$$
10	1 9	eqeltrid	$$⊢\phi \to W\in \mathrm{AssAlg}$$
11		eqid	$$⊢\mathrm{Scalar}\left(W\right)=\mathrm{Scalar}\left(W\right)$$
12	2 11	asclrhm	$$⊢W\in \mathrm{AssAlg}\to A\in \left(\mathrm{Scalar}\left(W\right)\mathrm{RingHom}W\right)$$
13	10 12	syl	$$⊢\phi \to A\in \left(\mathrm{Scalar}\left(W\right)\mathrm{RingHom}W\right)$$
14	5	crngringd	$$⊢\phi \to R\in \mathrm{Ring}$$
15	1	ply1sca	$$⊢R\in \mathrm{Ring}\to R=\mathrm{Scalar}\left(W\right)$$
16	14 15	syl	$$⊢\phi \to R=\mathrm{Scalar}\left(W\right)$$
17	16	eqcomd	$$⊢\phi \to \mathrm{Scalar}\left(W\right)=R$$
18	17	oveq1d	$$⊢\phi \to \mathrm{Scalar}\left(W\right)\mathrm{RingHom}W=R\mathrm{RingHom}W$$
19	13 18	eleqtrd	$$⊢\phi \to A\in \left(R\mathrm{RingHom}W\right)$$
20	19 6 4 3	rhmzrhval	$$⊢\phi \to A\left(C\left(X\right)\right)=B\left(X\right)$$