Metamath Proof Explorer


Theorem lcdsmul

Description: Scalar multiplication for the closed kernel vector space dual. (Contributed by NM, 20-Mar-2015)

Ref Expression
Hypotheses lcdsmul.h 𝐻 = ( LHyp ‘ 𝐾 )
lcdsmul.u 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
lcdsmul.f 𝐹 = ( Scalar ‘ 𝑈 )
lcdsmul.l 𝐿 = ( Base ‘ 𝐹 )
lcdsmul.t · = ( .r𝐹 )
lcdsmul.c 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
lcdsmul.s 𝑆 = ( Scalar ‘ 𝐶 )
lcdsmul.m = ( .r𝑆 )
lcdsmul.k ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
lcdsmul.x ( 𝜑𝑋𝐿 )
lcdsmul.y ( 𝜑𝑌𝐿 )
Assertion lcdsmul ( 𝜑 → ( 𝑋 𝑌 ) = ( 𝑌 · 𝑋 ) )

Proof

Step Hyp Ref Expression
1 lcdsmul.h 𝐻 = ( LHyp ‘ 𝐾 )
2 lcdsmul.u 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
3 lcdsmul.f 𝐹 = ( Scalar ‘ 𝑈 )
4 lcdsmul.l 𝐿 = ( Base ‘ 𝐹 )
5 lcdsmul.t · = ( .r𝐹 )
6 lcdsmul.c 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
7 lcdsmul.s 𝑆 = ( Scalar ‘ 𝐶 )
8 lcdsmul.m = ( .r𝑆 )
9 lcdsmul.k ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
10 lcdsmul.x ( 𝜑𝑋𝐿 )
11 lcdsmul.y ( 𝜑𝑌𝐿 )
12 eqid ( oppr𝐹 ) = ( oppr𝐹 )
13 1 2 3 12 6 7 9 lcdsca ( 𝜑𝑆 = ( oppr𝐹 ) )
14 13 fveq2d ( 𝜑 → ( .r𝑆 ) = ( .r ‘ ( oppr𝐹 ) ) )
15 8 14 syl5eq ( 𝜑 = ( .r ‘ ( oppr𝐹 ) ) )
16 15 oveqd ( 𝜑 → ( 𝑋 𝑌 ) = ( 𝑋 ( .r ‘ ( oppr𝐹 ) ) 𝑌 ) )
17 eqid ( .r ‘ ( oppr𝐹 ) ) = ( .r ‘ ( oppr𝐹 ) )
18 4 5 12 17 opprmul ( 𝑋 ( .r ‘ ( oppr𝐹 ) ) 𝑌 ) = ( 𝑌 · 𝑋 )
19 16 18 eqtrdi ( 𝜑 → ( 𝑋 𝑌 ) = ( 𝑌 · 𝑋 ) )