psrring

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

	Ref	Expression
Hypotheses	psrring.s	$⊢ S = I mPwSer R$
	psrring.i	$⊢ φ \to I \in V$
	psrring.r	$⊢ φ \to R \in Ring$
Assertion	psrring	$⊢ φ \to S \in Ring$

Proof

Step	Hyp	Ref	Expression
1		psrring.s	$⊢ S = I mPwSer R$
2		psrring.i	$⊢ φ \to I \in V$
3		psrring.r	$⊢ φ \to R \in Ring$
4		eqidd	$⊢ φ \to {Base}_{S} = {Base}_{S}$
5		eqidd	$⊢ φ \to +_{S} = +_{S}$
6		eqidd	$⊢ φ \to \cdot_{S} = \cdot_{S}$
7		ringgrp	$⊢ R \in Ring \to R \in Grp$
8	3 7	syl	$⊢ φ \to R \in Grp$
9	1 2 8	psrgrp	$⊢ φ \to S \in Grp$
10		eqid	$⊢ {Base}_{S} = {Base}_{S}$
11		eqid	$⊢ \cdot_{S} = \cdot_{S}$
12	3	3ad2ant1	$⊢ (φ \land x \in {Base}_{S} \land y \in {Base}_{S}) \to R \in Ring$
13		simp2	$⊢ (φ \land x \in {Base}_{S} \land y \in {Base}_{S}) \to x \in {Base}_{S}$
14		simp3	$⊢ (φ \land x \in {Base}_{S} \land y \in {Base}_{S}) \to y \in {Base}_{S}$
15	1 10 11 12 13 14	psrmulcl	$⊢ (φ \land x \in {Base}_{S} \land y \in {Base}_{S}) \to x \cdot_{S} y \in {Base}_{S}$
16	2	adantr	$⊢ (φ \land (x \in {Base}_{S} \land y \in {Base}_{S} \land z \in {Base}_{S})) \to I \in V$
17	3	adantr	$⊢ (φ \land (x \in {Base}_{S} \land y \in {Base}_{S} \land z \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		simpr1	$⊢ (φ \land (x \in {Base}_{S} \land y \in {Base}_{S} \land z \in {Base}_{S})) \to x \in {Base}_{S}$
20		simpr2	$⊢ (φ \land (x \in {Base}_{S} \land y \in {Base}_{S} \land z \in {Base}_{S})) \to y \in {Base}_{S}$
21		simpr3	$⊢ (φ \land (x \in {Base}_{S} \land y \in {Base}_{S} \land z \in {Base}_{S})) \to z \in {Base}_{S}$
22	1 16 17 18 11 10 19 20 21	psrass1	$⊢ (φ \land (x \in {Base}_{S} \land y \in {Base}_{S} \land z \in {Base}_{S})) \to (x \cdot_{S} y) \cdot_{S} z = x \cdot_{S} (y \cdot_{S} z)$
23		eqid	$⊢ +_{S} = +_{S}$
24	1 16 17 18 11 10 19 20 21 23	psrdi	$⊢ (φ \land (x \in {Base}_{S} \land y \in {Base}_{S} \land z \in {Base}_{S})) \to x \cdot_{S} (y +_{S} z) = (x \cdot_{S} y) +_{S} (x \cdot_{S} z)$
25	1 16 17 18 11 10 19 20 21 23	psrdir	$⊢ (φ \land (x \in {Base}_{S} \land y \in {Base}_{S} \land z \in {Base}_{S})) \to (x +_{S} y) \cdot_{S} z = (x \cdot_{S} z) +_{S} (y \cdot_{S} z)$
26		eqid	$⊢ 0_{R} = 0_{R}$
27		eqid	$⊢ 1_{R} = 1_{R}$
28		eqid	$⊢ (r \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} ⟼ if (r = I \times \{0\}, 1_{R}, 0_{R})) = (r \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} ⟼ if (r = I \times \{0\}, 1_{R}, 0_{R}))$
29	1 2 3 18 26 27 28 10	psr1cl	$⊢ φ \to (r \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} ⟼ if (r = I \times \{0\}, 1_{R}, 0_{R})) \in {Base}_{S}$
30	2	adantr	$⊢ (φ \land x \in {Base}_{S}) \to I \in V$
31	3	adantr	$⊢ (φ \land x \in {Base}_{S}) \to R \in Ring$
32		simpr	$⊢ (φ \land x \in {Base}_{S}) \to x \in {Base}_{S}$
33	1 30 31 18 26 27 28 10 11 32	psrlidm	$⊢ (φ \land x \in {Base}_{S}) \to (r \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} ⟼ if (r = I \times \{0\}, 1_{R}, 0_{R})) \cdot_{S} x = x$
34	1 30 31 18 26 27 28 10 11 32	psrridm	$⊢ (φ \land x \in {Base}_{S}) \to x \cdot_{S} (r \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} ⟼ if (r = I \times \{0\}, 1_{R}, 0_{R})) = x$
35	4 5 6 9 15 22 24 25 29 33 34	isringd	$⊢ φ \to S \in Ring$

Metamath Proof Explorer

Theorem psrring

Proof