This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem lbslsp

Description: Any element of a left module M can be expressed as a linear combination of the elements of a basis V of M . (Contributed by Thierry Arnoux, 3-Aug-2023)

Ref Expression
Hypotheses lbslsp.v ⊢ B = Base M
lbslsp.k ⊢ K = Base S
lbslsp.s ⊢ S = Scalar ⁡ M
lbslsp.z ⊢ 0 ˙ = 0 S
lbslsp.t ⊢ · ˙ = ⋅ M
lbslsp.m ⊢ φ → M ∈ LMod
lbslsp.1 ⊢ φ → V ∈ LBasis ⁡ M
Assertion lbslsp ⊢ φ → X ∈ B ↔ ∃ a ∈ K V finSupp 0 ˙⁡ a ∧ X = ∑ M v ∈ V a ⁡ v · ˙ v

Proof

Step Hyp Ref Expression
1 lbslsp.v ⊢ B = Base M
2 lbslsp.k ⊢ K = Base S
3 lbslsp.s ⊢ S = Scalar ⁡ M
4 lbslsp.z ⊢ 0 ˙ = 0 S
5 lbslsp.t ⊢ · ˙ = ⋅ M
6 lbslsp.m ⊢ φ → M ∈ LMod
7 lbslsp.1 ⊢ φ → V ∈ LBasis ⁡ M
8 eqid ⊢ LBasis ⁡ M = LBasis ⁡ M
9 eqid ⊢ LSpan ⁡ M = LSpan ⁡ M
10 1 8 9 lbssp ⊢ V ∈ LBasis ⁡ M → LSpan ⁡ M ⁡ V = B
11 7 10 syl ⊢ φ → LSpan ⁡ M ⁡ V = B
12 11 eleq2d ⊢ φ → X ∈ LSpan ⁡ M ⁡ V ↔ X ∈ B
13 1 8 lbsss ⊢ V ∈ LBasis ⁡ M → V ⊆ B
14 7 13 syl ⊢ φ → V ⊆ B
15 9 1 2 3 4 5 6 14 ellspds ⊢ φ → X ∈ LSpan ⁡ M ⁡ V ↔ ∃ a ∈ K V finSupp 0 ˙⁡ a ∧ X = ∑ M v ∈ V a ⁡ v · ˙ v
16 12 15 bitr3d ⊢ φ → X ∈ B ↔ ∃ a ∈ K V finSupp 0 ˙⁡ a ∧ X = ∑ M v ∈ V a ⁡ v · ˙ v