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	$⊢ S = I mPwSer R$
	mplsubg.p	$⊢ P = I mPoly R$
	mplsubg.u	$⊢ U = {Base}_{P}$
	mplsubg.i	$⊢ φ \to I \in W$
	mpllss.r	$⊢ φ \to R \in Ring$
Assertion	mplsubrg	$⊢ φ \to U \in SubRing (S)$

Proof

Step	Hyp	Ref	Expression
1		mplsubg.s	$⊢ S = I mPwSer R$
2		mplsubg.p	$⊢ P = I mPoly R$
3		mplsubg.u	$⊢ U = {Base}_{P}$
4		mplsubg.i	$⊢ φ \to I \in W$
5		mpllss.r	$⊢ φ \to R \in Ring$
6		ringgrp	$⊢ R \in Ring \to R \in Grp$
7	5 6	syl	$⊢ φ \to R \in Grp$
8	1 2 3 4 7	mplsubg	$⊢ φ \to U \in SubGrp (S)$
9	1 4 5	psrring	$⊢ φ \to S \in Ring$
10		eqid	$⊢ {Base}_{S} = {Base}_{S}$
11		eqid	$⊢ 1_{S} = 1_{S}$
12	10 11	ringidcl	$⊢ S \in Ring \to 1_{S} \in {Base}_{S}$
13	9 12	syl	$⊢ φ \to 1_{S} \in {Base}_{S}$
14		eqid	$⊢ \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} = \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}$
15		eqid	$⊢ 0_{R} = 0_{R}$
16		eqid	$⊢ 1_{R} = 1_{R}$
17	1 4 5 14 15 16 11	psr1	$⊢ φ \to 1_{S} = (k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} ⟼ if (k = I \times \{0\}, 1_{R}, 0_{R}))$
18		ovex	$⊢ {ℕ_{0}}^{I} \in V$
19	18	mptrabex	$⊢ (k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} ⟼ if (k = I \times \{0\}, 1_{R}, 0_{R})) \in V$
20		funmpt	$⊢ Fun (k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} ⟼ if (k = I \times \{0\}, 1_{R}, 0_{R}))$
21		fvex	$⊢ 0_{R} \in V$
22	19 20 21	3pm3.2i	$⊢ ((k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} ⟼ if (k = I \times \{0\}, 1_{R}, 0_{R})) \in V \land Fun (k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} ⟼ if (k = I \times \{0\}, 1_{R}, 0_{R})) \land 0_{R} \in V)$
23	22	a1i	$⊢ φ \to ((k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} ⟼ if (k = I \times \{0\}, 1_{R}, 0_{R})) \in V \land Fun (k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} ⟼ if (k = I \times \{0\}, 1_{R}, 0_{R})) \land 0_{R} \in V)$
24		snfi	$⊢ \{I \times \{0\}\} \in Fin$
25	24	a1i	$⊢ φ \to \{I \times \{0\}\} \in Fin$
26		eldifsni	$⊢ k \in (\{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} ∖ \{I \times \{0\}\}) \to k \neq I \times \{0\}$
27	26	adantl	$⊢ (φ \land k \in (\{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} ∖ \{I \times \{0\}\})) \to k \neq I \times \{0\}$
28		ifnefalse	$⊢ k \neq I \times \{0\} \to if (k = I \times \{0\}, 1_{R}, 0_{R}) = 0_{R}$
29	27 28	syl	$⊢ (φ \land k \in (\{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} ∖ \{I \times \{0\}\})) \to if (k = I \times \{0\}, 1_{R}, 0_{R}) = 0_{R}$
30	18	rabex	$⊢ \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \in V$
31	30	a1i	$⊢ φ \to \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \in V$
32	29 31	suppss2	$⊢ φ \to (k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} ⟼ if (k = I \times \{0\}, 1_{R}, 0_{R})) supp 0_{R} \subseteq \{I \times \{0\}\}$
33		suppssfifsupp	$⊢ (((k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} ⟼ if (k = I \times \{0\}, 1_{R}, 0_{R})) \in V \land Fun (k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} ⟼ if (k = I \times \{0\}, 1_{R}, 0_{R})) \land 0_{R} \in V) \land (\{I \times \{0\}\} \in Fin \land (k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} ⟼ if (k = I \times \{0\}, 1_{R}, 0_{R})) supp 0_{R} \subseteq \{I \times \{0\}\})) \to {finSupp}_{0_{R}} ((k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} ⟼ if (k = I \times \{0\}, 1_{R}, 0_{R})))$
34	23 25 32 33	syl12anc	$⊢ φ \to {finSupp}_{0_{R}} ((k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} ⟼ if (k = I \times \{0\}, 1_{R}, 0_{R})))$
35	17 34	eqbrtrd	$⊢ φ \to {finSupp}_{0_{R}} (1_{S})$
36	2 1 10 15 3	mplelbas	$⊢ 1_{S} \in U \leftrightarrow (1_{S} \in {Base}_{S} \land {finSupp}_{0_{R}} (1_{S}))$
37	13 35 36	sylanbrc	$⊢ φ \to 1_{S} \in U$
38	4	adantr	$⊢ (φ \land (x \in U \land y \in U)) \to I \in W$
39	5	adantr	$⊢ (φ \land (x \in U \land y \in U)) \to R \in Ring$
40		eqid	$⊢ \circ_{f} + [{supp}_{0_{R}} (x) \times {supp}_{0_{R}} (y)] = \circ_{f} + [{supp}_{0_{R}} (x) \times {supp}_{0_{R}} (y)]$
41		eqid	$⊢ \cdot_{R} = \cdot_{R}$
42		simprl	$⊢ (φ \land (x \in U \land y \in U)) \to x \in U$
43		simprr	$⊢ (φ \land (x \in U \land y \in U)) \to y \in U$
44	1 2 3 38 39 14 15 40 41 42 43	mplsubrglem	$⊢ (φ \land (x \in U \land y \in U)) \to x \cdot_{S} y \in U$
45	44	ralrimivva	$⊢ φ \to \forall x \in U \forall y \in U x \cdot_{S} y \in U$
46		eqid	$⊢ \cdot_{S} = \cdot_{S}$
47	10 11 46	issubrg2	$⊢ S \in Ring \to (U \in SubRing (S) \leftrightarrow (U \in SubGrp (S) \land 1_{S} \in U \land \forall x \in U \forall y \in U x \cdot_{S} y \in U))$
48	9 47	syl	$⊢ φ \to (U \in SubRing (S) \leftrightarrow (U \in SubGrp (S) \land 1_{S} \in U \land \forall x \in U \forall y \in U x \cdot_{S} y \in U))$
49	8 37 45 48	mpbir3and	$⊢ φ \to U \in SubRing (S)$

Metamath Proof Explorer

Theorem mplsubrg

Proof