lindsdom

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

		Ref	Expression
	Assertion	lindsdom	$⊢ (R \in DivRing \land I \in Fin \land X \in LIndS (R freeLMod I)) \to X ≼ I$

Proof

Step	Hyp	Ref	Expression
1		drngring	$⊢ R \in DivRing \to R \in Ring$
2		eqid	$⊢ R freeLMod I = R freeLMod I$
3	2	frlmlmod	$⊢ (R \in Ring \land I \in Fin) \to R freeLMod I \in LMod$
4	1 3	sylan	$⊢ (R \in DivRing \land I \in Fin) \to R freeLMod I \in LMod$
5		eqid	$⊢ {Base}_{(R freeLMod I)} = {Base}_{(R freeLMod I)}$
6		eqid	$⊢ LSubSp (R freeLMod I) = LSubSp (R freeLMod I)$
7	5 6	lssmre	$⊢ R freeLMod I \in LMod \to LSubSp (R freeLMod I) \in Moore ({Base}_{(R freeLMod I)})$
8	4 7	syl	$⊢ (R \in DivRing \land I \in Fin) \to LSubSp (R freeLMod I) \in Moore ({Base}_{(R freeLMod I)})$
9	8	3adant3	$⊢ (R \in DivRing \land I \in Fin \land X \in LIndS (R freeLMod I)) \to LSubSp (R freeLMod I) \in Moore ({Base}_{(R freeLMod I)})$
10		eqid	$⊢ mrCls (LSubSp (R freeLMod I)) = mrCls (LSubSp (R freeLMod I))$
11		eqid	$⊢ mrInd (LSubSp (R freeLMod I)) = mrInd (LSubSp (R freeLMod I))$
12	2	frlmsca	$⊢ (R \in DivRing \land I \in Fin) \to R = Scalar (R freeLMod I)$
13		simpl	$⊢ (R \in DivRing \land I \in Fin) \to R \in DivRing$
14	12 13	eqeltrrd	$⊢ (R \in DivRing \land I \in Fin) \to Scalar (R freeLMod I) \in DivRing$
15		eqid	$⊢ Scalar (R freeLMod I) = Scalar (R freeLMod I)$
16	15	islvec	$⊢ R freeLMod I \in LVec \leftrightarrow (R freeLMod I \in LMod \land Scalar (R freeLMod I) \in DivRing)$
17	4 14 16	sylanbrc	$⊢ (R \in DivRing \land I \in Fin) \to R freeLMod I \in LVec$
18	6 10 5	lssacsex	$⊢ R freeLMod I \in LVec \to (LSubSp (R freeLMod I) \in ACS ({Base}_{(R freeLMod I)}) \land \forall x \in 𝒫 {Base}_{(R freeLMod I)} \forall y \in {Base}_{(R freeLMod I)} \forall z \in (mrCls (LSubSp (R freeLMod I)) (x \cup \{y\}) ∖ mrCls (LSubSp (R freeLMod I)) (x)) y \in mrCls (LSubSp (R freeLMod I)) (x \cup \{z\}))$
19	17 18	syl	$⊢ (R \in DivRing \land I \in Fin) \to (LSubSp (R freeLMod I) \in ACS ({Base}_{(R freeLMod I)}) \land \forall x \in 𝒫 {Base}_{(R freeLMod I)} \forall y \in {Base}_{(R freeLMod I)} \forall z \in (mrCls (LSubSp (R freeLMod I)) (x \cup \{y\}) ∖ mrCls (LSubSp (R freeLMod I)) (x)) y \in mrCls (LSubSp (R freeLMod I)) (x \cup \{z\}))$
20	19	simprd	$⊢ (R \in DivRing \land I \in Fin) \to \forall x \in 𝒫 {Base}_{(R freeLMod I)} \forall y \in {Base}_{(R freeLMod I)} \forall z \in (mrCls (LSubSp (R freeLMod I)) (x \cup \{y\}) ∖ mrCls (LSubSp (R freeLMod I)) (x)) y \in mrCls (LSubSp (R freeLMod I)) (x \cup \{z\})$
21	20	3adant3	$⊢ (R \in DivRing \land I \in Fin \land X \in LIndS (R freeLMod I)) \to \forall x \in 𝒫 {Base}_{(R freeLMod I)} \forall y \in {Base}_{(R freeLMod I)} \forall z \in (mrCls (LSubSp (R freeLMod I)) (x \cup \{y\}) ∖ mrCls (LSubSp (R freeLMod I)) (x)) y \in mrCls (LSubSp (R freeLMod I)) (x \cup \{z\})$
22		dif0	$⊢ {Base}_{(R freeLMod I)} ∖ \emptyset = {Base}_{(R freeLMod I)}$
23	22	linds1	$⊢ X \in LIndS (R freeLMod I) \to X \subseteq {Base}_{(R freeLMod I)} ∖ \emptyset$
24	23	3ad2ant3	$⊢ (R \in DivRing \land I \in Fin \land X \in LIndS (R freeLMod I)) \to X \subseteq {Base}_{(R freeLMod I)} ∖ \emptyset$
25		eqid	$⊢ R unitVec I = R unitVec I$
26	25 2 5	uvcff	$⊢ (R \in Ring \land I \in Fin) \to (R unitVec I) : I ⟶ {Base}_{(R freeLMod I)}$
27	1 26	sylan	$⊢ (R \in DivRing \land I \in Fin) \to (R unitVec I) : I ⟶ {Base}_{(R freeLMod I)}$
28	27	frnd	$⊢ (R \in DivRing \land I \in Fin) \to ran (R unitVec I) \subseteq {Base}_{(R freeLMod I)}$
29	28 22	sseqtrrdi	$⊢ (R \in DivRing \land I \in Fin) \to ran (R unitVec I) \subseteq {Base}_{(R freeLMod I)} ∖ \emptyset$
30	29	3adant3	$⊢ (R \in DivRing \land I \in Fin \land X \in LIndS (R freeLMod I)) \to ran (R unitVec I) \subseteq {Base}_{(R freeLMod I)} ∖ \emptyset$
31	5	linds1	$⊢ X \in LIndS (R freeLMod I) \to X \subseteq {Base}_{(R freeLMod I)}$
32	31	3ad2ant3	$⊢ (R \in DivRing \land I \in Fin \land X \in LIndS (R freeLMod I)) \to X \subseteq {Base}_{(R freeLMod I)}$
33		un0	$⊢ ran (R unitVec I) \cup \emptyset = ran (R unitVec I)$
34	33	fveq2i	$⊢ mrCls (LSubSp (R freeLMod I)) (ran (R unitVec I) \cup \emptyset) = mrCls (LSubSp (R freeLMod I)) (ran (R unitVec I))$
35		eqid	$⊢ LSpan (R freeLMod I) = LSpan (R freeLMod I)$
36	6 35 10	mrclsp	$⊢ R freeLMod I \in LMod \to LSpan (R freeLMod I) = mrCls (LSubSp (R freeLMod I))$
37	4 36	syl	$⊢ (R \in DivRing \land I \in Fin) \to LSpan (R freeLMod I) = mrCls (LSubSp (R freeLMod I))$
38	37	fveq1d	$⊢ (R \in DivRing \land I \in Fin) \to LSpan (R freeLMod I) (ran (R unitVec I)) = mrCls (LSubSp (R freeLMod I)) (ran (R unitVec I))$
39		eqid	$⊢ LBasis (R freeLMod I) = LBasis (R freeLMod I)$
40	2 25 39	frlmlbs	$⊢ (R \in Ring \land I \in Fin) \to ran (R unitVec I) \in LBasis (R freeLMod I)$
41	1 40	sylan	$⊢ (R \in DivRing \land I \in Fin) \to ran (R unitVec I) \in LBasis (R freeLMod I)$
42	5 39 35	lbssp	$⊢ ran (R unitVec I) \in LBasis (R freeLMod I) \to LSpan (R freeLMod I) (ran (R unitVec I)) = {Base}_{(R freeLMod I)}$
43	41 42	syl	$⊢ (R \in DivRing \land I \in Fin) \to LSpan (R freeLMod I) (ran (R unitVec I)) = {Base}_{(R freeLMod I)}$
44	38 43	eqtr3d	$⊢ (R \in DivRing \land I \in Fin) \to mrCls (LSubSp (R freeLMod I)) (ran (R unitVec I)) = {Base}_{(R freeLMod I)}$
45	34 44	syl5eq	$⊢ (R \in DivRing \land I \in Fin) \to mrCls (LSubSp (R freeLMod I)) (ran (R unitVec I) \cup \emptyset) = {Base}_{(R freeLMod I)}$
46	45	3adant3	$⊢ (R \in DivRing \land I \in Fin \land X \in LIndS (R freeLMod I)) \to mrCls (LSubSp (R freeLMod I)) (ran (R unitVec I) \cup \emptyset) = {Base}_{(R freeLMod I)}$
47	32 46	sseqtrrd	$⊢ (R \in DivRing \land I \in Fin \land X \in LIndS (R freeLMod I)) \to X \subseteq mrCls (LSubSp (R freeLMod I)) (ran (R unitVec I) \cup \emptyset)$
48		un0	$⊢ X \cup \emptyset = X$
49		drngnzr	$⊢ R \in DivRing \to R \in NzRing$
50	49	adantr	$⊢ (R \in DivRing \land I \in Fin) \to R \in NzRing$
51	12 50	eqeltrrd	$⊢ (R \in DivRing \land I \in Fin) \to Scalar (R freeLMod I) \in NzRing$
52	4 51	jca	$⊢ (R \in DivRing \land I \in Fin) \to (R freeLMod I \in LMod \land Scalar (R freeLMod I) \in NzRing)$
53	35 15	lindsind2	$⊢ ((R freeLMod I \in LMod \land Scalar (R freeLMod I) \in NzRing) \land X \in LIndS (R freeLMod I) \land y \in X) \to \neg y \in LSpan (R freeLMod I) (X ∖ \{y\})$
54	53	3expa	$⊢ (((R freeLMod I \in LMod \land Scalar (R freeLMod I) \in NzRing) \land X \in LIndS (R freeLMod I)) \land y \in X) \to \neg y \in LSpan (R freeLMod I) (X ∖ \{y\})$
55	52 54	sylanl1	$⊢ (((R \in DivRing \land I \in Fin) \land X \in LIndS (R freeLMod I)) \land y \in X) \to \neg y \in LSpan (R freeLMod I) (X ∖ \{y\})$
56	37	fveq1d	$⊢ (R \in DivRing \land I \in Fin) \to LSpan (R freeLMod I) (X ∖ \{y\}) = mrCls (LSubSp (R freeLMod I)) (X ∖ \{y\})$
57	56	eleq2d	$⊢ (R \in DivRing \land I \in Fin) \to (y \in LSpan (R freeLMod I) (X ∖ \{y\}) \leftrightarrow y \in mrCls (LSubSp (R freeLMod I)) (X ∖ \{y\}))$
58	57	ad2antrr	$⊢ (((R \in DivRing \land I \in Fin) \land X \in LIndS (R freeLMod I)) \land y \in X) \to (y \in LSpan (R freeLMod I) (X ∖ \{y\}) \leftrightarrow y \in mrCls (LSubSp (R freeLMod I)) (X ∖ \{y\}))$
59	55 58	mtbid	$⊢ (((R \in DivRing \land I \in Fin) \land X \in LIndS (R freeLMod I)) \land y \in X) \to \neg y \in mrCls (LSubSp (R freeLMod I)) (X ∖ \{y\})$
60	59	ralrimiva	$⊢ ((R \in DivRing \land I \in Fin) \land X \in LIndS (R freeLMod I)) \to \forall y \in X \neg y \in mrCls (LSubSp (R freeLMod I)) (X ∖ \{y\})$
61	60	3impa	$⊢ (R \in DivRing \land I \in Fin \land X \in LIndS (R freeLMod I)) \to \forall y \in X \neg y \in mrCls (LSubSp (R freeLMod I)) (X ∖ \{y\})$
62	10 11	ismri2	$⊢ (LSubSp (R freeLMod I) \in Moore ({Base}_{(R freeLMod I)}) \land X \subseteq {Base}_{(R freeLMod I)}) \to (X \in mrInd (LSubSp (R freeLMod I)) \leftrightarrow \forall y \in X \neg y \in mrCls (LSubSp (R freeLMod I)) (X ∖ \{y\}))$
63	8 31 62	syl2an	$⊢ ((R \in DivRing \land I \in Fin) \land X \in LIndS (R freeLMod I)) \to (X \in mrInd (LSubSp (R freeLMod I)) \leftrightarrow \forall y \in X \neg y \in mrCls (LSubSp (R freeLMod I)) (X ∖ \{y\}))$
64	63	3impa	$⊢ (R \in DivRing \land I \in Fin \land X \in LIndS (R freeLMod I)) \to (X \in mrInd (LSubSp (R freeLMod I)) \leftrightarrow \forall y \in X \neg y \in mrCls (LSubSp (R freeLMod I)) (X ∖ \{y\}))$
65	61 64	mpbird	$⊢ (R \in DivRing \land I \in Fin \land X \in LIndS (R freeLMod I)) \to X \in mrInd (LSubSp (R freeLMod I))$
66	48 65	eqeltrid	$⊢ (R \in DivRing \land I \in Fin \land X \in LIndS (R freeLMod I)) \to X \cup \emptyset \in mrInd (LSubSp (R freeLMod I))$
67		simpr	$⊢ (R \in DivRing \land I \in Fin) \to I \in Fin$
68	25	uvcendim	$⊢ (R \in NzRing \land I \in Fin) \to I \approx ran (R unitVec I)$
69	49 68	sylan	$⊢ (R \in DivRing \land I \in Fin) \to I \approx ran (R unitVec I)$
70		enfi	$⊢ I \approx ran (R unitVec I) \to (I \in Fin \leftrightarrow ran (R unitVec I) \in Fin)$
71	69 70	syl	$⊢ (R \in DivRing \land I \in Fin) \to (I \in Fin \leftrightarrow ran (R unitVec I) \in Fin)$
72	67 71	mpbid	$⊢ (R \in DivRing \land I \in Fin) \to ran (R unitVec I) \in Fin$
73	72	olcd	$⊢ (R \in DivRing \land I \in Fin) \to (X \in Fin \lor ran (R unitVec I) \in Fin)$
74	73	3adant3	$⊢ (R \in DivRing \land I \in Fin \land X \in LIndS (R freeLMod I)) \to (X \in Fin \lor ran (R unitVec I) \in Fin)$
75	9 10 11 21 24 30 47 66 74	mreexexd	$⊢ (R \in DivRing \land I \in Fin \land X \in LIndS (R freeLMod I)) \to \exists f \in 𝒫 ran (R unitVec I) (X \approx f \land f \cup \emptyset \in mrInd (LSubSp (R freeLMod I)))$
76		simpl	$⊢ (X \approx f \land f \cup \emptyset \in mrInd (LSubSp (R freeLMod I))) \to X \approx f$
77		ovex	$⊢ R unitVec I \in V$
78	77	rnex	$⊢ ran (R unitVec I) \in V$
79		elpwi	$⊢ f \in 𝒫 ran (R unitVec I) \to f \subseteq ran (R unitVec I)$
80		ssdomg	$⊢ ran (R unitVec I) \in V \to (f \subseteq ran (R unitVec I) \to f ≼ ran (R unitVec I))$
81	78 79 80	mpsyl	$⊢ f \in 𝒫 ran (R unitVec I) \to f ≼ ran (R unitVec I)$
82		endomtr	$⊢ (X \approx f \land f ≼ ran (R unitVec I)) \to X ≼ ran (R unitVec I)$
83	76 81 82	syl2anr	$⊢ (f \in 𝒫 ran (R unitVec I) \land (X \approx f \land f \cup \emptyset \in mrInd (LSubSp (R freeLMod I)))) \to X ≼ ran (R unitVec I)$
84	83	rexlimiva	$⊢ \exists f \in 𝒫 ran (R unitVec I) (X \approx f \land f \cup \emptyset \in mrInd (LSubSp (R freeLMod I))) \to X ≼ ran (R unitVec I)$
85	75 84	syl	$⊢ (R \in DivRing \land I \in Fin \land X \in LIndS (R freeLMod I)) \to X ≼ ran (R unitVec I)$
86	69	ensymd	$⊢ (R \in DivRing \land I \in Fin) \to ran (R unitVec I) \approx I$
87	86	3adant3	$⊢ (R \in DivRing \land I \in Fin \land X \in LIndS (R freeLMod I)) \to ran (R unitVec I) \approx I$
88		domentr	$⊢ (X ≼ ran (R unitVec I) \land ran (R unitVec I) \approx I) \to X ≼ I$
89	85 87 88	syl2anc	$⊢ (R \in DivRing \land I \in Fin \land X \in LIndS (R freeLMod I)) \to X ≼ I$

Metamath Proof Explorer

Theorem lindsdom

Proof