mplsubrg

Description: The set of polynomials is closed under multiplication, i.e. it is a subring of the set of power series. (Contributed by Mario Carneiro, 9-Jan-2015)

	Ref	Expression
Hypotheses	mplsubg.s	⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 )
	mplsubg.p	⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
	mplsubg.u	⊢ 𝑈 = ( Base ‘ 𝑃 )
	mplsubg.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
	mpllss.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
Assertion	mplsubrg	⊢ ( 𝜑 → 𝑈 ∈ ( SubRing ‘ 𝑆 ) )

Proof

Step	Hyp	Ref	Expression
1		mplsubg.s	⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 )
2		mplsubg.p	⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
3		mplsubg.u	⊢ 𝑈 = ( Base ‘ 𝑃 )
4		mplsubg.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
5		mpllss.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
6		ringgrp	⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Grp )
7	5 6	syl	⊢ ( 𝜑 → 𝑅 ∈ Grp )
8	1 2 3 4 7	mplsubg	⊢ ( 𝜑 → 𝑈 ∈ ( SubGrp ‘ 𝑆 ) )
9	1 4 5	psrring	⊢ ( 𝜑 → 𝑆 ∈ Ring )
10		eqid	⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
11		eqid	⊢ ( 1_r ‘ 𝑆 ) = ( 1_r ‘ 𝑆 )
12	10 11	ringidcl	⊢ ( 𝑆 ∈ Ring → ( 1_r ‘ 𝑆 ) ∈ ( Base ‘ 𝑆 ) )
13	9 12	syl	⊢ ( 𝜑 → ( 1_r ‘ 𝑆 ) ∈ ( Base ‘ 𝑆 ) )
14		eqid	⊢ { 𝑓 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑓 “ ℕ ) ∈ Fin } = { 𝑓 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑓 “ ℕ ) ∈ Fin }
15		eqid	⊢ ( 0_g ‘ 𝑅 ) = ( 0_g ‘ 𝑅 )
16		eqid	⊢ ( 1_r ‘ 𝑅 ) = ( 1_r ‘ 𝑅 )
17	1 4 5 14 15 16 11	psr1	⊢ ( 𝜑 → ( 1_r ‘ 𝑆 ) = ( 𝑘 ∈ { 𝑓 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑓 “ ℕ ) ∈ Fin } ↦ if ( 𝑘 = ( 𝐼 × { 0 } ) , ( 1_r ‘ 𝑅 ) , ( 0_g ‘ 𝑅 ) ) ) )
18		ovex	⊢ ( ℕ₀ ↑_m 𝐼 ) ∈ V
19	18	mptrabex	⊢ ( 𝑘 ∈ { 𝑓 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑓 “ ℕ ) ∈ Fin } ↦ if ( 𝑘 = ( 𝐼 × { 0 } ) , ( 1_r ‘ 𝑅 ) , ( 0_g ‘ 𝑅 ) ) ) ∈ V
20		funmpt	⊢ Fun ( 𝑘 ∈ { 𝑓 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑓 “ ℕ ) ∈ Fin } ↦ if ( 𝑘 = ( 𝐼 × { 0 } ) , ( 1_r ‘ 𝑅 ) , ( 0_g ‘ 𝑅 ) ) )
21		fvex	⊢ ( 0_g ‘ 𝑅 ) ∈ V
22	19 20 21	3pm3.2i	⊢ ( ( 𝑘 ∈ { 𝑓 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑓 “ ℕ ) ∈ Fin } ↦ if ( 𝑘 = ( 𝐼 × { 0 } ) , ( 1_r ‘ 𝑅 ) , ( 0_g ‘ 𝑅 ) ) ) ∈ V ∧ Fun ( 𝑘 ∈ { 𝑓 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑓 “ ℕ ) ∈ Fin } ↦ if ( 𝑘 = ( 𝐼 × { 0 } ) , ( 1_r ‘ 𝑅 ) , ( 0_g ‘ 𝑅 ) ) ) ∧ ( 0_g ‘ 𝑅 ) ∈ V )
23	22	a1i	⊢ ( 𝜑 → ( ( 𝑘 ∈ { 𝑓 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑓 “ ℕ ) ∈ Fin } ↦ if ( 𝑘 = ( 𝐼 × { 0 } ) , ( 1_r ‘ 𝑅 ) , ( 0_g ‘ 𝑅 ) ) ) ∈ V ∧ Fun ( 𝑘 ∈ { 𝑓 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑓 “ ℕ ) ∈ Fin } ↦ if ( 𝑘 = ( 𝐼 × { 0 } ) , ( 1_r ‘ 𝑅 ) , ( 0_g ‘ 𝑅 ) ) ) ∧ ( 0_g ‘ 𝑅 ) ∈ V ) )
24		snfi	⊢ { ( 𝐼 × { 0 } ) } ∈ Fin
25	24	a1i	⊢ ( 𝜑 → { ( 𝐼 × { 0 } ) } ∈ Fin )
26		eldifsni	⊢ ( 𝑘 ∈ ( { 𝑓 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑓 “ ℕ ) ∈ Fin } ∖ { ( 𝐼 × { 0 } ) } ) → 𝑘 ≠ ( 𝐼 × { 0 } ) )
27	26	adantl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( { 𝑓 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑓 “ ℕ ) ∈ Fin } ∖ { ( 𝐼 × { 0 } ) } ) ) → 𝑘 ≠ ( 𝐼 × { 0 } ) )
28		ifnefalse	⊢ ( 𝑘 ≠ ( 𝐼 × { 0 } ) → if ( 𝑘 = ( 𝐼 × { 0 } ) , ( 1_r ‘ 𝑅 ) , ( 0_g ‘ 𝑅 ) ) = ( 0_g ‘ 𝑅 ) )
29	27 28	syl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( { 𝑓 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑓 “ ℕ ) ∈ Fin } ∖ { ( 𝐼 × { 0 } ) } ) ) → if ( 𝑘 = ( 𝐼 × { 0 } ) , ( 1_r ‘ 𝑅 ) , ( 0_g ‘ 𝑅 ) ) = ( 0_g ‘ 𝑅 ) )
30	18	rabex	⊢ { 𝑓 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑓 “ ℕ ) ∈ Fin } ∈ V
31	30	a1i	⊢ ( 𝜑 → { 𝑓 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑓 “ ℕ ) ∈ Fin } ∈ V )
32	29 31	suppss2	⊢ ( 𝜑 → ( ( 𝑘 ∈ { 𝑓 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑓 “ ℕ ) ∈ Fin } ↦ if ( 𝑘 = ( 𝐼 × { 0 } ) , ( 1_r ‘ 𝑅 ) , ( 0_g ‘ 𝑅 ) ) ) supp ( 0_g ‘ 𝑅 ) ) ⊆ { ( 𝐼 × { 0 } ) } )
33		suppssfifsupp	⊢ ( ( ( ( 𝑘 ∈ { 𝑓 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑓 “ ℕ ) ∈ Fin } ↦ if ( 𝑘 = ( 𝐼 × { 0 } ) , ( 1_r ‘ 𝑅 ) , ( 0_g ‘ 𝑅 ) ) ) ∈ V ∧ Fun ( 𝑘 ∈ { 𝑓 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑓 “ ℕ ) ∈ Fin } ↦ if ( 𝑘 = ( 𝐼 × { 0 } ) , ( 1_r ‘ 𝑅 ) , ( 0_g ‘ 𝑅 ) ) ) ∧ ( 0_g ‘ 𝑅 ) ∈ V ) ∧ ( { ( 𝐼 × { 0 } ) } ∈ Fin ∧ ( ( 𝑘 ∈ { 𝑓 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑓 “ ℕ ) ∈ Fin } ↦ if ( 𝑘 = ( 𝐼 × { 0 } ) , ( 1_r ‘ 𝑅 ) , ( 0_g ‘ 𝑅 ) ) ) supp ( 0_g ‘ 𝑅 ) ) ⊆ { ( 𝐼 × { 0 } ) } ) ) → ( 𝑘 ∈ { 𝑓 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑓 “ ℕ ) ∈ Fin } ↦ if ( 𝑘 = ( 𝐼 × { 0 } ) , ( 1_r ‘ 𝑅 ) , ( 0_g ‘ 𝑅 ) ) ) finSupp ( 0_g ‘ 𝑅 ) )
34	23 25 32 33	syl12anc	⊢ ( 𝜑 → ( 𝑘 ∈ { 𝑓 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑓 “ ℕ ) ∈ Fin } ↦ if ( 𝑘 = ( 𝐼 × { 0 } ) , ( 1_r ‘ 𝑅 ) , ( 0_g ‘ 𝑅 ) ) ) finSupp ( 0_g ‘ 𝑅 ) )
35	17 34	eqbrtrd	⊢ ( 𝜑 → ( 1_r ‘ 𝑆 ) finSupp ( 0_g ‘ 𝑅 ) )
36	2 1 10 15 3	mplelbas	⊢ ( ( 1_r ‘ 𝑆 ) ∈ 𝑈 ↔ ( ( 1_r ‘ 𝑆 ) ∈ ( Base ‘ 𝑆 ) ∧ ( 1_r ‘ 𝑆 ) finSupp ( 0_g ‘ 𝑅 ) ) )
37	13 35 36	sylanbrc	⊢ ( 𝜑 → ( 1_r ‘ 𝑆 ) ∈ 𝑈 )
38	4	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → 𝐼 ∈ 𝑊 )
39	5	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → 𝑅 ∈ Ring )
40		eqid	⊢ ( ∘_f + “ ( ( 𝑥 supp ( 0_g ‘ 𝑅 ) ) × ( 𝑦 supp ( 0_g ‘ 𝑅 ) ) ) ) = ( ∘_f + “ ( ( 𝑥 supp ( 0_g ‘ 𝑅 ) ) × ( 𝑦 supp ( 0_g ‘ 𝑅 ) ) ) )
41		eqid	⊢ ( ._r ‘ 𝑅 ) = ( ._r ‘ 𝑅 )
42		simprl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → 𝑥 ∈ 𝑈 )
43		simprr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → 𝑦 ∈ 𝑈 )
44	1 2 3 38 39 14 15 40 41 42 43	mplsubrglem	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → ( 𝑥 ( ._r ‘ 𝑆 ) 𝑦 ) ∈ 𝑈 )
45	44	ralrimivva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑈 ∀ 𝑦 ∈ 𝑈 ( 𝑥 ( ._r ‘ 𝑆 ) 𝑦 ) ∈ 𝑈 )
46		eqid	⊢ ( ._r ‘ 𝑆 ) = ( ._r ‘ 𝑆 )
47	10 11 46	issubrg2	⊢ ( 𝑆 ∈ Ring → ( 𝑈 ∈ ( SubRing ‘ 𝑆 ) ↔ ( 𝑈 ∈ ( SubGrp ‘ 𝑆 ) ∧ ( 1_r ‘ 𝑆 ) ∈ 𝑈 ∧ ∀ 𝑥 ∈ 𝑈 ∀ 𝑦 ∈ 𝑈 ( 𝑥 ( ._r ‘ 𝑆 ) 𝑦 ) ∈ 𝑈 ) ) )
48	9 47	syl	⊢ ( 𝜑 → ( 𝑈 ∈ ( SubRing ‘ 𝑆 ) ↔ ( 𝑈 ∈ ( SubGrp ‘ 𝑆 ) ∧ ( 1_r ‘ 𝑆 ) ∈ 𝑈 ∧ ∀ 𝑥 ∈ 𝑈 ∀ 𝑦 ∈ 𝑈 ( 𝑥 ( ._r ‘ 𝑆 ) 𝑦 ) ∈ 𝑈 ) ) )
49	8 37 45 48	mpbir3and	⊢ ( 𝜑 → 𝑈 ∈ ( SubRing ‘ 𝑆 ) )

Metamath Proof Explorer

Theorem mplsubrg

Proof