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

Metamath Proof Explorer

Theorem shslubi

Description: The least upper bound law for Hilbert subspace sum. (Contributed by NM, 15-Jun-2004) (New usage is discouraged.)

Ref Expression
Hypotheses shslub.1 
|- A e. SH
shslub.2 
|- B e. SH
shslub.3 
|- C e. SH
Assertion shslubi 
|- ( ( A C_ C /\ B C_ C ) <-> ( A +H B ) C_ C )

Proof

Step Hyp Ref Expression
1 shslub.1 
 |-  A e. SH
2 shslub.2 
 |-  B e. SH
3 shslub.3 
 |-  C e. SH
4 1 3 2 shlessi 
 |-  ( A C_ C -> ( A +H B ) C_ ( C +H B ) )
5 3 2 shscomi 
 |-  ( C +H B ) = ( B +H C )
6 4 5 sseqtrdi 
 |-  ( A C_ C -> ( A +H B ) C_ ( B +H C ) )
7 2 3 3 shlessi 
 |-  ( B C_ C -> ( B +H C ) C_ ( C +H C ) )
8 3 shsidmi 
 |-  ( C +H C ) = C
9 7 8 sseqtrdi 
 |-  ( B C_ C -> ( B +H C ) C_ C )
10 6 9 sylan9ss 
 |-  ( ( A C_ C /\ B C_ C ) -> ( A +H B ) C_ C )
11 1 2 shsub1i 
 |-  A C_ ( A +H B )
12 sstr 
 |-  ( ( A C_ ( A +H B ) /\ ( A +H B ) C_ C ) -> A C_ C )
13 11 12 mpan 
 |-  ( ( A +H B ) C_ C -> A C_ C )
14 2 1 shsub2i 
 |-  B C_ ( A +H B )
15 sstr 
 |-  ( ( B C_ ( A +H B ) /\ ( A +H B ) C_ C ) -> B C_ C )
16 14 15 mpan 
 |-  ( ( A +H B ) C_ C -> B C_ C )
17 13 16 jca 
 |-  ( ( A +H B ) C_ C -> ( A C_ C /\ B C_ C ) )
18 10 17 impbii 
 |-  ( ( A C_ C /\ B C_ C ) <-> ( A +H B ) C_ C )