Theorem djhsumss

Description: Subspace sum is a subset of subspace join. (Contributed by NM, 6-Aug-2014)

	Ref	Expression
Hypotheses	djhsumss.h	|- H = ( LHyp ` K )
	djhsumss.u	|- U = ( ( DVecH ` K ) ` W )
	djhsumss.v	|- V = ( Base ` U )
	djhsumss.p	|- .(+) = ( LSSum ` U )
	djhsumss.j	|- .\/ = ( ( joinH ` K ) ` W )
	djhsumss.k	|- ( ph -> ( K e. HL /\ W e. H ) )
	djhsumss.x	|- ( ph -> X C_ V )
	djhsumss.y	|- ( ph -> Y C_ V )
Assertion	djhsumss	|- ( ph -> ( X .(+) Y ) C_ ( X .\/ Y ) )

Proof

Step	Hyp	Ref	Expression
1		djhsumss.h	|- H = ( LHyp ` K )
2		djhsumss.u	|- U = ( ( DVecH ` K ) ` W )
3		djhsumss.v	|- V = ( Base ` U )
4		djhsumss.p	|- .(+) = ( LSSum ` U )
5		djhsumss.j	|- .\/ = ( ( joinH ` K ) ` W )
6		djhsumss.k	|- ( ph -> ( K e. HL /\ W e. H ) )
7		djhsumss.x	|- ( ph -> X C_ V )
8		djhsumss.y	|- ( ph -> Y C_ V )
9		eqid	|- ( LSpan ` U ) = ( LSpan ` U )
10	1 2 6	dvhlmod	|- ( ph -> U e. LMod )
11	3 9 4 7 8 10	lsmssspx	|- ( ph -> ( X .(+) Y ) C_ ( ( LSpan ` U ) ` ( X u. Y ) ) )
12	1 2 3 9 5 6 7 8	djhspss	|- ( ph -> ( ( LSpan ` U ) ` ( X u. Y ) ) C_ ( X .\/ Y ) )
13	11 12	sstrd	|- ( ph -> ( X .(+) Y ) C_ ( X .\/ Y ) )