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 ⊢ 𝐵 = ( Base ‘ 𝑀 )
lbslsp.k ⊢ 𝐾 = ( Base ‘ 𝑆 )
lbslsp.s ⊢ 𝑆 = ( Scalar ‘ 𝑀 )
lbslsp.z ⊢ 0 = ( 0g ‘ 𝑆 )
lbslsp.t ⊢ · = ( ·𝑠 ‘ 𝑀 )
lbslsp.m ⊢ ( 𝜑 → 𝑀 ∈ LMod )
lbslsp.1 ⊢ ( 𝜑 → 𝑉 ∈ ( LBasis ‘ 𝑀 ) )
Assertion lbslsp ( 𝜑 → ( 𝑋 ∈ 𝐵 ↔ ∃ 𝑎 ∈ ( 𝐾 ↑m 𝑉 ) ( 𝑎 finSupp 0 ∧ 𝑋 = ( 𝑀 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) · 𝑣 ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 lbslsp.v ⊢ 𝐵 = ( Base ‘ 𝑀 )
2 lbslsp.k ⊢ 𝐾 = ( Base ‘ 𝑆 )
3 lbslsp.s ⊢ 𝑆 = ( Scalar ‘ 𝑀 )
4 lbslsp.z ⊢ 0 = ( 0g ‘ 𝑆 )
5 lbslsp.t ⊢ · = ( ·𝑠 ‘ 𝑀 )
6 lbslsp.m ⊢ ( 𝜑 → 𝑀 ∈ LMod )
7 lbslsp.1 ⊢ ( 𝜑 → 𝑉 ∈ ( LBasis ‘ 𝑀 ) )
8 eqid ⊢ ( LBasis ‘ 𝑀 ) = ( LBasis ‘ 𝑀 )
9 eqid ⊢ ( LSpan ‘ 𝑀 ) = ( LSpan ‘ 𝑀 )
10 1 8 9 lbssp ⊢ ( 𝑉 ∈ ( LBasis ‘ 𝑀 ) → ( ( LSpan ‘ 𝑀 ) ‘ 𝑉 ) = 𝐵 )
11 7 10 syl ⊢ ( 𝜑 → ( ( LSpan ‘ 𝑀 ) ‘ 𝑉 ) = 𝐵 )
12 11 eleq2d ⊢ ( 𝜑 → ( 𝑋 ∈ ( ( LSpan ‘ 𝑀 ) ‘ 𝑉 ) ↔ 𝑋 ∈ 𝐵 ) )
13 1 8 lbsss ⊢ ( 𝑉 ∈ ( LBasis ‘ 𝑀 ) → 𝑉 ⊆ 𝐵 )
14 7 13 syl ⊢ ( 𝜑 → 𝑉 ⊆ 𝐵 )
15 9 1 2 3 4 5 6 14 ellspds ⊢ ( 𝜑 → ( 𝑋 ∈ ( ( LSpan ‘ 𝑀 ) ‘ 𝑉 ) ↔ ∃ 𝑎 ∈ ( 𝐾 ↑m 𝑉 ) ( 𝑎 finSupp 0 ∧ 𝑋 = ( 𝑀 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) · 𝑣 ) ) ) ) ) )
16 12 15 bitr3d ⊢ ( 𝜑 → ( 𝑋 ∈ 𝐵 ↔ ∃ 𝑎 ∈ ( 𝐾 ↑m 𝑉 ) ( 𝑎 finSupp 0 ∧ 𝑋 = ( 𝑀 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) · 𝑣 ) ) ) ) ) )