Mathbox for Norm Megill < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ldualset Structured version   Visualization version   GIF version

Theorem ldualset 36572
 Description: Define the (left) dual of a left vector space (or module) in which the vectors are functionals. In many texts, this is defined as a right vector space, but by reversing the multiplication we achieve a left vector space, as is done in definition of dual vector space in [Holland95] p. 218. This allows us to reuse our existing collection of left vector space theorems. Note the operation reversal in the scalar product to allow us to use the original scalar ring instead of the oppr ring, for convenience. (Contributed by NM, 18-Oct-2014.)
Hypotheses
Ref Expression
ldualset.v 𝑉 = (Base‘𝑊)
ldualset.a + = (+g𝑅)
ldualset.p = ( ∘f + ↾ (𝐹 × 𝐹))
ldualset.f 𝐹 = (LFnl‘𝑊)
ldualset.d 𝐷 = (LDual‘𝑊)
ldualset.r 𝑅 = (Scalar‘𝑊)
ldualset.k 𝐾 = (Base‘𝑅)
ldualset.t · = (.r𝑅)
ldualset.o 𝑂 = (oppr𝑅)
ldualset.s = (𝑘𝐾, 𝑓𝐹 ↦ (𝑓f · (𝑉 × {𝑘})))
ldualset.w (𝜑𝑊𝑋)
Assertion
Ref Expression
ldualset (𝜑𝐷 = ({⟨(Base‘ndx), 𝐹⟩, ⟨(+g‘ndx), ⟩, ⟨(Scalar‘ndx), 𝑂⟩} ∪ {⟨( ·𝑠 ‘ndx), ⟩}))
Distinct variable group:   𝑓,𝑘,𝑊
Allowed substitution hints:   𝜑(𝑓,𝑘)   𝐷(𝑓,𝑘)   + (𝑓,𝑘)   (𝑓,𝑘)   𝑅(𝑓,𝑘)   (𝑓,𝑘)   · (𝑓,𝑘)   𝐹(𝑓,𝑘)   𝐾(𝑓,𝑘)   𝑂(𝑓,𝑘)   𝑉(𝑓,𝑘)   𝑋(𝑓,𝑘)

