Metamath Proof Explorer

Theorem dflinc2

Description: Alternative definition of linear combinations using the function operation. (Contributed by AV, 1-Apr-2019)

Ref Expression
Assertion dflinc2 
|- linC = ( m e. _V |-> ( s e. ( ( Base ` ( Scalar ` m ) ) ^m v ) , v e. ~P ( Base ` m ) |-> ( m gsum ( s oF ( .s ` m ) ( _I |` v ) ) ) ) )

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 ( i e. v |-> ( ( s ` i ) ( .s ` m ) i ) ) ) ) )
2 elmapfn 
 |-  ( s e. ( ( Base ` ( Scalar ` m ) ) ^m v ) -> s Fn v )
3 2 adantr 
 |-  ( ( s e. ( ( Base ` ( Scalar ` m ) ) ^m v ) /\ v e. ~P ( Base ` m ) ) -> s Fn v )
4 fnresi 
 |-  ( _I |` v ) Fn v
5 4 a1i 
 |-  ( ( s e. ( ( Base ` ( Scalar ` m ) ) ^m v ) /\ v e. ~P ( Base ` m ) ) -> ( _I |` v ) Fn v )
6 vex 
 |-  v e. _V
7 6 a1i 
 |-  ( ( s e. ( ( Base ` ( Scalar ` m ) ) ^m v ) /\ v e. ~P ( Base ` m ) ) -> v e. _V )
8 inidm 
 |-  ( v i^i v ) = v
9 eqidd 
 |-  ( ( ( s e. ( ( Base ` ( Scalar ` m ) ) ^m v ) /\ v e. ~P ( Base ` m ) ) /\ i e. v ) -> ( s ` i ) = ( s ` i ) )
10 fvresi 
 |-  ( i e. v -> ( ( _I |` v ) ` i ) = i )
11 10 adantl 
 |-  ( ( ( s e. ( ( Base ` ( Scalar ` m ) ) ^m v ) /\ v e. ~P ( Base ` m ) ) /\ i e. v ) -> ( ( _I |` v ) ` i ) = i )
12 3 5 7 7 8 9 11 offval 
 |-  ( ( s e. ( ( Base ` ( Scalar ` m ) ) ^m v ) /\ v e. ~P ( Base ` m ) ) -> ( s oF ( .s ` m ) ( _I |` v ) ) = ( i e. v |-> ( ( s ` i ) ( .s ` m ) i ) ) )
13 12 eqcomd 
 |-  ( ( s e. ( ( Base ` ( Scalar ` m ) ) ^m v ) /\ v e. ~P ( Base ` m ) ) -> ( i e. v |-> ( ( s ` i ) ( .s ` m ) i ) ) = ( s oF ( .s ` m ) ( _I |` v ) ) )
14 13 oveq2d 
 |-  ( ( s e. ( ( Base ` ( Scalar ` m ) ) ^m v ) /\ v e. ~P ( Base ` m ) ) -> ( m gsum ( i e. v |-> ( ( s ` i ) ( .s ` m ) i ) ) ) = ( m gsum ( s oF ( .s ` m ) ( _I |` v ) ) ) )
15 14 mpoeq3ia 
 |-  ( s e. ( ( Base ` ( Scalar ` m ) ) ^m v ) , v e. ~P ( Base ` m ) |-> ( m gsum ( i e. v |-> ( ( s ` i ) ( .s ` m ) i ) ) ) ) = ( s e. ( ( Base ` ( Scalar ` m ) ) ^m v ) , v e. ~P ( Base ` m ) |-> ( m gsum ( s oF ( .s ` m ) ( _I |` v ) ) ) )
16 15 mpteq2i 
 |-  ( m e. _V |-> ( s e. ( ( Base ` ( Scalar ` m ) ) ^m v ) , v e. ~P ( Base ` m ) |-> ( m gsum ( i e. v |-> ( ( s ` i ) ( .s ` m ) i ) ) ) ) ) = ( m e. _V |-> ( s e. ( ( Base ` ( Scalar ` m ) ) ^m v ) , v e. ~P ( Base ` m ) |-> ( m gsum ( s oF ( .s ` m ) ( _I |` v ) ) ) ) )
17 1 16 eqtri 
 |-  linC = ( m e. _V |-> ( s e. ( ( Base ` ( Scalar ` m ) ) ^m v ) , v e. ~P ( Base ` m ) |-> ( m gsum ( s oF ( .s ` m ) ( _I |` v ) ) ) ) )