0nellinds

Description: The group identity cannot be an element of an independent set. (Contributed by Thierry Arnoux, 8-May-2023)

		Ref	Expression
	Hypothesis	0nellinds.1	$⊢ \underset{˙}{0} = 0_{W}$
	Assertion	0nellinds	$⊢ (W \in LVec \land F \in LIndS (W)) \to \neg \underset{˙}{0} \in F$

Proof

Step	Hyp	Ref	Expression
1		0nellinds.1	$⊢ \underset{˙}{0} = 0_{W}$
2		oveq2	$⊢ x = \underset{˙}{0} \to k \cdot_{W} x = k \cdot_{W} \underset{˙}{0}$
3		sneq	$⊢ x = \underset{˙}{0} \to \{x\} = \{\underset{˙}{0}\}$
4	3	difeq2d	$⊢ x = \underset{˙}{0} \to F ∖ \{x\} = F ∖ \{\underset{˙}{0}\}$
5	4	fveq2d	$⊢ x = \underset{˙}{0} \to LSpan (W) (F ∖ \{x\}) = LSpan (W) (F ∖ \{\underset{˙}{0}\})$
6	2 5	eleq12d	$⊢ x = \underset{˙}{0} \to (k \cdot_{W} x \in LSpan (W) (F ∖ \{x\}) \leftrightarrow k \cdot_{W} \underset{˙}{0} \in LSpan (W) (F ∖ \{\underset{˙}{0}\}))$
7	6	notbid	$⊢ x = \underset{˙}{0} \to (\neg k \cdot_{W} x \in LSpan (W) (F ∖ \{x\}) \leftrightarrow \neg k \cdot_{W} \underset{˙}{0} \in LSpan (W) (F ∖ \{\underset{˙}{0}\}))$
8	7	ralbidv	$⊢ x = \underset{˙}{0} \to (\forall k \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\}) \neg k \cdot_{W} x \in LSpan (W) (F ∖ \{x\}) \leftrightarrow \forall k \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\}) \neg k \cdot_{W} \underset{˙}{0} \in LSpan (W) (F ∖ \{\underset{˙}{0}\}))$
9		eqid	$⊢ {Base}_{W} = {Base}_{W}$
10		eqid	$⊢ \cdot_{W} = \cdot_{W}$
11		eqid	$⊢ LSpan (W) = LSpan (W)$
12		eqid	$⊢ Scalar (W) = Scalar (W)$
13		eqid	$⊢ {Base}_{Scalar (W)} = {Base}_{Scalar (W)}$
14		eqid	$⊢ 0_{Scalar (W)} = 0_{Scalar (W)}$
15	9 10 11 12 13 14	islinds2	$⊢ W \in LVec \to (F \in LIndS (W) \leftrightarrow (F \subseteq {Base}_{W} \land \forall x \in F \forall k \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\}) \neg k \cdot_{W} x \in LSpan (W) (F ∖ \{x\})))$
16	15	simplbda	$⊢ (W \in LVec \land F \in LIndS (W)) \to \forall x \in F \forall k \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\}) \neg k \cdot_{W} x \in LSpan (W) (F ∖ \{x\})$
17	16	adantr	$⊢ ((W \in LVec \land F \in LIndS (W)) \land \underset{˙}{0} \in F) \to \forall x \in F \forall k \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\}) \neg k \cdot_{W} x \in LSpan (W) (F ∖ \{x\})$
18		simpr	$⊢ ((W \in LVec \land F \in LIndS (W)) \land \underset{˙}{0} \in F) \to \underset{˙}{0} \in F$
19	8 17 18	rspcdva	$⊢ ((W \in LVec \land F \in LIndS (W)) \land \underset{˙}{0} \in F) \to \forall k \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\}) \neg k \cdot_{W} \underset{˙}{0} \in LSpan (W) (F ∖ \{\underset{˙}{0}\})$
20		lveclmod	$⊢ W \in LVec \to W \in LMod$
21		eqid	$⊢ 1_{Scalar (W)} = 1_{Scalar (W)}$
22	12 13 21	lmod1cl	$⊢ W \in LMod \to 1_{Scalar (W)} \in {Base}_{Scalar (W)}$
23	20 22	syl	$⊢ W \in LVec \to 1_{Scalar (W)} \in {Base}_{Scalar (W)}$
24	23	adantr	$⊢ (W \in LVec \land F \in LIndS (W)) \to 1_{Scalar (W)} \in {Base}_{Scalar (W)}$
25	12	lvecdrng	$⊢ W \in LVec \to Scalar (W) \in DivRing$
26	14 21	drngunz	$⊢ Scalar (W) \in DivRing \to 1_{Scalar (W)} \neq 0_{Scalar (W)}$
27	25 26	syl	$⊢ W \in LVec \to 1_{Scalar (W)} \neq 0_{Scalar (W)}$
28	27	adantr	$⊢ (W \in LVec \land F \in LIndS (W)) \to 1_{Scalar (W)} \neq 0_{Scalar (W)}$
29		eldifsn	$⊢ 1_{Scalar (W)} \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\}) \leftrightarrow (1_{Scalar (W)} \in {Base}_{Scalar (W)} \land 1_{Scalar (W)} \neq 0_{Scalar (W)})$
30	24 28 29	sylanbrc	$⊢ (W \in LVec \land F \in LIndS (W)) \to 1_{Scalar (W)} \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\})$
31	30	adantr	$⊢ ((W \in LVec \land F \in LIndS (W)) \land \underset{˙}{0} \in F) \to 1_{Scalar (W)} \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\})$
32	20	ad2antrr	$⊢ ((W \in LVec \land F \in LIndS (W)) \land \underset{˙}{0} \in F) \to W \in LMod$
33	12 10 13 1	lmodvs0	$⊢ (W \in LMod \land 1_{Scalar (W)} \in {Base}_{Scalar (W)}) \to 1_{Scalar (W)} \cdot_{W} \underset{˙}{0} = \underset{˙}{0}$
34	32 22 33	syl2anc2	$⊢ ((W \in LVec \land F \in LIndS (W)) \land \underset{˙}{0} \in F) \to 1_{Scalar (W)} \cdot_{W} \underset{˙}{0} = \underset{˙}{0}$
35	9	linds1	$⊢ F \in LIndS (W) \to F \subseteq {Base}_{W}$
36	35	ad2antlr	$⊢ ((W \in LVec \land F \in LIndS (W)) \land \underset{˙}{0} \in F) \to F \subseteq {Base}_{W}$
37	36	ssdifssd	$⊢ ((W \in LVec \land F \in LIndS (W)) \land \underset{˙}{0} \in F) \to F ∖ \{\underset{˙}{0}\} \subseteq {Base}_{W}$
38	1 9 11	0ellsp	$⊢ (W \in LMod \land F ∖ \{\underset{˙}{0}\} \subseteq {Base}_{W}) \to \underset{˙}{0} \in LSpan (W) (F ∖ \{\underset{˙}{0}\})$
39	32 37 38	syl2anc	$⊢ ((W \in LVec \land F \in LIndS (W)) \land \underset{˙}{0} \in F) \to \underset{˙}{0} \in LSpan (W) (F ∖ \{\underset{˙}{0}\})$
40	34 39	eqeltrd	$⊢ ((W \in LVec \land F \in LIndS (W)) \land \underset{˙}{0} \in F) \to 1_{Scalar (W)} \cdot_{W} \underset{˙}{0} \in LSpan (W) (F ∖ \{\underset{˙}{0}\})$
41		oveq1	$⊢ k = 1_{Scalar (W)} \to k \cdot_{W} \underset{˙}{0} = 1_{Scalar (W)} \cdot_{W} \underset{˙}{0}$
42	41	eleq1d	$⊢ k = 1_{Scalar (W)} \to (k \cdot_{W} \underset{˙}{0} \in LSpan (W) (F ∖ \{\underset{˙}{0}\}) \leftrightarrow 1_{Scalar (W)} \cdot_{W} \underset{˙}{0} \in LSpan (W) (F ∖ \{\underset{˙}{0}\}))$
43	42	rspcev	$⊢ (1_{Scalar (W)} \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\}) \land 1_{Scalar (W)} \cdot_{W} \underset{˙}{0} \in LSpan (W) (F ∖ \{\underset{˙}{0}\})) \to \exists k \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\}) k \cdot_{W} \underset{˙}{0} \in LSpan (W) (F ∖ \{\underset{˙}{0}\})$
44	31 40 43	syl2anc	$⊢ ((W \in LVec \land F \in LIndS (W)) \land \underset{˙}{0} \in F) \to \exists k \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\}) k \cdot_{W} \underset{˙}{0} \in LSpan (W) (F ∖ \{\underset{˙}{0}\})$
45		dfrex2	$⊢ \exists k \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\}) k \cdot_{W} \underset{˙}{0} \in LSpan (W) (F ∖ \{\underset{˙}{0}\}) \leftrightarrow \neg \forall k \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\}) \neg k \cdot_{W} \underset{˙}{0} \in LSpan (W) (F ∖ \{\underset{˙}{0}\})$
46	44 45	sylib	$⊢ ((W \in LVec \land F \in LIndS (W)) \land \underset{˙}{0} \in F) \to \neg \forall k \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\}) \neg k \cdot_{W} \underset{˙}{0} \in LSpan (W) (F ∖ \{\underset{˙}{0}\})$
47	19 46	pm2.65da	$⊢ (W \in LVec \land F \in LIndS (W)) \to \neg \underset{˙}{0} \in F$

Metamath Proof Explorer

Theorem 0nellinds

Proof