Theorem psrring

Description: The ring of power series is a ring. (Contributed by Mario Carneiro, 29-Dec-2014)

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

Proof

Step	Hyp	Ref	Expression
1		psrring.s	⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 )
2		psrring.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
3		psrring.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
4		eqidd	⊢ ( 𝜑 → ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 ) )
5		eqidd	⊢ ( 𝜑 → ( +g ‘ 𝑆 ) = ( +g ‘ 𝑆 ) )
6		eqidd	⊢ ( 𝜑 → ( .r ‘ 𝑆 ) = ( .r ‘ 𝑆 ) )
7		ringgrp	⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Grp )
8	3 7	syl	⊢ ( 𝜑 → 𝑅 ∈ Grp )
9	1 2 8	psrgrp	⊢ ( 𝜑 → 𝑆 ∈ Grp )
10		eqid	⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
11		eqid	⊢ ( .r ‘ 𝑆 ) = ( .r ‘ 𝑆 )
12	3	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) → 𝑅 ∈ Ring )
13		simp2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) → 𝑥 ∈ ( Base ‘ 𝑆 ) )
14		simp3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) → 𝑦 ∈ ( Base ‘ 𝑆 ) )
15	1 10 11 12 13 14	psrmulcl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) → ( 𝑥 ( .r ‘ 𝑆 ) 𝑦 ) ∈ ( Base ‘ 𝑆 ) )
16	2	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ) → 𝐼 ∈ 𝑉 )
17	3	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ) → 𝑅 ∈ Ring )
18		eqid	⊢ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
19		simpr1	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ) → 𝑥 ∈ ( Base ‘ 𝑆 ) )
20		simpr2	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ) → 𝑦 ∈ ( Base ‘ 𝑆 ) )
21		simpr3	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ) → 𝑧 ∈ ( Base ‘ 𝑆 ) )
22	1 16 17 18 11 10 19 20 21	psrass1	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ) → ( ( 𝑥 ( .r ‘ 𝑆 ) 𝑦 ) ( .r ‘ 𝑆 ) 𝑧 ) = ( 𝑥 ( .r ‘ 𝑆 ) ( 𝑦 ( .r ‘ 𝑆 ) 𝑧 ) ) )
23		eqid	⊢ ( +g ‘ 𝑆 ) = ( +g ‘ 𝑆 )
24	1 16 17 18 11 10 19 20 21 23	psrdi	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ) → ( 𝑥 ( .r ‘ 𝑆 ) ( 𝑦 ( +g ‘ 𝑆 ) 𝑧 ) ) = ( ( 𝑥 ( .r ‘ 𝑆 ) 𝑦 ) ( +g ‘ 𝑆 ) ( 𝑥 ( .r ‘ 𝑆 ) 𝑧 ) ) )
25	1 16 17 18 11 10 19 20 21 23	psrdir	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ) → ( ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ( .r ‘ 𝑆 ) 𝑧 ) = ( ( 𝑥 ( .r ‘ 𝑆 ) 𝑧 ) ( +g ‘ 𝑆 ) ( 𝑦 ( .r ‘ 𝑆 ) 𝑧 ) ) )
26		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
27		eqid	⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
28		eqid	⊢ ( 𝑟 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ↦ if ( 𝑟 = ( 𝐼 × { 0 } ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) = ( 𝑟 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ↦ if ( 𝑟 = ( 𝐼 × { 0 } ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) )
29	1 2 3 18 26 27 28 10	psr1cl	⊢ ( 𝜑 → ( 𝑟 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ↦ if ( 𝑟 = ( 𝐼 × { 0 } ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) ∈ ( Base ‘ 𝑆 ) )
30	2	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ) → 𝐼 ∈ 𝑉 )
31	3	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ) → 𝑅 ∈ Ring )
32		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ) → 𝑥 ∈ ( Base ‘ 𝑆 ) )
33	1 30 31 18 26 27 28 10 11 32	psrlidm	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ) → ( ( 𝑟 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ↦ if ( 𝑟 = ( 𝐼 × { 0 } ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) ( .r ‘ 𝑆 ) 𝑥 ) = 𝑥 )
34	1 30 31 18 26 27 28 10 11 32	psrridm	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ) → ( 𝑥 ( .r ‘ 𝑆 ) ( 𝑟 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ↦ if ( 𝑟 = ( 𝐼 × { 0 } ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) ) = 𝑥 )
35	4 5 6 9 15 22 24 25 29 33 34	isringd	⊢ ( 𝜑 → 𝑆 ∈ Ring )