Metamath Proof Explorer

Theorem islfld

Description: Properties that determine a linear functional. TODO: use this in place of islfl when it shortens the proof. (Contributed by NM, 19-Oct-2014)

Ref Expression
Hypotheses islfld.v ⊢ ( 𝜑 → 𝑉 = ( Base ‘ 𝑊 ) )
islfld.a ⊢ ( 𝜑 → + = ( +g ‘ 𝑊 ) )
islfld.d ⊢ ( 𝜑 → 𝐷 = ( Scalar ‘ 𝑊 ) )
islfld.s ⊢ ( 𝜑 → · = ( ·𝑠 ‘ 𝑊 ) )
islfld.k ⊢ ( 𝜑 → 𝐾 = ( Base ‘ 𝐷 ) )
islfld.p ⊢ ( 𝜑 → ⨣ = ( +g ‘ 𝐷 ) )
islfld.t ⊢ ( 𝜑 → × = ( .r ‘ 𝐷 ) )
islfld.f ⊢ ( 𝜑 → 𝐹 = ( LFnl ‘ 𝑊 ) )
islfld.u ⊢ ( 𝜑 → 𝐺 : 𝑉 ⟶ 𝐾 )
islfld.l ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝐾 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → ( 𝐺 ‘ ( ( 𝑟 · 𝑥 ) + 𝑦 ) ) = ( ( 𝑟 × ( 𝐺 ‘ 𝑥 ) ) ⨣ ( 𝐺 ‘ 𝑦 ) ) )
islfld.w ⊢ ( 𝜑 → 𝑊 ∈ 𝑋 )
Assertion islfld ( 𝜑 → 𝐺 ∈ 𝐹 )

Proof

