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

Metamath Proof Explorer

Theorem lspfixed

Description: Show membership in the span of the sum of two vectors, one of which ( Y ) is fixed in advance. (Contributed by NM, 27-May-2015) (Revised by AV, 12-Jul-2022)

Ref Expression
Hypotheses lspfixed.v 
|- V = ( Base ` W )
lspfixed.p 
|- .+ = ( +g ` W )
lspfixed.o 
|- .0. = ( 0g ` W )
lspfixed.n 
|- N = ( LSpan ` W )
lspfixed.w 
|- ( ph -> W e. LVec )
lspfixed.y 
|- ( ph -> Y e. V )
lspfixed.z 
|- ( ph -> Z e. V )
lspfixed.e 
|- ( ph -> -. X e. ( N ` { Y } ) )
lspfixed.f 
|- ( ph -> -. X e. ( N ` { Z } ) )
lspfixed.g 
|- ( ph -> X e. ( N ` { Y , Z } ) )
Assertion lspfixed 
|- ( ph -> E. z e. ( ( N ` { Z } ) \ { .0. } ) X e. ( N ` { ( Y .+ z ) } ) )

Proof

Step Hyp Ref Expression
1 lspfixed.v 
 |-  V = ( Base ` W )
2 lspfixed.p 
 |-  .+ = ( +g ` W )
3 lspfixed.o 
 |-  .0. = ( 0g ` W )
4 lspfixed.n 
 |-  N = ( LSpan ` W )
5 lspfixed.w 
 |-  ( ph -> W e. LVec )
6 lspfixed.y 
 |-  ( ph -> Y e. V )
7 lspfixed.z 
 |-  ( ph -> Z e. V )
8 lspfixed.e 
 |-  ( ph -> -. X e. ( N ` { Y } ) )
9 lspfixed.f 
 |-  ( ph -> -. X e. ( N ` { Z } ) )
10 lspfixed.g 
 |-  ( ph -> X e. ( N ` { Y , Z } ) )
11 eqid 
 |-  ( Scalar ` W ) = ( Scalar ` W )
12 eqid 
 |-  ( Base ` ( Scalar ` W ) ) = ( Base ` ( Scalar ` W ) )
13 eqid 
 |-  ( .s ` W ) = ( .s ` W )
14 lveclmod 
 |-  ( W e. LVec -> W e. LMod )
15 5 14 syl 
 |-  ( ph -> W e. LMod )
16 1 2 11 12 13 4 15 6 7 lspprel 
 |-  ( ph -> ( X e. ( N ` { Y , Z } ) <-> E. k e. ( Base ` ( Scalar ` W ) ) E. l e. ( Base ` ( Scalar ` W ) ) X = ( ( k ( .s ` W ) Y ) .+ ( l ( .s ` W ) Z ) ) ) )
17 10 16 mpbid 
 |-  ( ph -> E. k e. ( Base ` ( Scalar ` W ) ) E. l e. ( Base ` ( Scalar ` W ) ) X = ( ( k ( .s ` W ) Y ) .+ ( l ( .s ` W ) Z ) ) )
18 15 3ad2ant1 
 |-  ( ( ph /\ ( k e. ( Base ` ( Scalar ` W ) ) /\ l e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( k ( .s ` W ) Y ) .+ ( l ( .s ` W ) Z ) ) ) -> W e. LMod )
19 eqid 
 |-  ( LSubSp ` W ) = ( LSubSp ` W )
20 1 19 4 lspsncl 
 |-  ( ( W e. LMod /\ Z e. V ) -> ( N ` { Z } ) e. ( LSubSp ` W ) )
21 15 7 20 syl2anc 
 |-  ( ph -> ( N ` { Z } ) e. ( LSubSp ` W ) )
22 21 3ad2ant1 
 |-  ( ( ph /\ ( k e. ( Base ` ( Scalar ` W ) ) /\ l e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( k ( .s ` W ) Y ) .+ ( l ( .s ` W ) Z ) ) ) -> ( N ` { Z } ) e. ( LSubSp ` W ) )
23 5 3ad2ant1 
 |-  ( ( ph /\ ( k e. ( Base ` ( Scalar ` W ) ) /\ l e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( k ( .s ` W ) Y ) .+ ( l ( .s ` W ) Z ) ) ) -> W e. LVec )
24 11 lvecdrng 
 |-  ( W e. LVec -> ( Scalar ` W ) e. DivRing )
25 23 24 syl 
 |-  ( ( ph /\ ( k e. ( Base ` ( Scalar ` W ) ) /\ l e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( k ( .s ` W ) Y ) .+ ( l ( .s ` W ) Z ) ) ) -> ( Scalar ` W ) e. DivRing )
26 simp2l 
 |-  ( ( ph /\ ( k e. ( Base ` ( Scalar ` W ) ) /\ l e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( k ( .s ` W ) Y ) .+ ( l ( .s ` W ) Z ) ) ) -> k e. ( Base ` ( Scalar ` W ) ) )
27 9 3ad2ant1 
 |-  ( ( ph /\ ( k e. ( Base ` ( Scalar ` W ) ) /\ l e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( k ( .s ` W ) Y ) .+ ( l ( .s ` W ) Z ) ) ) -> -. X e. ( N ` { Z } ) )
28 simpl3 
 |-  ( ( ( ph /\ ( k e. ( Base ` ( Scalar ` W ) ) /\ l e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( k ( .s ` W ) Y ) .+ ( l ( .s ` W ) Z ) ) ) /\ k = ( 0g ` ( Scalar ` W ) ) ) -> X = ( ( k ( .s ` W ) Y ) .+ ( l ( .s ` W ) Z ) ) )
29 simpr 
 |-  ( ( ( ph /\ ( k e. ( Base ` ( Scalar ` W ) ) /\ l e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( k ( .s ` W ) Y ) .+ ( l ( .s ` W ) Z ) ) ) /\ k = ( 0g ` ( Scalar ` W ) ) ) -> k = ( 0g ` ( Scalar ` W ) ) )
30 29 oveq1d 
 |-  ( ( ( ph /\ ( k e. ( Base ` ( Scalar ` W ) ) /\ l e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( k ( .s ` W ) Y ) .+ ( l ( .s ` W ) Z ) ) ) /\ k = ( 0g ` ( Scalar ` W ) ) ) -> ( k ( .s ` W ) Y ) = ( ( 0g ` ( Scalar ` W ) ) ( .s ` W ) Y ) )
31 simpl1 
 |-  ( ( ( ph /\ ( k e. ( Base ` ( Scalar ` W ) ) /\ l e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( k ( .s ` W ) Y ) .+ ( l ( .s ` W ) Z ) ) ) /\ k = ( 0g ` ( Scalar ` W ) ) ) -> ph )
32 31 15 syl 
 |-  ( ( ( ph /\ ( k e. ( Base ` ( Scalar ` W ) ) /\ l e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( k ( .s ` W ) Y ) .+ ( l ( .s ` W ) Z ) ) ) /\ k = ( 0g ` ( Scalar ` W ) ) ) -> W e. LMod )
