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 37400
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 to reuse our existing collection of left vector space theorems. Note the operation reversal in the scalar product to allow 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 3459 . 2 (𝑊𝑋𝑊 ∈ V)
3 ldualset.d . . 3 𝐷 = (LDual‘𝑊)
4 fveq2 6825 . . . . . . . 8 (𝑤 = 𝑊 → (LFnl‘𝑤) = (LFnl‘𝑊))
5 ldualset.f . . . . . . . 8 𝐹 = (LFnl‘𝑊)
64, 5eqtr4di 2794 . . . . . . 7 (𝑤 = 𝑊 → (LFnl‘𝑤) = 𝐹)
76opeq2d 4824 . . . . . 6 (𝑤 = 𝑊 → ⟨(Base‘ndx), (LFnl‘𝑤)⟩ = ⟨(Base‘ndx), 𝐹⟩)
8 fveq2 6825 . . . . . . . . . . . . 13 (𝑤 = 𝑊 → (Scalar‘𝑤) = (Scalar‘𝑊))
9 ldualset.r . . . . . . . . . . . . 13 𝑅 = (Scalar‘𝑊)
108, 9eqtr4di 2794 . . . . . . . . . . . 12 (𝑤 = 𝑊 → (Scalar‘𝑤) = 𝑅)
1110fveq2d 6829 . . . . . . . . . . 11 (𝑤 = 𝑊 → (+g‘(Scalar‘𝑤)) = (+g𝑅))
12 ldualset.a . . . . . . . . . . 11 + = (+g𝑅)
1311, 12eqtr4di 2794 . . . . . . . . . 10 (𝑤 = 𝑊 → (+g‘(Scalar‘𝑤)) = + )
1413ofeqd 7597 . . . . . . . . 9 (𝑤 = 𝑊 → ∘f (+g‘(Scalar‘𝑤)) = ∘f + )
156sqxpeqd 5652 . . . . . . . . 9 (𝑤 = 𝑊 → ((LFnl‘𝑤) × (LFnl‘𝑤)) = (𝐹 × 𝐹))
1614, 15reseq12d 5924 . . . . . . . 8 (𝑤 = 𝑊 → ( ∘f (+g‘(Scalar‘𝑤)) ↾ ((LFnl‘𝑤) × (LFnl‘𝑤))) = ( ∘f + ↾ (𝐹 × 𝐹)))
17 ldualset.p . . . . . . . 8 = ( ∘f + ↾ (𝐹 × 𝐹))
1816, 17eqtr4di 2794 . . . . . . 7 (𝑤 = 𝑊 → ( ∘f (+g‘(Scalar‘𝑤)) ↾ ((LFnl‘𝑤) × (LFnl‘𝑤))) = )
1918opeq2d 4824 . . . . . 6 (𝑤 = 𝑊 → ⟨(+g‘ndx), ( ∘f (+g‘(Scalar‘𝑤)) ↾ ((LFnl‘𝑤) × (LFnl‘𝑤)))⟩ = ⟨(+g‘ndx), ⟩)
2010fveq2d 6829 . . . . . . . 8 (𝑤 = 𝑊 → (oppr‘(Scalar‘𝑤)) = (oppr𝑅))
21 ldualset.o . . . . . . . 8 𝑂 = (oppr𝑅)
2220, 21eqtr4di 2794 . . . . . . 7 (𝑤 = 𝑊 → (oppr‘(Scalar‘𝑤)) = 𝑂)
2322opeq2d 4824 . . . . . 6 (𝑤 = 𝑊 → ⟨(Scalar‘ndx), (oppr‘(Scalar‘𝑤))⟩ = ⟨(Scalar‘ndx), 𝑂⟩)
247, 19, 23tpeq123d 4696 . . . . 5 (𝑤 = 𝑊 → {⟨(Base‘ndx), (LFnl‘𝑤)⟩, ⟨(+g‘ndx), ( ∘f (+g‘(Scalar‘𝑤)) ↾ ((LFnl‘𝑤) × (LFnl‘𝑤)))⟩, ⟨(Scalar‘ndx), (oppr‘(Scalar‘𝑤))⟩} = {⟨(Base‘ndx), 𝐹⟩, ⟨(+g‘ndx), ⟩, ⟨(Scalar‘ndx), 𝑂⟩})
2510fveq2d 6829 . . . . . . . . . 10 (𝑤 = 𝑊 → (Base‘(Scalar‘𝑤)) = (Base‘𝑅))
26 ldualset.k . . . . . . . . . 10 𝐾 = (Base‘𝑅)
2725, 26eqtr4di 2794 . . . . . . . . 9 (𝑤 = 𝑊 → (Base‘(Scalar‘𝑤)) = 𝐾)
2810fveq2d 6829 . . . . . . . . . . . 12 (𝑤 = 𝑊 → (.r‘(Scalar‘𝑤)) = (.r𝑅))
29 ldualset.t . . . . . . . . . . . 12 · = (.r𝑅)
3028, 29eqtr4di 2794 . . . . . . . . . . 11 (𝑤 = 𝑊 → (.r‘(Scalar‘𝑤)) = · )
3130ofeqd 7597 . . . . . . . . . 10 (𝑤 = 𝑊 → ∘f (.r‘(Scalar‘𝑤)) = ∘f · )
32 eqidd 2737 . . . . . . . . . 10 (𝑤 = 𝑊𝑓 = 𝑓)
33 fveq2 6825 . . . . . . . . . . . 12 (𝑤 = 𝑊 → (Base‘𝑤) = (Base‘𝑊))
34 ldualset.v . . . . . . . . . . . 12 𝑉 = (Base‘𝑊)
3533, 34eqtr4di 2794 . . . . . . . . . . 11 (𝑤 = 𝑊 → (Base‘𝑤) = 𝑉)
3635xpeq1d 5649 . . . . . . . . . 10 (𝑤 = 𝑊 → ((Base‘𝑤) × {𝑘}) = (𝑉 × {𝑘}))
3731, 32, 36oveq123d 7358 . . . . . . . . 9 (𝑤 = 𝑊 → (𝑓f (.r‘(Scalar‘𝑤))((Base‘𝑤) × {𝑘})) = (𝑓f · (𝑉 × {𝑘})))
3827, 6, 37mpoeq123dv 7412 . . . . . . . 8 (𝑤 = 𝑊 → (𝑘 ∈ (Base‘(Scalar‘𝑤)), 𝑓 ∈ (LFnl‘𝑤) ↦ (𝑓f (.r‘(Scalar‘𝑤))((Base‘𝑤) × {𝑘}))) = (𝑘𝐾, 𝑓𝐹 ↦ (𝑓f · (𝑉 × {𝑘}))))
39 ldualset.s . . . . . . . 8 = (𝑘𝐾, 𝑓𝐹 ↦ (𝑓f · (𝑉 × {𝑘})))
4038, 39eqtr4di 2794 . . . . . . 7 (𝑤 = 𝑊 → (𝑘 ∈ (Base‘(Scalar‘𝑤)), 𝑓 ∈ (LFnl‘𝑤) ↦ (𝑓f (.r‘(Scalar‘𝑤))((Base‘𝑤) × {𝑘}))) = )
4140opeq2d 4824 . . . . . 6 (𝑤 = 𝑊 → ⟨( ·𝑠 ‘ndx), (𝑘 ∈ (Base‘(Scalar‘𝑤)), 𝑓 ∈ (LFnl‘𝑤) ↦ (𝑓f (.r‘(Scalar‘𝑤))((Base‘𝑤) × {𝑘})))⟩ = ⟨( ·𝑠 ‘ndx), ⟩)
4241sneqd 4585 . . . . 5 (𝑤 = 𝑊 → {⟨( ·𝑠 ‘ndx), (𝑘 ∈ (Base‘(Scalar‘𝑤)), 𝑓 ∈ (LFnl‘𝑤) ↦ (𝑓f (.r‘(Scalar‘𝑤))((Base‘𝑤) × {𝑘})))⟩} = {⟨( ·𝑠 ‘ndx), ⟩})
4324, 42uneq12d 4111 . . . 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), ⟩}))
44 df-ldual 37399 . . . 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‘𝑤) × {𝑘})))⟩}))
45 tpex 7659 . . . . 5 {⟨(Base‘ndx), 𝐹⟩, ⟨(+g‘ndx), ⟩, ⟨(Scalar‘ndx), 𝑂⟩} ∈ V
46 snex 5376 . . . . 5 {⟨( ·𝑠 ‘ndx), ⟩} ∈ V
4745, 46unex 7658 . . . 4 ({⟨(Base‘ndx), 𝐹⟩, ⟨(+g‘ndx), ⟩, ⟨(Scalar‘ndx), 𝑂⟩} ∪ {⟨( ·𝑠 ‘ndx), ⟩}) ∈ V
4843, 44, 47fvmpt 6931 . . 3 (𝑊 ∈ V → (LDual‘𝑊) = ({⟨(Base‘ndx), 𝐹⟩, ⟨(+g‘ndx), ⟩, ⟨(Scalar‘ndx), 𝑂⟩} ∪ {⟨( ·𝑠 ‘ndx), ⟩}))
493, 48eqtrid 2788 . 2 (𝑊 ∈ V → 𝐷 = ({⟨(Base‘ndx), 𝐹⟩, ⟨(+g‘ndx), ⟩, ⟨(Scalar‘ndx), 𝑂⟩} ∪ {⟨( ·𝑠 ‘ndx), ⟩}))
501, 2, 493syl 18 1 (𝜑𝐷 = ({⟨(Base‘ndx), 𝐹⟩, ⟨(+g‘ndx), ⟩, ⟨(Scalar‘ndx), 𝑂⟩} ∪ {⟨( ·𝑠 ‘ndx), ⟩}))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1540  wcel 2105  Vcvv 3441  cun 3896  {csn 4573  {ctp 4577  cop 4579   × cxp 5618  cres 5622  cfv 6479  (class class class)co 7337  cmpo 7339  f cof 7593  ndxcnx 16991  Basecbs 17009  +gcplusg 17059  .rcmulr 17060  Scalarcsca 17062   ·𝑠 cvsca 17063  opprcoppr 19956  LFnlclfn 37332  LDualcld 37398
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2707  ax-sep 5243  ax-nul 5250  ax-pr 5372  ax-un 7650
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2886  df-ral 3062  df-rex 3071  df-rab 3404  df-v 3443  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4270  df-if 4474  df-sn 4574  df-pr 4576  df-tp 4578  df-op 4580  df-uni 4853  df-br 5093  df-opab 5155  df-mpt 5176  df-id 5518  df-xp 5626  df-rel 5627  df-cnv 5628  df-co 5629  df-dm 5630  df-res 5632  df-iota 6431  df-fun 6481  df-fv 6487  df-ov 7340  df-oprab 7341  df-mpo 7342  df-of 7595  df-ldual 37399
This theorem is referenced by:  ldualvbase  37401  ldualfvadd  37403  ldualsca  37407  ldualfvs  37411
  Copyright terms: Public domain W3C validator