Metamath Proof Explorer


Theorem shs0i

Description: Hilbert subspace sum with the zero subspace. (Contributed by NM, 14-Jan-2005) (New usage is discouraged.)

Ref Expression
Hypothesis shne0.1 A S
Assertion shs0i A + 0 = A

Proof

Step Hyp Ref Expression
1 shne0.1 A S
2 h0elsh 0 S
3 1 2 shsval3i A + 0 = span A 0
4 sh0le A S 0 A
5 1 4 ax-mp 0 A
6 ssequn2 0 A A 0 = A
7 5 6 mpbi A 0 = A
8 7 fveq2i span A 0 = span A
9 spanid A S span A = A
10 1 9 ax-mp span A = A
11 3 8 10 3eqtri A + 0 = A