Theorem qqhrhm 34621

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 27946	. 2 ⊢ ℚ = (Base‘𝑄)
3	1	qrng1 27949	. 2 ⊢ 1 = (1r‘𝑄)
4		eqid 2761	. 2 ⊢ (1r‘𝑅) = (1r‘𝑅)
5		qex 13088	. . 3 ⊢ ℚ ∈ V
6		cnfldmul 21686	. . . 4 ⊢ · = (.r‘ℂfld)
7	1, 6	ressmulr 17478	. . 3 ⊢ (ℚ ∈ V → · = (.r‘𝑄))
8	5, 7	ax-mp 5	. 2 ⊢ · = (.r‘𝑄)
9		eqid 2761	. 2 ⊢ (.r‘𝑅) = (.r‘𝑅)
10	1	qdrng 27947	. . 3 ⊢ 𝑄 ∈ DivRing
11		drngring 20987	. . 3 ⊢ (𝑄 ∈ DivRing → 𝑄 ∈ Ring)
12	10, 11	mp1i 14	. 2 ⊢ ((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) → 𝑄 ∈ Ring)
13		isfld 20993	. . . . 5 ⊢ (𝑅 ∈ Field ↔ (𝑅 ∈ DivRing ∧ 𝑅 ∈ CRing))
14	13	simplbi 502	. . . 4 ⊢ (𝑅 ∈ Field → 𝑅 ∈ DivRing)
15	14	adantr 486	. . 3 ⊢ ((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) → 𝑅 ∈ DivRing)
16		drngring 20987	. . 3 ⊢ (𝑅 ∈ DivRing → 𝑅 ∈ Ring)
17	15, 16	syl 18	. 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 34617	. . 3 ⊢ ((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) → ((ℚHom‘𝑅)‘1) = (1r‘𝑅))
22	14, 21	sylan 592	. 2 ⊢ ((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) → ((ℚHom‘𝑅)‘1) = (1r‘𝑅))
23		eqid 2761	. . . 4 ⊢ (Unit‘𝑅) = (Unit‘𝑅)
24		eqid 2761	. . . 4 ⊢ (+g‘𝑅) = (+g‘𝑅)
25	13	simprbi 503	. . . . 5 ⊢ (𝑅 ∈ Field → 𝑅 ∈ CRing)
26	25	ad2antrr 739	. . . 4 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → 𝑅 ∈ CRing)
27	20	zrhrhm 21817	. . . . . . 7 ⊢ (𝑅 ∈ Ring → 𝐿 ∈ (ℤring RingHom 𝑅))
28		zringbas 21759	. . . . . . . 8 ⊢ ℤ = (Base‘ℤring)
29	28, 18	rhmf 20715	. . . . . . 7 ⊢ (𝐿 ∈ (ℤring RingHom 𝑅) → 𝐿:ℤ⟶𝐵)
30	17, 27, 29	3syl 19	. . . . . 6 ⊢ ((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) → 𝐿:ℤ⟶𝐵)
31	30	adantr 486	. . . . 5 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → 𝐿:ℤ⟶𝐵)
32		qnumcl 16916	. . . . . 6 ⊢ (𝑥 ∈ ℚ → (numer‘𝑥) ∈ ℤ)
33	32	ad2antrl 741	. . . . 5 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (numer‘𝑥) ∈ ℤ)
34	31, 33	ffvelcdmd 7085	. . . 4 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (𝐿‘(numer‘𝑥)) ∈ 𝐵)
35	14	ad2antrr 739	. . . . . 6 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → 𝑅 ∈ DivRing)
36		simplr 781	. . . . . 6 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (chr‘𝑅) = 0)
37	35, 36	jca 521	. . . . 5 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0))
38		qdencl 16917	. . . . . . 7 ⊢ (𝑥 ∈ ℚ → (denom‘𝑥) ∈ ℕ)
39	38	ad2antrl 741	. . . . . 6 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (denom‘𝑥) ∈ ℕ)
40	39	nnzd 12719	. . . . 5 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (denom‘𝑥) ∈ ℤ)
41	39	nnne0d 12388	. . . . 5 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (denom‘𝑥) ≠ 0)
42		eqid 2761	. . . . . 6 ⊢ (0g‘𝑅) = (0g‘𝑅)
43	18, 20, 42	elzrhunit 34609	. . . . 5 ⊢ (((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) ∧ ((denom‘𝑥) ∈ ℤ ∧ (denom‘𝑥) ≠ 0)) → (𝐿‘(denom‘𝑥)) ∈ (Unit‘𝑅))
44	37, 40, 41, 43	syl12anc 850	. . . 4 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (𝐿‘(denom‘𝑥)) ∈ (Unit‘𝑅))
45		qnumcl 16916	. . . . . 6 ⊢ (𝑦 ∈ ℚ → (numer‘𝑦) ∈ ℤ)
46	45	ad2antll 742	. . . . 5 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (numer‘𝑦) ∈ ℤ)
47	31, 46	ffvelcdmd 7085	. . . 4 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (𝐿‘(numer‘𝑦)) ∈ 𝐵)
48		qdencl 16917	. . . . . . 7 ⊢ (𝑦 ∈ ℚ → (denom‘𝑦) ∈ ℕ)
49	48	ad2antll 742	. . . . . 6 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (denom‘𝑦) ∈ ℕ)
50	49	nnzd 12719	. . . . 5 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (denom‘𝑦) ∈ ℤ)
51	49	nnne0d 12388	. . . . 5 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (denom‘𝑦) ≠ 0)
52	18, 20, 42	elzrhunit 34609	. . . . 5 ⊢ (((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) ∧ ((denom‘𝑦) ∈ ℤ ∧ (denom‘𝑦) ≠ 0)) → (𝐿‘(denom‘𝑦)) ∈ (Unit‘𝑅))
53	37, 50, 51, 52	syl12anc 850	. . . 4 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (𝐿‘(denom‘𝑦)) ∈ (Unit‘𝑅))
54	18, 23, 24, 19, 9, 26, 34, 44, 47, 53	rdivmuldivd 20643	. . 3 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (((𝐿‘(numer‘𝑥)) / (𝐿‘(denom‘𝑥)))(.r‘𝑅)((𝐿‘(numer‘𝑦)) / (𝐿‘(denom‘𝑦)))) = (((𝐿‘(numer‘𝑥))(.r‘𝑅)(𝐿‘(numer‘𝑦))) / ((𝐿‘(denom‘𝑥))(.r‘𝑅)(𝐿‘(denom‘𝑦)))))
55		qeqnumdivden 16922	. . . . . . 7 ⊢ (𝑥 ∈ ℚ → 𝑥 = ((numer‘𝑥) / (denom‘𝑥)))
56	55	fveq2d 6889	. . . . . 6 ⊢ (𝑥 ∈ ℚ → ((ℚHom‘𝑅)‘𝑥) = ((ℚHom‘𝑅)‘((numer‘𝑥) / (denom‘𝑥))))
57	56	ad2antrl 741	. . . . 5 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → ((ℚHom‘𝑅)‘𝑥) = ((ℚHom‘𝑅)‘((numer‘𝑥) / (denom‘𝑥))))
58	18, 19, 20	qqhvq 34619	. . . . . 6 ⊢ (((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) ∧ ((numer‘𝑥) ∈ ℤ ∧ (denom‘𝑥) ∈ ℤ ∧ (denom‘𝑥) ≠ 0)) → ((ℚHom‘𝑅)‘((numer‘𝑥) / (denom‘𝑥))) = ((𝐿‘(numer‘𝑥)) / (𝐿‘(denom‘𝑥))))
59	37, 33, 40, 41, 58	syl13anc 1399	. . . . 5 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → ((ℚHom‘𝑅)‘((numer‘𝑥) / (denom‘𝑥))) = ((𝐿‘(numer‘𝑥)) / (𝐿‘(denom‘𝑥))))
60	57, 59	eqtrd 2796	. . . 4 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → ((ℚHom‘𝑅)‘𝑥) = ((𝐿‘(numer‘𝑥)) / (𝐿‘(denom‘𝑥))))
61		qeqnumdivden 16922	. . . . . . 7 ⊢ (𝑦 ∈ ℚ → 𝑦 = ((numer‘𝑦) / (denom‘𝑦)))
62	61	fveq2d 6889	. . . . . 6 ⊢ (𝑦 ∈ ℚ → ((ℚHom‘𝑅)‘𝑦) = ((ℚHom‘𝑅)‘((numer‘𝑦) / (denom‘𝑦))))
63	62	ad2antll 742	. . . . 5 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → ((ℚHom‘𝑅)‘𝑦) = ((ℚHom‘𝑅)‘((numer‘𝑦) / (denom‘𝑦))))
64	18, 19, 20	qqhvq 34619	. . . . . 6 ⊢ (((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) ∧ ((numer‘𝑦) ∈ ℤ ∧ (denom‘𝑦) ∈ ℤ ∧ (denom‘𝑦) ≠ 0)) → ((ℚHom‘𝑅)‘((numer‘𝑦) / (denom‘𝑦))) = ((𝐿‘(numer‘𝑦)) / (𝐿‘(denom‘𝑦))))
65	37, 46, 50, 51, 64	syl13anc 1399	. . . . 5 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → ((ℚHom‘𝑅)‘((numer‘𝑦) / (denom‘𝑦))) = ((𝐿‘(numer‘𝑦)) / (𝐿‘(denom‘𝑦))))
66	63, 65	eqtrd 2796	. . . 4 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → ((ℚHom‘𝑅)‘𝑦) = ((𝐿‘(numer‘𝑦)) / (𝐿‘(denom‘𝑦))))
67	60, 66	oveq12d 7438	. . 3 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (((ℚHom‘𝑅)‘𝑥)(.r‘𝑅)((ℚHom‘𝑅)‘𝑦)) = (((𝐿‘(numer‘𝑥)) / (𝐿‘(denom‘𝑥)))(.r‘𝑅)((𝐿‘(numer‘𝑦)) / (𝐿‘(denom‘𝑦)))))
68	55	ad2antrl 741	. . . . . . 7 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → 𝑥 = ((numer‘𝑥) / (denom‘𝑥)))
69	61	ad2antll 742	. . . . . . 7 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → 𝑦 = ((numer‘𝑦) / (denom‘𝑦)))
70	68, 69	oveq12d 7438	. . . . . 6 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (𝑥 · 𝑦) = (((numer‘𝑥) / (denom‘𝑥)) · ((numer‘𝑦) / (denom‘𝑦))))
71	33	zcnd 12804	. . . . . . 7 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (numer‘𝑥) ∈ ℂ)
72	40	zcnd 12804	. . . . . . 7 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (denom‘𝑥) ∈ ℂ)
73	46	zcnd 12804	. . . . . . 7 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (numer‘𝑦) ∈ ℂ)
74	50	zcnd 12804	. . . . . . 7 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (denom‘𝑦) ∈ ℂ)
75	71, 72, 73, 74, 41, 51	divmuldivd 12134	. . . . . 6 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (((numer‘𝑥) / (denom‘𝑥)) · ((numer‘𝑦) / (denom‘𝑦))) = (((numer‘𝑥) · (numer‘𝑦)) / ((denom‘𝑥) · (denom‘𝑦))))
76	70, 75	eqtrd 2796	. . . . 5 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (𝑥 · 𝑦) = (((numer‘𝑥) · (numer‘𝑦)) / ((denom‘𝑥) · (denom‘𝑦))))
77	76	fveq2d 6889	. . . 4 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → ((ℚHom‘𝑅)‘(𝑥 · 𝑦)) = ((ℚHom‘𝑅)‘(((numer‘𝑥) · (numer‘𝑦)) / ((denom‘𝑥) · (denom‘𝑦)))))
78	33, 46	zmulcld 12809	. . . . 5 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → ((numer‘𝑥) · (numer‘𝑦)) ∈ ℤ)
79	40, 50	zmulcld 12809	. . . . 5 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → ((denom‘𝑥) · (denom‘𝑦)) ∈ ℤ)
80	72, 74, 41, 51	mulne0d 11968	. . . . 5 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → ((denom‘𝑥) · (denom‘𝑦)) ≠ 0)
81	18, 19, 20	qqhvq 34619	. . . . 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 1399	. . . 4 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → ((ℚHom‘𝑅)‘(((numer‘𝑥) · (numer‘𝑦)) / ((denom‘𝑥) · (denom‘𝑦)))) = ((𝐿‘((numer‘𝑥) · (numer‘𝑦))) / (𝐿‘((denom‘𝑥) · (denom‘𝑦)))))
83	35, 16	syl 18	. . . . . . 7 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → 𝑅 ∈ Ring)
84	83, 27	syl 18	. . . . . 6 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → 𝐿 ∈ (ℤring RingHom 𝑅))
85		zringmulr 21763	. . . . . . 7 ⊢ · = (.r‘ℤring)
86	28, 85, 9	rhmmul 20720	. . . . . 6 ⊢ ((𝐿 ∈ (ℤring RingHom 𝑅) ∧ (numer‘𝑥) ∈ ℤ ∧ (numer‘𝑦) ∈ ℤ) → (𝐿‘((numer‘𝑥) · (numer‘𝑦))) = ((𝐿‘(numer‘𝑥))(.r‘𝑅)(𝐿‘(numer‘𝑦))))
87	84, 33, 46, 86	syl3anc 1398	. . . . 5 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (𝐿‘((numer‘𝑥) · (numer‘𝑦))) = ((𝐿‘(numer‘𝑥))(.r‘𝑅)(𝐿‘(numer‘𝑦))))
88	28, 85, 9	rhmmul 20720	. . . . . 6 ⊢ ((𝐿 ∈ (ℤring RingHom 𝑅) ∧ (denom‘𝑥) ∈ ℤ ∧ (denom‘𝑦) ∈ ℤ) → (𝐿‘((denom‘𝑥) · (denom‘𝑦))) = ((𝐿‘(denom‘𝑥))(.r‘𝑅)(𝐿‘(denom‘𝑦))))
89	84, 40, 50, 88	syl3anc 1398	. . . . 5 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (𝐿‘((denom‘𝑥) · (denom‘𝑦))) = ((𝐿‘(denom‘𝑥))(.r‘𝑅)(𝐿‘(denom‘𝑦))))
90	87, 89	oveq12d 7438	. . . 4 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → ((𝐿‘((numer‘𝑥) · (numer‘𝑦))) / (𝐿‘((denom‘𝑥) · (denom‘𝑦)))) = (((𝐿‘(numer‘𝑥))(.r‘𝑅)(𝐿‘(numer‘𝑦))) / ((𝐿‘(denom‘𝑥))(.r‘𝑅)(𝐿‘(denom‘𝑦)))))
91	77, 82, 90	3eqtrd 2800	. . 3 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → ((ℚHom‘𝑅)‘(𝑥 · 𝑦)) = (((𝐿‘(numer‘𝑥))(.r‘𝑅)(𝐿‘(numer‘𝑦))) / ((𝐿‘(denom‘𝑥))(.r‘𝑅)(𝐿‘(denom‘𝑦)))))
92	54, 67, 91	3eqtr4rd 2807	. 2 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → ((ℚHom‘𝑅)‘(𝑥 · 𝑦)) = (((ℚHom‘𝑅)‘𝑥)(.r‘𝑅)((ℚHom‘𝑅)‘𝑦)))
93		cnfldadd 21684	. . . 4 ⊢ + = (+g‘ℂfld)
94	1, 93	ressplusg 17462	. . 3 ⊢ (ℚ ∈ V → + = (+g‘𝑄))
95	5, 94	ax-mp 5	. 2 ⊢ + = (+g‘𝑄)
96	18, 19, 20	qqhf 34618	. . 3 ⊢ ((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) → (ℚHom‘𝑅):ℚ⟶𝐵)
97	14, 96	sylan 592	. 2 ⊢ ((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) → (ℚHom‘𝑅):ℚ⟶𝐵)
98	33, 50	zmulcld 12809	. . . . 5 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → ((numer‘𝑥) · (denom‘𝑦)) ∈ ℤ)
99	31, 98	ffvelcdmd 7085	. . . 4 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (𝐿‘((numer‘𝑥) · (denom‘𝑦))) ∈ 𝐵)
100	46, 40	zmulcld 12809	. . . . 5 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → ((numer‘𝑦) · (denom‘𝑥)) ∈ ℤ)
101	31, 100	ffvelcdmd 7085	. . . 4 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (𝐿‘((numer‘𝑦) · (denom‘𝑥))) ∈ 𝐵)
102	23, 9	unitmulcl 20610	. . . . . 6 ⊢ ((𝑅 ∈ Ring ∧ (𝐿‘(denom‘𝑥)) ∈ (Unit‘𝑅) ∧ (𝐿‘(denom‘𝑦)) ∈ (Unit‘𝑅)) → ((𝐿‘(denom‘𝑥))(.r‘𝑅)(𝐿‘(denom‘𝑦))) ∈ (Unit‘𝑅))
103	83, 44, 53, 102	syl3anc 1398	. . . . 5 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → ((𝐿‘(denom‘𝑥))(.r‘𝑅)(𝐿‘(denom‘𝑦))) ∈ (Unit‘𝑅))
104	89, 103	eqeltrd 2861	. . . 4 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (𝐿‘((denom‘𝑥) · (denom‘𝑦))) ∈ (Unit‘𝑅))
105	18, 23, 24, 19	dvrdir 20642	. . . 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 1399	. . 3 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (((𝐿‘((numer‘𝑥) · (denom‘𝑦)))(+g‘𝑅)(𝐿‘((numer‘𝑦) · (denom‘𝑥)))) / (𝐿‘((denom‘𝑥) · (denom‘𝑦)))) = (((𝐿‘((numer‘𝑥) · (denom‘𝑦))) / (𝐿‘((denom‘𝑥) · (denom‘𝑦))))(+g‘𝑅)((𝐿‘((numer‘𝑦) · (denom‘𝑥))) / (𝐿‘((denom‘𝑥) · (denom‘𝑦))))))
107	68, 69	oveq12d 7438	. . . . . 6 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (𝑥 + 𝑦) = (((numer‘𝑥) / (denom‘𝑥)) + ((numer‘𝑦) / (denom‘𝑦))))
108	71, 72, 73, 74, 41, 51	divadddivd 12137	. . . . . 6 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (((numer‘𝑥) / (denom‘𝑥)) + ((numer‘𝑦) / (denom‘𝑦))) = ((((numer‘𝑥) · (denom‘𝑦)) + ((numer‘𝑦) · (denom‘𝑥))) / ((denom‘𝑥) · (denom‘𝑦))))
109	107, 108	eqtrd 2796	. . . . 5 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (𝑥 + 𝑦) = ((((numer‘𝑥) · (denom‘𝑦)) + ((numer‘𝑦) · (denom‘𝑥))) / ((denom‘𝑥) · (denom‘𝑦))))
110	109	fveq2d 6889	. . . 4 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → ((ℚHom‘𝑅)‘(𝑥 + 𝑦)) = ((ℚHom‘𝑅)‘((((numer‘𝑥) · (denom‘𝑦)) + ((numer‘𝑦) · (denom‘𝑥))) / ((denom‘𝑥) · (denom‘𝑦)))))
111	98, 100	zaddcld 12807	. . . . 5 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (((numer‘𝑥) · (denom‘𝑦)) + ((numer‘𝑦) · (denom‘𝑥))) ∈ ℤ)
112	18, 19, 20	qqhvq 34619	. . . . 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 1399	. . . 4 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → ((ℚHom‘𝑅)‘((((numer‘𝑥) · (denom‘𝑦)) + ((numer‘𝑦) · (denom‘𝑥))) / ((denom‘𝑥) · (denom‘𝑦)))) = ((𝐿‘(((numer‘𝑥) · (denom‘𝑦)) + ((numer‘𝑦) · (denom‘𝑥)))) / (𝐿‘((denom‘𝑥) · (denom‘𝑦)))))
114		rhmghm 20714	. . . . . 6 ⊢ (𝐿 ∈ (ℤring RingHom 𝑅) → 𝐿 ∈ (ℤring GrpHom 𝑅))
115	84, 114	syl 18	. . . . 5 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → 𝐿 ∈ (ℤring GrpHom 𝑅))
116		zringplusg 21760	. . . . . . 7 ⊢ + = (+g‘ℤring)
117	28, 116, 24	ghmlin 19435	. . . . . 6 ⊢ ((𝐿 ∈ (ℤring GrpHom 𝑅) ∧ ((numer‘𝑥) · (denom‘𝑦)) ∈ ℤ ∧ ((numer‘𝑦) · (denom‘𝑥)) ∈ ℤ) → (𝐿‘(((numer‘𝑥) · (denom‘𝑦)) + ((numer‘𝑦) · (denom‘𝑥)))) = ((𝐿‘((numer‘𝑥) · (denom‘𝑦)))(+g‘𝑅)(𝐿‘((numer‘𝑦) · (denom‘𝑥)))))
118	117	oveq1d 7435	. . . . 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 1398	. . . 4 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → ((𝐿‘(((numer‘𝑥) · (denom‘𝑦)) + ((numer‘𝑦) · (denom‘𝑥)))) / (𝐿‘((denom‘𝑥) · (denom‘𝑦)))) = (((𝐿‘((numer‘𝑥) · (denom‘𝑦)))(+g‘𝑅)(𝐿‘((numer‘𝑦) · (denom‘𝑥)))) / (𝐿‘((denom‘𝑥) · (denom‘𝑦)))))
120	110, 113, 119	3eqtrd 2800	. . 3 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → ((ℚHom‘𝑅)‘(𝑥 + 𝑦)) = (((𝐿‘((numer‘𝑥) · (denom‘𝑦)))(+g‘𝑅)(𝐿‘((numer‘𝑦) · (denom‘𝑥)))) / (𝐿‘((denom‘𝑥) · (denom‘𝑦)))))
121	23, 28, 19, 85	rhmdvd 33885	. . . . . 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 1415	. . . . 5 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → ((𝐿‘(numer‘𝑥)) / (𝐿‘(denom‘𝑥))) = ((𝐿‘((numer‘𝑥) · (denom‘𝑦))) / (𝐿‘((denom‘𝑥) · (denom‘𝑦)))))
123	57, 59, 122	3eqtrd 2800	. . . 4 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → ((ℚHom‘𝑅)‘𝑥) = ((𝐿‘((numer‘𝑥) · (denom‘𝑦))) / (𝐿‘((denom‘𝑥) · (denom‘𝑦)))))
124	23, 28, 19, 85	rhmdvd 33885	. . . . . . 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 1415	. . . . . 6 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → ((𝐿‘(numer‘𝑦)) / (𝐿‘(denom‘𝑦))) = ((𝐿‘((numer‘𝑦) · (denom‘𝑥))) / (𝐿‘((denom‘𝑦) · (denom‘𝑥)))))
126	72, 74	mulcomd 11330	. . . . . . . 8 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → ((denom‘𝑥) · (denom‘𝑦)) = ((denom‘𝑦) · (denom‘𝑥)))
127	126	fveq2d 6889	. . . . . . 7 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (𝐿‘((denom‘𝑥) · (denom‘𝑦))) = (𝐿‘((denom‘𝑦) · (denom‘𝑥))))
128	127	oveq2d 7436	. . . . . 6 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → ((𝐿‘((numer‘𝑦) · (denom‘𝑥))) / (𝐿‘((denom‘𝑥) · (denom‘𝑦)))) = ((𝐿‘((numer‘𝑦) · (denom‘𝑥))) / (𝐿‘((denom‘𝑦) · (denom‘𝑥)))))
129	125, 65, 128	3eqtr4d 2806	. . . . 5 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → ((ℚHom‘𝑅)‘((numer‘𝑦) / (denom‘𝑦))) = ((𝐿‘((numer‘𝑦) · (denom‘𝑥))) / (𝐿‘((denom‘𝑥) · (denom‘𝑦)))))
130	63, 129	eqtrd 2796	. . . 4 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → ((ℚHom‘𝑅)‘𝑦) = ((𝐿‘((numer‘𝑦) · (denom‘𝑥))) / (𝐿‘((denom‘𝑥) · (denom‘𝑦)))))
131	123, 130	oveq12d 7438	. . 3 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (((ℚHom‘𝑅)‘𝑥)(+g‘𝑅)((ℚHom‘𝑅)‘𝑦)) = (((𝐿‘((numer‘𝑥) · (denom‘𝑦))) / (𝐿‘((denom‘𝑥) · (denom‘𝑦))))(+g‘𝑅)((𝐿‘((numer‘𝑦) · (denom‘𝑥))) / (𝐿‘((denom‘𝑥) · (denom‘𝑦))))))
132	106, 120, 131	3eqtr4d 2806	. 2 ⊢ (((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → ((ℚHom‘𝑅)‘(𝑥 + 𝑦)) = (((ℚHom‘𝑅)‘𝑥)(+g‘𝑅)((ℚHom‘𝑅)‘𝑦)))
133	2, 3, 4, 8, 9, 12, 17, 22, 92, 18, 95, 24, 97, 132	isrhmd 20722	1 ⊢ ((𝑅 ∈ Field ∧ (chr‘𝑅) = 0) → (ℚHom‘𝑅) ∈ (𝑄 RingHom 𝑅))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103   = wceq 1570   ∈ wcel 2145   ≠ wne 2956  Vcvv 3451  ⟶wf 6534  ‘cfv 6538  (class class class)co 7420  0cc0 11200  1c1 11201   + caddc 11203   · cmul 11205   / cdiv 11973  ℕcn 12335  ℤcz 12693  ℚcq 13075  numercnumer 16909  denomcdenom 16910  Basecbs 17387   ↾_s cress 17408  +_gcplusg 17428  ._rcmulr 17429  0_gc0g 17610   GrpHom cghm 19427  1_rcur 20407  Ringcrg 20459  CRingccrg 20460  Unitcui 20585  /_rcdvr 20630   RingHom crh 20699  DivRingcdr 20980  Fieldcfield 20981  ℂ_fldccnfld 21678  ℤ_ringczring 21752  ℤRHomczrh 21805  chrcchr 21807  ℚHomcqqh 34602

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-rep 5232  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7751  ax-cnex 11256  ax-resscn 11257  ax-1cn 11258  ax-icn 11259  ax-addcl 11260  ax-addrcl 11261  ax-mulcl 11262  ax-mulrcl 11263  ax-mulcom 11264  ax-addass 11265  ax-mulass 11266  ax-distr 11267  ax-i2m1 11268  ax-1ne0 11269  ax-1rid 11270  ax-rnegex 11271  ax-rrecex 11272  ax-cnre 11273  ax-pre-lttri 11274  ax-pre-lttrn 11275  ax-pre-ltadd 11276  ax-pre-mulgt0 11277  ax-pre-sup 11278  ax-addf 11279  ax-mulf 11280

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3063  df-ral 3078  df-rex 3088  df-rmo 3366  df-reu 3367  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-tp 4589  df-op 4591  df-uni 4868  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5546  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-pred 6304  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-riota 7377  df-ov 7423  df-oprab 7424  df-mpo 7425  df-om 7878  df-1st 8001  df-2nd 8002  df-tpos 8243  df-frecs 8299  df-wrecs 8330  df-recs 8379  df-rdg 8418  df-1o 8476  df-er 8717  df-map 8849  df-en 8974  df-dom 8975  df-sdom 8976  df-fin 8977  df-sup 9434  df-inf 9435  df-pnf 11345  df-mnf 11346  df-xr 11347  df-ltxr 11348  df-le 11349  df-sub 11543  df-neg 11544  df-div 11974  df-nn 12336  df-2 12405  df-3 12406  df-4 12407  df-5 12408  df-6 12409  df-7 12410  df-8 12411  df-9 12412  df-n0 12607  df-z 12694  df-dec 12815  df-uz 12966  df-q 13076  df-rp 13121  df-fz 13640  df-fl 13932  df-mod 14010  df-seq 14145  df-exp 14205  df-cj 15266  df-re 15267  df-im 15268  df-sqrt 15402  df-abs 15403  df-dvds 16423  df-gcd 16665  df-numer 16911  df-denom 16912  df-gz 17108  df-struct 17325  df-sets 17342  df-slot 17360  df-ndx 17372  df-base 17388  df-ress 17409  df-plusg 17441  df-mulr 17442  df-starv 17443  df-tset 17447  df-ple 17448  df-ds 17450  df-unif 17451  df-0g 17612  df-mgm 18816  df-sgrp 18908  df-mnd 18924  df-mhm 18978  df-grp 19147  df-minusg 19148  df-sbg 19149  df-mulg 19278  df-subg 19333  df-ghm 19428  df-od 19742  df-cmn 19996  df-abl 19997  df-mgp 20361  df-rng 20375  df-ur 20408  df-ring 20461  df-cring 20462  df-oppr 20567  df-dvdsr 20587  df-unit 20588  df-invr 20618  df-dvr 20631  df-rhm 20702  df-subrng 20798  df-subrg 20822  df-drng 20982  df-field 20983  df-cnfld 21679  df-zring 21753  df-zrh 21809  df-chr 21811  df-qqh 34603

This theorem is used by: (None)