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	10	ringcmnd	$⊢ (φ \land k \in D) \to R \in CMnd$
12	7	psrbaglefi	$⊢ k \in D \to \{y \in D \| y \leq_{f} k\} \in Fin$
13	12	adantl	$⊢ (φ \land k \in D) \to \{y \in D \| y \leq_{f} k\} \in Fin$
14		eqid	$⊢ \cdot_{R} = \cdot_{R}$
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	ffvelcdmd	$⊢ ((φ \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	ffvelcdmd	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to Y (k -_{f} x) \in {Base}_{R}$
34	8 14 15 23 33	ringcld	$⊢ ((φ \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}$
35	34	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}$
36		fvexd	$⊢ (φ \land k \in D) \to 0_{R} \in V$
37	35 13 36	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)))$
38	8 9 11 13 35 37	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}$
39	38	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}$
40		fvex	$⊢ {Base}_{R} \in V$
41		ovex	$⊢ {ℕ_{0}}^{I} \in V$
42	7 41	rabex2	$⊢ D \in V$
43	40 42	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}$
44	39 43	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})$
45	1 2 14 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)))$
46		reldmpsr	$⊢ Rel dom mPwSer$
47	46 1 2	elbasov	$⊢ X \in B \to (I \in V \land R \in V)$
48	5 47	syl	$⊢ φ \to (I \in V \land R \in V)$
49	48	simpld	$⊢ φ \to I \in V$
50	1 8 7 2 49	psrbas	$⊢ φ \to B = {Base}_{R}^{D}$
51	44 45 50	3eltr4d	$⊢ φ \to X \underset{˙}{\cdot} Y \in B$

Metamath Proof Explorer

Theorem psrmulcllem

Proof