Metamath Proof Explorer

Theorem lsatfixedN

Description: Show equality with the span of the sum of two vectors, one of which ( X ) is fixed in advance. Compare lspfixed . (Contributed by NM, 29-May-2015) (New usage is discouraged.)

Ref Expression
Hypotheses lsatfixed.v 
|- V = ( Base ` W )
lsatfixed.p 
|- .+ = ( +g ` W )
lsatfixed.o 
|- .0. = ( 0g ` W )
lsatfixed.n 
|- N = ( LSpan ` W )
lsatfixed.a 
|- A = ( LSAtoms ` W )
lsatfixed.w 
|- ( ph -> W e. LVec )
lsatfixed.q 
|- ( ph -> Q e. A )
lsatfixed.x 
|- ( ph -> X e. V )
lsatfixed.y 
|- ( ph -> Y e. V )
lsatfixed.e 
|- ( ph -> Q =/= ( N ` { X } ) )
lsatfixed.f 
|- ( ph -> Q =/= ( N ` { Y } ) )
lsatfixed.g 
|- ( ph -> Q C_ ( N ` { X , Y } ) )
Assertion lsatfixedN 
|- ( ph -> E. z e. ( ( N ` { Y } ) \ { .0. } ) Q = ( N ` { ( X .+ z ) } ) )

Proof

Step Hyp Ref Expression
1 lsatfixed.v 
 |-  V = ( Base ` W )
2 lsatfixed.p 
 |-  .+ = ( +g ` W )
3 lsatfixed.o 
 |-  .0. = ( 0g ` W )
4 lsatfixed.n 
 |-  N = ( LSpan ` W )
5 lsatfixed.a 
 |-  A = ( LSAtoms ` W )
6 lsatfixed.w 
 |-  ( ph -> W e. LVec )
7 lsatfixed.q 
 |-  ( ph -> Q e. A )
8 lsatfixed.x 
 |-  ( ph -> X e. V )
9 lsatfixed.y 
 |-  ( ph -> Y e. V )
10 lsatfixed.e 
 |-  ( ph -> Q =/= ( N ` { X } ) )
11 lsatfixed.f 
 |-  ( ph -> Q =/= ( N ` { Y } ) )
12 lsatfixed.g 
 |-  ( ph -> Q C_ ( N ` { X , Y } ) )
13 1 4 3 5 islsat 
 |-  ( W e. LVec -> ( Q e. A <-> E. w e. ( V \ { .0. } ) Q = ( N ` { w } ) ) )
14 6 13 syl 
 |-  ( ph -> ( Q e. A <-> E. w e. ( V \ { .0. } ) Q = ( N ` { w } ) ) )
15 7 14 mpbid 
 |-  ( ph -> E. w e. ( V \ { .0. } ) Q = ( N ` { w } ) )
16 6 3ad2ant1 
 |-  ( ( ph /\ w e. ( V \ { .0. } ) /\ Q = ( N ` { w } ) ) -> W e. LVec )
17 8 3ad2ant1 
 |-  ( ( ph /\ w e. ( V \ { .0. } ) /\ Q = ( N ` { w } ) ) -> X e. V )
18 9 3ad2ant1 
 |-  ( ( ph /\ w e. ( V \ { .0. } ) /\ Q = ( N ` { w } ) ) -> Y e. V )
19 simp2 
 |-  ( ( ph /\ w e. ( V \ { .0. } ) /\ Q = ( N ` { w } ) ) -> w e. ( V \ { .0. } ) )
20 simp3 
 |-  ( ( ph /\ w e. ( V \ { .0. } ) /\ Q = ( N ` { w } ) ) -> Q = ( N ` { w } ) )
21 20 eqcomd 
 |-  ( ( ph /\ w e. ( V \ { .0. } ) /\ Q = ( N ` { w } ) ) -> ( N ` { w } ) = Q )
22 10 3ad2ant1 
 |-  ( ( ph /\ w e. ( V \ { .0. } ) /\ Q = ( N ` { w } ) ) -> Q =/= ( N ` { X } ) )
23 21 22 eqnetrd 
 |-  ( ( ph /\ w e. ( V \ { .0. } ) /\ Q = ( N ` { w } ) ) -> ( N ` { w } ) =/= ( N ` { X } ) )
