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	⊢ 𝐴 ∈ Sℋ
Assertion	shs0i	⊢ ( 𝐴 +ℋ 0ℋ ) = 𝐴

Proof

Step	Hyp	Ref	Expression
1		shne0.1	⊢ 𝐴 ∈ Sℋ
2		h0elsh	⊢ 0ℋ ∈ Sℋ
3	1 2	shsval3i	⊢ ( 𝐴 +ℋ 0ℋ ) = ( span ‘ ( 𝐴 ∪ 0ℋ ) )
4		sh0le	⊢ ( 𝐴 ∈ Sℋ → 0ℋ ⊆ 𝐴 )
5	1 4	ax-mp	⊢ 0ℋ ⊆ 𝐴
6		ssequn2	⊢ ( 0ℋ ⊆ 𝐴 ↔ ( 𝐴 ∪ 0ℋ ) = 𝐴 )
7	5 6	mpbi	⊢ ( 𝐴 ∪ 0ℋ ) = 𝐴
8	7	fveq2i	⊢ ( span ‘ ( 𝐴 ∪ 0ℋ ) ) = ( span ‘ 𝐴 )
9		spanid	⊢ ( 𝐴 ∈ Sℋ → ( span ‘ 𝐴 ) = 𝐴 )
10	1 9	ax-mp	⊢ ( span ‘ 𝐴 ) = 𝐴
11	3 8 10	3eqtri	⊢ ( 𝐴 +ℋ 0ℋ ) = 𝐴