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

Metamath Proof Explorer

Theorem shlesb1i

Description: Hilbert lattice ordering in terms of subspace sum. (Contributed by NM, 23-Nov-2004) (New usage is discouraged.)

Ref Expression
Hypotheses shlesb1.1 
|- A e. SH
shlesb1.2 
|- B e. SH
Assertion shlesb1i 
|- ( A C_ B <-> ( A +H B ) = B )

Proof

Step Hyp Ref Expression
1 shlesb1.1 
 |-  A e. SH
2 shlesb1.2 
 |-  B e. SH
3 ssid 
 |-  B C_ B
4 3 biantrur 
 |-  ( A C_ B <-> ( B C_ B /\ A C_ B ) )
5 2 1 2 shslubi 
 |-  ( ( B C_ B /\ A C_ B ) <-> ( B +H A ) C_ B )
6 2 1 shsub2i 
 |-  B C_ ( A +H B )
7 eqss 
 |-  ( ( A +H B ) = B <-> ( ( A +H B ) C_ B /\ B C_ ( A +H B ) ) )
8 6 7 mpbiran2 
 |-  ( ( A +H B ) = B <-> ( A +H B ) C_ B )
9 1 2 shscomi 
 |-  ( A +H B ) = ( B +H A )
10 9 sseq1i 
 |-  ( ( A +H B ) C_ B <-> ( B +H A ) C_ B )
11 8 10 bitr2i 
 |-  ( ( B +H A ) C_ B <-> ( A +H B ) = B )
12 4 5 11 3bitri 
 |-  ( A C_ B <-> ( A +H B ) = B )