Theorem shs00i

Description: Two subspaces are zero iff their join is zero. (Contributed by NM, 7-Aug-2004) (New usage is discouraged.)

	Ref	Expression
Hypotheses	shne0.1	$$⊢A\in {\mathbf{S}}_{\mathscr{H}}$$
	shs00.2	$$⊢B\in {\mathbf{S}}_{\mathscr{H}}$$
Assertion	shs00i	$$⊢\left(A=0_{\mathscr{H}}\wedge B=0_{\mathscr{H}}\right)\leftrightarrow A{+}_{\mathscr{H}}B=0_{\mathscr{H}}$$

Proof

Step	Hyp	Ref	Expression
1		shne0.1	$$⊢A\in {\mathbf{S}}_{\mathscr{H}}$$
2		shs00.2	$$⊢B\in {\mathbf{S}}_{\mathscr{H}}$$
3		oveq12	$$⊢\left(A=0_{\mathscr{H}}\wedge B=0_{\mathscr{H}}\right)\to A{+}_{\mathscr{H}}B=0_{\mathscr{H}}{+}_{\mathscr{H}}{0}_{\mathscr{H}}$$
4		h0elsh	$$⊢0_{\mathscr{H}}\in {\mathbf{S}}_{\mathscr{H}}$$
5	4	shs0i	$$⊢0_{\mathscr{H}}{+}_{\mathscr{H}}{0}_{\mathscr{H}}=0_{\mathscr{H}}$$
6	3 5	eqtrdi	$$⊢\left(A=0_{\mathscr{H}}\wedge B=0_{\mathscr{H}}\right)\to A{+}_{\mathscr{H}}B=0_{\mathscr{H}}$$
7	1 2	shsub1i	$$⊢A\subseteq A{+}_{\mathscr{H}}B$$
8		sseq2	$$⊢A{+}_{\mathscr{H}}B=0_{\mathscr{H}}\to \left(A\subseteq A{+}_{\mathscr{H}}B\leftrightarrow A\subseteq 0_{\mathscr{H}}\right)$$
9	7 8	mpbii	$$⊢A{+}_{\mathscr{H}}B=0_{\mathscr{H}}\to A\subseteq 0_{\mathscr{H}}$$
10		shle0	$$⊢A\in {\mathbf{S}}_{\mathscr{H}}\to \left(A\subseteq 0_{\mathscr{H}}\leftrightarrow A=0_{\mathscr{H}}\right)$$
11	1 10	ax-mp	$$⊢A\subseteq 0_{\mathscr{H}}\leftrightarrow A=0_{\mathscr{H}}$$
12	9 11	sylib	$$⊢A{+}_{\mathscr{H}}B=0_{\mathscr{H}}\to A=0_{\mathscr{H}}$$
13	2 1	shsub2i	$$⊢B\subseteq A{+}_{\mathscr{H}}B$$
14		sseq2	$$⊢A{+}_{\mathscr{H}}B=0_{\mathscr{H}}\to \left(B\subseteq A{+}_{\mathscr{H}}B\leftrightarrow B\subseteq 0_{\mathscr{H}}\right)$$
15	13 14	mpbii	$$⊢A{+}_{\mathscr{H}}B=0_{\mathscr{H}}\to B\subseteq 0_{\mathscr{H}}$$
16		shle0	$$⊢B\in {\mathbf{S}}_{\mathscr{H}}\to \left(B\subseteq 0_{\mathscr{H}}\leftrightarrow B=0_{\mathscr{H}}\right)$$
17	2 16	ax-mp	$$⊢B\subseteq 0_{\mathscr{H}}\leftrightarrow B=0_{\mathscr{H}}$$
18	15 17	sylib	$$⊢A{+}_{\mathscr{H}}B=0_{\mathscr{H}}\to B=0_{\mathscr{H}}$$
19	12 18	jca	$$⊢A{+}_{\mathscr{H}}B=0_{\mathscr{H}}\to \left(A=0_{\mathscr{H}}\wedge B=0_{\mathscr{H}}\right)$$
20	6 19	impbii	$$⊢\left(A=0_{\mathscr{H}}\wedge B=0_{\mathscr{H}}\right)\leftrightarrow A{+}_{\mathscr{H}}B=0_{\mathscr{H}}$$