Theorem linindscl

Description: A linearly independent set is a subset of (the base set of) a module. (Contributed by AV, 13-Apr-2019)

	Ref	Expression
Assertion	linindscl	$$⊢S\mathrm{linIndS}M\to S\in 𝒫{\mathrm{Base}}_M$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢{\mathrm{Base}}_M={\mathrm{Base}}_M$$
2		eqid	$$⊢0_M=0_M$$
3		eqid	$$⊢\mathrm{Scalar}\left(M\right)=\mathrm{Scalar}\left(M\right)$$
4		eqid	$$⊢{\mathrm{Base}}_{\mathrm{Scalar}\left(M\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left(M\right)}$$
5		eqid	$$⊢0_{\mathrm{Scalar}\left(M\right)}=0_{\mathrm{Scalar}\left(M\right)}$$
6	1 2 3 4 5	linindsi	$$⊢S\mathrm{linIndS}M\to \left(S\in 𝒫{\mathrm{Base}}_M\wedge \forall f\in \left({{\mathrm{Base}}_{\mathrm{Scalar}\left(M\right)}}^S\right)\left(\left({finSupp}_{0_{\mathrm{Scalar}\left(M\right)}}\left(f\right)\wedge f\mathrm{linC}\left(M\right)S=0_M\right)\to \forall x\in Sf\left(x\right)=0_{\mathrm{Scalar}\left(M\right)}\right)\right)$$
7	6	simpld	$$⊢S\mathrm{linIndS}M\to S\in 𝒫{\mathrm{Base}}_M$$