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 ) )