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	⊢ 𝑊 = ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( Scalar ‘ ndx ) , 𝐹 ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , · ⟩ } )
Assertion	lmodstr	⊢ 𝑊 Struct ⟨ 1 , 6 ⟩

Proof

Step	Hyp	Ref	Expression
1		lvecfn.w	⊢ 𝑊 = ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( Scalar ‘ ndx ) , 𝐹 ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , · ⟩ } )
2		1nn	⊢ 1 ∈ ℕ
3		basendx	⊢ ( Base ‘ ndx ) = 1
4		1lt2	⊢ 1 < 2
5		2nn	⊢ 2 ∈ ℕ
6		plusgndx	⊢ ( +g ‘ ndx ) = 2
7		2lt5	⊢ 2 < 5
8		5nn	⊢ 5 ∈ ℕ
9		scandx	⊢ ( Scalar ‘ ndx ) = 5
10	2 3 4 5 6 7 8 9	strle3	⊢ { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( Scalar ‘ ndx ) , 𝐹 ⟩ } Struct ⟨ 1 , 5 ⟩
11		6nn	⊢ 6 ∈ ℕ
12		vscandx	⊢ ( ·𝑠 ‘ ndx ) = 6
13	11 12	strle1	⊢ { ⟨ ( ·𝑠 ‘ ndx ) , · ⟩ } Struct ⟨ 6 , 6 ⟩
14		5lt6	⊢ 5 < 6
15	10 13 14	strleun	⊢ ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( Scalar ‘ ndx ) , 𝐹 ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , · ⟩ } ) Struct ⟨ 1 , 6 ⟩
16	1 15	eqbrtri	⊢ 𝑊 Struct ⟨ 1 , 6 ⟩