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	$⊢ \underset{˙}{0} = 0_{R}$
Assertion	zrhunitpreima	$⊢ (R \in DivRing \land chr (R) = 0) \to 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	$⊢ \underset{˙}{0} = 0_{R}$
4		eqid	$⊢ Unit (R) = Unit (R)$
5		eqid	$⊢ 0_{R} = 0_{R}$
6	1 4 5	isdrng	$⊢ R \in DivRing \leftrightarrow (R \in Ring \land Unit (R) = B ∖ \{0_{R}\})$
7	6	simprbi	$⊢ R \in DivRing \to Unit (R) = B ∖ \{0_{R}\}$
8	7	imaeq2d	$⊢ R \in DivRing \to L^{-1} [Unit (R)] = L^{-1} [B ∖ \{0_{R}\}]$
9	8	adantr	$⊢ (R \in DivRing \land chr (R) = 0) \to L^{-1} [Unit (R)] = L^{-1} [B ∖ \{0_{R}\}]$
10		drngring	$⊢ R \in DivRing \to R \in Ring$
11	2	zrhrhm	$⊢ R \in Ring \to L \in (ℤ_{ring} RingHom R)$
12		zringbas	$⊢ ℤ = {Base}_{ℤ_{ring}}$
13	12 1	rhmf	$⊢ L \in (ℤ_{ring} RingHom R) \to L : ℤ ⟶ B$
14		ffun	$⊢ L : ℤ ⟶ B \to Fun L$
15	11 13 14	3syl	$⊢ R \in Ring \to Fun L$
16		difpreima	$⊢ Fun L \to L^{-1} [B ∖ \{0_{R}\}] = L^{-1} [B] ∖ L^{-1} [\{0_{R}\}]$
17	10 15 16	3syl	$⊢ R \in DivRing \to L^{-1} [B ∖ \{0_{R}\}] = L^{-1} [B] ∖ L^{-1} [\{0_{R}\}]$
18	17	adantr	$⊢ (R \in DivRing \land chr (R) = 0) \to L^{-1} [B ∖ \{0_{R}\}] = L^{-1} [B] ∖ L^{-1} [\{0_{R}\}]$
19		fimacnv	$⊢ L : ℤ ⟶ B \to L^{-1} [B] = ℤ$
20	10 11 13 19	4syl	$⊢ R \in DivRing \to L^{-1} [B] = ℤ$
21	20	adantr	$⊢ (R \in DivRing \land chr (R) = 0) \to L^{-1} [B] = ℤ$
22	1 2 5	zrhker	$⊢ R \in Ring \to (chr (R) = 0 \leftrightarrow L^{-1} [\{0_{R}\}] = \{0\})$
23	22	biimpa	$⊢ (R \in Ring \land chr (R) = 0) \to L^{-1} [\{0_{R}\}] = \{0\}$
24	10 23	sylan	$⊢ (R \in DivRing \land chr (R) = 0) \to L^{-1} [\{0_{R}\}] = \{0\}$
25	21 24	difeq12d	$⊢ (R \in DivRing \land chr (R) = 0) \to L^{-1} [B] ∖ L^{-1} [\{0_{R}\}] = ℤ ∖ \{0\}$
26	9 18 25	3eqtrd	$⊢ (R \in DivRing \land chr (R) = 0) \to L^{-1} [Unit (R)] = ℤ ∖ \{0\}$

Metamath Proof Explorer

Theorem zrhunitpreima

Proof