Theorem lindssn

Description: Any singleton of a nonzero element is an independent set. (Contributed by Thierry Arnoux, 5-Aug-2023)

	Ref	Expression
Hypotheses	lindssn.1	$$⊢B={\mathrm{Base}}_W$$
	lindssn.2	$$⊢\underset{\dot{}}{0}=0_W$$
Assertion	lindssn	$$⊢\left(W\in \mathrm{LVec}\wedge X\in B\wedge X\ne \underset{\dot{}}{0}\right)\to \left\{X\right\}\in \mathrm{LIndS}\left(W\right)$$

Proof

Step	Hyp	Ref	Expression
1		lindssn.1	$$⊢B={\mathrm{Base}}_W$$
2		lindssn.2	$$⊢\underset{\dot{}}{0}=0_W$$
3		simp1	$$⊢\left(W\in \mathrm{LVec}\wedge X\in B\wedge X\ne \underset{\dot{}}{0}\right)\to W\in \mathrm{LVec}$$
4		snssi	$$⊢X\in B\to \left\{X\right\}\subseteq B$$
5	4	3ad2ant2	$$⊢\left(W\in \mathrm{LVec}\wedge X\in B\wedge X\ne \underset{\dot{}}{0}\right)\to \left\{X\right\}\subseteq B$$
6		simpr	$$⊢\left(\left(W\in \mathrm{LVec}\wedge X\in B\wedge X\ne \underset{\dot{}}{0}\right)\wedge y\in \left({\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\setminus \left\{0_{\mathrm{Scalar}\left(W\right)}\right\}\right)\right)\to y\in \left({\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\setminus \left\{0_{\mathrm{Scalar}\left(W\right)}\right\}\right)$$
7		eldifsni	$$⊢y\in \left({\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\setminus \left\{0_{\mathrm{Scalar}\left(W\right)}\right\}\right)\to y\ne 0_{\mathrm{Scalar}\left(W\right)}$$
8	6 7	syl	$$⊢\left(\left(W\in \mathrm{LVec}\wedge X\in B\wedge X\ne \underset{\dot{}}{0}\right)\wedge y\in \left({\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\setminus \left\{0_{\mathrm{Scalar}\left(W\right)}\right\}\right)\right)\to y\ne 0_{\mathrm{Scalar}\left(W\right)}$$
9	8	neneqd	$$⊢\left(\left(W\in \mathrm{LVec}\wedge X\in B\wedge X\ne \underset{\dot{}}{0}\right)\wedge y\in \left({\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\setminus \left\{0_{\mathrm{Scalar}\left(W\right)}\right\}\right)\right)\to \neg y=0_{\mathrm{Scalar}\left(W\right)}$$
10		simpl3	$$⊢\left(\left(W\in \mathrm{LVec}\wedge X\in B\wedge X\ne \underset{\dot{}}{0}\right)\wedge y\in \left({\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\setminus \left\{0_{\mathrm{Scalar}\left(W\right)}\right\}\right)\right)\to X\ne \underset{\dot{}}{0}$$
11	10	neneqd	$$⊢\left(\left(W\in \mathrm{LVec}\wedge X\in B\wedge X\ne \underset{\dot{}}{0}\right)\wedge y\in \left({\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\setminus \left\{0_{\mathrm{Scalar}\left(W\right)}\right\}\right)\right)\to \neg X=\underset{\dot{}}{0}$$
12		ioran	$$⊢\neg \left(y=0_{\mathrm{Scalar}\left(W\right)}\vee X=\underset{\dot{}}{0}\right)\leftrightarrow \left(\neg y=0_{\mathrm{Scalar}\left(W\right)}\wedge \neg X=\underset{\dot{}}{0}\right)$$
13	9 11 12	sylanbrc	$$⊢\left(\left(W\in \mathrm{LVec}\wedge X\in B\wedge X\ne \underset{\dot{}}{0}\right)\wedge y\in \left({\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\setminus \left\{0_{\mathrm{Scalar}\left(W\right)}\right\}\right)\right)\to \neg \left(y=0_{\mathrm{Scalar}\left(W\right)}\vee X=\underset{\dot{}}{0}\right)$$
14		eqid	$$⊢{\cdot }_W={\cdot }_W$$
15		eqid	$$⊢\mathrm{Scalar}\left(W\right)=\mathrm{Scalar}\left(W\right)$$
16		eqid	$$⊢{\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}$$
17		eqid	$$⊢0_{\mathrm{Scalar}\left(W\right)}=0_{\mathrm{Scalar}\left(W\right)}$$
18	3	adantr	$$⊢\left(\left(W\in \mathrm{LVec}\wedge X\in B\wedge X\ne \underset{\dot{}}{0}\right)\wedge y\in \left({\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\setminus \left\{0_{\mathrm{Scalar}\left(W\right)}\right\}\right)\right)\to W\in \mathrm{LVec}$$
19	6	eldifad	$$⊢\left(\left(W\in \mathrm{LVec}\wedge X\in B\wedge X\ne \underset{\dot{}}{0}\right)\wedge y\in \left({\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\setminus \left\{0_{\mathrm{Scalar}\left(W\right)}\right\}\right)\right)\to y\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}$$
20		simpl2	$$⊢\left(\left(W\in \mathrm{LVec}\wedge X\in B\wedge X\ne \underset{\dot{}}{0}\right)\wedge y\in \left({\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\setminus \left\{0_{\mathrm{Scalar}\left(W\right)}\right\}\right)\right)\to X\in B$$
21	1 14 15 16 17 2 18 19 20	lvecvs0or	$$⊢\left(\left(W\in \mathrm{LVec}\wedge X\in B\wedge X\ne \underset{\dot{}}{0}\right)\wedge y\in \left({\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\setminus \left\{0_{\mathrm{Scalar}\left(W\right)}\right\}\right)\right)\to \left(y{\cdot }_{W}X=\underset{\dot{}}{0}\leftrightarrow \left(y=0_{\mathrm{Scalar}\left(W\right)}\vee X=\underset{\dot{}}{0}\right)\right)$$
22	21	necon3abid	$$⊢\left(\left(W\in \mathrm{LVec}\wedge X\in B\wedge X\ne \underset{\dot{}}{0}\right)\wedge y\in \left({\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\setminus \left\{0_{\mathrm{Scalar}\left(W\right)}\right\}\right)\right)\to \left(y{\cdot }_{W}X\ne \underset{\dot{}}{0}\leftrightarrow \neg \left(y=0_{\mathrm{Scalar}\left(W\right)}\vee X=\underset{\dot{}}{0}\right)\right)$$
23	13 22	mpbird	$$⊢\left(\left(W\in \mathrm{LVec}\wedge X\in B\wedge X\ne \underset{\dot{}}{0}\right)\wedge y\in \left({\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\setminus \left\{0_{\mathrm{Scalar}\left(W\right)}\right\}\right)\right)\to y{\cdot }_{W}X\ne \underset{\dot{}}{0}$$
24		nelsn	$$⊢y{\cdot }_{W}X\ne \underset{\dot{}}{0}\to \neg y{\cdot }_{W}X\in \left\{\underset{\dot{}}{0}\right\}$$
25	23 24	syl	$$⊢\left(\left(W\in \mathrm{LVec}\wedge X\in B\wedge X\ne \underset{\dot{}}{0}\right)\wedge y\in \left({\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\setminus \left\{0_{\mathrm{Scalar}\left(W\right)}\right\}\right)\right)\to \neg y{\cdot }_{W}X\in \left\{\underset{\dot{}}{0}\right\}$$
26		difid	$$⊢\left\{X\right\}\setminus \left\{X\right\}=\varnothing$$
27	26	a1i	$$⊢\left(\left(W\in \mathrm{LVec}\wedge X\in B\wedge X\ne \underset{\dot{}}{0}\right)\wedge y\in \left({\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\setminus \left\{0_{\mathrm{Scalar}\left(W\right)}\right\}\right)\right)\to \left\{X\right\}\setminus \left\{X\right\}=\varnothing$$
28	27	fveq2d	$$⊢\left(\left(W\in \mathrm{LVec}\wedge X\in B\wedge X\ne \underset{\dot{}}{0}\right)\wedge y\in \left({\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\setminus \left\{0_{\mathrm{Scalar}\left(W\right)}\right\}\right)\right)\to \mathrm{LSpan}\left(W\right)\left(\left\{X\right\}\setminus \left\{X\right\}\right)=\mathrm{LSpan}\left(W\right)\left(\varnothing \right)$$
29		lveclmod	$$⊢W\in \mathrm{LVec}\to W\in \mathrm{LMod}$$
30		eqid	$$⊢\mathrm{LSpan}\left(W\right)=\mathrm{LSpan}\left(W\right)$$
31	2 30	lsp0	$$⊢W\in \mathrm{LMod}\to \mathrm{LSpan}\left(W\right)\left(\varnothing \right)=\left\{\underset{\dot{}}{0}\right\}$$
32	3 29 31	3syl	$$⊢\left(W\in \mathrm{LVec}\wedge X\in B\wedge X\ne \underset{\dot{}}{0}\right)\to \mathrm{LSpan}\left(W\right)\left(\varnothing \right)=\left\{\underset{\dot{}}{0}\right\}$$
33	32	adantr	$$⊢\left(\left(W\in \mathrm{LVec}\wedge X\in B\wedge X\ne \underset{\dot{}}{0}\right)\wedge y\in \left({\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\setminus \left\{0_{\mathrm{Scalar}\left(W\right)}\right\}\right)\right)\to \mathrm{LSpan}\left(W\right)\left(\varnothing \right)=\left\{\underset{\dot{}}{0}\right\}$$
34	28 33	eqtrd	$$⊢\left(\left(W\in \mathrm{LVec}\wedge X\in B\wedge X\ne \underset{\dot{}}{0}\right)\wedge y\in \left({\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\setminus \left\{0_{\mathrm{Scalar}\left(W\right)}\right\}\right)\right)\to \mathrm{LSpan}\left(W\right)\left(\left\{X\right\}\setminus \left\{X\right\}\right)=\left\{\underset{\dot{}}{0}\right\}$$
35	25 34	neleqtrrd	$$⊢\left(\left(W\in \mathrm{LVec}\wedge X\in B\wedge X\ne \underset{\dot{}}{0}\right)\wedge y\in \left({\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\setminus \left\{0_{\mathrm{Scalar}\left(W\right)}\right\}\right)\right)\to \neg y{\cdot }_{W}X\in \mathrm{LSpan}\left(W\right)\left(\left\{X\right\}\setminus \left\{X\right\}\right)$$
36	35	ralrimiva	$$⊢\left(W\in \mathrm{LVec}\wedge X\in B\wedge X\ne \underset{\dot{}}{0}\right)\to \forall y\in \left({\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\setminus \left\{0_{\mathrm{Scalar}\left(W\right)}\right\}\right)\neg y{\cdot }_{W}X\in \mathrm{LSpan}\left(W\right)\left(\left\{X\right\}\setminus \left\{X\right\}\right)$$
37		oveq2	$$⊢x=X\to y{\cdot }_{W}x=y{\cdot }_{W}X$$
38		sneq	$$⊢x=X\to \left\{x\right\}=\left\{X\right\}$$
39	38	difeq2d	$$⊢x=X\to \left\{X\right\}\setminus \left\{x\right\}=\left\{X\right\}\setminus \left\{X\right\}$$
40	39	fveq2d	$$⊢x=X\to \mathrm{LSpan}\left(W\right)\left(\left\{X\right\}\setminus \left\{x\right\}\right)=\mathrm{LSpan}\left(W\right)\left(\left\{X\right\}\setminus \left\{X\right\}\right)$$
41	37 40	eleq12d	$$⊢x=X\to \left(y{\cdot }_{W}x\in \mathrm{LSpan}\left(W\right)\left(\left\{X\right\}\setminus \left\{x\right\}\right)\leftrightarrow y{\cdot }_{W}X\in \mathrm{LSpan}\left(W\right)\left(\left\{X\right\}\setminus \left\{X\right\}\right)\right)$$
42	41	notbid	$$⊢x=X\to \left(\neg y{\cdot }_{W}x\in \mathrm{LSpan}\left(W\right)\left(\left\{X\right\}\setminus \left\{x\right\}\right)\leftrightarrow \neg y{\cdot }_{W}X\in \mathrm{LSpan}\left(W\right)\left(\left\{X\right\}\setminus \left\{X\right\}\right)\right)$$
43	42	ralbidv	$$⊢x=X\to \left(\forall y\in \left({\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\setminus \left\{0_{\mathrm{Scalar}\left(W\right)}\right\}\right)\neg y{\cdot }_{W}x\in \mathrm{LSpan}\left(W\right)\left(\left\{X\right\}\setminus \left\{x\right\}\right)\leftrightarrow \forall y\in \left({\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\setminus \left\{0_{\mathrm{Scalar}\left(W\right)}\right\}\right)\neg y{\cdot }_{W}X\in \mathrm{LSpan}\left(W\right)\left(\left\{X\right\}\setminus \left\{X\right\}\right)\right)$$
44	43	ralsng	$$⊢X\in B\to \left(\forall x\in \left\{X\right\}\forall y\in \left({\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\setminus \left\{0_{\mathrm{Scalar}\left(W\right)}\right\}\right)\neg y{\cdot }_{W}x\in \mathrm{LSpan}\left(W\right)\left(\left\{X\right\}\setminus \left\{x\right\}\right)\leftrightarrow \forall y\in \left({\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\setminus \left\{0_{\mathrm{Scalar}\left(W\right)}\right\}\right)\neg y{\cdot }_{W}X\in \mathrm{LSpan}\left(W\right)\left(\left\{X\right\}\setminus \left\{X\right\}\right)\right)$$
45	44	3ad2ant2	$$⊢\left(W\in \mathrm{LVec}\wedge X\in B\wedge X\ne \underset{\dot{}}{0}\right)\to \left(\forall x\in \left\{X\right\}\forall y\in \left({\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\setminus \left\{0_{\mathrm{Scalar}\left(W\right)}\right\}\right)\neg y{\cdot }_{W}x\in \mathrm{LSpan}\left(W\right)\left(\left\{X\right\}\setminus \left\{x\right\}\right)\leftrightarrow \forall y\in \left({\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\setminus \left\{0_{\mathrm{Scalar}\left(W\right)}\right\}\right)\neg y{\cdot }_{W}X\in \mathrm{LSpan}\left(W\right)\left(\left\{X\right\}\setminus \left\{X\right\}\right)\right)$$
46	36 45	mpbird	$$⊢\left(W\in \mathrm{LVec}\wedge X\in B\wedge X\ne \underset{\dot{}}{0}\right)\to \forall x\in \left\{X\right\}\forall y\in \left({\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\setminus \left\{0_{\mathrm{Scalar}\left(W\right)}\right\}\right)\neg y{\cdot }_{W}x\in \mathrm{LSpan}\left(W\right)\left(\left\{X\right\}\setminus \left\{x\right\}\right)$$
47	1 14 30 15 16 17	islinds2	$$⊢W\in \mathrm{LVec}\to \left(\left\{X\right\}\in \mathrm{LIndS}\left(W\right)\leftrightarrow \left(\left\{X\right\}\subseteq B\wedge \forall x\in \left\{X\right\}\forall y\in \left({\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\setminus \left\{0_{\mathrm{Scalar}\left(W\right)}\right\}\right)\neg y{\cdot }_{W}x\in \mathrm{LSpan}\left(W\right)\left(\left\{X\right\}\setminus \left\{x\right\}\right)\right)\right)$$
48	47	biimpar	$$⊢\left(W\in \mathrm{LVec}\wedge \left(\left\{X\right\}\subseteq B\wedge \forall x\in \left\{X\right\}\forall y\in \left({\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\setminus \left\{0_{\mathrm{Scalar}\left(W\right)}\right\}\right)\neg y{\cdot }_{W}x\in \mathrm{LSpan}\left(W\right)\left(\left\{X\right\}\setminus \left\{x\right\}\right)\right)\right)\to \left\{X\right\}\in \mathrm{LIndS}\left(W\right)$$
49	3 5 46 48	syl12anc	$$⊢\left(W\in \mathrm{LVec}\wedge X\in B\wedge X\ne \underset{\dot{}}{0}\right)\to \left\{X\right\}\in \mathrm{LIndS}\left(W\right)$$