Theorem psrcrng

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

	Ref	Expression
Hypotheses	psrcnrg.s	⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 )
	psrcnrg.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
	psrcnrg.r	⊢ ( 𝜑 → 𝑅 ∈ CRing )
Assertion	psrcrng	⊢ ( 𝜑 → 𝑆 ∈ CRing )

Proof

Step	Hyp	Ref	Expression
1		psrcnrg.s	⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 )
2		psrcnrg.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
3		psrcnrg.r	⊢ ( 𝜑 → 𝑅 ∈ CRing )
4		crngring	⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
5	3 4	syl	⊢ ( 𝜑 → 𝑅 ∈ Ring )
6	1 2 5	psrring	⊢ ( 𝜑 → 𝑆 ∈ Ring )
7		eqid	⊢ ( mulGrp ‘ 𝑆 ) = ( mulGrp ‘ 𝑆 )
8		eqid	⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
9	7 8	mgpbas	⊢ ( Base ‘ 𝑆 ) = ( Base ‘ ( mulGrp ‘ 𝑆 ) )
10	9	a1i	⊢ ( 𝜑 → ( Base ‘ 𝑆 ) = ( Base ‘ ( mulGrp ‘ 𝑆 ) ) )
11		eqid	⊢ ( .r ‘ 𝑆 ) = ( .r ‘ 𝑆 )
12	7 11	mgpplusg	⊢ ( .r ‘ 𝑆 ) = ( +g ‘ ( mulGrp ‘ 𝑆 ) )
13	12	a1i	⊢ ( 𝜑 → ( .r ‘ 𝑆 ) = ( +g ‘ ( mulGrp ‘ 𝑆 ) ) )
14	7	ringmgp	⊢ ( 𝑆 ∈ Ring → ( mulGrp ‘ 𝑆 ) ∈ Mnd )
15	6 14	syl	⊢ ( 𝜑 → ( mulGrp ‘ 𝑆 ) ∈ Mnd )
16	2	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) → 𝐼 ∈ 𝑉 )
17	5	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) → 𝑅 ∈ Ring )
18		eqid	⊢ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
19		simp2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) → 𝑥 ∈ ( Base ‘ 𝑆 ) )
20		simp3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) → 𝑦 ∈ ( Base ‘ 𝑆 ) )
21	3	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) → 𝑅 ∈ CRing )
22	1 16 17 18 11 8 19 20 21	psrcom	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) → ( 𝑥 ( .r ‘ 𝑆 ) 𝑦 ) = ( 𝑦 ( .r ‘ 𝑆 ) 𝑥 ) )
23	10 13 15 22	iscmnd	⊢ ( 𝜑 → ( mulGrp ‘ 𝑆 ) ∈ CMnd )
24	7	iscrng	⊢ ( 𝑆 ∈ CRing ↔ ( 𝑆 ∈ Ring ∧ ( mulGrp ‘ 𝑆 ) ∈ CMnd ) )
25	6 23 24	sylanbrc	⊢ ( 𝜑 → 𝑆 ∈ CRing )