This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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ℋ )