qqhf

Description: QQHom as a function. (Contributed by Thierry Arnoux, 28-Oct-2017)

	Ref	Expression
Hypotheses	qqhval2.0	$⊢ B = {Base}_{R}$
	qqhval2.1	$⊢ \underset{˙}{\times} = /_{r} (R)$
	qqhval2.2	$⊢ L = ℤRHom (R)$
Assertion	qqhf	$⊢ (R \in DivRing \land chr (R) = 0) \to ℚHom (R) : ℚ ⟶ B$

Proof

Step	Hyp	Ref	Expression
1		qqhval2.0	$⊢ B = {Base}_{R}$
2		qqhval2.1	$⊢ \underset{˙}{\times} = /_{r} (R)$
3		qqhval2.2	$⊢ L = ℤRHom (R)$
4	1 2 3	qqhval2	$⊢ (R \in DivRing \land chr (R) = 0) \to ℚHom (R) = (q \in ℚ ⟼ L (numer (q)) \underset{˙}{\times} L (denom (q)))$
5		drngring	$⊢ R \in DivRing \to R \in Ring$
6	5	adantr	$⊢ (R \in DivRing \land chr (R) = 0) \to R \in Ring$
7	6	adantr	$⊢ ((R \in DivRing \land chr (R) = 0) \land q \in ℚ) \to R \in Ring$
8	3	zrhrhm	$⊢ R \in Ring \to L \in (ℤ_{ring} RingHom R)$
9		zringbas	$⊢ ℤ = {Base}_{ℤ_{ring}}$
10	9 1	rhmf	$⊢ L \in (ℤ_{ring} RingHom R) \to L : ℤ ⟶ B$
11	7 8 10	3syl	$⊢ ((R \in DivRing \land chr (R) = 0) \land q \in ℚ) \to L : ℤ ⟶ B$
12		qnumcl	$⊢ q \in ℚ \to numer (q) \in ℤ$
13	12	adantl	$⊢ ((R \in DivRing \land chr (R) = 0) \land q \in ℚ) \to numer (q) \in ℤ$
14	11 13	ffvelcdmd	$⊢ ((R \in DivRing \land chr (R) = 0) \land q \in ℚ) \to L (numer (q)) \in B$
15		simpll	$⊢ ((R \in DivRing \land chr (R) = 0) \land q \in ℚ) \to R \in DivRing$
16		qdencl	$⊢ q \in ℚ \to denom (q) \in ℕ$
17	16	adantl	$⊢ ((R \in DivRing \land chr (R) = 0) \land q \in ℚ) \to denom (q) \in ℕ$
18	17	nnzd	$⊢ ((R \in DivRing \land chr (R) = 0) \land q \in ℚ) \to denom (q) \in ℤ$
19	11 18	ffvelcdmd	$⊢ ((R \in DivRing \land chr (R) = 0) \land q \in ℚ) \to L (denom (q)) \in B$
20	17	nnne0d	$⊢ ((R \in DivRing \land chr (R) = 0) \land q \in ℚ) \to denom (q) \neq 0$
21	20	neneqd	$⊢ ((R \in DivRing \land chr (R) = 0) \land q \in ℚ) \to \neg denom (q) = 0$
22		fvex	$⊢ denom (q) \in V$
23	22	elsn	$⊢ denom (q) \in \{0\} \leftrightarrow denom (q) = 0$
24	21 23	sylnibr	$⊢ ((R \in DivRing \land chr (R) = 0) \land q \in ℚ) \to \neg denom (q) \in \{0\}$
25		eqid	$⊢ 0_{R} = 0_{R}$
26	1 3 25	zrhker	$⊢ R \in Ring \to (chr (R) = 0 \leftrightarrow L^{-1} [\{0_{R}\}] = \{0\})$
27	26	biimpa	$⊢ (R \in Ring \land chr (R) = 0) \to L^{-1} [\{0_{R}\}] = \{0\}$
28	5 27	sylan	$⊢ (R \in DivRing \land chr (R) = 0) \to L^{-1} [\{0_{R}\}] = \{0\}$
29	28	adantr	$⊢ ((R \in DivRing \land chr (R) = 0) \land q \in ℚ) \to L^{-1} [\{0_{R}\}] = \{0\}$
30	24 29	neleqtrrd	$⊢ ((R \in DivRing \land chr (R) = 0) \land q \in ℚ) \to \neg denom (q) \in L^{-1} [\{0_{R}\}]$
31		ffn	$⊢ L : ℤ ⟶ B \to L Fn ℤ$
32	8 10 31	3syl	$⊢ R \in Ring \to L Fn ℤ$
33		elpreima	$⊢ L Fn ℤ \to (denom (q) \in L^{-1} [\{0_{R}\}] \leftrightarrow (denom (q) \in ℤ \land L (denom (q)) \in \{0_{R}\}))$
34	5 32 33	3syl	$⊢ R \in DivRing \to (denom (q) \in L^{-1} [\{0_{R}\}] \leftrightarrow (denom (q) \in ℤ \land L (denom (q)) \in \{0_{R}\}))$
35	34	biimpar	$⊢ (R \in DivRing \land (denom (q) \in ℤ \land L (denom (q)) \in \{0_{R}\})) \to denom (q) \in L^{-1} [\{0_{R}\}]$
36	35	expr	$⊢ (R \in DivRing \land denom (q) \in ℤ) \to (L (denom (q)) \in \{0_{R}\} \to denom (q) \in L^{-1} [\{0_{R}\}])$
37	36	con3dimp	$⊢ ((R \in DivRing \land denom (q) \in ℤ) \land \neg denom (q) \in L^{-1} [\{0_{R}\}]) \to \neg L (denom (q)) \in \{0_{R}\}$
38	15 18 30 37	syl21anc	$⊢ ((R \in DivRing \land chr (R) = 0) \land q \in ℚ) \to \neg L (denom (q)) \in \{0_{R}\}$
39		fvex	$⊢ L (denom (q)) \in V$
40	39	elsn	$⊢ L (denom (q)) \in \{0_{R}\} \leftrightarrow L (denom (q)) = 0_{R}$
41	38 40	sylnib	$⊢ ((R \in DivRing \land chr (R) = 0) \land q \in ℚ) \to \neg L (denom (q)) = 0_{R}$
42	41	neqned	$⊢ ((R \in DivRing \land chr (R) = 0) \land q \in ℚ) \to L (denom (q)) \neq 0_{R}$
43		eqid	$⊢ Unit (R) = Unit (R)$
44	1 43 25	drngunit	$⊢ R \in DivRing \to (L (denom (q)) \in Unit (R) \leftrightarrow (L (denom (q)) \in B \land L (denom (q)) \neq 0_{R}))$
45	44	biimpar	$⊢ (R \in DivRing \land (L (denom (q)) \in B \land L (denom (q)) \neq 0_{R})) \to L (denom (q)) \in Unit (R)$
46	15 19 42 45	syl12anc	$⊢ ((R \in DivRing \land chr (R) = 0) \land q \in ℚ) \to L (denom (q)) \in Unit (R)$
47	1 43 2	dvrcl	$⊢ (R \in Ring \land L (numer (q)) \in B \land L (denom (q)) \in Unit (R)) \to L (numer (q)) \underset{˙}{\times} L (denom (q)) \in B$
48	7 14 46 47	syl3anc	$⊢ ((R \in DivRing \land chr (R) = 0) \land q \in ℚ) \to L (numer (q)) \underset{˙}{\times} L (denom (q)) \in B$
49	4 48	fmpt3d	$⊢ (R \in DivRing \land chr (R) = 0) \to ℚHom (R) : ℚ ⟶ B$

Metamath Proof Explorer

Theorem qqhf

Proof