Metamath Proof Explorer

Theorem lincval0

Description: The value of an empty linear combination. (Contributed by AV, 12-Apr-2019)

Ref Expression
Assertion lincval0 
|- ( M e. X -> ( (/) ( linC ` M ) (/) ) = ( 0g ` M ) )

Proof

Step Hyp Ref Expression
1 0ex 
 |-  (/) e. _V
2 1 snid 
 |-  (/) e. { (/) }
3 fvex 
 |-  ( Base ` ( Scalar ` M ) ) e. _V
4 map0e 
 |-  ( ( Base ` ( Scalar ` M ) ) e. _V -> ( ( Base ` ( Scalar ` M ) ) ^m (/) ) = 1o )
5 3 4 mp1i 
 |-  ( M e. X -> ( ( Base ` ( Scalar ` M ) ) ^m (/) ) = 1o )
6 df1o2 
 |-  1o = { (/) }
7 5 6 eqtrdi 
 |-  ( M e. X -> ( ( Base ` ( Scalar ` M ) ) ^m (/) ) = { (/) } )
8 2 7 eleqtrrid 
 |-  ( M e. X -> (/) e. ( ( Base ` ( Scalar ` M ) ) ^m (/) ) )
9 0elpw 
 |-  (/) e. ~P ( Base ` M )
10 9 a1i 
 |-  ( M e. X -> (/) e. ~P ( Base ` M ) )
11 lincval 
 |-  ( ( M e. X /\ (/) e. ( ( Base ` ( Scalar ` M ) ) ^m (/) ) /\ (/) e. ~P ( Base ` M ) ) -> ( (/) ( linC ` M ) (/) ) = ( M gsum ( v e. (/) |-> ( ( (/) ` v ) ( .s ` M ) v ) ) ) )
12 8 10 11 mpd3an23 
 |-  ( M e. X -> ( (/) ( linC ` M ) (/) ) = ( M gsum ( v e. (/) |-> ( ( (/) ` v ) ( .s ` M ) v ) ) ) )
13 mpt0 
 |-  ( v e. (/) |-> ( ( (/) ` v ) ( .s ` M ) v ) ) = (/)
14 13 a1i 
 |-  ( M e. X -> ( v e. (/) |-> ( ( (/) ` v ) ( .s ` M ) v ) ) = (/) )
15 14 oveq2d 
 |-  ( M e. X -> ( M gsum ( v e. (/) |-> ( ( (/) ` v ) ( .s ` M ) v ) ) ) = ( M gsum (/) ) )
16 eqid 
 |-  ( 0g ` M ) = ( 0g ` M )
17 16 gsum0 
 |-  ( M gsum (/) ) = ( 0g ` M )
18 15 17 eqtrdi 
 |-  ( M e. X -> ( M gsum ( v e. (/) |-> ( ( (/) ` v ) ( .s ` M ) v ) ) ) = ( 0g ` M ) )
19 12 18 eqtrd 
 |-  ( M e. X -> ( (/) ( linC ` M ) (/) ) = ( 0g ` M ) )