Step |
Hyp |
Ref |
Expression |
1 |
|
lfl1.d |
|- D = ( Scalar ` W ) |
2 |
|
lfl1.o |
|- .0. = ( 0g ` D ) |
3 |
|
lfl1.u |
|- .1. = ( 1r ` D ) |
4 |
|
lfl1.v |
|- V = ( Base ` W ) |
5 |
|
lfl1.f |
|- F = ( LFnl ` W ) |
6 |
|
nne |
|- ( -. ( G ` z ) =/= .0. <-> ( G ` z ) = .0. ) |
7 |
6
|
ralbii |
|- ( A. z e. V -. ( G ` z ) =/= .0. <-> A. z e. V ( G ` z ) = .0. ) |
8 |
|
eqid |
|- ( Base ` D ) = ( Base ` D ) |
9 |
1 8 4 5
|
lflf |
|- ( ( W e. LVec /\ G e. F ) -> G : V --> ( Base ` D ) ) |
10 |
9
|
ffnd |
|- ( ( W e. LVec /\ G e. F ) -> G Fn V ) |
11 |
|
fconstfv |
|- ( G : V --> { .0. } <-> ( G Fn V /\ A. z e. V ( G ` z ) = .0. ) ) |
12 |
11
|
simplbi2 |
|- ( G Fn V -> ( A. z e. V ( G ` z ) = .0. -> G : V --> { .0. } ) ) |
13 |
10 12
|
syl |
|- ( ( W e. LVec /\ G e. F ) -> ( A. z e. V ( G ` z ) = .0. -> G : V --> { .0. } ) ) |
14 |
2
|
fvexi |
|- .0. e. _V |
15 |
14
|
fconst2 |
|- ( G : V --> { .0. } <-> G = ( V X. { .0. } ) ) |
16 |
13 15
|
syl6ib |
|- ( ( W e. LVec /\ G e. F ) -> ( A. z e. V ( G ` z ) = .0. -> G = ( V X. { .0. } ) ) ) |
17 |
7 16
|
syl5bi |
|- ( ( W e. LVec /\ G e. F ) -> ( A. z e. V -. ( G ` z ) =/= .0. -> G = ( V X. { .0. } ) ) ) |
18 |
17
|
necon3ad |
|- ( ( W e. LVec /\ G e. F ) -> ( G =/= ( V X. { .0. } ) -> -. A. z e. V -. ( G ` z ) =/= .0. ) ) |
19 |
|
dfrex2 |
|- ( E. z e. V ( G ` z ) =/= .0. <-> -. A. z e. V -. ( G ` z ) =/= .0. ) |
20 |
18 19
|
syl6ibr |
|- ( ( W e. LVec /\ G e. F ) -> ( G =/= ( V X. { .0. } ) -> E. z e. V ( G ` z ) =/= .0. ) ) |
21 |
20
|
3impia |
|- ( ( W e. LVec /\ G e. F /\ G =/= ( V X. { .0. } ) ) -> E. z e. V ( G ` z ) =/= .0. ) |
22 |
|
simp1l |
|- ( ( ( W e. LVec /\ G e. F ) /\ z e. V /\ ( G ` z ) =/= .0. ) -> W e. LVec ) |
23 |
|
lveclmod |
|- ( W e. LVec -> W e. LMod ) |
24 |
22 23
|
syl |
|- ( ( ( W e. LVec /\ G e. F ) /\ z e. V /\ ( G ` z ) =/= .0. ) -> W e. LMod ) |
25 |
1
|
lvecdrng |
|- ( W e. LVec -> D e. DivRing ) |
26 |
22 25
|
syl |
|- ( ( ( W e. LVec /\ G e. F ) /\ z e. V /\ ( G ` z ) =/= .0. ) -> D e. DivRing ) |
27 |
|
simp1r |
|- ( ( ( W e. LVec /\ G e. F ) /\ z e. V /\ ( G ` z ) =/= .0. ) -> G e. F ) |
28 |
|
simp2 |
|- ( ( ( W e. LVec /\ G e. F ) /\ z e. V /\ ( G ` z ) =/= .0. ) -> z e. V ) |
29 |
1 8 4 5
|
lflcl |
|- ( ( W e. LVec /\ G e. F /\ z e. V ) -> ( G ` z ) e. ( Base ` D ) ) |
30 |
22 27 28 29
|
syl3anc |
|- ( ( ( W e. LVec /\ G e. F ) /\ z e. V /\ ( G ` z ) =/= .0. ) -> ( G ` z ) e. ( Base ` D ) ) |
31 |
|
simp3 |
|- ( ( ( W e. LVec /\ G e. F ) /\ z e. V /\ ( G ` z ) =/= .0. ) -> ( G ` z ) =/= .0. ) |
32 |
|
eqid |
|- ( invr ` D ) = ( invr ` D ) |
33 |
8 2 32
|
drnginvrcl |
|- ( ( D e. DivRing /\ ( G ` z ) e. ( Base ` D ) /\ ( G ` z ) =/= .0. ) -> ( ( invr ` D ) ` ( G ` z ) ) e. ( Base ` D ) ) |
34 |
26 30 31 33
|
syl3anc |
|- ( ( ( W e. LVec /\ G e. F ) /\ z e. V /\ ( G ` z ) =/= .0. ) -> ( ( invr ` D ) ` ( G ` z ) ) e. ( Base ` D ) ) |
35 |
|
eqid |
|- ( .s ` W ) = ( .s ` W ) |
36 |
4 1 35 8
|
lmodvscl |
|- ( ( W e. LMod /\ ( ( invr ` D ) ` ( G ` z ) ) e. ( Base ` D ) /\ z e. V ) -> ( ( ( invr ` D ) ` ( G ` z ) ) ( .s ` W ) z ) e. V ) |
37 |
24 34 28 36
|
syl3anc |
|- ( ( ( W e. LVec /\ G e. F ) /\ z e. V /\ ( G ` z ) =/= .0. ) -> ( ( ( invr ` D ) ` ( G ` z ) ) ( .s ` W ) z ) e. V ) |
38 |
|
eqid |
|- ( .r ` D ) = ( .r ` D ) |
39 |
1 8 38 4 35 5
|
lflmul |
|- ( ( W e. LMod /\ G e. F /\ ( ( ( invr ` D ) ` ( G ` z ) ) e. ( Base ` D ) /\ z e. V ) ) -> ( G ` ( ( ( invr ` D ) ` ( G ` z ) ) ( .s ` W ) z ) ) = ( ( ( invr ` D ) ` ( G ` z ) ) ( .r ` D ) ( G ` z ) ) ) |
40 |
24 27 34 28 39
|
syl112anc |
|- ( ( ( W e. LVec /\ G e. F ) /\ z e. V /\ ( G ` z ) =/= .0. ) -> ( G ` ( ( ( invr ` D ) ` ( G ` z ) ) ( .s ` W ) z ) ) = ( ( ( invr ` D ) ` ( G ` z ) ) ( .r ` D ) ( G ` z ) ) ) |
41 |
8 2 38 3 32
|
drnginvrl |
|- ( ( D e. DivRing /\ ( G ` z ) e. ( Base ` D ) /\ ( G ` z ) =/= .0. ) -> ( ( ( invr ` D ) ` ( G ` z ) ) ( .r ` D ) ( G ` z ) ) = .1. ) |
42 |
26 30 31 41
|
syl3anc |
|- ( ( ( W e. LVec /\ G e. F ) /\ z e. V /\ ( G ` z ) =/= .0. ) -> ( ( ( invr ` D ) ` ( G ` z ) ) ( .r ` D ) ( G ` z ) ) = .1. ) |
43 |
40 42
|
eqtrd |
|- ( ( ( W e. LVec /\ G e. F ) /\ z e. V /\ ( G ` z ) =/= .0. ) -> ( G ` ( ( ( invr ` D ) ` ( G ` z ) ) ( .s ` W ) z ) ) = .1. ) |
44 |
|
fveqeq2 |
|- ( x = ( ( ( invr ` D ) ` ( G ` z ) ) ( .s ` W ) z ) -> ( ( G ` x ) = .1. <-> ( G ` ( ( ( invr ` D ) ` ( G ` z ) ) ( .s ` W ) z ) ) = .1. ) ) |
45 |
44
|
rspcev |
|- ( ( ( ( ( invr ` D ) ` ( G ` z ) ) ( .s ` W ) z ) e. V /\ ( G ` ( ( ( invr ` D ) ` ( G ` z ) ) ( .s ` W ) z ) ) = .1. ) -> E. x e. V ( G ` x ) = .1. ) |
46 |
37 43 45
|
syl2anc |
|- ( ( ( W e. LVec /\ G e. F ) /\ z e. V /\ ( G ` z ) =/= .0. ) -> E. x e. V ( G ` x ) = .1. ) |
47 |
46
|
rexlimdv3a |
|- ( ( W e. LVec /\ G e. F ) -> ( E. z e. V ( G ` z ) =/= .0. -> E. x e. V ( G ` x ) = .1. ) ) |
48 |
47
|
3adant3 |
|- ( ( W e. LVec /\ G e. F /\ G =/= ( V X. { .0. } ) ) -> ( E. z e. V ( G ` z ) =/= .0. -> E. x e. V ( G ` x ) = .1. ) ) |
49 |
21 48
|
mpd |
|- ( ( W e. LVec /\ G e. F /\ G =/= ( V X. { .0. } ) ) -> E. x e. V ( G ` x ) = .1. ) |