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

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