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		ofeq	$⊢ +_{r} = \underset{˙}{+} \to \circ_{f} +_{r} = \circ_{f} \underset{˙}{+}$
41	39 40	syl	$⊢ (((φ \land (i = I \land r = R)) \land d = D) \land b = B) \to \circ_{f} +_{r} = \circ_{f} \underset{˙}{+}$
42	35 35	xpeq12d	$⊢ (((φ \land (i = I \land r = R)) \land d = D) \land b = B) \to b \times b = B \times B$
43	41 42	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)}$
44	43 8	eqtr4di	$⊢ (((φ \land (i = I \land r = R)) \land d = D) \land b = B) \to {\circ_{f} +_{r} ↾}_{(b \times b)} = \underset{˙}{✚}$
45	44	opeq2d	$⊢ (((φ \land (i = I \land r = R)) \land d = D) \land b = B) \to ⟨+_{ndx}, {\circ_{f} +_{r} ↾}_{(b \times b)}⟩ = ⟨+_{ndx}, \underset{˙}{✚}⟩$
46	28	adantr	$⊢ (((φ \land (i = I \land r = R)) \land d = D) \land b = B) \to d = D$
47		rabeq	$⊢ d = D \to \{y \in d \| y \leq_{f} k\} = \{y \in D \| y \leq_{f} k\}$
48	46 47	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\}$
49	37	fveq2d	$⊢ (((φ \land (i = I \land r = R)) \land d = D) \land b = B) \to \cdot_{r} = \cdot_{R}$
50	49 4	eqtr4di	$⊢ (((φ \land (i = I \land r = R)) \land d = D) \land b = B) \to \cdot_{r} = \underset{˙}{\cdot}$
51	50	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)$
52	48 51	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))$
53	37 52	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))$
54	46 53	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)))$
55	35 35 54	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))))$
56	55 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}$
57	56	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}⟩$
58	36 45 57	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}⟩\}$
59	37	opeq2d	$⊢ (((φ \land (i = I \land r = R)) \land d = D) \land b = B) \to ⟨Scalar (ndx), r⟩ = ⟨Scalar (ndx), R⟩$
60	27	adantr	$⊢ (((φ \land (i = I \land r = R)) \land d = D) \land b = B) \to {Base}_{r} = K$
61		ofeq	$⊢ \cdot_{r} = \underset{˙}{\cdot} \to \circ_{f} \cdot_{r} = \circ_{f} \underset{˙}{\cdot}$
62	50 61	syl	$⊢ (((φ \land (i = I \land r = R)) \land d = D) \land b = B) \to \circ_{f} \cdot_{r} = \circ_{f} \underset{˙}{\cdot}$
63	46	xpeq1d	$⊢ (((φ \land (i = I \land r = R)) \land d = D) \land b = B) \to d \times \{x\} = D \times \{x\}$
64		eqidd	$⊢ (((φ \land (i = I \land r = R)) \land d = D) \land b = B) \to f = f$
65	62 63 64	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$
66	60 35 65	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)$
67	66 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{˙}{∙}$
68	67	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{˙}{∙}⟩$
69	37	fveq2d	$⊢ (((φ \land (i = I \land r = R)) \land d = D) \land b = B) \to TopOpen (r) = TopOpen (R)$
70	69 5	eqtr4di	$⊢ (((φ \land (i = I \land r = R)) \land d = D) \land b = B) \to TopOpen (r) = O$
71	70	sneqd	$⊢ (((φ \land (i = I \land r = R)) \land d = D) \land b = B) \to \{TopOpen (r)\} = \{O\}$
72	46 71	xpeq12d	$⊢ (((φ \land (i = I \land r = R)) \land d = D) \land b = B) \to d \times \{TopOpen (r)\} = D \times \{O\}$
73	72	fveq2d	$⊢ (((φ \land (i = I \land r = R)) \land d = D) \land b = B) \to \prod_{𝑡} (d \times \{TopOpen (r)\}) = \prod_{𝑡} (D \times \{O\})$
74	11	ad3antrrr	$⊢ (((φ \land (i = I \land r = R)) \land d = D) \land b = B) \to J = \prod_{𝑡} (D \times \{O\})$
75	73 74	eqtr4d	$⊢ (((φ \land (i = I \land r = R)) \land d = D) \land b = B) \to \prod_{𝑡} (d \times \{TopOpen (r)\}) = J$
76	75	opeq2d	$⊢ (((φ \land (i = I \land r = R)) \land d = D) \land b = B) \to ⟨TopSet (ndx), \prod_{𝑡} (d \times \{TopOpen (r)\})⟩ = ⟨TopSet (ndx), J⟩$
77	59 68 76	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⟩\}$
78	58 77	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⟩\}$
79	34 78	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⟩\}$
80	32 79	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⟩\}$
81	24 80	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⟩\}$
82	21 81	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⟩\}$
83	12	elexd	$⊢ φ \to I \in V$
84	13	elexd	$⊢ φ \to R \in V$
85		tpex	$⊢ \{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, \underset{˙}{✚}⟩, ⟨\cdot_{ndx}, \underset{˙}{\times}⟩\} \in V$
86		tpex	$⊢ \{⟨Scalar (ndx), R⟩, ⟨\cdot_{ndx}, \underset{˙}{∙}⟩, ⟨TopSet (ndx), J⟩\} \in V$
87	85 86	unex	$⊢ \{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, \underset{˙}{✚}⟩, ⟨\cdot_{ndx}, \underset{˙}{\times}⟩\} \cup \{⟨Scalar (ndx), R⟩, ⟨\cdot_{ndx}, \underset{˙}{∙}⟩, ⟨TopSet (ndx), J⟩\} \in V$
88	87	a1i	$⊢ φ \to \{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, \underset{˙}{✚}⟩, ⟨\cdot_{ndx}, \underset{˙}{\times}⟩\} \cup \{⟨Scalar (ndx), R⟩, ⟨\cdot_{ndx}, \underset{˙}{∙}⟩, ⟨TopSet (ndx), J⟩\} \in V$
89	15 82 83 84 88	ovmpod	$⊢ φ \to I mPwSer R = \{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, \underset{˙}{✚}⟩, ⟨\cdot_{ndx}, \underset{˙}{\times}⟩\} \cup \{⟨Scalar (ndx), R⟩, ⟨\cdot_{ndx}, \underset{˙}{∙}⟩, ⟨TopSet (ndx), J⟩\}$
90	1 89	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