Theorem shslubi

Description: The least upper bound law for Hilbert subspace sum. (Contributed by NM, 15-Jun-2004) (New usage is discouraged.)

	Ref	Expression
Hypotheses	shslub.1	|- A e. SH
	shslub.2	|- B e. SH
	shslub.3	|- C e. SH
Assertion	shslubi	|- ( ( A C_ C /\ B C_ C ) <-> ( A +H B ) C_ C )

Proof

Step	Hyp	Ref	Expression
1		shslub.1	|- A e. SH
2		shslub.2	|- B e. SH
3		shslub.3	|- C e. SH
4	1 3 2	shlessi	|- ( A C_ C -> ( A +H B ) C_ ( C +H B ) )
5	3 2	shscomi	|- ( C +H B ) = ( B +H C )
6	4 5	sseqtrdi	|- ( A C_ C -> ( A +H B ) C_ ( B +H C ) )
7	2 3 3	shlessi	|- ( B C_ C -> ( B +H C ) C_ ( C +H C ) )
8	3	shsidmi	|- ( C +H C ) = C
9	7 8	sseqtrdi	|- ( B C_ C -> ( B +H C ) C_ C )
10	6 9	sylan9ss	|- ( ( A C_ C /\ B C_ C ) -> ( A +H B ) C_ C )
11	1 2	shsub1i	|- A C_ ( A +H B )
12		sstr	|- ( ( A C_ ( A +H B ) /\ ( A +H B ) C_ C ) -> A C_ C )
13	11 12	mpan	|- ( ( A +H B ) C_ C -> A C_ C )
14	2 1	shsub2i	|- B C_ ( A +H B )
15		sstr	|- ( ( B C_ ( A +H B ) /\ ( A +H B ) C_ C ) -> B C_ C )
16	14 15	mpan	|- ( ( A +H B ) C_ C -> B C_ C )
17	13 16	jca	|- ( ( A +H B ) C_ C -> ( A C_ C /\ B C_ C ) )
18	10 17	impbii	|- ( ( A C_ C /\ B C_ C ) <-> ( A +H B ) C_ C )