Metamath Proof Explorer


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 ( 𝜑 → ( ( 𝐹 𝐺 ) ‘ 𝑋 ) = ( ( 𝐹𝑋 ) + ( 𝐺𝑋 ) ) )