Metamath Proof Explorer

Theorem lvecdimfi

Description: Finite version of lvecdim which does not require the axiom of choice. The axiom of choice is used in acsmapd , which is required in the infinite case. Suggested by Gérard Lang. (Contributed by Thierry Arnoux, 24-May-2023)

Ref Expression
Hypotheses lvecdimfi.j ⊢ J = LBasis ⁡ W
lvecdimfi.w ⊢ φ → W ∈ LVec
lvecdimfi.s ⊢ φ → S ∈ J
lvecdimfi.t ⊢ φ → T ∈ J
lvecdimfi.f ⊢ φ → S ∈ Fin
Assertion lvecdimfi ⊢ φ → S ≈ T

Proof

Step Hyp Ref Expression
1 lvecdimfi.j ⊢ J = LBasis ⁡ W
2 lvecdimfi.w ⊢ φ → W ∈ LVec
3 lvecdimfi.s ⊢ φ → S ∈ J
4 lvecdimfi.t ⊢ φ → T ∈ J
5 lvecdimfi.f ⊢ φ → S ∈ Fin
6 eqid ⊢ LSubSp ⁡ W = LSubSp ⁡ W
7 eqid ⊢ mrCls ⁡ LSubSp ⁡ W = mrCls ⁡ LSubSp ⁡ W
8 eqid ⊢ Base W = Base W
9 6 7 8 lssacsex ⊢ W ∈ LVec → LSubSp ⁡ W ∈ ACS ⁡ Base W ∧ ∀ x ∈ 𝒫 Base W ∀ y ∈ Base W ∀ z ∈ mrCls ⁡ LSubSp ⁡ W ⁡ x ∪ y ∖ mrCls ⁡ LSubSp ⁡ W ⁡ x y ∈ mrCls ⁡ LSubSp ⁡ W ⁡ x ∪ z
10 2 9 syl ⊢ φ → LSubSp ⁡ W ∈ ACS ⁡ Base W ∧ ∀ x ∈ 𝒫 Base W ∀ y ∈ Base W ∀ z ∈ mrCls ⁡ LSubSp ⁡ W ⁡ x ∪ y ∖ mrCls ⁡ LSubSp ⁡ W ⁡ x y ∈ mrCls ⁡ LSubSp ⁡ W ⁡ x ∪ z
11 10 simpld ⊢ φ → LSubSp ⁡ W ∈ ACS ⁡ Base W
12 11 acsmred ⊢ φ → LSubSp ⁡ W ∈ Moore ⁡ Base W
13 eqid ⊢ mrInd ⁡ LSubSp ⁡ W = mrInd ⁡ LSubSp ⁡ W
14 10 simprd ⊢ φ → ∀ x ∈ 𝒫 Base W ∀ y ∈ Base W ∀ z ∈ mrCls ⁡ LSubSp ⁡ W ⁡ x ∪ y ∖ mrCls ⁡ LSubSp ⁡ W ⁡ x y ∈ mrCls ⁡ LSubSp ⁡ W ⁡ x ∪ z
15 6 7 8 13 1 lbsacsbs ⊢ W ∈ LVec → S ∈ J ↔ S ∈ mrInd ⁡ LSubSp ⁡ W ∧ mrCls ⁡ LSubSp ⁡ W ⁡ S = Base W
16 15 biimpa ⊢ W ∈ LVec ∧ S ∈ J → S ∈ mrInd ⁡ LSubSp ⁡ W ∧ mrCls ⁡ LSubSp ⁡ W ⁡ S = Base W
17 2 3 16 syl2anc ⊢ φ → S ∈ mrInd ⁡ LSubSp ⁡ W ∧ mrCls ⁡ LSubSp ⁡ W ⁡ S = Base W
18 17 simpld ⊢ φ → S ∈ mrInd ⁡ LSubSp ⁡ W
19 6 7 8 13 1 lbsacsbs ⊢ W ∈ LVec → T ∈ J ↔ T ∈ mrInd ⁡ LSubSp ⁡ W ∧ mrCls ⁡ LSubSp ⁡ W ⁡ T = Base W
20 19 biimpa ⊢ W ∈ LVec ∧ T ∈ J → T ∈ mrInd ⁡ LSubSp ⁡ W ∧ mrCls ⁡ LSubSp ⁡ W ⁡ T = Base W
21 2 4 20 syl2anc ⊢ φ → T ∈ mrInd ⁡ LSubSp ⁡ W ∧ mrCls ⁡ LSubSp ⁡ W ⁡ T = Base W
22 21 simpld ⊢ φ → T ∈ mrInd ⁡ LSubSp ⁡ W
23 17 simprd ⊢ φ → mrCls ⁡ LSubSp ⁡ W ⁡ S = Base W
24 21 simprd ⊢ φ → mrCls ⁡ LSubSp ⁡ W ⁡ T = Base W
25 23 24 eqtr4d ⊢ φ → mrCls ⁡ LSubSp ⁡ W ⁡ S = mrCls ⁡ LSubSp ⁡ W ⁡ T
26 12 7 13 14 18 22 5 25 mreexfidimd ⊢ φ → S ≈ T