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 ⊢ 𝐽 = ( LBasis ‘ 𝑊 )
lvecdimfi.w ⊢ ( 𝜑 → 𝑊 ∈ LVec )
lvecdimfi.s ⊢ ( 𝜑 → 𝑆 ∈ 𝐽 )
lvecdimfi.t ⊢ ( 𝜑 → 𝑇 ∈ 𝐽 )
lvecdimfi.f ⊢ ( 𝜑 → 𝑆 ∈ Fin )
Assertion lvecdimfi ( 𝜑 → 𝑆 ≈ 𝑇 )

Proof

Step Hyp Ref Expression
1 lvecdimfi.j ⊢ 𝐽 = ( LBasis ‘ 𝑊 )
2 lvecdimfi.w ⊢ ( 𝜑 → 𝑊 ∈ LVec )
3 lvecdimfi.s ⊢ ( 𝜑 → 𝑆 ∈ 𝐽 )
4 lvecdimfi.t ⊢ ( 𝜑 → 𝑇 ∈ 𝐽 )
5 lvecdimfi.f ⊢ ( 𝜑 → 𝑆 ∈ Fin )
6 eqid ⊢ ( LSubSp ‘ 𝑊 ) = ( LSubSp ‘ 𝑊 )
7 eqid ⊢ ( mrCls ‘ ( LSubSp ‘ 𝑊 ) ) = ( mrCls ‘ ( LSubSp ‘ 𝑊 ) )
8 eqid ⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
9 6 7 8 lssacsex ⊢ ( 𝑊 ∈ LVec → ( ( LSubSp ‘ 𝑊 ) ∈ ( ACS ‘ ( Base ‘ 𝑊 ) ) ∧ ∀ 𝑥 ∈ 𝒫 ( Base ‘ 𝑊 ) ∀ 𝑦 ∈ ( Base ‘ 𝑊 ) ∀ 𝑧 ∈ ( ( ( mrCls ‘ ( LSubSp ‘ 𝑊 ) ) ‘ ( 𝑥 ∪ { 𝑦 } ) ) ∖ ( ( mrCls ‘ ( LSubSp ‘ 𝑊 ) ) ‘ 𝑥 ) ) 𝑦 ∈ ( ( mrCls ‘ ( LSubSp ‘ 𝑊 ) ) ‘ ( 𝑥 ∪ { 𝑧 } ) ) ) )
10 2 9 syl ⊢ ( 𝜑 → ( ( LSubSp ‘ 𝑊 ) ∈ ( ACS ‘ ( Base ‘ 𝑊 ) ) ∧ ∀ 𝑥 ∈ 𝒫 ( Base ‘ 𝑊 ) ∀ 𝑦 ∈ ( Base ‘ 𝑊 ) ∀ 𝑧 ∈ ( ( ( mrCls ‘ ( LSubSp ‘ 𝑊 ) ) ‘ ( 𝑥 ∪ { 𝑦 } ) ) ∖ ( ( mrCls ‘ ( LSubSp ‘ 𝑊 ) ) ‘ 𝑥 ) ) 𝑦 ∈ ( ( mrCls ‘ ( LSubSp ‘ 𝑊 ) ) ‘ ( 𝑥 ∪ { 𝑧 } ) ) ) )
11 10 simpld ⊢ ( 𝜑 → ( LSubSp ‘ 𝑊 ) ∈ ( ACS ‘ ( Base ‘ 𝑊 ) ) )
12 11 acsmred ⊢ ( 𝜑 → ( LSubSp ‘ 𝑊 ) ∈ ( Moore ‘ ( Base ‘ 𝑊 ) ) )
13 eqid ⊢ ( mrInd ‘ ( LSubSp ‘ 𝑊 ) ) = ( mrInd ‘ ( LSubSp ‘ 𝑊 ) )
14 10 simprd ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝒫 ( Base ‘ 𝑊 ) ∀ 𝑦 ∈ ( Base ‘ 𝑊 ) ∀ 𝑧 ∈ ( ( ( mrCls ‘ ( LSubSp ‘ 𝑊 ) ) ‘ ( 𝑥 ∪ { 𝑦 } ) ) ∖ ( ( mrCls ‘ ( LSubSp ‘ 𝑊 ) ) ‘ 𝑥 ) ) 𝑦 ∈ ( ( mrCls ‘ ( LSubSp ‘ 𝑊 ) ) ‘ ( 𝑥 ∪ { 𝑧 } ) ) )
15 6 7 8 13 1 lbsacsbs ⊢ ( 𝑊 ∈ LVec → ( 𝑆 ∈ 𝐽 ↔ ( 𝑆 ∈ ( mrInd ‘ ( LSubSp ‘ 𝑊 ) ) ∧ ( ( mrCls ‘ ( LSubSp ‘ 𝑊 ) ) ‘ 𝑆 ) = ( Base ‘ 𝑊 ) ) ) )
16 15 biimpa ⊢ ( ( 𝑊 ∈ LVec ∧ 𝑆 ∈ 𝐽 ) → ( 𝑆 ∈ ( mrInd ‘ ( LSubSp ‘ 𝑊 ) ) ∧ ( ( mrCls ‘ ( LSubSp ‘ 𝑊 ) ) ‘ 𝑆 ) = ( Base ‘ 𝑊 ) ) )
17 2 3 16 syl2anc ⊢ ( 𝜑 → ( 𝑆 ∈ ( mrInd ‘ ( LSubSp ‘ 𝑊 ) ) ∧ ( ( mrCls ‘ ( LSubSp ‘ 𝑊 ) ) ‘ 𝑆 ) = ( Base ‘ 𝑊 ) ) )
18 17 simpld ⊢ ( 𝜑 → 𝑆 ∈ ( mrInd ‘ ( LSubSp ‘ 𝑊 ) ) )
19 6 7 8 13 1 lbsacsbs ⊢ ( 𝑊 ∈ LVec → ( 𝑇 ∈ 𝐽 ↔ ( 𝑇 ∈ ( mrInd ‘ ( LSubSp ‘ 𝑊 ) ) ∧ ( ( mrCls ‘ ( LSubSp ‘ 𝑊 ) ) ‘ 𝑇 ) = ( Base ‘ 𝑊 ) ) ) )
20 19 biimpa ⊢ ( ( 𝑊 ∈ LVec ∧ 𝑇 ∈ 𝐽 ) → ( 𝑇 ∈ ( mrInd ‘ ( LSubSp ‘ 𝑊 ) ) ∧ ( ( mrCls ‘ ( LSubSp ‘ 𝑊 ) ) ‘ 𝑇 ) = ( Base ‘ 𝑊 ) ) )
21 2 4 20 syl2anc ⊢ ( 𝜑 → ( 𝑇 ∈ ( mrInd ‘ ( LSubSp ‘ 𝑊 ) ) ∧ ( ( mrCls ‘ ( LSubSp ‘ 𝑊 ) ) ‘ 𝑇 ) = ( Base ‘ 𝑊 ) ) )
22 21 simpld ⊢ ( 𝜑 → 𝑇 ∈ ( mrInd ‘ ( LSubSp ‘ 𝑊 ) ) )
23 17 simprd ⊢ ( 𝜑 → ( ( mrCls ‘ ( LSubSp ‘ 𝑊 ) ) ‘ 𝑆 ) = ( Base ‘ 𝑊 ) )
24 21 simprd ⊢ ( 𝜑 → ( ( mrCls ‘ ( LSubSp ‘ 𝑊 ) ) ‘ 𝑇 ) = ( Base ‘ 𝑊 ) )
25 23 24 eqtr4d ⊢ ( 𝜑 → ( ( mrCls ‘ ( LSubSp ‘ 𝑊 ) ) ‘ 𝑆 ) = ( ( mrCls ‘ ( LSubSp ‘ 𝑊 ) ) ‘ 𝑇 ) )
26 12 7 13 14 18 22 5 25 mreexfidimd ⊢ ( 𝜑 → 𝑆 ≈ 𝑇 )