Metamath Proof Explorer

Theorem elzrhunit

Description: Condition for the image by ZRHom to be a unit. (Contributed by Thierry Arnoux, 30-Oct-2017)

Ref Expression
Hypotheses zrhker.0 ⊢ B = Base R
zrhker.1 ⊢ L = ℤRHom ⁡ R
zrhker.2 ⊢ 0 ˙ = 0 R
Assertion elzrhunit ⊢ R ∈ DivRing ∧ chr ⁡ R = 0 ∧ M ∈ ℤ ∧ M ≠ 0 → L ⁡ M ∈ Unit ⁡ R

Proof

Step Hyp Ref Expression
1 zrhker.0 ⊢ B = Base R
2 zrhker.1 ⊢ L = ℤRHom ⁡ R
3 zrhker.2 ⊢ 0 ˙ = 0 R
4 simpll ⊢ R ∈ DivRing ∧ chr ⁡ R = 0 ∧ M ∈ ℤ ∧ M ≠ 0 → R ∈ DivRing
5 drngring ⊢ R ∈ DivRing → R ∈ Ring
6 2 zrhrhm ⊢ R ∈ Ring → L ∈ ℤ ring RingHom R
7 zringbas ⊢ ℤ = Base ℤ ring
8 7 1 rhmf ⊢ L ∈ ℤ ring RingHom R → L : ℤ ⟶ B
9 ffn ⊢ L : ℤ ⟶ B → L Fn ℤ
10 6 8 9 3syl ⊢ R ∈ Ring → L Fn ℤ
11 4 5 10 3syl ⊢ R ∈ DivRing ∧ chr ⁡ R = 0 ∧ M ∈ ℤ ∧ M ≠ 0 → L Fn ℤ
12 simprl ⊢ R ∈ DivRing ∧ chr ⁡ R = 0 ∧ M ∈ ℤ ∧ M ≠ 0 → M ∈ ℤ
13 elsng ⊢ M ∈ ℤ → M ∈ 0 ↔ M = 0
14 13 necon3bbid ⊢ M ∈ ℤ → ¬ M ∈ 0 ↔ M ≠ 0
15 14 biimpar ⊢ M ∈ ℤ ∧ M ≠ 0 → ¬ M ∈ 0
16 15 adantl ⊢ R ∈ DivRing ∧ chr ⁡ R = 0 ∧ M ∈ ℤ ∧ M ≠ 0 → ¬ M ∈ 0
17 12 16 eldifd ⊢ R ∈ DivRing ∧ chr ⁡ R = 0 ∧ M ∈ ℤ ∧ M ≠ 0 → M ∈ ℤ ∖ 0
18 1 2 3 zrhunitpreima ⊢ R ∈ DivRing ∧ chr ⁡ R = 0 → L -1 Unit ⁡ R = ℤ ∖ 0
19 18 adantr ⊢ R ∈ DivRing ∧ chr ⁡ R = 0 ∧ M ∈ ℤ ∧ M ≠ 0 → L -1 Unit ⁡ R = ℤ ∖ 0
20 17 19 eleqtrrd ⊢ R ∈ DivRing ∧ chr ⁡ R = 0 ∧ M ∈ ℤ ∧ M ≠ 0 → M ∈ L -1 Unit ⁡ R
21 elpreima ⊢ L Fn ℤ → M ∈ L -1 Unit ⁡ R ↔ M ∈ ℤ ∧ L ⁡ M ∈ Unit ⁡ R
22 21 simplbda ⊢ L Fn ℤ ∧ M ∈ L -1 Unit ⁡ R → L ⁡ M ∈ Unit ⁡ R
23 11 20 22 syl2anc ⊢ R ∈ DivRing ∧ chr ⁡ R = 0 ∧ M ∈ ℤ ∧ M ≠ 0 → L ⁡ M ∈ Unit ⁡ R