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 
|- B = ( Base ` E )
lvecendof1f1o.e 
|- ( ph -> E e. LVec )
lvecendof1f1o.d 
|- ( ph -> ( dim ` E ) e. NN0 )
lvecendof1f1o.u 
|- ( ph -> U e. ( E LMHom E ) )
lvecendof1f1o.1 
|- ( ph -> U : B -1-1-> B )
Assertion lvecendof1f1o 
|- ( ph -> U : B -1-1-onto-> B )

Proof

Step Hyp Ref Expression
1 lvecendof1f1o.b 
 |-  B = ( Base ` E )
2 lvecendof1f1o.e 
 |-  ( ph -> E e. LVec )
3 lvecendof1f1o.d 
 |-  ( ph -> ( dim ` E ) e. NN0 )
4 lvecendof1f1o.u 
 |-  ( ph -> U e. ( E LMHom E ) )
5 lvecendof1f1o.1 
 |-  ( ph -> U : B -1-1-> B )
6 1 1 lmhmf 
 |-  ( U e. ( E LMHom E ) -> U : B --> B )
7 4 6 syl 
 |-  ( ph -> U : B --> B )
8 7 ffnd 
 |-  ( ph -> U Fn B )
9 lmhmrnlss 
 |-  ( U e. ( E LMHom E ) -> ran U e. ( LSubSp ` E ) )
10 4 9 syl 
 |-  ( ph -> ran U e. ( LSubSp ` E ) )
11 eqid 
 |-  ( 0g ` E ) = ( 0g ` E )
12 eqid 
 |-  ( E |`s ( `' U " { ( 0g ` E ) } ) ) = ( E |`s ( `' U " { ( 0g ` E ) } ) )
13 eqid 
 |-  ( E |`s ran U ) = ( E |`s ran U )
14 11 12 13 dimkerim 
 |-  ( ( E e. LVec /\ U e. ( E LMHom E ) ) -> ( dim ` E ) = ( ( dim ` ( E |`s ( `' U " { ( 0g ` E ) } ) ) ) +e ( dim ` ( E |`s ran U ) ) ) )
15 2 4 14 syl2anc 
 |-  ( ph -> ( dim ` E ) = ( ( dim ` ( E |`s ( `' U " { ( 0g ` E ) } ) ) ) +e ( dim ` ( E |`s ran U ) ) ) )
16 eqid 
 |-  ( `' U " { ( 0g ` E ) } ) = ( `' U " { ( 0g ` E ) } )
17 eqid 
 |-  ( LSubSp ` E ) = ( LSubSp ` E )
18 16 11 17 lmhmkerlss 
 |-  ( U e. ( E LMHom E ) -> ( `' U " { ( 0g ` E ) } ) e. ( LSubSp ` E ) )
19 4 18 syl 
 |-  ( ph -> ( `' U " { ( 0g ` E ) } ) e. ( LSubSp ` E ) )
20 12 17 lsslvec 
 |-  ( ( E e. LVec /\ ( `' U " { ( 0g ` E ) } ) e. ( LSubSp ` E ) ) -> ( E |`s ( `' U " { ( 0g ` E ) } ) ) e. LVec )
21 2 19 20 syl2anc 
 |-  ( ph -> ( E |`s ( `' U " { ( 0g ` E ) } ) ) e. LVec )
22 4 lmhmghmd 
 |-  ( ph -> U e. ( E GrpHom E ) )
23 1 1 11 11 kerf1ghm 
 |-  ( U e. ( E GrpHom E ) -> ( U : B -1-1-> B <-> ( `' U " { ( 0g ` E ) } ) = { ( 0g ` E ) } ) )
24 23 biimpa 
 |-  ( ( U e. ( E GrpHom E ) /\ U : B -1-1-> B ) -> ( `' U " { ( 0g ` E ) } ) = { ( 0g ` E ) } )
25 22 5 24 syl2anc 
 |-  ( ph -> ( `' U " { ( 0g ` E ) } ) = { ( 0g ` E ) } )
26 cnvimass 
 |-  ( `' U " { ( 0g ` E ) } ) C_ dom U
27 26 7 fssdm 
 |-  ( ph -> ( `' U " { ( 0g ` E ) } ) C_ B )
28 12 1 ressbas2 
 |-  ( ( `' U " { ( 0g ` E ) } ) C_ B -> ( `' U " { ( 0g ` E ) } ) = ( Base ` ( E |`s ( `' U " { ( 0g ` E ) } ) ) ) )
29 27 28 syl 
 |-  ( ph -> ( `' U " { ( 0g ` E ) } ) = ( Base ` ( E |`s ( `' U " { ( 0g ` E ) } ) ) ) )
30 2 lvecgrpd 
 |-  ( ph -> E e. Grp )
31 30 grpmndd 
 |-  ( ph -> E e. Mnd )
32 1 11 mndidcl 
 |-  ( E e. Mnd -> ( 0g ` E ) e. B )
33 31 32 syl 
 |-  ( ph -> ( 0g ` E ) e. B )
