Metamath Proof Explorer


Theorem ellkr

Description: Membership in the kernel of a functional. ( elnlfn analog.) (Contributed by NM, 16-Apr-2014)

Ref Expression
Hypotheses lkrfval2.v V = Base W
lkrfval2.d D = Scalar W
lkrfval2.o 0 ˙ = 0 D
lkrfval2.f F = LFnl W
lkrfval2.k K = LKer W
Assertion ellkr W Y G F X K G X V G X = 0 ˙

Proof

Step Hyp Ref Expression
1 lkrfval2.v V = Base W
2 lkrfval2.d D = Scalar W
3 lkrfval2.o 0 ˙ = 0 D
4 lkrfval2.f F = LFnl W
5 lkrfval2.k K = LKer W
6 2 3 4 5 lkrval W Y G F K G = G -1 0 ˙
7 6 eleq2d W Y G F X K G X G -1 0 ˙
8 eqid Base D = Base D
9 2 8 1 4 lflf W Y G F G : V Base D
10 ffn G : V Base D G Fn V
11 elpreima G Fn V X G -1 0 ˙ X V G X 0 ˙
12 9 10 11 3syl W Y G F X G -1 0 ˙ X V G X 0 ˙
13 fvex G X V
14 13 elsn G X 0 ˙ G X = 0 ˙
15 14 anbi2i X V G X 0 ˙ X V G X = 0 ˙
16 12 15 bitrdi W Y G F X G -1 0 ˙ X V G X = 0 ˙
17 7 16 bitrd W Y G F X K G X V G X = 0 ˙