Step Hyp Ref Expression
1 islfld.v ⊢ ( 𝜑 → 𝑉 = ( Base ‘ 𝑊 ) )
2 islfld.a ⊢ ( 𝜑 → + = ( +g ‘ 𝑊 ) )
3 islfld.d ⊢ ( 𝜑 → 𝐷 = ( Scalar ‘ 𝑊 ) )
4 islfld.s ⊢ ( 𝜑 → · = ( ·𝑠 ‘ 𝑊 ) )
5 islfld.k ⊢ ( 𝜑 → 𝐾 = ( Base ‘ 𝐷 ) )
6 islfld.p ⊢ ( 𝜑 → ⨣ = ( +g ‘ 𝐷 ) )
7 islfld.t ⊢ ( 𝜑 → × = ( .r ‘ 𝐷 ) )
8 islfld.f ⊢ ( 𝜑 → 𝐹 = ( LFnl ‘ 𝑊 ) )
9 islfld.u ⊢ ( 𝜑 → 𝐺 : 𝑉 ⟶ 𝐾 )
10 islfld.l ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝐾 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → ( 𝐺 ‘ ( ( 𝑟 · 𝑥 ) + 𝑦 ) ) = ( ( 𝑟 × ( 𝐺 ‘ 𝑥 ) ) ⨣ ( 𝐺 ‘ 𝑦 ) ) )
11 islfld.w ⊢ ( 𝜑 → 𝑊 ∈ 𝑋 )
12 3 fveq2d ⊢ ( 𝜑 → ( Base ‘ 𝐷 ) = ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
13 5 12 eqtrd ⊢ ( 𝜑 → 𝐾 = ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
14 1 13 feq23d ⊢ ( 𝜑 → ( 𝐺 : 𝑉 ⟶ 𝐾 ↔ 𝐺 : ( Base ‘ 𝑊 ) ⟶ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) )
15 9 14 mpbid ⊢ ( 𝜑 → 𝐺 : ( Base ‘ 𝑊 ) ⟶ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
16 10 ralrimivvva ⊢ ( 𝜑 → ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝐺 ‘ ( ( 𝑟 · 𝑥 ) + 𝑦 ) ) = ( ( 𝑟 × ( 𝐺 ‘ 𝑥 ) ) ⨣ ( 𝐺 ‘ 𝑦 ) ) )
17 4 oveqd ⊢ ( 𝜑 → ( 𝑟 · 𝑥 ) = ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) )
18 eqidd ⊢ ( 𝜑 → 𝑦 = 𝑦 )
19 2 17 18 oveq123d ⊢ ( 𝜑 → ( ( 𝑟 · 𝑥 ) + 𝑦 ) = ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ( +g ‘ 𝑊 ) 𝑦 ) )
20 19 fveq2d ⊢ ( 𝜑 → ( 𝐺 ‘ ( ( 𝑟 · 𝑥 ) + 𝑦 ) ) = ( 𝐺 ‘ ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ( +g ‘ 𝑊 ) 𝑦 ) ) )
21 3 fveq2d ⊢ ( 𝜑 → ( +g ‘ 𝐷 ) = ( +g ‘ ( Scalar ‘ 𝑊 ) ) )
22 6 21 eqtrd ⊢ ( 𝜑 → ⨣ = ( +g ‘ ( Scalar ‘ 𝑊 ) ) )
23 3 fveq2d ⊢ ( 𝜑 → ( .r ‘ 𝐷 ) = ( .r ‘ ( Scalar ‘ 𝑊 ) ) )
24 7 23 eqtrd ⊢ ( 𝜑 → × = ( .r ‘ ( Scalar ‘ 𝑊 ) ) )
25 24 oveqd ⊢ ( 𝜑 → ( 𝑟 × ( 𝐺 ‘ 𝑥 ) ) = ( 𝑟 ( .r ‘ ( Scalar ‘ 𝑊 ) ) ( 𝐺 ‘ 𝑥 ) ) )
26 eqidd ⊢ ( 𝜑 → ( 𝐺 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑦 ) )
27 22 25 26 oveq123d ⊢ ( 𝜑 → ( ( 𝑟 × ( 𝐺 ‘ 𝑥 ) ) ⨣ ( 𝐺 ‘ 𝑦 ) ) = ( ( 𝑟 ( .r ‘ ( Scalar ‘ 𝑊 ) ) ( 𝐺 ‘ 𝑥 ) ) ( +g ‘ ( Scalar ‘ 𝑊 ) ) ( 𝐺 ‘ 𝑦 ) ) )
28 20 27 eqeq12d ⊢ ( 𝜑 → ( ( 𝐺 ‘ ( ( 𝑟 · 𝑥 ) + 𝑦 ) ) = ( ( 𝑟 × ( 𝐺 ‘ 𝑥 ) ) ⨣ ( 𝐺 ‘ 𝑦 ) ) ↔ ( 𝐺 ‘ ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ( +g ‘ 𝑊 ) 𝑦 ) ) = ( ( 𝑟 ( .r ‘ ( Scalar ‘ 𝑊 ) ) ( 𝐺 ‘ 𝑥 ) ) ( +g ‘ ( Scalar ‘ 𝑊 ) ) ( 𝐺 ‘ 𝑦 ) ) ) )
29 1 28 raleqbidv ⊢ ( 𝜑 → ( ∀ 𝑦 ∈ 𝑉 ( 𝐺 ‘ ( ( 𝑟 · 𝑥 ) + 𝑦 ) ) = ( ( 𝑟 × ( 𝐺 ‘ 𝑥 ) ) ⨣ ( 𝐺 ‘ 𝑦 ) ) ↔ ∀ 𝑦 ∈ ( Base ‘ 𝑊 ) ( 𝐺 ‘ ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ( +g ‘ 𝑊 ) 𝑦 ) ) = ( ( 𝑟 ( .r ‘ ( Scalar ‘ 𝑊 ) ) ( 𝐺 ‘ 𝑥 ) ) ( +g ‘ ( Scalar ‘ 𝑊 ) ) ( 𝐺 ‘ 𝑦 ) ) ) )
30 1 29 raleqbidv ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝐺 ‘ ( ( 𝑟 · 𝑥 ) + 𝑦 ) ) = ( ( 𝑟 × ( 𝐺 ‘ 𝑥 ) ) ⨣ ( 𝐺 ‘ 𝑦 ) ) ↔ ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ∀ 𝑦 ∈ ( Base ‘ 𝑊 ) ( 𝐺 ‘ ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ( +g ‘ 𝑊 ) 𝑦 ) ) = ( ( 𝑟 ( .r ‘ ( Scalar ‘ 𝑊 ) ) ( 𝐺 ‘ 𝑥 ) ) ( +g ‘ ( Scalar ‘ 𝑊 ) ) ( 𝐺 ‘ 𝑦 ) ) ) )
31 13 30 raleqbidv ⊢ ( 𝜑 → ( ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝐺 ‘ ( ( 𝑟 · 𝑥 ) + 𝑦 ) ) = ( ( 𝑟 × ( 𝐺 ‘ 𝑥 ) ) ⨣ ( 𝐺 ‘ 𝑦 ) ) ↔ ∀ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ∀ 𝑦 ∈ ( Base ‘ 𝑊 ) ( 𝐺 ‘ ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ( +g ‘ 𝑊 ) 𝑦 ) ) = ( ( 𝑟 ( .r ‘ ( Scalar ‘ 𝑊 ) ) ( 𝐺 ‘ 𝑥 ) ) ( +g ‘ ( Scalar ‘ 𝑊 ) ) ( 𝐺 ‘ 𝑦 ) ) ) )
32 16 31 mpbid ⊢ ( 𝜑 → ∀ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ∀ 𝑦 ∈ ( Base ‘ 𝑊 ) ( 𝐺 ‘ ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ( +g ‘ 𝑊 ) 𝑦 ) ) = ( ( 𝑟 ( .r ‘ ( Scalar ‘ 𝑊 ) ) ( 𝐺 ‘ 𝑥 ) ) ( +g ‘ ( Scalar ‘ 𝑊 ) ) ( 𝐺 ‘ 𝑦 ) ) )
33 eqid ⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
34 eqid ⊢ ( +g ‘ 𝑊 ) = ( +g ‘ 𝑊 )
35 eqid ⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
36 eqid ⊢ ( ·𝑠 ‘ 𝑊 ) = ( ·𝑠 ‘ 𝑊 )
37 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑊 ) ) = ( Base ‘ ( Scalar ‘ 𝑊 ) )
38 eqid ⊢ ( +g ‘ ( Scalar ‘ 𝑊 ) ) = ( +g ‘ ( Scalar ‘ 𝑊 ) )
39 eqid ⊢ ( .r ‘ ( Scalar ‘ 𝑊 ) ) = ( .r ‘ ( Scalar ‘ 𝑊 ) )
40 eqid ⊢ ( LFnl ‘ 𝑊 ) = ( LFnl ‘ 𝑊 )
41 33 34 35 36 37 38 39 40 islfl ⊢ ( 𝑊 ∈ 𝑋 → ( 𝐺 ∈ ( LFnl ‘ 𝑊 ) ↔ ( 𝐺 : ( Base ‘ 𝑊 ) ⟶ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ ∀ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ∀ 𝑦 ∈ ( Base ‘ 𝑊 ) ( 𝐺 ‘ ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ( +g ‘ 𝑊 ) 𝑦 ) ) = ( ( 𝑟 ( .r ‘ ( Scalar ‘ 𝑊 ) ) ( 𝐺 ‘ 𝑥 ) ) ( +g ‘ ( Scalar ‘ 𝑊 ) ) ( 𝐺 ‘ 𝑦 ) ) ) ) )
42 41 biimpar ⊢ ( ( 𝑊 ∈ 𝑋 ∧ ( 𝐺 : ( Base ‘ 𝑊 ) ⟶ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ ∀ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ∀ 𝑦 ∈ ( Base ‘ 𝑊 ) ( 𝐺 ‘ ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ( +g ‘ 𝑊 ) 𝑦 ) ) = ( ( 𝑟 ( .r ‘ ( Scalar ‘ 𝑊 ) ) ( 𝐺 ‘ 𝑥 ) ) ( +g ‘ ( Scalar ‘ 𝑊 ) ) ( 𝐺 ‘ 𝑦 ) ) ) ) → 𝐺 ∈ ( LFnl ‘ 𝑊 ) )
43 11 15 32 42 syl12anc ⊢ ( 𝜑 → 𝐺 ∈ ( LFnl ‘ 𝑊 ) )
44 43 8 eleqtrrd ⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )