Definition df-ldual

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. The restriction on oF ( +gv ) allows it to be a set; see ofmres . 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)

	Ref	Expression
Assertion	df-ldual	⊢ LDual = ( 𝑣 ∈ V ↦ ( { ⟨ ( Base ‘ ndx ) , ( LFnl ‘ 𝑣 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( ∘f ( +g ‘ ( Scalar ‘ 𝑣 ) ) ↾ ( ( LFnl ‘ 𝑣 ) × ( LFnl ‘ 𝑣 ) ) ) ⟩ , ⟨ ( Scalar ‘ ndx ) , ( oppr ‘ ( Scalar ‘ 𝑣 ) ) ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑣 ) ) , 𝑓 ∈ ( LFnl ‘ 𝑣 ) ↦ ( 𝑓 ∘f ( .r ‘ ( Scalar ‘ 𝑣 ) ) ( ( Base ‘ 𝑣 ) × { 𝑘 } ) ) ) ⟩ } ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cld	⊢ LDual
1		vv	⊢ 𝑣
2		cvv	⊢ V
3		cbs	⊢ Base
4		cnx	⊢ ndx
5	4 3	cfv	⊢ ( Base ‘ ndx )
6		clfn	⊢ LFnl
7	1	cv	⊢ 𝑣
8	7 6	cfv	⊢ ( LFnl ‘ 𝑣 )
9	5 8	cop	⊢ ⟨ ( Base ‘ ndx ) , ( LFnl ‘ 𝑣 ) ⟩
10		cplusg	⊢ +g
11	4 10	cfv	⊢ ( +g ‘ ndx )
12		csca	⊢ Scalar
13	7 12	cfv	⊢ ( Scalar ‘ 𝑣 )
14	13 10	cfv	⊢ ( +g ‘ ( Scalar ‘ 𝑣 ) )
15	14	cof	⊢ ∘f ( +g ‘ ( Scalar ‘ 𝑣 ) )
16	8 8	cxp	⊢ ( ( LFnl ‘ 𝑣 ) × ( LFnl ‘ 𝑣 ) )
17	15 16	cres	⊢ ( ∘f ( +g ‘ ( Scalar ‘ 𝑣 ) ) ↾ ( ( LFnl ‘ 𝑣 ) × ( LFnl ‘ 𝑣 ) ) )
18	11 17	cop	⊢ ⟨ ( +g ‘ ndx ) , ( ∘f ( +g ‘ ( Scalar ‘ 𝑣 ) ) ↾ ( ( LFnl ‘ 𝑣 ) × ( LFnl ‘ 𝑣 ) ) ) ⟩
19	4 12	cfv	⊢ ( Scalar ‘ ndx )
20		coppr	⊢ oppr
21	13 20	cfv	⊢ ( oppr ‘ ( Scalar ‘ 𝑣 ) )
22	19 21	cop	⊢ ⟨ ( Scalar ‘ ndx ) , ( oppr ‘ ( Scalar ‘ 𝑣 ) ) ⟩
23	9 18 22	ctp	⊢ { ⟨ ( Base ‘ ndx ) , ( LFnl ‘ 𝑣 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( ∘f ( +g ‘ ( Scalar ‘ 𝑣 ) ) ↾ ( ( LFnl ‘ 𝑣 ) × ( LFnl ‘ 𝑣 ) ) ) ⟩ , ⟨ ( Scalar ‘ ndx ) , ( oppr ‘ ( Scalar ‘ 𝑣 ) ) ⟩ }
24		cvsca	⊢ ·𝑠
25	4 24	cfv	⊢ ( ·𝑠 ‘ ndx )
26		vk	⊢ 𝑘
27	13 3	cfv	⊢ ( Base ‘ ( Scalar ‘ 𝑣 ) )
28		vf	⊢ 𝑓
29	28	cv	⊢ 𝑓
30		cmulr	⊢ .r
31	13 30	cfv	⊢ ( .r ‘ ( Scalar ‘ 𝑣 ) )
32	31	cof	⊢ ∘f ( .r ‘ ( Scalar ‘ 𝑣 ) )
33	7 3	cfv	⊢ ( Base ‘ 𝑣 )
34	26	cv	⊢ 𝑘
35	34	csn	⊢ { 𝑘 }
36	33 35	cxp	⊢ ( ( Base ‘ 𝑣 ) × { 𝑘 } )
37	29 36 32	co	⊢ ( 𝑓 ∘f ( .r ‘ ( Scalar ‘ 𝑣 ) ) ( ( Base ‘ 𝑣 ) × { 𝑘 } ) )
38	26 28 27 8 37	cmpo	⊢ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑣 ) ) , 𝑓 ∈ ( LFnl ‘ 𝑣 ) ↦ ( 𝑓 ∘f ( .r ‘ ( Scalar ‘ 𝑣 ) ) ( ( Base ‘ 𝑣 ) × { 𝑘 } ) ) )
39	25 38	cop	⊢ ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑣 ) ) , 𝑓 ∈ ( LFnl ‘ 𝑣 ) ↦ ( 𝑓 ∘f ( .r ‘ ( Scalar ‘ 𝑣 ) ) ( ( Base ‘ 𝑣 ) × { 𝑘 } ) ) ) ⟩
40	39	csn	⊢ { ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑣 ) ) , 𝑓 ∈ ( LFnl ‘ 𝑣 ) ↦ ( 𝑓 ∘f ( .r ‘ ( Scalar ‘ 𝑣 ) ) ( ( Base ‘ 𝑣 ) × { 𝑘 } ) ) ) ⟩ }
41	23 40	cun	⊢ ( { ⟨ ( Base ‘ ndx ) , ( LFnl ‘ 𝑣 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( ∘f ( +g ‘ ( Scalar ‘ 𝑣 ) ) ↾ ( ( LFnl ‘ 𝑣 ) × ( LFnl ‘ 𝑣 ) ) ) ⟩ , ⟨ ( Scalar ‘ ndx ) , ( oppr ‘ ( Scalar ‘ 𝑣 ) ) ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑣 ) ) , 𝑓 ∈ ( LFnl ‘ 𝑣 ) ↦ ( 𝑓 ∘f ( .r ‘ ( Scalar ‘ 𝑣 ) ) ( ( Base ‘ 𝑣 ) × { 𝑘 } ) ) ) ⟩ } )
42	1 2 41	cmpt	⊢ ( 𝑣 ∈ V ↦ ( { ⟨ ( Base ‘ ndx ) , ( LFnl ‘ 𝑣 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( ∘f ( +g ‘ ( Scalar ‘ 𝑣 ) ) ↾ ( ( LFnl ‘ 𝑣 ) × ( LFnl ‘ 𝑣 ) ) ) ⟩ , ⟨ ( Scalar ‘ ndx ) , ( oppr ‘ ( Scalar ‘ 𝑣 ) ) ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑣 ) ) , 𝑓 ∈ ( LFnl ‘ 𝑣 ) ↦ ( 𝑓 ∘f ( .r ‘ ( Scalar ‘ 𝑣 ) ) ( ( Base ‘ 𝑣 ) × { 𝑘 } ) ) ) ⟩ } ) )
43	0 42	wceq	⊢ LDual = ( 𝑣 ∈ V ↦ ( { ⟨ ( Base ‘ ndx ) , ( LFnl ‘ 𝑣 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( ∘f ( +g ‘ ( Scalar ‘ 𝑣 ) ) ↾ ( ( LFnl ‘ 𝑣 ) × ( LFnl ‘ 𝑣 ) ) ) ⟩ , ⟨ ( Scalar ‘ ndx ) , ( oppr ‘ ( Scalar ‘ 𝑣 ) ) ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑣 ) ) , 𝑓 ∈ ( LFnl ‘ 𝑣 ) ↦ ( 𝑓 ∘f ( .r ‘ ( Scalar ‘ 𝑣 ) ) ( ( Base ‘ 𝑣 ) × { 𝑘 } ) ) ) ⟩ } ) )