Metamath Proof Explorer

Theorem lcoval

Description: The value of a linear combination. (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 lcoval ⊢ M ∈ X ∧ V ∈ 𝒫 B → C ∈ 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 1 2 3 lcoop ⊢ M ∈ X ∧ V ∈ 𝒫 B → M LinCo V = c ∈ B | ∃ s ∈ R V finSupp 0 S⁡ s ∧ c = s linC ⁡ M V
5 4 eleq2d ⊢ M ∈ X ∧ V ∈ 𝒫 B → C ∈ M LinCo V ↔ C ∈ c ∈ B | ∃ s ∈ R V finSupp 0 S⁡ s ∧ c = s linC ⁡ M V
6 eqeq1 ⊢ c = C → c = s linC ⁡ M V ↔ C = s linC ⁡ M V
7 6 anbi2d ⊢ c = C → finSupp 0 S⁡ s ∧ c = s linC ⁡ M V ↔ finSupp 0 S⁡ s ∧ C = s linC ⁡ M V
8 7 rexbidv ⊢ c = C → ∃ s ∈ R V finSupp 0 S⁡ s ∧ c = s linC ⁡ M V ↔ ∃ s ∈ R V finSupp 0 S⁡ s ∧ C = s linC ⁡ M V
9 8 elrab ⊢ C ∈ c ∈ B | ∃ s ∈ R V finSupp 0 S⁡ s ∧ c = s linC ⁡ M V ↔ C ∈ B ∧ ∃ s ∈ R V finSupp 0 S⁡ s ∧ C = s linC ⁡ M V
10 5 9 bitrdi ⊢ M ∈ X ∧ V ∈ 𝒫 B → C ∈ M LinCo V ↔ C ∈ B ∧ ∃ s ∈ R V finSupp 0 S⁡ s ∧ C = s linC ⁡ M V