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

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 ⊢ 𝐴 ∈ Sℋ
shincl.2 ⊢ 𝐵 ∈ Sℋ
Assertion shsleji ( 𝐴 +ℋ 𝐵 ) ⊆ ( 𝐴 ∨ℋ 𝐵 )

Proof

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