Metamath Proof Explorer

Theorem shsleji

Description: Subspace sum is smaller than Hilbert lattice join. Remark in Kalmbach p. 65. (Contributed by NM, 19-Oct-1999) (Revised by Mario Carneiro, 15-May-2014) (New usage is discouraged.)

Ref Expression
Hypotheses shincl.1 ⊢ A ∈ S ℋ
shincl.2 ⊢ B ∈ S ℋ
Assertion shsleji ⊢ A + ℋ B ⊆ A ∨ ℋ B

Proof

Step Hyp Ref Expression
1 shincl.1 ⊢ A ∈ S ℋ
2 shincl.2 ⊢ B ∈ S ℋ
3 1 2 shseli ⊢ x ∈ A + ℋ B ↔ ∃ y ∈ A ∃ z ∈ B x = y + ℎ z
4 ssun1 ⊢ A ⊆ A ∪ B
5 1 2 shunssji ⊢ A ∪ B ⊆ A ∨ ℋ B
6 4 5 sstri ⊢ A ⊆ A ∨ ℋ B
7 6 sseli ⊢ y ∈ A → y ∈ A ∨ ℋ B
8 ssun2 ⊢ B ⊆ A ∪ B
9 8 5 sstri ⊢ B ⊆ A ∨ ℋ B
10 9 sseli ⊢ z ∈ B → z ∈ A ∨ ℋ B
11 shjcl ⊢ A ∈ S ℋ ∧ B ∈ S ℋ → A ∨ ℋ B ∈ C ℋ
12 1 2 11 mp2an ⊢ A ∨ ℋ B ∈ C ℋ
13 12 chshii ⊢ A ∨ ℋ B ∈ S ℋ
14 shaddcl ⊢ A ∨ ℋ B ∈ S ℋ ∧ y ∈ A ∨ ℋ B ∧ z ∈ A ∨ ℋ B → y + ℎ z ∈ A ∨ ℋ B
15 13 14 mp3an1 ⊢ y ∈ A ∨ ℋ B ∧ z ∈ A ∨ ℋ B → y + ℎ z ∈ A ∨ ℋ B
16 7 10 15 syl2an ⊢ y ∈ A ∧ z ∈ B → y + ℎ z ∈ A ∨ ℋ B
17 eleq1a ⊢ y + ℎ z ∈ A ∨ ℋ B → x = y + ℎ z → x ∈ A ∨ ℋ B
18 16 17 syl ⊢ y ∈ A ∧ z ∈ B → x = y + ℎ z → x ∈ A ∨ ℋ B
19 18 rexlimivv ⊢ ∃ y ∈ A ∃ z ∈ B x = y + ℎ z → x ∈ A ∨ ℋ B
20 3 19 sylbi ⊢ x ∈ A + ℋ B → x ∈ A ∨ ℋ B
21 20 ssriv ⊢ A + ℋ B ⊆ A ∨ ℋ B