Theorem ldualset 36265

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 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 3515	. 2 ⊢ (𝑊 ∈ 𝑋 → 𝑊 ∈ V)
3		ldualset.d	. . 3 ⊢ 𝐷 = (LDual‘𝑊)
4		fveq2 6673	. . . . . . . 8 ⊢ (𝑤 = 𝑊 → (LFnl‘𝑤) = (LFnl‘𝑊))
5		ldualset.f	. . . . . . . 8 ⊢ 𝐹 = (LFnl‘𝑊)
6	4, 5	syl6eqr 2877	. . . . . . 7 ⊢ (𝑤 = 𝑊 → (LFnl‘𝑤) = 𝐹)
7	6	opeq2d 4813	. . . . . 6 ⊢ (𝑤 = 𝑊 → ⟨(Base‘ndx), (LFnl‘𝑤)⟩ = ⟨(Base‘ndx), 𝐹⟩)
8		fveq2 6673	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝑊 → (Scalar‘𝑤) = (Scalar‘𝑊))
9		ldualset.r	. . . . . . . . . . . . 13 ⊢ 𝑅 = (Scalar‘𝑊)
10	8, 9	syl6eqr 2877	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝑊 → (Scalar‘𝑤) = 𝑅)
11	10	fveq2d 6677	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑊 → (+g‘(Scalar‘𝑤)) = (+g‘𝑅))
12		ldualset.a	. . . . . . . . . . 11 ⊢ + = (+g‘𝑅)
13	11, 12	syl6eqr 2877	. . . . . . . . . 10 ⊢ (𝑤 = 𝑊 → (+g‘(Scalar‘𝑤)) = + )
14		ofeq 7414	. . . . . . . . . 10 ⊢ ((+g‘(Scalar‘𝑤)) = + → ∘f (+g‘(Scalar‘𝑤)) = ∘f + )
15	13, 14	syl 17	. . . . . . . . 9 ⊢ (𝑤 = 𝑊 → ∘f (+g‘(Scalar‘𝑤)) = ∘f + )
16	6	sqxpeqd 5590	. . . . . . . . 9 ⊢ (𝑤 = 𝑊 → ((LFnl‘𝑤) × (LFnl‘𝑤)) = (𝐹 × 𝐹))
17	15, 16	reseq12d 5857	. . . . . . . 8 ⊢ (𝑤 = 𝑊 → ( ∘f (+g‘(Scalar‘𝑤)) ↾ ((LFnl‘𝑤) × (LFnl‘𝑤))) = ( ∘f + ↾ (𝐹 × 𝐹)))
18		ldualset.p	. . . . . . . 8 ⊢ ✚ = ( ∘f + ↾ (𝐹 × 𝐹))
19	17, 18	syl6eqr 2877	. . . . . . 7 ⊢ (𝑤 = 𝑊 → ( ∘f (+g‘(Scalar‘𝑤)) ↾ ((LFnl‘𝑤) × (LFnl‘𝑤))) = ✚ )
20	19	opeq2d 4813	. . . . . 6 ⊢ (𝑤 = 𝑊 → ⟨(+g‘ndx), ( ∘f (+g‘(Scalar‘𝑤)) ↾ ((LFnl‘𝑤) × (LFnl‘𝑤)))⟩ = ⟨(+g‘ndx), ✚ ⟩)
21	10	fveq2d 6677	. . . . . . . 8 ⊢ (𝑤 = 𝑊 → (oppr‘(Scalar‘𝑤)) = (oppr‘𝑅))
22		ldualset.o	. . . . . . . 8 ⊢ 𝑂 = (oppr‘𝑅)
23	21, 22	syl6eqr 2877	. . . . . . 7 ⊢ (𝑤 = 𝑊 → (oppr‘(Scalar‘𝑤)) = 𝑂)
24	23	opeq2d 4813	. . . . . 6 ⊢ (𝑤 = 𝑊 → ⟨(Scalar‘ndx), (oppr‘(Scalar‘𝑤))⟩ = ⟨(Scalar‘ndx), 𝑂⟩)
25	7, 20, 24	tpeq123d 4687	. . . . 5 ⊢ (𝑤 = 𝑊 → {⟨(Base‘ndx), (LFnl‘𝑤)⟩, ⟨(+g‘ndx), ( ∘f (+g‘(Scalar‘𝑤)) ↾ ((LFnl‘𝑤) × (LFnl‘𝑤)))⟩, ⟨(Scalar‘ndx), (oppr‘(Scalar‘𝑤))⟩} = {⟨(Base‘ndx), 𝐹⟩, ⟨(+g‘ndx), ✚ ⟩, ⟨(Scalar‘ndx), 𝑂⟩})
26	10	fveq2d 6677	. . . . . . . . . 10 ⊢ (𝑤 = 𝑊 → (Base‘(Scalar‘𝑤)) = (Base‘𝑅))
27		ldualset.k	. . . . . . . . . 10 ⊢ 𝐾 = (Base‘𝑅)
28	26, 27	syl6eqr 2877	. . . . . . . . 9 ⊢ (𝑤 = 𝑊 → (Base‘(Scalar‘𝑤)) = 𝐾)
29	10	fveq2d 6677	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝑊 → (.r‘(Scalar‘𝑤)) = (.r‘𝑅))
30		ldualset.t	. . . . . . . . . . . 12 ⊢ · = (.r‘𝑅)
31	29, 30	syl6eqr 2877	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑊 → (.r‘(Scalar‘𝑤)) = · )
32		ofeq 7414	. . . . . . . . . . 11 ⊢ ((.r‘(Scalar‘𝑤)) = · → ∘f (.r‘(Scalar‘𝑤)) = ∘f · )
33	31, 32	syl 17	. . . . . . . . . 10 ⊢ (𝑤 = 𝑊 → ∘f (.r‘(Scalar‘𝑤)) = ∘f · )
34		eqidd 2825	. . . . . . . . . 10 ⊢ (𝑤 = 𝑊 → 𝑓 = 𝑓)
35		fveq2 6673	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝑊 → (Base‘𝑤) = (Base‘𝑊))
36		ldualset.v	. . . . . . . . . . . 12 ⊢ 𝑉 = (Base‘𝑊)
37	35, 36	syl6eqr 2877	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑊 → (Base‘𝑤) = 𝑉)
38	37	xpeq1d 5587	. . . . . . . . . 10 ⊢ (𝑤 = 𝑊 → ((Base‘𝑤) × {𝑘}) = (𝑉 × {𝑘}))
39	33, 34, 38	oveq123d 7180	. . . . . . . . 9 ⊢ (𝑤 = 𝑊 → (𝑓 ∘f (.r‘(Scalar‘𝑤))((Base‘𝑤) × {𝑘})) = (𝑓 ∘f · (𝑉 × {𝑘})))
40	28, 6, 39	mpoeq123dv 7232	. . . . . . . 8 ⊢ (𝑤 = 𝑊 → (𝑘 ∈ (Base‘(Scalar‘𝑤)), 𝑓 ∈ (LFnl‘𝑤) ↦ (𝑓 ∘f (.r‘(Scalar‘𝑤))((Base‘𝑤) × {𝑘}))) = (𝑘 ∈ 𝐾, 𝑓 ∈ 𝐹 ↦ (𝑓 ∘f · (𝑉 × {𝑘}))))
41		ldualset.s	. . . . . . . 8 ⊢ ∙ = (𝑘 ∈ 𝐾, 𝑓 ∈ 𝐹 ↦ (𝑓 ∘f · (𝑉 × {𝑘})))
42	40, 41	syl6eqr 2877	. . . . . . 7 ⊢ (𝑤 = 𝑊 → (𝑘 ∈ (Base‘(Scalar‘𝑤)), 𝑓 ∈ (LFnl‘𝑤) ↦ (𝑓 ∘f (.r‘(Scalar‘𝑤))((Base‘𝑤) × {𝑘}))) = ∙ )
43	42	opeq2d 4813	. . . . . 6 ⊢ (𝑤 = 𝑊 → ⟨( ·𝑠 ‘ndx), (𝑘 ∈ (Base‘(Scalar‘𝑤)), 𝑓 ∈ (LFnl‘𝑤) ↦ (𝑓 ∘f (.r‘(Scalar‘𝑤))((Base‘𝑤) × {𝑘})))⟩ = ⟨( ·𝑠 ‘ndx), ∙ ⟩)
44	43	sneqd 4582	. . . . 5 ⊢ (𝑤 = 𝑊 → {⟨( ·𝑠 ‘ndx), (𝑘 ∈ (Base‘(Scalar‘𝑤)), 𝑓 ∈ (LFnl‘𝑤) ↦ (𝑓 ∘f (.r‘(Scalar‘𝑤))((Base‘𝑤) × {𝑘})))⟩} = {⟨( ·𝑠 ‘ndx), ∙ ⟩})
45	25, 44	uneq12d 4143	. . . 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 36264	. . . 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 7473	. . . . 5 ⊢ {⟨(Base‘ndx), 𝐹⟩, ⟨(+g‘ndx), ✚ ⟩, ⟨(Scalar‘ndx), 𝑂⟩} ∈ V
48		snex 5335	. . . . 5 ⊢ {⟨( ·𝑠 ‘ndx), ∙ ⟩} ∈ V
49	47, 48	unex 7472	. . . 4 ⊢ ({⟨(Base‘ndx), 𝐹⟩, ⟨(+g‘ndx), ✚ ⟩, ⟨(Scalar‘ndx), 𝑂⟩} ∪ {⟨( ·𝑠 ‘ndx), ∙ ⟩}) ∈ V
50	45, 46, 49	fvmpt 6771	. . 3 ⊢ (𝑊 ∈ V → (LDual‘𝑊) = ({⟨(Base‘ndx), 𝐹⟩, ⟨(+g‘ndx), ✚ ⟩, ⟨(Scalar‘ndx), 𝑂⟩} ∪ {⟨( ·𝑠 ‘ndx), ∙ ⟩}))
51	3, 50	syl5eq 2871	. 2 ⊢ (𝑊 ∈ V → 𝐷 = ({⟨(Base‘ndx), 𝐹⟩, ⟨(+g‘ndx), ✚ ⟩, ⟨(Scalar‘ndx), 𝑂⟩} ∪ {⟨( ·𝑠 ‘ndx), ∙ ⟩}))
52	1, 2, 51	3syl 18	1 ⊢ (𝜑 → 𝐷 = ({⟨(Base‘ndx), 𝐹⟩, ⟨(+g‘ndx), ✚ ⟩, ⟨(Scalar‘ndx), 𝑂⟩} ∪ {⟨( ·𝑠 ‘ndx), ∙ ⟩}))

