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

Metamath Proof Explorer

Theorem lbslsat

Proof