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	⊢ ( 𝜑 → ( 𝑋 ⊕ 𝑌 ) ⊆ ( 𝑋 ∨ 𝑌 ) )