This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem mplsubg

Description: The set of polynomials is closed under addition, i.e. it is a subgroup of the set of power series. (Contributed by Mario Carneiro, 8-Jan-2015) (Proof shortened by AV, 16-Jul-2019)

Ref Expression
Hypotheses mplsubg.s ⊢ S = I mPwSer R
mplsubg.p ⊢ P = I mPoly R
mplsubg.u ⊢ U = Base P
mplsubg.i ⊢ φ → I ∈ W
mplsubg.r ⊢ φ → R ∈ Grp
Assertion mplsubg ⊢ φ → U ∈ SubGrp ⁡ 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 ⊢ φ → I ∈ W
5 mplsubg.r ⊢ φ → R ∈ Grp
6 eqid ⊢ Base S = Base S
7 eqid ⊢ 0 R = 0 R
8 eqid ⊢ f ∈ ℕ 0 I | f -1 ℕ ∈ Fin = f ∈ ℕ 0 I | f -1 ℕ ∈ Fin
9 0fi ⊢ ∅ ∈ Fin
10 9 a1i ⊢ φ → ∅ ∈ Fin
11 unfi ⊢ x ∈ Fin ∧ y ∈ Fin → x ∪ y ∈ Fin
12 11 adantl ⊢ φ ∧ x ∈ Fin ∧ y ∈ Fin → x ∪ y ∈ Fin
13 ssfi ⊢ x ∈ Fin ∧ y ⊆ x → y ∈ Fin
14 13 adantl ⊢ φ ∧ x ∈ Fin ∧ y ⊆ x → y ∈ Fin
15 1 2 3 4 mplsubglem2 ⊢ φ → U = g ∈ Base S | g supp 0 R ∈ Fin
16 1 6 7 8 4 10 12 14 15 5 mplsubglem ⊢ φ → U ∈ SubGrp ⁡ S