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

Metamath Proof Explorer

Theorem shjshseli

Description: A closed subspace sum equals Hilbert lattice join. Part of Lemma 31.1.5 of MaedaMaeda p. 136. (Contributed by NM, 30-Nov-2004) (New usage is discouraged.)

Ref Expression
Hypotheses shjshs.1 
|- A e. SH
shjshs.2 
|- B e. SH
Assertion shjshseli 
|- ( ( A +H B ) e. CH <-> ( A +H B ) = ( A vH B ) )

Proof

Step Hyp Ref Expression
1 shjshs.1 
 |-  A e. SH
2 shjshs.2 
 |-  B e. SH
3 1 2 shjshsi 
 |-  ( A vH B ) = ( _|_ ` ( _|_ ` ( A +H B ) ) )
4 ococ 
 |-  ( ( A +H B ) e. CH -> ( _|_ ` ( _|_ ` ( A +H B ) ) ) = ( A +H B ) )
5 3 4 eqtr2id 
 |-  ( ( A +H B ) e. CH -> ( A +H B ) = ( A vH B ) )
6 1 2 shjcli 
 |-  ( A vH B ) e. CH
7 eleq1 
 |-  ( ( A +H B ) = ( A vH B ) -> ( ( A +H B ) e. CH <-> ( A vH B ) e. CH ) )
8 6 7 mpbiri 
 |-  ( ( A +H B ) = ( A vH B ) -> ( A +H B ) e. CH )
9 5 8 impbii 
 |-  ( ( A +H B ) e. CH <-> ( A +H B ) = ( A vH B ) )