This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 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 ⊢ 𝐵 = ( Base ‘ 𝑊 )
lbslelsp.j ⊢ 𝐽 = ( LBasis ‘ 𝑊 )
lbslelsp.k ⊢ 𝐾 = ( LSpan ‘ 𝑊 )
lbslelsp.w ⊢ ( 𝜑 → 𝑊 ∈ LVec )
lbslelsp.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐽 )
lbslelsp.y ⊢ ( 𝜑 → 𝑌 ⊆ 𝐵 )
lbslelsp.1 ⊢ ( 𝜑 → ( 𝐾 ‘ 𝑌 ) = 𝐵 )
Assertion lbslelsp ( 𝜑 → ( ♯ ‘ 𝑋 ) ≤ ( ♯ ‘ 𝑌 ) )

Proof

Step Hyp Ref Expression
1 lbslelsp.b ⊢ 𝐵 = ( Base ‘ 𝑊 )
2 lbslelsp.j ⊢ 𝐽 = ( LBasis ‘ 𝑊 )
3 lbslelsp.k ⊢ 𝐾 = ( LSpan ‘ 𝑊 )
4 lbslelsp.w ⊢ ( 𝜑 → 𝑊 ∈ LVec )
5 lbslelsp.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐽 )
6 lbslelsp.y ⊢ ( 𝜑 → 𝑌 ⊆ 𝐵 )
7 lbslelsp.1 ⊢ ( 𝜑 → ( 𝐾 ‘ 𝑌 ) = 𝐵 )
8 4 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑌 ∈ Fin ) ∧ 𝑠 ∈ 𝐽 ) ∧ 𝑠 ⊆ 𝑌 ) → 𝑊 ∈ LVec )
9 5 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑌 ∈ Fin ) ∧ 𝑠 ∈ 𝐽 ) ∧ 𝑠 ⊆ 𝑌 ) → 𝑋 ∈ 𝐽 )
10 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑌 ∈ Fin ) ∧ 𝑠 ∈ 𝐽 ) ∧ 𝑠 ⊆ 𝑌 ) → 𝑠 ∈ 𝐽 )
11 2 lvecdim ⊢ ( ( 𝑊 ∈ LVec ∧ 𝑋 ∈ 𝐽 ∧ 𝑠 ∈ 𝐽 ) → 𝑋 ≈ 𝑠 )
12 8 9 10 11 syl3anc ⊢ ( ( ( ( 𝜑 ∧ 𝑌 ∈ Fin ) ∧ 𝑠 ∈ 𝐽 ) ∧ 𝑠 ⊆ 𝑌 ) → 𝑋 ≈ 𝑠 )
13 hasheni ⊢ ( 𝑋 ≈ 𝑠 → ( ♯ ‘ 𝑋 ) = ( ♯ ‘ 𝑠 ) )
14 12 13 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑌 ∈ Fin ) ∧ 𝑠 ∈ 𝐽 ) ∧ 𝑠 ⊆ 𝑌 ) → ( ♯ ‘ 𝑋 ) = ( ♯ ‘ 𝑠 ) )
15 hashss ⊢ ( ( 𝑌 ∈ Fin ∧ 𝑠 ⊆ 𝑌 ) → ( ♯ ‘ 𝑠 ) ≤ ( ♯ ‘ 𝑌 ) )
16 15 ad4ant24 ⊢ ( ( ( ( 𝜑 ∧ 𝑌 ∈ Fin ) ∧ 𝑠 ∈ 𝐽 ) ∧ 𝑠 ⊆ 𝑌 ) → ( ♯ ‘ 𝑠 ) ≤ ( ♯ ‘ 𝑌 ) )
17 14 16 eqbrtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑌 ∈ Fin ) ∧ 𝑠 ∈ 𝐽 ) ∧ 𝑠 ⊆ 𝑌 ) → ( ♯ ‘ 𝑋 ) ≤ ( ♯ ‘ 𝑌 ) )
18 4 adantr ⊢ ( ( 𝜑 ∧ 𝑌 ∈ Fin ) → 𝑊 ∈ LVec )
19 simpr ⊢ ( ( 𝜑 ∧ 𝑌 ∈ Fin ) → 𝑌 ∈ Fin )
20 6 adantr ⊢ ( ( 𝜑 ∧ 𝑌 ∈ Fin ) → 𝑌 ⊆ 𝐵 )
21 7 adantr ⊢ ( ( 𝜑 ∧ 𝑌 ∈ Fin ) → ( 𝐾 ‘ 𝑌 ) = 𝐵 )
22 1 2 3 18 19 20 21 exsslsb ⊢ ( ( 𝜑 ∧ 𝑌 ∈ Fin ) → ∃ 𝑠 ∈ 𝐽 𝑠 ⊆ 𝑌 )
23 17 22 r19.29a ⊢ ( ( 𝜑 ∧ 𝑌 ∈ Fin ) → ( ♯ ‘ 𝑋 ) ≤ ( ♯ ‘ 𝑌 ) )
24 5 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝑌 ∈ Fin ) → 𝑋 ∈ 𝐽 )
25 hashxrcl ⊢ ( 𝑋 ∈ 𝐽 → ( ♯ ‘ 𝑋 ) ∈ ℝ* )
26 24 25 syl ⊢ ( ( 𝜑 ∧ ¬ 𝑌 ∈ Fin ) → ( ♯ ‘ 𝑋 ) ∈ ℝ* )
27 26 pnfged ⊢ ( ( 𝜑 ∧ ¬ 𝑌 ∈ Fin ) → ( ♯ ‘ 𝑋 ) ≤ +∞ )
28 1 fvexi ⊢ 𝐵 ∈ V
29 28 a1i ⊢ ( 𝜑 → 𝐵 ∈ V )
30 29 6 ssexd ⊢ ( 𝜑 → 𝑌 ∈ V )
31 hashinf ⊢ ( ( 𝑌 ∈ V ∧ ¬ 𝑌 ∈ Fin ) → ( ♯ ‘ 𝑌 ) = +∞ )
32 30 31 sylan ⊢ ( ( 𝜑 ∧ ¬ 𝑌 ∈ Fin ) → ( ♯ ‘ 𝑌 ) = +∞ )
33 27 32 breqtrrd ⊢ ( ( 𝜑 ∧ ¬ 𝑌 ∈ Fin ) → ( ♯ ‘ 𝑋 ) ≤ ( ♯ ‘ 𝑌 ) )
34 23 33 pm2.61dan ⊢ ( 𝜑 → ( ♯ ‘ 𝑋 ) ≤ ( ♯ ‘ 𝑌 ) )