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