Theorem djhspss

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

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

Proof

Step	Hyp	Ref	Expression
1		djhspss.h	|- H = ( LHyp ` K )
2		djhspss.u	|- U = ( ( DVecH ` K ) ` W )
3		djhspss.v	|- V = ( Base ` U )
4		djhspss.n	|- N = ( LSpan ` U )
5		djhspss.j	|- .\/ = ( ( joinH ` K ) ` W )
6		djhspss.k	|- ( ph -> ( K e. HL /\ W e. H ) )
7		djhspss.x	|- ( ph -> X C_ V )
8		djhspss.y	|- ( ph -> Y C_ V )
9		eqid	|- ( ( ocH ` K ) ` W ) = ( ( ocH ` K ) ` W )
10	7 8	unssd	|- ( ph -> ( X u. Y ) C_ V )
11	1 2 9 3 4 6 10	dochspss	|- ( ph -> ( N ` ( X u. Y ) ) C_ ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( X u. Y ) ) ) )
12	1 2 3 9 5	djhval2	|- ( ( ( K e. HL /\ W e. H ) /\ X C_ V /\ Y C_ V ) -> ( X .\/ Y ) = ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( X u. Y ) ) ) )
13	6 7 8 12	syl3anc	|- ( ph -> ( X .\/ Y ) = ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( X u. Y ) ) ) )
14	11 13	sseqtrrd	|- ( ph -> ( N ` ( X u. Y ) ) C_ ( X .\/ Y ) )