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