psrbas

Description: The base set of the multivariate power series structure. (Contributed by Mario Carneiro, 28-Dec-2014) (Revised by Mario Carneiro, 2-Oct-2015) (Proof shortened by AV, 8-Jul-2019)

	Ref	Expression
Hypotheses	psrbas.s	$⊢ S = I mPwSer R$
	psrbas.k	$⊢ K = {Base}_{R}$
	psrbas.d	$⊢ D = \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}$
	psrbas.b	$⊢ B = {Base}_{S}$
	psrbas.i	$⊢ φ \to I \in V$
Assertion	psrbas	$⊢ φ \to B = K^{D}$

Proof

Step	Hyp	Ref	Expression
1		psrbas.s	$⊢ S = I mPwSer R$
2		psrbas.k	$⊢ K = {Base}_{R}$
3		psrbas.d	$⊢ D = \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}$
4		psrbas.b	$⊢ B = {Base}_{S}$
5		psrbas.i	$⊢ φ \to I \in V$
6		eqid	$⊢ +_{R} = +_{R}$
7		eqid	$⊢ \cdot_{R} = \cdot_{R}$
8		eqid	$⊢ TopOpen (R) = TopOpen (R)$
9		eqidd	$⊢ (φ \land R \in V) \to K^{D} = K^{D}$
10		eqid	$⊢ {\circ_{f} +_{R} ↾}_{((K^{D}) \times (K^{D}))} = {\circ_{f} +_{R} ↾}_{((K^{D}) \times (K^{D}))}$
11		eqid	$⊢ (g \in (K^{D}), h \in (K^{D}) ⟼ (k \in D ⟼ \underset{x \in \{y \in D \| y \leq_{f} k\}}{\sum_{R}} (g (x) \cdot_{R} h (k -_{f} x)))) = (g \in (K^{D}), h \in (K^{D}) ⟼ (k \in D ⟼ \underset{x \in \{y \in D \| y \leq_{f} k\}}{\sum_{R}} (g (x) \cdot_{R} h (k -_{f} x))))$
12		eqid	$⊢ (x \in K, g \in (K^{D}) ⟼ (D \times \{x\}) {\cdot_{R}}_{f} g) = (x \in K, g \in (K^{D}) ⟼ (D \times \{x\}) {\cdot_{R}}_{f} g)$
13		eqidd	$⊢ (φ \land R \in V) \to \prod_{𝑡} (D \times \{TopOpen (R)\}) = \prod_{𝑡} (D \times \{TopOpen (R)\})$
14	5	adantr	$⊢ (φ \land R \in V) \to I \in V$
15		simpr	$⊢ (φ \land R \in V) \to R \in V$
16	1 2 6 7 8 3 9 10 11 12 13 14 15	psrval	$⊢ (φ \land R \in V) \to S = \{⟨{Base}_{ndx}, K^{D}⟩, ⟨+_{ndx}, {\circ_{f} +_{R} ↾}_{((K^{D}) \times (K^{D}))}⟩, ⟨\cdot_{ndx}, (g \in (K^{D}), h \in (K^{D}) ⟼ (k \in D ⟼ \underset{x \in \{y \in D \| y \leq_{f} k\}}{\sum_{R}} (g (x) \cdot_{R} h (k -_{f} x))))⟩\} \cup \{⟨Scalar (ndx), R⟩, ⟨\cdot_{ndx}, (x \in K, g \in (K^{D}) ⟼ (D \times \{x\}) {\cdot_{R}}_{f} g)⟩, ⟨TopSet (ndx), \prod_{𝑡} (D \times \{TopOpen (R)\})⟩\}$
17	16	fveq2d	$⊢ (φ \land R \in V) \to {Base}_{S} = {Base}_{(\{⟨{Base}_{ndx}, K^{D}⟩, ⟨+_{ndx}, {\circ_{f} +_{R} ↾}_{((K^{D}) \times (K^{D}))}⟩, ⟨\cdot_{ndx}, (g \in (K^{D}), h \in (K^{D}) ⟼ (k \in D ⟼ \underset{x \in \{y \in D \| y \leq_{f} k\}}{\sum_{R}} (g (x) \cdot_{R} h (k -_{f} x))))⟩\} \cup \{⟨Scalar (ndx), R⟩, ⟨\cdot_{ndx}, (x \in K, g \in (K^{D}) ⟼ (D \times \{x\}) {\cdot_{R}}_{f} g)⟩, ⟨TopSet (ndx), \prod_{𝑡} (D \times \{TopOpen (R)\})⟩\})}$
18		ovex	$⊢ K^{D} \in V$
19		psrvalstr	$⊢ (\{⟨{Base}_{ndx}, K^{D}⟩, ⟨+_{ndx}, {\circ_{f} +_{R} ↾}_{((K^{D}) \times (K^{D}))}⟩, ⟨\cdot_{ndx}, (g \in (K^{D}), h \in (K^{D}) ⟼ (k \in D ⟼ \underset{x \in \{y \in D \| y \leq_{f} k\}}{\sum_{R}} (g (x) \cdot_{R} h (k -_{f} x))))⟩\} \cup \{⟨Scalar (ndx), R⟩, ⟨\cdot_{ndx}, (x \in K, g \in (K^{D}) ⟼ (D \times \{x\}) {\cdot_{R}}_{f} g)⟩, ⟨TopSet (ndx), \prod_{𝑡} (D \times \{TopOpen (R)\})⟩\}) Struct ⟨1, 9⟩$
20		baseid	$⊢ Base = Slot {Base}_{ndx}$
21		snsstp1	$⊢ \{⟨{Base}_{ndx}, K^{D}⟩\} \subseteq \{⟨{Base}_{ndx}, K^{D}⟩, ⟨+_{ndx}, {\circ_{f} +_{R} ↾}_{((K^{D}) \times (K^{D}))}⟩, ⟨\cdot_{ndx}, (g \in (K^{D}), h \in (K^{D}) ⟼ (k \in D ⟼ \underset{x \in \{y \in D \| y \leq_{f} k\}}{\sum_{R}} (g (x) \cdot_{R} h (k -_{f} x))))⟩\}$
22		ssun1	$⊢ \{⟨{Base}_{ndx}, K^{D}⟩, ⟨+_{ndx}, {\circ_{f} +_{R} ↾}_{((K^{D}) \times (K^{D}))}⟩, ⟨\cdot_{ndx}, (g \in (K^{D}), h \in (K^{D}) ⟼ (k \in D ⟼ \underset{x \in \{y \in D \| y \leq_{f} k\}}{\sum_{R}} (g (x) \cdot_{R} h (k -_{f} x))))⟩\} \subseteq \{⟨{Base}_{ndx}, K^{D}⟩, ⟨+_{ndx}, {\circ_{f} +_{R} ↾}_{((K^{D}) \times (K^{D}))}⟩, ⟨\cdot_{ndx}, (g \in (K^{D}), h \in (K^{D}) ⟼ (k \in D ⟼ \underset{x \in \{y \in D \| y \leq_{f} k\}}{\sum_{R}} (g (x) \cdot_{R} h (k -_{f} x))))⟩\} \cup \{⟨Scalar (ndx), R⟩, ⟨\cdot_{ndx}, (x \in K, g \in (K^{D}) ⟼ (D \times \{x\}) {\cdot_{R}}_{f} g)⟩, ⟨TopSet (ndx), \prod_{𝑡} (D \times \{TopOpen (R)\})⟩\}$
23	21 22	sstri	$⊢ \{⟨{Base}_{ndx}, K^{D}⟩\} \subseteq \{⟨{Base}_{ndx}, K^{D}⟩, ⟨+_{ndx}, {\circ_{f} +_{R} ↾}_{((K^{D}) \times (K^{D}))}⟩, ⟨\cdot_{ndx}, (g \in (K^{D}), h \in (K^{D}) ⟼ (k \in D ⟼ \underset{x \in \{y \in D \| y \leq_{f} k\}}{\sum_{R}} (g (x) \cdot_{R} h (k -_{f} x))))⟩\} \cup \{⟨Scalar (ndx), R⟩, ⟨\cdot_{ndx}, (x \in K, g \in (K^{D}) ⟼ (D \times \{x\}) {\cdot_{R}}_{f} g)⟩, ⟨TopSet (ndx), \prod_{𝑡} (D \times \{TopOpen (R)\})⟩\}$
24	19 20 23	strfv	$⊢ K^{D} \in V \to K^{D} = {Base}_{(\{⟨{Base}_{ndx}, K^{D}⟩, ⟨+_{ndx}, {\circ_{f} +_{R} ↾}_{((K^{D}) \times (K^{D}))}⟩, ⟨\cdot_{ndx}, (g \in (K^{D}), h \in (K^{D}) ⟼ (k \in D ⟼ \underset{x \in \{y \in D \| y \leq_{f} k\}}{\sum_{R}} (g (x) \cdot_{R} h (k -_{f} x))))⟩\} \cup \{⟨Scalar (ndx), R⟩, ⟨\cdot_{ndx}, (x \in K, g \in (K^{D}) ⟼ (D \times \{x\}) {\cdot_{R}}_{f} g)⟩, ⟨TopSet (ndx), \prod_{𝑡} (D \times \{TopOpen (R)\})⟩\})}$
25	18 24	ax-mp	$⊢ K^{D} = {Base}_{(\{⟨{Base}_{ndx}, K^{D}⟩, ⟨+_{ndx}, {\circ_{f} +_{R} ↾}_{((K^{D}) \times (K^{D}))}⟩, ⟨\cdot_{ndx}, (g \in (K^{D}), h \in (K^{D}) ⟼ (k \in D ⟼ \underset{x \in \{y \in D \| y \leq_{f} k\}}{\sum_{R}} (g (x) \cdot_{R} h (k -_{f} x))))⟩\} \cup \{⟨Scalar (ndx), R⟩, ⟨\cdot_{ndx}, (x \in K, g \in (K^{D}) ⟼ (D \times \{x\}) {\cdot_{R}}_{f} g)⟩, ⟨TopSet (ndx), \prod_{𝑡} (D \times \{TopOpen (R)\})⟩\})}$
26	17 4 25	3eqtr4g	$⊢ (φ \land R \in V) \to B = K^{D}$
27		reldmpsr	$⊢ Rel dom mPwSer$
28	27	ovprc2	$⊢ \neg R \in V \to I mPwSer R = \emptyset$
29	28	adantl	$⊢ (φ \land \neg R \in V) \to I mPwSer R = \emptyset$
30	1 29	syl5eq	$⊢ (φ \land \neg R \in V) \to S = \emptyset$
31	30	fveq2d	$⊢ (φ \land \neg R \in V) \to {Base}_{S} = {Base}_{\emptyset}$
32		base0	$⊢ \emptyset = {Base}_{\emptyset}$
33	31 4 32	3eqtr4g	$⊢ (φ \land \neg R \in V) \to B = \emptyset$
34		fvprc	$⊢ \neg R \in V \to {Base}_{R} = \emptyset$
35	34	adantl	$⊢ (φ \land \neg R \in V) \to {Base}_{R} = \emptyset$
36	2 35	syl5eq	$⊢ (φ \land \neg R \in V) \to K = \emptyset$
37	3	fczpsrbag	$⊢ I \in V \to (x \in I ⟼ 0) \in D$
38	5 37	syl	$⊢ φ \to (x \in I ⟼ 0) \in D$
39	38	adantr	$⊢ (φ \land \neg R \in V) \to (x \in I ⟼ 0) \in D$
40	39	ne0d	$⊢ (φ \land \neg R \in V) \to D \neq \emptyset$
41	2	fvexi	$⊢ K \in V$
42		ovex	$⊢ {ℕ_{0}}^{I} \in V$
43	3 42	rabex2	$⊢ D \in V$
44	41 43	map0	$⊢ K^{D} = \emptyset \leftrightarrow (K = \emptyset \land D \neq \emptyset)$
45	36 40 44	sylanbrc	$⊢ (φ \land \neg R \in V) \to K^{D} = \emptyset$
46	33 45	eqtr4d	$⊢ (φ \land \neg R \in V) \to B = K^{D}$
47	26 46	pm2.61dan	$⊢ φ \to B = K^{D}$

Metamath Proof Explorer

Theorem psrbas

Proof