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 )