Theorem lmicdim

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

	Ref	Expression
Hypotheses	lmicdim.1	$$⊢\phi \to S{\simeq }_{𝑚}T$$
	lmicdim.2	$$⊢\phi \to S\in \mathrm{LVec}$$
Assertion	lmicdim	$$⊢\phi \to \dim \left(S\right)=\dim \left(T\right)$$

Proof

Step	Hyp	Ref	Expression
1		lmicdim.1	$$⊢\phi \to S{\simeq }_{𝑚}T$$
2		lmicdim.2	$$⊢\phi \to S\in \mathrm{LVec}$$
3		brlmic	$$⊢S{\simeq }_{𝑚}T\leftrightarrow S\mathrm{LMIso}T\ne \varnothing$$
4	1 3	sylib	$$⊢\phi \to S\mathrm{LMIso}T\ne \varnothing$$
5		n0	$$⊢S\mathrm{LMIso}T\ne \varnothing \leftrightarrow \exists ff\in \left(S\mathrm{LMIso}T\right)$$
6	4 5	sylib	$$⊢\phi \to \exists ff\in \left(S\mathrm{LMIso}T\right)$$
7		simpr	$$⊢\left(\phi \wedge f\in \left(S\mathrm{LMIso}T\right)\right)\to f\in \left(S\mathrm{LMIso}T\right)$$
8	2	adantr	$$⊢\left(\phi \wedge f\in \left(S\mathrm{LMIso}T\right)\right)\to S\in \mathrm{LVec}$$
9	7 8	lmimdim	$$⊢\left(\phi \wedge f\in \left(S\mathrm{LMIso}T\right)\right)\to \dim \left(S\right)=\dim \left(T\right)$$
10	6 9	exlimddv	$$⊢\phi \to \dim \left(S\right)=\dim \left(T\right)$$