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 
|- V = ( Base ` W )
lspval.s 
|- S = ( LSubSp ` W )
lspval.n 
|- N = ( LSpan ` W )
lspprcl.w 
|- ( ph -> W e. LMod )
lspprcl.x 
|- ( ph -> X e. V )
lspprcl.y 
|- ( ph -> Y e. V )
lsptpcl.z 
|- ( ph -> Z e. V )
Assertion lsptpcl 
|- ( ph -> ( N ` { X , Y , Z } ) e. S )

Proof

Step Hyp Ref Expression
1 lspval.v 
 |-  V = ( Base ` W )
2 lspval.s 
 |-  S = ( LSubSp ` W )
3 lspval.n 
 |-  N = ( LSpan ` W )
4 lspprcl.w 
 |-  ( ph -> W e. LMod )
5 lspprcl.x 
 |-  ( ph -> X e. V )
6 lspprcl.y 
 |-  ( ph -> Y e. V )
7 lsptpcl.z 
 |-  ( ph -> Z e. V )
8 df-tp 
 |-  { X , Y , Z } = ( { X , Y } u. { Z } )
9 5 6 prssd 
 |-  ( ph -> { X , Y } C_ V )
10 7 snssd 
 |-  ( ph -> { Z } C_ V )
11 9 10 unssd 
 |-  ( ph -> ( { X , Y } u. { Z } ) C_ V )
12 8 11 eqsstrid 
 |-  ( ph -> { X , Y , Z } C_ V )
13 1 2 3 lspcl 
 |-  ( ( W e. LMod /\ { X , Y , Z } C_ V ) -> ( N ` { X , Y , Z } ) e. S )
14 4 12 13 syl2anc 
 |-  ( ph -> ( N ` { X , Y , Z } ) e. S )