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

Proof

Step Hyp Ref Expression
1 lmodstr.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 ⟩