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

Metamath Proof Explorer

Theorem djhsumss

Description: Subspace sum is a subset of subspace join. (Contributed by NM, 6-Aug-2014)

Ref Expression
Hypotheses djhsumss.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
djhsumss.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
djhsumss.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
djhsumss.p ⊢ ⊕ = ( LSSum ‘ 𝑈 )
djhsumss.j ⊢ ∨ = ( ( joinH ‘ 𝐾 ) ‘ 𝑊 )
djhsumss.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
djhsumss.x ⊢ ( 𝜑 → 𝑋 ⊆ 𝑉 )
djhsumss.y ⊢ ( 𝜑 → 𝑌 ⊆ 𝑉 )
Assertion djhsumss ( 𝜑 → ( 𝑋 ⊕ 𝑌 ) ⊆ ( 𝑋 ∨ 𝑌 ) )

Proof

Step Hyp Ref Expression
1 djhsumss.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 djhsumss.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
3 djhsumss.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
4 djhsumss.p ⊢ ⊕ = ( LSSum ‘ 𝑈 )
5 djhsumss.j ⊢ ∨ = ( ( joinH ‘ 𝐾 ) ‘ 𝑊 )
6 djhsumss.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
7 djhsumss.x ⊢ ( 𝜑 → 𝑋 ⊆ 𝑉 )
8 djhsumss.y ⊢ ( 𝜑 → 𝑌 ⊆ 𝑉 )
9 eqid ⊢ ( LSpan ‘ 𝑈 ) = ( LSpan ‘ 𝑈 )
10 1 2 6 dvhlmod ⊢ ( 𝜑 → 𝑈 ∈ LMod )
11 3 9 4 7 8 10 lsmssspx ⊢ ( 𝜑 → ( 𝑋 ⊕ 𝑌 ) ⊆ ( ( LSpan ‘ 𝑈 ) ‘ ( 𝑋 ∪ 𝑌 ) ) )
12 1 2 3 9 5 6 7 8 djhspss ⊢ ( 𝜑 → ( ( LSpan ‘ 𝑈 ) ‘ ( 𝑋 ∪ 𝑌 ) ) ⊆ ( 𝑋 ∨ 𝑌 ) )
13 11 12 sstrd ⊢ ( 𝜑 → ( 𝑋 ⊕ 𝑌 ) ⊆ ( 𝑋 ∨ 𝑌 ) )