Theorem ldualfvadd

Description: Vector addition in the dual of a vector space. (Contributed by NM, 21-Oct-2014)

	Ref	Expression
Hypotheses	ldualvadd.f	⊢ 𝐹 = ( LFnl ‘ 𝑊 )
	ldualvadd.r	⊢ 𝑅 = ( Scalar ‘ 𝑊 )
	ldualvadd.a	⊢ + = ( +g ‘ 𝑅 )
	ldualvadd.d	⊢ 𝐷 = ( LDual ‘ 𝑊 )
	ldualvadd.p	⊢ ✚ = ( +g ‘ 𝐷 )
	ldualvadd.w	⊢ ( 𝜑 → 𝑊 ∈ 𝑋 )
	ldualfvadd.q	⊢ ⨣ = ( ∘f + ↾ ( 𝐹 × 𝐹 ) )
Assertion	ldualfvadd	⊢ ( 𝜑 → ✚ = ⨣ )

Proof

Step	Hyp	Ref	Expression
1		ldualvadd.f	⊢ 𝐹 = ( LFnl ‘ 𝑊 )
2		ldualvadd.r	⊢ 𝑅 = ( Scalar ‘ 𝑊 )
3		ldualvadd.a	⊢ + = ( +g ‘ 𝑅 )
4		ldualvadd.d	⊢ 𝐷 = ( LDual ‘ 𝑊 )
5		ldualvadd.p	⊢ ✚ = ( +g ‘ 𝐷 )
6		ldualvadd.w	⊢ ( 𝜑 → 𝑊 ∈ 𝑋 )
7		ldualfvadd.q	⊢ ⨣ = ( ∘f + ↾ ( 𝐹 × 𝐹 ) )
8		eqid	⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
9		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
10		eqid	⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
11		eqid	⊢ ( oppr ‘ 𝑅 ) = ( oppr ‘ 𝑅 )
12		eqid	⊢ ( 𝑘 ∈ ( Base ‘ 𝑅 ) , 𝑓 ∈ 𝐹 ↦ ( 𝑓 ∘f ( .r ‘ 𝑅 ) ( ( Base ‘ 𝑊 ) × { 𝑘 } ) ) ) = ( 𝑘 ∈ ( Base ‘ 𝑅 ) , 𝑓 ∈ 𝐹 ↦ ( 𝑓 ∘f ( .r ‘ 𝑅 ) ( ( Base ‘ 𝑊 ) × { 𝑘 } ) ) )
13	8 3 7 1 4 2 9 10 11 12 6	ldualset	⊢ ( 𝜑 → 𝐷 = ( { ⟨ ( Base ‘ ndx ) , 𝐹 ⟩ , ⟨ ( +g ‘ ndx ) , ⨣ ⟩ , ⟨ ( Scalar ‘ ndx ) , ( oppr ‘ 𝑅 ) ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑘 ∈ ( Base ‘ 𝑅 ) , 𝑓 ∈ 𝐹 ↦ ( 𝑓 ∘f ( .r ‘ 𝑅 ) ( ( Base ‘ 𝑊 ) × { 𝑘 } ) ) ) ⟩ } ) )
14	13	fveq2d	⊢ ( 𝜑 → ( +g ‘ 𝐷 ) = ( +g ‘ ( { ⟨ ( Base ‘ ndx ) , 𝐹 ⟩ , ⟨ ( +g ‘ ndx ) , ⨣ ⟩ , ⟨ ( Scalar ‘ ndx ) , ( oppr ‘ 𝑅 ) ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑘 ∈ ( Base ‘ 𝑅 ) , 𝑓 ∈ 𝐹 ↦ ( 𝑓 ∘f ( .r ‘ 𝑅 ) ( ( Base ‘ 𝑊 ) × { 𝑘 } ) ) ) ⟩ } ) ) )
15	1	fvexi	⊢ 𝐹 ∈ V
16		id	⊢ ( 𝐹 ∈ V → 𝐹 ∈ V )
17	16 16	ofmresex	⊢ ( 𝐹 ∈ V → ( ∘f + ↾ ( 𝐹 × 𝐹 ) ) ∈ V )
18	15 17	ax-mp	⊢ ( ∘f + ↾ ( 𝐹 × 𝐹 ) ) ∈ V
19	7 18	eqeltri	⊢ ⨣ ∈ V
20		eqid	⊢ ( { ⟨ ( Base ‘ ndx ) , 𝐹 ⟩ , ⟨ ( +g ‘ ndx ) , ⨣ ⟩ , ⟨ ( Scalar ‘ ndx ) , ( oppr ‘ 𝑅 ) ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑘 ∈ ( Base ‘ 𝑅 ) , 𝑓 ∈ 𝐹 ↦ ( 𝑓 ∘f ( .r ‘ 𝑅 ) ( ( Base ‘ 𝑊 ) × { 𝑘 } ) ) ) ⟩ } ) = ( { ⟨ ( Base ‘ ndx ) , 𝐹 ⟩ , ⟨ ( +g ‘ ndx ) , ⨣ ⟩ , ⟨ ( Scalar ‘ ndx ) , ( oppr ‘ 𝑅 ) ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑘 ∈ ( Base ‘ 𝑅 ) , 𝑓 ∈ 𝐹 ↦ ( 𝑓 ∘f ( .r ‘ 𝑅 ) ( ( Base ‘ 𝑊 ) × { 𝑘 } ) ) ) ⟩ } )
21	20	lmodplusg	⊢ ( ⨣ ∈ V → ⨣ = ( +g ‘ ( { ⟨ ( Base ‘ ndx ) , 𝐹 ⟩ , ⟨ ( +g ‘ ndx ) , ⨣ ⟩ , ⟨ ( Scalar ‘ ndx ) , ( oppr ‘ 𝑅 ) ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑘 ∈ ( Base ‘ 𝑅 ) , 𝑓 ∈ 𝐹 ↦ ( 𝑓 ∘f ( .r ‘ 𝑅 ) ( ( Base ‘ 𝑊 ) × { 𝑘 } ) ) ) ⟩ } ) ) )
22	19 21	ax-mp	⊢ ⨣ = ( +g ‘ ( { ⟨ ( Base ‘ ndx ) , 𝐹 ⟩ , ⟨ ( +g ‘ ndx ) , ⨣ ⟩ , ⟨ ( Scalar ‘ ndx ) , ( oppr ‘ 𝑅 ) ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑘 ∈ ( Base ‘ 𝑅 ) , 𝑓 ∈ 𝐹 ↦ ( 𝑓 ∘f ( .r ‘ 𝑅 ) ( ( Base ‘ 𝑊 ) × { 𝑘 } ) ) ) ⟩ } ) )
23	14 5 22	3eqtr4g	⊢ ( 𝜑 → ✚ = ⨣ )