Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  psrrng Structured version   Unicode version

Theorem psrrng 17830
 Description: The ring of power series is a ring. (Contributed by Mario Carneiro, 29-Dec-2014.)
Hypotheses
Ref Expression
psrrng.s mPwSer
psrrng.i
psrrng.r
Assertion
Ref Expression
psrrng

Proof of Theorem psrrng
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqidd 2461 . 2
2 eqidd 2461 . 2
3 eqidd 2461 . 2
4 psrrng.s . . 3 mPwSer
5 psrrng.i . . 3
6 psrrng.r . . . 4
7 rnggrp 16984 . . . 4
86, 7syl 16 . . 3
94, 5, 8psrgrp 17815 . 2
10 eqid 2460 . . 3
11 eqid 2460 . . 3
13 simp2 992 . . 3
14 simp3 993 . . 3
154, 10, 11, 12, 13, 14psrmulcl 17805 . 2
18 eqid 2460 . . 3
19 simpr1 997 . . 3
20 simpr2 998 . . 3
21 simpr3 999 . . 3
224, 16, 17, 18, 11, 10, 19, 20, 21psrass1 17824 . 2
23 eqid 2460 . . 3
244, 16, 17, 18, 11, 10, 19, 20, 21, 23psrdi 17825 . 2
254, 16, 17, 18, 11, 10, 19, 20, 21, 23psrdir 17826 . 2
26 eqid 2460 . . 3
27 eqid 2460 . . 3
28 eqid 2460 . . 3
294, 5, 6, 18, 26, 27, 28, 10psr1cl 17819 . 2