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 ⊢ 𝐵 = ( Base ‘ 𝑅 )
zrhker.1 ⊢ 𝐿 = ( ℤRHom ‘ 𝑅 )
zrhker.2 ⊢ 0 = ( 0g ‘ 𝑅 )
Assertion zrhunitpreima ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) → ( ◡ 𝐿 “ ( Unit ‘ 𝑅 ) ) = ( ℤ ∖ { 0 } ) )

Proof

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