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	⊢ 𝐴 ∈ Sℋ
	shslub.2	⊢ 𝐵 ∈ Sℋ
	shslub.3	⊢ 𝐶 ∈ Sℋ
Assertion	shslubi	⊢ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶 ) ↔ ( 𝐴 +ℋ 𝐵 ) ⊆ 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		shslub.1	⊢ 𝐴 ∈ Sℋ
2		shslub.2	⊢ 𝐵 ∈ Sℋ
3		shslub.3	⊢ 𝐶 ∈ Sℋ
4	1 3 2	shlessi	⊢ ( 𝐴 ⊆ 𝐶 → ( 𝐴 +ℋ 𝐵 ) ⊆ ( 𝐶 +ℋ 𝐵 ) )
5	3 2	shscomi	⊢ ( 𝐶 +ℋ 𝐵 ) = ( 𝐵 +ℋ 𝐶 )
6	4 5	sseqtrdi	⊢ ( 𝐴 ⊆ 𝐶 → ( 𝐴 +ℋ 𝐵 ) ⊆ ( 𝐵 +ℋ 𝐶 ) )
7	2 3 3	shlessi	⊢ ( 𝐵 ⊆ 𝐶 → ( 𝐵 +ℋ 𝐶 ) ⊆ ( 𝐶 +ℋ 𝐶 ) )
8	3	shsidmi	⊢ ( 𝐶 +ℋ 𝐶 ) = 𝐶
9	7 8	sseqtrdi	⊢ ( 𝐵 ⊆ 𝐶 → ( 𝐵 +ℋ 𝐶 ) ⊆ 𝐶 )
10	6 9	sylan9ss	⊢ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶 ) → ( 𝐴 +ℋ 𝐵 ) ⊆ 𝐶 )
11	1 2	shsub1i	⊢ 𝐴 ⊆ ( 𝐴 +ℋ 𝐵 )
12		sstr	⊢ ( ( 𝐴 ⊆ ( 𝐴 +ℋ 𝐵 ) ∧ ( 𝐴 +ℋ 𝐵 ) ⊆ 𝐶 ) → 𝐴 ⊆ 𝐶 )
13	11 12	mpan	⊢ ( ( 𝐴 +ℋ 𝐵 ) ⊆ 𝐶 → 𝐴 ⊆ 𝐶 )
14	2 1	shsub2i	⊢ 𝐵 ⊆ ( 𝐴 +ℋ 𝐵 )
15		sstr	⊢ ( ( 𝐵 ⊆ ( 𝐴 +ℋ 𝐵 ) ∧ ( 𝐴 +ℋ 𝐵 ) ⊆ 𝐶 ) → 𝐵 ⊆ 𝐶 )
16	14 15	mpan	⊢ ( ( 𝐴 +ℋ 𝐵 ) ⊆ 𝐶 → 𝐵 ⊆ 𝐶 )
17	13 16	jca	⊢ ( ( 𝐴 +ℋ 𝐵 ) ⊆ 𝐶 → ( 𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶 ) )
18	10 17	impbii	⊢ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶 ) ↔ ( 𝐴 +ℋ 𝐵 ) ⊆ 𝐶 )