Theorem assarrginv

Description: If an element X of an associative algebra A over a division ring K is regular, then it is a unit. Proposition 2. in Chapter 5. of BourbakiAlg2 p. 113. (Contributed by Thierry Arnoux, 3-Aug-2025)

	Ref	Expression
Hypotheses	assarrginv.1	$$⊢E=\mathrm{RLReg}\left(A\right)$$
	assarrginv.2	$$⊢U=\mathrm{Unit}\left(A\right)$$
	assarrginv.3	$$⊢K=\mathrm{Scalar}\left(A\right)$$
	assarrginv.4	$$⊢\phi \to A\in \mathrm{AssAlg}$$
	assarrginv.5	$$⊢\phi \to K\in \mathrm{DivRing}$$
	assarrginv.6	$$⊢\phi \to \dim \left(A\right)\in {\mathbb{N}}_0$$
	assarrginv.7	$$⊢\phi \to X\in E$$
Assertion	assarrginv	$$⊢\phi \to X\in U$$

Proof

Step	Hyp	Ref	Expression
1		assarrginv.1	$$⊢E=\mathrm{RLReg}\left(A\right)$$
2		assarrginv.2	$$⊢U=\mathrm{Unit}\left(A\right)$$
3		assarrginv.3	$$⊢K=\mathrm{Scalar}\left(A\right)$$
4		assarrginv.4	$$⊢\phi \to A\in \mathrm{AssAlg}$$
5		assarrginv.5	$$⊢\phi \to K\in \mathrm{DivRing}$$
6		assarrginv.6	$$⊢\phi \to \dim \left(A\right)\in {\mathbb{N}}_0$$
7		assarrginv.7	$$⊢\phi \to X\in E$$
8		eqid	$$⊢{\mathrm{Base}}_A={\mathrm{Base}}_A$$
9		eqid	$$⊢{\cdot }_A={\cdot }_A$$
10		eqid	$$⊢\left(a\in {\mathrm{Base}}_A⟼X{\cdot }_{A}a\right)=\left(a\in {\mathrm{Base}}_A⟼X{\cdot }_{A}a\right)$$
11	8 9 10 4 1 3 5 6 7	assalactf1o	$$⊢\phi \to \left(a\in {\mathrm{Base}}_A⟼X{\cdot }_{A}a\right):{\mathrm{Base}}_A\underset{1-1\; onto}{⟶}{\mathrm{Base}}_A$$
12		eqid	$$⊢{\mathrm{mulGrp}}_A={\mathrm{mulGrp}}_A$$
13	12 8	mgpbas	$$⊢{\mathrm{Base}}_A={\mathrm{Base}}_{{\mathrm{mulGrp}}_A}$$
14		eqid	$$⊢1_A=1_A$$
15	12 14	ringidval	$$⊢1_A=0_{{\mathrm{mulGrp}}_A}$$
16	12 9	mgpplusg	$$⊢{\cdot }_A={+}_{{\mathrm{mulGrp}}_A}$$
17		oveq2	$$⊢a=b\to X{\cdot }_{A}a=X{\cdot }_{A}b$$
18	17	cbvmptv	$$⊢\left(a\in {\mathrm{Base}}_A⟼X{\cdot }_{A}a\right)=\left(b\in {\mathrm{Base}}_A⟼X{\cdot }_{A}b\right)$$
19		assaring	$$⊢A\in \mathrm{AssAlg}\to A\in \mathrm{Ring}$$
20	4 19	syl	$$⊢\phi \to A\in \mathrm{Ring}$$
21	12	ringmgp	$$⊢A\in \mathrm{Ring}\to {\mathrm{mulGrp}}_A\in \mathrm{Mnd}$$
22	20 21	syl	$$⊢\phi \to {\mathrm{mulGrp}}_A\in \mathrm{Mnd}$$
23	1 8	rrgss	$$⊢E\subseteq {\mathrm{Base}}_A$$
24	23 7	sselid	$$⊢\phi \to X\in {\mathrm{Base}}_A$$
25	13 15 16 18 22 24	mndlactf1o	$$⊢\phi \to \left(\left(a\in {\mathrm{Base}}_A⟼X{\cdot }_{A}a\right):{\mathrm{Base}}_A\underset{1-1\; onto}{⟶}{\mathrm{Base}}_A\leftrightarrow \exists z\in {\mathrm{Base}}_A\left(X{\cdot }_{A}z=1_A\wedge z{\cdot }_{A}X=1_A\right)\right)$$
26	11 25	mpbid	$$⊢\phi \to \exists z\in {\mathrm{Base}}_A\left(X{\cdot }_{A}z=1_A\wedge z{\cdot }_{A}X=1_A\right)$$
27	8 2 9 14 24 20	isunit3	$$⊢\phi \to \left(X\in U\leftrightarrow \exists z\in {\mathrm{Base}}_A\left(X{\cdot }_{A}z=1_A\wedge z{\cdot }_{A}X=1_A\right)\right)$$
28	26 27	mpbird	$$⊢\phi \to X\in U$$