lbslsat

Description: A nonzero vector X is a basis of a line spanned by the singleton X . Spans of nonzero singletons are sometimes called "atoms", see df-lsatoms and for example lsatlspsn . (Contributed by Thierry Arnoux, 20-May-2023)

	Ref	Expression
Hypotheses	lbslsat.v	$⊢ V = {Base}_{W}$
	lbslsat.n	$⊢ N = LSpan (W)$
	lbslsat.z	$⊢ \underset{˙}{0} = 0_{W}$
	lbslsat.y	$⊢ Y = W ↾_{𝑠} N (\{X\})$
Assertion	lbslsat	$⊢ (W \in LVec \land X \in V \land X \neq \underset{˙}{0}) \to \{X\} \in LBasis (Y)$

Proof

Step	Hyp	Ref	Expression
1		lbslsat.v	$⊢ V = {Base}_{W}$
2		lbslsat.n	$⊢ N = LSpan (W)$
3		lbslsat.z	$⊢ \underset{˙}{0} = 0_{W}$
4		lbslsat.y	$⊢ Y = W ↾_{𝑠} N (\{X\})$
5		lveclmod	$⊢ W \in LVec \to W \in LMod$
6	5	adantr	$⊢ (W \in LVec \land X \in V) \to W \in LMod$
7		snssi	$⊢ X \in V \to \{X\} \subseteq V$
8	7	adantl	$⊢ (W \in LVec \land X \in V) \to \{X\} \subseteq V$
9		eqid	$⊢ LSubSp (W) = LSubSp (W)$
10	1 9 2	lspcl	$⊢ (W \in LMod \land \{X\} \subseteq V) \to N (\{X\}) \in LSubSp (W)$
11	6 8 10	syl2anc	$⊢ (W \in LVec \land X \in V) \to N (\{X\}) \in LSubSp (W)$
12	4 9	lsslvec	$⊢ (W \in LVec \land N (\{X\}) \in LSubSp (W)) \to Y \in LVec$
13	11 12	syldan	$⊢ (W \in LVec \land X \in V) \to Y \in LVec$
14	13	3adant3	$⊢ (W \in LVec \land X \in V \land X \neq \underset{˙}{0}) \to Y \in LVec$
15	1 2	lspssid	$⊢ (W \in LMod \land \{X\} \subseteq V) \to \{X\} \subseteq N (\{X\})$
16	6 8 15	syl2anc	$⊢ (W \in LVec \land X \in V) \to \{X\} \subseteq N (\{X\})$
17	1 2	lspssv	$⊢ (W \in LMod \land \{X\} \subseteq V) \to N (\{X\}) \subseteq V$
18	6 8 17	syl2anc	$⊢ (W \in LVec \land X \in V) \to N (\{X\}) \subseteq V$
19	4 1	ressbas2	$⊢ N (\{X\}) \subseteq V \to N (\{X\}) = {Base}_{Y}$
20	18 19	syl	$⊢ (W \in LVec \land X \in V) \to N (\{X\}) = {Base}_{Y}$
21	16 20	sseqtrd	$⊢ (W \in LVec \land X \in V) \to \{X\} \subseteq {Base}_{Y}$
22	21	3adant3	$⊢ (W \in LVec \land X \in V \land X \neq \underset{˙}{0}) \to \{X\} \subseteq {Base}_{Y}$
23	6	3adant3	$⊢ (W \in LVec \land X \in V \land X \neq \underset{˙}{0}) \to W \in LMod$
24	11	3adant3	$⊢ (W \in LVec \land X \in V \land X \neq \underset{˙}{0}) \to N (\{X\}) \in LSubSp (W)$
25	16	3adant3	$⊢ (W \in LVec \land X \in V \land X \neq \underset{˙}{0}) \to \{X\} \subseteq N (\{X\})$
26		eqid	$⊢ LSpan (Y) = LSpan (Y)$
27	4 2 26 9	lsslsp	$⊢ (W \in LMod \land N (\{X\}) \in LSubSp (W) \land \{X\} \subseteq N (\{X\})) \to N (\{X\}) = LSpan (Y) (\{X\})$
28	23 24 25 27	syl3anc	$⊢ (W \in LVec \land X \in V \land X \neq \underset{˙}{0}) \to N (\{X\}) = LSpan (Y) (\{X\})$
29	20	3adant3	$⊢ (W \in LVec \land X \in V \land X \neq \underset{˙}{0}) \to N (\{X\}) = {Base}_{Y}$
30	28 29	eqtr3d	$⊢ (W \in LVec \land X \in V \land X \neq \underset{˙}{0}) \to LSpan (Y) (\{X\}) = {Base}_{Y}$
31		difid	$⊢ \{X\} ∖ \{X\} = \emptyset$
32	31	fveq2i	$⊢ LSpan (Y) (\{X\} ∖ \{X\}) = LSpan (Y) (\emptyset)$
33	32	a1i	$⊢ (W \in LVec \land X \in V) \to LSpan (Y) (\{X\} ∖ \{X\}) = LSpan (Y) (\emptyset)$
34	33	eleq2d	$⊢ (W \in LVec \land X \in V) \to (X \in LSpan (Y) (\{X\} ∖ \{X\}) \leftrightarrow X \in LSpan (Y) (\emptyset))$
35	34	biimpa	$⊢ ((W \in LVec \land X \in V) \land X \in LSpan (Y) (\{X\} ∖ \{X\})) \to X \in LSpan (Y) (\emptyset)$
36		lveclmod	$⊢ Y \in LVec \to Y \in LMod$
37		eqid	$⊢ 0_{Y} = 0_{Y}$
38	37 26	lsp0	$⊢ Y \in LMod \to LSpan (Y) (\emptyset) = \{0_{Y}\}$
39	13 36 38	3syl	$⊢ (W \in LVec \land X \in V) \to LSpan (Y) (\emptyset) = \{0_{Y}\}$
40	39	adantr	$⊢ ((W \in LVec \land X \in V) \land X \in LSpan (Y) (\{X\} ∖ \{X\})) \to LSpan (Y) (\emptyset) = \{0_{Y}\}$
41	35 40	eleqtrd	$⊢ ((W \in LVec \land X \in V) \land X \in LSpan (Y) (\{X\} ∖ \{X\})) \to X \in \{0_{Y}\}$
42		elsni	$⊢ X \in \{0_{Y}\} \to X = 0_{Y}$
43	41 42	syl	$⊢ ((W \in LVec \land X \in V) \land X \in LSpan (Y) (\{X\} ∖ \{X\})) \to X = 0_{Y}$
44		lmodgrp	$⊢ W \in LMod \to W \in Grp$
45		grpmnd	$⊢ W \in Grp \to W \in Mnd$
46	6 44 45	3syl	$⊢ (W \in LVec \land X \in V) \to W \in Mnd$
47	3 1 2	0ellsp	$⊢ (W \in LMod \land \{X\} \subseteq V) \to \underset{˙}{0} \in N (\{X\})$
48	6 8 47	syl2anc	$⊢ (W \in LVec \land X \in V) \to \underset{˙}{0} \in N (\{X\})$
49	4 1 3	ress0g	$⊢ (W \in Mnd \land \underset{˙}{0} \in N (\{X\}) \land N (\{X\}) \subseteq V) \to \underset{˙}{0} = 0_{Y}$
50	46 48 18 49	syl3anc	$⊢ (W \in LVec \land X \in V) \to \underset{˙}{0} = 0_{Y}$
51	50	adantr	$⊢ ((W \in LVec \land X \in V) \land X \in LSpan (Y) (\{X\} ∖ \{X\})) \to \underset{˙}{0} = 0_{Y}$
52	43 51	eqtr4d	$⊢ ((W \in LVec \land X \in V) \land X \in LSpan (Y) (\{X\} ∖ \{X\})) \to X = \underset{˙}{0}$
53	52	ex	$⊢ (W \in LVec \land X \in V) \to (X \in LSpan (Y) (\{X\} ∖ \{X\}) \to X = \underset{˙}{0})$
54	53	necon3ad	$⊢ (W \in LVec \land X \in V) \to (X \neq \underset{˙}{0} \to \neg X \in LSpan (Y) (\{X\} ∖ \{X\}))$
55	54	3impia	$⊢ (W \in LVec \land X \in V \land X \neq \underset{˙}{0}) \to \neg X \in LSpan (Y) (\{X\} ∖ \{X\})$
56		id	$⊢ x = X \to x = X$
57		sneq	$⊢ x = X \to \{x\} = \{X\}$
58	57	difeq2d	$⊢ x = X \to \{X\} ∖ \{x\} = \{X\} ∖ \{X\}$
59	58	fveq2d	$⊢ x = X \to LSpan (Y) (\{X\} ∖ \{x\}) = LSpan (Y) (\{X\} ∖ \{X\})$
60	56 59	eleq12d	$⊢ x = X \to (x \in LSpan (Y) (\{X\} ∖ \{x\}) \leftrightarrow X \in LSpan (Y) (\{X\} ∖ \{X\}))$
61	60	notbid	$⊢ x = X \to (\neg x \in LSpan (Y) (\{X\} ∖ \{x\}) \leftrightarrow \neg X \in LSpan (Y) (\{X\} ∖ \{X\}))$
62	61	ralsng	$⊢ X \in V \to (\forall x \in \{X\} \neg x \in LSpan (Y) (\{X\} ∖ \{x\}) \leftrightarrow \neg X \in LSpan (Y) (\{X\} ∖ \{X\}))$
63	62	3ad2ant2	$⊢ (W \in LVec \land X \in V \land X \neq \underset{˙}{0}) \to (\forall x \in \{X\} \neg x \in LSpan (Y) (\{X\} ∖ \{x\}) \leftrightarrow \neg X \in LSpan (Y) (\{X\} ∖ \{X\}))$
64	55 63	mpbird	$⊢ (W \in LVec \land X \in V \land X \neq \underset{˙}{0}) \to \forall x \in \{X\} \neg x \in LSpan (Y) (\{X\} ∖ \{x\})$
65		eqid	$⊢ {Base}_{Y} = {Base}_{Y}$
66		eqid	$⊢ LBasis (Y) = LBasis (Y)$
67	65 66 26	islbs2	$⊢ Y \in LVec \to (\{X\} \in LBasis (Y) \leftrightarrow (\{X\} \subseteq {Base}_{Y} \land LSpan (Y) (\{X\}) = {Base}_{Y} \land \forall x \in \{X\} \neg x \in LSpan (Y) (\{X\} ∖ \{x\})))$
68	67	biimpar	$⊢ (Y \in LVec \land (\{X\} \subseteq {Base}_{Y} \land LSpan (Y) (\{X\}) = {Base}_{Y} \land \forall x \in \{X\} \neg x \in LSpan (Y) (\{X\} ∖ \{x\}))) \to \{X\} \in LBasis (Y)$
69	14 22 30 64 68	syl13anc	$⊢ (W \in LVec \land X \in V \land X \neq \underset{˙}{0}) \to \{X\} \in LBasis (Y)$

Metamath Proof Explorer

Theorem lbslsat

Proof