33 31 6 syl 
 |-  ( ( ( ph /\ ( k e. ( Base ` ( Scalar ` W ) ) /\ l e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( k ( .s ` W ) Y ) .+ ( l ( .s ` W ) Z ) ) ) /\ k = ( 0g ` ( Scalar ` W ) ) ) -> Y e. V )
34 eqid 
 |-  ( 0g ` ( Scalar ` W ) ) = ( 0g ` ( Scalar ` W ) )
35 1 11 13 34 3 lmod0vs 
 |-  ( ( W e. LMod /\ Y e. V ) -> ( ( 0g ` ( Scalar ` W ) ) ( .s ` W ) Y ) = .0. )
36 32 33 35 syl2anc 
 |-  ( ( ( ph /\ ( k e. ( Base ` ( Scalar ` W ) ) /\ l e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( k ( .s ` W ) Y ) .+ ( l ( .s ` W ) Z ) ) ) /\ k = ( 0g ` ( Scalar ` W ) ) ) -> ( ( 0g ` ( Scalar ` W ) ) ( .s ` W ) Y ) = .0. )
37 30 36 eqtrd 
 |-  ( ( ( ph /\ ( k e. ( Base ` ( Scalar ` W ) ) /\ l e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( k ( .s ` W ) Y ) .+ ( l ( .s ` W ) Z ) ) ) /\ k = ( 0g ` ( Scalar ` W ) ) ) -> ( k ( .s ` W ) Y ) = .0. )
38 37 oveq1d 
 |-  ( ( ( ph /\ ( k e. ( Base ` ( Scalar ` W ) ) /\ l e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( k ( .s ` W ) Y ) .+ ( l ( .s ` W ) Z ) ) ) /\ k = ( 0g ` ( Scalar ` W ) ) ) -> ( ( k ( .s ` W ) Y ) .+ ( l ( .s ` W ) Z ) ) = ( .0. .+ ( l ( .s ` W ) Z ) ) )
39 simp2r 
 |-  ( ( ph /\ ( k e. ( Base ` ( Scalar ` W ) ) /\ l e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( k ( .s ` W ) Y ) .+ ( l ( .s ` W ) Z ) ) ) -> l e. ( Base ` ( Scalar ` W ) ) )
40 7 3ad2ant1 
 |-  ( ( ph /\ ( k e. ( Base ` ( Scalar ` W ) ) /\ l e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( k ( .s ` W ) Y ) .+ ( l ( .s ` W ) Z ) ) ) -> Z e. V )
41 1 11 13 12 lmodvscl 
 |-  ( ( W e. LMod /\ l e. ( Base ` ( Scalar ` W ) ) /\ Z e. V ) -> ( l ( .s ` W ) Z ) e. V )
42 18 39 40 41 syl3anc 
 |-  ( ( ph /\ ( k e. ( Base ` ( Scalar ` W ) ) /\ l e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( k ( .s ` W ) Y ) .+ ( l ( .s ` W ) Z ) ) ) -> ( l ( .s ` W ) Z ) e. V )
43 42 adantr 
 |-  ( ( ( ph /\ ( k e. ( Base ` ( Scalar ` W ) ) /\ l e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( k ( .s ` W ) Y ) .+ ( l ( .s ` W ) Z ) ) ) /\ k = ( 0g ` ( Scalar ` W ) ) ) -> ( l ( .s ` W ) Z ) e. V )
44 1 2 3 lmod0vlid 
 |-  ( ( W e. LMod /\ ( l ( .s ` W ) Z ) e. V ) -> ( .0. .+ ( l ( .s ` W ) Z ) ) = ( l ( .s ` W ) Z ) )
45 32 43 44 syl2anc 
 |-  ( ( ( ph /\ ( k e. ( Base ` ( Scalar ` W ) ) /\ l e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( k ( .s ` W ) Y ) .+ ( l ( .s ` W ) Z ) ) ) /\ k = ( 0g ` ( Scalar ` W ) ) ) -> ( .0. .+ ( l ( .s ` W ) Z ) ) = ( l ( .s ` W ) Z ) )
