Description: Hilbert subspace sum with the zero subspace. (Contributed by NM, 14-Jan-2005) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypothesis | shne0.1 | ||
Assertion | shs0i |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | shne0.1 | ||
2 | h0elsh | ||
3 | 1 2 | shsval3i | |
4 | sh0le | ||
5 | 1 4 | ax-mp | |
6 | ssequn2 | ||
7 | 5 6 | mpbi | |
8 | 7 | fveq2i | |
9 | spanid | ||
10 | 1 9 | ax-mp | |
11 | 3 8 10 | 3eqtri |