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