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\in {\mathbf{S}}_{\mathscr{H}}$$
Assertion	shs0i	$$⊢A{+}_{\mathscr{H}}{0}_{\mathscr{H}}=A$$

Proof

Step	Hyp	Ref	Expression
1		shne0.1	$$⊢A\in {\mathbf{S}}_{\mathscr{H}}$$
2		h0elsh	$$⊢0_{\mathscr{H}}\in {\mathbf{S}}_{\mathscr{H}}$$
3	1 2	shsval3i	$$⊢A{+}_{\mathscr{H}}{0}_{\mathscr{H}}=\mathrm{span}\left(A\cup 0_{\mathscr{H}}\right)$$
4		sh0le	$$⊢A\in {\mathbf{S}}_{\mathscr{H}}\to 0_{\mathscr{H}}\subseteq A$$
5	1 4	ax-mp	$$⊢0_{\mathscr{H}}\subseteq A$$
6		ssequn2	$$⊢0_{\mathscr{H}}\subseteq A\leftrightarrow A\cup 0_{\mathscr{H}}=A$$
7	5 6	mpbi	$$⊢A\cup 0_{\mathscr{H}}=A$$
8	7	fveq2i	$$⊢\mathrm{span}\left(A\cup 0_{\mathscr{H}}\right)=\mathrm{span}\left(A\right)$$
9		spanid	$$⊢A\in {\mathbf{S}}_{\mathscr{H}}\to \mathrm{span}\left(A\right)=A$$
10	1 9	ax-mp	$$⊢\mathrm{span}\left(A\right)=A$$
11	3 8 10	3eqtri	$$⊢A{+}_{\mathscr{H}}{0}_{\mathscr{H}}=A$$