Mathbox for Norm Megill < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  lfli Structured version   Unicode version

Theorem lfli 29859
 Description: Property of a linear functional. (lnfnli 23543 analog.) (Contributed by NM, 16-Apr-2014.)
Hypotheses
Ref Expression
lflset.v
lflset.a
lflset.d Scalar
lflset.s
lflset.k
lflset.p
lflset.t
lflset.f LFnl
Assertion
Ref Expression
lfli

Proof of Theorem lfli
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 lflset.v . . . . 5
2 lflset.a . . . . 5
3 lflset.d . . . . 5 Scalar
4 lflset.s . . . . 5
5 lflset.k . . . . 5
6 lflset.p . . . . 5
7 lflset.t . . . . 5
8 lflset.f . . . . 5 LFnl
91, 2, 3, 4, 5, 6, 7, 8islfl 29858 . . . 4
109simplbda 608 . . 3
12 oveq1 6088 . . . . . . 7
1312oveq1d 6096 . . . . . 6
1413fveq2d 5732 . . . . 5
15 oveq1 6088 . . . . . 6
1615oveq1d 6096 . . . . 5
1714, 16eqeq12d 2450 . . . 4
18 oveq2 6089 . . . . . . 7
1918oveq1d 6096 . . . . . 6
2019fveq2d 5732 . . . . 5
21 fveq2 5728 . . . . . . 7
2221oveq2d 6097 . . . . . 6
2322oveq1d 6096 . . . . 5
2420, 23eqeq12d 2450 . . . 4
25 oveq2 6089 . . . . . 6
2625fveq2d 5732 . . . . 5
27 fveq2 5728 . . . . . 6
2827oveq2d 6097 . . . . 5
2926, 28eqeq12d 2450 . . . 4
3017, 24, 29rspc3v 3061 . . 3