24 1 3 4 16 19 17 23 lspsnne1 
 |-  ( ( ph /\ w e. ( V \ { .0. } ) /\ Q = ( N ` { w } ) ) -> -. w e. ( N ` { X } ) )
25 11 3ad2ant1 
 |-  ( ( ph /\ w e. ( V \ { .0. } ) /\ Q = ( N ` { w } ) ) -> Q =/= ( N ` { Y } ) )
26 21 25 eqnetrd 
 |-  ( ( ph /\ w e. ( V \ { .0. } ) /\ Q = ( N ` { w } ) ) -> ( N ` { w } ) =/= ( N ` { Y } ) )
27 1 3 4 16 19 18 26 lspsnne1 
 |-  ( ( ph /\ w e. ( V \ { .0. } ) /\ Q = ( N ` { w } ) ) -> -. w e. ( N ` { Y } ) )
28 12 3ad2ant1 
 |-  ( ( ph /\ w e. ( V \ { .0. } ) /\ Q = ( N ` { w } ) ) -> Q C_ ( N ` { X , Y } ) )
29 21 28 eqsstrd 
 |-  ( ( ph /\ w e. ( V \ { .0. } ) /\ Q = ( N ` { w } ) ) -> ( N ` { w } ) C_ ( N ` { X , Y } ) )
30 eqid 
 |-  ( LSubSp ` W ) = ( LSubSp ` W )
31 lveclmod 
 |-  ( W e. LVec -> W e. LMod )
32 6 31 syl 
 |-  ( ph -> W e. LMod )
33 32 3ad2ant1 
 |-  ( ( ph /\ w e. ( V \ { .0. } ) /\ Q = ( N ` { w } ) ) -> W e. LMod )
34 1 30 4 32 8 9 lspprcl 
 |-  ( ph -> ( N ` { X , Y } ) e. ( LSubSp ` W ) )
35 34 3ad2ant1 
 |-  ( ( ph /\ w e. ( V \ { .0. } ) /\ Q = ( N ` { w } ) ) -> ( N ` { X , Y } ) e. ( LSubSp ` W ) )
36 19 eldifad 
 |-  ( ( ph /\ w e. ( V \ { .0. } ) /\ Q = ( N ` { w } ) ) -> w e. V )
37 1 30 4 33 35 36 lspsnel5 
 |-  ( ( ph /\ w e. ( V \ { .0. } ) /\ Q = ( N ` { w } ) ) -> ( w e. ( N ` { X , Y } ) <-> ( N ` { w } ) C_ ( N ` { X , Y } ) ) )
38 29 37 mpbird 
 |-  ( ( ph /\ w e. ( V \ { .0. } ) /\ Q = ( N ` { w } ) ) -> w e. ( N ` { X , Y } ) )
39 1 2 3 4 16 17 18 24 27 38 lspfixed 
 |-  ( ( ph /\ w e. ( V \ { .0. } ) /\ Q = ( N ` { w } ) ) -> E. z e. ( ( N ` { Y } ) \ { .0. } ) w e. ( N ` { ( X .+ z ) } ) )
40 simpl1 
 |-  ( ( ( ph /\ w e. ( V \ { .0. } ) /\ Q = ( N ` { w } ) ) /\ z e. ( ( N ` { Y } ) \ { .0. } ) ) -> ph )
41 40 6 syl 
 |-  ( ( ( ph /\ w e. ( V \ { .0. } ) /\ Q = ( N ` { w } ) ) /\ z e. ( ( N ` { Y } ) \ { .0. } ) ) -> W e. LVec )
42 simpl2 
 |-  ( ( ( ph /\ w e. ( V \ { .0. } ) /\ Q = ( N ` { w } ) ) /\ z e. ( ( N ` { Y } ) \ { .0. } ) ) -> w e. ( V \ { .0. } ) )
43 40 32 syl 
 |-  ( ( ( ph /\ w e. ( V \ { .0. } ) /\ Q = ( N ` { w } ) ) /\ z e. ( ( N ` { Y } ) \ { .0. } ) ) -> W e. LMod )
44 40 8 syl 
 |-  ( ( ( ph /\ w e. ( V \ { .0. } ) /\ Q = ( N ` { w } ) ) /\ z e. ( ( N ` { Y } ) \ { .0. } ) ) -> X e. V )
45 9 snssd 
 |-  ( ph -> { Y } C_ V )
46 1 4 lspssv 
 |-  ( ( W e. LMod /\ { Y } C_ V ) -> ( N ` { Y } ) C_ V )
47 32 45 46 syl2anc 
 |-  ( ph -> ( N ` { Y } ) C_ V )
