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 = ( Poly1 ` R )
	ressply.2	|- H = ( R |`s T )
	ressply.3	|- U = ( Poly1 ` H )
	ressply.4	|- B = ( Base ` U )
	ressply.5	|- ( ph -> T e. ( SubRing ` R ) )
	ressply10g.6	|- Z = ( 0g ` S )
Assertion	ressply10g	|- ( ph -> Z = ( 0g ` U ) )

Proof

Step	Hyp	Ref	Expression
1		ressply.1	|- S = ( Poly1 ` R )
2		ressply.2	|- H = ( R |`s T )
3		ressply.3	|- U = ( Poly1 ` H )
4		ressply.4	|- B = ( Base ` U )
5		ressply.5	|- ( ph -> T e. ( SubRing ` R ) )
6		ressply10g.6	|- Z = ( 0g ` S )
7		eqid	|- ( algSc ` S ) = ( algSc ` S )
8		eqid	|- ( algSc ` U ) = ( algSc ` U )
9	1 7 2 3 5 8	subrg1ascl	|- ( ph -> ( algSc ` U ) = ( ( algSc ` S ) |` T ) )
10	9	fveq1d	|- ( ph -> ( ( algSc ` U ) ` ( 0g ` H ) ) = ( ( ( algSc ` S ) |` T ) ` ( 0g ` H ) ) )
11		eqid	|- ( 0g ` H ) = ( 0g ` H )
12		eqid	|- ( 0g ` U ) = ( 0g ` U )
13	2	subrgring	|- ( T e. ( SubRing ` R ) -> H e. Ring )
14	5 13	syl	|- ( ph -> H e. Ring )
15	3 8 11 12 14	ply1ascl0	|- ( ph -> ( ( algSc ` U ) ` ( 0g ` H ) ) = ( 0g ` U ) )
16		eqid	|- ( 0g ` R ) = ( 0g ` R )
17	2 16	subrg0	|- ( T e. ( SubRing ` R ) -> ( 0g ` R ) = ( 0g ` H ) )
18	5 17	syl	|- ( ph -> ( 0g ` R ) = ( 0g ` H ) )
19		subrgsubg	|- ( T e. ( SubRing ` R ) -> T e. ( SubGrp ` R ) )
20	16	subg0cl	|- ( T e. ( SubGrp ` R ) -> ( 0g ` R ) e. T )
21	5 19 20	3syl	|- ( ph -> ( 0g ` R ) e. T )
22	18 21	eqeltrrd	|- ( ph -> ( 0g ` H ) e. T )
23	22	fvresd	|- ( ph -> ( ( ( algSc ` S ) |` T ) ` ( 0g ` H ) ) = ( ( algSc ` S ) ` ( 0g ` H ) ) )
24	10 15 23	3eqtr3d	|- ( ph -> ( 0g ` U ) = ( ( algSc ` S ) ` ( 0g ` H ) ) )
25	18	fveq2d	|- ( ph -> ( ( algSc ` S ) ` ( 0g ` R ) ) = ( ( algSc ` S ) ` ( 0g ` H ) ) )
26		subrgrcl	|- ( T e. ( SubRing ` R ) -> R e. Ring )
27	5 26	syl	|- ( ph -> R e. Ring )
28	1 7 16 6 27	ply1ascl0	|- ( ph -> ( ( algSc ` S ) ` ( 0g ` R ) ) = Z )
29	24 25 28	3eqtr2rd	|- ( ph -> Z = ( 0g ` U ) )