islinindfis

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	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})))$

Proof

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	islininds	$⊢ (S \in Fin \land M \in W) \to (S linIndS M \leftrightarrow (S \in 𝒫 B \land \forall f \in (E^{S}) (({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z) \to \forall x \in S f (x) = \underset{˙}{0})))$
7		pm4.79	$⊢ (({finSupp}_{\underset{˙}{0}} (f) \to \forall x \in S f (x) = \underset{˙}{0}) \lor (f linC (M) S = Z \to \forall x \in S f (x) = \underset{˙}{0})) \leftrightarrow (({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z) \to \forall x \in S f (x) = \underset{˙}{0})$
8		elmapi	$⊢ f \in (E^{S}) \to f : S ⟶ E$
9	8	adantl	$⊢ ((S \in Fin \land M \in W) \land f \in (E^{S})) \to f : S ⟶ E$
10		simpll	$⊢ ((S \in Fin \land M \in W) \land f \in (E^{S})) \to S \in Fin$
11	5	fvexi	$⊢ \underset{˙}{0} \in V$
12	11	a1i	$⊢ ((S \in Fin \land M \in W) \land f \in (E^{S})) \to \underset{˙}{0} \in V$
13	9 10 12	fdmfifsupp	$⊢ ((S \in Fin \land M \in W) \land f \in (E^{S})) \to {finSupp}_{\underset{˙}{0}} (f)$
14	13	adantr	$⊢ (((S \in Fin \land M \in W) \land f \in (E^{S})) \land f linC (M) S = Z) \to {finSupp}_{\underset{˙}{0}} (f)$
15	14	imim1i	$⊢ ({finSupp}_{\underset{˙}{0}} (f) \to \forall x \in S f (x) = \underset{˙}{0}) \to ((((S \in Fin \land M \in W) \land f \in (E^{S})) \land f linC (M) S = Z) \to \forall x \in S f (x) = \underset{˙}{0})$
16	15	expd	$⊢ ({finSupp}_{\underset{˙}{0}} (f) \to \forall x \in S f (x) = \underset{˙}{0}) \to (((S \in Fin \land M \in W) \land f \in (E^{S})) \to (f linC (M) S = Z \to \forall x \in S f (x) = \underset{˙}{0}))$
17		ax-1	$⊢ (f linC (M) S = Z \to \forall x \in S f (x) = \underset{˙}{0}) \to (((S \in Fin \land M \in W) \land f \in (E^{S})) \to (f linC (M) S = Z \to \forall x \in S f (x) = \underset{˙}{0}))$
18	16 17	jaoi	$⊢ (({finSupp}_{\underset{˙}{0}} (f) \to \forall x \in S f (x) = \underset{˙}{0}) \lor (f linC (M) S = Z \to \forall x \in S f (x) = \underset{˙}{0})) \to (((S \in Fin \land M \in W) \land f \in (E^{S})) \to (f linC (M) S = Z \to \forall x \in S f (x) = \underset{˙}{0}))$
19	7 18	sylbir	$⊢ (({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z) \to \forall x \in S f (x) = \underset{˙}{0}) \to (((S \in Fin \land M \in W) \land f \in (E^{S})) \to (f linC (M) S = Z \to \forall x \in S f (x) = \underset{˙}{0}))$
20	19	com12	$⊢ ((S \in Fin \land M \in W) \land f \in (E^{S})) \to ((({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z) \to \forall x \in S f (x) = \underset{˙}{0}) \to (f linC (M) S = Z \to \forall x \in S f (x) = \underset{˙}{0}))$
21		pm3.42	$⊢ (f linC (M) S = Z \to \forall x \in S f (x) = \underset{˙}{0}) \to (({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z) \to \forall x \in S f (x) = \underset{˙}{0})$
22	20 21	impbid1	$⊢ ((S \in Fin \land M \in W) \land f \in (E^{S})) \to ((({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z) \to \forall x \in S f (x) = \underset{˙}{0}) \leftrightarrow (f linC (M) S = Z \to \forall x \in S f (x) = \underset{˙}{0}))$
23	22	ralbidva	$⊢ (S \in Fin \land M \in W) \to (\forall f \in (E^{S}) (({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z) \to \forall x \in S f (x) = \underset{˙}{0}) \leftrightarrow \forall f \in (E^{S}) (f linC (M) S = Z \to \forall x \in S f (x) = \underset{˙}{0}))$
24	23	anbi2d	$⊢ (S \in Fin \land M \in W) \to ((S \in 𝒫 B \land \forall f \in (E^{S}) (({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) S = Z) \to \forall x \in S f (x) = \underset{˙}{0})) \leftrightarrow (S \in 𝒫 B \land \forall f \in (E^{S}) (f linC (M) S = Z \to \forall x \in S f (x) = \underset{˙}{0})))$
25	6 24	bitrd	$⊢ (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})))$

Metamath Proof Explorer

Theorem islinindfis

Proof