qqhghm

Description: The QQHom homomorphism is a group homomorphism if the target structure is a division ring. (Contributed by Thierry Arnoux, 9-Nov-2017)

	Ref	Expression
Hypotheses	qqhval2.0	$⊢ B = {Base}_{R}$
	qqhval2.1	$⊢ \underset{˙}{\times} = /_{r} (R)$
	qqhval2.2	$⊢ L = ℤRHom (R)$
	qqhrhm.1	$⊢ Q = ℂ_{fld} ↾_{𝑠} ℚ$
Assertion	qqhghm	$⊢ (R \in DivRing \land chr (R) = 0) \to ℚHom (R) \in (Q GrpHom 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		qqhrhm.1	$⊢ Q = ℂ_{fld} ↾_{𝑠} ℚ$
5	4	qrngbas	$⊢ ℚ = {Base}_{Q}$
6		qex	$⊢ ℚ \in V$
7		cnfldadd	$⊢ + = +_{ℂ_{fld}}$
8	4 7	ressplusg	$⊢ ℚ \in V \to + = +_{Q}$
9	6 8	ax-mp	$⊢ + = +_{Q}$
10		eqid	$⊢ +_{R} = +_{R}$
11	4	qdrng	$⊢ Q \in DivRing$
12		drnggrp	$⊢ Q \in DivRing \to Q \in Grp$
13	11 12	mp1i	$⊢ (R \in DivRing \land chr (R) = 0) \to Q \in Grp$
14		drnggrp	$⊢ R \in DivRing \to R \in Grp$
15	14	adantr	$⊢ (R \in DivRing \land chr (R) = 0) \to R \in Grp$
16	1 2 3	qqhf	$⊢ (R \in DivRing \land chr (R) = 0) \to ℚHom (R) : ℚ ⟶ B$
17		drngring	$⊢ R \in DivRing \to R \in Ring$
18	17	ad2antrr	$⊢ ((R \in DivRing \land chr (R) = 0) \land (x \in ℚ \land y \in ℚ)) \to R \in Ring$
19	17	adantr	$⊢ (R \in DivRing \land chr (R) = 0) \to R \in Ring$
20	3	zrhrhm	$⊢ R \in Ring \to L \in (ℤ_{ring} RingHom R)$
21		zringbas	$⊢ ℤ = {Base}_{ℤ_{ring}}$
22	21 1	rhmf	$⊢ L \in (ℤ_{ring} RingHom R) \to L : ℤ ⟶ B$
23	19 20 22	3syl	$⊢ (R \in DivRing \land chr (R) = 0) \to L : ℤ ⟶ B$
24	23	adantr	$⊢ ((R \in DivRing \land chr (R) = 0) \land (x \in ℚ \land y \in ℚ)) \to L : ℤ ⟶ B$
25		qnumcl	$⊢ x \in ℚ \to numer (x) \in ℤ$
26	25	ad2antrl	$⊢ ((R \in DivRing \land chr (R) = 0) \land (x \in ℚ \land y \in ℚ)) \to numer (x) \in ℤ$
27		qdencl	$⊢ y \in ℚ \to denom (y) \in ℕ$
28	27	ad2antll	$⊢ ((R \in DivRing \land chr (R) = 0) \land (x \in ℚ \land y \in ℚ)) \to denom (y) \in ℕ$
29	28	nnzd	$⊢ ((R \in DivRing \land chr (R) = 0) \land (x \in ℚ \land y \in ℚ)) \to denom (y) \in ℤ$
30	26 29	zmulcld	$⊢ ((R \in DivRing \land chr (R) = 0) \land (x \in ℚ \land y \in ℚ)) \to numer (x) denom (y) \in ℤ$
31	24 30	ffvelrnd	$⊢ ((R \in DivRing \land chr (R) = 0) \land (x \in ℚ \land y \in ℚ)) \to L (numer (x) denom (y)) \in B$
32		qnumcl	$⊢ y \in ℚ \to numer (y) \in ℤ$
33	32	ad2antll	$⊢ ((R \in DivRing \land chr (R) = 0) \land (x \in ℚ \land y \in ℚ)) \to numer (y) \in ℤ$
34		qdencl	$⊢ x \in ℚ \to denom (x) \in ℕ$
35	34	ad2antrl	$⊢ ((R \in DivRing \land chr (R) = 0) \land (x \in ℚ \land y \in ℚ)) \to denom (x) \in ℕ$
36	35	nnzd	$⊢ ((R \in DivRing \land chr (R) = 0) \land (x \in ℚ \land y \in ℚ)) \to denom (x) \in ℤ$
37	33 36	zmulcld	$⊢ ((R \in DivRing \land chr (R) = 0) \land (x \in ℚ \land y \in ℚ)) \to numer (y) denom (x) \in ℤ$
38	24 37	ffvelrnd	$⊢ ((R \in DivRing \land chr (R) = 0) \land (x \in ℚ \land y \in ℚ)) \to L (numer (y) denom (x)) \in B$
39	18 20	syl	$⊢ ((R \in DivRing \land chr (R) = 0) \land (x \in ℚ \land y \in ℚ)) \to L \in (ℤ_{ring} RingHom R)$
40		zringmulr	$⊢ \times = \cdot_{ℤ_{ring}}$
41		eqid	$⊢ \cdot_{R} = \cdot_{R}$
42	21 40 41	rhmmul	$⊢ (L \in (ℤ_{ring} RingHom R) \land denom (x) \in ℤ \land denom (y) \in ℤ) \to L (denom (x) denom (y)) = L (denom (x)) \cdot_{R} L (denom (y))$
43	39 36 29 42	syl3anc	$⊢ ((R \in DivRing \land chr (R) = 0) \land (x \in ℚ \land y \in ℚ)) \to L (denom (x) denom (y)) = L (denom (x)) \cdot_{R} L (denom (y))$
44		simpl	$⊢ ((R \in DivRing \land chr (R) = 0) \land (x \in ℚ \land y \in ℚ)) \to (R \in DivRing \land chr (R) = 0)$
45	35	nnne0d	$⊢ ((R \in DivRing \land chr (R) = 0) \land (x \in ℚ \land y \in ℚ)) \to denom (x) \neq 0$
46		eqid	$⊢ 0_{R} = 0_{R}$
47	1 3 46	elzrhunit	$⊢ ((R \in DivRing \land chr (R) = 0) \land (denom (x) \in ℤ \land denom (x) \neq 0)) \to L (denom (x)) \in Unit (R)$
48	44 36 45 47	syl12anc	$⊢ ((R \in DivRing \land chr (R) = 0) \land (x \in ℚ \land y \in ℚ)) \to L (denom (x)) \in Unit (R)$
49	28	nnne0d	$⊢ ((R \in DivRing \land chr (R) = 0) \land (x \in ℚ \land y \in ℚ)) \to denom (y) \neq 0$
50	1 3 46	elzrhunit	$⊢ ((R \in DivRing \land chr (R) = 0) \land (denom (y) \in ℤ \land denom (y) \neq 0)) \to L (denom (y)) \in Unit (R)$
51	44 29 49 50	syl12anc	$⊢ ((R \in DivRing \land chr (R) = 0) \land (x \in ℚ \land y \in ℚ)) \to L (denom (y)) \in Unit (R)$
52		eqid	$⊢ Unit (R) = Unit (R)$
53	52 41	unitmulcl	$⊢ (R \in Ring \land L (denom (x)) \in Unit (R) \land L (denom (y)) \in Unit (R)) \to L (denom (x)) \cdot_{R} L (denom (y)) \in Unit (R)$
54	18 48 51 53	syl3anc	$⊢ ((R \in DivRing \land chr (R) = 0) \land (x \in ℚ \land y \in ℚ)) \to L (denom (x)) \cdot_{R} L (denom (y)) \in Unit (R)$
55	43 54	eqeltrd	$⊢ ((R \in DivRing \land chr (R) = 0) \land (x \in ℚ \land y \in ℚ)) \to L (denom (x) denom (y)) \in Unit (R)$
56	1 52 10 2	dvrdir	$⊢ (R \in Ring \land (L (numer (x) denom (y)) \in B \land L (numer (y) denom (x)) \in B \land L (denom (x) denom (y)) \in Unit (R))) \to (L (numer (x) denom (y)) +_{R} L (numer (y) denom (x))) \underset{˙}{\times} L (denom (x) denom (y)) = (L (numer (x) denom (y)) \underset{˙}{\times} L (denom (x) denom (y))) +_{R} (L (numer (y) denom (x)) \underset{˙}{\times} L (denom (x) denom (y)))$
57	18 31 38 55 56	syl13anc	$⊢ ((R \in DivRing \land chr (R) = 0) \land (x \in ℚ \land y \in ℚ)) \to (L (numer (x) denom (y)) +_{R} L (numer (y) denom (x))) \underset{˙}{\times} L (denom (x) denom (y)) = (L (numer (x) denom (y)) \underset{˙}{\times} L (denom (x) denom (y))) +_{R} (L (numer (y) denom (x)) \underset{˙}{\times} L (denom (x) denom (y)))$
58		qeqnumdivden	$⊢ x \in ℚ \to x = \frac{numer (x)}{denom (x)}$
59	58	ad2antrl	$⊢ ((R \in DivRing \land chr (R) = 0) \land (x \in ℚ \land y \in ℚ)) \to x = \frac{numer (x)}{denom (x)}$
60		qeqnumdivden	$⊢ y \in ℚ \to y = \frac{numer (y)}{denom (y)}$
61	60	ad2antll	$⊢ ((R \in DivRing \land chr (R) = 0) \land (x \in ℚ \land y \in ℚ)) \to y = \frac{numer (y)}{denom (y)}$
62	59 61	oveq12d	$⊢ ((R \in DivRing \land chr (R) = 0) \land (x \in ℚ \land y \in ℚ)) \to x + y = (\frac{numer (x)}{denom (x)}) + (\frac{numer (y)}{denom (y)})$
63	26	zcnd	$⊢ ((R \in DivRing \land chr (R) = 0) \land (x \in ℚ \land y \in ℚ)) \to numer (x) \in ℂ$
64	36	zcnd	$⊢ ((R \in DivRing \land chr (R) = 0) \land (x \in ℚ \land y \in ℚ)) \to denom (x) \in ℂ$
65	33	zcnd	$⊢ ((R \in DivRing \land chr (R) = 0) \land (x \in ℚ \land y \in ℚ)) \to numer (y) \in ℂ$
66	29	zcnd	$⊢ ((R \in DivRing \land chr (R) = 0) \land (x \in ℚ \land y \in ℚ)) \to denom (y) \in ℂ$
67	63 64 65 66 45 49	divadddivd	$⊢ ((R \in DivRing \land chr (R) = 0) \land (x \in ℚ \land y \in ℚ)) \to (\frac{numer (x)}{denom (x)}) + (\frac{numer (y)}{denom (y)}) = \frac{numer (x) denom (y) + numer (y) denom (x)}{denom (x) denom (y)}$
68	62 67	eqtrd	$⊢ ((R \in DivRing \land chr (R) = 0) \land (x \in ℚ \land y \in ℚ)) \to x + y = \frac{numer (x) denom (y) + numer (y) denom (x)}{denom (x) denom (y)}$
69	68	fveq2d	$⊢ ((R \in DivRing \land chr (R) = 0) \land (x \in ℚ \land y \in ℚ)) \to ℚHom (R) (x + y) = ℚHom (R) (\frac{numer (x) denom (y) + numer (y) denom (x)}{denom (x) denom (y)})$
70	30 37	zaddcld	$⊢ ((R \in DivRing \land chr (R) = 0) \land (x \in ℚ \land y \in ℚ)) \to numer (x) denom (y) + numer (y) denom (x) \in ℤ$
71	36 29	zmulcld	$⊢ ((R \in DivRing \land chr (R) = 0) \land (x \in ℚ \land y \in ℚ)) \to denom (x) denom (y) \in ℤ$
72	64 66 45 49	mulne0d	$⊢ ((R \in DivRing \land chr (R) = 0) \land (x \in ℚ \land y \in ℚ)) \to denom (x) denom (y) \neq 0$
73	1 2 3	qqhvq	$⊢ ((R \in DivRing \land chr (R) = 0) \land (numer (x) denom (y) + numer (y) denom (x) \in ℤ \land denom (x) denom (y) \in ℤ \land denom (x) denom (y) \neq 0)) \to ℚHom (R) (\frac{numer (x) denom (y) + numer (y) denom (x)}{denom (x) denom (y)}) = L (numer (x) denom (y) + numer (y) denom (x)) \underset{˙}{\times} L (denom (x) denom (y))$
74	44 70 71 72 73	syl13anc	$⊢ ((R \in DivRing \land chr (R) = 0) \land (x \in ℚ \land y \in ℚ)) \to ℚHom (R) (\frac{numer (x) denom (y) + numer (y) denom (x)}{denom (x) denom (y)}) = L (numer (x) denom (y) + numer (y) denom (x)) \underset{˙}{\times} L (denom (x) denom (y))$
75		rhmghm	$⊢ L \in (ℤ_{ring} RingHom R) \to L \in (ℤ_{ring} GrpHom R)$
76	39 75	syl	$⊢ ((R \in DivRing \land chr (R) = 0) \land (x \in ℚ \land y \in ℚ)) \to L \in (ℤ_{ring} GrpHom R)$
77		zringplusg	$⊢ + = +_{ℤ_{ring}}$
78	21 77 10	ghmlin	$⊢ (L \in (ℤ_{ring} GrpHom R) \land numer (x) denom (y) \in ℤ \land numer (y) denom (x) \in ℤ) \to L (numer (x) denom (y) + numer (y) denom (x)) = L (numer (x) denom (y)) +_{R} L (numer (y) denom (x))$
79	78	oveq1d	$⊢ (L \in (ℤ_{ring} GrpHom R) \land numer (x) denom (y) \in ℤ \land numer (y) denom (x) \in ℤ) \to L (numer (x) denom (y) + numer (y) denom (x)) \underset{˙}{\times} L (denom (x) denom (y)) = (L (numer (x) denom (y)) +_{R} L (numer (y) denom (x))) \underset{˙}{\times} L (denom (x) denom (y))$
80	76 30 37 79	syl3anc	$⊢ ((R \in DivRing \land chr (R) = 0) \land (x \in ℚ \land y \in ℚ)) \to L (numer (x) denom (y) + numer (y) denom (x)) \underset{˙}{\times} L (denom (x) denom (y)) = (L (numer (x) denom (y)) +_{R} L (numer (y) denom (x))) \underset{˙}{\times} L (denom (x) denom (y))$
81	69 74 80	3eqtrd	$⊢ ((R \in DivRing \land chr (R) = 0) \land (x \in ℚ \land y \in ℚ)) \to ℚHom (R) (x + y) = (L (numer (x) denom (y)) +_{R} L (numer (y) denom (x))) \underset{˙}{\times} L (denom (x) denom (y))$
82	58	fveq2d	$⊢ x \in ℚ \to ℚHom (R) (x) = ℚHom (R) (\frac{numer (x)}{denom (x)})$
83	82	ad2antrl	$⊢ ((R \in DivRing \land chr (R) = 0) \land (x \in ℚ \land y \in ℚ)) \to ℚHom (R) (x) = ℚHom (R) (\frac{numer (x)}{denom (x)})$
84	1 2 3	qqhvq	$⊢ ((R \in DivRing \land chr (R) = 0) \land (numer (x) \in ℤ \land denom (x) \in ℤ \land denom (x) \neq 0)) \to ℚHom (R) (\frac{numer (x)}{denom (x)}) = L (numer (x)) \underset{˙}{\times} L (denom (x))$
85	44 26 36 45 84	syl13anc	$⊢ ((R \in DivRing \land chr (R) = 0) \land (x \in ℚ \land y \in ℚ)) \to ℚHom (R) (\frac{numer (x)}{denom (x)}) = L (numer (x)) \underset{˙}{\times} L (denom (x))$
86	52 21 2 40	rhmdvd	$⊢ (L \in (ℤ_{ring} RingHom R) \land (numer (x) \in ℤ \land denom (x) \in ℤ \land denom (y) \in ℤ) \land (L (denom (x)) \in Unit (R) \land L (denom (y)) \in Unit (R))) \to L (numer (x)) \underset{˙}{\times} L (denom (x)) = L (numer (x) denom (y)) \underset{˙}{\times} L (denom (x) denom (y))$
87	39 26 36 29 48 51 86	syl132anc	$⊢ ((R \in DivRing \land chr (R) = 0) \land (x \in ℚ \land y \in ℚ)) \to L (numer (x)) \underset{˙}{\times} L (denom (x)) = L (numer (x) denom (y)) \underset{˙}{\times} L (denom (x) denom (y))$
88	83 85 87	3eqtrd	$⊢ ((R \in DivRing \land chr (R) = 0) \land (x \in ℚ \land y \in ℚ)) \to ℚHom (R) (x) = L (numer (x) denom (y)) \underset{˙}{\times} L (denom (x) denom (y))$
89	60	fveq2d	$⊢ y \in ℚ \to ℚHom (R) (y) = ℚHom (R) (\frac{numer (y)}{denom (y)})$
90	89	ad2antll	$⊢ ((R \in DivRing \land chr (R) = 0) \land (x \in ℚ \land y \in ℚ)) \to ℚHom (R) (y) = ℚHom (R) (\frac{numer (y)}{denom (y)})$
91	52 21 2 40	rhmdvd	$⊢ (L \in (ℤ_{ring} RingHom R) \land (numer (y) \in ℤ \land denom (y) \in ℤ \land denom (x) \in ℤ) \land (L (denom (y)) \in Unit (R) \land L (denom (x)) \in Unit (R))) \to L (numer (y)) \underset{˙}{\times} L (denom (y)) = L (numer (y) denom (x)) \underset{˙}{\times} L (denom (y) denom (x))$
92	39 33 29 36 51 48 91	syl132anc	$⊢ ((R \in DivRing \land chr (R) = 0) \land (x \in ℚ \land y \in ℚ)) \to L (numer (y)) \underset{˙}{\times} L (denom (y)) = L (numer (y) denom (x)) \underset{˙}{\times} L (denom (y) denom (x))$
93	1 2 3	qqhvq	$⊢ ((R \in DivRing \land chr (R) = 0) \land (numer (y) \in ℤ \land denom (y) \in ℤ \land denom (y) \neq 0)) \to ℚHom (R) (\frac{numer (y)}{denom (y)}) = L (numer (y)) \underset{˙}{\times} L (denom (y))$
94	44 33 29 49 93	syl13anc	$⊢ ((R \in DivRing \land chr (R) = 0) \land (x \in ℚ \land y \in ℚ)) \to ℚHom (R) (\frac{numer (y)}{denom (y)}) = L (numer (y)) \underset{˙}{\times} L (denom (y))$
95	64 66	mulcomd	$⊢ ((R \in DivRing \land chr (R) = 0) \land (x \in ℚ \land y \in ℚ)) \to denom (x) denom (y) = denom (y) denom (x)$
96	95	fveq2d	$⊢ ((R \in DivRing \land chr (R) = 0) \land (x \in ℚ \land y \in ℚ)) \to L (denom (x) denom (y)) = L (denom (y) denom (x))$
97	96	oveq2d	$⊢ ((R \in DivRing \land chr (R) = 0) \land (x \in ℚ \land y \in ℚ)) \to L (numer (y) denom (x)) \underset{˙}{\times} L (denom (x) denom (y)) = L (numer (y) denom (x)) \underset{˙}{\times} L (denom (y) denom (x))$
98	92 94 97	3eqtr4d	$⊢ ((R \in DivRing \land chr (R) = 0) \land (x \in ℚ \land y \in ℚ)) \to ℚHom (R) (\frac{numer (y)}{denom (y)}) = L (numer (y) denom (x)) \underset{˙}{\times} L (denom (x) denom (y))$
99	90 98	eqtrd	$⊢ ((R \in DivRing \land chr (R) = 0) \land (x \in ℚ \land y \in ℚ)) \to ℚHom (R) (y) = L (numer (y) denom (x)) \underset{˙}{\times} L (denom (x) denom (y))$
100	88 99	oveq12d	$⊢ ((R \in DivRing \land chr (R) = 0) \land (x \in ℚ \land y \in ℚ)) \to ℚHom (R) (x) +_{R} ℚHom (R) (y) = (L (numer (x) denom (y)) \underset{˙}{\times} L (denom (x) denom (y))) +_{R} (L (numer (y) denom (x)) \underset{˙}{\times} L (denom (x) denom (y)))$
101	57 81 100	3eqtr4d	$⊢ ((R \in DivRing \land chr (R) = 0) \land (x \in ℚ \land y \in ℚ)) \to ℚHom (R) (x + y) = ℚHom (R) (x) +_{R} ℚHom (R) (y)$
102	5 1 9 10 13 15 16 101	isghmd	$⊢ (R \in DivRing \land chr (R) = 0) \to ℚHom (R) \in (Q GrpHom R)$

Metamath Proof Explorer

Theorem qqhghm

Proof