Step |
Hyp |
Ref |
Expression |
1 |
|
phlfn.h |
โข ๐ป = ( { โจ ( Base โ ndx ) , ๐ต โฉ , โจ ( +g โ ndx ) , + โฉ , โจ ( Scalar โ ndx ) , ๐ โฉ } โช { โจ ( ยท๐ โ ndx ) , ยท โฉ , โจ ( ยท๐ โ ndx ) , , โฉ } ) |
2 |
1
|
phlstr |
โข ๐ป Struct โจ 1 , 8 โฉ |
3 |
|
plusgid |
โข +g = Slot ( +g โ ndx ) |
4 |
|
snsstp2 |
โข { โจ ( +g โ ndx ) , + โฉ } โ { โจ ( Base โ ndx ) , ๐ต โฉ , โจ ( +g โ ndx ) , + โฉ , โจ ( Scalar โ ndx ) , ๐ โฉ } |
5 |
|
ssun1 |
โข { โจ ( Base โ ndx ) , ๐ต โฉ , โจ ( +g โ ndx ) , + โฉ , โจ ( Scalar โ ndx ) , ๐ โฉ } โ ( { โจ ( Base โ ndx ) , ๐ต โฉ , โจ ( +g โ ndx ) , + โฉ , โจ ( Scalar โ ndx ) , ๐ โฉ } โช { โจ ( ยท๐ โ ndx ) , ยท โฉ , โจ ( ยท๐ โ ndx ) , , โฉ } ) |
6 |
5 1
|
sseqtrri |
โข { โจ ( Base โ ndx ) , ๐ต โฉ , โจ ( +g โ ndx ) , + โฉ , โจ ( Scalar โ ndx ) , ๐ โฉ } โ ๐ป |
7 |
4 6
|
sstri |
โข { โจ ( +g โ ndx ) , + โฉ } โ ๐ป |
8 |
2 3 7
|
strfv |
โข ( + โ ๐ โ + = ( +g โ ๐ป ) ) |