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 S
shs00.2 B S
Assertion shs00i A = 0 B = 0 A + B = 0

Proof

Step Hyp Ref Expression
1 shne0.1 A S
2 shs00.2 B S
3 oveq12 A = 0 B = 0 A + B = 0 + 0
4 h0elsh 0 S
5 4 shs0i 0 + 0 = 0
6 3 5 eqtrdi A = 0 B = 0 A + B = 0
7 1 2 shsub1i A A + B
8 sseq2 A + B = 0 A A + B A 0
9 7 8 mpbii A + B = 0 A 0
10 shle0 A S A 0 A = 0
11 1 10 ax-mp A 0 A = 0
12 9 11 sylib A + B = 0 A = 0
13 2 1 shsub2i B A + B
14 sseq2 A + B = 0 B A + B B 0
15 13 14 mpbii A + B = 0 B 0
16 shle0 B S B 0 B = 0
17 2 16 ax-mp B 0 B = 0
18 15 17 sylib A + B = 0 B = 0
19 12 18 jca A + B = 0 A = 0 B = 0
20 6 19 impbii A = 0 B = 0 A + B = 0