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 lvecfn.w 
|- W = ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( Scalar ` ndx ) , F >. } u. { <. ( .s ` ndx ) , .x. >. } )
Assertion lmodstr 
|- W Struct <. 1 , 6 >.

Proof

Step Hyp Ref Expression
1 lvecfn.w 
 |-  W = ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( Scalar ` ndx ) , F >. } u. { <. ( .s ` ndx ) , .x. >. } )
2 1nn 
 |-  1 e. NN
3 basendx 
 |-  ( Base ` ndx ) = 1
4 1lt2 
 |-  1 < 2
5 2nn 
 |-  2 e. NN
6 plusgndx 
 |-  ( +g ` ndx ) = 2
7 2lt5 
 |-  2 < 5
8 5nn 
 |-  5 e. NN
9 scandx 
 |-  ( Scalar ` ndx ) = 5
10 2 3 4 5 6 7 8 9 strle3 
 |-  { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( Scalar ` ndx ) , F >. } Struct <. 1 , 5 >.
11 6nn 
 |-  6 e. NN
12 vscandx 
 |-  ( .s ` ndx ) = 6
13 11 12 strle1 
 |-  { <. ( .s ` ndx ) , .x. >. } Struct <. 6 , 6 >.
14 5lt6 
 |-  5 < 6
15 10 13 14 strleun 
 |-  ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( Scalar ` ndx ) , F >. } u. { <. ( .s ` ndx ) , .x. >. } ) Struct <. 1 , 6 >.
16 1 15 eqbrtri 
 |-  W Struct <. 1 , 6 >.