psrmulr

Description: The multiplication operation of the multivariate power series structure. (Contributed by Mario Carneiro, 28-Dec-2014) (Revised by Mario Carneiro, 2-Oct-2015) (Proof shortened by AV, 2-Mar-2024)

	Ref	Expression
Hypotheses	psrmulr.s	$⊢ S = I mPwSer R$
	psrmulr.b	$⊢ B = {Base}_{S}$
	psrmulr.m	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	psrmulr.t	$⊢ \underset{˙}{∙} = \cdot_{S}$
	psrmulr.d	$⊢ D = \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\}$
Assertion	psrmulr	$⊢ \underset{˙}{∙} = (f \in B, g \in B ⟼ (k \in D ⟼ \underset{x \in \{y \in D \| y \leq_{f} k\}}{\sum_{R}} (f (x) \underset{˙}{\cdot} g (k -_{f} x))))$

Proof

Step	Hyp	Ref	Expression
1		psrmulr.s	$⊢ S = I mPwSer R$
2		psrmulr.b	$⊢ B = {Base}_{S}$
3		psrmulr.m	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
4		psrmulr.t	$⊢ \underset{˙}{∙} = \cdot_{S}$
5		psrmulr.d	$⊢ D = \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\}$
6		eqid	$⊢ {Base}_{R} = {Base}_{R}$
7		eqid	$⊢ +_{R} = +_{R}$
8		eqid	$⊢ TopOpen (R) = TopOpen (R)$
9		simpl	$⊢ (I \in V \land R \in V) \to I \in V$
10	1 6 5 2 9	psrbas	$⊢ (I \in V \land R \in V) \to B = {Base}_{R}^{D}$
11		eqid	$⊢ +_{S} = +_{S}$
12	1 2 7 11	psrplusg	$⊢ +_{S} = {\circ_{f} +_{R} ↾}_{(B \times B)}$
13		eqid	$⊢ (f \in B, g \in B ⟼ (k \in D ⟼ \underset{x \in \{y \in D \| y \leq_{f} k\}}{\sum_{R}} (f (x) \underset{˙}{\cdot} g (k -_{f} x)))) = (f \in B, g \in B ⟼ (k \in D ⟼ \underset{x \in \{y \in D \| y \leq_{f} k\}}{\sum_{R}} (f (x) \underset{˙}{\cdot} g (k -_{f} x))))$
14		eqid	$⊢ (x \in {Base}_{R}, f \in B ⟼ (D \times \{x\}) {\underset{˙}{\cdot}}_{f} f) = (x \in {Base}_{R}, f \in B ⟼ (D \times \{x\}) {\underset{˙}{\cdot}}_{f} f)$
15		eqidd	$⊢ (I \in V \land R \in V) \to \prod_{𝑡} (D \times \{TopOpen (R)\}) = \prod_{𝑡} (D \times \{TopOpen (R)\})$
16		simpr	$⊢ (I \in V \land R \in V) \to R \in V$
17	1 6 7 3 8 5 10 12 13 14 15 9 16	psrval	$⊢ (I \in V \land R \in V) \to S = \{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, +_{S}⟩, ⟨\cdot_{ndx}, (f \in B, g \in B ⟼ (k \in D ⟼ \underset{x \in \{y \in D \| y \leq_{f} k\}}{\sum_{R}} (f (x) \underset{˙}{\cdot} g (k -_{f} x))))⟩\} \cup \{⟨Scalar (ndx), R⟩, ⟨\cdot_{ndx}, (x \in {Base}_{R}, f \in B ⟼ (D \times \{x\}) {\underset{˙}{\cdot}}_{f} f)⟩, ⟨TopSet (ndx), \prod_{𝑡} (D \times \{TopOpen (R)\})⟩\}$
18	17	fveq2d	$⊢ (I \in V \land R \in V) \to \cdot_{S} = \cdot_{(\{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, +_{S}⟩, ⟨\cdot_{ndx}, (f \in B, g \in B ⟼ (k \in D ⟼ \underset{x \in \{y \in D \| y \leq_{f} k\}}{\sum_{R}} (f (x) \underset{˙}{\cdot} g (k -_{f} x))))⟩\} \cup \{⟨Scalar (ndx), R⟩, ⟨\cdot_{ndx}, (x \in {Base}_{R}, f \in B ⟼ (D \times \{x\}) {\underset{˙}{\cdot}}_{f} f)⟩, ⟨TopSet (ndx), \prod_{𝑡} (D \times \{TopOpen (R)\})⟩\})}$
19	2	fvexi	$⊢ B \in V$
20	19 19	mpoex	$⊢ (f \in B, g \in B ⟼ (k \in D ⟼ \underset{x \in \{y \in D \| y \leq_{f} k\}}{\sum_{R}} (f (x) \underset{˙}{\cdot} g (k -_{f} x)))) \in V$
21		psrvalstr	$⊢ (\{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, +_{S}⟩, ⟨\cdot_{ndx}, (f \in B, g \in B ⟼ (k \in D ⟼ \underset{x \in \{y \in D \| y \leq_{f} k\}}{\sum_{R}} (f (x) \underset{˙}{\cdot} g (k -_{f} x))))⟩\} \cup \{⟨Scalar (ndx), R⟩, ⟨\cdot_{ndx}, (x \in {Base}_{R}, f \in B ⟼ (D \times \{x\}) {\underset{˙}{\cdot}}_{f} f)⟩, ⟨TopSet (ndx), \prod_{𝑡} (D \times \{TopOpen (R)\})⟩\}) Struct ⟨1, 9⟩$
22		mulrid	$⊢ \cdot_{𝑟} = Slot \cdot_{ndx}$
23		snsstp3	$⊢ \{⟨\cdot_{ndx}, (f \in B, g \in B ⟼ (k \in D ⟼ \underset{x \in \{y \in D \| y \leq_{f} k\}}{\sum_{R}} (f (x) \underset{˙}{\cdot} g (k -_{f} x))))⟩\} \subseteq \{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, +_{S}⟩, ⟨\cdot_{ndx}, (f \in B, g \in B ⟼ (k \in D ⟼ \underset{x \in \{y \in D \| y \leq_{f} k\}}{\sum_{R}} (f (x) \underset{˙}{\cdot} g (k -_{f} x))))⟩\}$
24		ssun1	$⊢ \{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, +_{S}⟩, ⟨\cdot_{ndx}, (f \in B, g \in B ⟼ (k \in D ⟼ \underset{x \in \{y \in D \| y \leq_{f} k\}}{\sum_{R}} (f (x) \underset{˙}{\cdot} g (k -_{f} x))))⟩\} \subseteq \{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, +_{S}⟩, ⟨\cdot_{ndx}, (f \in B, g \in B ⟼ (k \in D ⟼ \underset{x \in \{y \in D \| y \leq_{f} k\}}{\sum_{R}} (f (x) \underset{˙}{\cdot} g (k -_{f} x))))⟩\} \cup \{⟨Scalar (ndx), R⟩, ⟨\cdot_{ndx}, (x \in {Base}_{R}, f \in B ⟼ (D \times \{x\}) {\underset{˙}{\cdot}}_{f} f)⟩, ⟨TopSet (ndx), \prod_{𝑡} (D \times \{TopOpen (R)\})⟩\}$
25	23 24	sstri	$⊢ \{⟨\cdot_{ndx}, (f \in B, g \in B ⟼ (k \in D ⟼ \underset{x \in \{y \in D \| y \leq_{f} k\}}{\sum_{R}} (f (x) \underset{˙}{\cdot} g (k -_{f} x))))⟩\} \subseteq \{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, +_{S}⟩, ⟨\cdot_{ndx}, (f \in B, g \in B ⟼ (k \in D ⟼ \underset{x \in \{y \in D \| y \leq_{f} k\}}{\sum_{R}} (f (x) \underset{˙}{\cdot} g (k -_{f} x))))⟩\} \cup \{⟨Scalar (ndx), R⟩, ⟨\cdot_{ndx}, (x \in {Base}_{R}, f \in B ⟼ (D \times \{x\}) {\underset{˙}{\cdot}}_{f} f)⟩, ⟨TopSet (ndx), \prod_{𝑡} (D \times \{TopOpen (R)\})⟩\}$
26	21 22 25	strfv	$⊢ (f \in B, g \in B ⟼ (k \in D ⟼ \underset{x \in \{y \in D \| y \leq_{f} k\}}{\sum_{R}} (f (x) \underset{˙}{\cdot} g (k -_{f} x)))) \in V \to (f \in B, g \in B ⟼ (k \in D ⟼ \underset{x \in \{y \in D \| y \leq_{f} k\}}{\sum_{R}} (f (x) \underset{˙}{\cdot} g (k -_{f} x)))) = \cdot_{(\{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, +_{S}⟩, ⟨\cdot_{ndx}, (f \in B, g \in B ⟼ (k \in D ⟼ \underset{x \in \{y \in D \| y \leq_{f} k\}}{\sum_{R}} (f (x) \underset{˙}{\cdot} g (k -_{f} x))))⟩\} \cup \{⟨Scalar (ndx), R⟩, ⟨\cdot_{ndx}, (x \in {Base}_{R}, f \in B ⟼ (D \times \{x\}) {\underset{˙}{\cdot}}_{f} f)⟩, ⟨TopSet (ndx), \prod_{𝑡} (D \times \{TopOpen (R)\})⟩\})}$
27	20 26	ax-mp	$⊢ (f \in B, g \in B ⟼ (k \in D ⟼ \underset{x \in \{y \in D \| y \leq_{f} k\}}{\sum_{R}} (f (x) \underset{˙}{\cdot} g (k -_{f} x)))) = \cdot_{(\{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, +_{S}⟩, ⟨\cdot_{ndx}, (f \in B, g \in B ⟼ (k \in D ⟼ \underset{x \in \{y \in D \| y \leq_{f} k\}}{\sum_{R}} (f (x) \underset{˙}{\cdot} g (k -_{f} x))))⟩\} \cup \{⟨Scalar (ndx), R⟩, ⟨\cdot_{ndx}, (x \in {Base}_{R}, f \in B ⟼ (D \times \{x\}) {\underset{˙}{\cdot}}_{f} f)⟩, ⟨TopSet (ndx), \prod_{𝑡} (D \times \{TopOpen (R)\})⟩\})}$
28	18 4 27	3eqtr4g	$⊢ (I \in V \land R \in V) \to \underset{˙}{∙} = (f \in B, g \in B ⟼ (k \in D ⟼ \underset{x \in \{y \in D \| y \leq_{f} k\}}{\sum_{R}} (f (x) \underset{˙}{\cdot} g (k -_{f} x))))$
29	22	str0	$⊢ \emptyset = \cdot_{\emptyset}$
30	29	eqcomi	$⊢ \cdot_{\emptyset} = \emptyset$
31		reldmpsr	$⊢ Rel dom mPwSer$
32	31	ovprc	$⊢ \neg (I \in V \land R \in V) \to I mPwSer R = \emptyset$
33	1 32	syl5eq	$⊢ \neg (I \in V \land R \in V) \to S = \emptyset$
34	33	fveq2d	$⊢ \neg (I \in V \land R \in V) \to \cdot_{S} = \cdot_{\emptyset}$
35	4 34	syl5eq	$⊢ \neg (I \in V \land R \in V) \to \underset{˙}{∙} = \cdot_{\emptyset}$
36	33	fveq2d	$⊢ \neg (I \in V \land R \in V) \to {Base}_{S} = {Base}_{\emptyset}$
37		base0	$⊢ \emptyset = {Base}_{\emptyset}$
38	36 2 37	3eqtr4g	$⊢ \neg (I \in V \land R \in V) \to B = \emptyset$
39	38	olcd	$⊢ \neg (I \in V \land R \in V) \to (B = \emptyset \lor B = \emptyset)$
40		0mpo0	$⊢ (B = \emptyset \lor B = \emptyset) \to (f \in B, g \in B ⟼ (k \in D ⟼ \underset{x \in \{y \in D \| y \leq_{f} k\}}{\sum_{R}} (f (x) \underset{˙}{\cdot} g (k -_{f} x)))) = \emptyset$
41	39 40	syl	$⊢ \neg (I \in V \land R \in V) \to (f \in B, g \in B ⟼ (k \in D ⟼ \underset{x \in \{y \in D \| y \leq_{f} k\}}{\sum_{R}} (f (x) \underset{˙}{\cdot} g (k -_{f} x)))) = \emptyset$
42	30 35 41	3eqtr4a	$⊢ \neg (I \in V \land R \in V) \to \underset{˙}{∙} = (f \in B, g \in B ⟼ (k \in D ⟼ \underset{x \in \{y \in D \| y \leq_{f} k\}}{\sum_{R}} (f (x) \underset{˙}{\cdot} g (k -_{f} x))))$
43	28 42	pm2.61i	$⊢ \underset{˙}{∙} = (f \in B, g \in B ⟼ (k \in D ⟼ \underset{x \in \{y \in D \| y \leq_{f} k\}}{\sum_{R}} (f (x) \underset{˙}{\cdot} g (k -_{f} x))))$

Metamath Proof Explorer

Theorem psrmulr

Proof