Metamath Proof Explorer

Theorem lincop

Description: A linear combination as operation. (Contributed by AV, 30-Mar-2019)

Ref Expression
Assertion 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 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 df-linc 
 |-  linC = ( m e. _V |-> ( s e. ( ( Base ` ( Scalar ` m ) ) ^m v ) , v e. ~P ( Base ` m ) |-> ( m gsum ( x e. v |-> ( ( s ` x ) ( .s ` m ) x ) ) ) ) )
2 2fveq3 
 |-  ( m = M -> ( Base ` ( Scalar ` m ) ) = ( Base ` ( Scalar ` M ) ) )
3 2 oveq1d 
 |-  ( m = M -> ( ( Base ` ( Scalar ` m ) ) ^m v ) = ( ( Base ` ( Scalar ` M ) ) ^m v ) )
4 fveq2 
 |-  ( m = M -> ( Base ` m ) = ( Base ` M ) )
5 4 pweqd 
 |-  ( m = M -> ~P ( Base ` m ) = ~P ( Base ` M ) )
6 id 
 |-  ( m = M -> m = M )
7 fveq2 
 |-  ( m = M -> ( .s ` m ) = ( .s ` M ) )
8 7 oveqd 
 |-  ( m = M -> ( ( s ` x ) ( .s ` m ) x ) = ( ( s ` x ) ( .s ` M ) x ) )
9 8 mpteq2dv 
 |-  ( m = M -> ( x e. v |-> ( ( s ` x ) ( .s ` m ) x ) ) = ( x e. v |-> ( ( s ` x ) ( .s ` M ) x ) ) )
10 6 9 oveq12d 
 |-  ( m = M -> ( m gsum ( x e. v |-> ( ( s ` x ) ( .s ` m ) x ) ) ) = ( M gsum ( x e. v |-> ( ( s ` x ) ( .s ` M ) x ) ) ) )
11 3 5 10 mpoeq123dv 
 |-  ( m = M -> ( 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 ) ) ) ) )
12 elex 
 |-  ( M e. X -> M e. _V )
13 fvex 
 |-  ( Base ` M ) e. _V
14 13 pwex 
 |-  ~P ( Base ` M ) e. _V
15 ovexd 
 |-  ( M e. X -> ( ( Base ` ( Scalar ` M ) ) ^m v ) e. _V )
16 15 ralrimivw 
 |-  ( M e. X -> A. v e. ~P ( Base ` M ) ( ( Base ` ( Scalar ` M ) ) ^m v ) e. _V )
17 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 ) ) ) )
18 17 mpoexxg2 
 |-  ( ( ~P ( Base ` M ) e. _V /\ A. v e. ~P ( Base ` M ) ( ( Base ` ( Scalar ` M ) ) ^m v ) e. _V ) -> ( s e. ( ( Base ` ( Scalar ` M ) ) ^m v ) , v e. ~P ( Base ` M ) |-> ( M gsum ( x e. v |-> ( ( s ` x ) ( .s ` M ) x ) ) ) ) e. _V )
19 14 16 18 sylancr 
 |-  ( 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 )
20 1 11 12 19 fvmptd3 
 |-  ( 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 ) ) ) ) )