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 ∈ X ∧ V ∈ 𝒫 B → M LinCo V = c ∈ B | ∃ s ∈ R V finSupp 0 S⁡ 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 ∈ X → M ∈ V
5 4 adantr ⊢ M ∈ X ∧ V ∈ 𝒫 B → M ∈ V
6 1 pweqi ⊢ 𝒫 B = 𝒫 Base M
7 6 eleq2i ⊢ V ∈ 𝒫 B ↔ V ∈ 𝒫 Base M
8 7 bilani ⊢ M ∈ X ∧ V ∈ 𝒫 B → V ∈ 𝒫 Base M
9 1 fvexi ⊢ B ∈ V
10 rabexg ⊢ B ∈ V → c ∈ B | ∃ s ∈ R V finSupp 0 S⁡ s ∧ c = s linC ⁡ M V ∈ V
11 9 10 mp1i ⊢ M ∈ X ∧ V ∈ 𝒫 B → c ∈ B | ∃ s ∈ R V finSupp 0 S⁡ s ∧ c = s linC ⁡ M V ∈ V
12 fveq2 ⊢ m = M → Base m = Base M
13 12 1 eqtr4di ⊢ m = M → Base m = B
14 13 adantr ⊢ m = M ∧ v = V → Base m = B
15 2fveq3 ⊢ m = M → Base Scalar ⁡ m = Base Scalar ⁡ M
16 15 adantr ⊢ m = M ∧ v = V → Base Scalar ⁡ m = Base Scalar ⁡ M
17 2 fveq2i ⊢ Base S = Base Scalar ⁡ M
18 3 17 eqtri ⊢ R = Base Scalar ⁡ M
19 16 18 eqtr4di ⊢ m = M ∧ v = V → Base Scalar ⁡ m = R
20 simpr ⊢ m = M ∧ v = V → v = V
21 19 20 oveq12d ⊢ m = M ∧ v = V → Base Scalar ⁡ m v = R V
22 2fveq3 ⊢ m = M → 0 Scalar ⁡ m = 0 Scalar ⁡ M
23 2 a1i ⊢ m = M → S = Scalar ⁡ M
24 23 eqcomd ⊢ m = M → Scalar ⁡ M = S
25 24 fveq2d ⊢ m = M → 0 Scalar ⁡ M = 0 S
26 22 25 eqtrd ⊢ m = M → 0 Scalar ⁡ m = 0 S
27 26 adantr ⊢ m = M ∧ v = V → 0 Scalar ⁡ m = 0 S
28 27 breq2d ⊢ m = M ∧ v = V → finSupp 0 Scalar ⁡ m ⁡ s ↔ finSupp 0 S⁡ s
29 fveq2 ⊢ m = M → linC ⁡ m = linC ⁡ M
30 29 adantr ⊢ m = M ∧ v = V → linC ⁡ m = linC ⁡ M
31 eqidd ⊢ m = M ∧ v = V → s = s
32 30 31 20 oveq123d ⊢ m = M ∧ v = V → s linC ⁡ m v = s linC ⁡ M V
33 32 eqeq2d ⊢ m = M ∧ v = V → c = s linC ⁡ m v ↔ c = s linC ⁡ M V
34 28 33 anbi12d ⊢ m = M ∧ v = V → finSupp 0 Scalar ⁡ m ⁡ s ∧ c = s linC ⁡ m v ↔ finSupp 0 S⁡ s ∧ c = s linC ⁡ M V
35 21 34 rexeqbidv ⊢ m = M ∧ v = V → ∃ s ∈ Base Scalar ⁡ m v finSupp 0 Scalar ⁡ m ⁡ s ∧ c = s linC ⁡ m v ↔ ∃ s ∈ R V finSupp 0 S⁡ s ∧ c = s linC ⁡ M V
36 14 35 rabeqbidv ⊢ m = M ∧ v = V → c ∈ Base m | ∃ s ∈ Base Scalar ⁡ m v finSupp 0 Scalar ⁡ m ⁡ s ∧ c = s linC ⁡ m v = c ∈ B | ∃ s ∈ R V finSupp 0 S⁡ s ∧ c = s linC ⁡ M V
37 12 pweqd ⊢ m = M → 𝒫 Base m = 𝒫 Base M
38 df-lco ⊢ LinCo = m ∈ V , v ∈ 𝒫 Base m ⟼ c ∈ Base m | ∃ s ∈ Base Scalar ⁡ m v finSupp 0 Scalar ⁡ m ⁡ s ∧ c = s linC ⁡ m v
39 36 37 38 ovmpox ⊢ M ∈ V ∧ V ∈ 𝒫 Base M ∧ c ∈ B | ∃ s ∈ R V finSupp 0 S⁡ s ∧ c = s linC ⁡ M V ∈ V → M LinCo V = c ∈ B | ∃ s ∈ R V finSupp 0 S⁡ s ∧ c = s linC ⁡ M V
40 5 8 11 39 syl3anc ⊢ M ∈ X ∧ V ∈ 𝒫 B → M LinCo V = c ∈ B | ∃ s ∈ R V finSupp 0 S⁡ s ∧ c = s linC ⁡ M V