Metamath Proof Explorer

Theorem lspindpi

Description: Partial independence property. (Contributed by NM, 23-Apr-2015)

Ref Expression
Hypotheses lspindpi.v 
|- V = ( Base ` W )
lspindpi.n 
|- N = ( LSpan ` W )
lspindpi.w 
|- ( ph -> W e. LVec )
lspindpi.x 
|- ( ph -> X e. V )
lspindpi.y 
|- ( ph -> Y e. V )
lspindpi.z 
|- ( ph -> Z e. V )
lspindpi.e 
|- ( ph -> -. X e. ( N ` { Y , Z } ) )
Assertion lspindpi 
|- ( ph -> ( ( N ` { X } ) =/= ( N ` { Y } ) /\ ( N ` { X } ) =/= ( N ` { Z } ) ) )

Proof

Step Hyp Ref Expression
1 lspindpi.v 
 |-  V = ( Base ` W )
2 lspindpi.n 
 |-  N = ( LSpan ` W )
3 lspindpi.w 
 |-  ( ph -> W e. LVec )
4 lspindpi.x 
 |-  ( ph -> X e. V )
5 lspindpi.y 
 |-  ( ph -> Y e. V )
6 lspindpi.z 
 |-  ( ph -> Z e. V )
7 lspindpi.e 
 |-  ( ph -> -. X e. ( N ` { Y , Z } ) )
8 lveclmod 
 |-  ( W e. LVec -> W e. LMod )
9 3 8 syl 
 |-  ( ph -> W e. LMod )
10 eqid 
 |-  ( LSubSp ` W ) = ( LSubSp ` W )
11 10 lsssssubg 
 |-  ( W e. LMod -> ( LSubSp ` W ) C_ ( SubGrp ` W ) )
12 9 11 syl 
 |-  ( ph -> ( LSubSp ` W ) C_ ( SubGrp ` W ) )
13 1 10 2 lspsncl 
 |-  ( ( W e. LMod /\ Y e. V ) -> ( N ` { Y } ) e. ( LSubSp ` W ) )
14 9 5 13 syl2anc 
 |-  ( ph -> ( N ` { Y } ) e. ( LSubSp ` W ) )
15 12 14 sseldd 
 |-  ( ph -> ( N ` { Y } ) e. ( SubGrp ` W ) )
16 1 10 2 lspsncl 
 |-  ( ( W e. LMod /\ Z e. V ) -> ( N ` { Z } ) e. ( LSubSp ` W ) )
17 9 6 16 syl2anc 
 |-  ( ph -> ( N ` { Z } ) e. ( LSubSp ` W ) )
18 12 17 sseldd 
 |-  ( ph -> ( N ` { Z } ) e. ( SubGrp ` W ) )
19 eqid 
 |-  ( LSSum ` W ) = ( LSSum ` W )
20 19 lsmub1 
 |-  ( ( ( N ` { Y } ) e. ( SubGrp ` W ) /\ ( N ` { Z } ) e. ( SubGrp ` W ) ) -> ( N ` { Y } ) C_ ( ( N ` { Y } ) ( LSSum ` W ) ( N ` { Z } ) ) )
21 15 18 20 syl2anc 
 |-  ( ph -> ( N ` { Y } ) C_ ( ( N ` { Y } ) ( LSSum ` W ) ( N ` { Z } ) ) )
22 1 2 19 9 5 6 lsmpr 
 |-  ( ph -> ( N ` { Y , Z } ) = ( ( N ` { Y } ) ( LSSum ` W ) ( N ` { Z } ) ) )
23 21 22 sseqtrrd 
 |-  ( ph -> ( N ` { Y } ) C_ ( N ` { Y , Z } ) )
24 sseq1 
 |-  ( ( N ` { X } ) = ( N ` { Y } ) -> ( ( N ` { X } ) C_ ( N ` { Y , Z } ) <-> ( N ` { Y } ) C_ ( N ` { Y , Z } ) ) )
25 23 24 syl5ibrcom 
 |-  ( ph -> ( ( N ` { X } ) = ( N ` { Y } ) -> ( N ` { X } ) C_ ( N ` { Y , Z } ) ) )
26 1 10 2 9 5 6 lspprcl 
 |-  ( ph -> ( N ` { Y , Z } ) e. ( LSubSp ` W ) )
27 1 10 2 9 26 4 ellspsn5b 
 |-  ( ph -> ( X e. ( N ` { Y , Z } ) <-> ( N ` { X } ) C_ ( N ` { Y , Z } ) ) )
28 25 27 sylibrd 
 |-  ( ph -> ( ( N ` { X } ) = ( N ` { Y } ) -> X e. ( N ` { Y , Z } ) ) )
29 28 necon3bd 
 |-  ( ph -> ( -. X e. ( N ` { Y , Z } ) -> ( N ` { X } ) =/= ( N ` { Y } ) ) )
30 7 29 mpd 
 |-  ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )
31 19 lsmub2 
 |-  ( ( ( N ` { Y } ) e. ( SubGrp ` W ) /\ ( N ` { Z } ) e. ( SubGrp ` W ) ) -> ( N ` { Z } ) C_ ( ( N ` { Y } ) ( LSSum ` W ) ( N ` { Z } ) ) )
32 15 18 31 syl2anc 
 |-  ( ph -> ( N ` { Z } ) C_ ( ( N ` { Y } ) ( LSSum ` W ) ( N ` { Z } ) ) )
33 32 22 sseqtrrd 
 |-  ( ph -> ( N ` { Z } ) C_ ( N ` { Y , Z } ) )
34 sseq1 
 |-  ( ( N ` { X } ) = ( N ` { Z } ) -> ( ( N ` { X } ) C_ ( N ` { Y , Z } ) <-> ( N ` { Z } ) C_ ( N ` { Y , Z } ) ) )
35 33 34 syl5ibrcom 
 |-  ( ph -> ( ( N ` { X } ) = ( N ` { Z } ) -> ( N ` { X } ) C_ ( N ` { Y , Z } ) ) )
36 35 27 sylibrd 
 |-  ( ph -> ( ( N ` { X } ) = ( N ` { Z } ) -> X e. ( N ` { Y , Z } ) ) )
37 36 necon3bd 
 |-  ( ph -> ( -. X e. ( N ` { Y , Z } ) -> ( N ` { X } ) =/= ( N ` { Z } ) ) )
38 7 37 mpd 
 |-  ( ph -> ( N ` { X } ) =/= ( N ` { Z } ) )
39 30 38 jca 
 |-  ( ph -> ( ( N ` { X } ) =/= ( N ` { Y } ) /\ ( N ` { X } ) =/= ( N ` { Z } ) ) )