Syntax hints:   → wi 4   = wceq 1536   ∈ wcel 2113  Vcvv 3497   ∪ cun 3937  {csn 4570  {ctp 4574  ⟨cop 4576   × cxp 5556   ↾ cres 5560  ‘cfv 6358  (class class class)co 7159   ∈ cmpo 7161   ∘_f cof 7410  ndxcnx 16483  Basecbs 16486  +_gcplusg 16568  ._rcmulr 16569  Scalarcsca 16571   ·_𝑠 cvsca 16572  opp_rcoppr 19375  LFnlclfn 36197  LDualcld 36263

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2796  ax-sep 5206  ax-nul 5213  ax-pr 5333  ax-un 7464

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-mo 2621  df-eu 2653  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2966  df-ral 3146  df-rex 3147  df-rab 3150  df-v 3499  df-sbc 3776  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-nul 4295  df-if 4471  df-sn 4571  df-pr 4573  df-tp 4575  df-op 4577  df-uni 4842  df-br 5070  df-opab 5132  df-mpt 5150  df-id 5463  df-xp 5564  df-rel 5565  df-cnv 5566  df-co 5567  df-dm 5568  df-res 5570  df-iota 6317  df-fun 6360  df-fv 6366  df-ov 7162  df-oprab 7163  df-mpo 7164  df-of 7412  df-ldual 36264

This theorem is referenced by:  ldualvbase  36266  ldualfvadd  36268  ldualsca  36272  ldualfvs  36276