Theorem lmodstr

Description: A constructed left module or left vector space is a structure. (Contributed by Mario Carneiro, 1-Oct-2013) (Revised by Mario Carneiro, 29-Aug-2015)

	Ref	Expression
Hypothesis	lvecfn.w	$$⊢W=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{+}⟩,⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),F⟩\right\}\cup \left\{⟨{\cdot }_{\mathrm{ndx}},\underset{\dot{}}{·}⟩\right\}$$
Assertion	lmodstr	$$⊢W\mathrm{Struct}⟨1,6⟩$$

Proof

Step	Hyp	Ref	Expression
1		lvecfn.w	$$⊢W=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{+}⟩,⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),F⟩\right\}\cup \left\{⟨{\cdot }_{\mathrm{ndx}},\underset{\dot{}}{·}⟩\right\}$$
2		1nn	$$⊢1\in \mathbb{N}$$
3		basendx	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}=1$$
4		1lt2	$$⊢1<2$$
5		2nn	$$⊢2\in \mathbb{N}$$
6		plusgndx	$$⊢{+}_{\mathrm{ndx}}=2$$
7		2lt5	$$⊢2<5$$
8		5nn	$$⊢5\in \mathbb{N}$$
9		scandx	$$⊢\mathrm{Scalar}\left(\mathrm{ndx}\right)=5$$
10	2 3 4 5 6 7 8 9	strle3	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{+}⟩,⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),F⟩\right\}\mathrm{Struct}⟨1,5⟩$$
11		6nn	$$⊢6\in \mathbb{N}$$
12		vscandx	$$⊢{\cdot }_{\mathrm{ndx}}=6$$
13	11 12	strle1	$$⊢\left\{⟨{\cdot }_{\mathrm{ndx}},\underset{\dot{}}{·}⟩\right\}\mathrm{Struct}⟨6,6⟩$$
14		5lt6	$$⊢5<6$$
15	10 13 14	strleun	$$⊢\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{+}⟩,⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),F⟩\right\}\cup \left\{⟨{\cdot }_{\mathrm{ndx}},\underset{\dot{}}{·}⟩\right\}\right)\mathrm{Struct}⟨1,6⟩$$
16	1 15	eqbrtri	$$⊢W\mathrm{Struct}⟨1,6⟩$$