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