Metamath Proof Explorer

Theorem lindslininds

Description: Equivalence of definitions df-linds and df-lininds for (linear) independence for (left) modules. (Contributed by AV, 26-Apr-2019) (Proof shortened by AV, 30-Jul-2019)

		Ref	Expression
	Assertion	lindslininds	$⊢ (S \in V \land M \in LMod) \to (S linIndS M \leftrightarrow S \in LIndS (M))$

Proof

Step	Hyp	Ref	Expression
1		eqid	$⊢ Scalar (M) = Scalar (M)$
2		eqid	$⊢ {Base}_{Scalar (M)} = {Base}_{Scalar (M)}$
3		eqid	$⊢ 0_{Scalar (M)} = 0_{Scalar (M)}$
4		eqid	$⊢ 0_{M} = 0_{M}$
5	1 2 3 4	lindslinindsimp1	$⊢ (S \in V \land M \in LMod) \to ((S \in 𝒫 {Base}_{M} \land \forall f \in ({Base}_{Scalar (M)}^{S}) (({finSupp}_{0_{Scalar (M)}} (f) \land f linC (M) S = 0_{M}) \to \forall x \in S f (x) = 0_{Scalar (M)})) \to (S \subseteq {Base}_{M} \land \forall s \in S \forall g \in ({Base}_{Scalar (M)} ∖ \{0_{Scalar (M)}\}) \neg g \cdot_{M} s \in LSpan (M) (S ∖ \{s\})))$
6	1 2 3 4	lindslinindsimp2	$⊢ (S \in V \land M \in LMod) \to ((S \subseteq {Base}_{M} \land \forall s \in S \forall g \in ({Base}_{Scalar (M)} ∖ \{0_{Scalar (M)}\}) \neg g \cdot_{M} s \in LSpan (M) (S ∖ \{s\})) \to (S \in 𝒫 {Base}_{M} \land \forall f \in ({Base}_{Scalar (M)}^{S}) (({finSupp}_{0_{Scalar (M)}} (f) \land f linC (M) S = 0_{M}) \to \forall x \in S f (x) = 0_{Scalar (M)})))$
7	5 6	impbid	$⊢ (S \in V \land M \in LMod) \to ((S \in 𝒫 {Base}_{M} \land \forall f \in ({Base}_{Scalar (M)}^{S}) (({finSupp}_{0_{Scalar (M)}} (f) \land f linC (M) S = 0_{M}) \to \forall x \in S f (x) = 0_{Scalar (M)})) \leftrightarrow (S \subseteq {Base}_{M} \land \forall s \in S \forall g \in ({Base}_{Scalar (M)} ∖ \{0_{Scalar (M)}\}) \neg g \cdot_{M} s \in LSpan (M) (S ∖ \{s\})))$
8		eqid	$⊢ {Base}_{M} = {Base}_{M}$
9	8 4 1 2 3	islininds	$⊢ (S \in V \land M \in LMod) \to (S linIndS M \leftrightarrow (S \in 𝒫 {Base}_{M} \land \forall f \in ({Base}_{Scalar (M)}^{S}) (({finSupp}_{0_{Scalar (M)}} (f) \land f linC (M) S = 0_{M}) \to \forall x \in S f (x) = 0_{Scalar (M)})))$
10		eqid	$⊢ \cdot_{M} = \cdot_{M}$
11		eqid	$⊢ LSpan (M) = LSpan (M)$
12	8 10 11 1 2 3	islinds2	$⊢ M \in LMod \to (S \in LIndS (M) \leftrightarrow (S \subseteq {Base}_{M} \land \forall s \in S \forall g \in ({Base}_{Scalar (M)} ∖ \{0_{Scalar (M)}\}) \neg g \cdot_{M} s \in LSpan (M) (S ∖ \{s\})))$
13	12	adantl	$⊢ (S \in V \land M \in LMod) \to (S \in LIndS (M) \leftrightarrow (S \subseteq {Base}_{M} \land \forall s \in S \forall g \in ({Base}_{Scalar (M)} ∖ \{0_{Scalar (M)}\}) \neg g \cdot_{M} s \in LSpan (M) (S ∖ \{s\})))$
14	7 9 13	3bitr4d	$⊢ (S \in V \land M \in LMod) \to (S linIndS M \leftrightarrow S \in LIndS (M))$