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

Metamath Proof Explorer

Theorem lmicdim

Description: Module isomorphisms preserve vector space dimensions. (Contributed by Thierry Arnoux, 25-Mar-2025)

Ref Expression
Hypotheses lmicdim.1 ⊢ φ → S ≃ 𝑚 T
lmicdim.2 ⊢ φ → S ∈ LVec
Assertion lmicdim ⊢ φ → dim ⁡ S = dim ⁡ T

Proof

Step Hyp Ref Expression
1 lmicdim.1 ⊢ φ → S ≃ 𝑚 T
2 lmicdim.2 ⊢ φ → S ∈ LVec
3 brlmic ⊢ S ≃ 𝑚 T ↔ S LMIso T ≠ ∅
4 1 3 sylib ⊢ φ → S LMIso T ≠ ∅
5 n0 ⊢ S LMIso T ≠ ∅ ↔ ∃ f f ∈ S LMIso T
6 4 5 sylib ⊢ φ → ∃ f f ∈ S LMIso T
7 simpr ⊢ φ ∧ f ∈ S LMIso T → f ∈ S LMIso T
8 2 adantr ⊢ φ ∧ f ∈ S LMIso T → S ∈ LVec
9 7 8 lmimdim ⊢ φ ∧ f ∈ S LMIso T → dim ⁡ S = dim ⁡ T
10 6 9 exlimddv ⊢ φ → dim ⁡ S = dim ⁡ T