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 
|- H = ( LHyp ` K )
hdmapln1.u 
|- U = ( ( DVecH ` K ) ` W )
hdmapln1.v 
|- V = ( Base ` U )
hdmapln1.p 
|- .+ = ( +g ` U )
hdmapln1.t 
|- .x. = ( .s ` U )
hdmapln1.r 
|- R = ( Scalar ` U )
hdmapln1.b 
|- B = ( Base ` R )
hdmapln1.q 
|- .+^ = ( +g ` R )
hdmapln1.m 
|- .X. = ( .r ` R )
hdmapln1.s 
|- S = ( ( HDMap ` K ) ` W )
hdmapln1.k 
|- ( ph -> ( K e. HL /\ W e. H ) )
hdmapln1.x 
|- ( ph -> X e. V )
hdmapln1.y 
|- ( ph -> Y e. V )
hdmapln1.z 
|- ( ph -> Z e. V )
hdmapln1.a 
|- ( ph -> A e. B )
Assertion hdmapln1 
|- ( ph -> ( ( S ` Z ) ` ( ( A .x. X ) .+ Y ) ) = ( ( A .X. ( ( S ` Z ) ` X ) ) .+^ ( ( S ` Z ) ` Y ) ) )

Proof

Step Hyp Ref Expression
1 hdmapln1.h 
 |-  H = ( LHyp ` K )
2 hdmapln1.u 
 |-  U = ( ( DVecH ` K ) ` W )
3 hdmapln1.v 
 |-  V = ( Base ` U )
4 hdmapln1.p 
 |-  .+ = ( +g ` U )
5 hdmapln1.t 
 |-  .x. = ( .s ` U )
6 hdmapln1.r 
 |-  R = ( Scalar ` U )
7 hdmapln1.b 
 |-  B = ( Base ` R )
8 hdmapln1.q 
 |-  .+^ = ( +g ` R )
9 hdmapln1.m 
 |-  .X. = ( .r ` R )
10 hdmapln1.s 
 |-  S = ( ( HDMap ` K ) ` W )
11 hdmapln1.k 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
12 hdmapln1.x 
 |-  ( ph -> X e. V )
13 hdmapln1.y 
 |-  ( ph -> Y e. V )
14 hdmapln1.z 
 |-  ( ph -> Z e. V )
15 hdmapln1.a 
 |-  ( ph -> A e. B )
16 1 2 11 dvhlmod 
 |-  ( ph -> U e. LMod )
17 eqid 
 |-  ( ( LCDual ` K ) ` W ) = ( ( LCDual ` K ) ` W )
18 eqid 
 |-  ( Base ` ( ( LCDual ` K ) ` W ) ) = ( Base ` ( ( LCDual ` K ) ` W ) )
19 eqid 
 |-  ( LFnl ` U ) = ( LFnl ` U )
20 1 2 3 17 18 10 11 14 hdmapcl 
 |-  ( ph -> ( S ` Z ) e. ( Base ` ( ( LCDual ` K ) ` W ) ) )
21 1 17 18 2 19 11 20 lcdvbaselfl 
 |-  ( ph -> ( S ` Z ) e. ( LFnl ` U ) )
22 3 4 6 5 7 8 9 19 lfli 
 |-  ( ( U e. LMod /\ ( S ` Z ) e. ( LFnl ` U ) /\ ( A e. B /\ X e. V /\ Y e. V ) ) -> ( ( S ` Z ) ` ( ( A .x. X ) .+ Y ) ) = ( ( A .X. ( ( S ` Z ) ` X ) ) .+^ ( ( S ` Z ) ` Y ) ) )
23 16 21 15 12 13 22 syl113anc 
 |-  ( ph -> ( ( S ` Z ) ` ( ( A .x. X ) .+ Y ) ) = ( ( A .X. ( ( S ` Z ) ` X ) ) .+^ ( ( S ` Z ) ` Y ) ) )