islinindfiss

Description: The property of being a linearly independent finite subset. (Contributed by AV, 27-Apr-2019)

	Ref	Expression
Hypotheses	islininds.b	$⊢ B = {Base}_{M}$
	islininds.z	$⊢ Z = 0_{M}$
	islininds.r	$⊢ R = Scalar (M)$
	islininds.e	$⊢ E = {Base}_{R}$
	islininds.0	$⊢ \underset{˙}{0} = 0_{R}$
Assertion	islinindfiss	$⊢ (M \in W \land S \in Fin \land S \in 𝒫 B) \to (S linIndS M \leftrightarrow \forall f \in (E^{S}) (f linC (M) S = Z \to \forall x \in S f (x) = \underset{˙}{0}))$

Step	Hyp	Ref	Expression
1		islininds.b	$⊢ B = {Base}_{M}$
2		islininds.z	$⊢ Z = 0_{M}$
3		islininds.r	$⊢ R = Scalar (M)$
4		islininds.e	$⊢ E = {Base}_{R}$
5		islininds.0	$⊢ \underset{˙}{0} = 0_{R}$
6	1 2 3 4 5	islinindfis	$⊢ (S \in Fin \land M \in W) \to (S linIndS M \leftrightarrow (S \in 𝒫 B \land \forall f \in (E^{S}) (f linC (M) S = Z \to \forall x \in S f (x) = \underset{˙}{0})))$
7	6	ancoms	$⊢ (M \in W \land S \in Fin) \to (S linIndS M \leftrightarrow (S \in 𝒫 B \land \forall f \in (E^{S}) (f linC (M) S = Z \to \forall x \in S f (x) = \underset{˙}{0})))$
8	7	3adant3	$⊢ (M \in W \land S \in Fin \land S \in 𝒫 B) \to (S linIndS M \leftrightarrow (S \in 𝒫 B \land \forall f \in (E^{S}) (f linC (M) S = Z \to \forall x \in S f (x) = \underset{˙}{0})))$
9	8	3anibar	$⊢ (M \in W \land S \in Fin \land S \in 𝒫 B) \to (S linIndS M \leftrightarrow \forall f \in (E^{S}) (f linC (M) S = Z \to \forall x \in S f (x) = \underset{˙}{0}))$

Metamath Proof Explorer