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

Theorem ldualset 34231
 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 = ( ∘𝑓 + ↾ (𝐹 × 𝐹))
ldualset.f 𝐹 = (LFnl‘𝑊)
ldualset.d 𝐷 = (LDual‘𝑊)
ldualset.r 𝑅 = (Scalar‘𝑊)
ldualset.k 𝐾 = (Base‘𝑅)
ldualset.t · = (.r𝑅)
ldualset.o 𝑂 = (oppr𝑅)
ldualset.s = (𝑘𝐾, 𝑓𝐹 ↦ (𝑓𝑓 · (𝑉 × {𝑘})))
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 3207 . 2 (𝑊𝑋𝑊 ∈ V)
3 ldualset.d . . 3 𝐷 = (LDual‘𝑊)
4 fveq2 6178 . . . . . . . 8 (𝑤 = 𝑊 → (LFnl‘𝑤) = (LFnl‘𝑊))
5 ldualset.f . . . . . . . 8 𝐹 = (LFnl‘𝑊)
64, 5syl6eqr 2672 . . . . . . 7 (𝑤 = 𝑊 → (LFnl‘𝑤) = 𝐹)
76opeq2d 4400 . . . . . 6 (𝑤 = 𝑊 → ⟨(Base‘ndx), (LFnl‘𝑤)⟩ = ⟨(Base‘ndx), 𝐹⟩)
8 fveq2 6178 . . . . . . . . . . . . 13 (𝑤 = 𝑊 → (Scalar‘𝑤) = (Scalar‘𝑊))
9 ldualset.r . . . . . . . . . . . . 13 𝑅 = (Scalar‘𝑊)
108, 9syl6eqr 2672 . . . . . . . . . . . 12 (𝑤 = 𝑊 → (Scalar‘𝑤) = 𝑅)
1110fveq2d 6182 . . . . . . . . . . 11 (𝑤 = 𝑊 → (+g‘(Scalar‘𝑤)) = (+g𝑅))
12 ldualset.a . . . . . . . . . . 11 + = (+g𝑅)
1311, 12syl6eqr 2672 . . . . . . . . . 10 (𝑤 = 𝑊 → (+g‘(Scalar‘𝑤)) = + )
14 ofeq 6884 . . . . . . . . . 10 ((+g‘(Scalar‘𝑤)) = + → ∘𝑓 (+g‘(Scalar‘𝑤)) = ∘𝑓 + )
1513, 14syl 17 . . . . . . . . 9 (𝑤 = 𝑊 → ∘𝑓 (+g‘(Scalar‘𝑤)) = ∘𝑓 + )
166sqxpeqd 5131 . . . . . . . . 9 (𝑤 = 𝑊 → ((LFnl‘𝑤) × (LFnl‘𝑤)) = (𝐹 × 𝐹))
1715, 16reseq12d 5386 . . . . . . . 8 (𝑤 = 𝑊 → ( ∘𝑓 (+g‘(Scalar‘𝑤)) ↾ ((LFnl‘𝑤) × (LFnl‘𝑤))) = ( ∘𝑓 + ↾ (𝐹 × 𝐹)))
18 ldualset.p . . . . . . . 8 = ( ∘𝑓 + ↾ (𝐹 × 𝐹))
1917, 18syl6eqr 2672 . . . . . . 7 (𝑤 = 𝑊 → ( ∘𝑓 (+g‘(Scalar‘𝑤)) ↾ ((LFnl‘𝑤) × (LFnl‘𝑤))) = )
2019opeq2d 4400 . . . . . 6 (𝑤 = 𝑊 → ⟨(+g‘ndx), ( ∘𝑓 (+g‘(Scalar‘𝑤)) ↾ ((LFnl‘𝑤) × (LFnl‘𝑤)))⟩ = ⟨(+g‘ndx), ⟩)
2110fveq2d 6182 . . . . . . . 8 (𝑤 = 𝑊 → (oppr‘(Scalar‘𝑤)) = (oppr𝑅))
22 ldualset.o . . . . . . . 8 𝑂 = (oppr𝑅)
2321, 22syl6eqr 2672 . . . . . . 7 (𝑤 = 𝑊 → (oppr‘(Scalar‘𝑤)) = 𝑂)
2423opeq2d 4400 . . . . . 6 (𝑤 = 𝑊 → ⟨(Scalar‘ndx), (oppr‘(Scalar‘𝑤))⟩ = ⟨(Scalar‘ndx), 𝑂⟩)
257, 20, 24tpeq123d 4274 . . . . 5 (𝑤 = 𝑊 → {⟨(Base‘ndx), (LFnl‘𝑤)⟩, ⟨(+g‘ndx), ( ∘𝑓 (+g‘(Scalar‘𝑤)) ↾ ((LFnl‘𝑤) × (LFnl‘𝑤)))⟩, ⟨(Scalar‘ndx), (oppr‘(Scalar‘𝑤))⟩} = {⟨(Base‘ndx), 𝐹⟩, ⟨(+g‘ndx), ⟩, ⟨(Scalar‘ndx), 𝑂⟩})
2610fveq2d 6182 . . . . . . . . . 10 (𝑤 = 𝑊 → (Base‘(Scalar‘𝑤)) = (Base‘𝑅))
27 ldualset.k . . . . . . . . . 10 𝐾 = (Base‘𝑅)
2826, 27syl6eqr 2672 . . . . . . . . 9 (𝑤 = 𝑊 → (Base‘(Scalar‘𝑤)) = 𝐾)
2910fveq2d 6182 . . . . . . . . . . . 12 (𝑤 = 𝑊 → (.r‘(Scalar‘𝑤)) = (.r𝑅))
30 ldualset.t . . . . . . . . . . . 12 · = (.r𝑅)
3129, 30syl6eqr 2672 . . . . . . . . . . 11 (𝑤 = 𝑊 → (.r‘(Scalar‘𝑤)) = · )
32 ofeq 6884 . . . . . . . . . . 11 ((.r‘(Scalar‘𝑤)) = · → ∘𝑓 (.r‘(Scalar‘𝑤)) = ∘𝑓 · )
3331, 32syl 17 . . . . . . . . . 10 (𝑤 = 𝑊 → ∘𝑓 (.r‘(Scalar‘𝑤)) = ∘𝑓 · )
34 eqidd 2621 . . . . . . . . . 10 (𝑤 = 𝑊𝑓 = 𝑓)
35 fveq2 6178 . . . . . . . . . . . 12 (𝑤 = 𝑊 → (Base‘𝑤) = (Base‘𝑊))
36 ldualset.v . . . . . . . . . . . 12 𝑉 = (Base‘𝑊)
3735, 36syl6eqr 2672 . . . . . . . . . . 11 (𝑤 = 𝑊 → (Base‘𝑤) = 𝑉)
3837xpeq1d 5128 . . . . . . . . . 10 (𝑤 = 𝑊 → ((Base‘𝑤) × {𝑘}) = (𝑉 × {𝑘}))
3933, 34, 38oveq123d 6656 . . . . . . . . 9 (𝑤 = 𝑊 → (𝑓𝑓 (.r‘(Scalar‘𝑤))((Base‘𝑤) × {𝑘})) = (𝑓𝑓 · (𝑉 × {𝑘})))
4028, 6, 39mpt2eq123dv 6702 . . . . . . . 8 (𝑤 = 𝑊 → (𝑘 ∈ (Base‘(Scalar‘𝑤)), 𝑓 ∈ (LFnl‘𝑤) ↦ (𝑓𝑓 (.r‘(Scalar‘𝑤))((Base‘𝑤) × {𝑘}))) = (𝑘𝐾, 𝑓𝐹 ↦ (𝑓𝑓 · (𝑉 × {𝑘}))))
41 ldualset.s . . . . . . . 8 = (𝑘𝐾, 𝑓𝐹 ↦ (𝑓𝑓 · (𝑉 × {𝑘})))
4240, 41syl6eqr 2672 . . . . . . 7 (𝑤 = 𝑊 → (𝑘 ∈ (Base‘(Scalar‘𝑤)), 𝑓 ∈ (LFnl‘𝑤) ↦ (𝑓𝑓 (.r‘(Scalar‘𝑤))((Base‘𝑤) × {𝑘}))) = )
4342opeq2d 4400 . . . . . 6 (𝑤 = 𝑊 → ⟨( ·𝑠 ‘ndx), (𝑘 ∈ (Base‘(Scalar‘𝑤)), 𝑓 ∈ (LFnl‘𝑤) ↦ (𝑓𝑓 (.r‘(Scalar‘𝑤))((Base‘𝑤) × {𝑘})))⟩ = ⟨( ·𝑠 ‘ndx), ⟩)
4443sneqd 4180 . . . . 5 (𝑤 = 𝑊 → {⟨( ·𝑠 ‘ndx), (𝑘 ∈ (Base‘(Scalar‘𝑤)), 𝑓 ∈ (LFnl‘𝑤) ↦ (𝑓𝑓 (.r‘(Scalar‘𝑤))((Base‘𝑤) × {𝑘})))⟩} = {⟨( ·𝑠 ‘ndx), ⟩})
4525, 44uneq12d 3760 . . . 4 (𝑤 = 𝑊 → ({⟨(Base‘ndx), (LFnl‘𝑤)⟩, ⟨(+g‘ndx), ( ∘𝑓 (+g‘(Scalar‘𝑤)) ↾ ((LFnl‘𝑤) × (LFnl‘𝑤)))⟩, ⟨(Scalar‘ndx), (oppr‘(Scalar‘𝑤))⟩} ∪ {⟨( ·𝑠 ‘ndx), (𝑘 ∈ (Base‘(Scalar‘𝑤)), 𝑓 ∈ (LFnl‘𝑤) ↦ (𝑓𝑓 (.r‘(Scalar‘𝑤))((Base‘𝑤) × {𝑘})))⟩}) = ({⟨(Base‘ndx), 𝐹⟩, ⟨(+g‘ndx), ⟩, ⟨(Scalar‘ndx), 𝑂⟩} ∪ {⟨( ·𝑠 ‘ndx), ⟩}))
46 df-ldual 34230 . . . 4 LDual = (𝑤 ∈ V ↦ ({⟨(Base‘ndx), (LFnl‘𝑤)⟩, ⟨(+g‘ndx), ( ∘𝑓 (+g‘(Scalar‘𝑤)) ↾ ((LFnl‘𝑤) × (LFnl‘𝑤)))⟩, ⟨(Scalar‘ndx), (oppr‘(Scalar‘𝑤))⟩} ∪ {⟨( ·𝑠 ‘ndx), (𝑘 ∈ (Base‘(Scalar‘𝑤)), 𝑓 ∈ (LFnl‘𝑤) ↦ (𝑓𝑓 (.r‘(Scalar‘𝑤))((Base‘𝑤) × {𝑘})))⟩}))
47 tpex 6942 . . . . 5 {⟨(Base‘ndx), 𝐹⟩, ⟨(+g‘ndx), ⟩, ⟨(Scalar‘ndx), 𝑂⟩} ∈ V
48 snex 4899 . . . . 5 {⟨( ·𝑠 ‘ndx), ⟩} ∈ V
4947, 48unex 6941 . . . 4 ({⟨(Base‘ndx), 𝐹⟩, ⟨(+g‘ndx), ⟩, ⟨(Scalar‘ndx), 𝑂⟩} ∪ {⟨( ·𝑠 ‘ndx), ⟩}) ∈ V
5045, 46, 49fvmpt 6269 . . 3 (𝑊 ∈ V → (LDual‘𝑊) = ({⟨(Base‘ndx), 𝐹⟩, ⟨(+g‘ndx), ⟩, ⟨(Scalar‘ndx), 𝑂⟩} ∪ {⟨( ·𝑠 ‘ndx), ⟩}))
513, 50syl5eq 2666 . 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 1481   ∈ wcel 1988  Vcvv 3195   ∪ cun 3565  {csn 4168  {ctp 4172  ⟨cop 4174   × cxp 5102   ↾ cres 5106  ‘cfv 5876  (class class class)co 6635   ↦ cmpt2 6637   ∘𝑓 cof 6880  ndxcnx 15835  Basecbs 15838  +gcplusg 15922  .rcmulr 15923  Scalarcsca 15925   ·𝑠 cvsca 15926  opprcoppr 18603  LFnlclfn 34163  LDualcld 34229 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-8 1990  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-sep 4772  ax-nul 4780  ax-pr 4897  ax-un 6934 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-eu 2472  df-mo 2473  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ral 2914  df-rex 2915  df-rab 2918  df-v 3197  df-sbc 3430  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-nul 3908  df-if 4078  df-sn 4169  df-pr 4171  df-tp 4173  df-op 4175  df-uni 4428  df-br 4645  df-opab 4704  df-mpt 4721  df-id 5014  df-xp 5110  df-rel 5111  df-cnv 5112  df-co 5113  df-dm 5114  df-res 5116  df-iota 5839  df-fun 5878  df-fv 5884  df-ov 6638  df-oprab 6639  df-mpt2 6640  df-of 6882  df-ldual 34230 This theorem is referenced by:  ldualvbase  34232  ldualfvadd  34234  ldualsca  34238  ldualfvs  34242
 Copyright terms: Public domain W3C validator