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 ( 𝑣 ∈ 𝑉 ↦ ( ( 𝑎 ‘ 𝑣 ) · 𝑣 ) ) ) ) ) )