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={\mathrm{Base}}_E$$
	lvecendof1f1o.e	$$⊢\phi \to E\in \mathrm{LVec}$$
	lvecendof1f1o.d	$$⊢\phi \to \dim \left(E\right)\in {\mathbb{N}}_0$$
	lvecendof1f1o.u	$$⊢\phi \to U\in \left(E\mathrm{LMHom}E\right)$$
	lvecendof1f1o.1	$$⊢\phi \to U:B\underset{1-1}{⟶}B$$
Assertion	lvecendof1f1o	$$⊢\phi \to U:B\underset{1-1\; onto}{⟶}B$$

Proof

Step	Hyp	Ref	Expression
1		lvecendof1f1o.b	$$⊢B={\mathrm{Base}}_E$$
2		lvecendof1f1o.e	$$⊢\phi \to E\in \mathrm{LVec}$$
3		lvecendof1f1o.d	$$⊢\phi \to \dim \left(E\right)\in {\mathbb{N}}_0$$
4		lvecendof1f1o.u	$$⊢\phi \to U\in \left(E\mathrm{LMHom}E\right)$$
5		lvecendof1f1o.1	$$⊢\phi \to U:B\underset{1-1}{⟶}B$$
6	1 1	lmhmf	$$⊢U\in \left(E\mathrm{LMHom}E\right)\to U:B⟶B$$
7	4 6	syl	$$⊢\phi \to U:B⟶B$$
8	7	ffnd	$$⊢\phi \to UFnB$$
9		lmhmrnlss	$$⊢U\in \left(E\mathrm{LMHom}E\right)\to \mathrm{ran}U\in \mathrm{LSubSp}\left(E\right)$$
10	4 9	syl	$$⊢\phi \to \mathrm{ran}U\in \mathrm{LSubSp}\left(E\right)$$
11		eqid	$$⊢0_E=0_E$$
12		eqid	$$⊢E{\upharpoonright }_{𝑠}{U}^{-1}\left[\left\{0_E\right\}\right]=E{\upharpoonright }_{𝑠}{U}^{-1}\left[\left\{0_E\right\}\right]$$
13		eqid	$$⊢E{\upharpoonright }_{𝑠}\mathrm{ran}U=E{\upharpoonright }_{𝑠}\mathrm{ran}U$$
14	11 12 13	dimkerim	$$⊢\left(E\in \mathrm{LVec}\wedge U\in \left(E\mathrm{LMHom}E\right)\right)\to \dim \left(E\right)=\dim \left(E{\upharpoonright }_{𝑠}{U}^{-1}\left[\left\{0_E\right\}\right]\right){+}_{𝑒}\dim \left(E{\upharpoonright }_{𝑠}\mathrm{ran}U\right)$$
15	2 4 14	syl2anc	$$⊢\phi \to \dim \left(E\right)=\dim \left(E{\upharpoonright }_{𝑠}{U}^{-1}\left[\left\{0_E\right\}\right]\right){+}_{𝑒}\dim \left(E{\upharpoonright }_{𝑠}\mathrm{ran}U\right)$$
16		eqid	$$⊢U^{-1}\left[\left\{0_E\right\}\right]=U^{-1}\left[\left\{0_E\right\}\right]$$
17		eqid	$$⊢\mathrm{LSubSp}\left(E\right)=\mathrm{LSubSp}\left(E\right)$$
18	16 11 17	lmhmkerlss	$$⊢U\in \left(E\mathrm{LMHom}E\right)\to U^{-1}\left[\left\{0_E\right\}\right]\in \mathrm{LSubSp}\left(E\right)$$
19	4 18	syl	$$⊢\phi \to U^{-1}\left[\left\{0_E\right\}\right]\in \mathrm{LSubSp}\left(E\right)$$
20	12 17	lsslvec	$$⊢\left(E\in \mathrm{LVec}\wedge U^{-1}\left[\left\{0_E\right\}\right]\in \mathrm{LSubSp}\left(E\right)\right)\to E{\upharpoonright }_{𝑠}{U}^{-1}\left[\left\{0_E\right\}\right]\in \mathrm{LVec}$$
21	2 19 20	syl2anc	$$⊢\phi \to E{\upharpoonright }_{𝑠}{U}^{-1}\left[\left\{0_E\right\}\right]\in \mathrm{LVec}$$
22	4	lmhmghmd	$$⊢\phi \to U\in \left(E\mathrm{GrpHom}E\right)$$
23	1 1 11 11	kerf1ghm	$$⊢U\in \left(E\mathrm{GrpHom}E\right)\to \left(U:B\underset{1-1}{⟶}B\leftrightarrow U^{-1}\left[\left\{0_E\right\}\right]=\left\{0_E\right\}\right)$$
24	23	biimpa	$$⊢\left(U\in \left(E\mathrm{GrpHom}E\right)\wedge U:B\underset{1-1}{⟶}B\right)\to U^{-1}\left[\left\{0_E\right\}\right]=\left\{0_E\right\}$$
25	22 5 24	syl2anc	$$⊢\phi \to U^{-1}\left[\left\{0_E\right\}\right]=\left\{0_E\right\}$$
26		cnvimass	$$⊢U^{-1}\left[\left\{0_E\right\}\right]\subseteq \mathrm{dom}U$$
27	26 7	fssdm	$$⊢\phi \to U^{-1}\left[\left\{0_E\right\}\right]\subseteq B$$
28	12 1	ressbas2	$$⊢U^{-1}\left[\left\{0_E\right\}\right]\subseteq B\to U^{-1}\left[\left\{0_E\right\}\right]={\mathrm{Base}}_{\left(E{\upharpoonright }_{𝑠}{U}^{-1}\left[\left\{0_E\right\}\right]\right)}$$
29	27 28	syl	$$⊢\phi \to U^{-1}\left[\left\{0_E\right\}\right]={\mathrm{Base}}_{\left(E{\upharpoonright }_{𝑠}{U}^{-1}\left[\left\{0_E\right\}\right]\right)}$$
30	2	lvecgrpd	$$⊢\phi \to E\in \mathrm{Grp}$$
31	30	grpmndd	$$⊢\phi \to E\in \mathrm{Mnd}$$
32	1 11	mndidcl	$$⊢E\in \mathrm{Mnd}\to 0_E\in B$$
33	31 32	syl	$$⊢\phi \to 0_E\in B$$
34	11 11	ghmid	$$⊢U\in \left(E\mathrm{GrpHom}E\right)\to U\left(0_E\right)=0_E$$
35	22 34	syl	$$⊢\phi \to U\left(0_E\right)=0_E$$
36		fvex	$$⊢0_E\in \mathrm{V}$$
37	36	snid	$$⊢0_E\in \left\{0_E\right\}$$
38	35 37	eqeltrdi	$$⊢\phi \to U\left(0_E\right)\in \left\{0_E\right\}$$
39	8 33 38	elpreimad	$$⊢\phi \to 0_E\in U^{-1}\left[\left\{0_E\right\}\right]$$
40	12 1 11	ress0g	$$⊢\left(E\in \mathrm{Mnd}\wedge 0_E\in U^{-1}\left[\left\{0_E\right\}\right]\wedge U^{-1}\left[\left\{0_E\right\}\right]\subseteq B\right)\to 0_E=0_{\left(E{\upharpoonright }_{𝑠}{U}^{-1}\left[\left\{0_E\right\}\right]\right)}$$
41	31 39 27 40	syl3anc	$$⊢\phi \to 0_E=0_{\left(E{\upharpoonright }_{𝑠}{U}^{-1}\left[\left\{0_E\right\}\right]\right)}$$
42	41	sneqd	$$⊢\phi \to \left\{0_E\right\}=\left\{0_{\left(E{\upharpoonright }_{𝑠}{U}^{-1}\left[\left\{0_E\right\}\right]\right)}\right\}$$
43	25 29 42	3eqtr3d	$$⊢\phi \to {\mathrm{Base}}_{\left(E{\upharpoonright }_{𝑠}{U}^{-1}\left[\left\{0_E\right\}\right]\right)}=\left\{0_{\left(E{\upharpoonright }_{𝑠}{U}^{-1}\left[\left\{0_E\right\}\right]\right)}\right\}$$
44		eqid	$$⊢0_{\left(E{\upharpoonright }_{𝑠}{U}^{-1}\left[\left\{0_E\right\}\right]\right)}=0_{\left(E{\upharpoonright }_{𝑠}{U}^{-1}\left[\left\{0_E\right\}\right]\right)}$$
45	44	lvecdim0	$$⊢E{\upharpoonright }_{𝑠}{U}^{-1}\left[\left\{0_E\right\}\right]\in \mathrm{LVec}\to \left(\dim \left(E{\upharpoonright }_{𝑠}{U}^{-1}\left[\left\{0_E\right\}\right]\right)=0\leftrightarrow {\mathrm{Base}}_{\left(E{\upharpoonright }_{𝑠}{U}^{-1}\left[\left\{0_E\right\}\right]\right)}=\left\{0_{\left(E{\upharpoonright }_{𝑠}{U}^{-1}\left[\left\{0_E\right\}\right]\right)}\right\}\right)$$
46	45	biimpar	$$⊢\left(E{\upharpoonright }_{𝑠}{U}^{-1}\left[\left\{0_E\right\}\right]\in \mathrm{LVec}\wedge {\mathrm{Base}}_{\left(E{\upharpoonright }_{𝑠}{U}^{-1}\left[\left\{0_E\right\}\right]\right)}=\left\{0_{\left(E{\upharpoonright }_{𝑠}{U}^{-1}\left[\left\{0_E\right\}\right]\right)}\right\}\right)\to \dim \left(E{\upharpoonright }_{𝑠}{U}^{-1}\left[\left\{0_E\right\}\right]\right)=0$$
47	21 43 46	syl2anc	$$⊢\phi \to \dim \left(E{\upharpoonright }_{𝑠}{U}^{-1}\left[\left\{0_E\right\}\right]\right)=0$$
48	47	oveq1d	$$⊢\phi \to \dim \left(E{\upharpoonright }_{𝑠}{U}^{-1}\left[\left\{0_E\right\}\right]\right){+}_{𝑒}\dim \left(E{\upharpoonright }_{𝑠}\mathrm{ran}U\right)=0{+}_{𝑒}\dim \left(E{\upharpoonright }_{𝑠}\mathrm{ran}U\right)$$
49	13 17	lsslvec	$$⊢\left(E\in \mathrm{LVec}\wedge \mathrm{ran}U\in \mathrm{LSubSp}\left(E\right)\right)\to E{\upharpoonright }_{𝑠}\mathrm{ran}U\in \mathrm{LVec}$$
50	2 10 49	syl2anc	$$⊢\phi \to E{\upharpoonright }_{𝑠}\mathrm{ran}U\in \mathrm{LVec}$$
51		dimcl	$$⊢E{\upharpoonright }_{𝑠}\mathrm{ran}U\in \mathrm{LVec}\to \dim \left(E{\upharpoonright }_{𝑠}\mathrm{ran}U\right)\in {\mathbb{N}}_0^{*}$$
52		xnn0xr	$$⊢\dim \left(E{\upharpoonright }_{𝑠}\mathrm{ran}U\right)\in {\mathbb{N}}_0^{*}\to \dim \left(E{\upharpoonright }_{𝑠}\mathrm{ran}U\right)\in {ℝ}^{*}$$
53		xaddlid	$$⊢\dim \left(E{\upharpoonright }_{𝑠}\mathrm{ran}U\right)\in {ℝ}^{*}\to 0{+}_{𝑒}\dim \left(E{\upharpoonright }_{𝑠}\mathrm{ran}U\right)=\dim \left(E{\upharpoonright }_{𝑠}\mathrm{ran}U\right)$$
54	50 51 52 53	4syl	$$⊢\phi \to 0{+}_{𝑒}\dim \left(E{\upharpoonright }_{𝑠}\mathrm{ran}U\right)=\dim \left(E{\upharpoonright }_{𝑠}\mathrm{ran}U\right)$$
55	15 48 54	3eqtrrd	$$⊢\phi \to \dim \left(E{\upharpoonright }_{𝑠}\mathrm{ran}U\right)=\dim \left(E\right)$$
56	1 2 3 10 55	dimlssid	$$⊢\phi \to \mathrm{ran}U=B$$
57		df-fo	$$⊢U:B\underset{onto}{⟶}B\leftrightarrow \left(UFnB\wedge \mathrm{ran}U=B\right)$$
58	8 56 57	sylanbrc	$$⊢\phi \to U:B\underset{onto}{⟶}B$$
59		df-f1o	$$⊢U:B\underset{1-1\; onto}{⟶}B\leftrightarrow \left(U:B\underset{1-1}{⟶}B\wedge U:B\underset{onto}{⟶}B\right)$$
60	5 58 59	sylanbrc	$$⊢\phi \to U:B\underset{1-1\; onto}{⟶}B$$