48 47 ssdifssd 
 |-  ( ph -> ( ( N ` { Y } ) \ { .0. } ) C_ V )
49 48 3ad2ant1 
 |-  ( ( ph /\ w e. ( V \ { .0. } ) /\ Q = ( N ` { w } ) ) -> ( ( N ` { Y } ) \ { .0. } ) C_ V )
50 49 sselda 
 |-  ( ( ( ph /\ w e. ( V \ { .0. } ) /\ Q = ( N ` { w } ) ) /\ z e. ( ( N ` { Y } ) \ { .0. } ) ) -> z e. V )
51 1 2 lmodvacl 
 |-  ( ( W e. LMod /\ X e. V /\ z e. V ) -> ( X .+ z ) e. V )
52 43 44 50 51 syl3anc 
 |-  ( ( ( ph /\ w e. ( V \ { .0. } ) /\ Q = ( N ` { w } ) ) /\ z e. ( ( N ` { Y } ) \ { .0. } ) ) -> ( X .+ z ) e. V )
53 1 3 4 41 42 52 lspsncmp 
 |-  ( ( ( ph /\ w e. ( V \ { .0. } ) /\ Q = ( N ` { w } ) ) /\ z e. ( ( N ` { Y } ) \ { .0. } ) ) -> ( ( N ` { w } ) C_ ( N ` { ( X .+ z ) } ) <-> ( N ` { w } ) = ( N ` { ( X .+ z ) } ) ) )
54 1 30 4 lspsncl 
 |-  ( ( W e. LMod /\ ( X .+ z ) e. V ) -> ( N ` { ( X .+ z ) } ) e. ( LSubSp ` W ) )
55 43 52 54 syl2anc 
 |-  ( ( ( ph /\ w e. ( V \ { .0. } ) /\ Q = ( N ` { w } ) ) /\ z e. ( ( N ` { Y } ) \ { .0. } ) ) -> ( N ` { ( X .+ z ) } ) e. ( LSubSp ` W ) )
56 42 eldifad 
 |-  ( ( ( ph /\ w e. ( V \ { .0. } ) /\ Q = ( N ` { w } ) ) /\ z e. ( ( N ` { Y } ) \ { .0. } ) ) -> w e. V )
57 1 30 4 43 55 56 lspsnel5 
 |-  ( ( ( ph /\ w e. ( V \ { .0. } ) /\ Q = ( N ` { w } ) ) /\ z e. ( ( N ` { Y } ) \ { .0. } ) ) -> ( w e. ( N ` { ( X .+ z ) } ) <-> ( N ` { w } ) C_ ( N ` { ( X .+ z ) } ) ) )
58 simpl3 
 |-  ( ( ( ph /\ w e. ( V \ { .0. } ) /\ Q = ( N ` { w } ) ) /\ z e. ( ( N ` { Y } ) \ { .0. } ) ) -> Q = ( N ` { w } ) )
59 58 eqeq1d 
 |-  ( ( ( ph /\ w e. ( V \ { .0. } ) /\ Q = ( N ` { w } ) ) /\ z e. ( ( N ` { Y } ) \ { .0. } ) ) -> ( Q = ( N ` { ( X .+ z ) } ) <-> ( N ` { w } ) = ( N ` { ( X .+ z ) } ) ) )
60 53 57 59 3bitr4rd 
 |-  ( ( ( ph /\ w e. ( V \ { .0. } ) /\ Q = ( N ` { w } ) ) /\ z e. ( ( N ` { Y } ) \ { .0. } ) ) -> ( Q = ( N ` { ( X .+ z ) } ) <-> w e. ( N ` { ( X .+ z ) } ) ) )
61 60 rexbidva 
 |-  ( ( ph /\ w e. ( V \ { .0. } ) /\ Q = ( N ` { w } ) ) -> ( E. z e. ( ( N ` { Y } ) \ { .0. } ) Q = ( N ` { ( X .+ z ) } ) <-> E. z e. ( ( N ` { Y } ) \ { .0. } ) w e. ( N ` { ( X .+ z ) } ) ) )
62 39 61 mpbird 
 |-  ( ( ph /\ w e. ( V \ { .0. } ) /\ Q = ( N ` { w } ) ) -> E. z e. ( ( N ` { Y } ) \ { .0. } ) Q = ( N ` { ( X .+ z ) } ) )
63 62 rexlimdv3a 
 |-  ( ph -> ( E. w e. ( V \ { .0. } ) Q = ( N ` { w } ) -> E. z e. ( ( N ` { Y } ) \ { .0. } ) Q = ( N ` { ( X .+ z ) } ) ) )
64 15 63 mpd 
 |-  ( ph -> E. z e. ( ( N ` { Y } ) \ { .0. } ) Q = ( N ` { ( X .+ z ) } ) )