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 φ K HL W H
djhunss.x φ X V
djhunss.y φ Y V
Assertion djhunssN φ X Y 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 φ K HL W H
6 djhunss.x φ X V
7 djhunss.y φ Y V
8 1 2 5 dvhlmod φ U LMod
9 6 7 unssd φ X Y V
10 eqid LSpan U = LSpan U
11 3 10 lspssid U LMod X Y V X Y LSpan U X Y
12 8 9 11 syl2anc φ X Y LSpan U X Y
13 1 2 3 10 4 5 6 7 djhspss φ LSpan U X Y X ˙ Y
14 12 13 sstrd φ X Y X ˙ Y