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	$⊢ \underset{˙}{0} = 0_{S}$
		lbslsp.t	$⊢ \underset{˙}{\cdot} = \cdot_{M}$
		lbslsp.m	$⊢ φ \to M \in LMod$
		lbslsp.1	$⊢ φ \to V \in LBasis (M)$
	Assertion	lbslsp	$⊢ φ \to (X \in B \leftrightarrow \exists a \in (K^{V}) ({finSupp}_{\underset{˙}{0}} (a) \land X = \underset{v \in V}{\sum_{M}} (a (v) \underset{˙}{\cdot} 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	$⊢ \underset{˙}{0} = 0_{S}$
5		lbslsp.t	$⊢ \underset{˙}{\cdot} = \cdot_{M}$
6		lbslsp.m	$⊢ φ \to M \in LMod$
7		lbslsp.1	$⊢ φ \to V \in LBasis (M)$
8		eqid	$⊢ LBasis (M) = LBasis (M)$
9		eqid	$⊢ LSpan (M) = LSpan (M)$
10	1 8 9	lbssp	$⊢ V \in LBasis (M) \to LSpan (M) (V) = B$
11	7 10	syl	$⊢ φ \to LSpan (M) (V) = B$
12	11	eleq2d	$⊢ φ \to (X \in LSpan (M) (V) \leftrightarrow X \in B)$
13	1 8	lbsss	$⊢ V \in LBasis (M) \to V \subseteq B$
14	7 13	syl	$⊢ φ \to V \subseteq B$
15	9 1 2 3 4 5 6 14	ellspds	$⊢ φ \to (X \in LSpan (M) (V) \leftrightarrow \exists a \in (K^{V}) ({finSupp}_{\underset{˙}{0}} (a) \land X = \underset{v \in V}{\sum_{M}} (a (v) \underset{˙}{\cdot} v)))$
16	12 15	bitr3d	$⊢ φ \to (X \in B \leftrightarrow \exists a \in (K^{V}) ({finSupp}_{\underset{˙}{0}} (a) \land X = \underset{v \in V}{\sum_{M}} (a (v) \underset{˙}{\cdot} v)))$