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	⊢ 𝑆 = ( Poly₁ ‘ 𝑅 )
	ressply.2	⊢ 𝐻 = ( 𝑅 ↾_s 𝑇 )
	ressply.3	⊢ 𝑈 = ( Poly₁ ‘ 𝐻 )
	ressply.4	⊢ 𝐵 = ( Base ‘ 𝑈 )
	ressply.5	⊢ ( 𝜑 → 𝑇 ∈ ( SubRing ‘ 𝑅 ) )
	ressply10g.6	⊢ 𝑍 = ( 0_g ‘ 𝑆 )
Assertion	ressply10g	⊢ ( 𝜑 → 𝑍 = ( 0_g ‘ 𝑈 ) )

Proof

Step	Hyp	Ref	Expression
1		ressply.1	⊢ 𝑆 = ( Poly₁ ‘ 𝑅 )
2		ressply.2	⊢ 𝐻 = ( 𝑅 ↾_s 𝑇 )
3		ressply.3	⊢ 𝑈 = ( Poly₁ ‘ 𝐻 )
4		ressply.4	⊢ 𝐵 = ( Base ‘ 𝑈 )
5		ressply.5	⊢ ( 𝜑 → 𝑇 ∈ ( SubRing ‘ 𝑅 ) )
6		ressply10g.6	⊢ 𝑍 = ( 0_g ‘ 𝑆 )
7		eqid	⊢ ( algSc ‘ 𝑆 ) = ( algSc ‘ 𝑆 )
8		eqid	⊢ ( algSc ‘ 𝑈 ) = ( algSc ‘ 𝑈 )
9	1 7 2 3 5 8	subrg1ascl	⊢ ( 𝜑 → ( algSc ‘ 𝑈 ) = ( ( algSc ‘ 𝑆 ) ↾ 𝑇 ) )
10	9	fveq1d	⊢ ( 𝜑 → ( ( algSc ‘ 𝑈 ) ‘ ( 0_g ‘ 𝐻 ) ) = ( ( ( algSc ‘ 𝑆 ) ↾ 𝑇 ) ‘ ( 0_g ‘ 𝐻 ) ) )
11		eqid	⊢ ( 0_g ‘ 𝐻 ) = ( 0_g ‘ 𝐻 )
12		eqid	⊢ ( 0_g ‘ 𝑈 ) = ( 0_g ‘ 𝑈 )
13	2	subrgring	⊢ ( 𝑇 ∈ ( SubRing ‘ 𝑅 ) → 𝐻 ∈ Ring )
14	5 13	syl	⊢ ( 𝜑 → 𝐻 ∈ Ring )
15	3 8 11 12 14	ply1ascl0	⊢ ( 𝜑 → ( ( algSc ‘ 𝑈 ) ‘ ( 0_g ‘ 𝐻 ) ) = ( 0_g ‘ 𝑈 ) )
16		eqid	⊢ ( 0_g ‘ 𝑅 ) = ( 0_g ‘ 𝑅 )
17	2 16	subrg0	⊢ ( 𝑇 ∈ ( SubRing ‘ 𝑅 ) → ( 0_g ‘ 𝑅 ) = ( 0_g ‘ 𝐻 ) )
18	5 17	syl	⊢ ( 𝜑 → ( 0_g ‘ 𝑅 ) = ( 0_g ‘ 𝐻 ) )
19		subrgsubg	⊢ ( 𝑇 ∈ ( SubRing ‘ 𝑅 ) → 𝑇 ∈ ( SubGrp ‘ 𝑅 ) )
20	16	subg0cl	⊢ ( 𝑇 ∈ ( SubGrp ‘ 𝑅 ) → ( 0_g ‘ 𝑅 ) ∈ 𝑇 )
21	5 19 20	3syl	⊢ ( 𝜑 → ( 0_g ‘ 𝑅 ) ∈ 𝑇 )
22	18 21	eqeltrrd	⊢ ( 𝜑 → ( 0_g ‘ 𝐻 ) ∈ 𝑇 )
23	22	fvresd	⊢ ( 𝜑 → ( ( ( algSc ‘ 𝑆 ) ↾ 𝑇 ) ‘ ( 0_g ‘ 𝐻 ) ) = ( ( algSc ‘ 𝑆 ) ‘ ( 0_g ‘ 𝐻 ) ) )
24	10 15 23	3eqtr3d	⊢ ( 𝜑 → ( 0_g ‘ 𝑈 ) = ( ( algSc ‘ 𝑆 ) ‘ ( 0_g ‘ 𝐻 ) ) )
25	18	fveq2d	⊢ ( 𝜑 → ( ( algSc ‘ 𝑆 ) ‘ ( 0_g ‘ 𝑅 ) ) = ( ( algSc ‘ 𝑆 ) ‘ ( 0_g ‘ 𝐻 ) ) )
26		subrgrcl	⊢ ( 𝑇 ∈ ( SubRing ‘ 𝑅 ) → 𝑅 ∈ Ring )
27	5 26	syl	⊢ ( 𝜑 → 𝑅 ∈ Ring )
28	1 7 16 6 27	ply1ascl0	⊢ ( 𝜑 → ( ( algSc ‘ 𝑆 ) ‘ ( 0_g ‘ 𝑅 ) ) = 𝑍 )
29	24 25 28	3eqtr2rd	⊢ ( 𝜑 → 𝑍 = ( 0_g ‘ 𝑈 ) )

Metamath Proof Explorer

Theorem ressply10g

Proof