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

Metamath Proof Explorer

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 ∈ S ℋ
shlesb1.2 ⊢ B ∈ S ℋ
Assertion shlesb1i ⊢ A ⊆ B ↔ A + ℋ B = B

Proof

Step Hyp Ref Expression
1 shlesb1.1 ⊢ A ∈ S ℋ
2 shlesb1.2 ⊢ B ∈ S ℋ
3 ssid ⊢ B ⊆ B
4 3 biantrur ⊢ A ⊆ B ↔ B ⊆ B ∧ A ⊆ B
5 2 1 2 shslubi ⊢ B ⊆ B ∧ A ⊆ B ↔ B + ℋ A ⊆ B
6 2 1 shsub2i ⊢ B ⊆ A + ℋ B
7 eqss ⊢ A + ℋ B = B ↔ A + ℋ B ⊆ B ∧ B ⊆ A + ℋ B
8 6 7 mpbiran2 ⊢ A + ℋ B = B ↔ A + ℋ B ⊆ B
9 1 2 shscomi ⊢ A + ℋ B = B + ℋ A
10 9 sseq1i ⊢ A + ℋ B ⊆ B ↔ B + ℋ A ⊆ B
11 8 10 bitr2i ⊢ B + ℋ A ⊆ B ↔ A + ℋ B = B
12 4 5 11 3bitri ⊢ A ⊆ B ↔ A + ℋ B = B