lindsenlbs

Description: A maximal linearly independent set in a free module of finite dimension over a division ring is a basis. (Contributed by Brendan Leahy, 2-Jun-2021)

		Ref	Expression
	Assertion	lindsenlbs	$⊢ ((R \in DivRing \land I \in Fin \land X \in LIndS (R freeLMod I)) \land X \approx I) \to X \in LBasis (R freeLMod I)$

Proof

Step	Hyp	Ref	Expression
1		simpl3	$⊢ ((R \in DivRing \land I \in Fin \land X \in LIndS (R freeLMod I)) \land X \approx I) \to X \in LIndS (R freeLMod I)$
2		drngring	$⊢ R \in DivRing \to R \in Ring$
3		eqid	$⊢ R freeLMod I = R freeLMod I$
4	3	frlmlmod	$⊢ (R \in Ring \land I \in Fin) \to R freeLMod I \in LMod$
5	2 4	sylan	$⊢ (R \in DivRing \land I \in Fin) \to R freeLMod I \in LMod$
6		eqid	$⊢ {Base}_{(R freeLMod I)} = {Base}_{(R freeLMod I)}$
7	6	linds1	$⊢ X \in LIndS (R freeLMod I) \to X \subseteq {Base}_{(R freeLMod I)}$
8		eqid	$⊢ LSpan (R freeLMod I) = LSpan (R freeLMod I)$
9	6 8	lspssv	$⊢ (R freeLMod I \in LMod \land X \subseteq {Base}_{(R freeLMod I)}) \to LSpan (R freeLMod I) (X) \subseteq {Base}_{(R freeLMod I)}$
10	5 7 9	syl2an	$⊢ ((R \in DivRing \land I \in Fin) \land X \in LIndS (R freeLMod I)) \to LSpan (R freeLMod I) (X) \subseteq {Base}_{(R freeLMod I)}$
11	10	3impa	$⊢ (R \in DivRing \land I \in Fin \land X \in LIndS (R freeLMod I)) \to LSpan (R freeLMod I) (X) \subseteq {Base}_{(R freeLMod I)}$
12	11	adantr	$⊢ ((R \in DivRing \land I \in Fin \land X \in LIndS (R freeLMod I)) \land X \approx I) \to LSpan (R freeLMod I) (X) \subseteq {Base}_{(R freeLMod I)}$
13		bren2	$⊢ X \approx I \leftrightarrow (X ≼ I \land \neg X ≺ I)$
14	13	simprbi	$⊢ X \approx I \to \neg X ≺ I$
15		snfi	$⊢ \{y\} \in Fin$
16		simp2	$⊢ (R \in DivRing \land I \in Fin \land X \in LIndS (R freeLMod I)) \to I \in Fin$
17		lindsdom	$⊢ (R \in DivRing \land I \in Fin \land X \in LIndS (R freeLMod I)) \to X ≼ I$
18		domfi	$⊢ (I \in Fin \land X ≼ I) \to X \in Fin$
19	16 17 18	syl2anc	$⊢ (R \in DivRing \land I \in Fin \land X \in LIndS (R freeLMod I)) \to X \in Fin$
20		unfi	$⊢ (\{y\} \in Fin \land X \in Fin) \to \{y\} \cup X \in Fin$
21	15 19 20	sylancr	$⊢ (R \in DivRing \land I \in Fin \land X \in LIndS (R freeLMod I)) \to \{y\} \cup X \in Fin$
22	21	adantr	$⊢ ((R \in DivRing \land I \in Fin \land X \in LIndS (R freeLMod I)) \land \neg y \in LSpan (R freeLMod I) (X)) \to \{y\} \cup X \in Fin$
23		vex	$⊢ y \in V$
24	23	snss	$⊢ y \in X \leftrightarrow \{y\} \subseteq X$
25	6 8	lspssid	$⊢ (R freeLMod I \in LMod \land X \subseteq {Base}_{(R freeLMod I)}) \to X \subseteq LSpan (R freeLMod I) (X)$
26	5 7 25	syl2an	$⊢ ((R \in DivRing \land I \in Fin) \land X \in LIndS (R freeLMod I)) \to X \subseteq LSpan (R freeLMod I) (X)$
27	26	3impa	$⊢ (R \in DivRing \land I \in Fin \land X \in LIndS (R freeLMod I)) \to X \subseteq LSpan (R freeLMod I) (X)$
28	27	sseld	$⊢ (R \in DivRing \land I \in Fin \land X \in LIndS (R freeLMod I)) \to (y \in X \to y \in LSpan (R freeLMod I) (X))$
29	24 28	biimtrrid	$⊢ (R \in DivRing \land I \in Fin \land X \in LIndS (R freeLMod I)) \to (\{y\} \subseteq X \to y \in LSpan (R freeLMod I) (X))$
30	29	con3dimp	$⊢ ((R \in DivRing \land I \in Fin \land X \in LIndS (R freeLMod I)) \land \neg y \in LSpan (R freeLMod I) (X)) \to \neg \{y\} \subseteq X$
31		nsspssun	$⊢ \neg \{y\} \subseteq X \leftrightarrow X \subset \{y\} \cup X$
32	30 31	sylib	$⊢ ((R \in DivRing \land I \in Fin \land X \in LIndS (R freeLMod I)) \land \neg y \in LSpan (R freeLMod I) (X)) \to X \subset \{y\} \cup X$
33		php3	$⊢ (\{y\} \cup X \in Fin \land X \subset \{y\} \cup X) \to X ≺ (\{y\} \cup X)$
34	22 32 33	syl2anc	$⊢ ((R \in DivRing \land I \in Fin \land X \in LIndS (R freeLMod I)) \land \neg y \in LSpan (R freeLMod I) (X)) \to X ≺ (\{y\} \cup X)$
35	34	adantrl	$⊢ ((R \in DivRing \land I \in Fin \land X \in LIndS (R freeLMod I)) \land (y \in {Base}_{(R freeLMod I)} \land \neg y \in LSpan (R freeLMod I) (X))) \to X ≺ (\{y\} \cup X)$
36		simpl1	$⊢ ((R \in DivRing \land I \in Fin \land X \in LIndS (R freeLMod I)) \land (y \in {Base}_{(R freeLMod I)} \land \neg y \in LSpan (R freeLMod I) (X))) \to R \in DivRing$
37		simpl2	$⊢ ((R \in DivRing \land I \in Fin \land X \in LIndS (R freeLMod I)) \land (y \in {Base}_{(R freeLMod I)} \land \neg y \in LSpan (R freeLMod I) (X))) \to I \in Fin$
38		snssi	$⊢ y \in {Base}_{(R freeLMod I)} \to \{y\} \subseteq {Base}_{(R freeLMod I)}$
39	38	adantr	$⊢ (y \in {Base}_{(R freeLMod I)} \land \neg y \in LSpan (R freeLMod I) (X)) \to \{y\} \subseteq {Base}_{(R freeLMod I)}$
40	7	3ad2ant3	$⊢ (R \in DivRing \land I \in Fin \land X \in LIndS (R freeLMod I)) \to X \subseteq {Base}_{(R freeLMod I)}$
41		unss	$⊢ (\{y\} \subseteq {Base}_{(R freeLMod I)} \land X \subseteq {Base}_{(R freeLMod I)}) \leftrightarrow \{y\} \cup X \subseteq {Base}_{(R freeLMod I)}$
42	41	biimpi	$⊢ (\{y\} \subseteq {Base}_{(R freeLMod I)} \land X \subseteq {Base}_{(R freeLMod I)}) \to \{y\} \cup X \subseteq {Base}_{(R freeLMod I)}$
43	39 40 42	syl2anr	$⊢ ((R \in DivRing \land I \in Fin \land X \in LIndS (R freeLMod I)) \land (y \in {Base}_{(R freeLMod I)} \land \neg y \in LSpan (R freeLMod I) (X))) \to \{y\} \cup X \subseteq {Base}_{(R freeLMod I)}$
44		simpr	$⊢ ((R \in DivRing \land I \in Fin \land X \in LIndS (R freeLMod I)) \land \neg y \in LSpan (R freeLMod I) (X)) \to \neg y \in LSpan (R freeLMod I) (X)$
45	28	con3dimp	$⊢ ((R \in DivRing \land I \in Fin \land X \in LIndS (R freeLMod I)) \land \neg y \in LSpan (R freeLMod I) (X)) \to \neg y \in X$
46		difsn	$⊢ \neg y \in X \to X ∖ \{y\} = X$
47	45 46	syl	$⊢ ((R \in DivRing \land I \in Fin \land X \in LIndS (R freeLMod I)) \land \neg y \in LSpan (R freeLMod I) (X)) \to X ∖ \{y\} = X$
48	47	fveq2d	$⊢ ((R \in DivRing \land I \in Fin \land X \in LIndS (R freeLMod I)) \land \neg y \in LSpan (R freeLMod I) (X)) \to LSpan (R freeLMod I) (X ∖ \{y\}) = LSpan (R freeLMod I) (X)$
49	44 48	neleqtrrd	$⊢ ((R \in DivRing \land I \in Fin \land X \in LIndS (R freeLMod I)) \land \neg y \in LSpan (R freeLMod I) (X)) \to \neg y \in LSpan (R freeLMod I) (X ∖ \{y\})$
50	49	adantlr	$⊢ (((R \in DivRing \land I \in Fin \land X \in LIndS (R freeLMod I)) \land y \in {Base}_{(R freeLMod I)}) \land \neg y \in LSpan (R freeLMod I) (X)) \to \neg y \in LSpan (R freeLMod I) (X ∖ \{y\})$
51		difsnid	$⊢ z \in X \to (X ∖ \{z\}) \cup \{z\} = X$
52	51	fveq2d	$⊢ z \in X \to LSpan (R freeLMod I) ((X ∖ \{z\}) \cup \{z\}) = LSpan (R freeLMod I) (X)$
53	52	eleq2d	$⊢ z \in X \to (y \in LSpan (R freeLMod I) ((X ∖ \{z\}) \cup \{z\}) \leftrightarrow y \in LSpan (R freeLMod I) (X))$
54	53	notbid	$⊢ z \in X \to (\neg y \in LSpan (R freeLMod I) ((X ∖ \{z\}) \cup \{z\}) \leftrightarrow \neg y \in LSpan (R freeLMod I) (X))$
55	54	biimparc	$⊢ (\neg y \in LSpan (R freeLMod I) (X) \land z \in X) \to \neg y \in LSpan (R freeLMod I) ((X ∖ \{z\}) \cup \{z\})$
56	55	adantll	$⊢ ((((R \in DivRing \land I \in Fin \land X \in LIndS (R freeLMod I)) \land y \in {Base}_{(R freeLMod I)}) \land \neg y \in LSpan (R freeLMod I) (X)) \land z \in X) \to \neg y \in LSpan (R freeLMod I) ((X ∖ \{z\}) \cup \{z\})$
57	3	frlmsca	$⊢ (R \in DivRing \land I \in Fin) \to R = Scalar (R freeLMod I)$
58		simpl	$⊢ (R \in DivRing \land I \in Fin) \to R \in DivRing$
59	57 58	eqeltrrd	$⊢ (R \in DivRing \land I \in Fin) \to Scalar (R freeLMod I) \in DivRing$
60		eqid	$⊢ Scalar (R freeLMod I) = Scalar (R freeLMod I)$
61	60	islvec	$⊢ R freeLMod I \in LVec \leftrightarrow (R freeLMod I \in LMod \land Scalar (R freeLMod I) \in DivRing)$
62	5 59 61	sylanbrc	$⊢ (R \in DivRing \land I \in Fin) \to R freeLMod I \in LVec$
63	62	3adant3	$⊢ (R \in DivRing \land I \in Fin \land X \in LIndS (R freeLMod I)) \to R freeLMod I \in LVec$
64	63	ad4antr	$⊢ (((((R \in DivRing \land I \in Fin \land X \in LIndS (R freeLMod I)) \land y \in {Base}_{(R freeLMod I)}) \land \neg y \in LSpan (R freeLMod I) (X)) \land z \in X) \land z \in LSpan (R freeLMod I) ((\{y\} \cup X) ∖ \{z\})) \to R freeLMod I \in LVec$
65	7	ssdifssd	$⊢ X \in LIndS (R freeLMod I) \to X ∖ \{z\} \subseteq {Base}_{(R freeLMod I)}$
66	65	3ad2ant3	$⊢ (R \in DivRing \land I \in Fin \land X \in LIndS (R freeLMod I)) \to X ∖ \{z\} \subseteq {Base}_{(R freeLMod I)}$
67	66	ad4antr	$⊢ (((((R \in DivRing \land I \in Fin \land X \in LIndS (R freeLMod I)) \land y \in {Base}_{(R freeLMod I)}) \land \neg y \in LSpan (R freeLMod I) (X)) \land z \in X) \land z \in LSpan (R freeLMod I) ((\{y\} \cup X) ∖ \{z\})) \to X ∖ \{z\} \subseteq {Base}_{(R freeLMod I)}$
68		simp-4r	$⊢ (((((R \in DivRing \land I \in Fin \land X \in LIndS (R freeLMod I)) \land y \in {Base}_{(R freeLMod I)}) \land \neg y \in LSpan (R freeLMod I) (X)) \land z \in X) \land z \in LSpan (R freeLMod I) ((\{y\} \cup X) ∖ \{z\})) \to y \in {Base}_{(R freeLMod I)}$
69		difundir	$⊢ (\{y\} \cup X) ∖ \{z\} = (\{y\} ∖ \{z\}) \cup (X ∖ \{z\})$
70	69	equncomi	$⊢ (\{y\} \cup X) ∖ \{z\} = (X ∖ \{z\}) \cup (\{y\} ∖ \{z\})$
71		elsni	$⊢ z \in \{y\} \to z = y$
72	71	eleq1d	$⊢ z \in \{y\} \to (z \in X \leftrightarrow y \in X)$
73	72	notbid	$⊢ z \in \{y\} \to (\neg z \in X \leftrightarrow \neg y \in X)$
74	45 73	syl5ibrcom	$⊢ ((R \in DivRing \land I \in Fin \land X \in LIndS (R freeLMod I)) \land \neg y \in LSpan (R freeLMod I) (X)) \to (z \in \{y\} \to \neg z \in X)$
75	74	con2d	$⊢ ((R \in DivRing \land I \in Fin \land X \in LIndS (R freeLMod I)) \land \neg y \in LSpan (R freeLMod I) (X)) \to (z \in X \to \neg z \in \{y\})$
76	75	imp	$⊢ (((R \in DivRing \land I \in Fin \land X \in LIndS (R freeLMod I)) \land \neg y \in LSpan (R freeLMod I) (X)) \land z \in X) \to \neg z \in \{y\}$
77		difsn	$⊢ \neg z \in \{y\} \to \{y\} ∖ \{z\} = \{y\}$
78	76 77	syl	$⊢ (((R \in DivRing \land I \in Fin \land X \in LIndS (R freeLMod I)) \land \neg y \in LSpan (R freeLMod I) (X)) \land z \in X) \to \{y\} ∖ \{z\} = \{y\}$
79	78	uneq2d	$⊢ (((R \in DivRing \land I \in Fin \land X \in LIndS (R freeLMod I)) \land \neg y \in LSpan (R freeLMod I) (X)) \land z \in X) \to (X ∖ \{z\}) \cup (\{y\} ∖ \{z\}) = (X ∖ \{z\}) \cup \{y\}$
80	70 79	eqtrid	$⊢ (((R \in DivRing \land I \in Fin \land X \in LIndS (R freeLMod I)) \land \neg y \in LSpan (R freeLMod I) (X)) \land z \in X) \to (\{y\} \cup X) ∖ \{z\} = (X ∖ \{z\}) \cup \{y\}$
81	80	fveq2d	$⊢ (((R \in DivRing \land I \in Fin \land X \in LIndS (R freeLMod I)) \land \neg y \in LSpan (R freeLMod I) (X)) \land z \in X) \to LSpan (R freeLMod I) ((\{y\} \cup X) ∖ \{z\}) = LSpan (R freeLMod I) ((X ∖ \{z\}) \cup \{y\})$
82	81	eleq2d	$⊢ (((R \in DivRing \land I \in Fin \land X \in LIndS (R freeLMod I)) \land \neg y \in LSpan (R freeLMod I) (X)) \land z \in X) \to (z \in LSpan (R freeLMod I) ((\{y\} \cup X) ∖ \{z\}) \leftrightarrow z \in LSpan (R freeLMod I) ((X ∖ \{z\}) \cup \{y\}))$
83	82	adantllr	$⊢ ((((R \in DivRing \land I \in Fin \land X \in LIndS (R freeLMod I)) \land y \in {Base}_{(R freeLMod I)}) \land \neg y \in LSpan (R freeLMod I) (X)) \land z \in X) \to (z \in LSpan (R freeLMod I) ((\{y\} \cup X) ∖ \{z\}) \leftrightarrow z \in LSpan (R freeLMod I) ((X ∖ \{z\}) \cup \{y\}))$
84	83	biimpa	$⊢ (((((R \in DivRing \land I \in Fin \land X \in LIndS (R freeLMod I)) \land y \in {Base}_{(R freeLMod I)}) \land \neg y \in LSpan (R freeLMod I) (X)) \land z \in X) \land z \in LSpan (R freeLMod I) ((\{y\} \cup X) ∖ \{z\})) \to z \in LSpan (R freeLMod I) ((X ∖ \{z\}) \cup \{y\})$
85		drngnzr	$⊢ R \in DivRing \to R \in NzRing$
86	85	adantr	$⊢ (R \in DivRing \land I \in Fin) \to R \in NzRing$
87	57 86	eqeltrrd	$⊢ (R \in DivRing \land I \in Fin) \to Scalar (R freeLMod I) \in NzRing$
88	5 87	jca	$⊢ (R \in DivRing \land I \in Fin) \to (R freeLMod I \in LMod \land Scalar (R freeLMod I) \in NzRing)$
89	88	anim1i	$⊢ ((R \in DivRing \land I \in Fin) \land X \in LIndS (R freeLMod I)) \to ((R freeLMod I \in LMod \land Scalar (R freeLMod I) \in NzRing) \land X \in LIndS (R freeLMod I))$
90	89	3impa	$⊢ (R \in DivRing \land I \in Fin \land X \in LIndS (R freeLMod I)) \to ((R freeLMod I \in LMod \land Scalar (R freeLMod I) \in NzRing) \land X \in LIndS (R freeLMod I))$
91	8 60	lindsind2	$⊢ ((R freeLMod I \in LMod \land Scalar (R freeLMod I) \in NzRing) \land X \in LIndS (R freeLMod I) \land z \in X) \to \neg z \in LSpan (R freeLMod I) (X ∖ \{z\})$
92	91	3expa	$⊢ (((R freeLMod I \in LMod \land Scalar (R freeLMod I) \in NzRing) \land X \in LIndS (R freeLMod I)) \land z \in X) \to \neg z \in LSpan (R freeLMod I) (X ∖ \{z\})$
93	90 92	sylan	$⊢ ((R \in DivRing \land I \in Fin \land X \in LIndS (R freeLMod I)) \land z \in X) \to \neg z \in LSpan (R freeLMod I) (X ∖ \{z\})$
94	93	ad5ant14	$⊢ (((((R \in DivRing \land I \in Fin \land X \in LIndS (R freeLMod I)) \land y \in {Base}_{(R freeLMod I)}) \land \neg y \in LSpan (R freeLMod I) (X)) \land z \in X) \land z \in LSpan (R freeLMod I) ((\{y\} \cup X) ∖ \{z\})) \to \neg z \in LSpan (R freeLMod I) (X ∖ \{z\})$
95	84 94	eldifd	$⊢ (((((R \in DivRing \land I \in Fin \land X \in LIndS (R freeLMod I)) \land y \in {Base}_{(R freeLMod I)}) \land \neg y \in LSpan (R freeLMod I) (X)) \land z \in X) \land z \in LSpan (R freeLMod I) ((\{y\} \cup X) ∖ \{z\})) \to z \in (LSpan (R freeLMod I) ((X ∖ \{z\}) \cup \{y\}) ∖ LSpan (R freeLMod I) (X ∖ \{z\}))$
96		eqid	$⊢ LSubSp (R freeLMod I) = LSubSp (R freeLMod I)$
97	6 96 8	lspsolv	$⊢ (R freeLMod I \in LVec \land (X ∖ \{z\} \subseteq {Base}_{(R freeLMod I)} \land y \in {Base}_{(R freeLMod I)} \land z \in (LSpan (R freeLMod I) ((X ∖ \{z\}) \cup \{y\}) ∖ LSpan (R freeLMod I) (X ∖ \{z\})))) \to y \in LSpan (R freeLMod I) ((X ∖ \{z\}) \cup \{z\})$
98	64 67 68 95 97	syl13anc	$⊢ (((((R \in DivRing \land I \in Fin \land X \in LIndS (R freeLMod I)) \land y \in {Base}_{(R freeLMod I)}) \land \neg y \in LSpan (R freeLMod I) (X)) \land z \in X) \land z \in LSpan (R freeLMod I) ((\{y\} \cup X) ∖ \{z\})) \to y \in LSpan (R freeLMod I) ((X ∖ \{z\}) \cup \{z\})$
99	56 98	mtand	$⊢ ((((R \in DivRing \land I \in Fin \land X \in LIndS (R freeLMod I)) \land y \in {Base}_{(R freeLMod I)}) \land \neg y \in LSpan (R freeLMod I) (X)) \land z \in X) \to \neg z \in LSpan (R freeLMod I) ((\{y\} \cup X) ∖ \{z\})$
100	99	ralrimiva	$⊢ (((R \in DivRing \land I \in Fin \land X \in LIndS (R freeLMod I)) \land y \in {Base}_{(R freeLMod I)}) \land \neg y \in LSpan (R freeLMod I) (X)) \to \forall z \in X \neg z \in LSpan (R freeLMod I) ((\{y\} \cup X) ∖ \{z\})$
101		ralunb	$⊢ \forall z \in (\{y\} \cup X) \neg z \in LSpan (R freeLMod I) ((\{y\} \cup X) ∖ \{z\}) \leftrightarrow (\forall z \in \{y\} \neg z \in LSpan (R freeLMod I) ((\{y\} \cup X) ∖ \{z\}) \land \forall z \in X \neg z \in LSpan (R freeLMod I) ((\{y\} \cup X) ∖ \{z\}))$
102		id	$⊢ z = y \to z = y$
103		sneq	$⊢ z = y \to \{z\} = \{y\}$
104	103	difeq2d	$⊢ z = y \to (\{y\} \cup X) ∖ \{z\} = (\{y\} \cup X) ∖ \{y\}$
105		uncom	$⊢ \{y\} \cup X = X \cup \{y\}$
106	105	difeq1i	$⊢ (\{y\} \cup X) ∖ \{y\} = (X \cup \{y\}) ∖ \{y\}$
107		difun2	$⊢ (X \cup \{y\}) ∖ \{y\} = X ∖ \{y\}$
108	106 107	eqtri	$⊢ (\{y\} \cup X) ∖ \{y\} = X ∖ \{y\}$
109	104 108	eqtrdi	$⊢ z = y \to (\{y\} \cup X) ∖ \{z\} = X ∖ \{y\}$
110	109	fveq2d	$⊢ z = y \to LSpan (R freeLMod I) ((\{y\} \cup X) ∖ \{z\}) = LSpan (R freeLMod I) (X ∖ \{y\})$
111	102 110	eleq12d	$⊢ z = y \to (z \in LSpan (R freeLMod I) ((\{y\} \cup X) ∖ \{z\}) \leftrightarrow y \in LSpan (R freeLMod I) (X ∖ \{y\}))$
112	111	notbid	$⊢ z = y \to (\neg z \in LSpan (R freeLMod I) ((\{y\} \cup X) ∖ \{z\}) \leftrightarrow \neg y \in LSpan (R freeLMod I) (X ∖ \{y\}))$
113	23 112	ralsn	$⊢ \forall z \in \{y\} \neg z \in LSpan (R freeLMod I) ((\{y\} \cup X) ∖ \{z\}) \leftrightarrow \neg y \in LSpan (R freeLMod I) (X ∖ \{y\})$
114	113	anbi1i	$⊢ (\forall z \in \{y\} \neg z \in LSpan (R freeLMod I) ((\{y\} \cup X) ∖ \{z\}) \land \forall z \in X \neg z \in LSpan (R freeLMod I) ((\{y\} \cup X) ∖ \{z\})) \leftrightarrow (\neg y \in LSpan (R freeLMod I) (X ∖ \{y\}) \land \forall z \in X \neg z \in LSpan (R freeLMod I) ((\{y\} \cup X) ∖ \{z\}))$
115	101 114	bitri	$⊢ \forall z \in (\{y\} \cup X) \neg z \in LSpan (R freeLMod I) ((\{y\} \cup X) ∖ \{z\}) \leftrightarrow (\neg y \in LSpan (R freeLMod I) (X ∖ \{y\}) \land \forall z \in X \neg z \in LSpan (R freeLMod I) ((\{y\} \cup X) ∖ \{z\}))$
116	50 100 115	sylanbrc	$⊢ (((R \in DivRing \land I \in Fin \land X \in LIndS (R freeLMod I)) \land y \in {Base}_{(R freeLMod I)}) \land \neg y \in LSpan (R freeLMod I) (X)) \to \forall z \in (\{y\} \cup X) \neg z \in LSpan (R freeLMod I) ((\{y\} \cup X) ∖ \{z\})$
117	116	ex	$⊢ ((R \in DivRing \land I \in Fin \land X \in LIndS (R freeLMod I)) \land y \in {Base}_{(R freeLMod I)}) \to (\neg y \in LSpan (R freeLMod I) (X) \to \forall z \in (\{y\} \cup X) \neg z \in LSpan (R freeLMod I) ((\{y\} \cup X) ∖ \{z\}))$
118	63	ad3antrrr	$⊢ ((((R \in DivRing \land I \in Fin \land X \in LIndS (R freeLMod I)) \land y \in {Base}_{(R freeLMod I)}) \land z \in (\{y\} \cup X)) \land x \in ({Base}_{Scalar (R freeLMod I)} ∖ \{0_{Scalar (R freeLMod I)}\})) \to R freeLMod I \in LVec$
119		eldifsn	$⊢ x \in ({Base}_{Scalar (R freeLMod I)} ∖ \{0_{Scalar (R freeLMod I)}\}) \leftrightarrow (x \in {Base}_{Scalar (R freeLMod I)} \land x \neq 0_{Scalar (R freeLMod I)})$
120	119	biimpi	$⊢ x \in ({Base}_{Scalar (R freeLMod I)} ∖ \{0_{Scalar (R freeLMod I)}\}) \to (x \in {Base}_{Scalar (R freeLMod I)} \land x \neq 0_{Scalar (R freeLMod I)})$
121	120	adantl	$⊢ ((((R \in DivRing \land I \in Fin \land X \in LIndS (R freeLMod I)) \land y \in {Base}_{(R freeLMod I)}) \land z \in (\{y\} \cup X)) \land x \in ({Base}_{Scalar (R freeLMod I)} ∖ \{0_{Scalar (R freeLMod I)}\})) \to (x \in {Base}_{Scalar (R freeLMod I)} \land x \neq 0_{Scalar (R freeLMod I)})$
122	38 7 42	syl2anr	$⊢ (X \in LIndS (R freeLMod I) \land y \in {Base}_{(R freeLMod I)}) \to \{y\} \cup X \subseteq {Base}_{(R freeLMod I)}$
123	122	3ad2antl3	$⊢ ((R \in DivRing \land I \in Fin \land X \in LIndS (R freeLMod I)) \land y \in {Base}_{(R freeLMod I)}) \to \{y\} \cup X \subseteq {Base}_{(R freeLMod I)}$
124	123	sselda	$⊢ (((R \in DivRing \land I \in Fin \land X \in LIndS (R freeLMod I)) \land y \in {Base}_{(R freeLMod I)}) \land z \in (\{y\} \cup X)) \to z \in {Base}_{(R freeLMod I)}$
125	124	adantr	$⊢ ((((R \in DivRing \land I \in Fin \land X \in LIndS (R freeLMod I)) \land y \in {Base}_{(R freeLMod I)}) \land z \in (\{y\} \cup X)) \land x \in ({Base}_{Scalar (R freeLMod I)} ∖ \{0_{Scalar (R freeLMod I)}\})) \to z \in {Base}_{(R freeLMod I)}$
126		eqid	$⊢ \cdot_{(R freeLMod I)} = \cdot_{(R freeLMod I)}$
127		eqid	$⊢ {Base}_{Scalar (R freeLMod I)} = {Base}_{Scalar (R freeLMod I)}$
128		eqid	$⊢ 0_{Scalar (R freeLMod I)} = 0_{Scalar (R freeLMod I)}$
129	6 60 126 127 128 8	lspsnvs	$⊢ (R freeLMod I \in LVec \land (x \in {Base}_{Scalar (R freeLMod I)} \land x \neq 0_{Scalar (R freeLMod I)}) \land z \in {Base}_{(R freeLMod I)}) \to LSpan (R freeLMod I) (\{x \cdot_{(R freeLMod I)} z\}) = LSpan (R freeLMod I) (\{z\})$
130	118 121 125 129	syl3anc	$⊢ ((((R \in DivRing \land I \in Fin \land X \in LIndS (R freeLMod I)) \land y \in {Base}_{(R freeLMod I)}) \land z \in (\{y\} \cup X)) \land x \in ({Base}_{Scalar (R freeLMod I)} ∖ \{0_{Scalar (R freeLMod I)}\})) \to LSpan (R freeLMod I) (\{x \cdot_{(R freeLMod I)} z\}) = LSpan (R freeLMod I) (\{z\})$
131	130	sseq1d	$⊢ ((((R \in DivRing \land I \in Fin \land X \in LIndS (R freeLMod I)) \land y \in {Base}_{(R freeLMod I)}) \land z \in (\{y\} \cup X)) \land x \in ({Base}_{Scalar (R freeLMod I)} ∖ \{0_{Scalar (R freeLMod I)}\})) \to (LSpan (R freeLMod I) (\{x \cdot_{(R freeLMod I)} z\}) \subseteq LSpan (R freeLMod I) ((\{y\} \cup X) ∖ \{z\}) \leftrightarrow LSpan (R freeLMod I) (\{z\}) \subseteq LSpan (R freeLMod I) ((\{y\} \cup X) ∖ \{z\}))$
132	5	3adant3	$⊢ (R \in DivRing \land I \in Fin \land X \in LIndS (R freeLMod I)) \to R freeLMod I \in LMod$
133	132	ad3antrrr	$⊢ ((((R \in DivRing \land I \in Fin \land X \in LIndS (R freeLMod I)) \land y \in {Base}_{(R freeLMod I)}) \land z \in (\{y\} \cup X)) \land x \in ({Base}_{Scalar (R freeLMod I)} ∖ \{0_{Scalar (R freeLMod I)}\})) \to R freeLMod I \in LMod$
134		df-3an	$⊢ (R \in DivRing \land I \in Fin \land X \in LIndS (R freeLMod I)) \leftrightarrow ((R \in DivRing \land I \in Fin) \land X \in LIndS (R freeLMod I))$
135	122	ssdifssd	$⊢ (X \in LIndS (R freeLMod I) \land y \in {Base}_{(R freeLMod I)}) \to (\{y\} \cup X) ∖ \{z\} \subseteq {Base}_{(R freeLMod I)}$
136	6 96 8	lspcl	$⊢ (R freeLMod I \in LMod \land (\{y\} \cup X) ∖ \{z\} \subseteq {Base}_{(R freeLMod I)}) \to LSpan (R freeLMod I) ((\{y\} \cup X) ∖ \{z\}) \in LSubSp (R freeLMod I)$
137	5 135 136	syl2an	$⊢ ((R \in DivRing \land I \in Fin) \land (X \in LIndS (R freeLMod I) \land y \in {Base}_{(R freeLMod I)})) \to LSpan (R freeLMod I) ((\{y\} \cup X) ∖ \{z\}) \in LSubSp (R freeLMod I)$
138	137	anassrs	$⊢ (((R \in DivRing \land I \in Fin) \land X \in LIndS (R freeLMod I)) \land y \in {Base}_{(R freeLMod I)}) \to LSpan (R freeLMod I) ((\{y\} \cup X) ∖ \{z\}) \in LSubSp (R freeLMod I)$
139	134 138	sylanb	$⊢ ((R \in DivRing \land I \in Fin \land X \in LIndS (R freeLMod I)) \land y \in {Base}_{(R freeLMod I)}) \to LSpan (R freeLMod I) ((\{y\} \cup X) ∖ \{z\}) \in LSubSp (R freeLMod I)$
140	139	ad2antrr	$⊢ ((((R \in DivRing \land I \in Fin \land X \in LIndS (R freeLMod I)) \land y \in {Base}_{(R freeLMod I)}) \land z \in (\{y\} \cup X)) \land x \in ({Base}_{Scalar (R freeLMod I)} ∖ \{0_{Scalar (R freeLMod I)}\})) \to LSpan (R freeLMod I) ((\{y\} \cup X) ∖ \{z\}) \in LSubSp (R freeLMod I)$
141		eldifi	$⊢ x \in ({Base}_{Scalar (R freeLMod I)} ∖ \{0_{Scalar (R freeLMod I)}\}) \to x \in {Base}_{Scalar (R freeLMod I)}$
142	141	adantl	$⊢ ((((R \in DivRing \land I \in Fin \land X \in LIndS (R freeLMod I)) \land y \in {Base}_{(R freeLMod I)}) \land z \in (\{y\} \cup X)) \land x \in ({Base}_{Scalar (R freeLMod I)} ∖ \{0_{Scalar (R freeLMod I)}\})) \to x \in {Base}_{Scalar (R freeLMod I)}$
143	6 60 126 127	lmodvscl	$⊢ (R freeLMod I \in LMod \land x \in {Base}_{Scalar (R freeLMod I)} \land z \in {Base}_{(R freeLMod I)}) \to x \cdot_{(R freeLMod I)} z \in {Base}_{(R freeLMod I)}$
144	133 142 125 143	syl3anc	$⊢ ((((R \in DivRing \land I \in Fin \land X \in LIndS (R freeLMod I)) \land y \in {Base}_{(R freeLMod I)}) \land z \in (\{y\} \cup X)) \land x \in ({Base}_{Scalar (R freeLMod I)} ∖ \{0_{Scalar (R freeLMod I)}\})) \to x \cdot_{(R freeLMod I)} z \in {Base}_{(R freeLMod I)}$
145	6 96 8 133 140 144	ellspsn5b	$⊢ ((((R \in DivRing \land I \in Fin \land X \in LIndS (R freeLMod I)) \land y \in {Base}_{(R freeLMod I)}) \land z \in (\{y\} \cup X)) \land x \in ({Base}_{Scalar (R freeLMod I)} ∖ \{0_{Scalar (R freeLMod I)}\})) \to (x \cdot_{(R freeLMod I)} z \in LSpan (R freeLMod I) ((\{y\} \cup X) ∖ \{z\}) \leftrightarrow LSpan (R freeLMod I) (\{x \cdot_{(R freeLMod I)} z\}) \subseteq LSpan (R freeLMod I) ((\{y\} \cup X) ∖ \{z\}))$
146	132	ad2antrr	$⊢ (((R \in DivRing \land I \in Fin \land X \in LIndS (R freeLMod I)) \land y \in {Base}_{(R freeLMod I)}) \land z \in (\{y\} \cup X)) \to R freeLMod I \in LMod$
147	139	adantr	$⊢ (((R \in DivRing \land I \in Fin \land X \in LIndS (R freeLMod I)) \land y \in {Base}_{(R freeLMod I)}) \land z \in (\{y\} \cup X)) \to LSpan (R freeLMod I) ((\{y\} \cup X) ∖ \{z\}) \in LSubSp (R freeLMod I)$
148	6 96 8 146 147 124	ellspsn5b	$⊢ (((R \in DivRing \land I \in Fin \land X \in LIndS (R freeLMod I)) \land y \in {Base}_{(R freeLMod I)}) \land z \in (\{y\} \cup X)) \to (z \in LSpan (R freeLMod I) ((\{y\} \cup X) ∖ \{z\}) \leftrightarrow LSpan (R freeLMod I) (\{z\}) \subseteq LSpan (R freeLMod I) ((\{y\} \cup X) ∖ \{z\}))$
149	148	adantr	$⊢ ((((R \in DivRing \land I \in Fin \land X \in LIndS (R freeLMod I)) \land y \in {Base}_{(R freeLMod I)}) \land z \in (\{y\} \cup X)) \land x \in ({Base}_{Scalar (R freeLMod I)} ∖ \{0_{Scalar (R freeLMod I)}\})) \to (z \in LSpan (R freeLMod I) ((\{y\} \cup X) ∖ \{z\}) \leftrightarrow LSpan (R freeLMod I) (\{z\}) \subseteq LSpan (R freeLMod I) ((\{y\} \cup X) ∖ \{z\}))$
150	131 145 149	3bitr4rd	$⊢ ((((R \in DivRing \land I \in Fin \land X \in LIndS (R freeLMod I)) \land y \in {Base}_{(R freeLMod I)}) \land z \in (\{y\} \cup X)) \land x \in ({Base}_{Scalar (R freeLMod I)} ∖ \{0_{Scalar (R freeLMod I)}\})) \to (z \in LSpan (R freeLMod I) ((\{y\} \cup X) ∖ \{z\}) \leftrightarrow x \cdot_{(R freeLMod I)} z \in LSpan (R freeLMod I) ((\{y\} \cup X) ∖ \{z\}))$
151	150	notbid	$⊢ ((((R \in DivRing \land I \in Fin \land X \in LIndS (R freeLMod I)) \land y \in {Base}_{(R freeLMod I)}) \land z \in (\{y\} \cup X)) \land x \in ({Base}_{Scalar (R freeLMod I)} ∖ \{0_{Scalar (R freeLMod I)}\})) \to (\neg z \in LSpan (R freeLMod I) ((\{y\} \cup X) ∖ \{z\}) \leftrightarrow \neg x \cdot_{(R freeLMod I)} z \in LSpan (R freeLMod I) ((\{y\} \cup X) ∖ \{z\}))$
152	151	biimpd	$⊢ ((((R \in DivRing \land I \in Fin \land X \in LIndS (R freeLMod I)) \land y \in {Base}_{(R freeLMod I)}) \land z \in (\{y\} \cup X)) \land x \in ({Base}_{Scalar (R freeLMod I)} ∖ \{0_{Scalar (R freeLMod I)}\})) \to (\neg z \in LSpan (R freeLMod I) ((\{y\} \cup X) ∖ \{z\}) \to \neg x \cdot_{(R freeLMod I)} z \in LSpan (R freeLMod I) ((\{y\} \cup X) ∖ \{z\}))$
153	152	ralrimdva	$⊢ (((R \in DivRing \land I \in Fin \land X \in LIndS (R freeLMod I)) \land y \in {Base}_{(R freeLMod I)}) \land z \in (\{y\} \cup X)) \to (\neg z \in LSpan (R freeLMod I) ((\{y\} \cup X) ∖ \{z\}) \to \forall x \in ({Base}_{Scalar (R freeLMod I)} ∖ \{0_{Scalar (R freeLMod I)}\}) \neg x \cdot_{(R freeLMod I)} z \in LSpan (R freeLMod I) ((\{y\} \cup X) ∖ \{z\}))$
154	153	ralimdva	$⊢ ((R \in DivRing \land I \in Fin \land X \in LIndS (R freeLMod I)) \land y \in {Base}_{(R freeLMod I)}) \to (\forall z \in (\{y\} \cup X) \neg z \in LSpan (R freeLMod I) ((\{y\} \cup X) ∖ \{z\}) \to \forall z \in (\{y\} \cup X) \forall x \in ({Base}_{Scalar (R freeLMod I)} ∖ \{0_{Scalar (R freeLMod I)}\}) \neg x \cdot_{(R freeLMod I)} z \in LSpan (R freeLMod I) ((\{y\} \cup X) ∖ \{z\}))$
155	117 154	syld	$⊢ ((R \in DivRing \land I \in Fin \land X \in LIndS (R freeLMod I)) \land y \in {Base}_{(R freeLMod I)}) \to (\neg y \in LSpan (R freeLMod I) (X) \to \forall z \in (\{y\} \cup X) \forall x \in ({Base}_{Scalar (R freeLMod I)} ∖ \{0_{Scalar (R freeLMod I)}\}) \neg x \cdot_{(R freeLMod I)} z \in LSpan (R freeLMod I) ((\{y\} \cup X) ∖ \{z\}))$
156	155	impr	$⊢ ((R \in DivRing \land I \in Fin \land X \in LIndS (R freeLMod I)) \land (y \in {Base}_{(R freeLMod I)} \land \neg y \in LSpan (R freeLMod I) (X))) \to \forall z \in (\{y\} \cup X) \forall x \in ({Base}_{Scalar (R freeLMod I)} ∖ \{0_{Scalar (R freeLMod I)}\}) \neg x \cdot_{(R freeLMod I)} z \in LSpan (R freeLMod I) ((\{y\} \cup X) ∖ \{z\})$
157		ovex	$⊢ R freeLMod I \in V$
158	6 126 8 60 127 128	islinds2	$⊢ R freeLMod I \in V \to (\{y\} \cup X \in LIndS (R freeLMod I) \leftrightarrow (\{y\} \cup X \subseteq {Base}_{(R freeLMod I)} \land \forall z \in (\{y\} \cup X) \forall x \in ({Base}_{Scalar (R freeLMod I)} ∖ \{0_{Scalar (R freeLMod I)}\}) \neg x \cdot_{(R freeLMod I)} z \in LSpan (R freeLMod I) ((\{y\} \cup X) ∖ \{z\})))$
159	157 158	ax-mp	$⊢ \{y\} \cup X \in LIndS (R freeLMod I) \leftrightarrow (\{y\} \cup X \subseteq {Base}_{(R freeLMod I)} \land \forall z \in (\{y\} \cup X) \forall x \in ({Base}_{Scalar (R freeLMod I)} ∖ \{0_{Scalar (R freeLMod I)}\}) \neg x \cdot_{(R freeLMod I)} z \in LSpan (R freeLMod I) ((\{y\} \cup X) ∖ \{z\}))$
160	43 156 159	sylanbrc	$⊢ ((R \in DivRing \land I \in Fin \land X \in LIndS (R freeLMod I)) \land (y \in {Base}_{(R freeLMod I)} \land \neg y \in LSpan (R freeLMod I) (X))) \to \{y\} \cup X \in LIndS (R freeLMod I)$
161		lindsdom	$⊢ (R \in DivRing \land I \in Fin \land \{y\} \cup X \in LIndS (R freeLMod I)) \to (\{y\} \cup X) ≼ I$
162	36 37 160 161	syl3anc	$⊢ ((R \in DivRing \land I \in Fin \land X \in LIndS (R freeLMod I)) \land (y \in {Base}_{(R freeLMod I)} \land \neg y \in LSpan (R freeLMod I) (X))) \to (\{y\} \cup X) ≼ I$
163		sdomdomtr	$⊢ (X ≺ (\{y\} \cup X) \land (\{y\} \cup X) ≼ I) \to X ≺ I$
164	35 162 163	syl2anc	$⊢ ((R \in DivRing \land I \in Fin \land X \in LIndS (R freeLMod I)) \land (y \in {Base}_{(R freeLMod I)} \land \neg y \in LSpan (R freeLMod I) (X))) \to X ≺ I$
165	164	stoic1a	$⊢ ((R \in DivRing \land I \in Fin \land X \in LIndS (R freeLMod I)) \land \neg X ≺ I) \to \neg (y \in {Base}_{(R freeLMod I)} \land \neg y \in LSpan (R freeLMod I) (X))$
166	14 165	sylan2	$⊢ ((R \in DivRing \land I \in Fin \land X \in LIndS (R freeLMod I)) \land X \approx I) \to \neg (y \in {Base}_{(R freeLMod I)} \land \neg y \in LSpan (R freeLMod I) (X))$
167		iman	$⊢ (y \in {Base}_{(R freeLMod I)} \to y \in LSpan (R freeLMod I) (X)) \leftrightarrow \neg (y \in {Base}_{(R freeLMod I)} \land \neg y \in LSpan (R freeLMod I) (X))$
168	166 167	sylibr	$⊢ ((R \in DivRing \land I \in Fin \land X \in LIndS (R freeLMod I)) \land X \approx I) \to (y \in {Base}_{(R freeLMod I)} \to y \in LSpan (R freeLMod I) (X))$
169	168	ssrdv	$⊢ ((R \in DivRing \land I \in Fin \land X \in LIndS (R freeLMod I)) \land X \approx I) \to {Base}_{(R freeLMod I)} \subseteq LSpan (R freeLMod I) (X)$
170	12 169	eqssd	$⊢ ((R \in DivRing \land I \in Fin \land X \in LIndS (R freeLMod I)) \land X \approx I) \to LSpan (R freeLMod I) (X) = {Base}_{(R freeLMod I)}$
171		eqid	$⊢ LBasis (R freeLMod I) = LBasis (R freeLMod I)$
172	6 171 8	islbs4	$⊢ X \in LBasis (R freeLMod I) \leftrightarrow (X \in LIndS (R freeLMod I) \land LSpan (R freeLMod I) (X) = {Base}_{(R freeLMod I)})$
173	1 170 172	sylanbrc	$⊢ ((R \in DivRing \land I \in Fin \land X \in LIndS (R freeLMod I)) \land X \approx I) \to X \in LBasis (R freeLMod I)$

Metamath Proof Explorer

Theorem lindsenlbs

Proof