dimlssid

Description: If the dimension of a linear subspace L is the dimension of the whole vector space E , then L is the whole space. (Contributed by Thierry Arnoux, 3-Aug-2025)

	Ref	Expression
Hypotheses	dimlssid.b	$⊢ B = {Base}_{E}$
	dimlssid.e	$⊢ φ \to E \in LVec$
	dimlssid.1	$⊢ φ \to \dim (E) \in ℕ_{0}$
	dimlssid.l	$⊢ φ \to L \in LSubSp (E)$
	dimlssid.2	$⊢ φ \to \dim (E ↾_{𝑠} L) = \dim (E)$
Assertion	dimlssid	$⊢ φ \to L = B$

Proof

Step	Hyp	Ref	Expression
1		dimlssid.b	$⊢ B = {Base}_{E}$
2		dimlssid.e	$⊢ φ \to E \in LVec$
3		dimlssid.1	$⊢ φ \to \dim (E) \in ℕ_{0}$
4		dimlssid.l	$⊢ φ \to L \in LSubSp (E)$
5		dimlssid.2	$⊢ φ \to \dim (E ↾_{𝑠} L) = \dim (E)$
6		eqid	$⊢ E ↾_{𝑠} L = E ↾_{𝑠} L$
7		eqid	$⊢ LSubSp (E) = LSubSp (E)$
8	6 7	lsslvec	$⊢ (E \in LVec \land L \in LSubSp (E)) \to E ↾_{𝑠} L \in LVec$
9	2 4 8	syl2anc	$⊢ φ \to E ↾_{𝑠} L \in LVec$
10		eqid	$⊢ LBasis (E ↾_{𝑠} L) = LBasis (E ↾_{𝑠} L)$
11	10	lbsex	$⊢ E ↾_{𝑠} L \in LVec \to LBasis (E ↾_{𝑠} L) \neq \emptyset$
12	9 11	syl	$⊢ φ \to LBasis (E ↾_{𝑠} L) \neq \emptyset$
13		simplr	$⊢ (((φ \land t \in LBasis (E ↾_{𝑠} L)) \land s \in LBasis (E)) \land t \subseteq s) \to s \in LBasis (E)$
14		eqid	$⊢ LBasis (E) = LBasis (E)$
15	14	dimval	$⊢ (E \in LVec \land s \in LBasis (E)) \to \dim (E) = \|s\|$
16	2 15	sylan	$⊢ (φ \land s \in LBasis (E)) \to \dim (E) = \|s\|$
17	16	ad4ant13	$⊢ (((φ \land t \in LBasis (E ↾_{𝑠} L)) \land s \in LBasis (E)) \land t \subseteq s) \to \dim (E) = \|s\|$
18	3	ad3antrrr	$⊢ (((φ \land t \in LBasis (E ↾_{𝑠} L)) \land s \in LBasis (E)) \land t \subseteq s) \to \dim (E) \in ℕ_{0}$
19	17 18	eqeltrrd	$⊢ (((φ \land t \in LBasis (E ↾_{𝑠} L)) \land s \in LBasis (E)) \land t \subseteq s) \to \|s\| \in ℕ_{0}$
20		hashclb	$⊢ s \in LBasis (E) \to (s \in Fin \leftrightarrow \|s\| \in ℕ_{0})$
21	20	biimpar	$⊢ (s \in LBasis (E) \land \|s\| \in ℕ_{0}) \to s \in Fin$
22	13 19 21	syl2anc	$⊢ (((φ \land t \in LBasis (E ↾_{𝑠} L)) \land s \in LBasis (E)) \land t \subseteq s) \to s \in Fin$
23		simpr	$⊢ (((φ \land t \in LBasis (E ↾_{𝑠} L)) \land s \in LBasis (E)) \land t \subseteq s) \to t \subseteq s$
24	5	ad3antrrr	$⊢ (((φ \land t \in LBasis (E ↾_{𝑠} L)) \land s \in LBasis (E)) \land t \subseteq s) \to \dim (E ↾_{𝑠} L) = \dim (E)$
25	9	ad3antrrr	$⊢ (((φ \land t \in LBasis (E ↾_{𝑠} L)) \land s \in LBasis (E)) \land t \subseteq s) \to E ↾_{𝑠} L \in LVec$
26		simpllr	$⊢ (((φ \land t \in LBasis (E ↾_{𝑠} L)) \land s \in LBasis (E)) \land t \subseteq s) \to t \in LBasis (E ↾_{𝑠} L)$
27	10	dimval	$⊢ (E ↾_{𝑠} L \in LVec \land t \in LBasis (E ↾_{𝑠} L)) \to \dim (E ↾_{𝑠} L) = \|t\|$
28	25 26 27	syl2anc	$⊢ (((φ \land t \in LBasis (E ↾_{𝑠} L)) \land s \in LBasis (E)) \land t \subseteq s) \to \dim (E ↾_{𝑠} L) = \|t\|$
29	24 28 17	3eqtr3d	$⊢ (((φ \land t \in LBasis (E ↾_{𝑠} L)) \land s \in LBasis (E)) \land t \subseteq s) \to \|t\| = \|s\|$
30	22 23 29	phphashrd	$⊢ (((φ \land t \in LBasis (E ↾_{𝑠} L)) \land s \in LBasis (E)) \land t \subseteq s) \to t = s$
31	30	fveq2d	$⊢ (((φ \land t \in LBasis (E ↾_{𝑠} L)) \land s \in LBasis (E)) \land t \subseteq s) \to LSpan (E) (t) = LSpan (E) (s)$
32	1 7	lssss	$⊢ L \in LSubSp (E) \to L \subseteq B$
33	6 1	ressbas2	$⊢ L \subseteq B \to L = {Base}_{(E ↾_{𝑠} L)}$
34	4 32 33	3syl	$⊢ φ \to L = {Base}_{(E ↾_{𝑠} L)}$
35	34	ad3antrrr	$⊢ (((φ \land t \in LBasis (E ↾_{𝑠} L)) \land s \in LBasis (E)) \land t \subseteq s) \to L = {Base}_{(E ↾_{𝑠} L)}$
36		eqid	$⊢ {Base}_{(E ↾_{𝑠} L)} = {Base}_{(E ↾_{𝑠} L)}$
37		eqid	$⊢ LSpan (E ↾_{𝑠} L) = LSpan (E ↾_{𝑠} L)$
38	36 10 37	lbssp	$⊢ t \in LBasis (E ↾_{𝑠} L) \to LSpan (E ↾_{𝑠} L) (t) = {Base}_{(E ↾_{𝑠} L)}$
39	26 38	syl	$⊢ (((φ \land t \in LBasis (E ↾_{𝑠} L)) \land s \in LBasis (E)) \land t \subseteq s) \to LSpan (E ↾_{𝑠} L) (t) = {Base}_{(E ↾_{𝑠} L)}$
40	2	lveclmodd	$⊢ φ \to E \in LMod$
41	40	ad3antrrr	$⊢ (((φ \land t \in LBasis (E ↾_{𝑠} L)) \land s \in LBasis (E)) \land t \subseteq s) \to E \in LMod$
42	4	ad3antrrr	$⊢ (((φ \land t \in LBasis (E ↾_{𝑠} L)) \land s \in LBasis (E)) \land t \subseteq s) \to L \in LSubSp (E)$
43	36 10	lbsss	$⊢ t \in LBasis (E ↾_{𝑠} L) \to t \subseteq {Base}_{(E ↾_{𝑠} L)}$
44	26 43	syl	$⊢ (((φ \land t \in LBasis (E ↾_{𝑠} L)) \land s \in LBasis (E)) \land t \subseteq s) \to t \subseteq {Base}_{(E ↾_{𝑠} L)}$
45	44 35	sseqtrrd	$⊢ (((φ \land t \in LBasis (E ↾_{𝑠} L)) \land s \in LBasis (E)) \land t \subseteq s) \to t \subseteq L$
46		eqid	$⊢ LSpan (E) = LSpan (E)$
47	6 46 37 7	lsslsp	$⊢ (E \in LMod \land L \in LSubSp (E) \land t \subseteq L) \to LSpan (E ↾_{𝑠} L) (t) = LSpan (E) (t)$
48	41 42 45 47	syl3anc	$⊢ (((φ \land t \in LBasis (E ↾_{𝑠} L)) \land s \in LBasis (E)) \land t \subseteq s) \to LSpan (E ↾_{𝑠} L) (t) = LSpan (E) (t)$
49	35 39 48	3eqtr2rd	$⊢ (((φ \land t \in LBasis (E ↾_{𝑠} L)) \land s \in LBasis (E)) \land t \subseteq s) \to LSpan (E) (t) = L$
50	1 14 46	lbssp	$⊢ s \in LBasis (E) \to LSpan (E) (s) = B$
51	13 50	syl	$⊢ (((φ \land t \in LBasis (E ↾_{𝑠} L)) \land s \in LBasis (E)) \land t \subseteq s) \to LSpan (E) (s) = B$
52	31 49 51	3eqtr3d	$⊢ (((φ \land t \in LBasis (E ↾_{𝑠} L)) \land s \in LBasis (E)) \land t \subseteq s) \to L = B$
53	2	adantr	$⊢ (φ \land t \in LBasis (E ↾_{𝑠} L)) \to E \in LVec$
54	43	adantl	$⊢ (φ \land t \in LBasis (E ↾_{𝑠} L)) \to t \subseteq {Base}_{(E ↾_{𝑠} L)}$
55	34	adantr	$⊢ (φ \land t \in LBasis (E ↾_{𝑠} L)) \to L = {Base}_{(E ↾_{𝑠} L)}$
56	54 55	sseqtrrd	$⊢ (φ \land t \in LBasis (E ↾_{𝑠} L)) \to t \subseteq L$
57	4 32	syl	$⊢ φ \to L \subseteq B$
58	57	adantr	$⊢ (φ \land t \in LBasis (E ↾_{𝑠} L)) \to L \subseteq B$
59	56 58	sstrd	$⊢ (φ \land t \in LBasis (E ↾_{𝑠} L)) \to t \subseteq B$
60	9	lveclmodd	$⊢ φ \to E ↾_{𝑠} L \in LMod$
61	60	ad2antrr	$⊢ ((φ \land t \in LBasis (E ↾_{𝑠} L)) \land u \in t) \to E ↾_{𝑠} L \in LMod$
62		eqid	$⊢ Scalar (E) = Scalar (E)$
63	62	lvecdrng	$⊢ E \in LVec \to Scalar (E) \in DivRing$
64		drngnzr	$⊢ Scalar (E) \in DivRing \to Scalar (E) \in NzRing$
65	2 63 64	3syl	$⊢ φ \to Scalar (E) \in NzRing$
66		eqid	$⊢ 1_{Scalar (E)} = 1_{Scalar (E)}$
67		eqid	$⊢ 0_{Scalar (E)} = 0_{Scalar (E)}$
68	66 67	nzrnz	$⊢ Scalar (E) \in NzRing \to 1_{Scalar (E)} \neq 0_{Scalar (E)}$
69	65 68	syl	$⊢ φ \to 1_{Scalar (E)} \neq 0_{Scalar (E)}$
70	6 62	resssca	$⊢ L \in LSubSp (E) \to Scalar (E) = Scalar (E ↾_{𝑠} L)$
71	4 70	syl	$⊢ φ \to Scalar (E) = Scalar (E ↾_{𝑠} L)$
72	71	fveq2d	$⊢ φ \to 1_{Scalar (E)} = 1_{Scalar (E ↾_{𝑠} L)}$
73	71	fveq2d	$⊢ φ \to 0_{Scalar (E)} = 0_{Scalar (E ↾_{𝑠} L)}$
74	69 72 73	3netr3d	$⊢ φ \to 1_{Scalar (E ↾_{𝑠} L)} \neq 0_{Scalar (E ↾_{𝑠} L)}$
75	74	ad2antrr	$⊢ ((φ \land t \in LBasis (E ↾_{𝑠} L)) \land u \in t) \to 1_{Scalar (E ↾_{𝑠} L)} \neq 0_{Scalar (E ↾_{𝑠} L)}$
76		simplr	$⊢ ((φ \land t \in LBasis (E ↾_{𝑠} L)) \land u \in t) \to t \in LBasis (E ↾_{𝑠} L)$
77		simpr	$⊢ ((φ \land t \in LBasis (E ↾_{𝑠} L)) \land u \in t) \to u \in t$
78		eqid	$⊢ Scalar (E ↾_{𝑠} L) = Scalar (E ↾_{𝑠} L)$
79		eqid	$⊢ 1_{Scalar (E ↾_{𝑠} L)} = 1_{Scalar (E ↾_{𝑠} L)}$
80		eqid	$⊢ 0_{Scalar (E ↾_{𝑠} L)} = 0_{Scalar (E ↾_{𝑠} L)}$
81	10 37 78 79 80	lbsind2	$⊢ ((E ↾_{𝑠} L \in LMod \land 1_{Scalar (E ↾_{𝑠} L)} \neq 0_{Scalar (E ↾_{𝑠} L)}) \land t \in LBasis (E ↾_{𝑠} L) \land u \in t) \to \neg u \in LSpan (E ↾_{𝑠} L) (t ∖ \{u\})$
82	61 75 76 77 81	syl211anc	$⊢ ((φ \land t \in LBasis (E ↾_{𝑠} L)) \land u \in t) \to \neg u \in LSpan (E ↾_{𝑠} L) (t ∖ \{u\})$
83	40	ad2antrr	$⊢ ((φ \land t \in LBasis (E ↾_{𝑠} L)) \land u \in t) \to E \in LMod$
84	4	ad2antrr	$⊢ ((φ \land t \in LBasis (E ↾_{𝑠} L)) \land u \in t) \to L \in LSubSp (E)$
85	56	adantr	$⊢ ((φ \land t \in LBasis (E ↾_{𝑠} L)) \land u \in t) \to t \subseteq L$
86	85	ssdifssd	$⊢ ((φ \land t \in LBasis (E ↾_{𝑠} L)) \land u \in t) \to t ∖ \{u\} \subseteq L$
87	6 46 37 7	lsslsp	$⊢ (E \in LMod \land L \in LSubSp (E) \land t ∖ \{u\} \subseteq L) \to LSpan (E ↾_{𝑠} L) (t ∖ \{u\}) = LSpan (E) (t ∖ \{u\})$
88	83 84 86 87	syl3anc	$⊢ ((φ \land t \in LBasis (E ↾_{𝑠} L)) \land u \in t) \to LSpan (E ↾_{𝑠} L) (t ∖ \{u\}) = LSpan (E) (t ∖ \{u\})$
89	82 88	neleqtrd	$⊢ ((φ \land t \in LBasis (E ↾_{𝑠} L)) \land u \in t) \to \neg u \in LSpan (E) (t ∖ \{u\})$
90	89	ralrimiva	$⊢ (φ \land t \in LBasis (E ↾_{𝑠} L)) \to \forall u \in t \neg u \in LSpan (E) (t ∖ \{u\})$
91	14 1 46	lbsext	$⊢ (E \in LVec \land t \subseteq B \land \forall u \in t \neg u \in LSpan (E) (t ∖ \{u\})) \to \exists s \in LBasis (E) t \subseteq s$
92	53 59 90 91	syl3anc	$⊢ (φ \land t \in LBasis (E ↾_{𝑠} L)) \to \exists s \in LBasis (E) t \subseteq s$
93	52 92	r19.29a	$⊢ (φ \land t \in LBasis (E ↾_{𝑠} L)) \to L = B$
94	12 93	n0limd	$⊢ φ \to L = B$

Metamath Proof Explorer

Theorem dimlssid

Proof