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