This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )