Theorem ldualset 40385

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 opp_r 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.

Step	Hyp	Ref	Expression
1		ldualset.w	. 2 ⊢ (𝜑 → 𝑊 ∈ 𝑋)
2		elex 3475	. 2 ⊢ (𝑊 ∈ 𝑋 → 𝑊 ∈ V)
3		ldualset.d	. . 3 ⊢ 𝐷 = (LDual‘𝑊)
4		fveq2 6911	. . . . . . . 8 ⊢ (𝑤 = 𝑊 → (LFnl‘𝑤) = (LFnl‘𝑊))
5		ldualset.f	. . . . . . . 8 ⊢ 𝐹 = (LFnl‘𝑊)
6	4, 5	eqtr4di 2816	. . . . . . 7 ⊢ (𝑤 = 𝑊 → (LFnl‘𝑤) = 𝐹)
7	6	opeq2d 4850	. . . . . 6 ⊢ (𝑤 = 𝑊 → ⟨(Base‘ndx), (LFnl‘𝑤)⟩ = ⟨(Base‘ndx), 𝐹⟩)
8		fveq2 6911	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝑊 → (Scalar‘𝑤) = (Scalar‘𝑊))
9		ldualset.r	. . . . . . . . . . . . 13 ⊢ 𝑅 = (Scalar‘𝑊)
10	8, 9	eqtr4di 2816	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝑊 → (Scalar‘𝑤) = 𝑅)
11	10	fveq2d 6915	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑊 → (+g‘(Scalar‘𝑤)) = (+g‘𝑅))
12		ldualset.a	. . . . . . . . . . 11 ⊢ + = (+g‘𝑅)
13	11, 12	eqtr4di 2816	. . . . . . . . . 10 ⊢ (𝑤 = 𝑊 → (+g‘(Scalar‘𝑤)) = + )
14	13	ofeqd 7722	. . . . . . . . 9 ⊢ (𝑤 = 𝑊 → ∘f (+g‘(Scalar‘𝑤)) = ∘f + )
15	6	sqxpeqd 5688	. . . . . . . . 9 ⊢ (𝑤 = 𝑊 → ((LFnl‘𝑤) × (LFnl‘𝑤)) = (𝐹 × 𝐹))
16	14, 15	reseq12d 5983	. . . . . . . 8 ⊢ (𝑤 = 𝑊 → ( ∘f (+g‘(Scalar‘𝑤)) ↾ ((LFnl‘𝑤) × (LFnl‘𝑤))) = ( ∘f + ↾ (𝐹 × 𝐹)))
17		ldualset.p	. . . . . . . 8 ⊢ + = ( ∘f + ↾ (𝐹 × 𝐹))
18	16, 17	eqtr4di 2816	. . . . . . 7 ⊢ (𝑤 = 𝑊 → ( ∘f (+g‘(Scalar‘𝑤)) ↾ ((LFnl‘𝑤) × (LFnl‘𝑤))) = + )
19	18	opeq2d 4850	. . . . . 6 ⊢ (𝑤 = 𝑊 → ⟨(+g‘ndx), ( ∘f (+g‘(Scalar‘𝑤)) ↾ ((LFnl‘𝑤) × (LFnl‘𝑤)))⟩ = ⟨(+g‘ndx), + ⟩)
20	10	fveq2d 6915	. . . . . . . 8 ⊢ (𝑤 = 𝑊 → (oppr‘(Scalar‘𝑤)) = (oppr‘𝑅))
21		ldualset.o	. . . . . . . 8 ⊢ 𝑂 = (oppr‘𝑅)
22	20, 21	eqtr4di 2816	. . . . . . 7 ⊢ (𝑤 = 𝑊 → (oppr‘(Scalar‘𝑤)) = 𝑂)
23	22	opeq2d 4850	. . . . . 6 ⊢ (𝑤 = 𝑊 → ⟨(Scalar‘ndx), (oppr‘(Scalar‘𝑤))⟩ = ⟨(Scalar‘ndx), 𝑂⟩)
24	7, 19, 23	tpeq123d 4709	. . . . 5 ⊢ (𝑤 = 𝑊 → {⟨(Base‘ndx), (LFnl‘𝑤)⟩, ⟨(+g‘ndx), ( ∘f (+g‘(Scalar‘𝑤)) ↾ ((LFnl‘𝑤) × (LFnl‘𝑤)))⟩, ⟨(Scalar‘ndx), (oppr‘(Scalar‘𝑤))⟩} = {⟨(Base‘ndx), 𝐹⟩, ⟨(+g‘ndx), + ⟩, ⟨(Scalar‘ndx), 𝑂⟩})
25	10	fveq2d 6915	. . . . . . . . . 10 ⊢ (𝑤 = 𝑊 → (Base‘(Scalar‘𝑤)) = (Base‘𝑅))
26		ldualset.k	. . . . . . . . . 10 ⊢ 𝐾 = (Base‘𝑅)
27	25, 26	eqtr4di 2816	. . . . . . . . 9 ⊢ (𝑤 = 𝑊 → (Base‘(Scalar‘𝑤)) = 𝐾)
28	10	fveq2d 6915	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝑊 → (.r‘(Scalar‘𝑤)) = (.r‘𝑅))
29		ldualset.t	. . . . . . . . . . . 12 ⊢ · = (.r‘𝑅)
30	28, 29	eqtr4di 2816	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑊 → (.r‘(Scalar‘𝑤)) = · )
31	30	ofeqd 7722	. . . . . . . . . 10 ⊢ (𝑤 = 𝑊 → ∘f (.r‘(Scalar‘𝑤)) = ∘f · )
32		eqidd 2764	. . . . . . . . . 10 ⊢ (𝑤 = 𝑊 → 𝑓 = 𝑓)
33		fveq2 6911	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝑊 → (Base‘𝑤) = (Base‘𝑊))
34		ldualset.v	. . . . . . . . . . . 12 ⊢ 𝑉 = (Base‘𝑊)
35	33, 34	eqtr4di 2816	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑊 → (Base‘𝑤) = 𝑉)
36	35	xpeq1d 5685	. . . . . . . . . 10 ⊢ (𝑤 = 𝑊 → ((Base‘𝑤) × {𝑘}) = (𝑉 × {𝑘}))
37	31, 32, 36	oveq123d 7467	. . . . . . . . 9 ⊢ (𝑤 = 𝑊 → (𝑓 ∘f (.r‘(Scalar‘𝑤))((Base‘𝑤) × {𝑘})) = (𝑓 ∘f · (𝑉 × {𝑘})))
38	27, 6, 37	mpoeq123dv 7521	. . . . . . . 8 ⊢ (𝑤 = 𝑊 → (𝑘 ∈ (Base‘(Scalar‘𝑤)), 𝑓 ∈ (LFnl‘𝑤) ↦ (𝑓 ∘f (.r‘(Scalar‘𝑤))((Base‘𝑤) × {𝑘}))) = (𝑘 ∈ 𝐾, 𝑓 ∈ 𝐹 ↦ (𝑓 ∘f · (𝑉 × {𝑘}))))
39		ldualset.s	. . . . . . . 8 ⊢ ∙ = (𝑘 ∈ 𝐾, 𝑓 ∈ 𝐹 ↦ (𝑓 ∘f · (𝑉 × {𝑘})))
40	38, 39	eqtr4di 2816	. . . . . . 7 ⊢ (𝑤 = 𝑊 → (𝑘 ∈ (Base‘(Scalar‘𝑤)), 𝑓 ∈ (LFnl‘𝑤) ↦ (𝑓 ∘f (.r‘(Scalar‘𝑤))((Base‘𝑤) × {𝑘}))) = ∙ )
41	40	opeq2d 4850	. . . . . 6 ⊢ (𝑤 = 𝑊 → ⟨( ·𝑠 ‘ndx), (𝑘 ∈ (Base‘(Scalar‘𝑤)), 𝑓 ∈ (LFnl‘𝑤) ↦ (𝑓 ∘f (.r‘(Scalar‘𝑤))((Base‘𝑤) × {𝑘})))⟩ = ⟨( ·𝑠 ‘ndx), ∙ ⟩)
42	41	sneqd 4596	. . . . 5 ⊢ (𝑤 = 𝑊 → {⟨( ·𝑠 ‘ndx), (𝑘 ∈ (Base‘(Scalar‘𝑤)), 𝑓 ∈ (LFnl‘𝑤) ↦ (𝑓 ∘f (.r‘(Scalar‘𝑤))((Base‘𝑤) × {𝑘})))⟩} = {⟨( ·𝑠 ‘ndx), ∙ ⟩})
43	24, 42	uneq12d 4171	. . . 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 40384	. . . 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 7789	. . . . 5 ⊢ {⟨(Base‘ndx), 𝐹⟩, ⟨(+g‘ndx), + ⟩, ⟨(Scalar‘ndx), 𝑂⟩} ∈ V
46		snex 5402	. . . . 5 ⊢ {⟨( ·𝑠 ‘ndx), ∙ ⟩} ∈ V
47	45, 46	unex 7788	. . . 4 ⊢ ({⟨(Base‘ndx), 𝐹⟩, ⟨(+g‘ndx), + ⟩, ⟨(Scalar‘ndx), 𝑂⟩} ∪ {⟨( ·𝑠 ‘ndx), ∙ ⟩}) ∈ V
48	43, 44, 47	fvmpt 7019	. . 3 ⊢ (𝑊 ∈ V → (LDual‘𝑊) = ({⟨(Base‘ndx), 𝐹⟩, ⟨(+g‘ndx), + ⟩, ⟨(Scalar‘ndx), 𝑂⟩} ∪ {⟨( ·𝑠 ‘ndx), ∙ ⟩}))
49	3, 48	eqtrid 2810	. 2 ⊢ (𝑊 ∈ V → 𝐷 = ({⟨(Base‘ndx), 𝐹⟩, ⟨(+g‘ndx), + ⟩, ⟨(Scalar‘ndx), 𝑂⟩} ∪ {⟨( ·𝑠 ‘ndx), ∙ ⟩}))
50	1, 2, 49	3syl 19	1 ⊢ (𝜑 → 𝐷 = ({⟨(Base‘ndx), 𝐹⟩, ⟨(+g‘ndx), + ⟩, ⟨(Scalar‘ndx), 𝑂⟩} ∪ {⟨( ·𝑠 ‘ndx), ∙ ⟩}))

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2147  Vcvv 3454   ∪ cun 4152  {csn 4588  {ctp 4592  ⟨cop 4838   × cxp 5654   ↾ cres 5658  ‘cfv 6561  (class class class)co 7446   ∈ cmpo 7448   ∘_f cof 7718  ndxcnx 17403  Basecbs 17419  +_gcplusg 17460  ._rcmulr 17461  Scalarcsca 17463   ·_𝑠 cvsca 17464  opp_rcoppr 20599  LFnlclfn 40317  LDualcld 40383

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5253  ax-pr 5396  ax-un 7778

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-tp 4593  df-op 4839  df-uni 4871  df-br 5107  df-opab 5172  df-mpt 5191  df-id 5551  df-xp 5662  df-rel 5663  df-cnv 5664  df-co 5665  df-dm 5666  df-res 5668  df-iota 6515  df-fun 6563  df-fv 6569  df-ov 7449  df-oprab 7450  df-mpo 7451  df-of 7720  df-ldual 40384

This theorem is used by:  ldualvbase  40386  ldualfvadd  40388  ldualsca  40392  ldualfvs  40396