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 )