Metamath Proof Explorer

Theorem zrhunitpreima

Description: The preimage by ZRHom of the units of a division ring is ( ZZ \ { 0 } ) . (Contributed by Thierry Arnoux, 22-Oct-2017)

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

Proof

Step Hyp Ref Expression
1 zrhker.0 ⊢ B = Base R
2 zrhker.1 ⊢ L = ℤRHom ⁡ R
3 zrhker.2 ⊢ 0 ˙ = 0 R
4 eqid ⊢ Unit ⁡ R = Unit ⁡ R
5 eqid ⊢ 0 R = 0 R
6 1 4 5 isdrng ⊢ R ∈ DivRing ↔ R ∈ Ring ∧ Unit ⁡ R = B ∖ 0 R
7 6 simprbi ⊢ R ∈ DivRing → Unit ⁡ R = B ∖ 0 R
8 7 imaeq2d ⊢ R ∈ DivRing → L -1 Unit ⁡ R = L -1 B ∖ 0 R
9 8 adantr ⊢ R ∈ DivRing ∧ chr ⁡ R = 0 → L -1 Unit ⁡ R = L -1 B ∖ 0 R
10 drngring ⊢ R ∈ DivRing → R ∈ Ring
11 2 zrhrhm ⊢ R ∈ Ring → L ∈ ℤ ring RingHom R
12 zringbas ⊢ ℤ = Base ℤ ring
13 12 1 rhmf ⊢ L ∈ ℤ ring RingHom R → L : ℤ ⟶ B
14 ffun ⊢ L : ℤ ⟶ B → Fun ⁡ L
15 11 13 14 3syl ⊢ R ∈ Ring → Fun ⁡ L
16 difpreima ⊢ Fun ⁡ L → L -1 B ∖ 0 R = L -1 B ∖ L -1 0 R
17 10 15 16 3syl ⊢ R ∈ DivRing → L -1 B ∖ 0 R = L -1 B ∖ L -1 0 R
18 17 adantr ⊢ R ∈ DivRing ∧ chr ⁡ R = 0 → L -1 B ∖ 0 R = L -1 B ∖ L -1 0 R
19 fimacnv ⊢ L : ℤ ⟶ B → L -1 B = ℤ
20 10 11 13 19 4syl ⊢ R ∈ DivRing → L -1 B = ℤ
21 20 adantr ⊢ R ∈ DivRing ∧ chr ⁡ R = 0 → L -1 B = ℤ
22 1 2 5 zrhker ⊢ R ∈ Ring → chr ⁡ R = 0 ↔ L -1 0 R = 0
23 22 biimpa ⊢ R ∈ Ring ∧ chr ⁡ R = 0 → L -1 0 R = 0
24 10 23 sylan ⊢ R ∈ DivRing ∧ chr ⁡ R = 0 → L -1 0 R = 0
25 21 24 difeq12d ⊢ R ∈ DivRing ∧ chr ⁡ R = 0 → L -1 B ∖ L -1 0 R = ℤ ∖ 0
26 9 18 25 3eqtrd ⊢ R ∈ DivRing ∧ chr ⁡ R = 0 → L -1 Unit ⁡ R = ℤ ∖ 0