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 · ˙ = D
lkrsc.f F = LFnl W
lkrsc.l L = LKer W
lkrsc.w φ W LVec
lkrsc.g φ G F
lkrsc.r φ R K
lkrsc.o 0 ˙ = 0 D
lkrsc.e φ R 0 ˙
Assertion lkrsc φ L G · ˙ f V × 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 · ˙ = D
5 lkrsc.f F = LFnl W
6 lkrsc.l L = LKer W
7 lkrsc.w φ W LVec
8 lkrsc.g φ G F
9 lkrsc.r φ R K
10 lkrsc.o 0 ˙ = 0 D
11 lkrsc.e φ R 0 ˙
12 1 fvexi V V
13 12 a1i φ V V
14 2 3 1 5 lflf W LVec G F G : V K
15 7 8 14 syl2anc φ G : V K
16 15 ffnd φ G Fn V
17 eqidd φ v V G v = G v
18 13 9 16 17 ofc2 φ v V G · ˙ f V × R v = G v · ˙ R
19 18 eqeq1d φ v V G · ˙ f V × R v = 0 ˙ G v · ˙ R = 0 ˙
20 2 lvecdrng W LVec D DivRing
21 7 20 syl φ D DivRing
22 21 adantr φ v V D DivRing
23 7 adantr φ v V W LVec
24 8 adantr φ v V G F
25 simpr φ v V v V
26 2 3 1 5 lflcl W LVec G F v V G v K
27 23 24 25 26 syl3anc φ v V G v K
28 9 adantr φ v V R K
29 11 adantr φ v V R 0 ˙
30 3 10 4 22 27 28 29 drngmuleq0 φ v V G v · ˙ R = 0 ˙ G v = 0 ˙
31 19 30 bitrd φ v V G · ˙ f V × R v = 0 ˙ G v = 0 ˙
32 31 pm5.32da φ v V G · ˙ f V × R v = 0 ˙ v V G v = 0 ˙
33 lveclmod W LVec W LMod
34 7 33 syl φ W LMod
35 1 2 3 4 5 34 8 9 lflvscl φ G · ˙ f V × R F
36 1 2 10 5 6 ellkr W LVec G · ˙ f V × R F v L G · ˙ f V × R v V G · ˙ f V × R v = 0 ˙
37 7 35 36 syl2anc φ v L G · ˙ f V × R v V G · ˙ f V × R v = 0 ˙
38 1 2 10 5 6 ellkr W LVec G F v L G v V G v = 0 ˙
39 7 8 38 syl2anc φ v L G v V G v = 0 ˙
40 32 37 39 3bitr4d φ v L G · ˙ f V × R v L G
41 40 eqrdv φ L G · ˙ f V × R = L G