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=BaseM
lcoop.s ⊢S=Scalar⁡M
lcoop.r ⊢R=BaseS
Assertion lcoop ⊢M∈X∧V∈𝒫B→MLinCoV=c∈B|∃s∈RVfinSupp0S⁡s∧c=slinC⁡MV

Proof

Step Hyp Ref Expression
1 lcoop.b ⊢B=BaseM
2 lcoop.s ⊢S=Scalar⁡M
3 lcoop.r ⊢R=BaseS
4 elex ⊢M∈X→M∈V
5 4 adantr ⊢M∈X∧V∈𝒫B→M∈V
6 1 pweqi ⊢𝒫B=𝒫BaseM
7 6 eleq2i ⊢V∈𝒫B↔V∈𝒫BaseM
8 7 biimpi ⊢V∈𝒫B→V∈𝒫BaseM
9 8 adantl ⊢M∈X∧V∈𝒫B→V∈𝒫BaseM
10 1 fvexi ⊢B∈V
11 rabexg ⊢B∈V→c∈B|∃s∈RVfinSupp0S⁡s∧c=slinC⁡MV∈V
12 10 11 mp1i ⊢M∈X∧V∈𝒫B→c∈B|∃s∈RVfinSupp0S⁡s∧c=slinC⁡MV∈V
13 fveq2 ⊢m=M→Basem=BaseM
14 13 1 eqtr4di ⊢m=M→Basem=B
15 14 adantr ⊢m=M∧v=V→Basem=B
16 2fveq3 ⊢m=M→BaseScalar⁡m=BaseScalar⁡M
17 16 adantr ⊢m=M∧v=V→BaseScalar⁡m=BaseScalar⁡M
18 2 fveq2i ⊢BaseS=BaseScalar⁡M
19 3 18 eqtri ⊢R=BaseScalar⁡M
20 17 19 eqtr4di ⊢m=M∧v=V→BaseScalar⁡m=R
21 simpr ⊢m=M∧v=V→v=V
22 20 21 oveq12d ⊢m=M∧v=V→BaseScalar⁡mv=RV
23 2fveq3 ⊢m=M→0Scalar⁡m=0Scalar⁡M
24 2 a1i ⊢m=M→S=Scalar⁡M
25 24 eqcomd ⊢m=M→Scalar⁡M=S
26 25 fveq2d ⊢m=M→0Scalar⁡M=0S
27 23 26 eqtrd ⊢m=M→0Scalar⁡m=0S
28 27 adantr ⊢m=M∧v=V→0Scalar⁡m=0S
29 28 breq2d ⊢m=M∧v=V→finSupp0Scalar⁡m⁡s↔finSupp0S⁡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→slinC⁡mv=slinC⁡MV
34 33 eqeq2d ⊢m=M∧v=V→c=slinC⁡mv↔c=slinC⁡MV
35 29 34 anbi12d ⊢m=M∧v=V→finSupp0Scalar⁡m⁡s∧c=slinC⁡mv↔finSupp0S⁡s∧c=slinC⁡MV
36 22 35 rexeqbidv ⊢m=M∧v=V→∃s∈BaseScalar⁡mvfinSupp0Scalar⁡m⁡s∧c=slinC⁡mv↔∃s∈RVfinSupp0S⁡s∧c=slinC⁡MV
37 15 36 rabeqbidv ⊢m=M∧v=V→c∈Basem|∃s∈BaseScalar⁡mvfinSupp0Scalar⁡m⁡s∧c=slinC⁡mv=c∈B|∃s∈RVfinSupp0S⁡s∧c=slinC⁡MV
38 13 pweqd ⊢m=M→𝒫Basem=𝒫BaseM
39 df-lco ⊢LinCo=m∈V,v∈𝒫Basem⟼c∈Basem|∃s∈BaseScalar⁡mvfinSupp0Scalar⁡m⁡s∧c=slinC⁡mv
40 37 38 39 ovmpox ⊢M∈V∧V∈𝒫BaseM∧c∈B|∃s∈RVfinSupp0S⁡s∧c=slinC⁡MV∈V→MLinCoV=c∈B|∃s∈RVfinSupp0S⁡s∧c=slinC⁡MV
41 5 9 12 40 syl3anc ⊢M∈X∧V∈𝒫B→MLinCoV=c∈B|∃s∈RVfinSupp0S⁡s∧c=slinC⁡MV