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

Metamath Proof Explorer

Theorem lsptpcl

Description: The span of an unordered triple is a subspace (frequently used special case of lspcl ). (Contributed by NM, 22-May-2015)

Ref Expression
Hypotheses lspval.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
lspval.s ⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
lspval.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
lspprcl.w ⊢ ( 𝜑 → 𝑊 ∈ LMod )
lspprcl.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
lspprcl.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
lsptpcl.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑉 )
Assertion lsptpcl ( 𝜑 → ( 𝑁 ‘ { 𝑋 , 𝑌 , 𝑍 } ) ∈ 𝑆 )

Proof

Step Hyp Ref Expression
1 lspval.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 lspval.s ⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
3 lspval.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
4 lspprcl.w ⊢ ( 𝜑 → 𝑊 ∈ LMod )
5 lspprcl.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
6 lspprcl.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
7 lsptpcl.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑉 )
8 df-tp ⊢ { 𝑋 , 𝑌 , 𝑍 } = ( { 𝑋 , 𝑌 } ∪ { 𝑍 } )
9 5 6 prssd ⊢ ( 𝜑 → { 𝑋 , 𝑌 } ⊆ 𝑉 )
10 7 snssd ⊢ ( 𝜑 → { 𝑍 } ⊆ 𝑉 )
11 9 10 unssd ⊢ ( 𝜑 → ( { 𝑋 , 𝑌 } ∪ { 𝑍 } ) ⊆ 𝑉 )
12 8 11 eqsstrid ⊢ ( 𝜑 → { 𝑋 , 𝑌 , 𝑍 } ⊆ 𝑉 )
13 1 2 3 lspcl ⊢ ( ( 𝑊 ∈ LMod ∧ { 𝑋 , 𝑌 , 𝑍 } ⊆ 𝑉 ) → ( 𝑁 ‘ { 𝑋 , 𝑌 , 𝑍 } ) ∈ 𝑆 )
14 4 12 13 syl2anc ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 , 𝑌 , 𝑍 } ) ∈ 𝑆 )