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

Theorem ldualset 36141
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 3510 . 2 (𝑊𝑋𝑊 ∈ V)
3 ldualset.d . . 3 𝐷 = (LDual‘𝑊)
4 fveq2 6663 . . . . . . . 8 (𝑤 = 𝑊 → (LFnl‘𝑤) = (LFnl‘𝑊))
5 ldualset.f . . . . . . . 8 𝐹 = (LFnl‘𝑊)
64, 5syl6eqr 2871 . . . . . . 7 (𝑤 = 𝑊 → (LFnl‘𝑤) = 𝐹)
76opeq2d 4802 . . . . . 6 (𝑤 = 𝑊 → ⟨(Base‘ndx), (LFnl‘𝑤)⟩ = ⟨(Base‘ndx), 𝐹⟩)
8 fveq2 6663 . . . . . . . . . . . . 13 (𝑤 = 𝑊 → (Scalar‘𝑤) = (Scalar‘𝑊))
9 ldualset.r . . . . . . . . . . . . 13 𝑅 = (Scalar‘𝑊)
108, 9syl6eqr 2871 . . . . . . . . . . . 12 (𝑤 = 𝑊 → (Scalar‘𝑤) = 𝑅)
1110fveq2d 6667 . . . . . . . . . . 11 (𝑤 = 𝑊 → (+g‘(Scalar‘𝑤)) = (+g𝑅))
12 ldualset.a . . . . . . . . . . 11 + = (+g𝑅)
1311, 12syl6eqr 2871 . . . . . . . . . 10 (𝑤 = 𝑊 → (+g‘(Scalar‘𝑤)) = + )
14 ofeq 7400 . . . . . . . . . 10 ((+g‘(Scalar‘𝑤)) = + → ∘f (+g‘(Scalar‘𝑤)) = ∘f + )
1513, 14syl 17 . . . . . . . . 9 (𝑤 = 𝑊 → ∘f (+g‘(Scalar‘𝑤)) = ∘f + )
166sqxpeqd 5580 . . . . . . . . 9 (𝑤 = 𝑊 → ((LFnl‘𝑤) × (LFnl‘𝑤)) = (𝐹 × 𝐹))
1715, 16reseq12d 5847 . . . . . . . 8 (𝑤 = 𝑊 → ( ∘f (+g‘(Scalar‘𝑤)) ↾ ((LFnl‘𝑤) × (LFnl‘𝑤))) = ( ∘f + ↾ (𝐹 × 𝐹)))
18 ldualset.p . . . . . . . 8 = ( ∘f + ↾ (𝐹 × 𝐹))
1917, 18syl6eqr 2871 . . . . . . 7 (𝑤 = 𝑊 → ( ∘f (+g‘(Scalar‘𝑤)) ↾ ((LFnl‘𝑤) × (LFnl‘𝑤))) = )
2019opeq2d 4802 . . . . . 6 (𝑤 = 𝑊 → ⟨(+g‘ndx), ( ∘f (+g‘(Scalar‘𝑤)) ↾ ((LFnl‘𝑤) × (LFnl‘𝑤)))⟩ = ⟨(+g‘ndx), ⟩)
2110fveq2d 6667 . . . . . . . 8 (𝑤 = 𝑊 → (oppr‘(Scalar‘𝑤)) = (oppr𝑅))
22 ldualset.o . . . . . . . 8 𝑂 = (oppr𝑅)
2321, 22syl6eqr 2871 . . . . . . 7 (𝑤 = 𝑊 → (oppr‘(Scalar‘𝑤)) = 𝑂)
2423opeq2d 4802 . . . . . 6 (𝑤 = 𝑊 → ⟨(Scalar‘ndx), (oppr‘(Scalar‘𝑤))⟩ = ⟨(Scalar‘ndx), 𝑂⟩)
257, 20, 24tpeq123d 4676 . . . . 5 (𝑤 = 𝑊 → {⟨(Base‘ndx), (LFnl‘𝑤)⟩, ⟨(+g‘ndx), ( ∘f (+g‘(Scalar‘𝑤)) ↾ ((LFnl‘𝑤) × (LFnl‘𝑤)))⟩, ⟨(Scalar‘ndx), (oppr‘(Scalar‘𝑤))⟩} = {⟨(Base‘ndx), 𝐹⟩, ⟨(+g‘ndx), ⟩, ⟨(Scalar‘ndx), 𝑂⟩})
2610fveq2d 6667 . . . . . . . . . 10 (𝑤 = 𝑊 → (Base‘(Scalar‘𝑤)) = (Base‘𝑅))
27 ldualset.k . . . . . . . . . 10 𝐾 = (Base‘𝑅)
2826, 27syl6eqr 2871 . . . . . . . . 9 (𝑤 = 𝑊 → (Base‘(Scalar‘𝑤)) = 𝐾)
2910fveq2d 6667 . . . . . . . . . . . 12 (𝑤 = 𝑊 → (.r‘(Scalar‘𝑤)) = (.r𝑅))
30 ldualset.t . . . . . . . . . . . 12 · = (.r𝑅)
3129, 30syl6eqr 2871 . . . . . . . . . . 11 (𝑤 = 𝑊 → (.r‘(Scalar‘𝑤)) = · )
32 ofeq 7400 . . . . . . . . . . 11 ((.r‘(Scalar‘𝑤)) = · → ∘f (.r‘(Scalar‘𝑤)) = ∘f · )
3331, 32syl 17 . . . . . . . . . 10 (𝑤 = 𝑊 → ∘f (.r‘(Scalar‘𝑤)) = ∘f · )
34 eqidd 2819 . . . . . . . . . 10 (𝑤 = 𝑊𝑓 = 𝑓)
35 fveq2 6663 . . . . . . . . . . . 12 (𝑤 = 𝑊 → (Base‘𝑤) = (Base‘𝑊))
36 ldualset.v . . . . . . . . . . . 12 𝑉 = (Base‘𝑊)
3735, 36syl6eqr 2871 . . . . . . . . . . 11 (𝑤 = 𝑊 → (Base‘𝑤) = 𝑉)
3837xpeq1d 5577 . . . . . . . . . 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, 41syl6eqr 2871 . . . . . . 7 (𝑤 = 𝑊 → (𝑘 ∈ (Base‘(Scalar‘𝑤)), 𝑓 ∈ (LFnl‘𝑤) ↦ (𝑓f (.r‘(Scalar‘𝑤))((Base‘𝑤) × {𝑘}))) = )
4342opeq2d 4802 . . . . . 6 (𝑤 = 𝑊 → ⟨( ·𝑠 ‘ndx), (𝑘 ∈ (Base‘(Scalar‘𝑤)), 𝑓 ∈ (LFnl‘𝑤) ↦ (𝑓f (.r‘(Scalar‘𝑤))((Base‘𝑤) × {𝑘})))⟩ = ⟨( ·𝑠 ‘ndx), ⟩)
4443sneqd 4569 . . . . 5 (𝑤 = 𝑊 → {⟨( ·𝑠 ‘ndx), (𝑘 ∈ (Base‘(Scalar‘𝑤)), 𝑓 ∈ (LFnl‘𝑤) ↦ (𝑓f (.r‘(Scalar‘𝑤))((Base‘𝑤) × {𝑘})))⟩} = {⟨( ·𝑠 ‘ndx), ⟩})
4525, 44uneq12d 4137 . . . 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 36140 . . . 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 7459 . . . . 5 {⟨(Base‘ndx), 𝐹⟩, ⟨(+g‘ndx), ⟩, ⟨(Scalar‘ndx), 𝑂⟩} ∈ V
48 snex 5322 . . . . 5 {⟨( ·𝑠 ‘ndx), ⟩} ∈ V
4947, 48unex 7458 . . . 4 ({⟨(Base‘ndx), 𝐹⟩, ⟨(+g‘ndx), ⟩, ⟨(Scalar‘ndx), 𝑂⟩} ∪ {⟨( ·𝑠 ‘ndx), ⟩}) ∈ V
5045, 46, 49fvmpt 6761 . . 3 (𝑊 ∈ V → (LDual‘𝑊) = ({⟨(Base‘ndx), 𝐹⟩, ⟨(+g‘ndx), ⟩, ⟨(Scalar‘ndx), 𝑂⟩} ∪ {⟨( ·𝑠 ‘ndx), ⟩}))
513, 50syl5eq 2865 . 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 1528  wcel 2105  Vcvv 3492  cun 3931  {csn 4557  {ctp 4561  cop 4563   × cxp 5546  cres 5550  cfv 6348  (class class class)co 7145  cmpo 7147  f cof 7396  ndxcnx 16468  Basecbs 16471  +gcplusg 16553  .rcmulr 16554  Scalarcsca 16556   ·𝑠 cvsca 16557  opprcoppr 19301  LFnlclfn 36073  LDualcld 36139
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-sep 5194  ax-nul 5201  ax-pr 5320  ax-un 7450
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ral 3140  df-rex 3141  df-rab 3144  df-v 3494  df-sbc 3770  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4464  df-sn 4558  df-pr 4560  df-tp 4562  df-op 4564  df-uni 4831  df-br 5058  df-opab 5120  df-mpt 5138  df-id 5453  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-res 5560  df-iota 6307  df-fun 6350  df-fv 6356  df-ov 7148  df-oprab 7149  df-mpo 7150  df-of 7398  df-ldual 36140
This theorem is referenced by:  ldualvbase  36142  ldualfvadd  36144  ldualsca  36148  ldualfvs  36152
  Copyright terms: Public domain W3C validator