Theorem psrvalstr

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

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

Proof

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