Theorem ressply10g

Description: A restricted polynomial algebra has the same group identity (zero polynomial). (Contributed by Thierry Arnoux, 20-Jan-2025)

	Ref	Expression
Hypotheses	ressply.1	$$⊢S={\mathrm{Poly}}_1\left(R\right)$$
	ressply.2	$$⊢H=R{\upharpoonright }_{𝑠}T$$
	ressply.3	$$⊢U={\mathrm{Poly}}_1\left(H\right)$$
	ressply.4	$$⊢B={\mathrm{Base}}_U$$
	ressply.5	$$⊢\phi \to T\in \mathrm{SubRing}\left(R\right)$$
	ressply10g.6	$$⊢Z=0_S$$
Assertion	ressply10g	$$⊢\phi \to Z=0_U$$

Proof

Step	Hyp	Ref	Expression
1		ressply.1	$$⊢S={\mathrm{Poly}}_1\left(R\right)$$
2		ressply.2	$$⊢H=R{\upharpoonright }_{𝑠}T$$
3		ressply.3	$$⊢U={\mathrm{Poly}}_1\left(H\right)$$
4		ressply.4	$$⊢B={\mathrm{Base}}_U$$
5		ressply.5	$$⊢\phi \to T\in \mathrm{SubRing}\left(R\right)$$
6		ressply10g.6	$$⊢Z=0_S$$
7		eqid	$$⊢\mathrm{algSc}\left(S\right)=\mathrm{algSc}\left(S\right)$$
8		eqid	$$⊢\mathrm{algSc}\left(U\right)=\mathrm{algSc}\left(U\right)$$
9	1 7 2 3 5 8	subrg1ascl	$$⊢\phi \to \mathrm{algSc}\left(U\right)={\mathrm{algSc}\left(S\right)\upharpoonright }_T$$
10	9	fveq1d	$$⊢\phi \to \mathrm{algSc}\left(U\right)\left(0_H\right)=\left({\mathrm{algSc}\left(S\right)\upharpoonright }_T\right)\left(0_H\right)$$
11		eqid	$$⊢0_H=0_H$$
12		eqid	$$⊢0_U=0_U$$
13	2	subrgring	$$⊢T\in \mathrm{SubRing}\left(R\right)\to H\in \mathrm{Ring}$$
14	5 13	syl	$$⊢\phi \to H\in \mathrm{Ring}$$
15	3 8 11 12 14	ply1ascl0	$$⊢\phi \to \mathrm{algSc}\left(U\right)\left(0_H\right)=0_U$$
16		eqid	$$⊢0_R=0_R$$
17	2 16	subrg0	$$⊢T\in \mathrm{SubRing}\left(R\right)\to 0_R=0_H$$
18	5 17	syl	$$⊢\phi \to 0_R=0_H$$
19		subrgsubg	$$⊢T\in \mathrm{SubRing}\left(R\right)\to T\in \mathrm{SubGrp}\left(R\right)$$
20	16	subg0cl	$$⊢T\in \mathrm{SubGrp}\left(R\right)\to 0_R\in T$$
21	5 19 20	3syl	$$⊢\phi \to 0_R\in T$$
22	18 21	eqeltrrd	$$⊢\phi \to 0_H\in T$$
23	22	fvresd	$$⊢\phi \to \left({\mathrm{algSc}\left(S\right)\upharpoonright }_T\right)\left(0_H\right)=\mathrm{algSc}\left(S\right)\left(0_H\right)$$
24	10 15 23	3eqtr3d	$$⊢\phi \to 0_U=\mathrm{algSc}\left(S\right)\left(0_H\right)$$
25	18	fveq2d	$$⊢\phi \to \mathrm{algSc}\left(S\right)\left(0_R\right)=\mathrm{algSc}\left(S\right)\left(0_H\right)$$
26		subrgrcl	$$⊢T\in \mathrm{SubRing}\left(R\right)\to R\in \mathrm{Ring}$$
27	5 26	syl	$$⊢\phi \to R\in \mathrm{Ring}$$
28	1 7 16 6 27	ply1ascl0	$$⊢\phi \to \mathrm{algSc}\left(S\right)\left(0_R\right)=Z$$
29	24 25 28	3eqtr2rd	$$⊢\phi \to Z=0_U$$