Metamath Proof Explorer

Theorem lcoop

Description: A linear combination as operation. (Contributed by AV, 5-Apr-2019) (Revised by AV, 28-Jul-2019)

Ref Expression
Hypotheses lcoop.b 
|- B = ( Base ` M )
lcoop.s 
|- S = ( Scalar ` M )
lcoop.r 
|- R = ( Base ` S )
Assertion lcoop 
|- ( ( M e. X /\ V e. ~P B ) -> ( M LinCo V ) = { c e. B | E. s e. ( R ^m V ) ( s finSupp ( 0g ` S ) /\ c = ( s ( linC ` M ) V ) ) } )

Proof

Step Hyp Ref Expression
1 lcoop.b 
 |-  B = ( Base ` M )
2 lcoop.s 
 |-  S = ( Scalar ` M )
3 lcoop.r 
 |-  R = ( Base ` S )
4 elex 
 |-  ( M e. X -> M e. _V )
5 4 adantr 
 |-  ( ( M e. X /\ V e. ~P B ) -> M e. _V )
6 1 pweqi 
 |-  ~P B = ~P ( Base ` M )
7 6 eleq2i 
 |-  ( V e. ~P B <-> V e. ~P ( Base ` M ) )
8 7 biimpi 
 |-  ( V e. ~P B -> V e. ~P ( Base ` M ) )
9 8 adantl 
 |-  ( ( M e. X /\ V e. ~P B ) -> V e. ~P ( Base ` M ) )
10 1 fvexi 
 |-  B e. _V
11 rabexg 
 |-  ( B e. _V -> { c e. B | E. s e. ( R ^m V ) ( s finSupp ( 0g ` S ) /\ c = ( s ( linC ` M ) V ) ) } e. _V )
12 10 11 mp1i 
 |-  ( ( M e. X /\ V e. ~P B ) -> { c e. B | E. s e. ( R ^m V ) ( s finSupp ( 0g ` S ) /\ c = ( s ( linC ` M ) V ) ) } e. _V )
13 fveq2 
 |-  ( m = M -> ( Base ` m ) = ( Base ` M ) )
14 13 1 eqtr4di 
 |-  ( m = M -> ( Base ` m ) = B )
15 14 adantr 
 |-  ( ( m = M /\ v = V ) -> ( Base ` m ) = B )
16 2fveq3 
 |-  ( m = M -> ( Base ` ( Scalar ` m ) ) = ( Base ` ( Scalar ` M ) ) )
17 16 adantr 
 |-  ( ( m = M /\ v = V ) -> ( Base ` ( Scalar ` m ) ) = ( Base ` ( Scalar ` M ) ) )
18 2 fveq2i 
 |-  ( Base ` S ) = ( Base ` ( Scalar ` M ) )
19 3 18 eqtri 
 |-  R = ( Base ` ( Scalar ` M ) )
20 17 19 eqtr4di 
 |-  ( ( m = M /\ v = V ) -> ( Base ` ( Scalar ` m ) ) = R )
21 simpr 
 |-  ( ( m = M /\ v = V ) -> v = V )
22 20 21 oveq12d 
 |-  ( ( m = M /\ v = V ) -> ( ( Base ` ( Scalar ` m ) ) ^m v ) = ( R ^m V ) )
23 2fveq3 
 |-  ( m = M -> ( 0g ` ( Scalar ` m ) ) = ( 0g ` ( Scalar ` M ) ) )
24 2 a1i 
 |-  ( m = M -> S = ( Scalar ` M ) )
25 24 eqcomd 
 |-  ( m = M -> ( Scalar ` M ) = S )
26 25 fveq2d 
 |-  ( m = M -> ( 0g ` ( Scalar ` M ) ) = ( 0g ` S ) )
27 23 26 eqtrd 
 |-  ( m = M -> ( 0g ` ( Scalar ` m ) ) = ( 0g ` S ) )
28 27 adantr 
 |-  ( ( m = M /\ v = V ) -> ( 0g ` ( Scalar ` m ) ) = ( 0g ` S ) )
29 28 breq2d 
 |-  ( ( m = M /\ v = V ) -> ( s finSupp ( 0g ` ( Scalar ` m ) ) <-> s finSupp ( 0g ` S ) ) )
30 fveq2 
 |-  ( m = M -> ( linC ` m ) = ( linC ` M ) )
31 30 adantr 
 |-  ( ( m = M /\ v = V ) -> ( linC ` m ) = ( linC ` M ) )
32 eqidd 
 |-  ( ( m = M /\ v = V ) -> s = s )
33 31 32 21 oveq123d 
 |-  ( ( m = M /\ v = V ) -> ( s ( linC ` m ) v ) = ( s ( linC ` M ) V ) )
34 33 eqeq2d 
 |-  ( ( m = M /\ v = V ) -> ( c = ( s ( linC ` m ) v ) <-> c = ( s ( linC ` M ) V ) ) )
35 29 34 anbi12d 
 |-  ( ( m = M /\ v = V ) -> ( ( s finSupp ( 0g ` ( Scalar ` m ) ) /\ c = ( s ( linC ` m ) v ) ) <-> ( s finSupp ( 0g ` S ) /\ c = ( s ( linC ` M ) V ) ) ) )
36 22 35 rexeqbidv 
 |-  ( ( m = M /\ v = V ) -> ( E. s e. ( ( Base ` ( Scalar ` m ) ) ^m v ) ( s finSupp ( 0g ` ( Scalar ` m ) ) /\ c = ( s ( linC ` m ) v ) ) <-> E. s e. ( R ^m V ) ( s finSupp ( 0g ` S ) /\ c = ( s ( linC ` M ) V ) ) ) )
37 15 36 rabeqbidv 
 |-  ( ( m = M /\ v = V ) -> { c e. ( Base ` m ) | E. s e. ( ( Base ` ( Scalar ` m ) ) ^m v ) ( s finSupp ( 0g ` ( Scalar ` m ) ) /\ c = ( s ( linC ` m ) v ) ) } = { c e. B | E. s e. ( R ^m V ) ( s finSupp ( 0g ` S ) /\ c = ( s ( linC ` M ) V ) ) } )
38 13 pweqd 
 |-  ( m = M -> ~P ( Base ` m ) = ~P ( Base ` M ) )
39 df-lco 
 |-  LinCo = ( m e. _V , v e. ~P ( Base ` m ) |-> { c e. ( Base ` m ) | E. s e. ( ( Base ` ( Scalar ` m ) ) ^m v ) ( s finSupp ( 0g ` ( Scalar ` m ) ) /\ c = ( s ( linC ` m ) v ) ) } )
40 37 38 39 ovmpox 
 |-  ( ( M e. _V /\ V e. ~P ( Base ` M ) /\ { c e. B | E. s e. ( R ^m V ) ( s finSupp ( 0g ` S ) /\ c = ( s ( linC ` M ) V ) ) } e. _V ) -> ( M LinCo V ) = { c e. B | E. s e. ( R ^m V ) ( s finSupp ( 0g ` S ) /\ c = ( s ( linC ` M ) V ) ) } )
41 5 9 12 40 syl3anc 
 |-  ( ( M e. X /\ V e. ~P B ) -> ( M LinCo V ) = { c e. B | E. s e. ( R ^m V ) ( s finSupp ( 0g ` S ) /\ c = ( s ( linC ` M ) V ) ) } )