Theorem lmimdim

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

	Ref	Expression
Hypotheses	lmimdim.1	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑆 LMIso 𝑇 ) )
	lmimdim.2	⊢ ( 𝜑 → 𝑆 ∈ LVec )
Assertion	lmimdim	⊢ ( 𝜑 → ( dim ‘ 𝑆 ) = ( dim ‘ 𝑇 ) )

Proof

Step	Hyp	Ref	Expression
1		lmimdim.1	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑆 LMIso 𝑇 ) )
2		lmimdim.2	⊢ ( 𝜑 → 𝑆 ∈ LVec )
3		eqid	⊢ ( LBasis ‘ 𝑆 ) = ( LBasis ‘ 𝑆 )
4	3	lbsex	⊢ ( 𝑆 ∈ LVec → ( LBasis ‘ 𝑆 ) ≠ ∅ )
5	2 4	syl	⊢ ( 𝜑 → ( LBasis ‘ 𝑆 ) ≠ ∅ )
6		n0	⊢ ( ( LBasis ‘ 𝑆 ) ≠ ∅ ↔ ∃ 𝑏 𝑏 ∈ ( LBasis ‘ 𝑆 ) )
7	5 6	sylib	⊢ ( 𝜑 → ∃ 𝑏 𝑏 ∈ ( LBasis ‘ 𝑆 ) )
8	1	adantr	⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( LBasis ‘ 𝑆 ) ) → 𝐹 ∈ ( 𝑆 LMIso 𝑇 ) )
9	8	resexd	⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( LBasis ‘ 𝑆 ) ) → ( 𝐹 ↾ 𝑏 ) ∈ V )
10		eqid	⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
11		eqid	⊢ ( Base ‘ 𝑇 ) = ( Base ‘ 𝑇 )
12	10 11	lmimf1o	⊢ ( 𝐹 ∈ ( 𝑆 LMIso 𝑇 ) → 𝐹 : ( Base ‘ 𝑆 ) –1-1-onto→ ( Base ‘ 𝑇 ) )
13		f1of1	⊢ ( 𝐹 : ( Base ‘ 𝑆 ) –1-1-onto→ ( Base ‘ 𝑇 ) → 𝐹 : ( Base ‘ 𝑆 ) –1-1→ ( Base ‘ 𝑇 ) )
14	8 12 13	3syl	⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( LBasis ‘ 𝑆 ) ) → 𝐹 : ( Base ‘ 𝑆 ) –1-1→ ( Base ‘ 𝑇 ) )
15	10 3	lbsss	⊢ ( 𝑏 ∈ ( LBasis ‘ 𝑆 ) → 𝑏 ⊆ ( Base ‘ 𝑆 ) )
16	15	adantl	⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( LBasis ‘ 𝑆 ) ) → 𝑏 ⊆ ( Base ‘ 𝑆 ) )
17		f1ssres	⊢ ( ( 𝐹 : ( Base ‘ 𝑆 ) –1-1→ ( Base ‘ 𝑇 ) ∧ 𝑏 ⊆ ( Base ‘ 𝑆 ) ) → ( 𝐹 ↾ 𝑏 ) : 𝑏 –1-1→ ( Base ‘ 𝑇 ) )
18	14 16 17	syl2anc	⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( LBasis ‘ 𝑆 ) ) → ( 𝐹 ↾ 𝑏 ) : 𝑏 –1-1→ ( Base ‘ 𝑇 ) )
19		hashf1dmrn	⊢ ( ( ( 𝐹 ↾ 𝑏 ) ∈ V ∧ ( 𝐹 ↾ 𝑏 ) : 𝑏 –1-1→ ( Base ‘ 𝑇 ) ) → ( ♯ ‘ 𝑏 ) = ( ♯ ‘ ran ( 𝐹 ↾ 𝑏 ) ) )
20	9 18 19	syl2anc	⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( LBasis ‘ 𝑆 ) ) → ( ♯ ‘ 𝑏 ) = ( ♯ ‘ ran ( 𝐹 ↾ 𝑏 ) ) )
21		df-ima	⊢ ( 𝐹 “ 𝑏 ) = ran ( 𝐹 ↾ 𝑏 )
22	21	fveq2i	⊢ ( ♯ ‘ ( 𝐹 “ 𝑏 ) ) = ( ♯ ‘ ran ( 𝐹 ↾ 𝑏 ) )
23	20 22	eqtr4di	⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( LBasis ‘ 𝑆 ) ) → ( ♯ ‘ 𝑏 ) = ( ♯ ‘ ( 𝐹 “ 𝑏 ) ) )
24	3	dimval	⊢ ( ( 𝑆 ∈ LVec ∧ 𝑏 ∈ ( LBasis ‘ 𝑆 ) ) → ( dim ‘ 𝑆 ) = ( ♯ ‘ 𝑏 ) )
25	2 24	sylan	⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( LBasis ‘ 𝑆 ) ) → ( dim ‘ 𝑆 ) = ( ♯ ‘ 𝑏 ) )
26		lmimlmhm	⊢ ( 𝐹 ∈ ( 𝑆 LMIso 𝑇 ) → 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) )
27	1 26	syl	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) )
28		lmhmlvec	⊢ ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) → ( 𝑆 ∈ LVec ↔ 𝑇 ∈ LVec ) )
29	28	biimpa	⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑆 ∈ LVec ) → 𝑇 ∈ LVec )
30	27 2 29	syl2anc	⊢ ( 𝜑 → 𝑇 ∈ LVec )
31	30	adantr	⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( LBasis ‘ 𝑆 ) ) → 𝑇 ∈ LVec )
32		eqid	⊢ ( LBasis ‘ 𝑇 ) = ( LBasis ‘ 𝑇 )
33	3 32	lmimlbs	⊢ ( ( 𝐹 ∈ ( 𝑆 LMIso 𝑇 ) ∧ 𝑏 ∈ ( LBasis ‘ 𝑆 ) ) → ( 𝐹 “ 𝑏 ) ∈ ( LBasis ‘ 𝑇 ) )
34	1 33	sylan	⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( LBasis ‘ 𝑆 ) ) → ( 𝐹 “ 𝑏 ) ∈ ( LBasis ‘ 𝑇 ) )
35	32	dimval	⊢ ( ( 𝑇 ∈ LVec ∧ ( 𝐹 “ 𝑏 ) ∈ ( LBasis ‘ 𝑇 ) ) → ( dim ‘ 𝑇 ) = ( ♯ ‘ ( 𝐹 “ 𝑏 ) ) )
36	31 34 35	syl2anc	⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( LBasis ‘ 𝑆 ) ) → ( dim ‘ 𝑇 ) = ( ♯ ‘ ( 𝐹 “ 𝑏 ) ) )
37	23 25 36	3eqtr4d	⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( LBasis ‘ 𝑆 ) ) → ( dim ‘ 𝑆 ) = ( dim ‘ 𝑇 ) )
38	7 37	exlimddv	⊢ ( 𝜑 → ( dim ‘ 𝑆 ) = ( dim ‘ 𝑇 ) )