Proof of Theorem ldualset
Dummy variable 𝑤 is distinct from all other variables.
StepHypRef Expression
1 ldualset.w . 2 (𝜑𝑊𝑋)
2 elex 3460 . 2 (𝑊𝑋𝑊 ∈ V)
3 ldualset.d . . 3 𝐷 = (LDual‘𝑊)
4 fveq2 6655 . . . . . . . 8 (𝑤 = 𝑊 → (LFnl‘𝑤) = (LFnl‘𝑊))
5 ldualset.f . . . . . . . 8 𝐹 = (LFnl‘𝑊)
64, 5eqtr4di 2851 . . . . . . 7 (𝑤 = 𝑊 → (LFnl‘𝑤) = 𝐹)
76opeq2d 4776 . . . . . 6 (𝑤 = 𝑊 → ⟨(Base‘ndx), (LFnl‘𝑤)⟩ = ⟨(Base‘ndx), 𝐹⟩)
8 fveq2 6655 . . . . . . . . . . . . 13 (𝑤 = 𝑊 → (Scalar‘𝑤) = (Scalar‘𝑊))
9 ldualset.r . . . . . . . . . . . . 13 𝑅 = (Scalar‘𝑊)
108, 9eqtr4di 2851 . . . . . . . . . . . 12 (𝑤 = 𝑊 → (Scalar‘𝑤) = 𝑅)
1110fveq2d 6659 . . . . . . . . . . 11 (𝑤 = 𝑊 → (+g‘(Scalar‘𝑤)) = (+g𝑅))
12 ldualset.a . . . . . . . . . . 11 + = (+g𝑅)
1311, 12eqtr4di 2851 . . . . . . . . . 10 (𝑤 = 𝑊 → (+g‘(Scalar‘𝑤)) = + )
14 ofeq 7402 . . . . . . . . . 10 ((+g‘(Scalar‘𝑤)) = + → ∘f (+g‘(Scalar‘𝑤)) = ∘f + )
1513, 14syl 17 . . . . . . . . 9 (𝑤 = 𝑊 → ∘f (+g‘(Scalar‘𝑤)) = ∘f + )
166sqxpeqd 5555 . . . . . . . . 9 (𝑤 = 𝑊 → ((LFnl‘𝑤) × (LFnl‘𝑤)) = (𝐹 × 𝐹))
1715, 16reseq12d 5823 . . . . . . . 8 (𝑤 = 𝑊 → ( ∘f (+g‘(Scalar‘𝑤)) ↾ ((LFnl‘𝑤) × (LFnl‘𝑤))) = ( ∘f + ↾ (𝐹 × 𝐹)))
18 ldualset.p . . . . . . . 8 = ( ∘f + ↾ (𝐹 × 𝐹))
1917, 18eqtr4di 2851 . . . . . . 7 (𝑤 = 𝑊 → ( ∘f (+g‘(Scalar‘𝑤)) ↾ ((LFnl‘𝑤) × (LFnl‘𝑤))) = )
2019opeq2d 4776 . . . . . 6 (𝑤 = 𝑊 → ⟨(+g‘ndx), ( ∘f (+g‘(Scalar‘𝑤)) ↾ ((LFnl‘𝑤) × (LFnl‘𝑤)))⟩ = ⟨(+g‘ndx), ⟩)
2110fveq2d 6659 . . . . . . . 8 (𝑤 = 𝑊 → (oppr‘(Scalar‘𝑤)) = (oppr𝑅))
22 ldualset.o . . . . . . . 8 𝑂 = (oppr𝑅)
2321, 22eqtr4di 2851 . . . . . . 7 (𝑤 = 𝑊 → (oppr‘(Scalar‘𝑤)) = 𝑂)
2423opeq2d 4776 . . . . . 6 (𝑤 = 𝑊 → ⟨(Scalar‘ndx), (oppr‘(Scalar‘𝑤))⟩ = ⟨(Scalar‘ndx), 𝑂⟩)
257, 20, 24tpeq123d 4647 . . . . 5 (𝑤 = 𝑊 → {⟨(Base‘ndx), (LFnl‘𝑤)⟩, ⟨(+g‘ndx), ( ∘f (+g‘(Scalar‘𝑤)) ↾ ((LFnl‘𝑤) × (LFnl‘𝑤)))⟩, ⟨(Scalar‘ndx), (oppr‘(Scalar‘𝑤))⟩} = {⟨(Base‘ndx), 𝐹⟩, ⟨(+g‘ndx), ⟩, ⟨(Scalar‘ndx), 𝑂⟩})
2610fveq2d 6659 . . . . . . . . . 10 (𝑤 = 𝑊 → (Base‘(Scalar‘𝑤)) = (Base‘𝑅))
27 ldualset.k . . . . . . . . . 10 𝐾 = (Base‘𝑅)
2826, 27eqtr4di 2851 . . . . . . . . 9 (𝑤 = 𝑊 → (Base‘(Scalar‘𝑤)) = 𝐾)
2910fveq2d 6659 . . . . . . . . . . . 12 (𝑤 = 𝑊 → (.r‘(Scalar‘𝑤)) = (.r𝑅))
30 ldualset.t . . . . . . . . . . . 12 · = (.r𝑅)
3129, 30eqtr4di 2851 . . . . . . . . . . 11 (𝑤 = 𝑊 → (.r‘(Scalar‘𝑤)) = · )
32 ofeq 7402 . . . . . . . . . . 11 ((.r‘(Scalar‘𝑤)) = · → ∘f (.r‘(Scalar‘𝑤)) = ∘f · )
3331, 32syl 17 . . . . . . . . . 10 (𝑤 = 𝑊 → ∘f (.r‘(Scalar‘𝑤)) = ∘f · )
34 eqidd 2799 . . . . . . . . . 10 (𝑤 = 𝑊𝑓 = 𝑓)
35 fveq2 6655 . . . . . . . . . . . 12 (𝑤 = 𝑊 → (Base‘𝑤) = (Base‘𝑊))
36 ldualset.v . . . . . . . . . . . 12 𝑉 = (Base‘𝑊)
3735, 36eqtr4di 2851 . . . . . . . . . . 11 (𝑤 = 𝑊 → (Base‘𝑤) = 𝑉)
3837xpeq1d 5552 . . . . . . . . . 10 (𝑤 = 𝑊 → ((Base‘𝑤) × {𝑘}) = (𝑉 × {𝑘}))
3933, 34, 38oveq123d 7166 . . . . . . . . 9 (𝑤 = 𝑊 → (𝑓f (.r‘(Scalar‘𝑤))((Base‘𝑤) × {𝑘})) = (𝑓f · (𝑉 × {𝑘})))
4028, 6, 39mpoeq123dv 7218 . . . . . . . 8 (𝑤 = 𝑊 → (𝑘 ∈ (Base‘(Scalar‘𝑤)), 𝑓 ∈ (LFnl‘𝑤) ↦ (𝑓f (.r‘(Scalar‘𝑤))((Base‘𝑤) × {𝑘}))) = (𝑘𝐾, 𝑓𝐹 ↦ (𝑓f · (𝑉 × {𝑘}))))
41 ldualset.s . . . . . . . 8 = (𝑘𝐾, 𝑓𝐹 ↦ (𝑓f · (𝑉 × {𝑘})))
4240, 41eqtr4di 2851 . . . . . . 7 (𝑤 = 𝑊 → (𝑘 ∈ (Base‘(Scalar‘𝑤)), 𝑓 ∈ (LFnl‘𝑤) ↦ (𝑓f (.r‘(Scalar‘𝑤))((Base‘𝑤) × {𝑘}))) = )
4342opeq2d 4776 . . . . . 6 (𝑤 = 𝑊 → ⟨( ·𝑠 ‘ndx), (𝑘 ∈ (Base‘(Scalar‘𝑤)), 𝑓 ∈ (LFnl‘𝑤) ↦ (𝑓f (.r‘(Scalar‘𝑤))((Base‘𝑤) × {𝑘})))⟩ = ⟨( ·𝑠 ‘ndx), ⟩)
4443sneqd 4540 . . . . 5 (𝑤 = 𝑊 → {⟨( ·𝑠 ‘ndx), (𝑘 ∈ (Base‘(Scalar‘𝑤)), 𝑓 ∈ (LFnl‘𝑤) ↦ (𝑓f (.r‘(Scalar‘𝑤))((Base‘𝑤) × {𝑘})))⟩} = {⟨( ·𝑠 ‘ndx), ⟩})
4525, 44uneq12d 4094 . . . 4 (𝑤 = 𝑊 → ({⟨(Base‘ndx), (LFnl‘𝑤)⟩, ⟨(+g‘ndx), ( ∘f (+g‘(Scalar‘𝑤)) ↾ ((LFnl‘𝑤) × (LFnl‘𝑤)))⟩, ⟨(Scalar‘ndx), (oppr‘(Scalar‘𝑤))⟩} ∪ {⟨( ·𝑠 ‘ndx), (𝑘 ∈ (Base‘(Scalar‘𝑤)), 𝑓 ∈ (LFnl‘𝑤) ↦ (𝑓f (.r‘(Scalar‘𝑤))((Base‘𝑤) × {𝑘})))⟩}) = ({⟨(Base‘ndx), 𝐹⟩, ⟨(+g‘ndx), ⟩, ⟨(Scalar‘ndx), 𝑂⟩} ∪ {⟨( ·𝑠 ‘ndx), ⟩}))
46 df-ldual 36571 . . . 4 LDual = (𝑤 ∈ V ↦ ({⟨(Base‘ndx), (LFnl‘𝑤)⟩, ⟨(+g‘ndx), ( ∘f (+g‘(Scalar‘𝑤)) ↾ ((LFnl‘𝑤) × (LFnl‘𝑤)))⟩, ⟨(Scalar‘ndx), (oppr‘(Scalar‘𝑤))⟩} ∪ {⟨( ·𝑠 ‘ndx), (𝑘 ∈ (Base‘(Scalar‘𝑤)), 𝑓 ∈ (LFnl‘𝑤) ↦ (𝑓f (.r‘(Scalar‘𝑤))((Base‘𝑤) × {𝑘})))⟩}))
47 tpex 7463 . . . . 5 {⟨(Base‘ndx), 𝐹⟩, ⟨(+g‘ndx), ⟩, ⟨(Scalar‘ndx), 𝑂⟩} ∈ V
48 snex 5301 . . . . 5 {⟨( ·𝑠 ‘ndx), ⟩} ∈ V
4947, 48unex 7462 . . . 4 ({⟨(Base‘ndx), 𝐹⟩, ⟨(+g‘ndx), ⟩, ⟨(Scalar‘ndx), 𝑂⟩} ∪ {⟨( ·𝑠 ‘ndx), ⟩}) ∈ V
5045, 46, 49fvmpt 6755 . . 3 (𝑊 ∈ V → (LDual‘𝑊) = ({⟨(Base‘ndx), 𝐹⟩, ⟨(+g‘ndx), ⟩, ⟨(Scalar‘ndx), 𝑂⟩} ∪ {⟨( ·𝑠 ‘ndx), ⟩}))
513, 50syl5eq 2845 . 2 (𝑊 ∈ V → 𝐷 = ({⟨(Base‘ndx), 𝐹⟩, ⟨(+g‘ndx), ⟩, ⟨(Scalar‘ndx), 𝑂⟩} ∪ {⟨( ·𝑠 ‘ndx), ⟩}))
521, 2, 513syl 18 1 (𝜑𝐷 = ({⟨(Base‘ndx), 𝐹⟩, ⟨(+g‘ndx), ⟩, ⟨(Scalar‘ndx), 𝑂⟩} ∪ {⟨( ·𝑠 ‘ndx), ⟩}))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   = wceq 1538   ∈ wcel 2111  Vcvv 3442   ∪ cun 3881  {csn 4528  {ctp 4532  ⟨cop 4534   × cxp 5521   ↾ cres 5525  ‘cfv 6332  (class class class)co 7145   ∈ cmpo 7147   ∘f cof 7398  ndxcnx 16492  Basecbs 16495  +gcplusg 16577  .rcmulr 16578  Scalarcsca 16580   ·𝑠 cvsca 16581  opprcoppr 19389  LFnlclfn 36504  LDualcld 36570 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5171  ax-nul 5178  ax-pr 5299  ax-un 7454 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ral 3111  df-rex 3112  df-rab 3115  df-v 3444  df-sbc 3723  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4247  df-if 4429  df-sn 4529  df-pr 4531  df-tp 4533  df-op 4535  df-uni 4805  df-br 5035  df-opab 5097  df-mpt 5115  df-id 5429  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-res 5535  df-iota 6291  df-fun 6334  df-fv 6340  df-ov 7148  df-oprab 7149  df-mpo 7150  df-of 7400  df-ldual 36571 This theorem is referenced by:  ldualvbase  36573  ldualfvadd  36575  ldualsca  36579  ldualfvs  36583
 Copyright terms: Public domain W3C validator