This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶 ) ↔ ( 𝐴 +ℋ 𝐵 ) ⊆ 𝐶 )