ldualvaddval

Description: The value of the value of vector addition in the dual of a vector space. (Contributed by NM, 7-Jan-2015)

	Ref	Expression
Hypotheses	ldualvaddval.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
	ldualvaddval.r	⊢ 𝑅 = ( Scalar ‘ 𝑊 )
	ldualvaddval.a	⊢ + = ( +_g ‘ 𝑅 )
	ldualvaddval.f	⊢ 𝐹 = ( LFnl ‘ 𝑊 )
	ldualvaddval.d	⊢ 𝐷 = ( LDual ‘ 𝑊 )
	ldualvaddval.p	⊢ ✚ = ( +_g ‘ 𝐷 )
	ldualvaddval.w	⊢ ( 𝜑 → 𝑊 ∈ LMod )
	ldualvaddval.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
	ldualvaddval.h	⊢ ( 𝜑 → 𝐻 ∈ 𝐹 )
	ldualvaddval.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
Assertion	ldualvaddval	⊢ ( 𝜑 → ( ( 𝐺 ✚ 𝐻 ) ‘ 𝑋 ) = ( ( 𝐺 ‘ 𝑋 ) + ( 𝐻 ‘ 𝑋 ) ) )

Proof

Step	Hyp	Ref	Expression
1		ldualvaddval.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
2		ldualvaddval.r	⊢ 𝑅 = ( Scalar ‘ 𝑊 )
3		ldualvaddval.a	⊢ + = ( +_g ‘ 𝑅 )
4		ldualvaddval.f	⊢ 𝐹 = ( LFnl ‘ 𝑊 )
5		ldualvaddval.d	⊢ 𝐷 = ( LDual ‘ 𝑊 )
6		ldualvaddval.p	⊢ ✚ = ( +_g ‘ 𝐷 )
7		ldualvaddval.w	⊢ ( 𝜑 → 𝑊 ∈ LMod )
8		ldualvaddval.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
9		ldualvaddval.h	⊢ ( 𝜑 → 𝐻 ∈ 𝐹 )
10		ldualvaddval.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
11	4 2 3 5 6 7 8 9	ldualvadd	⊢ ( 𝜑 → ( 𝐺 ✚ 𝐻 ) = ( 𝐺 ∘_f + 𝐻 ) )
12	11	fveq1d	⊢ ( 𝜑 → ( ( 𝐺 ✚ 𝐻 ) ‘ 𝑋 ) = ( ( 𝐺 ∘_f + 𝐻 ) ‘ 𝑋 ) )
13		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
14	2 13 1 4	lflf	⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ) → 𝐺 : 𝑉 ⟶ ( Base ‘ 𝑅 ) )
15	14	ffnd	⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ) → 𝐺 Fn 𝑉 )
16	7 8 15	syl2anc	⊢ ( 𝜑 → 𝐺 Fn 𝑉 )
17	2 13 1 4	lflf	⊢ ( ( 𝑊 ∈ LMod ∧ 𝐻 ∈ 𝐹 ) → 𝐻 : 𝑉 ⟶ ( Base ‘ 𝑅 ) )
18	17	ffnd	⊢ ( ( 𝑊 ∈ LMod ∧ 𝐻 ∈ 𝐹 ) → 𝐻 Fn 𝑉 )
19	7 9 18	syl2anc	⊢ ( 𝜑 → 𝐻 Fn 𝑉 )
20	1	fvexi	⊢ 𝑉 ∈ V
21	20	a1i	⊢ ( 𝜑 → 𝑉 ∈ V )
22		inidm	⊢ ( 𝑉 ∩ 𝑉 ) = 𝑉
23		eqidd	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑉 ) → ( 𝐺 ‘ 𝑋 ) = ( 𝐺 ‘ 𝑋 ) )
24		eqidd	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑉 ) → ( 𝐻 ‘ 𝑋 ) = ( 𝐻 ‘ 𝑋 ) )
25	16 19 21 21 22 23 24	ofval	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑉 ) → ( ( 𝐺 ∘_f + 𝐻 ) ‘ 𝑋 ) = ( ( 𝐺 ‘ 𝑋 ) + ( 𝐻 ‘ 𝑋 ) ) )
26	10 25	mpdan	⊢ ( 𝜑 → ( ( 𝐺 ∘_f + 𝐻 ) ‘ 𝑋 ) = ( ( 𝐺 ‘ 𝑋 ) + ( 𝐻 ‘ 𝑋 ) ) )
27	12 26	eqtrd	⊢ ( 𝜑 → ( ( 𝐺 ✚ 𝐻 ) ‘ 𝑋 ) = ( ( 𝐺 ‘ 𝑋 ) + ( 𝐻 ‘ 𝑋 ) ) )

Metamath Proof Explorer

Theorem ldualvaddval

Proof