psrval

Description: Value of the multivariate power series structure. (Contributed by Mario Carneiro, 29-Dec-2014)

	Ref	Expression
Hypotheses	psrval.s	$⊢ S = I mPwSer R$
	psrval.k	$⊢ K = {Base}_{R}$
	psrval.a	$⊢ \underset{˙}{+} = +_{R}$
	psrval.m	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	psrval.o	$⊢ O = TopOpen (R)$
	psrval.d	$⊢ D = \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\}$
	psrval.b	$⊢ φ \to B = K^{D}$
	psrval.p	$⊢ \underset{˙}{✚} = {\circ_{f} \underset{˙}{+} ↾}_{(B \times B)}$
	psrval.t	$⊢ \underset{˙}{\times} = (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))))$
	psrval.v	$⊢ \underset{˙}{∙} = (x \in K, f \in B ⟼ (D \times \{x\}) {\underset{˙}{\cdot}}_{f} f)$
	psrval.j	$⊢ φ \to J = \prod_{𝑡} (D \times \{O\})$
	psrval.i	$⊢ φ \to I \in W$
	psrval.r	$⊢ φ \to R \in X$
Assertion	psrval	$⊢ φ \to S = \{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, \underset{˙}{✚}⟩, ⟨\cdot_{ndx}, \underset{˙}{\times}⟩\} \cup \{⟨Scalar (ndx), R⟩, ⟨\cdot_{ndx}, \underset{˙}{∙}⟩, ⟨TopSet (ndx), J⟩\}$

Proof

