lbslelsp

Description: The size of a basis X of a vector space W is less than the size of a generating set Y . (Contributed by Thierry Arnoux, 13-Oct-2025)

	Ref	Expression
Hypotheses	lbslelsp.b	$⊢ B = {Base}_{W}$
	lbslelsp.j	$⊢ J = LBasis (W)$
	lbslelsp.k	$⊢ K = LSpan (W)$
	lbslelsp.w	$⊢ φ \to W \in LVec$
	lbslelsp.x	$⊢ φ \to X \in J$
	lbslelsp.y	$⊢ φ \to Y \subseteq B$
	lbslelsp.1	$⊢ φ \to K (Y) = B$
Assertion	lbslelsp	$⊢ φ \to \|X\| \leq \|Y\|$

Proof

Step	Hyp	Ref	Expression
1		lbslelsp.b	$⊢ B = {Base}_{W}$
2		lbslelsp.j	$⊢ J = LBasis (W)$
3		lbslelsp.k	$⊢ K = LSpan (W)$
4		lbslelsp.w	$⊢ φ \to W \in LVec$
5		lbslelsp.x	$⊢ φ \to X \in J$
6		lbslelsp.y	$⊢ φ \to Y \subseteq B$
7		lbslelsp.1	$⊢ φ \to K (Y) = B$
8	4	ad3antrrr	$⊢ (((φ \land Y \in Fin) \land s \in J) \land s \subseteq Y) \to W \in LVec$
9	5	ad3antrrr	$⊢ (((φ \land Y \in Fin) \land s \in J) \land s \subseteq Y) \to X \in J$
10		simplr	$⊢ (((φ \land Y \in Fin) \land s \in J) \land s \subseteq Y) \to s \in J$
11	2	lvecdim	$⊢ (W \in LVec \land X \in J \land s \in J) \to X \approx s$
12	8 9 10 11	syl3anc	$⊢ (((φ \land Y \in Fin) \land s \in J) \land s \subseteq Y) \to X \approx s$
13		hasheni	$⊢ X \approx s \to \|X\| = \|s\|$
14	12 13	syl	$⊢ (((φ \land Y \in Fin) \land s \in J) \land s \subseteq Y) \to \|X\| = \|s\|$
15		hashss	$⊢ (Y \in Fin \land s \subseteq Y) \to \|s\| \leq \|Y\|$
16	15	ad4ant24	$⊢ (((φ \land Y \in Fin) \land s \in J) \land s \subseteq Y) \to \|s\| \leq \|Y\|$
17	14 16	eqbrtrd	$⊢ (((φ \land Y \in Fin) \land s \in J) \land s \subseteq Y) \to \|X\| \leq \|Y\|$
18	4	adantr	$⊢ (φ \land Y \in Fin) \to W \in LVec$
19		simpr	$⊢ (φ \land Y \in Fin) \to Y \in Fin$
20	6	adantr	$⊢ (φ \land Y \in Fin) \to Y \subseteq B$
21	7	adantr	$⊢ (φ \land Y \in Fin) \to K (Y) = B$
22	1 2 3 18 19 20 21	exsslsb	$⊢ (φ \land Y \in Fin) \to \exists s \in J s \subseteq Y$
23	17 22	r19.29a	$⊢ (φ \land Y \in Fin) \to \|X\| \leq \|Y\|$
24	5	adantr	$⊢ (φ \land \neg Y \in Fin) \to X \in J$
25		hashxrcl	$⊢ X \in J \to \|X\| \in ℝ^{*}$
26	24 25	syl	$⊢ (φ \land \neg Y \in Fin) \to \|X\| \in ℝ^{*}$
27	26	pnfged	$⊢ (φ \land \neg Y \in Fin) \to \|X\| \leq +∞$
28	1	fvexi	$⊢ B \in V$
29	28	a1i	$⊢ φ \to B \in V$
30	29 6	ssexd	$⊢ φ \to Y \in V$
31		hashinf	$⊢ (Y \in V \land \neg Y \in Fin) \to \|Y\| = +∞$
32	30 31	sylan	$⊢ (φ \land \neg Y \in Fin) \to \|Y\| = +∞$
33	27 32	breqtrrd	$⊢ (φ \land \neg Y \in Fin) \to \|X\| \leq \|Y\|$
34	23 33	pm2.61dan	$⊢ φ \to \|X\| \leq \|Y\|$

Metamath Proof Explorer

Theorem lbslelsp

Proof