dchrinvcl - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > dchrinvcl		Structured version Visualization version GIF version

Theorem dchrinvcl 27162

Description: Closure of the group inverse operation on Dirichlet characters. (Contributed by Mario Carneiro, 19-Apr-2016.)

**Hypotheses**
Ref	Expression
dchrmhm.g	⊢ 𝐺 = (DChr‘𝑁)
dchrmhm.z	⊢ 𝑍 = (ℤ/nℤ‘𝑁)
dchrmhm.b	⊢ 𝐷 = (Base‘𝐺)
dchrn0.b	⊢ 𝐵 = (Base‘𝑍)
dchrn0.u	⊢ 𝑈 = (Unit‘𝑍)
dchr1cl.o	⊢ 1 = (𝑘 ∈ 𝐵 ↦ if(𝑘 ∈ 𝑈, 1, 0))
dchrmullid.t	⊢ · = (+_g‘𝐺)
dchrmullid.x	⊢ (𝜑 → 𝑋 ∈ 𝐷)
dchrinvcl.n	⊢ 𝐾 = (𝑘 ∈ 𝐵 ↦ if(𝑘 ∈ 𝑈, (1 / (𝑋‘𝑘)), 0))

**Assertion**
Ref	Expression
dchrinvcl	⊢ (𝜑 → (𝐾 ∈ 𝐷 ∧ (𝐾 · 𝑋) = 1 ))

Distinct variable groups: 𝐵,𝑘 𝑈,𝑘 𝑘,𝑁 𝜑,𝑘 𝑘,𝑋 𝑘,𝑍 Allowed substitution hints: 𝐷(𝑘) · (𝑘) 1 (𝑘) 𝐺(𝑘) 𝐾(𝑘)

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

