psrvalstr

Description: The multivariate power series structure is a function. (Contributed by Mario Carneiro, 8-Feb-2015)

		Ref	Expression
	Assertion	psrvalstr	$⊢ (\{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, \underset{˙}{+}⟩, ⟨\cdot_{ndx}, \underset{˙}{\times}⟩\} \cup \{⟨Scalar (ndx), R⟩, ⟨\cdot_{ndx}, \underset{˙}{\cdot}⟩, ⟨TopSet (ndx), J⟩\}) Struct ⟨1, 9⟩$

Step	Hyp	Ref	Expression
1		eqid	$⊢ \{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, \underset{˙}{+}⟩, ⟨\cdot_{ndx}, \underset{˙}{\times}⟩\} = \{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, \underset{˙}{+}⟩, ⟨\cdot_{ndx}, \underset{˙}{\times}⟩\}$
2	1	rngstr	$⊢ \{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, \underset{˙}{+}⟩, ⟨\cdot_{ndx}, \underset{˙}{\times}⟩\} Struct ⟨1, 3⟩$
3		5nn	$⊢ 5 \in ℕ$
4		scandx	$⊢ Scalar (ndx) = 5$
5		5lt6	$⊢ 5 < 6$
6		6nn	$⊢ 6 \in ℕ$
7		vscandx	$⊢ \cdot_{ndx} = 6$
8		6lt9	$⊢ 6 < 9$
9		9nn	$⊢ 9 \in ℕ$
10		tsetndx	$⊢ TopSet (ndx) = 9$
11	3 4 5 6 7 8 9 10	strle3	$⊢ \{⟨Scalar (ndx), R⟩, ⟨\cdot_{ndx}, \underset{˙}{\cdot}⟩, ⟨TopSet (ndx), J⟩\} Struct ⟨5, 9⟩$
12		3lt5	$⊢ 3 < 5$
13	2 11 12	strleun	$⊢ (\{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, \underset{˙}{+}⟩, ⟨\cdot_{ndx}, \underset{˙}{\times}⟩\} \cup \{⟨Scalar (ndx), R⟩, ⟨\cdot_{ndx}, \underset{˙}{\cdot}⟩, ⟨TopSet (ndx), J⟩\}) Struct ⟨1, 9⟩$

Metamath Proof Explorer