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	⊢ 𝐸 = ( RLReg ‘ 𝐴 )
	assarrginv.2	⊢ 𝑈 = ( Unit ‘ 𝐴 )
	assarrginv.3	⊢ 𝐾 = ( Scalar ‘ 𝐴 )
	assarrginv.4	⊢ ( 𝜑 → 𝐴 ∈ AssAlg )
	assarrginv.5	⊢ ( 𝜑 → 𝐾 ∈ DivRing )
	assarrginv.6	⊢ ( 𝜑 → ( dim ‘ 𝐴 ) ∈ ℕ0 )
	assarrginv.7	⊢ ( 𝜑 → 𝑋 ∈ 𝐸 )
Assertion	assarrginv	⊢ ( 𝜑 → 𝑋 ∈ 𝑈 )

Proof

Step	Hyp	Ref	Expression
1		assarrginv.1	⊢ 𝐸 = ( RLReg ‘ 𝐴 )
2		assarrginv.2	⊢ 𝑈 = ( Unit ‘ 𝐴 )
3		assarrginv.3	⊢ 𝐾 = ( Scalar ‘ 𝐴 )
4		assarrginv.4	⊢ ( 𝜑 → 𝐴 ∈ AssAlg )
5		assarrginv.5	⊢ ( 𝜑 → 𝐾 ∈ DivRing )
6		assarrginv.6	⊢ ( 𝜑 → ( dim ‘ 𝐴 ) ∈ ℕ0 )
7		assarrginv.7	⊢ ( 𝜑 → 𝑋 ∈ 𝐸 )
8		eqid	⊢ ( Base ‘ 𝐴 ) = ( Base ‘ 𝐴 )
9		eqid	⊢ ( .r ‘ 𝐴 ) = ( .r ‘ 𝐴 )
10		eqid	⊢ ( 𝑎 ∈ ( Base ‘ 𝐴 ) ↦ ( 𝑋 ( .r ‘ 𝐴 ) 𝑎 ) ) = ( 𝑎 ∈ ( Base ‘ 𝐴 ) ↦ ( 𝑋 ( .r ‘ 𝐴 ) 𝑎 ) )
11	8 9 10 4 1 3 5 6 7	assalactf1o	⊢ ( 𝜑 → ( 𝑎 ∈ ( Base ‘ 𝐴 ) ↦ ( 𝑋 ( .r ‘ 𝐴 ) 𝑎 ) ) : ( Base ‘ 𝐴 ) –1-1-onto→ ( Base ‘ 𝐴 ) )
12		eqid	⊢ ( mulGrp ‘ 𝐴 ) = ( mulGrp ‘ 𝐴 )
13	12 8	mgpbas	⊢ ( Base ‘ 𝐴 ) = ( Base ‘ ( mulGrp ‘ 𝐴 ) )
14		eqid	⊢ ( 1r ‘ 𝐴 ) = ( 1r ‘ 𝐴 )
15	12 14	ringidval	⊢ ( 1r ‘ 𝐴 ) = ( 0g ‘ ( mulGrp ‘ 𝐴 ) )
16	12 9	mgpplusg	⊢ ( .r ‘ 𝐴 ) = ( +g ‘ ( mulGrp ‘ 𝐴 ) )
17		oveq2	⊢ ( 𝑎 = 𝑏 → ( 𝑋 ( .r ‘ 𝐴 ) 𝑎 ) = ( 𝑋 ( .r ‘ 𝐴 ) 𝑏 ) )
18	17	cbvmptv	⊢ ( 𝑎 ∈ ( Base ‘ 𝐴 ) ↦ ( 𝑋 ( .r ‘ 𝐴 ) 𝑎 ) ) = ( 𝑏 ∈ ( Base ‘ 𝐴 ) ↦ ( 𝑋 ( .r ‘ 𝐴 ) 𝑏 ) )
19		assaring	⊢ ( 𝐴 ∈ AssAlg → 𝐴 ∈ Ring )
20	4 19	syl	⊢ ( 𝜑 → 𝐴 ∈ Ring )
21	12	ringmgp	⊢ ( 𝐴 ∈ Ring → ( mulGrp ‘ 𝐴 ) ∈ Mnd )
22	20 21	syl	⊢ ( 𝜑 → ( mulGrp ‘ 𝐴 ) ∈ Mnd )
23	1 8	rrgss	⊢ 𝐸 ⊆ ( Base ‘ 𝐴 )
24	23 7	sselid	⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝐴 ) )
25	13 15 16 18 22 24	mndlactf1o	⊢ ( 𝜑 → ( ( 𝑎 ∈ ( Base ‘ 𝐴 ) ↦ ( 𝑋 ( .r ‘ 𝐴 ) 𝑎 ) ) : ( Base ‘ 𝐴 ) –1-1-onto→ ( Base ‘ 𝐴 ) ↔ ∃ 𝑧 ∈ ( Base ‘ 𝐴 ) ( ( 𝑋 ( .r ‘ 𝐴 ) 𝑧 ) = ( 1r ‘ 𝐴 ) ∧ ( 𝑧 ( .r ‘ 𝐴 ) 𝑋 ) = ( 1r ‘ 𝐴 ) ) ) )
26	11 25	mpbid	⊢ ( 𝜑 → ∃ 𝑧 ∈ ( Base ‘ 𝐴 ) ( ( 𝑋 ( .r ‘ 𝐴 ) 𝑧 ) = ( 1r ‘ 𝐴 ) ∧ ( 𝑧 ( .r ‘ 𝐴 ) 𝑋 ) = ( 1r ‘ 𝐴 ) ) )
27	8 2 9 14 24 20	isunit3	⊢ ( 𝜑 → ( 𝑋 ∈ 𝑈 ↔ ∃ 𝑧 ∈ ( Base ‘ 𝐴 ) ( ( 𝑋 ( .r ‘ 𝐴 ) 𝑧 ) = ( 1r ‘ 𝐴 ) ∧ ( 𝑧 ( .r ‘ 𝐴 ) 𝑋 ) = ( 1r ‘ 𝐴 ) ) ) )
28	26 27	mpbird	⊢ ( 𝜑 → 𝑋 ∈ 𝑈 )