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 e. SH
	shincl.2	|- B e. SH
Assertion	shsleji	|- ( A +H B ) C_ ( A vH B )

Proof

Step	Hyp	Ref	Expression
1		shincl.1	|- A e. SH
2		shincl.2	|- B e. SH
3	1 2	shseli	|- ( x e. ( A +H B ) <-> E. y e. A E. z e. B x = ( y +h z ) )
4		ssun1	|- A C_ ( A u. B )
5	1 2	shunssji	|- ( A u. B ) C_ ( A vH B )
6	4 5	sstri	|- A C_ ( A vH B )
7	6	sseli	|- ( y e. A -> y e. ( A vH B ) )
8		ssun2	|- B C_ ( A u. B )
9	8 5	sstri	|- B C_ ( A vH B )
10	9	sseli	|- ( z e. B -> z e. ( A vH B ) )
11		shjcl	|- ( ( A e. SH /\ B e. SH ) -> ( A vH B ) e. CH )
12	1 2 11	mp2an	|- ( A vH B ) e. CH
13	12	chshii	|- ( A vH B ) e. SH
14		shaddcl	|- ( ( ( A vH B ) e. SH /\ y e. ( A vH B ) /\ z e. ( A vH B ) ) -> ( y +h z ) e. ( A vH B ) )
15	13 14	mp3an1	|- ( ( y e. ( A vH B ) /\ z e. ( A vH B ) ) -> ( y +h z ) e. ( A vH B ) )
16	7 10 15	syl2an	|- ( ( y e. A /\ z e. B ) -> ( y +h z ) e. ( A vH B ) )
17		eleq1a	|- ( ( y +h z ) e. ( A vH B ) -> ( x = ( y +h z ) -> x e. ( A vH B ) ) )
18	16 17	syl	|- ( ( y e. A /\ z e. B ) -> ( x = ( y +h z ) -> x e. ( A vH B ) ) )
19	18	rexlimivv	|- ( E. y e. A E. z e. B x = ( y +h z ) -> x e. ( A vH B ) )
20	3 19	sylbi	|- ( x e. ( A +H B ) -> x e. ( A vH B ) )
21	20	ssriv	|- ( A +H B ) C_ ( A vH B )