Metamath Proof Explorer

Theorem lvecendof1f1o

Description: If an endomorphism U of a vector space E of finite dimension is injective, then it is bijective. Item (b) of Corollary of Proposition 9 in BourbakiAlg1 p. 298 . (Contributed by Thierry Arnoux, 3-Aug-2025)

Ref Expression
Hypotheses lvecendof1f1o.b ⊢ 𝐵 = ( Base ‘ 𝐸 )
lvecendof1f1o.e ⊢ ( 𝜑 → 𝐸 ∈ LVec )
lvecendof1f1o.d ⊢ ( 𝜑 → ( dim ‘ 𝐸 ) ∈ ℕ0 )
lvecendof1f1o.u ⊢ ( 𝜑 → 𝑈 ∈ ( 𝐸 LMHom 𝐸 ) )
lvecendof1f1o.1 ⊢ ( 𝜑 → 𝑈 : 𝐵 –1-1→ 𝐵 )
Assertion lvecendof1f1o ( 𝜑 → 𝑈 : 𝐵 –1-1-onto→ 𝐵 )

Proof

Step Hyp Ref Expression
1 lvecendof1f1o.b ⊢ 𝐵 = ( Base ‘ 𝐸 )
2 lvecendof1f1o.e ⊢ ( 𝜑 → 𝐸 ∈ LVec )
3 lvecendof1f1o.d ⊢ ( 𝜑 → ( dim ‘ 𝐸 ) ∈ ℕ0 )
4 lvecendof1f1o.u ⊢ ( 𝜑 → 𝑈 ∈ ( 𝐸 LMHom 𝐸 ) )
5 lvecendof1f1o.1 ⊢ ( 𝜑 → 𝑈 : 𝐵 –1-1→ 𝐵 )
6 1 1 lmhmf ⊢ ( 𝑈 ∈ ( 𝐸 LMHom 𝐸 ) → 𝑈 : 𝐵 ⟶ 𝐵 )
7 4 6 syl ⊢ ( 𝜑 → 𝑈 : 𝐵 ⟶ 𝐵 )
8 7 ffnd ⊢ ( 𝜑 → 𝑈 Fn 𝐵 )
9 lmhmrnlss ⊢ ( 𝑈 ∈ ( 𝐸 LMHom 𝐸 ) → ran 𝑈 ∈ ( LSubSp ‘ 𝐸 ) )
10 4 9 syl ⊢ ( 𝜑 → ran 𝑈 ∈ ( LSubSp ‘ 𝐸 ) )
11 eqid ⊢ ( 0g ‘ 𝐸 ) = ( 0g ‘ 𝐸 )
12 eqid ⊢ ( 𝐸 ↾s ( ◡ 𝑈 “ { ( 0g ‘ 𝐸 ) } ) ) = ( 𝐸 ↾s ( ◡ 𝑈 “ { ( 0g ‘ 𝐸 ) } ) )
13 eqid ⊢ ( 𝐸 ↾s ran 𝑈 ) = ( 𝐸 ↾s ran 𝑈 )
14 11 12 13 dimkerim ⊢ ( ( 𝐸 ∈ LVec ∧ 𝑈 ∈ ( 𝐸 LMHom 𝐸 ) ) → ( dim ‘ 𝐸 ) = ( ( dim ‘ ( 𝐸 ↾s ( ◡ 𝑈 “ { ( 0g ‘ 𝐸 ) } ) ) ) +𝑒 ( dim ‘ ( 𝐸 ↾s ran 𝑈 ) ) ) )
15 2 4 14 syl2anc ⊢ ( 𝜑 → ( dim ‘ 𝐸 ) = ( ( dim ‘ ( 𝐸 ↾s ( ◡ 𝑈 “ { ( 0g ‘ 𝐸 ) } ) ) ) +𝑒 ( dim ‘ ( 𝐸 ↾s ran 𝑈 ) ) ) )
16 eqid ⊢ ( ◡ 𝑈 “ { ( 0g ‘ 𝐸 ) } ) = ( ◡ 𝑈 “ { ( 0g ‘ 𝐸 ) } )
17 eqid ⊢ ( LSubSp ‘ 𝐸 ) = ( LSubSp ‘ 𝐸 )
18 16 11 17 lmhmkerlss ⊢ ( 𝑈 ∈ ( 𝐸 LMHom 𝐸 ) → ( ◡ 𝑈 “ { ( 0g ‘ 𝐸 ) } ) ∈ ( LSubSp ‘ 𝐸 ) )
19 4 18 syl ⊢ ( 𝜑 → ( ◡ 𝑈 “ { ( 0g ‘ 𝐸 ) } ) ∈ ( LSubSp ‘ 𝐸 ) )
20 12 17 lsslvec ⊢ ( ( 𝐸 ∈ LVec ∧ ( ◡ 𝑈 “ { ( 0g ‘ 𝐸 ) } ) ∈ ( LSubSp ‘ 𝐸 ) ) → ( 𝐸 ↾s ( ◡ 𝑈 “ { ( 0g ‘ 𝐸 ) } ) ) ∈ LVec )
21 2 19 20 syl2anc ⊢ ( 𝜑 → ( 𝐸 ↾s ( ◡ 𝑈 “ { ( 0g ‘ 𝐸 ) } ) ) ∈ LVec )
22 4 lmhmghmd ⊢ ( 𝜑 → 𝑈 ∈ ( 𝐸 GrpHom 𝐸 ) )
23 1 1 11 11 kerf1ghm ⊢ ( 𝑈 ∈ ( 𝐸 GrpHom 𝐸 ) → ( 𝑈 : 𝐵 –1-1→ 𝐵 ↔ ( ◡ 𝑈 “ { ( 0g ‘ 𝐸 ) } ) = { ( 0g ‘ 𝐸 ) } ) )
24 23 biimpa ⊢ ( ( 𝑈 ∈ ( 𝐸 GrpHom 𝐸 ) ∧ 𝑈 : 𝐵 –1-1→ 𝐵 ) → ( ◡ 𝑈 “ { ( 0g ‘ 𝐸 ) } ) = { ( 0g ‘ 𝐸 ) } )
25 22 5 24 syl2anc ⊢ ( 𝜑 → ( ◡ 𝑈 “ { ( 0g ‘ 𝐸 ) } ) = { ( 0g ‘ 𝐸 ) } )
26 cnvimass ⊢ ( ◡ 𝑈 “ { ( 0g ‘ 𝐸 ) } ) ⊆ dom 𝑈
27 26 7 fssdm ⊢ ( 𝜑 → ( ◡ 𝑈 “ { ( 0g ‘ 𝐸 ) } ) ⊆ 𝐵 )
28 12 1 ressbas2 ⊢ ( ( ◡ 𝑈 “ { ( 0g ‘ 𝐸 ) } ) ⊆ 𝐵 → ( ◡ 𝑈 “ { ( 0g ‘ 𝐸 ) } ) = ( Base ‘ ( 𝐸 ↾s ( ◡ 𝑈 “ { ( 0g ‘ 𝐸 ) } ) ) ) )
29 27 28 syl ⊢ ( 𝜑 → ( ◡ 𝑈 “ { ( 0g ‘ 𝐸 ) } ) = ( Base ‘ ( 𝐸 ↾s ( ◡ 𝑈 “ { ( 0g ‘ 𝐸 ) } ) ) ) )
30 2 lvecgrpd ⊢ ( 𝜑 → 𝐸 ∈ Grp )
31 30 grpmndd ⊢ ( 𝜑 → 𝐸 ∈ Mnd )
32 1 11 mndidcl ⊢ ( 𝐸 ∈ Mnd → ( 0g ‘ 𝐸 ) ∈ 𝐵 )
33 31 32 syl ⊢ ( 𝜑 → ( 0g ‘ 𝐸 ) ∈ 𝐵 )
34 11 11 ghmid ⊢ ( 𝑈 ∈ ( 𝐸 GrpHom 𝐸 ) → ( 𝑈 ‘ ( 0g ‘ 𝐸 ) ) = ( 0g ‘ 𝐸 ) )
35 22 34 syl ⊢ ( 𝜑 → ( 𝑈 ‘ ( 0g ‘ 𝐸 ) ) = ( 0g ‘ 𝐸 ) )
36 fvex ⊢ ( 0g ‘ 𝐸 ) ∈ V
37 36 snid ⊢ ( 0g ‘ 𝐸 ) ∈ { ( 0g ‘ 𝐸 ) }
38 35 37 eqeltrdi ⊢ ( 𝜑 → ( 𝑈 ‘ ( 0g ‘ 𝐸 ) ) ∈ { ( 0g ‘ 𝐸 ) } )
39 8 33 38 elpreimad ⊢ ( 𝜑 → ( 0g ‘ 𝐸 ) ∈ ( ◡ 𝑈 “ { ( 0g ‘ 𝐸 ) } ) )
40 12 1 11 ress0g ⊢ ( ( 𝐸 ∈ Mnd ∧ ( 0g ‘ 𝐸 ) ∈ ( ◡ 𝑈 “ { ( 0g ‘ 𝐸 ) } ) ∧ ( ◡ 𝑈 “ { ( 0g ‘ 𝐸 ) } ) ⊆ 𝐵 ) → ( 0g ‘ 𝐸 ) = ( 0g ‘ ( 𝐸 ↾s ( ◡ 𝑈 “ { ( 0g ‘ 𝐸 ) } ) ) ) )
41 31 39 27 40 syl3anc ⊢ ( 𝜑 → ( 0g ‘ 𝐸 ) = ( 0g ‘ ( 𝐸 ↾s ( ◡ 𝑈 “ { ( 0g ‘ 𝐸 ) } ) ) ) )
42 41 sneqd ⊢ ( 𝜑 → { ( 0g ‘ 𝐸 ) } = { ( 0g ‘ ( 𝐸 ↾s ( ◡ 𝑈 “ { ( 0g ‘ 𝐸 ) } ) ) ) } )
43 25 29 42 3eqtr3d ⊢ ( 𝜑 → ( Base ‘ ( 𝐸 ↾s ( ◡ 𝑈 “ { ( 0g ‘ 𝐸 ) } ) ) ) = { ( 0g ‘ ( 𝐸 ↾s ( ◡ 𝑈 “ { ( 0g ‘ 𝐸 ) } ) ) ) } )
44 eqid ⊢ ( 0g ‘ ( 𝐸 ↾s ( ◡ 𝑈 “ { ( 0g ‘ 𝐸 ) } ) ) ) = ( 0g ‘ ( 𝐸 ↾s ( ◡ 𝑈 “ { ( 0g ‘ 𝐸 ) } ) ) )
45 44 lvecdim0 ⊢ ( ( 𝐸 ↾s ( ◡ 𝑈 “ { ( 0g ‘ 𝐸 ) } ) ) ∈ LVec → ( ( dim ‘ ( 𝐸 ↾s ( ◡ 𝑈 “ { ( 0g ‘ 𝐸 ) } ) ) ) = 0 ↔ ( Base ‘ ( 𝐸 ↾s ( ◡ 𝑈 “ { ( 0g ‘ 𝐸 ) } ) ) ) = { ( 0g ‘ ( 𝐸 ↾s ( ◡ 𝑈 “ { ( 0g ‘ 𝐸 ) } ) ) ) } ) )
46 45 biimpar ⊢ ( ( ( 𝐸 ↾s ( ◡ 𝑈 “ { ( 0g ‘ 𝐸 ) } ) ) ∈ LVec ∧ ( Base ‘ ( 𝐸 ↾s ( ◡ 𝑈 “ { ( 0g ‘ 𝐸 ) } ) ) ) = { ( 0g ‘ ( 𝐸 ↾s ( ◡ 𝑈 “ { ( 0g ‘ 𝐸 ) } ) ) ) } ) → ( dim ‘ ( 𝐸 ↾s ( ◡ 𝑈 “ { ( 0g ‘ 𝐸 ) } ) ) ) = 0 )
47 21 43 46 syl2anc ⊢ ( 𝜑 → ( dim ‘ ( 𝐸 ↾s ( ◡ 𝑈 “ { ( 0g ‘ 𝐸 ) } ) ) ) = 0 )
48 47 oveq1d ⊢ ( 𝜑 → ( ( dim ‘ ( 𝐸 ↾s ( ◡ 𝑈 “ { ( 0g ‘ 𝐸 ) } ) ) ) +𝑒 ( dim ‘ ( 𝐸 ↾s ran 𝑈 ) ) ) = ( 0 +𝑒 ( dim ‘ ( 𝐸 ↾s ran 𝑈 ) ) ) )
49 13 17 lsslvec ⊢ ( ( 𝐸 ∈ LVec ∧ ran 𝑈 ∈ ( LSubSp ‘ 𝐸 ) ) → ( 𝐸 ↾s ran 𝑈 ) ∈ LVec )
50 2 10 49 syl2anc ⊢ ( 𝜑 → ( 𝐸 ↾s ran 𝑈 ) ∈ LVec )
51 dimcl ⊢ ( ( 𝐸 ↾s ran 𝑈 ) ∈ LVec → ( dim ‘ ( 𝐸 ↾s ran 𝑈 ) ) ∈ ℕ0* )
52 xnn0xr ⊢ ( ( dim ‘ ( 𝐸 ↾s ran 𝑈 ) ) ∈ ℕ0* → ( dim ‘ ( 𝐸 ↾s ran 𝑈 ) ) ∈ ℝ* )
53 xaddlid ⊢ ( ( dim ‘ ( 𝐸 ↾s ran 𝑈 ) ) ∈ ℝ* → ( 0 +𝑒 ( dim ‘ ( 𝐸 ↾s ran 𝑈 ) ) ) = ( dim ‘ ( 𝐸 ↾s ran 𝑈 ) ) )
54 50 51 52 53 4syl ⊢ ( 𝜑 → ( 0 +𝑒 ( dim ‘ ( 𝐸 ↾s ran 𝑈 ) ) ) = ( dim ‘ ( 𝐸 ↾s ran 𝑈 ) ) )
55 15 48 54 3eqtrrd ⊢ ( 𝜑 → ( dim ‘ ( 𝐸 ↾s ran 𝑈 ) ) = ( dim ‘ 𝐸 ) )
56 1 2 3 10 55 dimlssid ⊢ ( 𝜑 → ran 𝑈 = 𝐵 )
57 df-fo ⊢ ( 𝑈 : 𝐵 –onto→ 𝐵 ↔ ( 𝑈 Fn 𝐵 ∧ ran 𝑈 = 𝐵 ) )
58 8 56 57 sylanbrc ⊢ ( 𝜑 → 𝑈 : 𝐵 –onto→ 𝐵 )
59 df-f1o ⊢ ( 𝑈 : 𝐵 –1-1-onto→ 𝐵 ↔ ( 𝑈 : 𝐵 –1-1→ 𝐵 ∧ 𝑈 : 𝐵 –onto→ 𝐵 ) )
60 5 58 59 sylanbrc ⊢ ( 𝜑 → 𝑈 : 𝐵 –1-1-onto→ 𝐵 )