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

Metamath Proof Explorer

Theorem psrcrng

Description: The ring of power series is commutative ring. (Contributed by Mario Carneiro, 10-Jan-2015)

Ref Expression
Hypotheses psrcnrg.s ⊢ S = I mPwSer R
psrcnrg.i ⊢ φ → I ∈ V
psrcnrg.r ⊢ φ → R ∈ CRing
Assertion psrcrng ⊢ φ → S ∈ CRing

Proof

Step Hyp Ref Expression
1 psrcnrg.s ⊢ S = I mPwSer R
2 psrcnrg.i ⊢ φ → I ∈ V
3 psrcnrg.r ⊢ φ → R ∈ CRing
4 crngring ⊢ R ∈ CRing → R ∈ Ring
5 3 4 syl ⊢ φ → R ∈ Ring
6 1 2 5 psrring ⊢ φ → S ∈ Ring
7 eqid ⊢ mulGrp S = mulGrp S
8 eqid ⊢ Base S = Base S
9 7 8 mgpbas ⊢ Base S = Base mulGrp S
10 9 a1i ⊢ φ → Base S = Base mulGrp S
11 eqid ⊢ ⋅ S = ⋅ S
12 7 11 mgpplusg ⊢ ⋅ S = + mulGrp S
13 12 a1i ⊢ φ → ⋅ S = + mulGrp S
14 7 ringmgp ⊢ S ∈ Ring → mulGrp S ∈ Mnd
15 6 14 syl ⊢ φ → mulGrp S ∈ Mnd
16 2 3ad2ant1 ⊢ φ ∧ x ∈ Base S ∧ y ∈ Base S → I ∈ V
17 5 3ad2ant1 ⊢ φ ∧ x ∈ Base S ∧ y ∈ Base S → R ∈ Ring
18 eqid ⊢ f ∈ ℕ 0 I | f -1 ℕ ∈ Fin = f ∈ ℕ 0 I | f -1 ℕ ∈ Fin
19 simp2 ⊢ φ ∧ x ∈ Base S ∧ y ∈ Base S → x ∈ Base S
20 simp3 ⊢ φ ∧ x ∈ Base S ∧ y ∈ Base S → y ∈ Base S
21 3 3ad2ant1 ⊢ φ ∧ x ∈ Base S ∧ y ∈ Base S → R ∈ CRing
22 1 16 17 18 11 8 19 20 21 psrcom ⊢ φ ∧ x ∈ Base S ∧ y ∈ Base S → x ⋅ S y = y ⋅ S x
23 10 13 15 22 iscmnd ⊢ φ → mulGrp S ∈ CMnd
24 7 iscrng ⊢ S ∈ CRing ↔ S ∈ Ring ∧ mulGrp S ∈ CMnd
25 6 23 24 sylanbrc ⊢ φ → S ∈ CRing