psrmulcllem

Description: Closure of the power series multiplication operation. (Contributed by Mario Carneiro, 29-Dec-2014)

	Ref	Expression
Hypotheses	psrmulcl.s	$⊢ S = I mPwSer R$
	psrmulcl.b	$⊢ B = {Base}_{S}$
	psrmulcl.t	$⊢ \underset{˙}{\cdot} = \cdot_{S}$
	psrmulcl.r	$⊢ φ \to R \in Ring$
	psrmulcl.x	$⊢ φ \to X \in B$
	psrmulcl.y	$⊢ φ \to Y \in B$
	psrmulcl.d	$⊢ D = \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}$
Assertion	psrmulcllem	$⊢ φ \to X \underset{˙}{\cdot} Y \in B$

Proof

Step	Hyp	Ref	Expression
1		psrmulcl.s	$⊢ S = I mPwSer R$
2		psrmulcl.b	$⊢ B = {Base}_{S}$
3		psrmulcl.t	$⊢ \underset{˙}{\cdot} = \cdot_{S}$
4		psrmulcl.r	$⊢ φ \to R \in Ring$
5		psrmulcl.x	$⊢ φ \to X \in B$
6		psrmulcl.y	$⊢ φ \to Y \in B$
7		psrmulcl.d	$⊢ D = \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}$
8		eqid	$⊢ {Base}_{R} = {Base}_{R}$
9		eqid	$⊢ 0_{R} = 0_{R}$
10	4	adantr	$⊢ (φ \land k \in D) \to R \in Ring$
11		ringcmn	$⊢ R \in Ring \to R \in CMnd$
12	10 11	syl	$⊢ (φ \land k \in D) \to R \in CMnd$
13	7	psrbaglefi	$⊢ k \in D \to \{y \in D \| y \leq_{f} k\} \in Fin$
14	13	adantl	$⊢ (φ \land k \in D) \to \{y \in D \| y \leq_{f} k\} \in Fin$
15	4	ad2antrr	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to R \in Ring$
16	1 8 7 2 5	psrelbas	$⊢ φ \to X : D ⟶ {Base}_{R}$
17	16	ad2antrr	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to X : D ⟶ {Base}_{R}$
18		simpr	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to x \in \{y \in D \| y \leq_{f} k\}$
19		breq1	$⊢ y = x \to (y \leq_{f} k \leftrightarrow x \leq_{f} k)$
20	19	elrab	$⊢ x \in \{y \in D \| y \leq_{f} k\} \leftrightarrow (x \in D \land x \leq_{f} k)$
21	18 20	sylib	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to (x \in D \land x \leq_{f} k)$
22	21	simpld	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to x \in D$
23	17 22	ffvelrnd	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to X (x) \in {Base}_{R}$
24	1 8 7 2 6	psrelbas	$⊢ φ \to Y : D ⟶ {Base}_{R}$
25	24	ad2antrr	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to Y : D ⟶ {Base}_{R}$
26		simplr	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to k \in D$
27	7	psrbagf	$⊢ x \in D \to x : I ⟶ ℕ_{0}$
28	22 27	syl	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to x : I ⟶ ℕ_{0}$
29	21	simprd	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to x \leq_{f} k$
30	7	psrbagcon	$⊢ (k \in D \land x : I ⟶ ℕ_{0} \land x \leq_{f} k) \to (k -_{f} x \in D \land (k -_{f} x) \leq_{f} k)$
31	26 28 29 30	syl3anc	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to (k -_{f} x \in D \land (k -_{f} x) \leq_{f} k)$
32	31	simpld	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to k -_{f} x \in D$
33	25 32	ffvelrnd	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to Y (k -_{f} x) \in {Base}_{R}$
34		eqid	$⊢ \cdot_{R} = \cdot_{R}$
35	8 34	ringcl	$⊢ (R \in Ring \land X (x) \in {Base}_{R} \land Y (k -_{f} x) \in {Base}_{R}) \to X (x) \cdot_{R} Y (k -_{f} x) \in {Base}_{R}$
36	15 23 33 35	syl3anc	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to X (x) \cdot_{R} Y (k -_{f} x) \in {Base}_{R}$
37	36	fmpttd	$⊢ (φ \land k \in D) \to (x \in \{y \in D \| y \leq_{f} k\} ⟼ X (x) \cdot_{R} Y (k -_{f} x)) : \{y \in D \| y \leq_{f} k\} ⟶ {Base}_{R}$
38		fvexd	$⊢ (φ \land k \in D) \to 0_{R} \in V$
39	37 14 38	fdmfifsupp	$⊢ (φ \land k \in D) \to {finSupp}_{0_{R}} ((x \in \{y \in D \| y \leq_{f} k\} ⟼ X (x) \cdot_{R} Y (k -_{f} x)))$
40	8 9 12 14 37 39	gsumcl	$⊢ (φ \land k \in D) \to \underset{x \in \{y \in D \| y \leq_{f} k\}}{\sum_{R}} (X (x) \cdot_{R} Y (k -_{f} x)) \in {Base}_{R}$
41	40	fmpttd	$⊢ φ \to (k \in D ⟼ \underset{x \in \{y \in D \| y \leq_{f} k\}}{\sum_{R}} (X (x) \cdot_{R} Y (k -_{f} x))) : D ⟶ {Base}_{R}$
42		fvex	$⊢ {Base}_{R} \in V$
43		ovex	$⊢ {ℕ_{0}}^{I} \in V$
44	7 43	rabex2	$⊢ D \in V$
45	42 44	elmap	$⊢ (k \in D ⟼ \underset{x \in \{y \in D \| y \leq_{f} k\}}{\sum_{R}} (X (x) \cdot_{R} Y (k -_{f} x))) \in ({Base}_{R}^{D}) \leftrightarrow (k \in D ⟼ \underset{x \in \{y \in D \| y \leq_{f} k\}}{\sum_{R}} (X (x) \cdot_{R} Y (k -_{f} x))) : D ⟶ {Base}_{R}$
46	41 45	sylibr	$⊢ φ \to (k \in D ⟼ \underset{x \in \{y \in D \| y \leq_{f} k\}}{\sum_{R}} (X (x) \cdot_{R} Y (k -_{f} x))) \in ({Base}_{R}^{D})$
47	1 2 34 3 7 5 6	psrmulfval	$⊢ φ \to X \underset{˙}{\cdot} Y = (k \in D ⟼ \underset{x \in \{y \in D \| y \leq_{f} k\}}{\sum_{R}} (X (x) \cdot_{R} Y (k -_{f} x)))$
48		reldmpsr	$⊢ Rel dom mPwSer$
49	48 1 2	elbasov	$⊢ X \in B \to (I \in V \land R \in V)$
50	5 49	syl	$⊢ φ \to (I \in V \land R \in V)$
51	50	simpld	$⊢ φ \to I \in V$
52	1 8 7 2 51	psrbas	$⊢ φ \to B = {Base}_{R}^{D}$
53	46 47 52	3eltr4d	$⊢ φ \to X \underset{˙}{\cdot} Y \in B$

Metamath Proof Explorer

Theorem psrmulcllem

Proof