Theorem linindsi

Description: The implications of being a linearly independent subset. (Contributed by AV, 13-Apr-2019) (Revised by AV, 30-Jul-2019)

	Ref	Expression
Hypotheses	islininds.b	$$⊢B={\mathrm{Base}}_M$$
	islininds.z	$$⊢Z=0_M$$
	islininds.r	$$⊢R=\mathrm{Scalar}\left(M\right)$$
	islininds.e	$$⊢E={\mathrm{Base}}_R$$
	islininds.0	$$⊢\underset{\dot{}}{0}=0_R$$
Assertion	linindsi	$$⊢S\mathrm{linIndS}M\to \left(S\in 𝒫B\wedge \forall f\in \left(E^S\right)\left(\left({finSupp}_{\underset{\dot{}}{0}}\left(f\right)\wedge f\mathrm{linC}\left(M\right)S=Z\right)\to \forall x\in Sf\left(x\right)=\underset{\dot{}}{0}\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		islininds.b	$$⊢B={\mathrm{Base}}_M$$
2		islininds.z	$$⊢Z=0_M$$
3		islininds.r	$$⊢R=\mathrm{Scalar}\left(M\right)$$
4		islininds.e	$$⊢E={\mathrm{Base}}_R$$
5		islininds.0	$$⊢\underset{\dot{}}{0}=0_R$$
6		linindsv	$$⊢S\mathrm{linIndS}M\to \left(S\in \mathrm{V}\wedge M\in \mathrm{V}\right)$$
7	1 2 3 4 5	islininds	$$⊢\left(S\in \mathrm{V}\wedge M\in \mathrm{V}\right)\to \left(S\mathrm{linIndS}M\leftrightarrow \left(S\in 𝒫B\wedge \forall f\in \left(E^S\right)\left(\left({finSupp}_{\underset{\dot{}}{0}}\left(f\right)\wedge f\mathrm{linC}\left(M\right)S=Z\right)\to \forall x\in Sf\left(x\right)=\underset{\dot{}}{0}\right)\right)\right)$$
8	6 7	syl	$$⊢S\mathrm{linIndS}M\to \left(S\mathrm{linIndS}M\leftrightarrow \left(S\in 𝒫B\wedge \forall f\in \left(E^S\right)\left(\left({finSupp}_{\underset{\dot{}}{0}}\left(f\right)\wedge f\mathrm{linC}\left(M\right)S=Z\right)\to \forall x\in Sf\left(x\right)=\underset{\dot{}}{0}\right)\right)\right)$$
9	8	ibi	$$⊢S\mathrm{linIndS}M\to \left(S\in 𝒫B\wedge \forall f\in \left(E^S\right)\left(\left({finSupp}_{\underset{\dot{}}{0}}\left(f\right)\wedge f\mathrm{linC}\left(M\right)S=Z\right)\to \forall x\in Sf\left(x\right)=\underset{\dot{}}{0}\right)\right)$$