qqh0

Description: The image of 0 by the QQHom homomorphism is the ring's zero. (Contributed by Thierry Arnoux, 22-Oct-2017)

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

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		zssq	$⊢ ℤ \subseteq ℚ$
5		0z	$⊢ 0 \in ℤ$
6	4 5	sselii	$⊢ 0 \in ℚ$
7	1 2 3	qqhvval	$⊢ ((R \in DivRing \land chr (R) = 0) \land 0 \in ℚ) \to ℚHom (R) (0) = L (numer (0)) \underset{˙}{\times} L (denom (0))$
8	6 7	mpan2	$⊢ (R \in DivRing \land chr (R) = 0) \to ℚHom (R) (0) = L (numer (0)) \underset{˙}{\times} L (denom (0))$
9		1z	$⊢ 1 \in ℤ$
10		gcd0id	$⊢ 1 \in ℤ \to 0 \gcd 1 = \|1\|$
11	9 10	ax-mp	$⊢ 0 \gcd 1 = \|1\|$
12		abs1	$⊢ \|1\| = 1$
13	11 12	eqtri	$⊢ 0 \gcd 1 = 1$
14		0cn	$⊢ 0 \in ℂ$
15	14	div1i	$⊢ \frac{0}{1} = 0$
16	15	eqcomi	$⊢ 0 = \frac{0}{1}$
17	13 16	pm3.2i	$⊢ (0 \gcd 1 = 1 \land 0 = \frac{0}{1})$
18		1nn	$⊢ 1 \in ℕ$
19		qnumdenbi	$⊢ (0 \in ℚ \land 0 \in ℤ \land 1 \in ℕ) \to ((0 \gcd 1 = 1 \land 0 = \frac{0}{1}) \leftrightarrow (numer (0) = 0 \land denom (0) = 1))$
20	6 5 18 19	mp3an	$⊢ (0 \gcd 1 = 1 \land 0 = \frac{0}{1}) \leftrightarrow (numer (0) = 0 \land denom (0) = 1)$
21	17 20	mpbi	$⊢ (numer (0) = 0 \land denom (0) = 1)$
22	21	simpli	$⊢ numer (0) = 0$
23	22	fveq2i	$⊢ L (numer (0)) = L (0)$
24	21	simpri	$⊢ denom (0) = 1$
25	24	fveq2i	$⊢ L (denom (0)) = L (1)$
26	23 25	oveq12i	$⊢ L (numer (0)) \underset{˙}{\times} L (denom (0)) = L (0) \underset{˙}{\times} L (1)$
27		drngring	$⊢ R \in DivRing \to R \in Ring$
28		eqid	$⊢ 0_{R} = 0_{R}$
29	3 28	zrh0	$⊢ R \in Ring \to L (0) = 0_{R}$
30		eqid	$⊢ 1_{R} = 1_{R}$
31	3 30	zrh1	$⊢ R \in Ring \to L (1) = 1_{R}$
32	29 31	oveq12d	$⊢ R \in Ring \to L (0) \underset{˙}{\times} L (1) = 0_{R} \underset{˙}{\times} 1_{R}$
33	27 32	syl	$⊢ R \in DivRing \to L (0) \underset{˙}{\times} L (1) = 0_{R} \underset{˙}{\times} 1_{R}$
34		drnggrp	$⊢ R \in DivRing \to R \in Grp$
35	1 28	grpidcl	$⊢ R \in Grp \to 0_{R} \in B$
36	34 35	syl	$⊢ R \in DivRing \to 0_{R} \in B$
37	1 2 30	dvr1	$⊢ (R \in Ring \land 0_{R} \in B) \to 0_{R} \underset{˙}{\times} 1_{R} = 0_{R}$
38	27 36 37	syl2anc	$⊢ R \in DivRing \to 0_{R} \underset{˙}{\times} 1_{R} = 0_{R}$
39	33 38	eqtrd	$⊢ R \in DivRing \to L (0) \underset{˙}{\times} L (1) = 0_{R}$
40	26 39	eqtrid	$⊢ R \in DivRing \to L (numer (0)) \underset{˙}{\times} L (denom (0)) = 0_{R}$
41	40	adantr	$⊢ (R \in DivRing \land chr (R) = 0) \to L (numer (0)) \underset{˙}{\times} L (denom (0)) = 0_{R}$
42	8 41	eqtrd	$⊢ (R \in DivRing \land chr (R) = 0) \to ℚHom (R) (0) = 0_{R}$

Metamath Proof Explorer

Theorem qqh0

Proof