Metamath Proof Explorer

Theorem djhunssN

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

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

Proof

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