Theorem 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	⊢ 𝐵 = ( Base ‘ 𝑅 )
	qqhval2.1	⊢ / = ( /r ‘ 𝑅 )
	qqhval2.2	⊢ 𝐿 = ( ℤRHom ‘ 𝑅 )
	qqhrhm.1	⊢ 𝑄 = ( ℂfld ↾s ℚ )
Assertion	qqhghm	⊢ ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) → ( ℚHom ‘ 𝑅 ) ∈ ( 𝑄 GrpHom 𝑅 ) )

Proof

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