Theorem ldualset 39624

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 3453	. 2 ⊢ (𝑊 ∈ 𝑋 → 𝑊 ∈ V)
3		ldualset.d	. . 3 ⊢ 𝐷 = (LDual‘𝑊)
4		fveq2 6834	. . . . . . . 8 ⊢ (𝑤 = 𝑊 → (LFnl‘𝑤) = (LFnl‘𝑊))
5		ldualset.f	. . . . . . . 8 ⊢ 𝐹 = (LFnl‘𝑊)
6	4, 5	eqtr4di 2793	. . . . . . 7 ⊢ (𝑤 = 𝑊 → (LFnl‘𝑤) = 𝐹)
7	6	opeq2d 4818	. . . . . 6 ⊢ (𝑤 = 𝑊 → ⟨(Base‘ndx), (LFnl‘𝑤)⟩ = ⟨(Base‘ndx), 𝐹⟩)
8		fveq2 6834	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝑊 → (Scalar‘𝑤) = (Scalar‘𝑊))
9		ldualset.r	. . . . . . . . . . . . 13 ⊢ 𝑅 = (Scalar‘𝑊)
10	8, 9	eqtr4di 2793	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝑊 → (Scalar‘𝑤) = 𝑅)
11	10	fveq2d 6838	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑊 → (+g‘(Scalar‘𝑤)) = (+g‘𝑅))
12		ldualset.a	. . . . . . . . . . 11 ⊢ + = (+g‘𝑅)
13	11, 12	eqtr4di 2793	. . . . . . . . . 10 ⊢ (𝑤 = 𝑊 → (+g‘(Scalar‘𝑤)) = + )
14	13	ofeqd 7629	. . . . . . . . 9 ⊢ (𝑤 = 𝑊 → ∘f (+g‘(Scalar‘𝑤)) = ∘f + )
15	6	sqxpeqd 5657	. . . . . . . . 9 ⊢ (𝑤 = 𝑊 → ((LFnl‘𝑤) × (LFnl‘𝑤)) = (𝐹 × 𝐹))
16	14, 15	reseq12d 5939	. . . . . . . 8 ⊢ (𝑤 = 𝑊 → ( ∘f (+g‘(Scalar‘𝑤)) ↾ ((LFnl‘𝑤) × (LFnl‘𝑤))) = ( ∘f + ↾ (𝐹 × 𝐹)))
17		ldualset.p	. . . . . . . 8 ⊢ ✚ = ( ∘f + ↾ (𝐹 × 𝐹))
18	16, 17	eqtr4di 2793	. . . . . . 7 ⊢ (𝑤 = 𝑊 → ( ∘f (+g‘(Scalar‘𝑤)) ↾ ((LFnl‘𝑤) × (LFnl‘𝑤))) = ✚ )
19	18	opeq2d 4818	. . . . . 6 ⊢ (𝑤 = 𝑊 → ⟨(+g‘ndx), ( ∘f (+g‘(Scalar‘𝑤)) ↾ ((LFnl‘𝑤) × (LFnl‘𝑤)))⟩ = ⟨(+g‘ndx), ✚ ⟩)
20	10	fveq2d 6838	. . . . . . . 8 ⊢ (𝑤 = 𝑊 → (oppr‘(Scalar‘𝑤)) = (oppr‘𝑅))
21		ldualset.o	. . . . . . . 8 ⊢ 𝑂 = (oppr‘𝑅)
22	20, 21	eqtr4di 2793	. . . . . . 7 ⊢ (𝑤 = 𝑊 → (oppr‘(Scalar‘𝑤)) = 𝑂)
23	22	opeq2d 4818	. . . . . 6 ⊢ (𝑤 = 𝑊 → ⟨(Scalar‘ndx), (oppr‘(Scalar‘𝑤))⟩ = ⟨(Scalar‘ndx), 𝑂⟩)
24	7, 19, 23	tpeq123d 4687	. . . . 5 ⊢ (𝑤 = 𝑊 → {⟨(Base‘ndx), (LFnl‘𝑤)⟩, ⟨(+g‘ndx), ( ∘f (+g‘(Scalar‘𝑤)) ↾ ((LFnl‘𝑤) × (LFnl‘𝑤)))⟩, ⟨(Scalar‘ndx), (oppr‘(Scalar‘𝑤))⟩} = {⟨(Base‘ndx), 𝐹⟩, ⟨(+g‘ndx), ✚ ⟩, ⟨(Scalar‘ndx), 𝑂⟩})
25	10	fveq2d 6838	. . . . . . . . . 10 ⊢ (𝑤 = 𝑊 → (Base‘(Scalar‘𝑤)) = (Base‘𝑅))
26		ldualset.k	. . . . . . . . . 10 ⊢ 𝐾 = (Base‘𝑅)
27	25, 26	eqtr4di 2793	. . . . . . . . 9 ⊢ (𝑤 = 𝑊 → (Base‘(Scalar‘𝑤)) = 𝐾)
28	10	fveq2d 6838	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝑊 → (.r‘(Scalar‘𝑤)) = (.r‘𝑅))
29		ldualset.t	. . . . . . . . . . . 12 ⊢ · = (.r‘𝑅)
30	28, 29	eqtr4di 2793	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑊 → (.r‘(Scalar‘𝑤)) = · )
31	30	ofeqd 7629	. . . . . . . . . 10 ⊢ (𝑤 = 𝑊 → ∘f (.r‘(Scalar‘𝑤)) = ∘f · )
32		eqidd 2741	. . . . . . . . . 10 ⊢ (𝑤 = 𝑊 → 𝑓 = 𝑓)
33		fveq2 6834	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝑊 → (Base‘𝑤) = (Base‘𝑊))
34		ldualset.v	. . . . . . . . . . . 12 ⊢ 𝑉 = (Base‘𝑊)
35	33, 34	eqtr4di 2793	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑊 → (Base‘𝑤) = 𝑉)
36	35	xpeq1d 5654	. . . . . . . . . 10 ⊢ (𝑤 = 𝑊 → ((Base‘𝑤) × {𝑘}) = (𝑉 × {𝑘}))
37	31, 32, 36	oveq123d 7384	. . . . . . . . 9 ⊢ (𝑤 = 𝑊 → (𝑓 ∘f (.r‘(Scalar‘𝑤))((Base‘𝑤) × {𝑘})) = (𝑓 ∘f · (𝑉 × {𝑘})))
38	27, 6, 37	mpoeq123dv 7438	. . . . . . . 8 ⊢ (𝑤 = 𝑊 → (𝑘 ∈ (Base‘(Scalar‘𝑤)), 𝑓 ∈ (LFnl‘𝑤) ↦ (𝑓 ∘f (.r‘(Scalar‘𝑤))((Base‘𝑤) × {𝑘}))) = (𝑘 ∈ 𝐾, 𝑓 ∈ 𝐹 ↦ (𝑓 ∘f · (𝑉 × {𝑘}))))
39		ldualset.s	. . . . . . . 8 ⊢ ∙ = (𝑘 ∈ 𝐾, 𝑓 ∈ 𝐹 ↦ (𝑓 ∘f · (𝑉 × {𝑘})))
40	38, 39	eqtr4di 2793	. . . . . . 7 ⊢ (𝑤 = 𝑊 → (𝑘 ∈ (Base‘(Scalar‘𝑤)), 𝑓 ∈ (LFnl‘𝑤) ↦ (𝑓 ∘f (.r‘(Scalar‘𝑤))((Base‘𝑤) × {𝑘}))) = ∙ )
41	40	opeq2d 4818	. . . . . 6 ⊢ (𝑤 = 𝑊 → ⟨( ·𝑠 ‘ndx), (𝑘 ∈ (Base‘(Scalar‘𝑤)), 𝑓 ∈ (LFnl‘𝑤) ↦ (𝑓 ∘f (.r‘(Scalar‘𝑤))((Base‘𝑤) × {𝑘})))⟩ = ⟨( ·𝑠 ‘ndx), ∙ ⟩)
42	41	sneqd 4574	. . . . 5 ⊢ (𝑤 = 𝑊 → {⟨( ·𝑠 ‘ndx), (𝑘 ∈ (Base‘(Scalar‘𝑤)), 𝑓 ∈ (LFnl‘𝑤) ↦ (𝑓 ∘f (.r‘(Scalar‘𝑤))((Base‘𝑤) × {𝑘})))⟩} = {⟨( ·𝑠 ‘ndx), ∙ ⟩})
43	24, 42	uneq12d 4106	. . . 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 39623	. . . 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 7696	. . . . 5 ⊢ {⟨(Base‘ndx), 𝐹⟩, ⟨(+g‘ndx), ✚ ⟩, ⟨(Scalar‘ndx), 𝑂⟩} ∈ V
46		snex 5375	. . . . 5 ⊢ {⟨( ·𝑠 ‘ndx), ∙ ⟩} ∈ V
47	45, 46	unex 7694	. . . 4 ⊢ ({⟨(Base‘ndx), 𝐹⟩, ⟨(+g‘ndx), ✚ ⟩, ⟨(Scalar‘ndx), 𝑂⟩} ∪ {⟨( ·𝑠 ‘ndx), ∙ ⟩}) ∈ V
48	43, 44, 47	fvmpt 6942	. . 3 ⊢ (𝑊 ∈ V → (LDual‘𝑊) = ({⟨(Base‘ndx), 𝐹⟩, ⟨(+g‘ndx), ✚ ⟩, ⟨(Scalar‘ndx), 𝑂⟩} ∪ {⟨( ·𝑠 ‘ndx), ∙ ⟩}))
49	3, 48	eqtrid 2787	. 2 ⊢ (𝑊 ∈ V → 𝐷 = ({⟨(Base‘ndx), 𝐹⟩, ⟨(+g‘ndx), ✚ ⟩, ⟨(Scalar‘ndx), 𝑂⟩} ∪ {⟨( ·𝑠 ‘ndx), ∙ ⟩}))
50	1, 2, 49	3syl 18	1 ⊢ (𝜑 → 𝐷 = ({⟨(Base‘ndx), 𝐹⟩, ⟨(+g‘ndx), ✚ ⟩, ⟨(Scalar‘ndx), 𝑂⟩} ∪ {⟨( ·𝑠 ‘ndx), ∙ ⟩}))

Syntax hints:   → wi 4   = wceq 1547   ∈ wcel 2119  Vcvv 3432   ∪ cun 3888  {csn 4562  {ctp 4566  ⟨cop 4568   × cxp 5623   ↾ cres 5627  ‘cfv 6492  (class class class)co 7363   ∈ cmpo 7365   ∘_f cof 7625  ndxcnx 17161  Basecbs 17177  +_gcplusg 17218  ._rcmulr 17219  Scalarcsca 17221   ·_𝑠 cvsca 17222  opp_rcoppr 20314  LFnlclfn 39556  LDualcld 39622

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2712  ax-sep 5225  ax-pr 5369  ax-un 7685

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2719  df-cleq 2732  df-clel 2815  df-nfc 2889  df-ral 3055  df-rex 3065  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-tp 4567  df-op 4569  df-uni 4846  df-br 5080  df-opab 5142  df-mpt 5161  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-res 5637  df-iota 6448  df-fun 6494  df-fv 6500  df-ov 7366  df-oprab 7367  df-mpo 7368  df-of 7627  df-ldual 39623

This theorem is referenced by:  ldualvbase  39625  ldualfvadd  39627  ldualsca  39631  ldualfvs  39635