Metamath Proof Explorer


Theorem ldualkrsc

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

Ref Expression
Hypotheses ldualkrsc.r R = Scalar W
ldualkrsc.k K = Base R
ldualkrsc.o 0 ˙ = 0 R
ldualkrsc.f F = LFnl W
ldualkrsc.l L = LKer W
ldualkrsc.d D = LDual W
ldualkrsc.s · ˙ = D
ldualkrsc.w φ W LVec
ldualkrsc.g φ G F
ldualkrsc.x φ X K
ldualkrsc.e φ X 0 ˙
Assertion ldualkrsc φ L X · ˙ G = L G

Proof

Step Hyp Ref Expression
1 ldualkrsc.r R = Scalar W
2 ldualkrsc.k K = Base R
3 ldualkrsc.o 0 ˙ = 0 R
4 ldualkrsc.f F = LFnl W
5 ldualkrsc.l L = LKer W
6 ldualkrsc.d D = LDual W
7 ldualkrsc.s · ˙ = D
8 ldualkrsc.w φ W LVec
9 ldualkrsc.g φ G F
10 ldualkrsc.x φ X K
11 ldualkrsc.e φ X 0 ˙
12 eqid Base W = Base W
13 eqid R = R
14 4 12 1 2 13 6 7 8 10 9 ldualvs φ X · ˙ G = G R f Base W × X
15 14 fveq2d φ L X · ˙ G = L G R f Base W × X
16 12 1 2 13 4 5 8 9 10 3 11 lkrsc φ L G R f Base W × X = L G
17 15 16 eqtrd φ L X · ˙ G = L G