psrcrng

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

Step	Hyp	Ref	Expression
1		psrcnrg.s	$⊢ S = I mPwSer R$
2		psrcnrg.i	$⊢ φ \to I \in V$
3		psrcnrg.r	$⊢ φ \to R \in CRing$
4		crngring	$⊢ R \in CRing \to R \in Ring$
5	3 4	syl	$⊢ φ \to R \in Ring$
6	1 2 5	psrring	$⊢ φ \to S \in 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	$⊢ φ \to {Base}_{S} = {Base}_{{mulGrp}_{S}}$
11		eqid	$⊢ \cdot_{S} = \cdot_{S}$
12	7 11	mgpplusg	$⊢ \cdot_{S} = +_{{mulGrp}_{S}}$
13	12	a1i	$⊢ φ \to \cdot_{S} = +_{{mulGrp}_{S}}$
14	7	ringmgp	$⊢ S \in Ring \to {mulGrp}_{S} \in Mnd$
15	6 14	syl	$⊢ φ \to {mulGrp}_{S} \in Mnd$
16	2	3ad2ant1	$⊢ (φ \land x \in {Base}_{S} \land y \in {Base}_{S}) \to I \in V$
17	5	3ad2ant1	$⊢ (φ \land x \in {Base}_{S} \land y \in {Base}_{S}) \to R \in Ring$
18		eqid	$⊢ \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} = \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}$
19		simp2	$⊢ (φ \land x \in {Base}_{S} \land y \in {Base}_{S}) \to x \in {Base}_{S}$
20		simp3	$⊢ (φ \land x \in {Base}_{S} \land y \in {Base}_{S}) \to y \in {Base}_{S}$
21	3	3ad2ant1	$⊢ (φ \land x \in {Base}_{S} \land y \in {Base}_{S}) \to R \in CRing$
22	1 16 17 18 11 8 19 20 21	psrcom	$⊢ (φ \land x \in {Base}_{S} \land y \in {Base}_{S}) \to x \cdot_{S} y = y \cdot_{S} x$
23	10 13 15 22	iscmnd	$⊢ φ \to {mulGrp}_{S} \in CMnd$
24	7	iscrng	$⊢ S \in CRing \leftrightarrow (S \in Ring \land {mulGrp}_{S} \in CMnd)$
25	6 23 24	sylanbrc	$⊢ φ \to S \in CRing$

Metamath Proof Explorer