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