Metamath Proof Explorer

Theorem lincval

Description: The value of a linear combination. (Contributed by AV, 30-Mar-2019)

Ref Expression
Assertion lincval 
|- ( ( M e. X /\ S e. ( ( Base ` ( Scalar ` M ) ) ^m V ) /\ V e. ~P ( Base ` M ) ) -> ( S ( linC ` M ) V ) = ( M gsum ( x e. V |-> ( ( S ` x ) ( .s ` M ) x ) ) ) )

Proof

Step Hyp Ref Expression
1 lincop 
 |-  ( M e. X -> ( linC ` M ) = ( s e. ( ( Base ` ( Scalar ` M ) ) ^m v ) , v e. ~P ( Base ` M ) |-> ( M gsum ( x e. v |-> ( ( s ` x ) ( .s ` M ) x ) ) ) ) )
2 1 3ad2ant1 
 |-  ( ( M e. X /\ S e. ( ( Base ` ( Scalar ` M ) ) ^m V ) /\ V e. ~P ( Base ` M ) ) -> ( linC ` M ) = ( s e. ( ( Base ` ( Scalar ` M ) ) ^m v ) , v e. ~P ( Base ` M ) |-> ( M gsum ( x e. v |-> ( ( s ` x ) ( .s ` M ) x ) ) ) ) )
3 2 oveqd 
 |-  ( ( M e. X /\ S e. ( ( Base ` ( Scalar ` M ) ) ^m V ) /\ V e. ~P ( Base ` M ) ) -> ( S ( linC ` M ) V ) = ( S ( s e. ( ( Base ` ( Scalar ` M ) ) ^m v ) , v e. ~P ( Base ` M ) |-> ( M gsum ( x e. v |-> ( ( s ` x ) ( .s ` M ) x ) ) ) ) V ) )
4 simp2 
 |-  ( ( M e. X /\ S e. ( ( Base ` ( Scalar ` M ) ) ^m V ) /\ V e. ~P ( Base ` M ) ) -> S e. ( ( Base ` ( Scalar ` M ) ) ^m V ) )
5 simp3 
 |-  ( ( M e. X /\ S e. ( ( Base ` ( Scalar ` M ) ) ^m V ) /\ V e. ~P ( Base ` M ) ) -> V e. ~P ( Base ` M ) )
6 ovexd 
 |-  ( ( M e. X /\ S e. ( ( Base ` ( Scalar ` M ) ) ^m V ) /\ V e. ~P ( Base ` M ) ) -> ( M gsum ( x e. V |-> ( ( S ` x ) ( .s ` M ) x ) ) ) e. _V )
7 simpr 
 |-  ( ( s = S /\ v = V ) -> v = V )
8 fveq1 
 |-  ( s = S -> ( s ` x ) = ( S ` x ) )
9 8 oveq1d 
 |-  ( s = S -> ( ( s ` x ) ( .s ` M ) x ) = ( ( S ` x ) ( .s ` M ) x ) )
10 9 adantr 
 |-  ( ( s = S /\ v = V ) -> ( ( s ` x ) ( .s ` M ) x ) = ( ( S ` x ) ( .s ` M ) x ) )
11 7 10 mpteq12dv 
 |-  ( ( s = S /\ v = V ) -> ( x e. v |-> ( ( s ` x ) ( .s ` M ) x ) ) = ( x e. V |-> ( ( S ` x ) ( .s ` M ) x ) ) )
12 11 oveq2d 
 |-  ( ( s = S /\ v = V ) -> ( M gsum ( x e. v |-> ( ( s ` x ) ( .s ` M ) x ) ) ) = ( M gsum ( x e. V |-> ( ( S ` x ) ( .s ` M ) x ) ) ) )
13 oveq2 
 |-  ( v = V -> ( ( Base ` ( Scalar ` M ) ) ^m v ) = ( ( Base ` ( Scalar ` M ) ) ^m V ) )
14 eqid 
 |-  ( s e. ( ( Base ` ( Scalar ` M ) ) ^m v ) , v e. ~P ( Base ` M ) |-> ( M gsum ( x e. v |-> ( ( s ` x ) ( .s ` M ) x ) ) ) ) = ( s e. ( ( Base ` ( Scalar ` M ) ) ^m v ) , v e. ~P ( Base ` M ) |-> ( M gsum ( x e. v |-> ( ( s ` x ) ( .s ` M ) x ) ) ) )
15 12 13 14 ovmpox2 
 |-  ( ( S e. ( ( Base ` ( Scalar ` M ) ) ^m V ) /\ V e. ~P ( Base ` M ) /\ ( M gsum ( x e. V |-> ( ( S ` x ) ( .s ` M ) x ) ) ) e. _V ) -> ( S ( s e. ( ( Base ` ( Scalar ` M ) ) ^m v ) , v e. ~P ( Base ` M ) |-> ( M gsum ( x e. v |-> ( ( s ` x ) ( .s ` M ) x ) ) ) ) V ) = ( M gsum ( x e. V |-> ( ( S ` x ) ( .s ` M ) x ) ) ) )
16 4 5 6 15 syl3anc 
 |-  ( ( M e. X /\ S e. ( ( Base ` ( Scalar ` M ) ) ^m V ) /\ V e. ~P ( Base ` M ) ) -> ( S ( s e. ( ( Base ` ( Scalar ` M ) ) ^m v ) , v e. ~P ( Base ` M ) |-> ( M gsum ( x e. v |-> ( ( s ` x ) ( .s ` M ) x ) ) ) ) V ) = ( M gsum ( x e. V |-> ( ( S ` x ) ( .s ` M ) x ) ) ) )
17 3 16 eqtrd 
 |-  ( ( M e. X /\ S e. ( ( Base ` ( Scalar ` M ) ) ^m V ) /\ V e. ~P ( Base ` M ) ) -> ( S ( linC ` M ) V ) = ( M gsum ( x e. V |-> ( ( S ` x ) ( .s ` M ) x ) ) ) )