Theorem lcdvaddval

Description: The value of the value of vector addition in the closed kernel vector space dual. (Contributed by NM, 10-Jun-2015)

	Ref	Expression
Hypotheses	lcdvaddval.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	lcdvaddval.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
	lcdvaddval.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
	lcdvaddval.r	⊢ 𝑅 = ( Scalar ‘ 𝑈 )
	lcdvaddval.a	⊢ + = ( +g ‘ 𝑅 )
	lcdvaddval.c	⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
	lcdvaddval.d	⊢ 𝐷 = ( Base ‘ 𝐶 )
	lcdvaddval.p	⊢ ✚ = ( +g ‘ 𝐶 )
	lcdvaddval.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
	lcdvaddval.f	⊢ ( 𝜑 → 𝐹 ∈ 𝐷 )
	lcdvaddval.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐷 )
	lcdvaddval.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
Assertion	lcdvaddval	⊢ ( 𝜑 → ( ( 𝐹 ✚ 𝐺 ) ‘ 𝑋 ) = ( ( 𝐹 ‘ 𝑋 ) + ( 𝐺 ‘ 𝑋 ) ) )

Proof

Step	Hyp	Ref	Expression
1		lcdvaddval.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		lcdvaddval.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
3		lcdvaddval.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
4		lcdvaddval.r	⊢ 𝑅 = ( Scalar ‘ 𝑈 )
5		lcdvaddval.a	⊢ + = ( +g ‘ 𝑅 )
6		lcdvaddval.c	⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
7		lcdvaddval.d	⊢ 𝐷 = ( Base ‘ 𝐶 )
8		lcdvaddval.p	⊢ ✚ = ( +g ‘ 𝐶 )
9		lcdvaddval.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
10		lcdvaddval.f	⊢ ( 𝜑 → 𝐹 ∈ 𝐷 )
11		lcdvaddval.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐷 )
12		lcdvaddval.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
13		eqid	⊢ ( LDual ‘ 𝑈 ) = ( LDual ‘ 𝑈 )
14		eqid	⊢ ( +g ‘ ( LDual ‘ 𝑈 ) ) = ( +g ‘ ( LDual ‘ 𝑈 ) )
15	1 2 13 14 6 8 9	lcdvadd	⊢ ( 𝜑 → ✚ = ( +g ‘ ( LDual ‘ 𝑈 ) ) )
16	15	oveqd	⊢ ( 𝜑 → ( 𝐹 ✚ 𝐺 ) = ( 𝐹 ( +g ‘ ( LDual ‘ 𝑈 ) ) 𝐺 ) )
17	16	fveq1d	⊢ ( 𝜑 → ( ( 𝐹 ✚ 𝐺 ) ‘ 𝑋 ) = ( ( 𝐹 ( +g ‘ ( LDual ‘ 𝑈 ) ) 𝐺 ) ‘ 𝑋 ) )
18		eqid	⊢ ( LFnl ‘ 𝑈 ) = ( LFnl ‘ 𝑈 )
19	1 2 9	dvhlmod	⊢ ( 𝜑 → 𝑈 ∈ LMod )
20	1 6 7 2 18 9 10	lcdvbaselfl	⊢ ( 𝜑 → 𝐹 ∈ ( LFnl ‘ 𝑈 ) )
21	1 6 7 2 18 9 11	lcdvbaselfl	⊢ ( 𝜑 → 𝐺 ∈ ( LFnl ‘ 𝑈 ) )
22	3 4 5 18 13 14 19 20 21 12	ldualvaddval	⊢ ( 𝜑 → ( ( 𝐹 ( +g ‘ ( LDual ‘ 𝑈 ) ) 𝐺 ) ‘ 𝑋 ) = ( ( 𝐹 ‘ 𝑋 ) + ( 𝐺 ‘ 𝑋 ) ) )
23	17 22	eqtrd	⊢ ( 𝜑 → ( ( 𝐹 ✚ 𝐺 ) ‘ 𝑋 ) = ( ( 𝐹 ‘ 𝑋 ) + ( 𝐺 ‘ 𝑋 ) ) )