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 ) } ) ) |