Theorem lflf 39010

Description: A linear functional is a function from vectors to scalars. (lnfnfi 31956 analog.) (Contributed by NM, 15-Apr-2014.)

Hypotheses

Ref	Expression
lflf.d	⊢ 𝐷 = (Scalar‘𝑊)
lflf.k	⊢ 𝐾 = (Base‘𝐷)
lflf.v	⊢ 𝑉 = (Base‘𝑊)
lflf.f	⊢ 𝐹 = (LFnl‘𝑊)

Assertion

Ref	Expression
lflf	⊢ ((𝑊 ∈ 𝑋 ∧ 𝐺 ∈ 𝐹) → 𝐺:𝑉⟶𝐾)

Proof of Theorem lflf

Dummy variables 𝑥 𝑟 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		lflf.v	. . 3 ⊢ 𝑉 = (Base‘𝑊)
2		eqid 2734	. . 3 ⊢ (+g‘𝑊) = (+g‘𝑊)
3		lflf.d	. . 3 ⊢ 𝐷 = (Scalar‘𝑊)
4		eqid 2734	. . 3 ⊢ ( ·𝑠 ‘𝑊) = ( ·𝑠 ‘𝑊)
5		lflf.k	. . 3 ⊢ 𝐾 = (Base‘𝐷)
6		eqid 2734	. . 3 ⊢ (+g‘𝐷) = (+g‘𝐷)
7		eqid 2734	. . 3 ⊢ (.r‘𝐷) = (.r‘𝐷)
8		lflf.f	. . 3 ⊢ 𝐹 = (LFnl‘𝑊)
9	1, 2, 3, 4, 5, 6, 7, 8	islfl 39007	. 2 ⊢ (𝑊 ∈ 𝑋 → (𝐺 ∈ 𝐹 ↔ (𝐺:𝑉⟶𝐾 ∧ ∀𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 (𝐺‘((𝑟( ·𝑠 ‘𝑊)𝑥)(+g‘𝑊)𝑦)) = ((𝑟(.r‘𝐷)(𝐺‘𝑥))(+g‘𝐷)(𝐺‘𝑦)))))
10	9	simprbda 498	1 ⊢ ((𝑊 ∈ 𝑋 ∧ 𝐺 ∈ 𝐹) → 𝐺:𝑉⟶𝐾)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1539   ∈ wcel 2107  ∀wral 3050  ⟶wf 6524  ‘cfv 6528  (class class class)co 7400  Basecbs 17215  +_gcplusg 17258  ._rcmulr 17259  Scalarcsca 17261   ·_𝑠 cvsca 17262  LFnlclfn 39004

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2706  ax-sep 5264  ax-nul 5274  ax-pow 5333  ax-pr 5400  ax-un 7724

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2808  df-nfc 2884  df-ne 2932  df-ral 3051  df-rex 3060  df-rab 3414  df-v 3459  df-sbc 3764  df-dif 3927  df-un 3929  df-in 3931  df-ss 3941  df-nul 4307  df-if 4499  df-pw 4575  df-sn 4600  df-pr 4602  df-op 4606  df-uni 4882  df-br 5118  df-opab 5180  df-mpt 5200  df-id 5546  df-xp 5658  df-rel 5659  df-cnv 5660  df-co 5661  df-dm 5662  df-rn 5663  df-iota 6481  df-fun 6530  df-fn 6531  df-f 6532  df-fv 6536  df-ov 7403  df-oprab 7404  df-mpo 7405  df-map 8837  df-lfl 39005

This theorem is referenced by:  lflcl  39011  lfl1  39017  lfladdcl  39018  lfladdcom  39019  lfladdass  39020  lfladd0l  39021  lflnegl  39023  lflvscl  39024  lflvsdi1  39025  lflvsdi2  39026  lflvsass  39028  lfl0sc  39029  lfl1sc  39031  ellkr  39036  lkr0f  39041  lkrsc  39044  eqlkr2  39047  eqlkr3  39048  ldualvaddval  39078  ldualvsval  39085