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 ⊢ 𝐸 = ( 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 ⊢ ( 𝜑 → 𝑋 ∈ 𝑈 )