Metamath Proof Explorer


Theorem islfl

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

Ref Expression
Hypotheses lflset.v 𝑉 = ( Base ‘ 𝑊 )
lflset.a + = ( +g𝑊 )
lflset.d 𝐷 = ( Scalar ‘ 𝑊 )
lflset.s · = ( ·𝑠𝑊 )
lflset.k 𝐾 = ( Base ‘ 𝐷 )
lflset.p = ( +g𝐷 )
lflset.t × = ( .r𝐷 )
lflset.f 𝐹 = ( LFnl ‘ 𝑊 )
Assertion islfl ( 𝑊𝑋 → ( 𝐺𝐹 ↔ ( 𝐺 : 𝑉𝐾 ∧ ∀ 𝑟𝐾𝑥𝑉𝑦𝑉 ( 𝐺 ‘ ( ( 𝑟 · 𝑥 ) + 𝑦 ) ) = ( ( 𝑟 × ( 𝐺𝑥 ) ) ( 𝐺𝑦 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 lflset.v 𝑉 = ( Base ‘ 𝑊 )
2 lflset.a + = ( +g𝑊 )
3 lflset.d 𝐷 = ( Scalar ‘ 𝑊 )
4 lflset.s · = ( ·𝑠𝑊 )
5 lflset.k 𝐾 = ( Base ‘ 𝐷 )
6 lflset.p = ( +g𝐷 )
7 lflset.t × = ( .r𝐷 )
8 lflset.f 𝐹 = ( LFnl ‘ 𝑊 )
9 1 2 3 4 5 6 7 8 lflset ( 𝑊𝑋𝐹 = { 𝑓 ∈ ( 𝐾m 𝑉 ) ∣ ∀ 𝑟𝐾𝑥𝑉𝑦𝑉 ( 𝑓 ‘ ( ( 𝑟 · 𝑥 ) + 𝑦 ) ) = ( ( 𝑟 × ( 𝑓𝑥 ) ) ( 𝑓𝑦 ) ) } )
10 9 eleq2d ( 𝑊𝑋 → ( 𝐺𝐹𝐺 ∈ { 𝑓 ∈ ( 𝐾m 𝑉 ) ∣ ∀ 𝑟𝐾𝑥𝑉𝑦𝑉 ( 𝑓 ‘ ( ( 𝑟 · 𝑥 ) + 𝑦 ) ) = ( ( 𝑟 × ( 𝑓𝑥 ) ) ( 𝑓𝑦 ) ) } ) )
11 fveq1 ( 𝑓 = 𝐺 → ( 𝑓 ‘ ( ( 𝑟 · 𝑥 ) + 𝑦 ) ) = ( 𝐺 ‘ ( ( 𝑟 · 𝑥 ) + 𝑦 ) ) )
12 fveq1 ( 𝑓 = 𝐺 → ( 𝑓𝑥 ) = ( 𝐺𝑥 ) )
13 12 oveq2d ( 𝑓 = 𝐺 → ( 𝑟 × ( 𝑓𝑥 ) ) = ( 𝑟 × ( 𝐺𝑥 ) ) )
14 fveq1 ( 𝑓 = 𝐺 → ( 𝑓𝑦 ) = ( 𝐺𝑦 ) )
15 13 14 oveq12d ( 𝑓 = 𝐺 → ( ( 𝑟 × ( 𝑓𝑥 ) ) ( 𝑓𝑦 ) ) = ( ( 𝑟 × ( 𝐺𝑥 ) ) ( 𝐺𝑦 ) ) )
16 11 15 eqeq12d ( 𝑓 = 𝐺 → ( ( 𝑓 ‘ ( ( 𝑟 · 𝑥 ) + 𝑦 ) ) = ( ( 𝑟 × ( 𝑓𝑥 ) ) ( 𝑓𝑦 ) ) ↔ ( 𝐺 ‘ ( ( 𝑟 · 𝑥 ) + 𝑦 ) ) = ( ( 𝑟 × ( 𝐺𝑥 ) ) ( 𝐺𝑦 ) ) ) )
17 16 2ralbidv ( 𝑓 = 𝐺 → ( ∀ 𝑥𝑉𝑦𝑉 ( 𝑓 ‘ ( ( 𝑟 · 𝑥 ) + 𝑦 ) ) = ( ( 𝑟 × ( 𝑓𝑥 ) ) ( 𝑓𝑦 ) ) ↔ ∀ 𝑥𝑉𝑦𝑉 ( 𝐺 ‘ ( ( 𝑟 · 𝑥 ) + 𝑦 ) ) = ( ( 𝑟 × ( 𝐺𝑥 ) ) ( 𝐺𝑦 ) ) ) )
18 17 ralbidv ( 𝑓 = 𝐺 → ( ∀ 𝑟𝐾𝑥𝑉𝑦𝑉 ( 𝑓 ‘ ( ( 𝑟 · 𝑥 ) + 𝑦 ) ) = ( ( 𝑟 × ( 𝑓𝑥 ) ) ( 𝑓𝑦 ) ) ↔ ∀ 𝑟𝐾𝑥𝑉𝑦𝑉 ( 𝐺 ‘ ( ( 𝑟 · 𝑥 ) + 𝑦 ) ) = ( ( 𝑟 × ( 𝐺𝑥 ) ) ( 𝐺𝑦 ) ) ) )
19 18 elrab ( 𝐺 ∈ { 𝑓 ∈ ( 𝐾m 𝑉 ) ∣ ∀ 𝑟𝐾𝑥𝑉𝑦𝑉 ( 𝑓 ‘ ( ( 𝑟 · 𝑥 ) + 𝑦 ) ) = ( ( 𝑟 × ( 𝑓𝑥 ) ) ( 𝑓𝑦 ) ) } ↔ ( 𝐺 ∈ ( 𝐾m 𝑉 ) ∧ ∀ 𝑟𝐾𝑥𝑉𝑦𝑉 ( 𝐺 ‘ ( ( 𝑟 · 𝑥 ) + 𝑦 ) ) = ( ( 𝑟 × ( 𝐺𝑥 ) ) ( 𝐺𝑦 ) ) ) )
20 5 fvexi 𝐾 ∈ V
21 1 fvexi 𝑉 ∈ V
22 20 21 elmap ( 𝐺 ∈ ( 𝐾m 𝑉 ) ↔ 𝐺 : 𝑉𝐾 )
23 22 anbi1i ( ( 𝐺 ∈ ( 𝐾m 𝑉 ) ∧ ∀ 𝑟𝐾𝑥𝑉𝑦𝑉 ( 𝐺 ‘ ( ( 𝑟 · 𝑥 ) + 𝑦 ) ) = ( ( 𝑟 × ( 𝐺𝑥 ) ) ( 𝐺𝑦 ) ) ) ↔ ( 𝐺 : 𝑉𝐾 ∧ ∀ 𝑟𝐾𝑥𝑉𝑦𝑉 ( 𝐺 ‘ ( ( 𝑟 · 𝑥 ) + 𝑦 ) ) = ( ( 𝑟 × ( 𝐺𝑥 ) ) ( 𝐺𝑦 ) ) ) )
24 19 23 bitri ( 𝐺 ∈ { 𝑓 ∈ ( 𝐾m 𝑉 ) ∣ ∀ 𝑟𝐾𝑥𝑉𝑦𝑉 ( 𝑓 ‘ ( ( 𝑟 · 𝑥 ) + 𝑦 ) ) = ( ( 𝑟 × ( 𝑓𝑥 ) ) ( 𝑓𝑦 ) ) } ↔ ( 𝐺 : 𝑉𝐾 ∧ ∀ 𝑟𝐾𝑥𝑉𝑦𝑉 ( 𝐺 ‘ ( ( 𝑟 · 𝑥 ) + 𝑦 ) ) = ( ( 𝑟 × ( 𝐺𝑥 ) ) ( 𝐺𝑦 ) ) ) )
25 10 24 bitrdi ( 𝑊𝑋 → ( 𝐺𝐹 ↔ ( 𝐺 : 𝑉𝐾 ∧ ∀ 𝑟𝐾𝑥𝑉𝑦𝑉 ( 𝐺 ‘ ( ( 𝑟 · 𝑥 ) + 𝑦 ) ) = ( ( 𝑟 × ( 𝐺𝑥 ) ) ( 𝐺𝑦 ) ) ) ) )