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 ⊢ 𝐴 ∈ Sℋ
shlesb1.2 ⊢ 𝐵 ∈ Sℋ
Assertion shlesb1i ( 𝐴 ⊆ 𝐵 ↔ ( 𝐴 +ℋ 𝐵 ) = 𝐵 )

Proof

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