qqh1

Description: The image of 1 by the QQHom homomorphism is the ring's unit. (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	qqh1	$⊢ (R \in DivRing \land chr (R) = 0) \to ℚHom (R) (1) = 1_{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		1z	$⊢ 1 \in ℤ$
6	4 5	sselii	$⊢ 1 \in ℚ$
7	1 2 3	qqhvval	$⊢ ((R \in DivRing \land chr (R) = 0) \land 1 \in ℚ) \to ℚHom (R) (1) = L (numer (1)) \underset{˙}{\times} L (denom (1))$
8	6 7	mpan2	$⊢ (R \in DivRing \land chr (R) = 0) \to ℚHom (R) (1) = L (numer (1)) \underset{˙}{\times} L (denom (1))$
9		gcd1	$⊢ 1 \in ℤ \to 1 \gcd 1 = 1$
10	5 9	ax-mp	$⊢ 1 \gcd 1 = 1$
11		1div1e1	$⊢ \frac{1}{1} = 1$
12	11	eqcomi	$⊢ 1 = \frac{1}{1}$
13	10 12	pm3.2i	$⊢ (1 \gcd 1 = 1 \land 1 = \frac{1}{1})$
14		1nn	$⊢ 1 \in ℕ$
15		qnumdenbi	$⊢ (1 \in ℚ \land 1 \in ℤ \land 1 \in ℕ) \to ((1 \gcd 1 = 1 \land 1 = \frac{1}{1}) \leftrightarrow (numer (1) = 1 \land denom (1) = 1))$
16	6 5 14 15	mp3an	$⊢ (1 \gcd 1 = 1 \land 1 = \frac{1}{1}) \leftrightarrow (numer (1) = 1 \land denom (1) = 1)$
17	13 16	mpbi	$⊢ (numer (1) = 1 \land denom (1) = 1)$
18	17	simpli	$⊢ numer (1) = 1$
19	18	fveq2i	$⊢ L (numer (1)) = L (1)$
20	17	simpri	$⊢ denom (1) = 1$
21	20	fveq2i	$⊢ L (denom (1)) = L (1)$
22	19 21	oveq12i	$⊢ L (numer (1)) \underset{˙}{\times} L (denom (1)) = L (1) \underset{˙}{\times} L (1)$
23		drngring	$⊢ R \in DivRing \to R \in Ring$
24		eqid	$⊢ 1_{R} = 1_{R}$
25	3 24	zrh1	$⊢ R \in Ring \to L (1) = 1_{R}$
26	25 25	oveq12d	$⊢ R \in Ring \to L (1) \underset{˙}{\times} L (1) = 1_{R} \underset{˙}{\times} 1_{R}$
27	23 26	syl	$⊢ R \in DivRing \to L (1) \underset{˙}{\times} L (1) = 1_{R} \underset{˙}{\times} 1_{R}$
28	1 24	ringidcl	$⊢ R \in Ring \to 1_{R} \in B$
29	1 2 24	dvr1	$⊢ (R \in Ring \land 1_{R} \in B) \to 1_{R} \underset{˙}{\times} 1_{R} = 1_{R}$
30	23 28 29	syl2anc2	$⊢ R \in DivRing \to 1_{R} \underset{˙}{\times} 1_{R} = 1_{R}$
31	27 30	eqtrd	$⊢ R \in DivRing \to L (1) \underset{˙}{\times} L (1) = 1_{R}$
32	22 31	eqtrid	$⊢ R \in DivRing \to L (numer (1)) \underset{˙}{\times} L (denom (1)) = 1_{R}$
33	32	adantr	$⊢ (R \in DivRing \land chr (R) = 0) \to L (numer (1)) \underset{˙}{\times} L (denom (1)) = 1_{R}$
34	8 33	eqtrd	$⊢ (R \in DivRing \land chr (R) = 0) \to ℚHom (R) (1) = 1_{R}$

Metamath Proof Explorer

Theorem qqh1

Proof