46 28 38 45 3eqtrd 
 |-  ( ( ( ph /\ ( k e. ( Base ` ( Scalar ` W ) ) /\ l e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( k ( .s ` W ) Y ) .+ ( l ( .s ` W ) Z ) ) ) /\ k = ( 0g ` ( Scalar ` W ) ) ) -> X = ( l ( .s ` W ) Z ) )
47 31 21 syl 
 |-  ( ( ( ph /\ ( k e. ( Base ` ( Scalar ` W ) ) /\ l e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( k ( .s ` W ) Y ) .+ ( l ( .s ` W ) Z ) ) ) /\ k = ( 0g ` ( Scalar ` W ) ) ) -> ( N ` { Z } ) e. ( LSubSp ` W ) )
48 simpl2r 
 |-  ( ( ( ph /\ ( k e. ( Base ` ( Scalar ` W ) ) /\ l e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( k ( .s ` W ) Y ) .+ ( l ( .s ` W ) Z ) ) ) /\ k = ( 0g ` ( Scalar ` W ) ) ) -> l e. ( Base ` ( Scalar ` W ) ) )
49 1 4 lspsnid 
 |-  ( ( W e. LMod /\ Z e. V ) -> Z e. ( N ` { Z } ) )
50 15 7 49 syl2anc 
 |-  ( ph -> Z e. ( N ` { Z } ) )
51 31 50 syl 
 |-  ( ( ( ph /\ ( k e. ( Base ` ( Scalar ` W ) ) /\ l e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( k ( .s ` W ) Y ) .+ ( l ( .s ` W ) Z ) ) ) /\ k = ( 0g ` ( Scalar ` W ) ) ) -> Z e. ( N ` { Z } ) )
52 11 13 12 19 lssvscl 
 |-  ( ( ( W e. LMod /\ ( N ` { Z } ) e. ( LSubSp ` W ) ) /\ ( l e. ( Base ` ( Scalar ` W ) ) /\ Z e. ( N ` { Z } ) ) ) -> ( l ( .s ` W ) Z ) e. ( N ` { Z } ) )
53 32 47 48 51 52 syl22anc 
 |-  ( ( ( ph /\ ( k e. ( Base ` ( Scalar ` W ) ) /\ l e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( k ( .s ` W ) Y ) .+ ( l ( .s ` W ) Z ) ) ) /\ k = ( 0g ` ( Scalar ` W ) ) ) -> ( l ( .s ` W ) Z ) e. ( N ` { Z } ) )
54 46 53 eqeltrd 
 |-  ( ( ( ph /\ ( k e. ( Base ` ( Scalar ` W ) ) /\ l e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( k ( .s ` W ) Y ) .+ ( l ( .s ` W ) Z ) ) ) /\ k = ( 0g ` ( Scalar ` W ) ) ) -> X e. ( N ` { Z } ) )
55 54 ex 
 |-  ( ( ph /\ ( k e. ( Base ` ( Scalar ` W ) ) /\ l e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( k ( .s ` W ) Y ) .+ ( l ( .s ` W ) Z ) ) ) -> ( k = ( 0g ` ( Scalar ` W ) ) -> X e. ( N ` { Z } ) ) )
56 55 necon3bd 
 |-  ( ( ph /\ ( k e. ( Base ` ( Scalar ` W ) ) /\ l e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( k ( .s ` W ) Y ) .+ ( l ( .s ` W ) Z ) ) ) -> ( -. X e. ( N ` { Z } ) -> k =/= ( 0g ` ( Scalar ` W ) ) ) )
57 27 56 mpd 
 |-  ( ( ph /\ ( k e. ( Base ` ( Scalar ` W ) ) /\ l e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( k ( .s ` W ) Y ) .+ ( l ( .s ` W ) Z ) ) ) -> k =/= ( 0g ` ( Scalar ` W ) ) )
58 eqid 
 |-  ( invr ` ( Scalar ` W ) ) = ( invr ` ( Scalar ` W ) )
59 12 34 58 drnginvrcl 
 |-  ( ( ( Scalar ` W ) e. DivRing /\ k e. ( Base ` ( Scalar ` W ) ) /\ k =/= ( 0g ` ( Scalar ` W ) ) ) -> ( ( invr ` ( Scalar ` W ) ) ` k ) e. ( Base ` ( Scalar ` W ) ) )
60 25 26 57 59 syl3anc 
 |-  ( ( ph /\ ( k e. ( Base ` ( Scalar ` W ) ) /\ l e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( k ( .s ` W ) Y ) .+ ( l ( .s ` W ) Z ) ) ) -> ( ( invr ` ( Scalar ` W ) ) ` k ) e. ( Base ` ( Scalar ` W ) ) )
61 50 3ad2ant1 
 |-  ( ( ph /\ ( k e. ( Base ` ( Scalar ` W ) ) /\ l e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( k ( .s ` W ) Y ) .+ ( l ( .s ` W ) Z ) ) ) -> Z e. ( N ` { Z } ) )
62 18 22 39 61 52 syl22anc 
 |-  ( ( ph /\ ( k e. ( Base ` ( Scalar ` W ) ) /\ l e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( k ( .s ` W ) Y ) .+ ( l ( .s ` W ) Z ) ) ) -> ( l ( .s ` W ) Z ) e. ( N ` { Z } ) )
63 11 13 12 19 lssvscl 
 |-  ( ( ( W e. LMod /\ ( N ` { Z } ) e. ( LSubSp ` W ) ) /\ ( ( ( invr ` ( Scalar ` W ) ) ` k ) e. ( Base ` ( Scalar ` W ) ) /\ ( l ( .s ` W ) Z ) e. ( N ` { Z } ) ) ) -> ( ( ( invr ` ( Scalar ` W ) ) ` k ) ( .s ` W ) ( l ( .s ` W ) Z ) ) e. ( N ` { Z } ) )
64 18 22 60 62 63 syl22anc 
 |-  ( ( ph /\ ( k e. ( Base ` ( Scalar ` W ) ) /\ l e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( k ( .s ` W ) Y ) .+ ( l ( .s ` W ) Z ) ) ) -> ( ( ( invr ` ( Scalar ` W ) ) ` k ) ( .s ` W ) ( l ( .s ` W ) Z ) ) e. ( N ` { Z } ) )
65 12 34 58 drnginvrn0 
 |-  ( ( ( Scalar ` W ) e. DivRing /\ k e. ( Base ` ( Scalar ` W ) ) /\ k =/= ( 0g ` ( Scalar ` W ) ) ) -> ( ( invr ` ( Scalar ` W ) ) ` k ) =/= ( 0g ` ( Scalar ` W ) ) )
66 25 26 57 65 syl3anc 
 |-  ( ( ph /\ ( k e. ( Base ` ( Scalar ` W ) ) /\ l e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( k ( .s ` W ) Y ) .+ ( l ( .s ` W ) Z ) ) ) -> ( ( invr ` ( Scalar ` W ) ) ` k ) =/= ( 0g ` ( Scalar ` W ) ) )
67 8 3ad2ant1 
 |-  ( ( ph /\ ( k e. ( Base ` ( Scalar ` W ) ) /\ l e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( k ( .s ` W ) Y ) .+ ( l ( .s ` W ) Z ) ) ) -> -. X e. ( N ` { Y } ) )
68 simpl3 
 |-  ( ( ( ph /\ ( k e. ( Base ` ( Scalar ` W ) ) /\ l e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( k ( .s ` W ) Y ) .+ ( l ( .s ` W ) Z ) ) ) /\ l = ( 0g ` ( Scalar ` W ) ) ) -> X = ( ( k ( .s ` W ) Y ) .+ ( l ( .s ` W ) Z ) ) )
69 oveq1 
 |-  ( l = ( 0g ` ( Scalar ` W ) ) -> ( l ( .s ` W ) Z ) = ( ( 0g ` ( Scalar ` W ) ) ( .s ` W ) Z ) )
70 1 11 13 34 3 lmod0vs 
 |-  ( ( W e. LMod /\ Z e. V ) -> ( ( 0g ` ( Scalar ` W ) ) ( .s ` W ) Z ) = .0. )
71 18 40 70 syl2anc 
 |-  ( ( ph /\ ( k e. ( Base ` ( Scalar ` W ) ) /\ l e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( k ( .s ` W ) Y ) .+ ( l ( .s ` W ) Z ) ) ) -> ( ( 0g ` ( Scalar ` W ) ) ( .s ` W ) Z ) = .0. )
72 69 71 sylan9eqr 
 |-  ( ( ( ph /\ ( k e. ( Base ` ( Scalar ` W ) ) /\ l e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( k ( .s ` W ) Y ) .+ ( l ( .s ` W ) Z ) ) ) /\ l = ( 0g ` ( Scalar ` W ) ) ) -> ( l ( .s ` W ) Z ) = .0. )
73 72 oveq2d 
 |-  ( ( ( ph /\ ( k e. ( Base ` ( Scalar ` W ) ) /\ l e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( k ( .s ` W ) Y ) .+ ( l ( .s ` W ) Z ) ) ) /\ l = ( 0g ` ( Scalar ` W ) ) ) -> ( ( k ( .s ` W ) Y ) .+ ( l ( .s ` W ) Z ) ) = ( ( k ( .s ` W ) Y ) .+ .0. ) )
74 6 3ad2ant1 
 |-  ( ( ph /\ ( k e. ( Base ` ( Scalar ` W ) ) /\ l e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( k ( .s ` W ) Y ) .+ ( l ( .s ` W ) Z ) ) ) -> Y e. V )
75 1 11 13 12 lmodvscl 
 |-  ( ( W e. LMod /\ k e. ( Base ` ( Scalar ` W ) ) /\ Y e. V ) -> ( k ( .s ` W ) Y ) e. V )
76 18 26 74 75 syl3anc 
 |-  ( ( ph /\ ( k e. ( Base ` ( Scalar ` W ) ) /\ l e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( k ( .s ` W ) Y ) .+ ( l ( .s ` W ) Z ) ) ) -> ( k ( .s ` W ) Y ) e. V )
77 1 2 3 lmod0vrid 
 |-  ( ( W e. LMod /\ ( k ( .s ` W ) Y ) e. V ) -> ( ( k ( .s ` W ) Y ) .+ .0. ) = ( k ( .s ` W ) Y ) )
78 18 76 77 syl2anc 
 |-  ( ( ph /\ ( k e. ( Base ` ( Scalar ` W ) ) /\ l e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( k ( .s ` W ) Y ) .+ ( l ( .s ` W ) Z ) ) ) -> ( ( k ( .s ` W ) Y ) .+ .0. ) = ( k ( .s ` W ) Y ) )
79 78 adantr 
 |-  ( ( ( ph /\ ( k e. ( Base ` ( Scalar ` W ) ) /\ l e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( k ( .s ` W ) Y ) .+ ( l ( .s ` W ) Z ) ) ) /\ l = ( 0g ` ( Scalar ` W ) ) ) -> ( ( k ( .s ` W ) Y ) .+ .0. ) = ( k ( .s ` W ) Y ) )
80 68 73 79 3eqtrd 
 |-  ( ( ( ph /\ ( k e. ( Base ` ( Scalar ` W ) ) /\ l e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( k ( .s ` W ) Y ) .+ ( l ( .s ` W ) Z ) ) ) /\ l = ( 0g ` ( Scalar ` W ) ) ) -> X = ( k ( .s ` W ) Y ) )
81 1 19 4 lspsncl 
 |-  ( ( W e. LMod /\ Y e. V ) -> ( N ` { Y } ) e. ( LSubSp ` W ) )
82 15 6 81 syl2anc 
 |-  ( ph -> ( N ` { Y } ) e. ( LSubSp ` W ) )
83 82 3ad2ant1 
 |-  ( ( ph /\ ( k e. ( Base ` ( Scalar ` W ) ) /\ l e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( k ( .s ` W ) Y ) .+ ( l ( .s ` W ) Z ) ) ) -> ( N ` { Y } ) e. ( LSubSp ` W ) )
84 1 4 lspsnid 
 |-  ( ( W e. LMod /\ Y e. V ) -> Y e. ( N ` { Y } ) )
85 15 6 84 syl2anc 
 |-  ( ph -> Y e. ( N ` { Y } ) )
86 85 3ad2ant1 
 |-  ( ( ph /\ ( k e. ( Base ` ( Scalar ` W ) ) /\ l e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( k ( .s ` W ) Y ) .+ ( l ( .s ` W ) Z ) ) ) -> Y e. ( N ` { Y } ) )
87 11 13 12 19 lssvscl 
 |-  ( ( ( W e. LMod /\ ( N ` { Y } ) e. ( LSubSp ` W ) ) /\ ( k e. ( Base ` ( Scalar ` W ) ) /\ Y e. ( N ` { Y } ) ) ) -> ( k ( .s ` W ) Y ) e. ( N ` { Y } ) )
88 18 83 26 86 87 syl22anc 
 |-  ( ( ph /\ ( k e. ( Base ` ( Scalar ` W ) ) /\ l e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( k ( .s ` W ) Y ) .+ ( l ( .s ` W ) Z ) ) ) -> ( k ( .s ` W ) Y ) e. ( N ` { Y } ) )
89 88 adantr 
 |-  ( ( ( ph /\ ( k e. ( Base ` ( Scalar ` W ) ) /\ l e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( k ( .s ` W ) Y ) .+ ( l ( .s ` W ) Z ) ) ) /\ l = ( 0g ` ( Scalar ` W ) ) ) -> ( k ( .s ` W ) Y ) e. ( N ` { Y } ) )
90 80 89 eqeltrd 
 |-  ( ( ( ph /\ ( k e. ( Base ` ( Scalar ` W ) ) /\ l e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( k ( .s ` W ) Y ) .+ ( l ( .s ` W ) Z ) ) ) /\ l = ( 0g ` ( Scalar ` W ) ) ) -> X e. ( N ` { Y } ) )
91 90 ex 
 |-  ( ( ph /\ ( k e. ( Base ` ( Scalar ` W ) ) /\ l e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( k ( .s ` W ) Y ) .+ ( l ( .s ` W ) Z ) ) ) -> ( l = ( 0g ` ( Scalar ` W ) ) -> X e. ( N ` { Y } ) ) )
92 91 necon3bd 
 |-  ( ( ph /\ ( k e. ( Base ` ( Scalar ` W ) ) /\ l e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( k ( .s ` W ) Y ) .+ ( l ( .s ` W ) Z ) ) ) -> ( -. X e. ( N ` { Y } ) -> l =/= ( 0g ` ( Scalar ` W ) ) ) )
93 67 92 mpd 
 |-  ( ( ph /\ ( k e. ( Base ` ( Scalar ` W ) ) /\ l e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( k ( .s ` W ) Y ) .+ ( l ( .s ` W ) Z ) ) ) -> l =/= ( 0g ` ( Scalar ` W ) ) )
94 simpl1 
 |-  ( ( ( ph /\ ( k e. ( Base ` ( Scalar ` W ) ) /\ l e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( k ( .s ` W ) Y ) .+ ( l ( .s ` W ) Z ) ) ) /\ Z = .0. ) -> ph )
95 94 10 syl 
 |-  ( ( ( ph /\ ( k e. ( Base ` ( Scalar ` W ) ) /\ l e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( k ( .s ` W ) Y ) .+ ( l ( .s ` W ) Z ) ) ) /\ Z = .0. ) -> X e. ( N ` { Y , Z } ) )
96 preq2 
 |-  ( Z = .0. -> { Y , Z } = { Y , .0. } )
97 96 fveq2d 
 |-  ( Z = .0. -> ( N ` { Y , Z } ) = ( N ` { Y , .0. } ) )
98 1 3 4 18 74 lsppr0 
 |-  ( ( ph /\ ( k e. ( Base ` ( Scalar ` W ) ) /\ l e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( k ( .s ` W ) Y ) .+ ( l ( .s ` W ) Z ) ) ) -> ( N ` { Y , .0. } ) = ( N ` { Y } ) )
99 97 98 sylan9eqr 
 |-  ( ( ( ph /\ ( k e. ( Base ` ( Scalar ` W ) ) /\ l e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( k ( .s ` W ) Y ) .+ ( l ( .s ` W ) Z ) ) ) /\ Z = .0. ) -> ( N ` { Y , Z } ) = ( N ` { Y } ) )
100 95 99 eleqtrd 
 |-  ( ( ( ph /\ ( k e. ( Base ` ( Scalar ` W ) ) /\ l e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( k ( .s ` W ) Y ) .+ ( l ( .s ` W ) Z ) ) ) /\ Z = .0. ) -> X e. ( N ` { Y } ) )
101 100 ex 
 |-  ( ( ph /\ ( k e. ( Base ` ( Scalar ` W ) ) /\ l e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( k ( .s ` W ) Y ) .+ ( l ( .s ` W ) Z ) ) ) -> ( Z = .0. -> X e. ( N ` { Y } ) ) )
102 101 necon3bd 
 |-  ( ( ph /\ ( k e. ( Base ` ( Scalar ` W ) ) /\ l e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( k ( .s ` W ) Y ) .+ ( l ( .s ` W ) Z ) ) ) -> ( -. X e. ( N ` { Y } ) -> Z =/= .0. ) )
103 67 102 mpd 
 |-  ( ( ph /\ ( k e. ( Base ` ( Scalar ` W ) ) /\ l e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( k ( .s ` W ) Y ) .+ ( l ( .s ` W ) Z ) ) ) -> Z =/= .0. )
104 1 13 11 12 34 3 23 39 40 lvecvsn0 
 |-  ( ( ph /\ ( k e. ( Base ` ( Scalar ` W ) ) /\ l e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( k ( .s ` W ) Y ) .+ ( l ( .s ` W ) Z ) ) ) -> ( ( l ( .s ` W ) Z ) =/= .0. <-> ( l =/= ( 0g ` ( Scalar ` W ) ) /\ Z =/= .0. ) ) )
105 93 103 104 mpbir2and 
 |-  ( ( ph /\ ( k e. ( Base ` ( Scalar ` W ) ) /\ l e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( k ( .s ` W ) Y ) .+ ( l ( .s ` W ) Z ) ) ) -> ( l ( .s ` W ) Z ) =/= .0. )
106 1 13 11 12 34 3 23 60 42 lvecvsn0 
 |-  ( ( ph /\ ( k e. ( Base ` ( Scalar ` W ) ) /\ l e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( k ( .s ` W ) Y ) .+ ( l ( .s ` W ) Z ) ) ) -> ( ( ( ( invr ` ( Scalar ` W ) ) ` k ) ( .s ` W ) ( l ( .s ` W ) Z ) ) =/= .0. <-> ( ( ( invr ` ( Scalar ` W ) ) ` k ) =/= ( 0g ` ( Scalar ` W ) ) /\ ( l ( .s ` W ) Z ) =/= .0. ) ) )
107 66 105 106 mpbir2and 
 |-  ( ( ph /\ ( k e. ( Base ` ( Scalar ` W ) ) /\ l e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( k ( .s ` W ) Y ) .+ ( l ( .s ` W ) Z ) ) ) -> ( ( ( invr ` ( Scalar ` W ) ) ` k ) ( .s ` W ) ( l ( .s ` W ) Z ) ) =/= .0. )
108 eldifsn 
 |-  ( ( ( ( invr ` ( Scalar ` W ) ) ` k ) ( .s ` W ) ( l ( .s ` W ) Z ) ) e. ( ( N ` { Z } ) \ { .0. } ) <-> ( ( ( ( invr ` ( Scalar ` W ) ) ` k ) ( .s ` W ) ( l ( .s ` W ) Z ) ) e. ( N ` { Z } ) /\ ( ( ( invr ` ( Scalar ` W ) ) ` k ) ( .s ` W ) ( l ( .s ` W ) Z ) ) =/= .0. ) )
109 64 107 108 sylanbrc 
 |-  ( ( ph /\ ( k e. ( Base ` ( Scalar ` W ) ) /\ l e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( k ( .s ` W ) Y ) .+ ( l ( .s ` W ) Z ) ) ) -> ( ( ( invr ` ( Scalar ` W ) ) ` k ) ( .s ` W ) ( l ( .s ` W ) Z ) ) e. ( ( N ` { Z } ) \ { .0. } ) )
110 simp3 
 |-  ( ( ph /\ ( k e. ( Base ` ( Scalar ` W ) ) /\ l e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( k ( .s ` W ) Y ) .+ ( l ( .s ` W ) Z ) ) ) -> X = ( ( k ( .s ` W ) Y ) .+ ( l ( .s ` W ) Z ) ) )
111 1 2 lmodvacl 
 |-  ( ( W e. LMod /\ ( k ( .s ` W ) Y ) e. V /\ ( l ( .s ` W ) Z ) e. V ) -> ( ( k ( .s ` W ) Y ) .+ ( l ( .s ` W ) Z ) ) e. V )
112 18 76 42 111 syl3anc 
 |-  ( ( ph /\ ( k e. ( Base ` ( Scalar ` W ) ) /\ l e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( k ( .s ` W ) Y ) .+ ( l ( .s ` W ) Z ) ) ) -> ( ( k ( .s ` W ) Y ) .+ ( l ( .s ` W ) Z ) ) e. V )
113 1 4 lspsnid 
 |-  ( ( W e. LMod /\ ( ( k ( .s ` W ) Y ) .+ ( l ( .s ` W ) Z ) ) e. V ) -> ( ( k ( .s ` W ) Y ) .+ ( l ( .s ` W ) Z ) ) e. ( N ` { ( ( k ( .s ` W ) Y ) .+ ( l ( .s ` W ) Z ) ) } ) )
114 18 112 113 syl2anc 
 |-  ( ( ph /\ ( k e. ( Base ` ( Scalar ` W ) ) /\ l e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( k ( .s ` W ) Y ) .+ ( l ( .s ` W ) Z ) ) ) -> ( ( k ( .s ` W ) Y ) .+ ( l ( .s ` W ) Z ) ) e. ( N ` { ( ( k ( .s ` W ) Y ) .+ ( l ( .s ` W ) Z ) ) } ) )
115 110 114 eqeltrd 
 |-  ( ( ph /\ ( k e. ( Base ` ( Scalar ` W ) ) /\ l e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( k ( .s ` W ) Y ) .+ ( l ( .s ` W ) Z ) ) ) -> X e. ( N ` { ( ( k ( .s ` W ) Y ) .+ ( l ( .s ` W ) Z ) ) } ) )
116 1 11 13 12 34 4 lspsnvs 
 |-  ( ( W e. LVec /\ ( ( ( invr ` ( Scalar ` W ) ) ` k ) e. ( Base ` ( Scalar ` W ) ) /\ ( ( invr ` ( Scalar ` W ) ) ` k ) =/= ( 0g ` ( Scalar ` W ) ) ) /\ ( ( k ( .s ` W ) Y ) .+ ( l ( .s ` W ) Z ) ) e. V ) -> ( N ` { ( ( ( invr ` ( Scalar ` W ) ) ` k ) ( .s ` W ) ( ( k ( .s ` W ) Y ) .+ ( l ( .s ` W ) Z ) ) ) } ) = ( N ` { ( ( k ( .s ` W ) Y ) .+ ( l ( .s ` W ) Z ) ) } ) )
117 23 60 66 112 116 syl121anc 
 |-  ( ( ph /\ ( k e. ( Base ` ( Scalar ` W ) ) /\ l e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( k ( .s ` W ) Y ) .+ ( l ( .s ` W ) Z ) ) ) -> ( N ` { ( ( ( invr ` ( Scalar ` W ) ) ` k ) ( .s ` W ) ( ( k ( .s ` W ) Y ) .+ ( l ( .s ` W ) Z ) ) ) } ) = ( N ` { ( ( k ( .s ` W ) Y ) .+ ( l ( .s ` W ) Z ) ) } ) )
118 1 2 11 13 12 lmodvsdi 
 |-  ( ( W e. LMod /\ ( ( ( invr ` ( Scalar ` W ) ) ` k ) e. ( Base ` ( Scalar ` W ) ) /\ ( k ( .s ` W ) Y ) e. V /\ ( l ( .s ` W ) Z ) e. V ) ) -> ( ( ( invr ` ( Scalar ` W ) ) ` k ) ( .s ` W ) ( ( k ( .s ` W ) Y ) .+ ( l ( .s ` W ) Z ) ) ) = ( ( ( ( invr ` ( Scalar ` W ) ) ` k ) ( .s ` W ) ( k ( .s ` W ) Y ) ) .+ ( ( ( invr ` ( Scalar ` W ) ) ` k ) ( .s ` W ) ( l ( .s ` W ) Z ) ) ) )
119 18 60 76 42 118 syl13anc 
 |-  ( ( ph /\ ( k e. ( Base ` ( Scalar ` W ) ) /\ l e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( k ( .s ` W ) Y ) .+ ( l ( .s ` W ) Z ) ) ) -> ( ( ( invr ` ( Scalar ` W ) ) ` k ) ( .s ` W ) ( ( k ( .s ` W ) Y ) .+ ( l ( .s ` W ) Z ) ) ) = ( ( ( ( invr ` ( Scalar ` W ) ) ` k ) ( .s ` W ) ( k ( .s ` W ) Y ) ) .+ ( ( ( invr ` ( Scalar ` W ) ) ` k ) ( .s ` W ) ( l ( .s ` W ) Z ) ) ) )
120 eqid 
 |-  ( .r ` ( Scalar ` W ) ) = ( .r ` ( Scalar ` W ) )
121 eqid 
 |-  ( 1r ` ( Scalar ` W ) ) = ( 1r ` ( Scalar ` W ) )
122 12 34 120 121 58 drnginvrl 
 |-  ( ( ( Scalar ` W ) e. DivRing /\ k e. ( Base ` ( Scalar ` W ) ) /\ k =/= ( 0g ` ( Scalar ` W ) ) ) -> ( ( ( invr ` ( Scalar ` W ) ) ` k ) ( .r ` ( Scalar ` W ) ) k ) = ( 1r ` ( Scalar ` W ) ) )
123 25 26 57 122 syl3anc 
 |-  ( ( ph /\ ( k e. ( Base ` ( Scalar ` W ) ) /\ l e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( k ( .s ` W ) Y ) .+ ( l ( .s ` W ) Z ) ) ) -> ( ( ( invr ` ( Scalar ` W ) ) ` k ) ( .r ` ( Scalar ` W ) ) k ) = ( 1r ` ( Scalar ` W ) ) )
124 123 oveq1d 
 |-  ( ( ph /\ ( k e. ( Base ` ( Scalar ` W ) ) /\ l e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( k ( .s ` W ) Y ) .+ ( l ( .s ` W ) Z ) ) ) -> ( ( ( ( invr ` ( Scalar ` W ) ) ` k ) ( .r ` ( Scalar ` W ) ) k ) ( .s ` W ) Y ) = ( ( 1r ` ( Scalar ` W ) ) ( .s ` W ) Y ) )
125 1 11 13 12 120 lmodvsass 
 |-  ( ( W e. LMod /\ ( ( ( invr ` ( Scalar ` W ) ) ` k ) e. ( Base ` ( Scalar ` W ) ) /\ k e. ( Base ` ( Scalar ` W ) ) /\ Y e. V ) ) -> ( ( ( ( invr ` ( Scalar ` W ) ) ` k ) ( .r ` ( Scalar ` W ) ) k ) ( .s ` W ) Y ) = ( ( ( invr ` ( Scalar ` W ) ) ` k ) ( .s ` W ) ( k ( .s ` W ) Y ) ) )
126 18 60 26 74 125 syl13anc 
 |-  ( ( ph /\ ( k e. ( Base ` ( Scalar ` W ) ) /\ l e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( k ( .s ` W ) Y ) .+ ( l ( .s ` W ) Z ) ) ) -> ( ( ( ( invr ` ( Scalar ` W ) ) ` k ) ( .r ` ( Scalar ` W ) ) k ) ( .s ` W ) Y ) = ( ( ( invr ` ( Scalar ` W ) ) ` k ) ( .s ` W ) ( k ( .s ` W ) Y ) ) )
127 1 11 13 121 lmodvs1 
 |-  ( ( W e. LMod /\ Y e. V ) -> ( ( 1r ` ( Scalar ` W ) ) ( .s ` W ) Y ) = Y )
128 18 74 127 syl2anc 
 |-  ( ( ph /\ ( k e. ( Base ` ( Scalar ` W ) ) /\ l e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( k ( .s ` W ) Y ) .+ ( l ( .s ` W ) Z ) ) ) -> ( ( 1r ` ( Scalar ` W ) ) ( .s ` W ) Y ) = Y )
129 124 126 128 3eqtr3d 
 |-  ( ( ph /\ ( k e. ( Base ` ( Scalar ` W ) ) /\ l e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( k ( .s ` W ) Y ) .+ ( l ( .s ` W ) Z ) ) ) -> ( ( ( invr ` ( Scalar ` W ) ) ` k ) ( .s ` W ) ( k ( .s ` W ) Y ) ) = Y )
130 129 oveq1d 
 |-  ( ( ph /\ ( k e. ( Base ` ( Scalar ` W ) ) /\ l e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( k ( .s ` W ) Y ) .+ ( l ( .s ` W ) Z ) ) ) -> ( ( ( ( invr ` ( Scalar ` W ) ) ` k ) ( .s ` W ) ( k ( .s ` W ) Y ) ) .+ ( ( ( invr ` ( Scalar ` W ) ) ` k ) ( .s ` W ) ( l ( .s ` W ) Z ) ) ) = ( Y .+ ( ( ( invr ` ( Scalar ` W ) ) ` k ) ( .s ` W ) ( l ( .s ` W ) Z ) ) ) )
131 119 130 eqtrd 
 |-  ( ( ph /\ ( k e. ( Base ` ( Scalar ` W ) ) /\ l e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( k ( .s ` W ) Y ) .+ ( l ( .s ` W ) Z ) ) ) -> ( ( ( invr ` ( Scalar ` W ) ) ` k ) ( .s ` W ) ( ( k ( .s ` W ) Y ) .+ ( l ( .s ` W ) Z ) ) ) = ( Y .+ ( ( ( invr ` ( Scalar ` W ) ) ` k ) ( .s ` W ) ( l ( .s ` W ) Z ) ) ) )
132 131 sneqd 
 |-  ( ( ph /\ ( k e. ( Base ` ( Scalar ` W ) ) /\ l e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( k ( .s ` W ) Y ) .+ ( l ( .s ` W ) Z ) ) ) -> { ( ( ( invr ` ( Scalar ` W ) ) ` k ) ( .s ` W ) ( ( k ( .s ` W ) Y ) .+ ( l ( .s ` W ) Z ) ) ) } = { ( Y .+ ( ( ( invr ` ( Scalar ` W ) ) ` k ) ( .s ` W ) ( l ( .s ` W ) Z ) ) ) } )
133 132 fveq2d 
 |-  ( ( ph /\ ( k e. ( Base ` ( Scalar ` W ) ) /\ l e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( k ( .s ` W ) Y ) .+ ( l ( .s ` W ) Z ) ) ) -> ( N ` { ( ( ( invr ` ( Scalar ` W ) ) ` k ) ( .s ` W ) ( ( k ( .s ` W ) Y ) .+ ( l ( .s ` W ) Z ) ) ) } ) = ( N ` { ( Y .+ ( ( ( invr ` ( Scalar ` W ) ) ` k ) ( .s ` W ) ( l ( .s ` W ) Z ) ) ) } ) )
134 117 133 eqtr3d 
 |-  ( ( ph /\ ( k e. ( Base ` ( Scalar ` W ) ) /\ l e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( k ( .s ` W ) Y ) .+ ( l ( .s ` W ) Z ) ) ) -> ( N ` { ( ( k ( .s ` W ) Y ) .+ ( l ( .s ` W ) Z ) ) } ) = ( N ` { ( Y .+ ( ( ( invr ` ( Scalar ` W ) ) ` k ) ( .s ` W ) ( l ( .s ` W ) Z ) ) ) } ) )
135 115 134 eleqtrd 
 |-  ( ( ph /\ ( k e. ( Base ` ( Scalar ` W ) ) /\ l e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( k ( .s ` W ) Y ) .+ ( l ( .s ` W ) Z ) ) ) -> X e. ( N ` { ( Y .+ ( ( ( invr ` ( Scalar ` W ) ) ` k ) ( .s ` W ) ( l ( .s ` W ) Z ) ) ) } ) )
136 oveq2 
 |-  ( z = ( ( ( invr ` ( Scalar ` W ) ) ` k ) ( .s ` W ) ( l ( .s ` W ) Z ) ) -> ( Y .+ z ) = ( Y .+ ( ( ( invr ` ( Scalar ` W ) ) ` k ) ( .s ` W ) ( l ( .s ` W ) Z ) ) ) )
137 136 sneqd 
 |-  ( z = ( ( ( invr ` ( Scalar ` W ) ) ` k ) ( .s ` W ) ( l ( .s ` W ) Z ) ) -> { ( Y .+ z ) } = { ( Y .+ ( ( ( invr ` ( Scalar ` W ) ) ` k ) ( .s ` W ) ( l ( .s ` W ) Z ) ) ) } )
138 137 fveq2d 
 |-  ( z = ( ( ( invr ` ( Scalar ` W ) ) ` k ) ( .s ` W ) ( l ( .s ` W ) Z ) ) -> ( N ` { ( Y .+ z ) } ) = ( N ` { ( Y .+ ( ( ( invr ` ( Scalar ` W ) ) ` k ) ( .s ` W ) ( l ( .s ` W ) Z ) ) ) } ) )
139 138 eleq2d 
 |-  ( z = ( ( ( invr ` ( Scalar ` W ) ) ` k ) ( .s ` W ) ( l ( .s ` W ) Z ) ) -> ( X e. ( N ` { ( Y .+ z ) } ) <-> X e. ( N ` { ( Y .+ ( ( ( invr ` ( Scalar ` W ) ) ` k ) ( .s ` W ) ( l ( .s ` W ) Z ) ) ) } ) ) )
140 139 rspcev 
 |-  ( ( ( ( ( invr ` ( Scalar ` W ) ) ` k ) ( .s ` W ) ( l ( .s ` W ) Z ) ) e. ( ( N ` { Z } ) \ { .0. } ) /\ X e. ( N ` { ( Y .+ ( ( ( invr ` ( Scalar ` W ) ) ` k ) ( .s ` W ) ( l ( .s ` W ) Z ) ) ) } ) ) -> E. z e. ( ( N ` { Z } ) \ { .0. } ) X e. ( N ` { ( Y .+ z ) } ) )
141 109 135 140 syl2anc 
 |-  ( ( ph /\ ( k e. ( Base ` ( Scalar ` W ) ) /\ l e. ( Base ` ( Scalar ` W ) ) ) /\ X = ( ( k ( .s ` W ) Y ) .+ ( l ( .s ` W ) Z ) ) ) -> E. z e. ( ( N ` { Z } ) \ { .0. } ) X e. ( N ` { ( Y .+ z ) } ) )
142 141 3exp 
 |-  ( ph -> ( ( k e. ( Base ` ( Scalar ` W ) ) /\ l e. ( Base ` ( Scalar ` W ) ) ) -> ( X = ( ( k ( .s ` W ) Y ) .+ ( l ( .s ` W ) Z ) ) -> E. z e. ( ( N ` { Z } ) \ { .0. } ) X e. ( N ` { ( Y .+ z ) } ) ) ) )
143 142 rexlimdvv 
 |-  ( ph -> ( E. k e. ( Base ` ( Scalar ` W ) ) E. l e. ( Base ` ( Scalar ` W ) ) X = ( ( k ( .s ` W ) Y ) .+ ( l ( .s ` W ) Z ) ) -> E. z e. ( ( N ` { Z } ) \ { .0. } ) X e. ( N ` { ( Y .+ z ) } ) ) )
144 17 143 mpd 
 |-  ( ph -> E. z e. ( ( N ` { Z } ) \ { .0. } ) X e. ( N ` { ( Y .+ z ) } ) )