Metamath Proof Explorer


Theorem islfl

Description: The predicate "is a linear functional". (Contributed by NM, 15-Apr-2014)

Ref Expression
Hypotheses lflset.v V = Base W
lflset.a + ˙ = + W
lflset.d D = Scalar W
lflset.s · ˙ = W
lflset.k K = Base D
lflset.p ˙ = + D
lflset.t × ˙ = D
lflset.f F = LFnl W
Assertion islfl W X G F G : V K r K x V y V G r · ˙ x + ˙ y = r × ˙ G x ˙ G y

Proof

Step Hyp Ref Expression
1 lflset.v V = Base W
2 lflset.a + ˙ = + W
3 lflset.d D = Scalar W
4 lflset.s · ˙ = W
5 lflset.k K = Base D
6 lflset.p ˙ = + D
7 lflset.t × ˙ = D
8 lflset.f F = LFnl W
9 1 2 3 4 5 6 7 8 lflset W X F = f K V | r K x V y V f r · ˙ x + ˙ y = r × ˙ f x ˙ f y
10 9 eleq2d W X G F G f K V | r K x V y V f r · ˙ x + ˙ y = r × ˙ f x ˙ f y
11 fveq1 f = G f r · ˙ x + ˙ y = G r · ˙ x + ˙ y
12 fveq1 f = G f x = G x
13 12 oveq2d f = G r × ˙ f x = r × ˙ G x
14 fveq1 f = G f y = G y
15 13 14 oveq12d f = G r × ˙ f x ˙ f y = r × ˙ G x ˙ G y
16 11 15 eqeq12d f = G f r · ˙ x + ˙ y = r × ˙ f x ˙ f y G r · ˙ x + ˙ y = r × ˙ G x ˙ G y
17 16 2ralbidv f = G x V y V f r · ˙ x + ˙ y = r × ˙ f x ˙ f y x V y V G r · ˙ x + ˙ y = r × ˙ G x ˙ G y
18 17 ralbidv f = G r K x V y V f r · ˙ x + ˙ y = r × ˙ f x ˙ f y r K x V y V G r · ˙ x + ˙ y = r × ˙ G x ˙ G y
19 18 elrab G f K V | r K x V y V f r · ˙ x + ˙ y = r × ˙ f x ˙ f y G K V r K x V y V G r · ˙ x + ˙ y = r × ˙ G x ˙ G y
20 5 fvexi K V
21 1 fvexi V V
22 20 21 elmap G K V G : V K
23 22 anbi1i G K V r K x V y V G r · ˙ x + ˙ y = r × ˙ G x ˙ G y G : V K r K x V y V G r · ˙ x + ˙ y = r × ˙ G x ˙ G y
24 19 23 bitri G f K V | r K x V y V f r · ˙ x + ˙ y = r × ˙ f x ˙ f y G : V K r K x V y V G r · ˙ x + ˙ y = r × ˙ G x ˙ G y
25 10 24 bitrdi W X G F G : V K r K x V y V G r · ˙ x + ˙ y = r × ˙ G x ˙ G y