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 
|- A e. SH
shs00.2 
|- B e. SH
Assertion shs00i 
|- ( ( A = 0H /\ B = 0H ) <-> ( A +H B ) = 0H )

Proof

Step Hyp Ref Expression
1 shne0.1 
 |-  A e. SH
2 shs00.2 
 |-  B e. SH
3 oveq12 
 |-  ( ( A = 0H /\ B = 0H ) -> ( A +H B ) = ( 0H +H 0H ) )
4 h0elsh 
 |-  0H e. SH
5 4 shs0i 
 |-  ( 0H +H 0H ) = 0H
6 3 5 eqtrdi 
 |-  ( ( A = 0H /\ B = 0H ) -> ( A +H B ) = 0H )
7 1 2 shsub1i 
 |-  A C_ ( A +H B )
8 sseq2 
 |-  ( ( A +H B ) = 0H -> ( A C_ ( A +H B ) <-> A C_ 0H ) )
9 7 8 mpbii 
 |-  ( ( A +H B ) = 0H -> A C_ 0H )
10 shle0 
 |-  ( A e. SH -> ( A C_ 0H <-> A = 0H ) )
11 1 10 ax-mp 
 |-  ( A C_ 0H <-> A = 0H )
12 9 11 sylib 
 |-  ( ( A +H B ) = 0H -> A = 0H )
13 2 1 shsub2i 
 |-  B C_ ( A +H B )
14 sseq2 
 |-  ( ( A +H B ) = 0H -> ( B C_ ( A +H B ) <-> B C_ 0H ) )
15 13 14 mpbii 
 |-  ( ( A +H B ) = 0H -> B C_ 0H )
16 shle0 
 |-  ( B e. SH -> ( B C_ 0H <-> B = 0H ) )
17 2 16 ax-mp 
 |-  ( B C_ 0H <-> B = 0H )
18 15 17 sylib 
 |-  ( ( A +H B ) = 0H -> B = 0H )
19 12 18 jca 
 |-  ( ( A +H B ) = 0H -> ( A = 0H /\ B = 0H ) )
20 6 19 impbii 
 |-  ( ( A = 0H /\ B = 0H ) <-> ( A +H B ) = 0H )