qqhrhm - Mathbox for Thierry Arnoux

	Mathbox for Thierry Arnoux		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > qqhrhm		Structured version Visualization version GIF version

Theorem qqhrhm 33962

Description: The ℚHom 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.)

**Hypotheses**
Ref	Expression
qqhval2.0	⊢ 𝐵 = (Base‘𝑅)
qqhval2.1	⊢ / = (/_r‘𝑅)
qqhval2.2	⊢ 𝐿 = (ℤRHom‘𝑅)
qqhrhm.1	⊢ 𝑄 = (ℂ_fld ↾_s ℚ)

**Assertion**
Ref	Expression
qqhrhm	⊢ ((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) → (ℚHom‘𝑅) ∈ (𝑄 RingHom 𝑅))

Proof of Theorem qqhrhm Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		qqhrhm.1	. . 3 ⊢ 𝑄 = (ℂ_fld ↾_s ℚ)
2	1	qrngbas 27528	. 2 ⊢ ℚ = (Base‘𝑄)
3	1	qrng1 27531	. 2 ⊢ 1 = (1_r‘𝑄)
4		eqid 2729	. 2 ⊢ (1_r‘𝑅) = (1_r‘𝑅)
5		qex 12862	. . 3 ⊢ ℚ ∈ V
6		cnfldmul 21269	. . . 4 ⊢ · = (._r‘ℂ_fld)
7	1, 6	ressmulr 17211	. . 3 ⊢ (ℚ ∈ V → · = (._r‘𝑄))
8	5, 7	ax-mp 5	. 2 ⊢ · = (._r‘𝑄)
9		eqid 2729	. 2 ⊢ (._r‘𝑅) = (._r‘𝑅)
10	1	qdrng 27529	. . 3 ⊢ 𝑄 ∈ DivRing
11		drngring 20621	. . 3 ⊢ (𝑄 ∈ DivRing → 𝑄 ∈ Ring)
12	10, 11	mp1i 13	. 2 ⊢ ((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) → 𝑄 ∈ Ring)
13		isfld 20625	. . . . 5 ⊢ (𝑅 ∈ Field ↔ (𝑅 ∈ DivRing ∧ 𝑅 ∈ CRing))
14	13	simplbi 497	. . . 4 ⊢ (𝑅 ∈ Field → 𝑅 ∈ DivRing)
15	14	adantr 480	. . 3 ⊢ ((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) → 𝑅 ∈ DivRing)
16		drngring 20621	. . 3 ⊢ (𝑅 ∈ DivRing → 𝑅 ∈ Ring)
17	15, 16	syl 17	. 2 ⊢ ((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) → 𝑅 ∈ Ring)
18		qqhval2.0	. . . 4 ⊢ 𝐵 = (Base‘𝑅)
19		qqhval2.1	. . . 4 ⊢ / = (/_r‘𝑅)
20		qqhval2.2	. . . 4 ⊢ 𝐿 = (ℤRHom‘𝑅)
21	18, 19, 20	qqh1 33958	. . 3 ⊢ ((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) → ((ℚHom‘𝑅)‘1) = (1_r‘𝑅))
22	14, 21	sylan 580	. 2 ⊢ ((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) → ((ℚHom‘𝑅)‘1) = (1_r‘𝑅))
23		eqid 2729	. . . 4 ⊢ (Unit‘𝑅) = (Unit‘𝑅)
24		eqid 2729	. . . 4 ⊢ (+_g‘𝑅) = (+_g‘𝑅)
25	13	simprbi 496	. . . . 5 ⊢ (𝑅 ∈ Field → 𝑅 ∈ CRing)
26	25	ad2antrr 726	. . . 4 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → 𝑅 ∈ CRing)
27	20	zrhrhm 21418	. . . . . . 7 ⊢ (𝑅 ∈ Ring → 𝐿 ∈ (ℤ_ring RingHom 𝑅))
28		zringbas 21360	. . . . . . . 8 ⊢ ℤ = (Base‘ℤ_ring)
29	28, 18	rhmf 20370	. . . . . . 7 ⊢ (𝐿 ∈ (ℤ_ring RingHom 𝑅) → 𝐿:ℤ⟶𝐵)
30	17, 27, 29	3syl 18	. . . . . 6 ⊢ ((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) → 𝐿:ℤ⟶𝐵)
31	30	adantr 480	. . . . 5 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → 𝐿:ℤ⟶𝐵)
32		qnumcl 16651	. . . . . 6 ⊢ (𝑥 ∈ ℚ → (numer‘𝑥) ∈ ℤ)
33	32	ad2antrl 728	. . . . 5 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (numer‘𝑥) ∈ ℤ)
34	31, 33	ffvelcdmd 7019	. . . 4 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (𝐿‘(numer‘𝑥)) ∈ 𝐵)
35	14	ad2antrr 726	. . . . . 6 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → 𝑅 ∈ DivRing)
36		simplr 768	. . . . . 6 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (chr‘𝑅) = 0)
37	35, 36	jca 511	. . . . 5 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0))
38		qdencl 16652	. . . . . . 7 ⊢ (𝑥 ∈ ℚ → (denom‘𝑥) ∈ ℕ)
39	38	ad2antrl 728	. . . . . 6 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (denom‘𝑥) ∈ ℕ)
40	39	nnzd 12498	. . . . 5 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (denom‘𝑥) ∈ ℤ)
41	39	nnne0d 12178	. . . . 5 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (denom‘𝑥) ≠ 0)
42		eqid 2729	. . . . . 6 ⊢ (0_g‘𝑅) = (0_g‘𝑅)
43	18, 20, 42	elzrhunit 33950	. . . . 5 ⊢ (((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) ∧ ((denom‘𝑥) ∈ ℤ ∧ (denom‘𝑥) ≠ 0)) → (𝐿‘(denom‘𝑥)) ∈ (Unit‘𝑅))
44	37, 40, 41, 43	syl12anc 836	. . . 4 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (𝐿‘(denom‘𝑥)) ∈ (Unit‘𝑅))
45		qnumcl 16651	. . . . . 6 ⊢ (𝑦 ∈ ℚ → (numer‘𝑦) ∈ ℤ)
46	45	ad2antll 729	. . . . 5 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (numer‘𝑦) ∈ ℤ)
47	31, 46	ffvelcdmd 7019	. . . 4 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (𝐿‘(numer‘𝑦)) ∈ 𝐵)
48		qdencl 16652	. . . . . . 7 ⊢ (𝑦 ∈ ℚ → (denom‘𝑦) ∈ ℕ)
49	48	ad2antll 729	. . . . . 6 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (denom‘𝑦) ∈ ℕ)
50	49	nnzd 12498	. . . . 5 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (denom‘𝑦) ∈ ℤ)
51	49	nnne0d 12178	. . . . 5 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (denom‘𝑦) ≠ 0)
52	18, 20, 42	elzrhunit 33950	. . . . 5 ⊢ (((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) ∧ ((denom‘𝑦) ∈ ℤ ∧ (denom‘𝑦) ≠ 0)) → (𝐿‘(denom‘𝑦)) ∈ (Unit‘𝑅))
53	37, 50, 51, 52	syl12anc 836	. . . 4 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (𝐿‘(denom‘𝑦)) ∈ (Unit‘𝑅))
54	18, 23, 24, 19, 9, 26, 34, 44, 47, 53	rdivmuldivd 20298	. . 3 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (((𝐿‘(numer‘𝑥)) / (𝐿‘(denom‘𝑥)))(._r‘𝑅)((𝐿‘(numer‘𝑦)) / (𝐿‘(denom‘𝑦)))) = (((𝐿‘(numer‘𝑥))(._r‘𝑅)(𝐿‘(numer‘𝑦))) / ((𝐿‘(denom‘𝑥))(._r‘𝑅)(𝐿‘(denom‘𝑦)))))
55		qeqnumdivden 16657	. . . . . . 7 ⊢ (𝑥 ∈ ℚ → 𝑥 = ((numer‘𝑥) / (denom‘𝑥)))
56	55	fveq2d 6826	. . . . . 6 ⊢ (𝑥 ∈ ℚ → ((ℚHom‘𝑅)‘𝑥) = ((ℚHom‘𝑅)‘((numer‘𝑥) / (denom‘𝑥))))
57	56	ad2antrl 728	. . . . 5 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → ((ℚHom‘𝑅)‘𝑥) = ((ℚHom‘𝑅)‘((numer‘𝑥) / (denom‘𝑥))))
58	18, 19, 20	qqhvq 33960	. . . . . 6 ⊢ (((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) ∧ ((numer‘𝑥) ∈ ℤ ∧ (denom‘𝑥) ∈ ℤ ∧ (denom‘𝑥) ≠ 0)) → ((ℚHom‘𝑅)‘((numer‘𝑥) / (denom‘𝑥))) = ((𝐿‘(numer‘𝑥)) / (𝐿‘(denom‘𝑥))))
59	37, 33, 40, 41, 58	syl13anc 1374	. . . . 5 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → ((ℚHom‘𝑅)‘((numer‘𝑥) / (denom‘𝑥))) = ((𝐿‘(numer‘𝑥)) / (𝐿‘(denom‘𝑥))))
60	57, 59	eqtrd 2764	. . . 4 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → ((ℚHom‘𝑅)‘𝑥) = ((𝐿‘(numer‘𝑥)) / (𝐿‘(denom‘𝑥))))
61		qeqnumdivden 16657	. . . . . . 7 ⊢ (𝑦 ∈ ℚ → 𝑦 = ((numer‘𝑦) / (denom‘𝑦)))
62	61	fveq2d 6826	. . . . . 6 ⊢ (𝑦 ∈ ℚ → ((ℚHom‘𝑅)‘𝑦) = ((ℚHom‘𝑅)‘((numer‘𝑦) / (denom‘𝑦))))
63	62	ad2antll 729	. . . . 5 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → ((ℚHom‘𝑅)‘𝑦) = ((ℚHom‘𝑅)‘((numer‘𝑦) / (denom‘𝑦))))
64	18, 19, 20	qqhvq 33960	. . . . . 6 ⊢ (((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) ∧ ((numer‘𝑦) ∈ ℤ ∧ (denom‘𝑦) ∈ ℤ ∧ (denom‘𝑦) ≠ 0)) → ((ℚHom‘𝑅)‘((numer‘𝑦) / (denom‘𝑦))) = ((𝐿‘(numer‘𝑦)) / (𝐿‘(denom‘𝑦))))
65	37, 46, 50, 51, 64	syl13anc 1374	. . . . 5 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → ((ℚHom‘𝑅)‘((numer‘𝑦) / (denom‘𝑦))) = ((𝐿‘(numer‘𝑦)) / (𝐿‘(denom‘𝑦))))
66	63, 65	eqtrd 2764	. . . 4 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → ((ℚHom‘𝑅)‘𝑦) = ((𝐿‘(numer‘𝑦)) / (𝐿‘(denom‘𝑦))))
67	60, 66	oveq12d 7367	. . 3 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (((ℚHom‘𝑅)‘𝑥)(._r‘𝑅)((ℚHom‘𝑅)‘𝑦)) = (((𝐿‘(numer‘𝑥)) / (𝐿‘(denom‘𝑥)))(._r‘𝑅)((𝐿‘(numer‘𝑦)) / (𝐿‘(denom‘𝑦)))))
68	55	ad2antrl 728	. . . . . . 7 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → 𝑥 = ((numer‘𝑥) / (denom‘𝑥)))
69	61	ad2antll 729	. . . . . . 7 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → 𝑦 = ((numer‘𝑦) / (denom‘𝑦)))
70	68, 69	oveq12d 7367	. . . . . 6 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (𝑥 · 𝑦) = (((numer‘𝑥) / (denom‘𝑥)) · ((numer‘𝑦) / (denom‘𝑦))))
71	33	zcnd 12581	. . . . . . 7 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (numer‘𝑥) ∈ ℂ)
72	40	zcnd 12581	. . . . . . 7 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (denom‘𝑥) ∈ ℂ)
73	46	zcnd 12581	. . . . . . 7 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (numer‘𝑦) ∈ ℂ)
74	50	zcnd 12581	. . . . . . 7 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (denom‘𝑦) ∈ ℂ)
75	71, 72, 73, 74, 41, 51	divmuldivd 11941	. . . . . 6 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (((numer‘𝑥) / (denom‘𝑥)) · ((numer‘𝑦) / (denom‘𝑦))) = (((numer‘𝑥) · (numer‘𝑦)) / ((denom‘𝑥) · (denom‘𝑦))))
76	70, 75	eqtrd 2764	. . . . 5 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (𝑥 · 𝑦) = (((numer‘𝑥) · (numer‘𝑦)) / ((denom‘𝑥) · (denom‘𝑦))))
77	76	fveq2d 6826	. . . 4 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → ((ℚHom‘𝑅)‘(𝑥 · 𝑦)) = ((ℚHom‘𝑅)‘(((numer‘𝑥) · (numer‘𝑦)) / ((denom‘𝑥) · (denom‘𝑦)))))
78	33, 46	zmulcld 12586	. . . . 5 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → ((numer‘𝑥) · (numer‘𝑦)) ∈ ℤ)
79	40, 50	zmulcld 12586	. . . . 5 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → ((denom‘𝑥) · (denom‘𝑦)) ∈ ℤ)
80	72, 74, 41, 51	mulne0d 11772	. . . . 5 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → ((denom‘𝑥) · (denom‘𝑦)) ≠ 0)
81	18, 19, 20	qqhvq 33960	. . . . 5 ⊢ (((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) ∧ (((numer‘𝑥) · (numer‘𝑦)) ∈ ℤ ∧ ((denom‘𝑥) · (denom‘𝑦)) ∈ ℤ ∧ ((denom‘𝑥) · (denom‘𝑦)) ≠ 0)) → ((ℚHom‘𝑅)‘(((numer‘𝑥) · (numer‘𝑦)) / ((denom‘𝑥) · (denom‘𝑦)))) = ((𝐿‘((numer‘𝑥) · (numer‘𝑦))) / (𝐿‘((denom‘𝑥) · (denom‘𝑦)))))
82	37, 78, 79, 80, 81	syl13anc 1374	. . . 4 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → ((ℚHom‘𝑅)‘(((numer‘𝑥) · (numer‘𝑦)) / ((denom‘𝑥) · (denom‘𝑦)))) = ((𝐿‘((numer‘𝑥) · (numer‘𝑦))) / (𝐿‘((denom‘𝑥) · (denom‘𝑦)))))
83	35, 16	syl 17	. . . . . . 7 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → 𝑅 ∈ Ring)
84	83, 27	syl 17	. . . . . 6 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → 𝐿 ∈ (ℤ_ring RingHom 𝑅))
85		zringmulr 21364	. . . . . . 7 ⊢ · = (._r‘ℤ_ring)
86	28, 85, 9	rhmmul 20371	. . . . . 6 ⊢ ((𝐿 ∈ (ℤ_ring RingHom 𝑅) ∧ (numer‘𝑥) ∈ ℤ ∧ (numer‘𝑦) ∈ ℤ) → (𝐿‘((numer‘𝑥) · (numer‘𝑦))) = ((𝐿‘(numer‘𝑥))(._r‘𝑅)(𝐿‘(numer‘𝑦))))
87	84, 33, 46, 86	syl3anc 1373	. . . . 5 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (𝐿‘((numer‘𝑥) · (numer‘𝑦))) = ((𝐿‘(numer‘𝑥))(._r‘𝑅)(𝐿‘(numer‘𝑦))))
88	28, 85, 9	rhmmul 20371	. . . . . 6 ⊢ ((𝐿 ∈ (ℤ_ring RingHom 𝑅) ∧ (denom‘𝑥) ∈ ℤ ∧ (denom‘𝑦) ∈ ℤ) → (𝐿‘((denom‘𝑥) · (denom‘𝑦))) = ((𝐿‘(denom‘𝑥))(._r‘𝑅)(𝐿‘(denom‘𝑦))))
89	84, 40, 50, 88	syl3anc 1373	. . . . 5 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (𝐿‘((denom‘𝑥) · (denom‘𝑦))) = ((𝐿‘(denom‘𝑥))(._r‘𝑅)(𝐿‘(denom‘𝑦))))
90	87, 89	oveq12d 7367	. . . 4 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → ((𝐿‘((numer‘𝑥) · (numer‘𝑦))) / (𝐿‘((denom‘𝑥) · (denom‘𝑦)))) = (((𝐿‘(numer‘𝑥))(._r‘𝑅)(𝐿‘(numer‘𝑦))) / ((𝐿‘(denom‘𝑥))(._r‘𝑅)(𝐿‘(denom‘𝑦)))))
91	77, 82, 90	3eqtrd 2768	. . 3 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → ((ℚHom‘𝑅)‘(𝑥 · 𝑦)) = (((𝐿‘(numer‘𝑥))(._r‘𝑅)(𝐿‘(numer‘𝑦))) / ((𝐿‘(denom‘𝑥))(._r‘𝑅)(𝐿‘(denom‘𝑦)))))
92	54, 67, 91	3eqtr4rd 2775	. 2 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → ((ℚHom‘𝑅)‘(𝑥 · 𝑦)) = (((ℚHom‘𝑅)‘𝑥)(._r‘𝑅)((ℚHom‘𝑅)‘𝑦)))
93		cnfldadd 21267	. . . 4 ⊢ + = (+_g‘ℂ_fld)
94	1, 93	ressplusg 17195	. . 3 ⊢ (ℚ ∈ V → + = (+_g‘𝑄))
95	5, 94	ax-mp 5	. 2 ⊢ + = (+_g‘𝑄)
96	18, 19, 20	qqhf 33959	. . 3 ⊢ ((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) → (ℚHom‘𝑅):ℚ⟶𝐵)
97	14, 96	sylan 580	. 2 ⊢ ((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) → (ℚHom‘𝑅):ℚ⟶𝐵)
98	33, 50	zmulcld 12586	. . . . 5 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → ((numer‘𝑥) · (denom‘𝑦)) ∈ ℤ)
99	31, 98	ffvelcdmd 7019	. . . 4 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (𝐿‘((numer‘𝑥) · (denom‘𝑦))) ∈ 𝐵)
100	46, 40	zmulcld 12586	. . . . 5 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → ((numer‘𝑦) · (denom‘𝑥)) ∈ ℤ)
101	31, 100	ffvelcdmd 7019	. . . 4 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (𝐿‘((numer‘𝑦) · (denom‘𝑥))) ∈ 𝐵)
102	23, 9	unitmulcl 20265	. . . . . 6 ⊢ ((𝑅 ∈ Ring ∧ (𝐿‘(denom‘𝑥)) ∈ (Unit‘𝑅) ∧ (𝐿‘(denom‘𝑦)) ∈ (Unit‘𝑅)) → ((𝐿‘(denom‘𝑥))(._r‘𝑅)(𝐿‘(denom‘𝑦))) ∈ (Unit‘𝑅))
103	83, 44, 53, 102	syl3anc 1373	. . . . 5 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → ((𝐿‘(denom‘𝑥))(._r‘𝑅)(𝐿‘(denom‘𝑦))) ∈ (Unit‘𝑅))
104	89, 103	eqeltrd 2828	. . . 4 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (𝐿‘((denom‘𝑥) · (denom‘𝑦))) ∈ (Unit‘𝑅))
105	18, 23, 24, 19	dvrdir 20297	. . . 4 ⊢ ((𝑅 ∈ Ring ∧ ((𝐿‘((numer‘𝑥) · (denom‘𝑦))) ∈ 𝐵 ∧ (𝐿‘((numer‘𝑦) · (denom‘𝑥))) ∈ 𝐵 ∧ (𝐿‘((denom‘𝑥) · (denom‘𝑦))) ∈ (Unit‘𝑅))) → (((𝐿‘((numer‘𝑥) · (denom‘𝑦)))(+_g‘𝑅)(𝐿‘((numer‘𝑦) · (denom‘𝑥)))) / (𝐿‘((denom‘𝑥) · (denom‘𝑦)))) = (((𝐿‘((numer‘𝑥) · (denom‘𝑦))) / (𝐿‘((denom‘𝑥) · (denom‘𝑦))))(+_g‘𝑅)((𝐿‘((numer‘𝑦) · (denom‘𝑥))) / (𝐿‘((denom‘𝑥) · (denom‘𝑦))))))
106	83, 99, 101, 104, 105	syl13anc 1374	. . 3 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (((𝐿‘((numer‘𝑥) · (denom‘𝑦)))(+_g‘𝑅)(𝐿‘((numer‘𝑦) · (denom‘𝑥)))) / (𝐿‘((denom‘𝑥) · (denom‘𝑦)))) = (((𝐿‘((numer‘𝑥) · (denom‘𝑦))) / (𝐿‘((denom‘𝑥) · (denom‘𝑦))))(+_g‘𝑅)((𝐿‘((numer‘𝑦) · (denom‘𝑥))) / (𝐿‘((denom‘𝑥) · (denom‘𝑦))))))
107	68, 69	oveq12d 7367	. . . . . 6 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (𝑥 + 𝑦) = (((numer‘𝑥) / (denom‘𝑥)) + ((numer‘𝑦) / (denom‘𝑦))))
108	71, 72, 73, 74, 41, 51	divadddivd 11944	. . . . . 6 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (((numer‘𝑥) / (denom‘𝑥)) + ((numer‘𝑦) / (denom‘𝑦))) = ((((numer‘𝑥) · (denom‘𝑦)) + ((numer‘𝑦) · (denom‘𝑥))) / ((denom‘𝑥) · (denom‘𝑦))))
109	107, 108	eqtrd 2764	. . . . 5 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (𝑥 + 𝑦) = ((((numer‘𝑥) · (denom‘𝑦)) + ((numer‘𝑦) · (denom‘𝑥))) / ((denom‘𝑥) · (denom‘𝑦))))
110	109	fveq2d 6826	. . . 4 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → ((ℚHom‘𝑅)‘(𝑥 + 𝑦)) = ((ℚHom‘𝑅)‘((((numer‘𝑥) · (denom‘𝑦)) + ((numer‘𝑦) · (denom‘𝑥))) / ((denom‘𝑥) · (denom‘𝑦)))))
111	98, 100	zaddcld 12584	. . . . 5 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (((numer‘𝑥) · (denom‘𝑦)) + ((numer‘𝑦) · (denom‘𝑥))) ∈ ℤ)
112	18, 19, 20	qqhvq 33960	. . . . 5 ⊢ (((𝑅 ∈ 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‘𝑦)))))
113	37, 111, 79, 80, 112	syl13anc 1374	. . . 4 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → ((ℚHom‘𝑅)‘((((numer‘𝑥) · (denom‘𝑦)) + ((numer‘𝑦) · (denom‘𝑥))) / ((denom‘𝑥) · (denom‘𝑦)))) = ((𝐿‘(((numer‘𝑥) · (denom‘𝑦)) + ((numer‘𝑦) · (denom‘𝑥)))) / (𝐿‘((denom‘𝑥) · (denom‘𝑦)))))
114		rhmghm 20369	. . . . . 6 ⊢ (𝐿 ∈ (ℤ_ring RingHom 𝑅) → 𝐿 ∈ (ℤ_ring GrpHom 𝑅))
115	84, 114	syl 17	. . . . 5 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → 𝐿 ∈ (ℤ_ring GrpHom 𝑅))
116		zringplusg 21361	. . . . . . 7 ⊢ + = (+_g‘ℤ_ring)
117	28, 116, 24	ghmlin 19100	. . . . . 6 ⊢ ((𝐿 ∈ (ℤ_ring GrpHom 𝑅) ∧ ((numer‘𝑥) · (denom‘𝑦)) ∈ ℤ ∧ ((numer‘𝑦) · (denom‘𝑥)) ∈ ℤ) → (𝐿‘(((numer‘𝑥) · (denom‘𝑦)) + ((numer‘𝑦) · (denom‘𝑥)))) = ((𝐿‘((numer‘𝑥) · (denom‘𝑦)))(+_g‘𝑅)(𝐿‘((numer‘𝑦) · (denom‘𝑥)))))
118	117	oveq1d 7364	. . . . 5 ⊢ ((𝐿 ∈ (ℤ_ring GrpHom 𝑅) ∧ ((numer‘𝑥) · (denom‘𝑦)) ∈ ℤ ∧ ((numer‘𝑦) · (denom‘𝑥)) ∈ ℤ) → ((𝐿‘(((numer‘𝑥) · (denom‘𝑦)) + ((numer‘𝑦) · (denom‘𝑥)))) / (𝐿‘((denom‘𝑥) · (denom‘𝑦)))) = (((𝐿‘((numer‘𝑥) · (denom‘𝑦)))(+_g‘𝑅)(𝐿‘((numer‘𝑦) · (denom‘𝑥)))) / (𝐿‘((denom‘𝑥) · (denom‘𝑦)))))
119	115, 98, 100, 118	syl3anc 1373	. . . 4 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → ((𝐿‘(((numer‘𝑥) · (denom‘𝑦)) + ((numer‘𝑦) · (denom‘𝑥)))) / (𝐿‘((denom‘𝑥) · (denom‘𝑦)))) = (((𝐿‘((numer‘𝑥) · (denom‘𝑦)))(+_g‘𝑅)(𝐿‘((numer‘𝑦) · (denom‘𝑥)))) / (𝐿‘((denom‘𝑥) · (denom‘𝑦)))))
120	110, 113, 119	3eqtrd 2768	. . 3 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → ((ℚHom‘𝑅)‘(𝑥 + 𝑦)) = (((𝐿‘((numer‘𝑥) · (denom‘𝑦)))(+_g‘𝑅)(𝐿‘((numer‘𝑦) · (denom‘𝑥)))) / (𝐿‘((denom‘𝑥) · (denom‘𝑦)))))
121	23, 28, 19, 85	rhmdvd 33263	. . . . . 6 ⊢ ((𝐿 ∈ (ℤ_ring RingHom 𝑅) ∧ ((numer‘𝑥) ∈ ℤ ∧ (denom‘𝑥) ∈ ℤ ∧ (denom‘𝑦) ∈ ℤ) ∧ ((𝐿‘(denom‘𝑥)) ∈ (Unit‘𝑅) ∧ (𝐿‘(denom‘𝑦)) ∈ (Unit‘𝑅))) → ((𝐿‘(numer‘𝑥)) / (𝐿‘(denom‘𝑥))) = ((𝐿‘((numer‘𝑥) · (denom‘𝑦))) / (𝐿‘((denom‘𝑥) · (denom‘𝑦)))))
122	84, 33, 40, 50, 44, 53, 121	syl132anc 1390	. . . . 5 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → ((𝐿‘(numer‘𝑥)) / (𝐿‘(denom‘𝑥))) = ((𝐿‘((numer‘𝑥) · (denom‘𝑦))) / (𝐿‘((denom‘𝑥) · (denom‘𝑦)))))
123	57, 59, 122	3eqtrd 2768	. . . 4 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → ((ℚHom‘𝑅)‘𝑥) = ((𝐿‘((numer‘𝑥) · (denom‘𝑦))) / (𝐿‘((denom‘𝑥) · (denom‘𝑦)))))
124	23, 28, 19, 85	rhmdvd 33263	. . . . . . 7 ⊢ ((𝐿 ∈ (ℤ_ring RingHom 𝑅) ∧ ((numer‘𝑦) ∈ ℤ ∧ (denom‘𝑦) ∈ ℤ ∧ (denom‘𝑥) ∈ ℤ) ∧ ((𝐿‘(denom‘𝑦)) ∈ (Unit‘𝑅) ∧ (𝐿‘(denom‘𝑥)) ∈ (Unit‘𝑅))) → ((𝐿‘(numer‘𝑦)) / (𝐿‘(denom‘𝑦))) = ((𝐿‘((numer‘𝑦) · (denom‘𝑥))) / (𝐿‘((denom‘𝑦) · (denom‘𝑥)))))
125	84, 46, 50, 40, 53, 44, 124	syl132anc 1390	. . . . . 6 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → ((𝐿‘(numer‘𝑦)) / (𝐿‘(denom‘𝑦))) = ((𝐿‘((numer‘𝑦) · (denom‘𝑥))) / (𝐿‘((denom‘𝑦) · (denom‘𝑥)))))
126	72, 74	mulcomd 11136	. . . . . . . 8 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → ((denom‘𝑥) · (denom‘𝑦)) = ((denom‘𝑦) · (denom‘𝑥)))
127	126	fveq2d 6826	. . . . . . 7 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (𝐿‘((denom‘𝑥) · (denom‘𝑦))) = (𝐿‘((denom‘𝑦) · (denom‘𝑥))))
128	127	oveq2d 7365	. . . . . 6 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → ((𝐿‘((numer‘𝑦) · (denom‘𝑥))) / (𝐿‘((denom‘𝑥) · (denom‘𝑦)))) = ((𝐿‘((numer‘𝑦) · (denom‘𝑥))) / (𝐿‘((denom‘𝑦) · (denom‘𝑥)))))
129	125, 65, 128	3eqtr4d 2774	. . . . 5 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → ((ℚHom‘𝑅)‘((numer‘𝑦) / (denom‘𝑦))) = ((𝐿‘((numer‘𝑦) · (denom‘𝑥))) / (𝐿‘((denom‘𝑥) · (denom‘𝑦)))))
130	63, 129	eqtrd 2764	. . . 4 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → ((ℚHom‘𝑅)‘𝑦) = ((𝐿‘((numer‘𝑦) · (denom‘𝑥))) / (𝐿‘((denom‘𝑥) · (denom‘𝑦)))))
131	123, 130	oveq12d 7367	. . 3 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (((ℚHom‘𝑅)‘𝑥)(+_g‘𝑅)((ℚHom‘𝑅)‘𝑦)) = (((𝐿‘((numer‘𝑥) · (denom‘𝑦))) / (𝐿‘((denom‘𝑥) · (denom‘𝑦))))(+_g‘𝑅)((𝐿‘((numer‘𝑦) · (denom‘𝑥))) / (𝐿‘((denom‘𝑥) · (denom‘𝑦))))))
132	106, 120, 131	3eqtr4d 2774	. 2 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → ((ℚHom‘𝑅)‘(𝑥 + 𝑦)) = (((ℚHom‘𝑅)‘𝑥)(+_g‘𝑅)((ℚHom‘𝑅)‘𝑦)))
133	2, 3, 4, 8, 9, 12, 17, 22, 92, 18, 95, 24, 97, 132	isrhmd 20373	1 ⊢ ((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) → (ℚHom‘𝑅) ∈ (𝑄 RingHom 𝑅))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1086 = wceq 1540 ∈ wcel 2109 ≠ wne 2925 Vcvv 3436 ⟶wf 6478 ‘cfv 6482 (class class class)co 7349 0cc0 11009 1c1 11010 + caddc 11012 · cmul 11014 / cdiv 11777 ℕcn 12128 ℤcz 12471 ℚcq 12849 numercnumer 16644 denomcdenom 16645 Basecbs 17120 ↾_s cress 17141 +_gcplusg 17161 ._rcmulr 17162 0_gc0g 17343 GrpHom cghm 19091 1_rcur 20066 Ringcrg 20118 CRingccrg 20119 Unitcui 20240 /_rcdvr 20285 RingHom crh 20354 DivRingcdr 20614 Fieldcfield 20615 ℂ_fldccnfld 21261 ℤ_ringczring 21353 ℤRHomczrh 21406 chrcchr 21408 ℚHomcqqh 33943

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-rep 5218 ax-sep 5235 ax-nul 5245 ax-pow 5304 ax-pr 5371 ax-un 7671 ax-cnex 11065 ax-resscn 11066 ax-1cn 11067 ax-icn 11068 ax-addcl 11069 ax-addrcl 11070 ax-mulcl 11071 ax-mulrcl 11072 ax-mulcom 11073 ax-addass 11074 ax-mulass 11075 ax-distr 11076 ax-i2m1 11077 ax-1ne0 11078 ax-1rid 11079 ax-rnegex 11080 ax-rrecex 11081 ax-cnre 11082 ax-pre-lttri 11083 ax-pre-lttrn 11084 ax-pre-ltadd 11085 ax-pre-mulgt0 11086 ax-pre-sup 11087 ax-addf 11088 ax-mulf 11089

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-nel 3030 df-ral 3045 df-rex 3054 df-rmo 3343 df-reu 3344 df-rab 3395 df-v 3438 df-sbc 3743 df-csb 3852 df-dif 3906 df-un 3908 df-in 3910 df-ss 3920 df-pss 3923 df-nul 4285 df-if 4477 df-pw 4553 df-sn 4578 df-pr 4580 df-tp 4582 df-op 4584 df-uni 4859 df-iun 4943 df-br 5093 df-opab 5155 df-mpt 5174 df-tr 5200 df-id 5514 df-eprel 5519 df-po 5527 df-so 5528 df-fr 5572 df-we 5574 df-xp 5625 df-rel 5626 df-cnv 5627 df-co 5628 df-dm 5629 df-rn 5630 df-res 5631 df-ima 5632 df-pred 6249 df-ord 6310 df-on 6311 df-lim 6312 df-suc 6313 df-iota 6438 df-fun 6484 df-fn 6485 df-f 6486 df-f1 6487 df-fo 6488 df-f1o 6489 df-fv 6490 df-riota 7306 df-ov 7352 df-oprab 7353 df-mpo 7354 df-om 7800 df-1st 7924 df-2nd 7925 df-tpos 8159 df-frecs 8214 df-wrecs 8245 df-recs 8294 df-rdg 8332 df-1o 8388 df-er 8625 df-map 8755 df-en 8873 df-dom 8874 df-sdom 8875 df-fin 8876 df-sup 9332 df-inf 9333 df-pnf 11151 df-mnf 11152 df-xr 11153 df-ltxr 11154 df-le 11155 df-sub 11349 df-neg 11350 df-div 11778 df-nn 12129 df-2 12191 df-3 12192 df-4 12193 df-5 12194 df-6 12195 df-7 12196 df-8 12197 df-9 12198 df-n0 12385 df-z 12472 df-dec 12592 df-uz 12736 df-q 12850 df-rp 12894 df-fz 13411 df-fl 13696 df-mod 13774 df-seq 13909 df-exp 13969 df-cj 15006 df-re 15007 df-im 15008 df-sqrt 15142 df-abs 15143 df-dvds 16164 df-gcd 16406 df-numer 16646 df-denom 16647 df-gz 16842 df-struct 17058 df-sets 17075 df-slot 17093 df-ndx 17105 df-base 17121 df-ress 17142 df-plusg 17174 df-mulr 17175 df-starv 17176 df-tset 17180 df-ple 17181 df-ds 17183 df-unif 17184 df-0g 17345 df-mgm 18514 df-sgrp 18593 df-mnd 18609 df-mhm 18657 df-grp 18815 df-minusg 18816 df-sbg 18817 df-mulg 18947 df-subg 19002 df-ghm 19092 df-od 19407 df-cmn 19661 df-abl 19662 df-mgp 20026 df-rng 20038 df-ur 20067 df-ring 20120 df-cring 20121 df-oppr 20222 df-dvdsr 20242 df-unit 20243 df-invr 20273 df-dvr 20286 df-rhm 20357 df-subrng 20431 df-subrg 20455 df-drng 20616 df-field 20617 df-cnfld 21262 df-zring 21354 df-zrh 21410 df-chr 21412 df-qqh 33944

This theorem is referenced by: (None)

W3C validator