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