Metamath Proof Explorer


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=LHypK
djhspss.u U=DVecHKW
djhspss.v V=BaseU
djhspss.n N=LSpanU
djhspss.j ˙=joinHKW
djhspss.k φKHLWH
djhspss.x φXV
djhspss.y φYV
Assertion djhspss φNXYX˙Y

Proof

Step Hyp Ref Expression
1 djhspss.h H=LHypK
2 djhspss.u U=DVecHKW
3 djhspss.v V=BaseU
4 djhspss.n N=LSpanU
5 djhspss.j ˙=joinHKW
6 djhspss.k φKHLWH
7 djhspss.x φXV
8 djhspss.y φYV
9 eqid ocHKW=ocHKW
10 7 8 unssd φXYV
11 1 2 9 3 4 6 10 dochspss φNXYocHKWocHKWXY
12 1 2 3 9 5 djhval2 KHLWHXVYVX˙Y=ocHKWocHKWXY
13 6 7 8 12 syl3anc φX˙Y=ocHKWocHKWXY
14 11 13 sseqtrrd φNXYX˙Y