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

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 = LHyp ⁡ K
djhspss.u ⊢ U = DVecH ⁡ K ⁡ W
djhspss.v ⊢ V = Base U
djhspss.n ⊢ N = LSpan ⁡ U
djhspss.j ⊢ ∨ ˙ = joinH ⁡ K ⁡ W
djhspss.k ⊢ φ → K ∈ HL ∧ W ∈ H
djhspss.x ⊢ φ → X ⊆ V
djhspss.y ⊢ φ → Y ⊆ V
Assertion djhspss ⊢ φ → N ⁡ X ∪ Y ⊆ X ∨ ˙ Y

Proof

Step Hyp Ref Expression
1 djhspss.h ⊢ H = LHyp ⁡ K
2 djhspss.u ⊢ U = DVecH ⁡ K ⁡ W
3 djhspss.v ⊢ V = Base U
4 djhspss.n ⊢ N = LSpan ⁡ U
5 djhspss.j ⊢ ∨ ˙ = joinH ⁡ K ⁡ W
6 djhspss.k ⊢ φ → K ∈ HL ∧ W ∈ H
7 djhspss.x ⊢ φ → X ⊆ V
8 djhspss.y ⊢ φ → Y ⊆ V
9 eqid ⊢ ocH ⁡ K ⁡ W = ocH ⁡ K ⁡ W
10 7 8 unssd ⊢ φ → X ∪ Y ⊆ V
11 1 2 9 3 4 6 10 dochspss ⊢ φ → N ⁡ X ∪ Y ⊆ ocH ⁡ K ⁡ W ⁡ ocH ⁡ K ⁡ W ⁡ X ∪ Y
12 1 2 3 9 5 djhval2 ⊢ K ∈ HL ∧ W ∈ H ∧ X ⊆ V ∧ Y ⊆ V → X ∨ ˙ Y = ocH ⁡ K ⁡ W ⁡ ocH ⁡ K ⁡ W ⁡ X ∪ Y
13 6 7 8 12 syl3anc ⊢ φ → X ∨ ˙ Y = ocH ⁡ K ⁡ W ⁡ ocH ⁡ K ⁡ W ⁡ X ∪ Y
14 11 13 sseqtrrd ⊢ φ → N ⁡ X ∪ Y ⊆ X ∨ ˙ Y