34 11 11 ghmid 
 |-  ( U e. ( E GrpHom E ) -> ( U ` ( 0g ` E ) ) = ( 0g ` E ) )
35 22 34 syl 
 |-  ( ph -> ( U ` ( 0g ` E ) ) = ( 0g ` E ) )
36 fvex 
 |-  ( 0g ` E ) e. _V
37 36 snid 
 |-  ( 0g ` E ) e. { ( 0g ` E ) }
38 35 37 eqeltrdi 
 |-  ( ph -> ( U ` ( 0g ` E ) ) e. { ( 0g ` E ) } )
39 8 33 38 elpreimad 
 |-  ( ph -> ( 0g ` E ) e. ( `' U " { ( 0g ` E ) } ) )
40 12 1 11 ress0g 
 |-  ( ( E e. Mnd /\ ( 0g ` E ) e. ( `' U " { ( 0g ` E ) } ) /\ ( `' U " { ( 0g ` E ) } ) C_ B ) -> ( 0g ` E ) = ( 0g ` ( E |`s ( `' U " { ( 0g ` E ) } ) ) ) )
41 31 39 27 40 syl3anc 
 |-  ( ph -> ( 0g ` E ) = ( 0g ` ( E |`s ( `' U " { ( 0g ` E ) } ) ) ) )
42 41 sneqd 
 |-  ( ph -> { ( 0g ` E ) } = { ( 0g ` ( E |`s ( `' U " { ( 0g ` E ) } ) ) ) } )
43 25 29 42 3eqtr3d 
 |-  ( ph -> ( Base ` ( E |`s ( `' U " { ( 0g ` E ) } ) ) ) = { ( 0g ` ( E |`s ( `' U " { ( 0g ` E ) } ) ) ) } )
44 eqid 
 |-  ( 0g ` ( E |`s ( `' U " { ( 0g ` E ) } ) ) ) = ( 0g ` ( E |`s ( `' U " { ( 0g ` E ) } ) ) )
45 44 lvecdim0 
 |-  ( ( E |`s ( `' U " { ( 0g ` E ) } ) ) e. LVec -> ( ( dim ` ( E |`s ( `' U " { ( 0g ` E ) } ) ) ) = 0 <-> ( Base ` ( E |`s ( `' U " { ( 0g ` E ) } ) ) ) = { ( 0g ` ( E |`s ( `' U " { ( 0g ` E ) } ) ) ) } ) )
46 45 biimpar 
 |-  ( ( ( E |`s ( `' U " { ( 0g ` E ) } ) ) e. LVec /\ ( Base ` ( E |`s ( `' U " { ( 0g ` E ) } ) ) ) = { ( 0g ` ( E |`s ( `' U " { ( 0g ` E ) } ) ) ) } ) -> ( dim ` ( E |`s ( `' U " { ( 0g ` E ) } ) ) ) = 0 )
47 21 43 46 syl2anc 
 |-  ( ph -> ( dim ` ( E |`s ( `' U " { ( 0g ` E ) } ) ) ) = 0 )
48 47 oveq1d 
 |-  ( ph -> ( ( dim ` ( E |`s ( `' U " { ( 0g ` E ) } ) ) ) +e ( dim ` ( E |`s ran U ) ) ) = ( 0 +e ( dim ` ( E |`s ran U ) ) ) )
49 13 17 lsslvec 
 |-  ( ( E e. LVec /\ ran U e. ( LSubSp ` E ) ) -> ( E |`s ran U ) e. LVec )
50 2 10 49 syl2anc 
 |-  ( ph -> ( E |`s ran U ) e. LVec )
51 dimcl 
 |-  ( ( E |`s ran U ) e. LVec -> ( dim ` ( E |`s ran U ) ) e. NN0* )
52 xnn0xr 
 |-  ( ( dim ` ( E |`s ran U ) ) e. NN0* -> ( dim ` ( E |`s ran U ) ) e. RR* )
53 xaddlid 
 |-  ( ( dim ` ( E |`s ran U ) ) e. RR* -> ( 0 +e ( dim ` ( E |`s ran U ) ) ) = ( dim ` ( E |`s ran U ) ) )
54 50 51 52 53 4syl 
 |-  ( ph -> ( 0 +e ( dim ` ( E |`s ran U ) ) ) = ( dim ` ( E |`s ran U ) ) )
55 15 48 54 3eqtrrd 
 |-  ( ph -> ( dim ` ( E |`s ran U ) ) = ( dim ` E ) )
56 1 2 3 10 55 dimlssid 
 |-  ( ph -> ran U = B )
57 df-fo 
 |-  ( U : B -onto-> B <-> ( U Fn B /\ ran U = B ) )
58 8 56 57 sylanbrc 
 |-  ( ph -> U : B -onto-> B )
59 df-f1o 
 |-  ( U : B -1-1-onto-> B <-> ( U : B -1-1-> B /\ U : B -onto-> B ) )
60 5 58 59 sylanbrc 
 |-  ( ph -> U : B -1-1-onto-> B )