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		reldmpsr	$⊢ Rel dom mPwSer$
14	13 1 2	elbasov	$⊢ X \in B \to (I \in V \land R \in V)$
15	5 14	syl	$⊢ φ \to (I \in V \land R \in V)$
16	15	simpld	$⊢ φ \to I \in V$
17	7	psrbaglefi	$⊢ (I \in V \land k \in D) \to \{y \in D \| y \leq_{f} k\} \in Fin$
18	16 17	sylan	$⊢ (φ \land k \in D) \to \{y \in D \| y \leq_{f} k\} \in Fin$
19	4	ad2antrr	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to R \in Ring$
20	1 8 7 2 5	psrelbas	$⊢ φ \to X : D ⟶ {Base}_{R}$
21	20	ad2antrr	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to X : D ⟶ {Base}_{R}$
22		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\}$
23		breq1	$⊢ y = x \to (y \leq_{f} k \leftrightarrow x \leq_{f} k)$
24	23	elrab	$⊢ x \in \{y \in D \| y \leq_{f} k\} \leftrightarrow (x \in D \land x \leq_{f} k)$
25	22 24	sylib	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to (x \in D \land x \leq_{f} k)$
26	25	simpld	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to x \in D$
27	21 26	ffvelrnd	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to X (x) \in {Base}_{R}$
28	1 8 7 2 6	psrelbas	$⊢ φ \to Y : D ⟶ {Base}_{R}$
29	28	ad2antrr	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to Y : D ⟶ {Base}_{R}$
30	16	ad2antrr	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to I \in V$
31		simplr	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to k \in D$
32	7	psrbagf	$⊢ (I \in V \land x \in D) \to x : I ⟶ ℕ_{0}$
33	30 26 32	syl2anc	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to x : I ⟶ ℕ_{0}$
34	25	simprd	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to x \leq_{f} k$
35	7	psrbagcon	$⊢ (I \in V \land (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)$
36	30 31 33 34 35	syl13anc	$⊢ ((φ \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)$
37	36	simpld	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to k -_{f} x \in D$
38	29 37	ffvelrnd	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to Y (k -_{f} x) \in {Base}_{R}$
39		eqid	$⊢ \cdot_{R} = \cdot_{R}$
40	8 39	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}$
41	19 27 38 40	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}$
42	41	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}$
43		fvexd	$⊢ (φ \land k \in D) \to 0_{R} \in V$
44	42 18 43	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)))$
45	8 9 12 18 42 44	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}$
46	45	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}$
47		fvex	$⊢ {Base}_{R} \in V$
48		ovex	$⊢ {ℕ_{0}}^{I} \in V$
49	7 48	rabex2	$⊢ D \in V$
50	47 49	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}$
51	46 50	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})$
52	1 2 39 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)))$
53	1 8 7 2 16	psrbas	$⊢ φ \to B = {Base}_{R}^{D}$
54	51 52 53	3eltr4d	$⊢ φ \to X \underset{˙}{\cdot} Y \in B$

Metamath Proof Explorer

Theorem psrmulcllem

Proof