Metamath Proof Explorer

Theorem djhunssN

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

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

Proof

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