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

Metamath Proof Explorer

Theorem shsleji

Description: Subspace sum is smaller than Hilbert lattice join. Remark in Kalmbach p. 65. (Contributed by NM, 19-Oct-1999) (Revised by Mario Carneiro, 15-May-2014) (New usage is discouraged.)

Ref Expression
Hypotheses shincl.1 
|- A e. SH
shincl.2 
|- B e. SH
Assertion shsleji 
|- ( A +H B ) C_ ( A vH B )

Proof

Step Hyp Ref Expression
1 shincl.1 
 |-  A e. SH
2 shincl.2 
 |-  B e. SH
3 1 2 shseli 
 |-  ( x e. ( A +H B ) <-> E. y e. A E. z e. B x = ( y +h z ) )
4 ssun1 
 |-  A C_ ( A u. B )
5 1 2 shunssji 
 |-  ( A u. B ) C_ ( A vH B )
6 4 5 sstri 
 |-  A C_ ( A vH B )
7 6 sseli 
 |-  ( y e. A -> y e. ( A vH B ) )
8 ssun2 
 |-  B C_ ( A u. B )
9 8 5 sstri 
 |-  B C_ ( A vH B )
10 9 sseli 
 |-  ( z e. B -> z e. ( A vH B ) )
11 shjcl 
 |-  ( ( A e. SH /\ B e. SH ) -> ( A vH B ) e. CH )
12 1 2 11 mp2an 
 |-  ( A vH B ) e. CH
13 12 chshii 
 |-  ( A vH B ) e. SH
14 shaddcl 
 |-  ( ( ( A vH B ) e. SH /\ y e. ( A vH B ) /\ z e. ( A vH B ) ) -> ( y +h z ) e. ( A vH B ) )
15 13 14 mp3an1 
 |-  ( ( y e. ( A vH B ) /\ z e. ( A vH B ) ) -> ( y +h z ) e. ( A vH B ) )
16 7 10 15 syl2an 
 |-  ( ( y e. A /\ z e. B ) -> ( y +h z ) e. ( A vH B ) )
17 eleq1a 
 |-  ( ( y +h z ) e. ( A vH B ) -> ( x = ( y +h z ) -> x e. ( A vH B ) ) )
18 16 17 syl 
 |-  ( ( y e. A /\ z e. B ) -> ( x = ( y +h z ) -> x e. ( A vH B ) ) )
19 18 rexlimivv 
 |-  ( E. y e. A E. z e. B x = ( y +h z ) -> x e. ( A vH B ) )
20 3 19 sylbi 
 |-  ( x e. ( A +H B ) -> x e. ( A vH B ) )
21 20 ssriv 
 |-  ( A +H B ) C_ ( A vH B )