Theorem ldualfvs

Description: Scalar product operation for the dual of a vector space. (Contributed by NM, 18-Oct-2014)

	Ref	Expression
Hypotheses	ldualfvs.f	⊢ 𝐹 = ( LFnl ‘ 𝑊 )
	ldualfvs.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
	ldualfvs.r	⊢ 𝑅 = ( Scalar ‘ 𝑊 )
	ldualfvs.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
	ldualfvs.t	⊢ × = ( .r ‘ 𝑅 )
	ldualfvs.d	⊢ 𝐷 = ( LDual ‘ 𝑊 )
	ldualfvs.s	⊢ ∙ = ( ·𝑠 ‘ 𝐷 )
	ldualfvs.w	⊢ ( 𝜑 → 𝑊 ∈ 𝑌 )
	ldualfvs.m	⊢ · = ( 𝑘 ∈ 𝐾 , 𝑓 ∈ 𝐹 ↦ ( 𝑓 ∘f × ( 𝑉 × { 𝑘 } ) ) )
Assertion	ldualfvs	⊢ ( 𝜑 → ∙ = · )

Proof

Step	Hyp	Ref	Expression
1		ldualfvs.f	⊢ 𝐹 = ( LFnl ‘ 𝑊 )
2		ldualfvs.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
3		ldualfvs.r	⊢ 𝑅 = ( Scalar ‘ 𝑊 )
4		ldualfvs.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
5		ldualfvs.t	⊢ × = ( .r ‘ 𝑅 )
6		ldualfvs.d	⊢ 𝐷 = ( LDual ‘ 𝑊 )
7		ldualfvs.s	⊢ ∙ = ( ·𝑠 ‘ 𝐷 )
8		ldualfvs.w	⊢ ( 𝜑 → 𝑊 ∈ 𝑌 )
9		ldualfvs.m	⊢ · = ( 𝑘 ∈ 𝐾 , 𝑓 ∈ 𝐹 ↦ ( 𝑓 ∘f × ( 𝑉 × { 𝑘 } ) ) )
10		eqid	⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
11		eqid	⊢ ( ∘f ( +g ‘ 𝑅 ) ↾ ( 𝐹 × 𝐹 ) ) = ( ∘f ( +g ‘ 𝑅 ) ↾ ( 𝐹 × 𝐹 ) )
12		eqid	⊢ ( oppr ‘ 𝑅 ) = ( oppr ‘ 𝑅 )
13		eqid	⊢ ( 𝑘 ∈ 𝐾 , 𝑓 ∈ 𝐹 ↦ ( 𝑓 ∘f × ( 𝑉 × { 𝑘 } ) ) ) = ( 𝑘 ∈ 𝐾 , 𝑓 ∈ 𝐹 ↦ ( 𝑓 ∘f × ( 𝑉 × { 𝑘 } ) ) )
14	2 10 11 1 6 3 4 5 12 13 8	ldualset	⊢ ( 𝜑 → 𝐷 = ( { ⟨ ( Base ‘ ndx ) , 𝐹 ⟩ , ⟨ ( +g ‘ ndx ) , ( ∘f ( +g ‘ 𝑅 ) ↾ ( 𝐹 × 𝐹 ) ) ⟩ , ⟨ ( Scalar ‘ ndx ) , ( oppr ‘ 𝑅 ) ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑘 ∈ 𝐾 , 𝑓 ∈ 𝐹 ↦ ( 𝑓 ∘f × ( 𝑉 × { 𝑘 } ) ) ) ⟩ } ) )
15	14	fveq2d	⊢ ( 𝜑 → ( ·𝑠 ‘ 𝐷 ) = ( ·𝑠 ‘ ( { ⟨ ( Base ‘ ndx ) , 𝐹 ⟩ , ⟨ ( +g ‘ ndx ) , ( ∘f ( +g ‘ 𝑅 ) ↾ ( 𝐹 × 𝐹 ) ) ⟩ , ⟨ ( Scalar ‘ ndx ) , ( oppr ‘ 𝑅 ) ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑘 ∈ 𝐾 , 𝑓 ∈ 𝐹 ↦ ( 𝑓 ∘f × ( 𝑉 × { 𝑘 } ) ) ) ⟩ } ) ) )
16	4	fvexi	⊢ 𝐾 ∈ V
17	1	fvexi	⊢ 𝐹 ∈ V
18	16 17	mpoex	⊢ ( 𝑘 ∈ 𝐾 , 𝑓 ∈ 𝐹 ↦ ( 𝑓 ∘f × ( 𝑉 × { 𝑘 } ) ) ) ∈ V
19		eqid	⊢ ( { ⟨ ( Base ‘ ndx ) , 𝐹 ⟩ , ⟨ ( +g ‘ ndx ) , ( ∘f ( +g ‘ 𝑅 ) ↾ ( 𝐹 × 𝐹 ) ) ⟩ , ⟨ ( Scalar ‘ ndx ) , ( oppr ‘ 𝑅 ) ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑘 ∈ 𝐾 , 𝑓 ∈ 𝐹 ↦ ( 𝑓 ∘f × ( 𝑉 × { 𝑘 } ) ) ) ⟩ } ) = ( { ⟨ ( Base ‘ ndx ) , 𝐹 ⟩ , ⟨ ( +g ‘ ndx ) , ( ∘f ( +g ‘ 𝑅 ) ↾ ( 𝐹 × 𝐹 ) ) ⟩ , ⟨ ( Scalar ‘ ndx ) , ( oppr ‘ 𝑅 ) ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑘 ∈ 𝐾 , 𝑓 ∈ 𝐹 ↦ ( 𝑓 ∘f × ( 𝑉 × { 𝑘 } ) ) ) ⟩ } )
20	19	lmodvsca	⊢ ( ( 𝑘 ∈ 𝐾 , 𝑓 ∈ 𝐹 ↦ ( 𝑓 ∘f × ( 𝑉 × { 𝑘 } ) ) ) ∈ V → ( 𝑘 ∈ 𝐾 , 𝑓 ∈ 𝐹 ↦ ( 𝑓 ∘f × ( 𝑉 × { 𝑘 } ) ) ) = ( ·𝑠 ‘ ( { ⟨ ( Base ‘ ndx ) , 𝐹 ⟩ , ⟨ ( +g ‘ ndx ) , ( ∘f ( +g ‘ 𝑅 ) ↾ ( 𝐹 × 𝐹 ) ) ⟩ , ⟨ ( Scalar ‘ ndx ) , ( oppr ‘ 𝑅 ) ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑘 ∈ 𝐾 , 𝑓 ∈ 𝐹 ↦ ( 𝑓 ∘f × ( 𝑉 × { 𝑘 } ) ) ) ⟩ } ) ) )
21	18 20	ax-mp	⊢ ( 𝑘 ∈ 𝐾 , 𝑓 ∈ 𝐹 ↦ ( 𝑓 ∘f × ( 𝑉 × { 𝑘 } ) ) ) = ( ·𝑠 ‘ ( { ⟨ ( Base ‘ ndx ) , 𝐹 ⟩ , ⟨ ( +g ‘ ndx ) , ( ∘f ( +g ‘ 𝑅 ) ↾ ( 𝐹 × 𝐹 ) ) ⟩ , ⟨ ( Scalar ‘ ndx ) , ( oppr ‘ 𝑅 ) ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑘 ∈ 𝐾 , 𝑓 ∈ 𝐹 ↦ ( 𝑓 ∘f × ( 𝑉 × { 𝑘 } ) ) ) ⟩ } ) )
22	9 21	eqtri	⊢ · = ( ·𝑠 ‘ ( { ⟨ ( Base ‘ ndx ) , 𝐹 ⟩ , ⟨ ( +g ‘ ndx ) , ( ∘f ( +g ‘ 𝑅 ) ↾ ( 𝐹 × 𝐹 ) ) ⟩ , ⟨ ( Scalar ‘ ndx ) , ( oppr ‘ 𝑅 ) ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑘 ∈ 𝐾 , 𝑓 ∈ 𝐹 ↦ ( 𝑓 ∘f × ( 𝑉 × { 𝑘 } ) ) ) ⟩ } ) )
23	15 7 22	3eqtr4g	⊢ ( 𝜑 → ∙ = · )