Step |
Hyp |
Ref |
Expression |
1 |
|
lmodstr.w |
|- W = ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( Scalar ` ndx ) , F >. } u. { <. ( .s ` ndx ) , .x. >. } ) |
2 |
1
|
lmodstr |
|- W Struct <. 1 , 6 >. |
3 |
|
baseid |
|- Base = Slot ( Base ` ndx ) |
4 |
|
snsstp1 |
|- { <. ( Base ` ndx ) , B >. } C_ { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( Scalar ` ndx ) , F >. } |
5 |
|
ssun1 |
|- { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( Scalar ` ndx ) , F >. } C_ ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( Scalar ` ndx ) , F >. } u. { <. ( .s ` ndx ) , .x. >. } ) |
6 |
5 1
|
sseqtrri |
|- { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( Scalar ` ndx ) , F >. } C_ W |
7 |
4 6
|
sstri |
|- { <. ( Base ` ndx ) , B >. } C_ W |
8 |
2 3 7
|
strfv |
|- ( B e. X -> B = ( Base ` W ) ) |