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

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

Proof of Theorem psrgrp
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqidd 2403 . 2
2 eqidd 2403 . 2
3 psrgrp.s . . 3 mPwSer
4 eqid 2402 . . 3
5 eqid 2402 . . 3
6 psrgrp.r . . . 4
8 simp2 998 . . 3
9 simp3 999 . . 3
103, 4, 5, 7, 8, 9psraddcl 18354 . 2
11 ovex 6305 . . . . . . 7
1211rabex 4544 . . . . . 6
1312a1i 11 . . . . 5
14 eqid 2402 . . . . . 6
15 eqid 2402 . . . . . 6
16 simpr1 1003 . . . . . 6
173, 14, 15, 4, 16psrelbas 18350 . . . . 5
18 simpr2 1004 . . . . . 6
193, 14, 15, 4, 18psrelbas 18350 . . . . 5
20 simpr3 1005 . . . . . 6
213, 14, 15, 4, 20psrelbas 18350 . . . . 5
226adantr 463 . . . . . 6
23 eqid 2402 . . . . . . 7
2414, 23grpass 16386 . . . . . 6
2522, 24sylan 469 . . . . 5
2613, 17, 19, 21, 25caofass 6555 . . . 4
273, 4, 23, 5, 16, 18psradd 18353 . . . . 5
2827oveq1d 6292 . . . 4
293, 4, 23, 5, 18, 20psradd 18353 . . . . 5
3029oveq2d 6293 . . . 4
3126, 28, 303eqtr4d 2453 . . 3
32103adant3r3 1208 . . . 4
333, 4, 23, 5, 32, 20psradd 18353 . . 3
343, 4, 5, 22, 18, 20psraddcl 18354 . . . 4
353, 4, 23, 5, 16, 34psradd 18353 . . 3
3631, 33, 353eqtr4d 2453 . 2
37 psrgrp.i . . 3
38 eqid 2402 . . 3
393, 37, 6, 15, 38, 4psr0cl 18365 . 2