Metamath Proof Explorer


Theorem hdmapln1

Description: Linearity property that will be used for inner product. TODO: try to combine hypotheses in hdmap*ln* series. (Contributed by NM, 7-Jun-2015)

Ref Expression
Hypotheses hdmapln1.h 𝐻 = ( LHyp ‘ 𝐾 )
hdmapln1.u 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
hdmapln1.v 𝑉 = ( Base ‘ 𝑈 )
hdmapln1.p + = ( +g𝑈 )
hdmapln1.t · = ( ·𝑠𝑈 )
hdmapln1.r 𝑅 = ( Scalar ‘ 𝑈 )
hdmapln1.b 𝐵 = ( Base ‘ 𝑅 )
hdmapln1.q = ( +g𝑅 )
hdmapln1.m × = ( .r𝑅 )
hdmapln1.s 𝑆 = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 )
hdmapln1.k ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
hdmapln1.x ( 𝜑𝑋𝑉 )
hdmapln1.y ( 𝜑𝑌𝑉 )
hdmapln1.z ( 𝜑𝑍𝑉 )
hdmapln1.a ( 𝜑𝐴𝐵 )
Assertion hdmapln1 ( 𝜑 → ( ( 𝑆𝑍 ) ‘ ( ( 𝐴 · 𝑋 ) + 𝑌 ) ) = ( ( 𝐴 × ( ( 𝑆𝑍 ) ‘ 𝑋 ) ) ( ( 𝑆𝑍 ) ‘ 𝑌 ) ) )

Proof

Step Hyp Ref Expression
1 hdmapln1.h 𝐻 = ( LHyp ‘ 𝐾 )
2 hdmapln1.u 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
3 hdmapln1.v 𝑉 = ( Base ‘ 𝑈 )
4 hdmapln1.p + = ( +g𝑈 )
5 hdmapln1.t · = ( ·𝑠𝑈 )
6 hdmapln1.r 𝑅 = ( Scalar ‘ 𝑈 )
7 hdmapln1.b 𝐵 = ( Base ‘ 𝑅 )
8 hdmapln1.q = ( +g𝑅 )
9 hdmapln1.m × = ( .r𝑅 )
10 hdmapln1.s 𝑆 = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 )
11 hdmapln1.k ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
12 hdmapln1.x ( 𝜑𝑋𝑉 )
13 hdmapln1.y ( 𝜑𝑌𝑉 )
14 hdmapln1.z ( 𝜑𝑍𝑉 )
15 hdmapln1.a ( 𝜑𝐴𝐵 )
16 1 2 11 dvhlmod ( 𝜑𝑈 ∈ LMod )
17 eqid ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
18 eqid ( Base ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) = ( Base ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) )
19 eqid ( LFnl ‘ 𝑈 ) = ( LFnl ‘ 𝑈 )
20 1 2 3 17 18 10 11 14 hdmapcl ( 𝜑 → ( 𝑆𝑍 ) ∈ ( Base ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) )
21 1 17 18 2 19 11 20 lcdvbaselfl ( 𝜑 → ( 𝑆𝑍 ) ∈ ( LFnl ‘ 𝑈 ) )
22 3 4 6 5 7 8 9 19 lfli ( ( 𝑈 ∈ LMod ∧ ( 𝑆𝑍 ) ∈ ( LFnl ‘ 𝑈 ) ∧ ( 𝐴𝐵𝑋𝑉𝑌𝑉 ) ) → ( ( 𝑆𝑍 ) ‘ ( ( 𝐴 · 𝑋 ) + 𝑌 ) ) = ( ( 𝐴 × ( ( 𝑆𝑍 ) ‘ 𝑋 ) ) ( ( 𝑆𝑍 ) ‘ 𝑌 ) ) )
23 16 21 15 12 13 22 syl113anc ( 𝜑 → ( ( 𝑆𝑍 ) ‘ ( ( 𝐴 · 𝑋 ) + 𝑌 ) ) = ( ( 𝐴 × ( ( 𝑆𝑍 ) ‘ 𝑋 ) ) ( ( 𝑆𝑍 ) ‘ 𝑌 ) ) )