Theorem rhmply1vr1

Description: A ring homomorphism between two univariate polynomial algebras sends one variable to the other. (Contributed by SN, 20-May-2025)

	Ref	Expression
Hypotheses	rhmply1vr1.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
	rhmply1vr1.q	$$⊢Q={\mathrm{Poly}}_1\left(S\right)$$
	rhmply1vr1.b	$$⊢B={\mathrm{Base}}_P$$
	rhmply1vr1.f	$$⊢F=\left(p\in B⟼H\circ p\right)$$
	rhmply1vr1.x	$$⊢X={\mathrm{var}}_1\left(R\right)$$
	rhmply1vr1.y	$$⊢Y={\mathrm{var}}_1\left(S\right)$$
	rhmply1vr1.h	$$⊢\phi \to H\in \left(R\mathrm{RingHom}S\right)$$
Assertion	rhmply1vr1	$$⊢\phi \to F\left(X\right)=Y$$

Proof

Step	Hyp	Ref	Expression
1		rhmply1vr1.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
2		rhmply1vr1.q	$$⊢Q={\mathrm{Poly}}_1\left(S\right)$$
3		rhmply1vr1.b	$$⊢B={\mathrm{Base}}_P$$
4		rhmply1vr1.f	$$⊢F=\left(p\in B⟼H\circ p\right)$$
5		rhmply1vr1.x	$$⊢X={\mathrm{var}}_1\left(R\right)$$
6		rhmply1vr1.y	$$⊢Y={\mathrm{var}}_1\left(S\right)$$
7		rhmply1vr1.h	$$⊢\phi \to H\in \left(R\mathrm{RingHom}S\right)$$
8		coeq2	$$⊢p=X\to H\circ p=H\circ X$$
9		rhmrcl1	$$⊢H\in \left(R\mathrm{RingHom}S\right)\to R\in \mathrm{Ring}$$
10	7 9	syl	$$⊢\phi \to R\in \mathrm{Ring}$$
11	5 1 3	vr1cl	$$⊢R\in \mathrm{Ring}\to X\in B$$
12	10 11	syl	$$⊢\phi \to X\in B$$
13	5	fvexi	$$⊢X\in \mathrm{V}$$
14	13	a1i	$$⊢\phi \to X\in \mathrm{V}$$
15	7 14	coexd	$$⊢\phi \to H\circ X\in \mathrm{V}$$
16	4 8 12 15	fvmptd3	$$⊢\phi \to F\left(X\right)=H\circ X$$
17		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
18		eqid	$$⊢{\mathrm{Base}}_S={\mathrm{Base}}_S$$
19	17 18	rhmf	$$⊢H\in \left(R\mathrm{RingHom}S\right)\to H:{\mathrm{Base}}_R⟶{\mathrm{Base}}_S$$
20	7 19	syl	$$⊢\phi \to H:{\mathrm{Base}}_R⟶{\mathrm{Base}}_S$$
21		eqid	$$⊢1_R=1_R$$
22	17 21	ringidcl	$$⊢R\in \mathrm{Ring}\to 1_R\in {\mathrm{Base}}_R$$
23	10 22	syl	$$⊢\phi \to 1_R\in {\mathrm{Base}}_R$$
24		eqid	$$⊢0_R=0_R$$
25	17 24	ring0cl	$$⊢R\in \mathrm{Ring}\to 0_R\in {\mathrm{Base}}_R$$
26	10 25	syl	$$⊢\phi \to 0_R\in {\mathrm{Base}}_R$$
27	23 26	ifcld	$$⊢\phi \to if\left(f=\left(y\in 1_{𝑜}⟼if\left(y=\varnothing ,1,0\right)\right),1_R,0_R\right)\in {\mathrm{Base}}_R$$
28	27	adantr	$$⊢\left(\phi \wedge f\in \left\{h\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\to if\left(f=\left(y\in 1_{𝑜}⟼if\left(y=\varnothing ,1,0\right)\right),1_R,0_R\right)\in {\mathrm{Base}}_R$$
29	20 28	cofmpt	$$⊢\phi \to H\circ \left(f\in \left\{h\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼if\left(f=\left(y\in 1_{𝑜}⟼if\left(y=\varnothing ,1,0\right)\right),1_R,0_R\right)\right)=\left(f\in \left\{h\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼H\left(if\left(f=\left(y\in 1_{𝑜}⟼if\left(y=\varnothing ,1,0\right)\right),1_R,0_R\right)\right)\right)$$
30		fvif	$$⊢H\left(if\left(f=\left(y\in 1_{𝑜}⟼if\left(y=\varnothing ,1,0\right)\right),1_R,0_R\right)\right)=if\left(f=\left(y\in 1_{𝑜}⟼if\left(y=\varnothing ,1,0\right)\right),H\left(1_R\right),H\left(0_R\right)\right)$$
31		eqid	$$⊢1_S=1_S$$
32	21 31	rhm1	$$⊢H\in \left(R\mathrm{RingHom}S\right)\to H\left(1_R\right)=1_S$$
33	7 32	syl	$$⊢\phi \to H\left(1_R\right)=1_S$$
34		rhmghm	$$⊢H\in \left(R\mathrm{RingHom}S\right)\to H\in \left(R\mathrm{GrpHom}S\right)$$
35		eqid	$$⊢0_S=0_S$$
36	24 35	ghmid	$$⊢H\in \left(R\mathrm{GrpHom}S\right)\to H\left(0_R\right)=0_S$$
37	7 34 36	3syl	$$⊢\phi \to H\left(0_R\right)=0_S$$
38	33 37	ifeq12d	$$⊢\phi \to if\left(f=\left(y\in 1_{𝑜}⟼if\left(y=\varnothing ,1,0\right)\right),H\left(1_R\right),H\left(0_R\right)\right)=if\left(f=\left(y\in 1_{𝑜}⟼if\left(y=\varnothing ,1,0\right)\right),1_S,0_S\right)$$
39	30 38	eqtrid	$$⊢\phi \to H\left(if\left(f=\left(y\in 1_{𝑜}⟼if\left(y=\varnothing ,1,0\right)\right),1_R,0_R\right)\right)=if\left(f=\left(y\in 1_{𝑜}⟼if\left(y=\varnothing ,1,0\right)\right),1_S,0_S\right)$$
40	39	mpteq2dv	$$⊢\phi \to \left(f\in \left\{h\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼H\left(if\left(f=\left(y\in 1_{𝑜}⟼if\left(y=\varnothing ,1,0\right)\right),1_R,0_R\right)\right)\right)=\left(f\in \left\{h\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼if\left(f=\left(y\in 1_{𝑜}⟼if\left(y=\varnothing ,1,0\right)\right),1_S,0_S\right)\right)$$
41	29 40	eqtrd	$$⊢\phi \to H\circ \left(f\in \left\{h\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼if\left(f=\left(y\in 1_{𝑜}⟼if\left(y=\varnothing ,1,0\right)\right),1_R,0_R\right)\right)=\left(f\in \left\{h\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼if\left(f=\left(y\in 1_{𝑜}⟼if\left(y=\varnothing ,1,0\right)\right),1_S,0_S\right)\right)$$
42		eqid	$$⊢1_{𝑜}\mathrm{mVar}R=1_{𝑜}\mathrm{mVar}R$$
43		eqid	$$⊢\left\{h\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}=\left\{h\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
44		1oex	$$⊢1_{𝑜}\in \mathrm{V}$$
45	44	a1i	$$⊢\phi \to 1_{𝑜}\in \mathrm{V}$$
46		0lt1o	$$⊢\varnothing \in 1_{𝑜}$$
47	46	a1i	$$⊢\phi \to \varnothing \in 1_{𝑜}$$
48	42 43 24 21 45 10 47	mvrval	$$⊢\phi \to \left(1_{𝑜}\mathrm{mVar}R\right)\left(\varnothing \right)=\left(f\in \left\{h\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼if\left(f=\left(y\in 1_{𝑜}⟼if\left(y=\varnothing ,1,0\right)\right),1_R,0_R\right)\right)$$
49	48	coeq2d	$$⊢\phi \to H\circ \left(1_{𝑜}\mathrm{mVar}R\right)\left(\varnothing \right)=H\circ \left(f\in \left\{h\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼if\left(f=\left(y\in 1_{𝑜}⟼if\left(y=\varnothing ,1,0\right)\right),1_R,0_R\right)\right)$$
50		eqid	$$⊢1_{𝑜}\mathrm{mVar}S=1_{𝑜}\mathrm{mVar}S$$
51		rhmrcl2	$$⊢H\in \left(R\mathrm{RingHom}S\right)\to S\in \mathrm{Ring}$$
52	7 51	syl	$$⊢\phi \to S\in \mathrm{Ring}$$
53	50 43 35 31 45 52 47	mvrval	$$⊢\phi \to \left(1_{𝑜}\mathrm{mVar}S\right)\left(\varnothing \right)=\left(f\in \left\{h\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼if\left(f=\left(y\in 1_{𝑜}⟼if\left(y=\varnothing ,1,0\right)\right),1_S,0_S\right)\right)$$
54	41 49 53	3eqtr4d	$$⊢\phi \to H\circ \left(1_{𝑜}\mathrm{mVar}R\right)\left(\varnothing \right)=\left(1_{𝑜}\mathrm{mVar}S\right)\left(\varnothing \right)$$
55	5	vr1val	$$⊢X=\left(1_{𝑜}\mathrm{mVar}R\right)\left(\varnothing \right)$$
56	55	coeq2i	$$⊢H\circ X=H\circ \left(1_{𝑜}\mathrm{mVar}R\right)\left(\varnothing \right)$$
57	6	vr1val	$$⊢Y=\left(1_{𝑜}\mathrm{mVar}S\right)\left(\varnothing \right)$$
58	54 56 57	3eqtr4g	$$⊢\phi \to H\circ X=Y$$
59	16 58	eqtrd	$$⊢\phi \to F\left(X\right)=Y$$