qqhrhm

Description: The QQHom homomorphism is a ring homomorphism if the target structure is a field. If the target structure is a division ring, it is a group homomorphism, but not a ring homomorphism, because it does not preserve the ring multiplication operation. (Contributed by Thierry Arnoux, 29-Oct-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	qqhrhm	$⊢ (R \in Field \land chr (R) = 0) \to ℚHom (R) \in (Q RingHom 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	4	qrng1	$⊢ 1 = 1_{Q}$
7		eqid	$⊢ 1_{R} = 1_{R}$
8		qex	$⊢ ℚ \in V$
9		cnfldmul	$⊢ \times = \cdot_{ℂ_{fld}}$
10	4 9	ressmulr	$⊢ ℚ \in V \to \times = \cdot_{Q}$
11	8 10	ax-mp	$⊢ \times = \cdot_{Q}$
12		eqid	$⊢ \cdot_{R} = \cdot_{R}$
13	4	qdrng	$⊢ Q \in DivRing$
14		drngring	$⊢ Q \in DivRing \to Q \in Ring$
15	13 14	mp1i	$⊢ (R \in Field \land chr (R) = 0) \to Q \in Ring$
16		isfld	$⊢ R \in Field \leftrightarrow (R \in DivRing \land R \in CRing)$
17	16	simplbi	$⊢ R \in Field \to R \in DivRing$
18	17	adantr	$⊢ (R \in Field \land chr (R) = 0) \to R \in DivRing$
19		drngring	$⊢ R \in DivRing \to R \in Ring$
20	18 19	syl	$⊢ (R \in Field \land chr (R) = 0) \to R \in Ring$
21	1 2 3	qqh1	$⊢ (R \in DivRing \land chr (R) = 0) \to ℚHom (R) (1) = 1_{R}$
22	17 21	sylan	$⊢ (R \in Field \land chr (R) = 0) \to ℚHom (R) (1) = 1_{R}$
23		eqid	$⊢ Unit (R) = Unit (R)$
24		eqid	$⊢ +_{R} = +_{R}$
25	16	simprbi	$⊢ R \in Field \to R \in CRing$
26	25	ad2antrr	$⊢ ((R \in Field \land chr (R) = 0) \land (x \in ℚ \land y \in ℚ)) \to R \in CRing$
27	3	zrhrhm	$⊢ R \in Ring \to L \in (ℤ_{ring} RingHom R)$
28		zringbas	$⊢ ℤ = {Base}_{ℤ_{ring}}$
29	28 1	rhmf	$⊢ L \in (ℤ_{ring} RingHom R) \to L : ℤ ⟶ B$
30	20 27 29	3syl	$⊢ (R \in Field \land chr (R) = 0) \to L : ℤ ⟶ B$
31	30	adantr	$⊢ ((R \in Field \land chr (R) = 0) \land (x \in ℚ \land y \in ℚ)) \to L : ℤ ⟶ B$
32		qnumcl	$⊢ x \in ℚ \to numer (x) \in ℤ$
33	32	ad2antrl	$⊢ ((R \in Field \land chr (R) = 0) \land (x \in ℚ \land y \in ℚ)) \to numer (x) \in ℤ$
34	31 33	ffvelcdmd	$⊢ ((R \in Field \land chr (R) = 0) \land (x \in ℚ \land y \in ℚ)) \to L (numer (x)) \in B$
35	17	ad2antrr	$⊢ ((R \in Field \land chr (R) = 0) \land (x \in ℚ \land y \in ℚ)) \to R \in DivRing$
36		simplr	$⊢ ((R \in Field \land chr (R) = 0) \land (x \in ℚ \land y \in ℚ)) \to chr (R) = 0$
37	35 36	jca	$⊢ ((R \in Field \land chr (R) = 0) \land (x \in ℚ \land y \in ℚ)) \to (R \in DivRing \land chr (R) = 0)$
38		qdencl	$⊢ x \in ℚ \to denom (x) \in ℕ$
39	38	ad2antrl	$⊢ ((R \in Field \land chr (R) = 0) \land (x \in ℚ \land y \in ℚ)) \to denom (x) \in ℕ$
40	39	nnzd	$⊢ ((R \in Field \land chr (R) = 0) \land (x \in ℚ \land y \in ℚ)) \to denom (x) \in ℤ$
41	39	nnne0d	$⊢ ((R \in Field \land chr (R) = 0) \land (x \in ℚ \land y \in ℚ)) \to denom (x) \neq 0$
42		eqid	$⊢ 0_{R} = 0_{R}$
43	1 3 42	elzrhunit	$⊢ ((R \in DivRing \land chr (R) = 0) \land (denom (x) \in ℤ \land denom (x) \neq 0)) \to L (denom (x)) \in Unit (R)$
44	37 40 41 43	syl12anc	$⊢ ((R \in Field \land chr (R) = 0) \land (x \in ℚ \land y \in ℚ)) \to L (denom (x)) \in Unit (R)$
45		qnumcl	$⊢ y \in ℚ \to numer (y) \in ℤ$
46	45	ad2antll	$⊢ ((R \in Field \land chr (R) = 0) \land (x \in ℚ \land y \in ℚ)) \to numer (y) \in ℤ$
47	31 46	ffvelcdmd	$⊢ ((R \in Field \land chr (R) = 0) \land (x \in ℚ \land y \in ℚ)) \to L (numer (y)) \in B$
48		qdencl	$⊢ y \in ℚ \to denom (y) \in ℕ$
49	48	ad2antll	$⊢ ((R \in Field \land chr (R) = 0) \land (x \in ℚ \land y \in ℚ)) \to denom (y) \in ℕ$
50	49	nnzd	$⊢ ((R \in Field \land chr (R) = 0) \land (x \in ℚ \land y \in ℚ)) \to denom (y) \in ℤ$
51	49	nnne0d	$⊢ ((R \in Field \land chr (R) = 0) \land (x \in ℚ \land y \in ℚ)) \to denom (y) \neq 0$
52	1 3 42	elzrhunit	$⊢ ((R \in DivRing \land chr (R) = 0) \land (denom (y) \in ℤ \land denom (y) \neq 0)) \to L (denom (y)) \in Unit (R)$
53	37 50 51 52	syl12anc	$⊢ ((R \in Field \land chr (R) = 0) \land (x \in ℚ \land y \in ℚ)) \to L (denom (y)) \in Unit (R)$
54	1 23 24 2 12 26 34 44 47 53	rdivmuldivd	$⊢ ((R \in Field \land chr (R) = 0) \land (x \in ℚ \land y \in ℚ)) \to (L (numer (x)) \underset{˙}{\times} L (denom (x))) \cdot_{R} (L (numer (y)) \underset{˙}{\times} L (denom (y))) = (L (numer (x)) \cdot_{R} L (numer (y))) \underset{˙}{\times} (L (denom (x)) \cdot_{R} L (denom (y)))$
55		qeqnumdivden	$⊢ x \in ℚ \to x = \frac{numer (x)}{denom (x)}$
56	55	fveq2d	$⊢ x \in ℚ \to ℚHom (R) (x) = ℚHom (R) (\frac{numer (x)}{denom (x)})$
57	56	ad2antrl	$⊢ ((R \in Field \land chr (R) = 0) \land (x \in ℚ \land y \in ℚ)) \to ℚHom (R) (x) = ℚHom (R) (\frac{numer (x)}{denom (x)})$
58	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))$
59	37 33 40 41 58	syl13anc	$⊢ ((R \in Field \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))$
60	57 59	eqtrd	$⊢ ((R \in Field \land chr (R) = 0) \land (x \in ℚ \land y \in ℚ)) \to ℚHom (R) (x) = L (numer (x)) \underset{˙}{\times} L (denom (x))$
61		qeqnumdivden	$⊢ y \in ℚ \to y = \frac{numer (y)}{denom (y)}$
62	61	fveq2d	$⊢ y \in ℚ \to ℚHom (R) (y) = ℚHom (R) (\frac{numer (y)}{denom (y)})$
63	62	ad2antll	$⊢ ((R \in Field \land chr (R) = 0) \land (x \in ℚ \land y \in ℚ)) \to ℚHom (R) (y) = ℚHom (R) (\frac{numer (y)}{denom (y)})$
64	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))$
65	37 46 50 51 64	syl13anc	$⊢ ((R \in Field \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))$
66	63 65	eqtrd	$⊢ ((R \in Field \land chr (R) = 0) \land (x \in ℚ \land y \in ℚ)) \to ℚHom (R) (y) = L (numer (y)) \underset{˙}{\times} L (denom (y))$
67	60 66	oveq12d	$⊢ ((R \in Field \land chr (R) = 0) \land (x \in ℚ \land y \in ℚ)) \to ℚHom (R) (x) \cdot_{R} ℚHom (R) (y) = (L (numer (x)) \underset{˙}{\times} L (denom (x))) \cdot_{R} (L (numer (y)) \underset{˙}{\times} L (denom (y)))$
68	55	ad2antrl	$⊢ ((R \in Field \land chr (R) = 0) \land (x \in ℚ \land y \in ℚ)) \to x = \frac{numer (x)}{denom (x)}$
69	61	ad2antll	$⊢ ((R \in Field \land chr (R) = 0) \land (x \in ℚ \land y \in ℚ)) \to y = \frac{numer (y)}{denom (y)}$
70	68 69	oveq12d	$⊢ ((R \in Field \land chr (R) = 0) \land (x \in ℚ \land y \in ℚ)) \to x y = (\frac{numer (x)}{denom (x)}) (\frac{numer (y)}{denom (y)})$
71	33	zcnd	$⊢ ((R \in Field \land chr (R) = 0) \land (x \in ℚ \land y \in ℚ)) \to numer (x) \in ℂ$
72	40	zcnd	$⊢ ((R \in Field \land chr (R) = 0) \land (x \in ℚ \land y \in ℚ)) \to denom (x) \in ℂ$
73	46	zcnd	$⊢ ((R \in Field \land chr (R) = 0) \land (x \in ℚ \land y \in ℚ)) \to numer (y) \in ℂ$
74	50	zcnd	$⊢ ((R \in Field \land chr (R) = 0) \land (x \in ℚ \land y \in ℚ)) \to denom (y) \in ℂ$
75	71 72 73 74 41 51	divmuldivd	$⊢ ((R \in Field \land chr (R) = 0) \land (x \in ℚ \land y \in ℚ)) \to (\frac{numer (x)}{denom (x)}) (\frac{numer (y)}{denom (y)}) = \frac{numer (x) numer (y)}{denom (x) denom (y)}$
76	70 75	eqtrd	$⊢ ((R \in Field \land chr (R) = 0) \land (x \in ℚ \land y \in ℚ)) \to x y = \frac{numer (x) numer (y)}{denom (x) denom (y)}$
77	76	fveq2d	$⊢ ((R \in Field \land chr (R) = 0) \land (x \in ℚ \land y \in ℚ)) \to ℚHom (R) (x y) = ℚHom (R) (\frac{numer (x) numer (y)}{denom (x) denom (y)})$
78	33 46	zmulcld	$⊢ ((R \in Field \land chr (R) = 0) \land (x \in ℚ \land y \in ℚ)) \to numer (x) numer (y) \in ℤ$
79	40 50	zmulcld	$⊢ ((R \in Field \land chr (R) = 0) \land (x \in ℚ \land y \in ℚ)) \to denom (x) denom (y) \in ℤ$
80	72 74 41 51	mulne0d	$⊢ ((R \in Field \land chr (R) = 0) \land (x \in ℚ \land y \in ℚ)) \to denom (x) denom (y) \neq 0$
81	1 2 3	qqhvq	$⊢ ((R \in DivRing \land chr (R) = 0) \land (numer (x) numer (y) \in ℤ \land denom (x) denom (y) \in ℤ \land denom (x) denom (y) \neq 0)) \to ℚHom (R) (\frac{numer (x) numer (y)}{denom (x) denom (y)}) = L (numer (x) numer (y)) \underset{˙}{\times} L (denom (x) denom (y))$
82	37 78 79 80 81	syl13anc	$⊢ ((R \in Field \land chr (R) = 0) \land (x \in ℚ \land y \in ℚ)) \to ℚHom (R) (\frac{numer (x) numer (y)}{denom (x) denom (y)}) = L (numer (x) numer (y)) \underset{˙}{\times} L (denom (x) denom (y))$
83	35 19	syl	$⊢ ((R \in Field \land chr (R) = 0) \land (x \in ℚ \land y \in ℚ)) \to R \in Ring$
84	83 27	syl	$⊢ ((R \in Field \land chr (R) = 0) \land (x \in ℚ \land y \in ℚ)) \to L \in (ℤ_{ring} RingHom R)$
85		zringmulr	$⊢ \times = \cdot_{ℤ_{ring}}$
86	28 85 12	rhmmul	$⊢ (L \in (ℤ_{ring} RingHom R) \land numer (x) \in ℤ \land numer (y) \in ℤ) \to L (numer (x) numer (y)) = L (numer (x)) \cdot_{R} L (numer (y))$
87	84 33 46 86	syl3anc	$⊢ ((R \in Field \land chr (R) = 0) \land (x \in ℚ \land y \in ℚ)) \to L (numer (x) numer (y)) = L (numer (x)) \cdot_{R} L (numer (y))$
88	28 85 12	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))$
89	84 40 50 88	syl3anc	$⊢ ((R \in Field \land chr (R) = 0) \land (x \in ℚ \land y \in ℚ)) \to L (denom (x) denom (y)) = L (denom (x)) \cdot_{R} L (denom (y))$
90	87 89	oveq12d	$⊢ ((R \in Field \land chr (R) = 0) \land (x \in ℚ \land y \in ℚ)) \to L (numer (x) numer (y)) \underset{˙}{\times} L (denom (x) denom (y)) = (L (numer (x)) \cdot_{R} L (numer (y))) \underset{˙}{\times} (L (denom (x)) \cdot_{R} L (denom (y)))$
91	77 82 90	3eqtrd	$⊢ ((R \in Field \land chr (R) = 0) \land (x \in ℚ \land y \in ℚ)) \to ℚHom (R) (x y) = (L (numer (x)) \cdot_{R} L (numer (y))) \underset{˙}{\times} (L (denom (x)) \cdot_{R} L (denom (y)))$
92	54 67 91	3eqtr4rd	$⊢ ((R \in Field \land chr (R) = 0) \land (x \in ℚ \land y \in ℚ)) \to ℚHom (R) (x y) = ℚHom (R) (x) \cdot_{R} ℚHom (R) (y)$
93		cnfldadd	$⊢ + = +_{ℂ_{fld}}$
94	4 93	ressplusg	$⊢ ℚ \in V \to + = +_{Q}$
95	8 94	ax-mp	$⊢ + = +_{Q}$
96	1 2 3	qqhf	$⊢ (R \in DivRing \land chr (R) = 0) \to ℚHom (R) : ℚ ⟶ B$
97	17 96	sylan	$⊢ (R \in Field \land chr (R) = 0) \to ℚHom (R) : ℚ ⟶ B$
98	33 50	zmulcld	$⊢ ((R \in Field \land chr (R) = 0) \land (x \in ℚ \land y \in ℚ)) \to numer (x) denom (y) \in ℤ$
99	31 98	ffvelcdmd	$⊢ ((R \in Field \land chr (R) = 0) \land (x \in ℚ \land y \in ℚ)) \to L (numer (x) denom (y)) \in B$
100	46 40	zmulcld	$⊢ ((R \in Field \land chr (R) = 0) \land (x \in ℚ \land y \in ℚ)) \to numer (y) denom (x) \in ℤ$
101	31 100	ffvelcdmd	$⊢ ((R \in Field \land chr (R) = 0) \land (x \in ℚ \land y \in ℚ)) \to L (numer (y) denom (x)) \in B$
102	23 12	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)$
103	83 44 53 102	syl3anc	$⊢ ((R \in Field \land chr (R) = 0) \land (x \in ℚ \land y \in ℚ)) \to L (denom (x)) \cdot_{R} L (denom (y)) \in Unit (R)$
104	89 103	eqeltrd	$⊢ ((R \in Field \land chr (R) = 0) \land (x \in ℚ \land y \in ℚ)) \to L (denom (x) denom (y)) \in Unit (R)$
105	1 23 24 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)))$
106	83 99 101 104 105	syl13anc	$⊢ ((R \in Field \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)))$
107	68 69	oveq12d	$⊢ ((R \in Field \land chr (R) = 0) \land (x \in ℚ \land y \in ℚ)) \to x + y = (\frac{numer (x)}{denom (x)}) + (\frac{numer (y)}{denom (y)})$
108	71 72 73 74 41 51	divadddivd	$⊢ ((R \in Field \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)}$
109	107 108	eqtrd	$⊢ ((R \in Field \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)}$
110	109	fveq2d	$⊢ ((R \in Field \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)})$
111	98 100	zaddcld	$⊢ ((R \in Field \land chr (R) = 0) \land (x \in ℚ \land y \in ℚ)) \to numer (x) denom (y) + numer (y) denom (x) \in ℤ$
112	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))$
113	37 111 79 80 112	syl13anc	$⊢ ((R \in Field \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))$
114		rhmghm	$⊢ L \in (ℤ_{ring} RingHom R) \to L \in (ℤ_{ring} GrpHom R)$
115	84 114	syl	$⊢ ((R \in Field \land chr (R) = 0) \land (x \in ℚ \land y \in ℚ)) \to L \in (ℤ_{ring} GrpHom R)$
116		zringplusg	$⊢ + = +_{ℤ_{ring}}$
117	28 116 24	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))$
118	117	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))$
119	115 98 100 118	syl3anc	$⊢ ((R \in Field \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))$
120	110 113 119	3eqtrd	$⊢ ((R \in Field \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))$
121	23 28 2 85	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))$
122	84 33 40 50 44 53 121	syl132anc	$⊢ ((R \in Field \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))$
123	57 59 122	3eqtrd	$⊢ ((R \in Field \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))$
124	23 28 2 85	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))$
125	84 46 50 40 53 44 124	syl132anc	$⊢ ((R \in Field \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))$
126	72 74	mulcomd	$⊢ ((R \in Field \land chr (R) = 0) \land (x \in ℚ \land y \in ℚ)) \to denom (x) denom (y) = denom (y) denom (x)$
127	126	fveq2d	$⊢ ((R \in Field \land chr (R) = 0) \land (x \in ℚ \land y \in ℚ)) \to L (denom (x) denom (y)) = L (denom (y) denom (x))$
128	127	oveq2d	$⊢ ((R \in Field \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))$
129	125 65 128	3eqtr4d	$⊢ ((R \in Field \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))$
130	63 129	eqtrd	$⊢ ((R \in Field \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))$
131	123 130	oveq12d	$⊢ ((R \in Field \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)))$
132	106 120 131	3eqtr4d	$⊢ ((R \in Field \land chr (R) = 0) \land (x \in ℚ \land y \in ℚ)) \to ℚHom (R) (x + y) = ℚHom (R) (x) +_{R} ℚHom (R) (y)$
133	5 6 7 11 12 15 20 22 92 1 95 24 97 132	isrhmd	$⊢ (R \in Field \land chr (R) = 0) \to ℚHom (R) \in (Q RingHom R)$

Metamath Proof Explorer

Theorem qqhrhm

Proof