psrvscafval

Description: The scalar 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-Nov-2024)

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

Proof

Step	Hyp	Ref	Expression
1		psrvsca.s	$⊢ S = I mPwSer R$
2		psrvsca.n	$⊢ \underset{˙}{∙} = \cdot_{S}$
3		psrvsca.k	$⊢ K = {Base}_{R}$
4		psrvsca.b	$⊢ B = {Base}_{S}$
5		psrvsca.m	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
6		psrvsca.d	$⊢ D = \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\}$
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 3 6 4 9	psrbas	$⊢ (I \in V \land R \in V) \to B = K^{D}$
11		eqid	$⊢ +_{S} = +_{S}$
12	1 4 7 11	psrplusg	$⊢ +_{S} = {\circ_{f} +_{R} ↾}_{(B \times B)}$
13		eqid	$⊢ \cdot_{S} = \cdot_{S}$
14	1 4 5 13 6	psrmulr	$⊢ \cdot_{S} = (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))))$
15		eqid	$⊢ (x \in K, f \in B ⟼ (D \times \{x\}) {\underset{˙}{\cdot}}_{f} f) = (x \in K, f \in B ⟼ (D \times \{x\}) {\underset{˙}{\cdot}}_{f} f)$
16		eqidd	$⊢ (I \in V \land R \in V) \to \prod_{𝑡} (D \times \{TopOpen (R)\}) = \prod_{𝑡} (D \times \{TopOpen (R)\})$
17		simpr	$⊢ (I \in V \land R \in V) \to R \in V$
18	1 3 7 5 8 6 10 12 14 15 16 9 17	psrval	$⊢ (I \in V \land R \in V) \to S = \{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, +_{S}⟩, ⟨\cdot_{ndx}, \cdot_{S}⟩\} \cup \{⟨Scalar (ndx), R⟩, ⟨\cdot_{ndx}, (x \in K, f \in B ⟼ (D \times \{x\}) {\underset{˙}{\cdot}}_{f} f)⟩, ⟨TopSet (ndx), \prod_{𝑡} (D \times \{TopOpen (R)\})⟩\}$
19	18	fveq2d	$⊢ (I \in V \land R \in V) \to \cdot_{S} = \cdot_{(\{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, +_{S}⟩, ⟨\cdot_{ndx}, \cdot_{S}⟩\} \cup \{⟨Scalar (ndx), R⟩, ⟨\cdot_{ndx}, (x \in K, f \in B ⟼ (D \times \{x\}) {\underset{˙}{\cdot}}_{f} f)⟩, ⟨TopSet (ndx), \prod_{𝑡} (D \times \{TopOpen (R)\})⟩\})}$
20	3	fvexi	$⊢ K \in V$
21	4	fvexi	$⊢ B \in V$
22	20 21	mpoex	$⊢ (x \in K, f \in B ⟼ (D \times \{x\}) {\underset{˙}{\cdot}}_{f} f) \in V$
23		psrvalstr	$⊢ (\{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, +_{S}⟩, ⟨\cdot_{ndx}, \cdot_{S}⟩\} \cup \{⟨Scalar (ndx), R⟩, ⟨\cdot_{ndx}, (x \in K, f \in B ⟼ (D \times \{x\}) {\underset{˙}{\cdot}}_{f} f)⟩, ⟨TopSet (ndx), \prod_{𝑡} (D \times \{TopOpen (R)\})⟩\}) Struct ⟨1, 9⟩$
24		vscaid	$⊢ \cdot_{𝑠} = Slot \cdot_{ndx}$
25		snsstp2	$⊢ \{⟨\cdot_{ndx}, (x \in K, f \in B ⟼ (D \times \{x\}) {\underset{˙}{\cdot}}_{f} f)⟩\} \subseteq \{⟨Scalar (ndx), R⟩, ⟨\cdot_{ndx}, (x \in K, f \in B ⟼ (D \times \{x\}) {\underset{˙}{\cdot}}_{f} f)⟩, ⟨TopSet (ndx), \prod_{𝑡} (D \times \{TopOpen (R)\})⟩\}$
26		ssun2	$⊢ \{⟨Scalar (ndx), R⟩, ⟨\cdot_{ndx}, (x \in K, f \in B ⟼ (D \times \{x\}) {\underset{˙}{\cdot}}_{f} f)⟩, ⟨TopSet (ndx), \prod_{𝑡} (D \times \{TopOpen (R)\})⟩\} \subseteq \{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, +_{S}⟩, ⟨\cdot_{ndx}, \cdot_{S}⟩\} \cup \{⟨Scalar (ndx), R⟩, ⟨\cdot_{ndx}, (x \in K, f \in B ⟼ (D \times \{x\}) {\underset{˙}{\cdot}}_{f} f)⟩, ⟨TopSet (ndx), \prod_{𝑡} (D \times \{TopOpen (R)\})⟩\}$
27	25 26	sstri	$⊢ \{⟨\cdot_{ndx}, (x \in K, f \in B ⟼ (D \times \{x\}) {\underset{˙}{\cdot}}_{f} f)⟩\} \subseteq \{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, +_{S}⟩, ⟨\cdot_{ndx}, \cdot_{S}⟩\} \cup \{⟨Scalar (ndx), R⟩, ⟨\cdot_{ndx}, (x \in K, f \in B ⟼ (D \times \{x\}) {\underset{˙}{\cdot}}_{f} f)⟩, ⟨TopSet (ndx), \prod_{𝑡} (D \times \{TopOpen (R)\})⟩\}$
28	23 24 27	strfv	$⊢ (x \in K, f \in B ⟼ (D \times \{x\}) {\underset{˙}{\cdot}}_{f} f) \in V \to (x \in K, f \in B ⟼ (D \times \{x\}) {\underset{˙}{\cdot}}_{f} f) = \cdot_{(\{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, +_{S}⟩, ⟨\cdot_{ndx}, \cdot_{S}⟩\} \cup \{⟨Scalar (ndx), R⟩, ⟨\cdot_{ndx}, (x \in K, f \in B ⟼ (D \times \{x\}) {\underset{˙}{\cdot}}_{f} f)⟩, ⟨TopSet (ndx), \prod_{𝑡} (D \times \{TopOpen (R)\})⟩\})}$
29	22 28	ax-mp	$⊢ (x \in K, f \in B ⟼ (D \times \{x\}) {\underset{˙}{\cdot}}_{f} f) = \cdot_{(\{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, +_{S}⟩, ⟨\cdot_{ndx}, \cdot_{S}⟩\} \cup \{⟨Scalar (ndx), R⟩, ⟨\cdot_{ndx}, (x \in K, f \in B ⟼ (D \times \{x\}) {\underset{˙}{\cdot}}_{f} f)⟩, ⟨TopSet (ndx), \prod_{𝑡} (D \times \{TopOpen (R)\})⟩\})}$
30	19 2 29	3eqtr4g	$⊢ (I \in V \land R \in V) \to \underset{˙}{∙} = (x \in K, f \in B ⟼ (D \times \{x\}) {\underset{˙}{\cdot}}_{f} f)$
31		eqid	$⊢ \emptyset = \emptyset$
32		fn0	$⊢ \emptyset Fn \emptyset \leftrightarrow \emptyset = \emptyset$
33	31 32	mpbir	$⊢ \emptyset Fn \emptyset$
34		reldmpsr	$⊢ Rel dom mPwSer$
35	34	ovprc	$⊢ \neg (I \in V \land R \in V) \to I mPwSer R = \emptyset$
36	1 35	eqtrid	$⊢ \neg (I \in V \land R \in V) \to S = \emptyset$
37	36	fveq2d	$⊢ \neg (I \in V \land R \in V) \to \cdot_{S} = \cdot_{\emptyset}$
38	24	str0	$⊢ \emptyset = \cdot_{\emptyset}$
39	37 2 38	3eqtr4g	$⊢ \neg (I \in V \land R \in V) \to \underset{˙}{∙} = \emptyset$
40	34 1 4	elbasov	$⊢ f \in B \to (I \in V \land R \in V)$
41	40	con3i	$⊢ \neg (I \in V \land R \in V) \to \neg f \in B$
42	41	eq0rdv	$⊢ \neg (I \in V \land R \in V) \to B = \emptyset$
43	42	xpeq2d	$⊢ \neg (I \in V \land R \in V) \to K \times B = K \times \emptyset$
44		xp0	$⊢ K \times \emptyset = \emptyset$
45	43 44	eqtrdi	$⊢ \neg (I \in V \land R \in V) \to K \times B = \emptyset$
46	39 45	fneq12d	$⊢ \neg (I \in V \land R \in V) \to (\underset{˙}{∙} Fn (K \times B) \leftrightarrow \emptyset Fn \emptyset)$
47	33 46	mpbiri	$⊢ \neg (I \in V \land R \in V) \to \underset{˙}{∙} Fn (K \times B)$
48		fnov	$⊢ \underset{˙}{∙} Fn (K \times B) \leftrightarrow \underset{˙}{∙} = (x \in K, f \in B ⟼ x \underset{˙}{∙} f)$
49	47 48	sylib	$⊢ \neg (I \in V \land R \in V) \to \underset{˙}{∙} = (x \in K, f \in B ⟼ x \underset{˙}{∙} f)$
50	41	pm2.21d	$⊢ \neg (I \in V \land R \in V) \to (f \in B \to (D \times \{x\}) {\underset{˙}{\cdot}}_{f} f = x \underset{˙}{∙} f)$
51	50	a1d	$⊢ \neg (I \in V \land R \in V) \to (x \in K \to (f \in B \to (D \times \{x\}) {\underset{˙}{\cdot}}_{f} f = x \underset{˙}{∙} f))$
52	51	3imp	$⊢ (\neg (I \in V \land R \in V) \land x \in K \land f \in B) \to (D \times \{x\}) {\underset{˙}{\cdot}}_{f} f = x \underset{˙}{∙} f$
53	52	mpoeq3dva	$⊢ \neg (I \in V \land R \in V) \to (x \in K, f \in B ⟼ (D \times \{x\}) {\underset{˙}{\cdot}}_{f} f) = (x \in K, f \in B ⟼ x \underset{˙}{∙} f)$
54	49 53	eqtr4d	$⊢ \neg (I \in V \land R \in V) \to \underset{˙}{∙} = (x \in K, f \in B ⟼ (D \times \{x\}) {\underset{˙}{\cdot}}_{f} f)$
55	30 54	pm2.61i	$⊢ \underset{˙}{∙} = (x \in K, f \in B ⟼ (D \times \{x\}) {\underset{˙}{\cdot}}_{f} f)$

Metamath Proof Explorer

Theorem psrvscafval

Proof