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	⊢ 𝐴 ∈ Sℋ
	shs00.2	⊢ 𝐵 ∈ Sℋ
Assertion	shs00i	⊢ ( ( 𝐴 = 0ℋ ∧ 𝐵 = 0ℋ ) ↔ ( 𝐴 +ℋ 𝐵 ) = 0ℋ )

Proof

Step	Hyp	Ref	Expression
1		shne0.1	⊢ 𝐴 ∈ Sℋ
2		shs00.2	⊢ 𝐵 ∈ Sℋ
3		oveq12	⊢ ( ( 𝐴 = 0ℋ ∧ 𝐵 = 0ℋ ) → ( 𝐴 +ℋ 𝐵 ) = ( 0ℋ +ℋ 0ℋ ) )
4		h0elsh	⊢ 0ℋ ∈ Sℋ
5	4	shs0i	⊢ ( 0ℋ +ℋ 0ℋ ) = 0ℋ
6	3 5	eqtrdi	⊢ ( ( 𝐴 = 0ℋ ∧ 𝐵 = 0ℋ ) → ( 𝐴 +ℋ 𝐵 ) = 0ℋ )
7	1 2	shsub1i	⊢ 𝐴 ⊆ ( 𝐴 +ℋ 𝐵 )
8		sseq2	⊢ ( ( 𝐴 +ℋ 𝐵 ) = 0ℋ → ( 𝐴 ⊆ ( 𝐴 +ℋ 𝐵 ) ↔ 𝐴 ⊆ 0ℋ ) )
9	7 8	mpbii	⊢ ( ( 𝐴 +ℋ 𝐵 ) = 0ℋ → 𝐴 ⊆ 0ℋ )
10		shle0	⊢ ( 𝐴 ∈ Sℋ → ( 𝐴 ⊆ 0ℋ ↔ 𝐴 = 0ℋ ) )
11	1 10	ax-mp	⊢ ( 𝐴 ⊆ 0ℋ ↔ 𝐴 = 0ℋ )
12	9 11	sylib	⊢ ( ( 𝐴 +ℋ 𝐵 ) = 0ℋ → 𝐴 = 0ℋ )
13	2 1	shsub2i	⊢ 𝐵 ⊆ ( 𝐴 +ℋ 𝐵 )
14		sseq2	⊢ ( ( 𝐴 +ℋ 𝐵 ) = 0ℋ → ( 𝐵 ⊆ ( 𝐴 +ℋ 𝐵 ) ↔ 𝐵 ⊆ 0ℋ ) )
15	13 14	mpbii	⊢ ( ( 𝐴 +ℋ 𝐵 ) = 0ℋ → 𝐵 ⊆ 0ℋ )
16		shle0	⊢ ( 𝐵 ∈ Sℋ → ( 𝐵 ⊆ 0ℋ ↔ 𝐵 = 0ℋ ) )
17	2 16	ax-mp	⊢ ( 𝐵 ⊆ 0ℋ ↔ 𝐵 = 0ℋ )
18	15 17	sylib	⊢ ( ( 𝐴 +ℋ 𝐵 ) = 0ℋ → 𝐵 = 0ℋ )
19	12 18	jca	⊢ ( ( 𝐴 +ℋ 𝐵 ) = 0ℋ → ( 𝐴 = 0ℋ ∧ 𝐵 = 0ℋ ) )
20	6 19	impbii	⊢ ( ( 𝐴 = 0ℋ ∧ 𝐵 = 0ℋ ) ↔ ( 𝐴 +ℋ 𝐵 ) = 0ℋ )