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 biimpi ⊢ V ∈ 𝒫 B → V ∈ 𝒫 Base M
9 8 adantl ⊢ M ∈ X ∧ V ∈ 𝒫 B → V ∈ 𝒫 Base M
10 1 fvexi ⊢ B ∈ V
11 rabexg ⊢ B ∈ V → c ∈ B | ∃ s ∈ R V finSupp 0 S⁡ s ∧ c = s linC ⁡ M V ∈ V
12 10 11 mp1i ⊢ M ∈ X ∧ V ∈ 𝒫 B → c ∈ B | ∃ s ∈ R V finSupp 0 S⁡ s ∧ c = s linC ⁡ M V ∈ 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 v = R V
23 2fveq3 ⊢ m = M → 0 Scalar ⁡ m = 0 Scalar ⁡ M
24 2 a1i ⊢ m = M → S = Scalar ⁡ M
25 24 eqcomd ⊢ m = M → Scalar ⁡ M = S
26 25 fveq2d ⊢ m = M → 0 Scalar ⁡ M = 0 S
27 23 26 eqtrd ⊢ m = M → 0 Scalar ⁡ m = 0 S
28 27 adantr ⊢ m = M ∧ v = V → 0 Scalar ⁡ m = 0 S
29 28 breq2d ⊢ m = M ∧ v = V → finSupp 0 Scalar ⁡ m ⁡ s ↔ finSupp 0 S⁡ 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 → finSupp 0 Scalar ⁡ m ⁡ s ∧ c = s linC ⁡ m v ↔ finSupp 0 S⁡ s ∧ c = s linC ⁡ M V
36 22 35 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
37 15 36 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
38 13 pweqd ⊢ m = M → 𝒫 Base m = 𝒫 Base M
39 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
40 37 38 39 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
41 5 9 12 40 syl3anc ⊢ M ∈ X ∧ V ∈ 𝒫 B → M LinCo V = c ∈ B | ∃ s ∈ R V finSupp 0 S⁡ s ∧ c = s linC ⁡ M V