Metamath Proof Explorer

Theorem 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 ⊢ 𝐵 = ( Base ‘ 𝐸 )
dimlssid.e ⊢ ( 𝜑 → 𝐸 ∈ LVec )
dimlssid.1 ⊢ ( 𝜑 → ( dim ‘ 𝐸 ) ∈ ℕ0 )
dimlssid.l ⊢ ( 𝜑 → 𝐿 ∈ ( LSubSp ‘ 𝐸 ) )
dimlssid.2 ⊢ ( 𝜑 → ( dim ‘ ( 𝐸 ↾s 𝐿 ) ) = ( dim ‘ 𝐸 ) )
Assertion dimlssid ( 𝜑 → 𝐿 = 𝐵 )

Proof

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