islinds5

Description: A set is linearly independent if and only if it has no non-trivial representations of zero. (Contributed by Thierry Arnoux, 18-May-2023)

	Ref	Expression
Hypotheses	islinds5.b	$⊢ B = {Base}_{W}$
	islinds5.k	$⊢ K = {Base}_{F}$
	islinds5.r	$⊢ F = Scalar (W)$
	islinds5.t	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
	islinds5.z	$⊢ O = 0_{W}$
	islinds5.y	$⊢ \underset{˙}{0} = 0_{F}$
Assertion	islinds5	$⊢ (W \in LMod \land V \subseteq B) \to (V \in LIndS (W) \leftrightarrow \forall a \in (K^{V}) (({finSupp}_{\underset{˙}{0}} (a) \land \underset{v \in V}{\sum_{W}} (a (v) \underset{˙}{\cdot} v) = O) \to a = V \times \{\underset{˙}{0}\}))$

Proof

Step	Hyp	Ref	Expression
1		islinds5.b	$⊢ B = {Base}_{W}$
2		islinds5.k	$⊢ K = {Base}_{F}$
3		islinds5.r	$⊢ F = Scalar (W)$
4		islinds5.t	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
5		islinds5.z	$⊢ O = 0_{W}$
6		islinds5.y	$⊢ \underset{˙}{0} = 0_{F}$
7	1	islinds	$⊢ W \in LMod \to (V \in LIndS (W) \leftrightarrow (V \subseteq B \land ({I ↾}_{V}) LIndF W))$
8	7	baibd	$⊢ (W \in LMod \land V \subseteq B) \to (V \in LIndS (W) \leftrightarrow ({I ↾}_{V}) LIndF W)$
9		simpl	$⊢ (W \in LMod \land V \subseteq B) \to W \in LMod$
10	1	fvexi	$⊢ B \in V$
11	10	a1i	$⊢ (W \in LMod \land V \subseteq B) \to B \in V$
12		simpr	$⊢ (W \in LMod \land V \subseteq B) \to V \subseteq B$
13	11 12	ssexd	$⊢ (W \in LMod \land V \subseteq B) \to V \in V$
14		f1oi	$⊢ ({I ↾}_{V}) : V \underset{1-1 onto}{⟶} V$
15		f1of	$⊢ ({I ↾}_{V}) : V \underset{1-1 onto}{⟶} V \to ({I ↾}_{V}) : V ⟶ V$
16	14 15	mp1i	$⊢ (W \in LMod \land V \subseteq B) \to ({I ↾}_{V}) : V ⟶ V$
17	16 12	fssd	$⊢ (W \in LMod \land V \subseteq B) \to ({I ↾}_{V}) : V ⟶ B$
18		eqid	$⊢ {Base}_{(F freeLMod V)} = {Base}_{(F freeLMod V)}$
19	1 3 4 5 6 18	islindf4	$⊢ (W \in LMod \land V \in V \land ({I ↾}_{V}) : V ⟶ B) \to (({I ↾}_{V}) LIndF W \leftrightarrow \forall a \in {Base}_{(F freeLMod V)} (\sum_{W} (a {\underset{˙}{\cdot}}_{f} ({I ↾}_{V})) = O \to a = V \times \{\underset{˙}{0}\}))$
20	9 13 17 19	syl3anc	$⊢ (W \in LMod \land V \subseteq B) \to (({I ↾}_{V}) LIndF W \leftrightarrow \forall a \in {Base}_{(F freeLMod V)} (\sum_{W} (a {\underset{˙}{\cdot}}_{f} ({I ↾}_{V})) = O \to a = V \times \{\underset{˙}{0}\}))$
21	3	fvexi	$⊢ F \in V$
22		eqid	$⊢ F freeLMod V = F freeLMod V$
23	22 2 6 18	frlmelbas	$⊢ (F \in V \land V \in V) \to (a \in {Base}_{(F freeLMod V)} \leftrightarrow (a \in (K^{V}) \land {finSupp}_{\underset{˙}{0}} (a)))$
24	21 13 23	sylancr	$⊢ (W \in LMod \land V \subseteq B) \to (a \in {Base}_{(F freeLMod V)} \leftrightarrow (a \in (K^{V}) \land {finSupp}_{\underset{˙}{0}} (a)))$
25	24	imbi1d	$⊢ (W \in LMod \land V \subseteq B) \to ((a \in {Base}_{(F freeLMod V)} \to (\sum_{W} (a {\underset{˙}{\cdot}}_{f} ({I ↾}_{V})) = O \to a = V \times \{\underset{˙}{0}\})) \leftrightarrow ((a \in (K^{V}) \land {finSupp}_{\underset{˙}{0}} (a)) \to (\sum_{W} (a {\underset{˙}{\cdot}}_{f} ({I ↾}_{V})) = O \to a = V \times \{\underset{˙}{0}\})))$
26		elmapfn	$⊢ a \in (K^{V}) \to a Fn V$
27	26	ad2antrl	$⊢ ((W \in LMod \land V \subseteq B) \land (a \in (K^{V}) \land {finSupp}_{\underset{˙}{0}} (a))) \to a Fn V$
28	17	adantr	$⊢ ((W \in LMod \land V \subseteq B) \land (a \in (K^{V}) \land {finSupp}_{\underset{˙}{0}} (a))) \to ({I ↾}_{V}) : V ⟶ B$
29	28	ffnd	$⊢ ((W \in LMod \land V \subseteq B) \land (a \in (K^{V}) \land {finSupp}_{\underset{˙}{0}} (a))) \to ({I ↾}_{V}) Fn V$
30	13	adantr	$⊢ ((W \in LMod \land V \subseteq B) \land (a \in (K^{V}) \land {finSupp}_{\underset{˙}{0}} (a))) \to V \in V$
31		inidm	$⊢ V \cap V = V$
32		eqidd	$⊢ (((W \in LMod \land V \subseteq B) \land (a \in (K^{V}) \land {finSupp}_{\underset{˙}{0}} (a))) \land v \in V) \to a (v) = a (v)$
33		fvresi	$⊢ v \in V \to ({I ↾}_{V}) (v) = v$
34	33	adantl	$⊢ (((W \in LMod \land V \subseteq B) \land (a \in (K^{V}) \land {finSupp}_{\underset{˙}{0}} (a))) \land v \in V) \to ({I ↾}_{V}) (v) = v$
35	27 29 30 30 31 32 34	offval	$⊢ ((W \in LMod \land V \subseteq B) \land (a \in (K^{V}) \land {finSupp}_{\underset{˙}{0}} (a))) \to a {\underset{˙}{\cdot}}_{f} ({I ↾}_{V}) = (v \in V ⟼ a (v) \underset{˙}{\cdot} v)$
36	35	oveq2d	$⊢ ((W \in LMod \land V \subseteq B) \land (a \in (K^{V}) \land {finSupp}_{\underset{˙}{0}} (a))) \to \sum_{W} (a {\underset{˙}{\cdot}}_{f} ({I ↾}_{V})) = \underset{v \in V}{\sum_{W}} (a (v) \underset{˙}{\cdot} v)$
37	36	eqeq1d	$⊢ ((W \in LMod \land V \subseteq B) \land (a \in (K^{V}) \land {finSupp}_{\underset{˙}{0}} (a))) \to (\sum_{W} (a {\underset{˙}{\cdot}}_{f} ({I ↾}_{V})) = O \leftrightarrow \underset{v \in V}{\sum_{W}} (a (v) \underset{˙}{\cdot} v) = O)$
38	37	imbi1d	$⊢ ((W \in LMod \land V \subseteq B) \land (a \in (K^{V}) \land {finSupp}_{\underset{˙}{0}} (a))) \to ((\sum_{W} (a {\underset{˙}{\cdot}}_{f} ({I ↾}_{V})) = O \to a = V \times \{\underset{˙}{0}\}) \leftrightarrow (\underset{v \in V}{\sum_{W}} (a (v) \underset{˙}{\cdot} v) = O \to a = V \times \{\underset{˙}{0}\}))$
39	38	pm5.74da	$⊢ (W \in LMod \land V \subseteq B) \to (((a \in (K^{V}) \land {finSupp}_{\underset{˙}{0}} (a)) \to (\sum_{W} (a {\underset{˙}{\cdot}}_{f} ({I ↾}_{V})) = O \to a = V \times \{\underset{˙}{0}\})) \leftrightarrow ((a \in (K^{V}) \land {finSupp}_{\underset{˙}{0}} (a)) \to (\underset{v \in V}{\sum_{W}} (a (v) \underset{˙}{\cdot} v) = O \to a = V \times \{\underset{˙}{0}\})))$
40		impexp	$⊢ ((a \in (K^{V}) \land {finSupp}_{\underset{˙}{0}} (a)) \to (\underset{v \in V}{\sum_{W}} (a (v) \underset{˙}{\cdot} v) = O \to a = V \times \{\underset{˙}{0}\})) \leftrightarrow (a \in (K^{V}) \to ({finSupp}_{\underset{˙}{0}} (a) \to (\underset{v \in V}{\sum_{W}} (a (v) \underset{˙}{\cdot} v) = O \to a = V \times \{\underset{˙}{0}\})))$
41		impexp	$⊢ (({finSupp}_{\underset{˙}{0}} (a) \land \underset{v \in V}{\sum_{W}} (a (v) \underset{˙}{\cdot} v) = O) \to a = V \times \{\underset{˙}{0}\}) \leftrightarrow ({finSupp}_{\underset{˙}{0}} (a) \to (\underset{v \in V}{\sum_{W}} (a (v) \underset{˙}{\cdot} v) = O \to a = V \times \{\underset{˙}{0}\}))$
42	41	imbi2i	$⊢ (a \in (K^{V}) \to (({finSupp}_{\underset{˙}{0}} (a) \land \underset{v \in V}{\sum_{W}} (a (v) \underset{˙}{\cdot} v) = O) \to a = V \times \{\underset{˙}{0}\})) \leftrightarrow (a \in (K^{V}) \to ({finSupp}_{\underset{˙}{0}} (a) \to (\underset{v \in V}{\sum_{W}} (a (v) \underset{˙}{\cdot} v) = O \to a = V \times \{\underset{˙}{0}\})))$
43	40 42	bitr4i	$⊢ ((a \in (K^{V}) \land {finSupp}_{\underset{˙}{0}} (a)) \to (\underset{v \in V}{\sum_{W}} (a (v) \underset{˙}{\cdot} v) = O \to a = V \times \{\underset{˙}{0}\})) \leftrightarrow (a \in (K^{V}) \to (({finSupp}_{\underset{˙}{0}} (a) \land \underset{v \in V}{\sum_{W}} (a (v) \underset{˙}{\cdot} v) = O) \to a = V \times \{\underset{˙}{0}\}))$
44	43	a1i	$⊢ (W \in LMod \land V \subseteq B) \to (((a \in (K^{V}) \land {finSupp}_{\underset{˙}{0}} (a)) \to (\underset{v \in V}{\sum_{W}} (a (v) \underset{˙}{\cdot} v) = O \to a = V \times \{\underset{˙}{0}\})) \leftrightarrow (a \in (K^{V}) \to (({finSupp}_{\underset{˙}{0}} (a) \land \underset{v \in V}{\sum_{W}} (a (v) \underset{˙}{\cdot} v) = O) \to a = V \times \{\underset{˙}{0}\})))$
45	25 39 44	3bitrd	$⊢ (W \in LMod \land V \subseteq B) \to ((a \in {Base}_{(F freeLMod V)} \to (\sum_{W} (a {\underset{˙}{\cdot}}_{f} ({I ↾}_{V})) = O \to a = V \times \{\underset{˙}{0}\})) \leftrightarrow (a \in (K^{V}) \to (({finSupp}_{\underset{˙}{0}} (a) \land \underset{v \in V}{\sum_{W}} (a (v) \underset{˙}{\cdot} v) = O) \to a = V \times \{\underset{˙}{0}\})))$
46	45	ralbidv2	$⊢ (W \in LMod \land V \subseteq B) \to (\forall a \in {Base}_{(F freeLMod V)} (\sum_{W} (a {\underset{˙}{\cdot}}_{f} ({I ↾}_{V})) = O \to a = V \times \{\underset{˙}{0}\}) \leftrightarrow \forall a \in (K^{V}) (({finSupp}_{\underset{˙}{0}} (a) \land \underset{v \in V}{\sum_{W}} (a (v) \underset{˙}{\cdot} v) = O) \to a = V \times \{\underset{˙}{0}\}))$
47	8 20 46	3bitrd	$⊢ (W \in LMod \land V \subseteq B) \to (V \in LIndS (W) \leftrightarrow \forall a \in (K^{V}) (({finSupp}_{\underset{˙}{0}} (a) \land \underset{v \in V}{\sum_{W}} (a (v) \underset{˙}{\cdot} v) = O) \to a = V \times \{\underset{˙}{0}\}))$

Metamath Proof Explorer

Theorem islinds5

Proof