Step	Hyp	Ref	Expression
1		dchrinvcl.n	. . 3 ⊢ 𝐾 = (𝑘 ∈ 𝐵 ↦ if(𝑘 ∈ 𝑈, (1 / (𝑋‘𝑘)), 0))
2		dchrmhm.g	. . . 4 ⊢ 𝐺 = (DChr‘𝑁)
3		dchrmhm.z	. . . 4 ⊢ 𝑍 = (ℤ/nℤ‘𝑁)
4		dchrn0.b	. . . 4 ⊢ 𝐵 = (Base‘𝑍)
5		dchrn0.u	. . . 4 ⊢ 𝑈 = (Unit‘𝑍)
6		dchrmullid.x	. . . . 5 ⊢ (𝜑 → 𝑋 ∈ 𝐷)
7		dchrmhm.b	. . . . . 6 ⊢ 𝐷 = (Base‘𝐺)
8	2, 7	dchrrcl 27149	. . . . 5 ⊢ (𝑋 ∈ 𝐷 → 𝑁 ∈ ℕ)
9	6, 8	syl 17	. . . 4 ⊢ (𝜑 → 𝑁 ∈ ℕ)
10		fveq2 6822	. . . . 5 ⊢ (𝑘 = 𝑥 → (𝑋‘𝑘) = (𝑋‘𝑥))
11	10	oveq2d 7365	. . . 4 ⊢ (𝑘 = 𝑥 → (1 / (𝑋‘𝑘)) = (1 / (𝑋‘𝑥)))
12		fveq2 6822	. . . . 5 ⊢ (𝑘 = 𝑦 → (𝑋‘𝑘) = (𝑋‘𝑦))
13	12	oveq2d 7365	. . . 4 ⊢ (𝑘 = 𝑦 → (1 / (𝑋‘𝑘)) = (1 / (𝑋‘𝑦)))
14		fveq2 6822	. . . . 5 ⊢ (𝑘 = (𝑥(._r‘𝑍)𝑦) → (𝑋‘𝑘) = (𝑋‘(𝑥(._r‘𝑍)𝑦)))
15	14	oveq2d 7365	. . . 4 ⊢ (𝑘 = (𝑥(._r‘𝑍)𝑦) → (1 / (𝑋‘𝑘)) = (1 / (𝑋‘(𝑥(._r‘𝑍)𝑦))))
16		fveq2 6822	. . . . 5 ⊢ (𝑘 = (1_r‘𝑍) → (𝑋‘𝑘) = (𝑋‘(1_r‘𝑍)))
17	16	oveq2d 7365	. . . 4 ⊢ (𝑘 = (1_r‘𝑍) → (1 / (𝑋‘𝑘)) = (1 / (𝑋‘(1_r‘𝑍))))
18	2, 3, 7, 4, 6	dchrf 27151	. . . . . 6 ⊢ (𝜑 → 𝑋:𝐵⟶ℂ)
19	4, 5	unitss 20261	. . . . . . 7 ⊢ 𝑈 ⊆ 𝐵
20	19	sseli 3931	. . . . . 6 ⊢ (𝑘 ∈ 𝑈 → 𝑘 ∈ 𝐵)
21		ffvelcdm 7015	. . . . . 6 ⊢ ((𝑋:𝐵⟶ℂ ∧ 𝑘 ∈ 𝐵) → (𝑋‘𝑘) ∈ ℂ)
22	18, 20, 21	syl2an 596	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑈) → (𝑋‘𝑘) ∈ ℂ)
23		simpr 484	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑈) → 𝑘 ∈ 𝑈)
24	6	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑈) → 𝑋 ∈ 𝐷)
25	20	adantl 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑈) → 𝑘 ∈ 𝐵)
26	2, 3, 7, 4, 5, 24, 25	dchrn0 27159	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑈) → ((𝑋‘𝑘) ≠ 0 ↔ 𝑘 ∈ 𝑈))
27	23, 26	mpbird 257	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑈) → (𝑋‘𝑘) ≠ 0)
28	22, 27	reccld 11893	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑈) → (1 / (𝑋‘𝑘)) ∈ ℂ)
29		1t1e1 12285	. . . . . . . 8 ⊢ (1 · 1) = 1
30	29	eqcomi 2738	. . . . . . 7 ⊢ 1 = (1 · 1)
31	30	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → 1 = (1 · 1))
32	2, 3, 7	dchrmhm 27150	. . . . . . . 8 ⊢ 𝐷 ⊆ ((mulGrp‘𝑍) MndHom (mulGrp‘ℂ_fld))
33	6	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → 𝑋 ∈ 𝐷)
34	32, 33	sselid 3933	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → 𝑋 ∈ ((mulGrp‘𝑍) MndHom (mulGrp‘ℂ_fld)))
35		simprl 770	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → 𝑥 ∈ 𝑈)
36	19, 35	sselid 3933	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → 𝑥 ∈ 𝐵)
37		simprr 772	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → 𝑦 ∈ 𝑈)
38	19, 37	sselid 3933	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → 𝑦 ∈ 𝐵)
39		eqid 2729	. . . . . . . . 9 ⊢ (mulGrp‘𝑍) = (mulGrp‘𝑍)
40	39, 4	mgpbas 20030	. . . . . . . 8 ⊢ 𝐵 = (Base‘(mulGrp‘𝑍))
41		eqid 2729	. . . . . . . . 9 ⊢ (._r‘𝑍) = (._r‘𝑍)
42	39, 41	mgpplusg 20029	. . . . . . . 8 ⊢ (._r‘𝑍) = (+_g‘(mulGrp‘𝑍))
43		eqid 2729	. . . . . . . . 9 ⊢ (mulGrp‘ℂ_fld) = (mulGrp‘ℂ_fld)
44		cnfldmul 21269	. . . . . . . . 9 ⊢ · = (._r‘ℂ_fld)
45	43, 44	mgpplusg 20029	. . . . . . . 8 ⊢ · = (+_g‘(mulGrp‘ℂ_fld))
46	40, 42, 45	mhmlin 18667	. . . . . . 7 ⊢ ((𝑋 ∈ ((mulGrp‘𝑍) MndHom (mulGrp‘ℂ_fld)) ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑋‘(𝑥(._r‘𝑍)𝑦)) = ((𝑋‘𝑥) · (𝑋‘𝑦)))
47	34, 36, 38, 46	syl3anc 1373	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → (𝑋‘(𝑥(._r‘𝑍)𝑦)) = ((𝑋‘𝑥) · (𝑋‘𝑦)))
48	31, 47	oveq12d 7367	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → (1 / (𝑋‘(𝑥(._r‘𝑍)𝑦))) = ((1 · 1) / ((𝑋‘𝑥) · (𝑋‘𝑦))))
49		1cnd 11110	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → 1 ∈ ℂ)
50	18	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → 𝑋:𝐵⟶ℂ)
51	50, 36	ffvelcdmd 7019	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → (𝑋‘𝑥) ∈ ℂ)
52	50, 38	ffvelcdmd 7019	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → (𝑋‘𝑦) ∈ ℂ)
53	2, 3, 7, 4, 5, 33, 36	dchrn0 27159	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → ((𝑋‘𝑥) ≠ 0 ↔ 𝑥 ∈ 𝑈))
54	35, 53	mpbird 257	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → (𝑋‘𝑥) ≠ 0)
55	2, 3, 7, 4, 5, 33, 38	dchrn0 27159	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → ((𝑋‘𝑦) ≠ 0 ↔ 𝑦 ∈ 𝑈))
56	37, 55	mpbird 257	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → (𝑋‘𝑦) ≠ 0)
57	49, 51, 49, 52, 54, 56	divmuldivd 11941	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → ((1 / (𝑋‘𝑥)) · (1 / (𝑋‘𝑦))) = ((1 · 1) / ((𝑋‘𝑥) · (𝑋‘𝑦))))
58	48, 57	eqtr4d 2767	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → (1 / (𝑋‘(𝑥(._r‘𝑍)𝑦))) = ((1 / (𝑋‘𝑥)) · (1 / (𝑋‘𝑦))))
59	32, 6	sselid 3933	. . . . . . 7 ⊢ (𝜑 → 𝑋 ∈ ((mulGrp‘𝑍) MndHom (mulGrp‘ℂ_fld)))
60		eqid 2729	. . . . . . . . 9 ⊢ (1_r‘𝑍) = (1_r‘𝑍)
61	39, 60	ringidval 20068	. . . . . . . 8 ⊢ (1_r‘𝑍) = (0_g‘(mulGrp‘𝑍))
62		cnfld1 21300	. . . . . . . . 9 ⊢ 1 = (1_r‘ℂ_fld)
63	43, 62	ringidval 20068	. . . . . . . 8 ⊢ 1 = (0_g‘(mulGrp‘ℂ_fld))
64	61, 63	mhm0 18668	. . . . . . 7 ⊢ (𝑋 ∈ ((mulGrp‘𝑍) MndHom (mulGrp‘ℂ_fld)) → (𝑋‘(1_r‘𝑍)) = 1)
65	59, 64	syl 17	. . . . . 6 ⊢ (𝜑 → (𝑋‘(1_r‘𝑍)) = 1)
66	65	oveq2d 7365	. . . . 5 ⊢ (𝜑 → (1 / (𝑋‘(1_r‘𝑍))) = (1 / 1))
67		1div1e1 11815	. . . . 5 ⊢ (1 / 1) = 1
68	66, 67	eqtrdi 2780	. . . 4 ⊢ (𝜑 → (1 / (𝑋‘(1_r‘𝑍))) = 1)
69	2, 3, 4, 5, 9, 7, 11, 13, 15, 17, 28, 58, 68	dchrelbasd 27148	. . 3 ⊢ (𝜑 → (𝑘 ∈ 𝐵 ↦ if(𝑘 ∈ 𝑈, (1 / (𝑋‘𝑘)), 0)) ∈ 𝐷)
70	1, 69	eqeltrid 2832	. 2 ⊢ (𝜑 → 𝐾 ∈ 𝐷)
71		dchrmullid.t	. . . 4 ⊢ · = (+_g‘𝐺)
72	2, 3, 7, 71, 70, 6	dchrmul 27157	. . 3 ⊢ (𝜑 → (𝐾 · 𝑋) = (𝐾 ∘_f · 𝑋))
73	4	fvexi 6836	. . . . . 6 ⊢ 𝐵 ∈ V
74	73	a1i 11	. . . . 5 ⊢ (𝜑 → 𝐵 ∈ V)
75		ovex 7382	. . . . . . 7 ⊢ (1 / (𝑋‘𝑘)) ∈ V
76		c0ex 11109	. . . . . . 7 ⊢ 0 ∈ V
77	75, 76	ifex 4527	. . . . . 6 ⊢ if(𝑘 ∈ 𝑈, (1 / (𝑋‘𝑘)), 0) ∈ V
78	77	a1i 11	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → if(𝑘 ∈ 𝑈, (1 / (𝑋‘𝑘)), 0) ∈ V)
79	18	ffvelcdmda 7018	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → (𝑋‘𝑘) ∈ ℂ)
80	1	a1i 11	. . . . 5 ⊢ (𝜑 → 𝐾 = (𝑘 ∈ 𝐵 ↦ if(𝑘 ∈ 𝑈, (1 / (𝑋‘𝑘)), 0)))
81	18	feqmptd 6891	. . . . 5 ⊢ (𝜑 → 𝑋 = (𝑘 ∈ 𝐵 ↦ (𝑋‘𝑘)))
82	74, 78, 79, 80, 81	offval2 7633	. . . 4 ⊢ (𝜑 → (𝐾 ∘_f · 𝑋) = (𝑘 ∈ 𝐵 ↦ (if(𝑘 ∈ 𝑈, (1 / (𝑋‘𝑘)), 0) · (𝑋‘𝑘))))
83		dchr1cl.o	. . . . 5 ⊢ 1 = (𝑘 ∈ 𝐵 ↦ if(𝑘 ∈ 𝑈, 1, 0))
84		ovif 7447	. . . . . . 7 ⊢ (if(𝑘 ∈ 𝑈, (1 / (𝑋‘𝑘)), 0) · (𝑋‘𝑘)) = if(𝑘 ∈ 𝑈, ((1 / (𝑋‘𝑘)) · (𝑋‘𝑘)), (0 · (𝑋‘𝑘)))
85	79	adantr 480	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵) ∧ 𝑘 ∈ 𝑈) → (𝑋‘𝑘) ∈ ℂ)
86	6	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → 𝑋 ∈ 𝐷)
87		simpr 484	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → 𝑘 ∈ 𝐵)
88	2, 3, 7, 4, 5, 86, 87	dchrn0 27159	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → ((𝑋‘𝑘) ≠ 0 ↔ 𝑘 ∈ 𝑈))
89	88	biimpar 477	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵) ∧ 𝑘 ∈ 𝑈) → (𝑋‘𝑘) ≠ 0)
90	85, 89	recid2d 11896	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵) ∧ 𝑘 ∈ 𝑈) → ((1 / (𝑋‘𝑘)) · (𝑋‘𝑘)) = 1)
91	90	ifeq1da 4508	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → if(𝑘 ∈ 𝑈, ((1 / (𝑋‘𝑘)) · (𝑋‘𝑘)), (0 · (𝑋‘𝑘))) = if(𝑘 ∈ 𝑈, 1, (0 · (𝑋‘𝑘))))
92	79	mul02d 11314	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → (0 · (𝑋‘𝑘)) = 0)
93	92	ifeq2d 4497	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → if(𝑘 ∈ 𝑈, 1, (0 · (𝑋‘𝑘))) = if(𝑘 ∈ 𝑈, 1, 0))
94	91, 93	eqtrd 2764	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → if(𝑘 ∈ 𝑈, ((1 / (𝑋‘𝑘)) · (𝑋‘𝑘)), (0 · (𝑋‘𝑘))) = if(𝑘 ∈ 𝑈, 1, 0))
95	84, 94	eqtrid 2776	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → (if(𝑘 ∈ 𝑈, (1 / (𝑋‘𝑘)), 0) · (𝑋‘𝑘)) = if(𝑘 ∈ 𝑈, 1, 0))
96	95	mpteq2dva 5185	. . . . 5 ⊢ (𝜑 → (𝑘 ∈ 𝐵 ↦ (if(𝑘 ∈ 𝑈, (1 / (𝑋‘𝑘)), 0) · (𝑋‘𝑘))) = (𝑘 ∈ 𝐵 ↦ if(𝑘 ∈ 𝑈, 1, 0)))
97	83, 96	eqtr4id 2783	. . . 4 ⊢ (𝜑 → 1 = (𝑘 ∈ 𝐵 ↦ (if(𝑘 ∈ 𝑈, (1 / (𝑋‘𝑘)), 0) · (𝑋‘𝑘))))
98	82, 97	eqtr4d 2767	. . 3 ⊢ (𝜑 → (𝐾 ∘_f · 𝑋) = 1 )
99	72, 98	eqtrd 2764	. 2 ⊢ (𝜑 → (𝐾 · 𝑋) = 1 )
100	70, 99	jca 511	1 ⊢ (𝜑 → (𝐾 ∈ 𝐷 ∧ (𝐾 · 𝑋) = 1 ))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 = wceq 1540 ∈ wcel 2109 ≠ wne 2925 Vcvv 3436 ifcif 4476 ↦ cmpt 5173 ⟶wf 6478 ‘cfv 6482 (class class class)co 7349 ∘_f cof 7611 ℂcc 11007 0cc0 11009 1c1 11010 · cmul 11014 / cdiv 11777 ℕcn 12128 Basecbs 17120 +_gcplusg 17161 ._rcmulr 17162 MndHom cmhm 18655 mulGrpcmgp 20025 1_rcur 20066 Unitcui 20240 ℂ_fldccnfld 21261 ℤ/nℤczn 21409 DChrcdchr 27141

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-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-int 4897 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-of 7613 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-ec 8627 df-qs 8631 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-fz 13411 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-sca 17177 df-vsca 17178 df-ip 17179 df-tset 17180 df-ple 17181 df-ds 17183 df-unif 17184 df-0g 17345 df-imas 17412 df-qus 17413 df-mgm 18514 df-sgrp 18593 df-mnd 18609 df-mhm 18657 df-grp 18815 df-minusg 18816 df-sbg 18817 df-subg 19002 df-nsg 19003 df-eqg 19004 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-subrng 20431 df-subrg 20455 df-lmod 20765 df-lss 20835 df-lsp 20875 df-sra 21077 df-rgmod 21078 df-lidl 21115 df-rsp 21116 df-2idl 21157 df-cnfld 21262 df-zring 21354 df-zn 21413 df-dchr 27142

This theorem is referenced by: dchrabl 27163

W3C validator