Description: The subspace sum is a subset of Hilbert space. (Contributed by Mario Carneiro, 23-Dec-2013) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Assertion | shsss | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | shsval | |
|
2 | imassrn | |
|
3 | ax-hfvadd | |
|
4 | frn | |
|
5 | 3 4 | ax-mp | |
6 | 2 5 | sstri | |
7 | 1 6 | eqsstrdi | |