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 ( 𝐴 + 𝐵 ) ⊆ ( 𝐴 𝐵 )