This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	lmodstr.w	$⊢ W = \{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, \underset{˙}{+}⟩, ⟨Scalar (ndx), F⟩\} \cup \{⟨\cdot_{ndx}, \underset{˙}{\cdot}⟩\}$
	Assertion	lmodstr	$⊢ W Struct ⟨1, 6⟩$

Proof

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