Metamath Proof Explorer

Theorem ldualset

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)

Ref Expression
Hypotheses 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 ldualset ( 𝜑 → 𝐷 = ( { ⟨ ( Base ‘ ndx ) , 𝐹 ⟩ , ⟨ ( +g ‘ ndx ) , ✚ ⟩ , ⟨ ( Scalar ‘ ndx ) , 𝑂 ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , ∙ ⟩ } ) )

Proof

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