This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 = ( RLReg ` A )
assarrginv.2 
|- U = ( Unit ` A )
assarrginv.3 
|- K = ( Scalar ` A )
assarrginv.4 
|- ( ph -> A e. AssAlg )
assarrginv.5 
|- ( ph -> K e. DivRing )
assarrginv.6 
|- ( ph -> ( dim ` A ) e. NN0 )
assarrginv.7 
|- ( ph -> X e. E )
Assertion assarrginv 
|- ( ph -> X e. U )

Proof

Step Hyp Ref Expression
1 assarrginv.1 
 |-  E = ( RLReg ` A )
2 assarrginv.2 
 |-  U = ( Unit ` A )
3 assarrginv.3 
 |-  K = ( Scalar ` A )
4 assarrginv.4 
 |-  ( ph -> A e. AssAlg )
5 assarrginv.5 
 |-  ( ph -> K e. DivRing )
6 assarrginv.6 
 |-  ( ph -> ( dim ` A ) e. NN0 )
7 assarrginv.7 
 |-  ( ph -> X e. E )
8 eqid 
 |-  ( Base ` A ) = ( Base ` A )
9 eqid 
 |-  ( .r ` A ) = ( .r ` A )
10 eqid 
 |-  ( a e. ( Base ` A ) |-> ( X ( .r ` A ) a ) ) = ( a e. ( Base ` A ) |-> ( X ( .r ` A ) a ) )
11 8 9 10 4 1 3 5 6 7 assalactf1o 
 |-  ( ph -> ( a e. ( Base ` A ) |-> ( X ( .r ` A ) a ) ) : ( Base ` A ) -1-1-onto-> ( Base ` A ) )
12 eqid 
 |-  ( mulGrp ` A ) = ( mulGrp ` A )
13 12 8 mgpbas 
 |-  ( Base ` A ) = ( Base ` ( mulGrp ` A ) )
14 eqid 
 |-  ( 1r ` A ) = ( 1r ` A )
15 12 14 ringidval 
 |-  ( 1r ` A ) = ( 0g ` ( mulGrp ` A ) )
16 12 9 mgpplusg 
 |-  ( .r ` A ) = ( +g ` ( mulGrp ` A ) )
17 oveq2 
 |-  ( a = b -> ( X ( .r ` A ) a ) = ( X ( .r ` A ) b ) )
18 17 cbvmptv 
 |-  ( a e. ( Base ` A ) |-> ( X ( .r ` A ) a ) ) = ( b e. ( Base ` A ) |-> ( X ( .r ` A ) b ) )
19 assaring 
 |-  ( A e. AssAlg -> A e. Ring )
20 4 19 syl 
 |-  ( ph -> A e. Ring )
21 12 ringmgp 
 |-  ( A e. Ring -> ( mulGrp ` A ) e. Mnd )
22 20 21 syl 
 |-  ( ph -> ( mulGrp ` A ) e. Mnd )
23 1 8 rrgss 
 |-  E C_ ( Base ` A )
24 23 7 sselid 
 |-  ( ph -> X e. ( Base ` A ) )
25 13 15 16 18 22 24 mndlactf1o 
 |-  ( ph -> ( ( a e. ( Base ` A ) |-> ( X ( .r ` A ) a ) ) : ( Base ` A ) -1-1-onto-> ( Base ` A ) <-> E. z e. ( Base ` A ) ( ( X ( .r ` A ) z ) = ( 1r ` A ) /\ ( z ( .r ` A ) X ) = ( 1r ` A ) ) ) )
26 11 25 mpbid 
 |-  ( ph -> E. z e. ( Base ` A ) ( ( X ( .r ` A ) z ) = ( 1r ` A ) /\ ( z ( .r ` A ) X ) = ( 1r ` A ) ) )
27 8 2 9 14 24 20 isunit3 
 |-  ( ph -> ( X e. U <-> E. z e. ( Base ` A ) ( ( X ( .r ` A ) z ) = ( 1r ` A ) /\ ( z ( .r ` A ) X ) = ( 1r ` A ) ) ) )
28 26 27 mpbird 
 |-  ( ph -> X e. U )