Step	Hyp	Ref	Expression
1		psrval.s	$⊢ S = I mPwSer R$
2		psrval.k	$⊢ K = {Base}_{R}$
3		psrval.a	$⊢ \underset{˙}{+} = +_{R}$
4		psrval.m	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
5		psrval.o	$⊢ O = TopOpen (R)$
6		psrval.d	$⊢ D = \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\}$
7		psrval.b	$⊢ φ \to B = K^{D}$
8		psrval.p	$⊢ \underset{˙}{✚} = {\circ_{f} \underset{˙}{+} ↾}_{(B \times B)}$
9		psrval.t	$⊢ \underset{˙}{\times} = (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))))$
10		psrval.v	$⊢ \underset{˙}{∙} = (x \in K, f \in B ⟼ (D \times \{x\}) {\underset{˙}{\cdot}}_{f} f)$
11		psrval.j	$⊢ φ \to J = \prod_{𝑡} (D \times \{O\})$
12		psrval.i	$⊢ φ \to I \in W$
13		psrval.r	$⊢ φ \to R \in X$
14		df-psr	$⊢ mPwSer = (i \in V, r \in V ⟼ ⦋ \{h \in ({ℕ_{0}}^{i}) \| h^{-1} [ℕ] \in Fin\} / d ⦌ ⦋ ({Base}_{r}^{d}) / b ⦌ (\{⟨{Base}_{ndx}, b⟩, ⟨+_{ndx}, {\circ_{f} +_{r} ↾}_{(b \times b)}⟩, ⟨\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) \cdot_{r} g (k -_{f} x))))⟩\} \cup \{⟨Scalar (ndx), r⟩, ⟨\cdot_{ndx}, (x \in {Base}_{r}, f \in b ⟼ (d \times \{x\}) {\cdot_{r}}_{f} f)⟩, ⟨TopSet (ndx), \prod_{𝑡} (d \times \{TopOpen (r)\})⟩\}))$
15	14	a1i	$⊢ φ \to mPwSer = (i \in V, r \in V ⟼ ⦋ \{h \in ({ℕ_{0}}^{i}) \| h^{-1} [ℕ] \in Fin\} / d ⦌ ⦋ ({Base}_{r}^{d}) / b ⦌ (\{⟨{Base}_{ndx}, b⟩, ⟨+_{ndx}, {\circ_{f} +_{r} ↾}_{(b \times b)}⟩, ⟨\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) \cdot_{r} g (k -_{f} x))))⟩\} \cup \{⟨Scalar (ndx), r⟩, ⟨\cdot_{ndx}, (x \in {Base}_{r}, f \in b ⟼ (d \times \{x\}) {\cdot_{r}}_{f} f)⟩, ⟨TopSet (ndx), \prod_{𝑡} (d \times \{TopOpen (r)\})⟩\}))$
16		simprl	$⊢ (φ \land (i = I \land r = R)) \to i = I$
17	16	oveq2d	$⊢ (φ \land (i = I \land r = R)) \to {ℕ_{0}}^{i} = {ℕ_{0}}^{I}$
18		rabeq	$⊢ {ℕ_{0}}^{i} = {ℕ_{0}}^{I} \to \{h \in ({ℕ_{0}}^{i}) \| h^{-1} [ℕ] \in Fin\} = \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\}$
19	17 18	syl	$⊢ (φ \land (i = I \land r = R)) \to \{h \in ({ℕ_{0}}^{i}) \| h^{-1} [ℕ] \in Fin\} = \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\}$
20	19 6	eqtr4di	$⊢ (φ \land (i = I \land r = R)) \to \{h \in ({ℕ_{0}}^{i}) \| h^{-1} [ℕ] \in Fin\} = D$
21	20	csbeq1d	$⊢ (φ \land (i = I \land r = R)) \to ⦋ \{h \in ({ℕ_{0}}^{i}) \| h^{-1} [ℕ] \in Fin\} / d ⦌ ⦋ ({Base}_{r}^{d}) / b ⦌ (\{⟨{Base}_{ndx}, b⟩, ⟨+_{ndx}, {\circ_{f} +_{r} ↾}_{(b \times b)}⟩, ⟨\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) \cdot_{r} g (k -_{f} x))))⟩\} \cup \{⟨Scalar (ndx), r⟩, ⟨\cdot_{ndx}, (x \in {Base}_{r}, f \in b ⟼ (d \times \{x\}) {\cdot_{r}}_{f} f)⟩, ⟨TopSet (ndx), \prod_{𝑡} (d \times \{TopOpen (r)\})⟩\}) = ⦋ D / d ⦌ ⦋ ({Base}_{r}^{d}) / b ⦌ (\{⟨{Base}_{ndx}, b⟩, ⟨+_{ndx}, {\circ_{f} +_{r} ↾}_{(b \times b)}⟩, ⟨\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) \cdot_{r} g (k -_{f} x))))⟩\} \cup \{⟨Scalar (ndx), r⟩, ⟨\cdot_{ndx}, (x \in {Base}_{r}, f \in b ⟼ (d \times \{x\}) {\cdot_{r}}_{f} f)⟩, ⟨TopSet (ndx), \prod_{𝑡} (d \times \{TopOpen (r)\})⟩\})$
22		ovex	$⊢ {ℕ_{0}}^{i} \in V$
23	22	rabex	$⊢ \{h \in ({ℕ_{0}}^{i}) \| h^{-1} [ℕ] \in Fin\} \in V$
24	20 23	eqeltrrdi	$⊢ (φ \land (i = I \land r = R)) \to D \in V$
25		simplrr	$⊢ ((φ \land (i = I \land r = R)) \land d = D) \to r = R$
26	25	fveq2d	$⊢ ((φ \land (i = I \land r = R)) \land d = D) \to {Base}_{r} = {Base}_{R}$
27	26 2	eqtr4di	$⊢ ((φ \land (i = I \land r = R)) \land d = D) \to {Base}_{r} = K$
28		simpr	$⊢ ((φ \land (i = I \land r = R)) \land d = D) \to d = D$
29	27 28	oveq12d	$⊢ ((φ \land (i = I \land r = R)) \land d = D) \to {Base}_{r}^{d} = K^{D}$
30	7	ad2antrr	$⊢ ((φ \land (i = I \land r = R)) \land d = D) \to B = K^{D}$
31	29 30	eqtr4d	$⊢ ((φ \land (i = I \land r = R)) \land d = D) \to {Base}_{r}^{d} = B$
32	31	csbeq1d	$⊢ ((φ \land (i = I \land r = R)) \land d = D) \to ⦋ ({Base}_{r}^{d}) / b ⦌ (\{⟨{Base}_{ndx}, b⟩, ⟨+_{ndx}, {\circ_{f} +_{r} ↾}_{(b \times b)}⟩, ⟨\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) \cdot_{r} g (k -_{f} x))))⟩\} \cup \{⟨Scalar (ndx), r⟩, ⟨\cdot_{ndx}, (x \in {Base}_{r}, f \in b ⟼ (d \times \{x\}) {\cdot_{r}}_{f} f)⟩, ⟨TopSet (ndx), \prod_{𝑡} (d \times \{TopOpen (r)\})⟩\}) = ⦋ B / b ⦌ (\{⟨{Base}_{ndx}, b⟩, ⟨+_{ndx}, {\circ_{f} +_{r} ↾}_{(b \times b)}⟩, ⟨\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) \cdot_{r} g (k -_{f} x))))⟩\} \cup \{⟨Scalar (ndx), r⟩, ⟨\cdot_{ndx}, (x \in {Base}_{r}, f \in b ⟼ (d \times \{x\}) {\cdot_{r}}_{f} f)⟩, ⟨TopSet (ndx), \prod_{𝑡} (d \times \{TopOpen (r)\})⟩\})$
33		ovex	$⊢ {Base}_{r}^{d} \in V$
34	31 33	eqeltrrdi	$⊢ ((φ \land (i = I \land r = R)) \land d = D) \to B \in V$
35		simpr	$⊢ (((φ \land (i = I \land r = R)) \land d = D) \land b = B) \to b = B$
36	35	opeq2d	$⊢ (((φ \land (i = I \land r = R)) \land d = D) \land b = B) \to ⟨{Base}_{ndx}, b⟩ = ⟨{Base}_{ndx}, B⟩$
37	25	adantr	$⊢ (((φ \land (i = I \land r = R)) \land d = D) \land b = B) \to r = R$
38	37	fveq2d	$⊢ (((φ \land (i = I \land r = R)) \land d = D) \land b = B) \to +_{r} = +_{R}$
39	38 3	eqtr4di	$⊢ (((φ \land (i = I \land r = R)) \land d = D) \land b = B) \to +_{r} = \underset{˙}{+}$
40	39	ofeqd	$⊢ (((φ \land (i = I \land r = R)) \land d = D) \land b = B) \to \circ_{f} +_{r} = \circ_{f} \underset{˙}{+}$
41	35 35	xpeq12d	$⊢ (((φ \land (i = I \land r = R)) \land d = D) \land b = B) \to b \times b = B \times B$
42	40 41	reseq12d	$⊢ (((φ \land (i = I \land r = R)) \land d = D) \land b = B) \to {\circ_{f} +_{r} ↾}_{(b \times b)} = {\circ_{f} \underset{˙}{+} ↾}_{(B \times B)}$
43	42 8	eqtr4di	$⊢ (((φ \land (i = I \land r = R)) \land d = D) \land b = B) \to {\circ_{f} +_{r} ↾}_{(b \times b)} = \underset{˙}{✚}$
44	43	opeq2d	$⊢ (((φ \land (i = I \land r = R)) \land d = D) \land b = B) \to ⟨+_{ndx}, {\circ_{f} +_{r} ↾}_{(b \times b)}⟩ = ⟨+_{ndx}, \underset{˙}{✚}⟩$
45	28	adantr	$⊢ (((φ \land (i = I \land r = R)) \land d = D) \land b = B) \to d = D$
46		rabeq	$⊢ d = D \to \{y \in d \| y \leq_{f} k\} = \{y \in D \| y \leq_{f} k\}$
47	45 46	syl	$⊢ (((φ \land (i = I \land r = R)) \land d = D) \land b = B) \to \{y \in d \| y \leq_{f} k\} = \{y \in D \| y \leq_{f} k\}$
48	37	fveq2d	$⊢ (((φ \land (i = I \land r = R)) \land d = D) \land b = B) \to \cdot_{r} = \cdot_{R}$
49	48 4	eqtr4di	$⊢ (((φ \land (i = I \land r = R)) \land d = D) \land b = B) \to \cdot_{r} = \underset{˙}{\cdot}$
50	49	oveqd	$⊢ (((φ \land (i = I \land r = R)) \land d = D) \land b = B) \to f (x) \cdot_{r} g (k -_{f} x) = f (x) \underset{˙}{\cdot} g (k -_{f} x)$
51	47 50	mpteq12dv	$⊢ (((φ \land (i = I \land r = R)) \land d = D) \land b = B) \to (x \in \{y \in d \| y \leq_{f} k\} ⟼ f (x) \cdot_{r} g (k -_{f} x)) = (x \in \{y \in D \| y \leq_{f} k\} ⟼ f (x) \underset{˙}{\cdot} g (k -_{f} x))$
52	37 51	oveq12d	$⊢ (((φ \land (i = I \land r = R)) \land d = D) \land b = B) \to \underset{x \in \{y \in d \| y \leq_{f} k\}}{\sum_{r}} (f (x) \cdot_{r} g (k -_{f} x)) = \underset{x \in \{y \in D \| y \leq_{f} k\}}{\sum_{R}} (f (x) \underset{˙}{\cdot} g (k -_{f} x))$
53	45 52	mpteq12dv	$⊢ (((φ \land (i = I \land r = R)) \land d = D) \land b = B) \to (k \in d ⟼ \underset{x \in \{y \in d \| y \leq_{f} k\}}{\sum_{r}} (f (x) \cdot_{r} g (k -_{f} x))) = (k \in D ⟼ \underset{x \in \{y \in D \| y \leq_{f} k\}}{\sum_{R}} (f (x) \underset{˙}{\cdot} g (k -_{f} x)))$
54	35 35 53	mpoeq123dv	$⊢ (((φ \land (i = I \land r = R)) \land d = D) \land b = B) \to (f \in b, g \in b ⟼ (k \in d ⟼ \underset{x \in \{y \in d \| y \leq_{f} k\}}{\sum_{r}} (f (x) \cdot_{r} 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))))$
55	54 9	eqtr4di	$⊢ (((φ \land (i = I \land r = R)) \land d = D) \land b = B) \to (f \in b, g \in b ⟼ (k \in d ⟼ \underset{x \in \{y \in d \| y \leq_{f} k\}}{\sum_{r}} (f (x) \cdot_{r} g (k -_{f} x)))) = \underset{˙}{\times}$
56	55	opeq2d	$⊢ (((φ \land (i = I \land r = R)) \land d = D) \land b = B) \to ⟨\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) \cdot_{r} g (k -_{f} x))))⟩ = ⟨\cdot_{ndx}, \underset{˙}{\times}⟩$
57	36 44 56	tpeq123d	$⊢ (((φ \land (i = I \land r = R)) \land d = D) \land b = B) \to \{⟨{Base}_{ndx}, b⟩, ⟨+_{ndx}, {\circ_{f} +_{r} ↾}_{(b \times b)}⟩, ⟨\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) \cdot_{r} g (k -_{f} x))))⟩\} = \{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, \underset{˙}{✚}⟩, ⟨\cdot_{ndx}, \underset{˙}{\times}⟩\}$
58	37	opeq2d	$⊢ (((φ \land (i = I \land r = R)) \land d = D) \land b = B) \to ⟨Scalar (ndx), r⟩ = ⟨Scalar (ndx), R⟩$
59	27	adantr	$⊢ (((φ \land (i = I \land r = R)) \land d = D) \land b = B) \to {Base}_{r} = K$
60	49	ofeqd	$⊢ (((φ \land (i = I \land r = R)) \land d = D) \land b = B) \to \circ_{f} \cdot_{r} = \circ_{f} \underset{˙}{\cdot}$
61	45	xpeq1d	$⊢ (((φ \land (i = I \land r = R)) \land d = D) \land b = B) \to d \times \{x\} = D \times \{x\}$
62		eqidd	$⊢ (((φ \land (i = I \land r = R)) \land d = D) \land b = B) \to f = f$
63	60 61 62	oveq123d	$⊢ (((φ \land (i = I \land r = R)) \land d = D) \land b = B) \to (d \times \{x\}) {\cdot_{r}}_{f} f = (D \times \{x\}) {\underset{˙}{\cdot}}_{f} f$
64	59 35 63	mpoeq123dv	$⊢ (((φ \land (i = I \land r = R)) \land d = D) \land b = B) \to (x \in {Base}_{r}, f \in b ⟼ (d \times \{x\}) {\cdot_{r}}_{f} f) = (x \in K, f \in B ⟼ (D \times \{x\}) {\underset{˙}{\cdot}}_{f} f)$
65	64 10	eqtr4di	$⊢ (((φ \land (i = I \land r = R)) \land d = D) \land b = B) \to (x \in {Base}_{r}, f \in b ⟼ (d \times \{x\}) {\cdot_{r}}_{f} f) = \underset{˙}{∙}$
66	65	opeq2d	$⊢ (((φ \land (i = I \land r = R)) \land d = D) \land b = B) \to ⟨\cdot_{ndx}, (x \in {Base}_{r}, f \in b ⟼ (d \times \{x\}) {\cdot_{r}}_{f} f)⟩ = ⟨\cdot_{ndx}, \underset{˙}{∙}⟩$
67	37	fveq2d	$⊢ (((φ \land (i = I \land r = R)) \land d = D) \land b = B) \to TopOpen (r) = TopOpen (R)$
68	67 5	eqtr4di	$⊢ (((φ \land (i = I \land r = R)) \land d = D) \land b = B) \to TopOpen (r) = O$
69	68	sneqd	$⊢ (((φ \land (i = I \land r = R)) \land d = D) \land b = B) \to \{TopOpen (r)\} = \{O\}$
70	45 69	xpeq12d	$⊢ (((φ \land (i = I \land r = R)) \land d = D) \land b = B) \to d \times \{TopOpen (r)\} = D \times \{O\}$
71	70	fveq2d	$⊢ (((φ \land (i = I \land r = R)) \land d = D) \land b = B) \to \prod_{𝑡} (d \times \{TopOpen (r)\}) = \prod_{𝑡} (D \times \{O\})$
72	11	ad3antrrr	$⊢ (((φ \land (i = I \land r = R)) \land d = D) \land b = B) \to J = \prod_{𝑡} (D \times \{O\})$
73	71 72	eqtr4d	$⊢ (((φ \land (i = I \land r = R)) \land d = D) \land b = B) \to \prod_{𝑡} (d \times \{TopOpen (r)\}) = J$
74	73	opeq2d	$⊢ (((φ \land (i = I \land r = R)) \land d = D) \land b = B) \to ⟨TopSet (ndx), \prod_{𝑡} (d \times \{TopOpen (r)\})⟩ = ⟨TopSet (ndx), J⟩$
75	58 66 74	tpeq123d	$⊢ (((φ \land (i = I \land r = R)) \land d = D) \land b = B) \to \{⟨Scalar (ndx), r⟩, ⟨\cdot_{ndx}, (x \in {Base}_{r}, f \in b ⟼ (d \times \{x\}) {\cdot_{r}}_{f} f)⟩, ⟨TopSet (ndx), \prod_{𝑡} (d \times \{TopOpen (r)\})⟩\} = \{⟨Scalar (ndx), R⟩, ⟨\cdot_{ndx}, \underset{˙}{∙}⟩, ⟨TopSet (ndx), J⟩\}$
76	57 75	uneq12d	$⊢ (((φ \land (i = I \land r = R)) \land d = D) \land b = B) \to \{⟨{Base}_{ndx}, b⟩, ⟨+_{ndx}, {\circ_{f} +_{r} ↾}_{(b \times b)}⟩, ⟨\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) \cdot_{r} g (k -_{f} x))))⟩\} \cup \{⟨Scalar (ndx), r⟩, ⟨\cdot_{ndx}, (x \in {Base}_{r}, f \in b ⟼ (d \times \{x\}) {\cdot_{r}}_{f} f)⟩, ⟨TopSet (ndx), \prod_{𝑡} (d \times \{TopOpen (r)\})⟩\} = \{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, \underset{˙}{✚}⟩, ⟨\cdot_{ndx}, \underset{˙}{\times}⟩\} \cup \{⟨Scalar (ndx), R⟩, ⟨\cdot_{ndx}, \underset{˙}{∙}⟩, ⟨TopSet (ndx), J⟩\}$
77	34 76	csbied	$⊢ ((φ \land (i = I \land r = R)) \land d = D) \to ⦋ B / b ⦌ (\{⟨{Base}_{ndx}, b⟩, ⟨+_{ndx}, {\circ_{f} +_{r} ↾}_{(b \times b)}⟩, ⟨\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) \cdot_{r} g (k -_{f} x))))⟩\} \cup \{⟨Scalar (ndx), r⟩, ⟨\cdot_{ndx}, (x \in {Base}_{r}, f \in b ⟼ (d \times \{x\}) {\cdot_{r}}_{f} f)⟩, ⟨TopSet (ndx), \prod_{𝑡} (d \times \{TopOpen (r)\})⟩\}) = \{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, \underset{˙}{✚}⟩, ⟨\cdot_{ndx}, \underset{˙}{\times}⟩\} \cup \{⟨Scalar (ndx), R⟩, ⟨\cdot_{ndx}, \underset{˙}{∙}⟩, ⟨TopSet (ndx), J⟩\}$
78	32 77	eqtrd	$⊢ ((φ \land (i = I \land r = R)) \land d = D) \to ⦋ ({Base}_{r}^{d}) / b ⦌ (\{⟨{Base}_{ndx}, b⟩, ⟨+_{ndx}, {\circ_{f} +_{r} ↾}_{(b \times b)}⟩, ⟨\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) \cdot_{r} g (k -_{f} x))))⟩\} \cup \{⟨Scalar (ndx), r⟩, ⟨\cdot_{ndx}, (x \in {Base}_{r}, f \in b ⟼ (d \times \{x\}) {\cdot_{r}}_{f} f)⟩, ⟨TopSet (ndx), \prod_{𝑡} (d \times \{TopOpen (r)\})⟩\}) = \{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, \underset{˙}{✚}⟩, ⟨\cdot_{ndx}, \underset{˙}{\times}⟩\} \cup \{⟨Scalar (ndx), R⟩, ⟨\cdot_{ndx}, \underset{˙}{∙}⟩, ⟨TopSet (ndx), J⟩\}$
79	24 78	csbied	$⊢ (φ \land (i = I \land r = R)) \to ⦋ D / d ⦌ ⦋ ({Base}_{r}^{d}) / b ⦌ (\{⟨{Base}_{ndx}, b⟩, ⟨+_{ndx}, {\circ_{f} +_{r} ↾}_{(b \times b)}⟩, ⟨\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) \cdot_{r} g (k -_{f} x))))⟩\} \cup \{⟨Scalar (ndx), r⟩, ⟨\cdot_{ndx}, (x \in {Base}_{r}, f \in b ⟼ (d \times \{x\}) {\cdot_{r}}_{f} f)⟩, ⟨TopSet (ndx), \prod_{𝑡} (d \times \{TopOpen (r)\})⟩\}) = \{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, \underset{˙}{✚}⟩, ⟨\cdot_{ndx}, \underset{˙}{\times}⟩\} \cup \{⟨Scalar (ndx), R⟩, ⟨\cdot_{ndx}, \underset{˙}{∙}⟩, ⟨TopSet (ndx), J⟩\}$
80	21 79	eqtrd	$⊢ (φ \land (i = I \land r = R)) \to ⦋ \{h \in ({ℕ_{0}}^{i}) \| h^{-1} [ℕ] \in Fin\} / d ⦌ ⦋ ({Base}_{r}^{d}) / b ⦌ (\{⟨{Base}_{ndx}, b⟩, ⟨+_{ndx}, {\circ_{f} +_{r} ↾}_{(b \times b)}⟩, ⟨\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) \cdot_{r} g (k -_{f} x))))⟩\} \cup \{⟨Scalar (ndx), r⟩, ⟨\cdot_{ndx}, (x \in {Base}_{r}, f \in b ⟼ (d \times \{x\}) {\cdot_{r}}_{f} f)⟩, ⟨TopSet (ndx), \prod_{𝑡} (d \times \{TopOpen (r)\})⟩\}) = \{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, \underset{˙}{✚}⟩, ⟨\cdot_{ndx}, \underset{˙}{\times}⟩\} \cup \{⟨Scalar (ndx), R⟩, ⟨\cdot_{ndx}, \underset{˙}{∙}⟩, ⟨TopSet (ndx), J⟩\}$
81	12	elexd	$⊢ φ \to I \in V$
82	13	elexd	$⊢ φ \to R \in V$
83		tpex	$⊢ \{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, \underset{˙}{✚}⟩, ⟨\cdot_{ndx}, \underset{˙}{\times}⟩\} \in V$
84		tpex	$⊢ \{⟨Scalar (ndx), R⟩, ⟨\cdot_{ndx}, \underset{˙}{∙}⟩, ⟨TopSet (ndx), J⟩\} \in V$
85	83 84	unex	$⊢ \{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, \underset{˙}{✚}⟩, ⟨\cdot_{ndx}, \underset{˙}{\times}⟩\} \cup \{⟨Scalar (ndx), R⟩, ⟨\cdot_{ndx}, \underset{˙}{∙}⟩, ⟨TopSet (ndx), J⟩\} \in V$
86	85	a1i	$⊢ φ \to \{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, \underset{˙}{✚}⟩, ⟨\cdot_{ndx}, \underset{˙}{\times}⟩\} \cup \{⟨Scalar (ndx), R⟩, ⟨\cdot_{ndx}, \underset{˙}{∙}⟩, ⟨TopSet (ndx), J⟩\} \in V$
87	15 80 81 82 86	ovmpod	$⊢ φ \to I mPwSer R = \{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, \underset{˙}{✚}⟩, ⟨\cdot_{ndx}, \underset{˙}{\times}⟩\} \cup \{⟨Scalar (ndx), R⟩, ⟨\cdot_{ndx}, \underset{˙}{∙}⟩, ⟨TopSet (ndx), J⟩\}$
88	1 87	eqtrid	$⊢ φ \to S = \{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, \underset{˙}{✚}⟩, ⟨\cdot_{ndx}, \underset{˙}{\times}⟩\} \cup \{⟨Scalar (ndx), R⟩, ⟨\cdot_{ndx}, \underset{˙}{∙}⟩, ⟨TopSet (ndx), J⟩\}$

Metamath Proof Explorer

Theorem psrval

Proof