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 ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
djhspss.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
djhspss.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
djhspss.n ⊢ 𝑁 = ( LSpan ‘ 𝑈 )
djhspss.j ⊢ ∨ = ( ( joinH ‘ 𝐾 ) ‘ 𝑊 )
djhspss.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
djhspss.x ⊢ ( 𝜑 → 𝑋 ⊆ 𝑉 )
djhspss.y ⊢ ( 𝜑 → 𝑌 ⊆ 𝑉 )
Assertion djhspss ( 𝜑 → ( 𝑁 ‘ ( 𝑋 ∪ 𝑌 ) ) ⊆ ( 𝑋 ∨ 𝑌 ) )

Proof

Step Hyp Ref Expression
1 djhspss.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 djhspss.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
3 djhspss.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
4 djhspss.n ⊢ 𝑁 = ( LSpan ‘ 𝑈 )
5 djhspss.j ⊢ ∨ = ( ( joinH ‘ 𝐾 ) ‘ 𝑊 )
6 djhspss.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
7 djhspss.x ⊢ ( 𝜑 → 𝑋 ⊆ 𝑉 )
8 djhspss.y ⊢ ( 𝜑 → 𝑌 ⊆ 𝑉 )
9 eqid ⊢ ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
10 7 8 unssd ⊢ ( 𝜑 → ( 𝑋 ∪ 𝑌 ) ⊆ 𝑉 )
11 1 2 9 3 4 6 10 dochspss ⊢ ( 𝜑 → ( 𝑁 ‘ ( 𝑋 ∪ 𝑌 ) ) ⊆ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑋 ∪ 𝑌 ) ) ) )
12 1 2 3 9 5 djhval2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ⊆ 𝑉 ∧ 𝑌 ⊆ 𝑉 ) → ( 𝑋 ∨ 𝑌 ) = ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑋 ∪ 𝑌 ) ) ) )
13 6 7 8 12 syl3anc ⊢ ( 𝜑 → ( 𝑋 ∨ 𝑌 ) = ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑋 ∪ 𝑌 ) ) ) )
14 11 13 sseqtrrd ⊢ ( 𝜑 → ( 𝑁 ‘ ( 𝑋 ∪ 𝑌 ) ) ⊆ ( 𝑋 ∨ 𝑌 ) )