Metamath Proof Explorer

Theorem lkrsc

Description: The kernel of a nonzero scalar product of a functional equals the kernel of the functional. (Contributed by NM, 9-Oct-2014)

Ref Expression
Hypotheses lkrsc.v 
|- V = ( Base ` W )
lkrsc.d 
|- D = ( Scalar ` W )
lkrsc.k 
|- K = ( Base ` D )
lkrsc.t 
|- .x. = ( .r ` D )
lkrsc.f 
|- F = ( LFnl ` W )
lkrsc.l 
|- L = ( LKer ` W )
lkrsc.w 
|- ( ph -> W e. LVec )
lkrsc.g 
|- ( ph -> G e. F )
lkrsc.r 
|- ( ph -> R e. K )
lkrsc.o 
|- .0. = ( 0g ` D )
lkrsc.e 
|- ( ph -> R =/= .0. )
Assertion lkrsc 
|- ( ph -> ( L ` ( G oF .x. ( V X. { R } ) ) ) = ( L ` G ) )

Proof

Step Hyp Ref Expression
1 lkrsc.v 
 |-  V = ( Base ` W )
2 lkrsc.d 
 |-  D = ( Scalar ` W )
3 lkrsc.k 
 |-  K = ( Base ` D )
4 lkrsc.t 
 |-  .x. = ( .r ` D )
5 lkrsc.f 
 |-  F = ( LFnl ` W )
6 lkrsc.l 
 |-  L = ( LKer ` W )
7 lkrsc.w 
 |-  ( ph -> W e. LVec )
8 lkrsc.g 
 |-  ( ph -> G e. F )
9 lkrsc.r 
 |-  ( ph -> R e. K )
10 lkrsc.o 
 |-  .0. = ( 0g ` D )
11 lkrsc.e 
 |-  ( ph -> R =/= .0. )
12 1 fvexi 
 |-  V e. _V
13 12 a1i 
 |-  ( ph -> V e. _V )
14 2 3 1 5 lflf 
 |-  ( ( W e. LVec /\ G e. F ) -> G : V --> K )
15 7 8 14 syl2anc 
 |-  ( ph -> G : V --> K )
16 15 ffnd 
 |-  ( ph -> G Fn V )
17 eqidd 
 |-  ( ( ph /\ v e. V ) -> ( G ` v ) = ( G ` v ) )
18 13 9 16 17 ofc2 
 |-  ( ( ph /\ v e. V ) -> ( ( G oF .x. ( V X. { R } ) ) ` v ) = ( ( G ` v ) .x. R ) )
19 18 eqeq1d 
 |-  ( ( ph /\ v e. V ) -> ( ( ( G oF .x. ( V X. { R } ) ) ` v ) = .0. <-> ( ( G ` v ) .x. R ) = .0. ) )
20 2 lvecdrng 
 |-  ( W e. LVec -> D e. DivRing )
21 7 20 syl 
 |-  ( ph -> D e. DivRing )
22 21 adantr 
 |-  ( ( ph /\ v e. V ) -> D e. DivRing )
23 7 adantr 
 |-  ( ( ph /\ v e. V ) -> W e. LVec )
24 8 adantr 
 |-  ( ( ph /\ v e. V ) -> G e. F )
25 simpr 
 |-  ( ( ph /\ v e. V ) -> v e. V )
26 2 3 1 5 lflcl 
 |-  ( ( W e. LVec /\ G e. F /\ v e. V ) -> ( G ` v ) e. K )
27 23 24 25 26 syl3anc 
 |-  ( ( ph /\ v e. V ) -> ( G ` v ) e. K )
28 9 adantr 
 |-  ( ( ph /\ v e. V ) -> R e. K )
29 11 adantr 
 |-  ( ( ph /\ v e. V ) -> R =/= .0. )
30 3 10 4 22 27 28 29 drngmuleq0 
 |-  ( ( ph /\ v e. V ) -> ( ( ( G ` v ) .x. R ) = .0. <-> ( G ` v ) = .0. ) )
31 19 30 bitrd 
 |-  ( ( ph /\ v e. V ) -> ( ( ( G oF .x. ( V X. { R } ) ) ` v ) = .0. <-> ( G ` v ) = .0. ) )
32 31 pm5.32da 
 |-  ( ph -> ( ( v e. V /\ ( ( G oF .x. ( V X. { R } ) ) ` v ) = .0. ) <-> ( v e. V /\ ( G ` v ) = .0. ) ) )
33 lveclmod 
 |-  ( W e. LVec -> W e. LMod )
34 7 33 syl 
 |-  ( ph -> W e. LMod )
35 1 2 3 4 5 34 8 9 lflvscl 
 |-  ( ph -> ( G oF .x. ( V X. { R } ) ) e. F )
36 1 2 10 5 6 ellkr 
 |-  ( ( W e. LVec /\ ( G oF .x. ( V X. { R } ) ) e. F ) -> ( v e. ( L ` ( G oF .x. ( V X. { R } ) ) ) <-> ( v e. V /\ ( ( G oF .x. ( V X. { R } ) ) ` v ) = .0. ) ) )
37 7 35 36 syl2anc 
 |-  ( ph -> ( v e. ( L ` ( G oF .x. ( V X. { R } ) ) ) <-> ( v e. V /\ ( ( G oF .x. ( V X. { R } ) ) ` v ) = .0. ) ) )
38 1 2 10 5 6 ellkr 
 |-  ( ( W e. LVec /\ G e. F ) -> ( v e. ( L ` G ) <-> ( v e. V /\ ( G ` v ) = .0. ) ) )
39 7 8 38 syl2anc 
 |-  ( ph -> ( v e. ( L ` G ) <-> ( v e. V /\ ( G ` v ) = .0. ) ) )
40 32 37 39 3bitr4d 
 |-  ( ph -> ( v e. ( L ` ( G oF .x. ( V X. { R } ) ) ) <-> v e. ( L ` G ) ) )
41 40 eqrdv 
 |-  ( ph -> ( L ` ( G oF .x. ( V X. { R } ) ) ) = ( L ` G ) )