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 ⊢ ( 𝑊 ∈ 𝑋 → ( 𝐺 ∈ 𝐹 ↔ ( 𝐺 : 𝑉 ⟶ 𝐾 ∧ ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝐺 ‘ ( ( 𝑟 · 𝑥 ) + 𝑦 ) ) = ( ( 𝑟 × ( 𝐺 ‘ 𝑥 ) ) ⨣ ( 𝐺 ‘ 𝑦 ) ) ) ) )