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 e. SH
Assertion	shs0i	|- ( A +H 0H ) = A

Proof

Step	Hyp	Ref	Expression
1		shne0.1	|- A e. SH
2		h0elsh	|- 0H e. SH
3	1 2	shsval3i	|- ( A +H 0H ) = ( span ` ( A u. 0H ) )
4		sh0le	|- ( A e. SH -> 0H C_ A )
5	1 4	ax-mp	|- 0H C_ A
6		ssequn2	|- ( 0H C_ A <-> ( A u. 0H ) = A )
7	5 6	mpbi	|- ( A u. 0H ) = A
8	7	fveq2i	|- ( span ` ( A u. 0H ) ) = ( span ` A )
9		spanid	|- ( A e. SH -> ( span ` A ) = A )
10	1 9	ax-mp	|- ( span ` A ) = A
11	3 8 10	3eqtri	|- ( A +H 0H ) = A