Step |
Hyp |
Ref |
Expression |
1 |
|
algpart.a |
โข ๐ด = ( { โจ ( Base โ ndx ) , ๐ต โฉ , โจ ( +g โ ndx ) , + โฉ , โจ ( .r โ ndx ) , ร โฉ } โช { โจ ( Scalar โ ndx ) , ๐ โฉ , โจ ( ยท๐ โ ndx ) , ยท โฉ } ) |
2 |
1
|
algstr |
โข ๐ด Struct โจ 1 , 6 โฉ |
3 |
|
scaid |
โข Scalar = Slot ( Scalar โ ndx ) |
4 |
|
snsspr1 |
โข { โจ ( Scalar โ ndx ) , ๐ โฉ } โ { โจ ( Scalar โ ndx ) , ๐ โฉ , โจ ( ยท๐ โ ndx ) , ยท โฉ } |
5 |
|
ssun2 |
โข { โจ ( Scalar โ ndx ) , ๐ โฉ , โจ ( ยท๐ โ ndx ) , ยท โฉ } โ ( { โจ ( Base โ ndx ) , ๐ต โฉ , โจ ( +g โ ndx ) , + โฉ , โจ ( .r โ ndx ) , ร โฉ } โช { โจ ( Scalar โ ndx ) , ๐ โฉ , โจ ( ยท๐ โ ndx ) , ยท โฉ } ) |
6 |
5 1
|
sseqtrri |
โข { โจ ( Scalar โ ndx ) , ๐ โฉ , โจ ( ยท๐ โ ndx ) , ยท โฉ } โ ๐ด |
7 |
4 6
|
sstri |
โข { โจ ( Scalar โ ndx ) , ๐ โฉ } โ ๐ด |
8 |
2 3 7
|
strfv |
โข ( ๐ โ ๐ โ ๐ = ( Scalar โ ๐ด ) ) |