lmimdim

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

	Ref	Expression
Hypotheses	lmimdim.1	$⊢ φ \to F \in (S LMIso T)$
	lmimdim.2	$⊢ φ \to S \in LVec$
Assertion	lmimdim	$⊢ φ \to \dim (S) = \dim (T)$

Proof

Step	Hyp	Ref	Expression
1		lmimdim.1	$⊢ φ \to F \in (S LMIso T)$
2		lmimdim.2	$⊢ φ \to S \in LVec$
3		eqid	$⊢ LBasis (S) = LBasis (S)$
4	3	lbsex	$⊢ S \in LVec \to LBasis (S) \neq \emptyset$
5	2 4	syl	$⊢ φ \to LBasis (S) \neq \emptyset$
6		n0	$⊢ LBasis (S) \neq \emptyset \leftrightarrow \exists b b \in LBasis (S)$
7	5 6	sylib	$⊢ φ \to \exists b b \in LBasis (S)$
8	1	adantr	$⊢ (φ \land b \in LBasis (S)) \to F \in (S LMIso T)$
9	8	resexd	$⊢ (φ \land b \in LBasis (S)) \to {F ↾}_{b} \in V$
10		eqid	$⊢ {Base}_{S} = {Base}_{S}$
11		eqid	$⊢ {Base}_{T} = {Base}_{T}$
12	10 11	lmimf1o	$⊢ F \in (S LMIso T) \to F : {Base}_{S} \underset{1-1 onto}{⟶} {Base}_{T}$
13		f1of1	$⊢ F : {Base}_{S} \underset{1-1 onto}{⟶} {Base}_{T} \to F : {Base}_{S} \underset{1-1}{⟶} {Base}_{T}$
14	8 12 13	3syl	$⊢ (φ \land b \in LBasis (S)) \to F : {Base}_{S} \underset{1-1}{⟶} {Base}_{T}$
15	10 3	lbsss	$⊢ b \in LBasis (S) \to b \subseteq {Base}_{S}$
16	15	adantl	$⊢ (φ \land b \in LBasis (S)) \to b \subseteq {Base}_{S}$
17		f1ssres	$⊢ (F : {Base}_{S} \underset{1-1}{⟶} {Base}_{T} \land b \subseteq {Base}_{S}) \to ({F ↾}_{b}) : b \underset{1-1}{⟶} {Base}_{T}$
18	14 16 17	syl2anc	$⊢ (φ \land b \in LBasis (S)) \to ({F ↾}_{b}) : b \underset{1-1}{⟶} {Base}_{T}$
19		hashf1dmrn	$⊢ ({F ↾}_{b} \in V \land ({F ↾}_{b}) : b \underset{1-1}{⟶} {Base}_{T}) \to \|b\| = \|ran ({F ↾}_{b})\|$
20	9 18 19	syl2anc	$⊢ (φ \land b \in LBasis (S)) \to \|b\| = \|ran ({F ↾}_{b})\|$
21		df-ima	$⊢ F [b] = ran ({F ↾}_{b})$
22	21	fveq2i	$⊢ \|F [b]\| = \|ran ({F ↾}_{b})\|$
23	20 22	eqtr4di	$⊢ (φ \land b \in LBasis (S)) \to \|b\| = \|F [b]\|$
24	3	dimval	$⊢ (S \in LVec \land b \in LBasis (S)) \to \dim (S) = \|b\|$
25	2 24	sylan	$⊢ (φ \land b \in LBasis (S)) \to \dim (S) = \|b\|$
26		lmimlmhm	$⊢ F \in (S LMIso T) \to F \in (S LMHom T)$
27	1 26	syl	$⊢ φ \to F \in (S LMHom T)$
28		lmhmlvec	$⊢ F \in (S LMHom T) \to (S \in LVec \leftrightarrow T \in LVec)$
29	28	biimpa	$⊢ (F \in (S LMHom T) \land S \in LVec) \to T \in LVec$
30	27 2 29	syl2anc	$⊢ φ \to T \in LVec$
31	30	adantr	$⊢ (φ \land b \in LBasis (S)) \to T \in LVec$
32		eqid	$⊢ LBasis (T) = LBasis (T)$
33	3 32	lmimlbs	$⊢ (F \in (S LMIso T) \land b \in LBasis (S)) \to F [b] \in LBasis (T)$
34	1 33	sylan	$⊢ (φ \land b \in LBasis (S)) \to F [b] \in LBasis (T)$
35	32	dimval	$⊢ (T \in LVec \land F [b] \in LBasis (T)) \to \dim (T) = \|F [b]\|$
36	31 34 35	syl2anc	$⊢ (φ \land b \in LBasis (S)) \to \dim (T) = \|F [b]\|$
37	23 25 36	3eqtr4d	$⊢ (φ \land b \in LBasis (S)) \to \dim (S) = \dim (T)$
38	7 37	exlimddv	$⊢ φ \to \dim (S) = \dim (T)$

Metamath Proof Explorer

Theorem lmimdim

Proof