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 ⊢ φ → A ∈ AssAlg
assarrginv.5 ⊢ φ → K ∈ DivRing
assarrginv.6 ⊢ φ → dim ⁡ A ∈ ℕ 0
assarrginv.7 ⊢ φ → X ∈ E
Assertion assarrginv ⊢ φ → X ∈ 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 ⊢ φ → A ∈ AssAlg
5 assarrginv.5 ⊢ φ → K ∈ DivRing
6 assarrginv.6 ⊢ φ → dim ⁡ A ∈ ℕ 0
7 assarrginv.7 ⊢ φ → X ∈ E
8 eqid ⊢ Base A = Base A
9 eqid ⊢ ⋅ A = ⋅ A
10 eqid ⊢ a ∈ Base A ⟼ X ⋅ A a = a ∈ Base A ⟼ X ⋅ A a
11 8 9 10 4 1 3 5 6 7 assalactf1o ⊢ φ → a ∈ Base A ⟼ X ⋅ 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 ⊢ 1 A = 1 A
15 12 14 ringidval ⊢ 1 A = 0 mulGrp A
16 12 9 mgpplusg ⊢ ⋅ A = + mulGrp A
17 oveq2 ⊢ a = b → X ⋅ A a = X ⋅ A b
18 17 cbvmptv ⊢ a ∈ Base A ⟼ X ⋅ A a = b ∈ Base A ⟼ X ⋅ A b
19 assaring ⊢ A ∈ AssAlg → A ∈ Ring
20 4 19 syl ⊢ φ → A ∈ Ring
21 12 ringmgp ⊢ A ∈ Ring → mulGrp A ∈ Mnd
22 20 21 syl ⊢ φ → mulGrp A ∈ Mnd
23 1 8 rrgss ⊢ E ⊆ Base A
24 23 7 sselid ⊢ φ → X ∈ Base A
25 13 15 16 18 22 24 mndlactf1o ⊢ φ → a ∈ Base A ⟼ X ⋅ A a : Base A ⟶ 1-1 onto Base A ↔ ∃ z ∈ Base A X ⋅ A z = 1 A ∧ z ⋅ A X = 1 A
26 11 25 mpbid ⊢ φ → ∃ z ∈ Base A X ⋅ A z = 1 A ∧ z ⋅ A X = 1 A
27 8 2 9 14 24 20 isunit3 ⊢ φ → X ∈ U ↔ ∃ z ∈ Base A X ⋅ A z = 1 A ∧ z ⋅ A X = 1 A
28 26 27 mpbird ⊢ φ → X ∈ U