Metamath Proof Explorer


Theorem eqlkr2

Description: Two functionals with the same kernel are the same up to a constant. (Contributed by NM, 10-Oct-2014)

Ref Expression
Hypotheses eqlkr.d D = Scalar W
eqlkr.k K = Base D
eqlkr.t · ˙ = D
eqlkr.v V = Base W
eqlkr.f F = LFnl W
eqlkr.l L = LKer W
Assertion eqlkr2 W LVec G F H F L G = L H r K H = G · ˙ f V × r

Proof

Step Hyp Ref Expression
1 eqlkr.d D = Scalar W
2 eqlkr.k K = Base D
3 eqlkr.t · ˙ = D
4 eqlkr.v V = Base W
5 eqlkr.f F = LFnl W
6 eqlkr.l L = LKer W
7 1 2 3 4 5 6 eqlkr W LVec G F H F L G = L H r K x V H x = G x · ˙ r
8 4 fvexi V V
9 8 a1i W LVec G F H F L G = L H r K V V
10 simpl1 W LVec G F H F L G = L H r K W LVec
11 simpl2l W LVec G F H F L G = L H r K G F
12 1 2 4 5 lflf W LVec G F G : V K
13 10 11 12 syl2anc W LVec G F H F L G = L H r K G : V K
14 13 ffnd W LVec G F H F L G = L H r K G Fn V
15 vex r V
16 fnconstg r V V × r Fn V
17 15 16 mp1i W LVec G F H F L G = L H r K V × r Fn V
18 simpl2r W LVec G F H F L G = L H r K H F
19 1 2 4 5 lflf W LVec H F H : V K
20 10 18 19 syl2anc W LVec G F H F L G = L H r K H : V K
21 20 ffnd W LVec G F H F L G = L H r K H Fn V
22 eqidd W LVec G F H F L G = L H r K x V G x = G x
23 15 fvconst2 x V V × r x = r
24 23 adantl W LVec G F H F L G = L H r K x V V × r x = r
25 9 14 17 21 22 24 offveqb W LVec G F H F L G = L H r K H = G · ˙ f V × r x V H x = G x · ˙ r
26 25 rexbidva W LVec G F H F L G = L H r K H = G · ˙ f V × r r K x V H x = G x · ˙ r
27 7 26 mpbird W LVec G F H F L G = L H r K H = G · ˙ f V × r