dchrptlem3 - Metamath Proof Explorer

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

Theorem dchrptlem3 24891

Description: Lemma for dchrpt 24892. (Contributed by Mario Carneiro, 28-Apr-2016.)

**Hypotheses**
Ref	Expression
dchrpt.g	⊢ 𝐺 = (DChr‘𝑁)
dchrpt.z	⊢ 𝑍 = (ℤ/nℤ‘𝑁)
dchrpt.d	⊢ 𝐷 = (Base‘𝐺)
dchrpt.b	⊢ 𝐵 = (Base‘𝑍)
dchrpt.1	⊢ 1 = (1_r‘𝑍)
dchrpt.n	⊢ (𝜑 → 𝑁 ∈ ℕ)
dchrpt.n1	⊢ (𝜑 → 𝐴 ≠ 1 )
dchrpt.u	⊢ 𝑈 = (Unit‘𝑍)
dchrpt.h	⊢ 𝐻 = ((mulGrp‘𝑍) ↾_s 𝑈)
dchrpt.m	⊢ · = (._g‘𝐻)
dchrpt.s	⊢ 𝑆 = (𝑘 ∈ dom 𝑊 ↦ ran (𝑛 ∈ ℤ ↦ (𝑛 · (𝑊‘𝑘))))
dchrpt.au	⊢ (𝜑 → 𝐴 ∈ 𝑈)
dchrpt.w	⊢ (𝜑 → 𝑊 ∈ Word 𝑈)
dchrpt.2	⊢ (𝜑 → 𝐻dom DProd 𝑆)
dchrpt.3	⊢ (𝜑 → (𝐻 DProd 𝑆) = 𝑈)

**Assertion**
Ref	Expression
dchrptlem3	⊢ (𝜑 → ∃𝑥 ∈ 𝐷 (𝑥‘𝐴) ≠ 1)

Distinct variable groups: 𝑘,𝑛,𝑥, 1 𝐴,𝑘,𝑛,𝑥 𝑥,𝐵 𝑥,𝐺 𝑘,𝐻,𝑛,𝑥 𝑥,𝑁 𝑘,𝑊,𝑛,𝑥 · ,𝑘,𝑛,𝑥 𝑆,𝑘,𝑛,𝑥 𝑘,𝑍,𝑛,𝑥 𝑥,𝐷 𝜑,𝑘,𝑛,𝑥 𝑥,𝑈 Allowed substitution hints: 𝐵(𝑘,𝑛) 𝐷(𝑘,𝑛) 𝑈(𝑘,𝑛) 𝐺(𝑘,𝑛) 𝑁(𝑘,𝑛)

Proof of Theorem dchrptlem3 Dummy variables 𝑎 ℎ 𝑚 𝑢 𝑖 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		dchrpt.n1	. . . . 5 ⊢ (𝜑 → 𝐴 ≠ 1 )
2		dchrpt.n	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑁 ∈ ℕ)
3	2	nnnn0d 11295	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑁 ∈ ℕ₀)
4		dchrpt.z	. . . . . . . . . . . 12 ⊢ 𝑍 = (ℤ/nℤ‘𝑁)
5	4	zncrng 19812	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℕ₀ → 𝑍 ∈ CRing)
6	3, 5	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝑍 ∈ CRing)
7		crngring 18479	. . . . . . . . . 10 ⊢ (𝑍 ∈ CRing → 𝑍 ∈ Ring)
8	6, 7	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝑍 ∈ Ring)
9		dchrpt.u	. . . . . . . . . 10 ⊢ 𝑈 = (Unit‘𝑍)
10		dchrpt.h	. . . . . . . . . 10 ⊢ 𝐻 = ((mulGrp‘𝑍) ↾_s 𝑈)
11	9, 10	unitgrp 18588	. . . . . . . . 9 ⊢ (𝑍 ∈ Ring → 𝐻 ∈ Grp)
12	8, 11	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝐻 ∈ Grp)
13		grpmnd 17350	. . . . . . . 8 ⊢ (𝐻 ∈ Grp → 𝐻 ∈ Mnd)
14	12, 13	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝐻 ∈ Mnd)
15		dchrpt.w	. . . . . . . 8 ⊢ (𝜑 → 𝑊 ∈ Word 𝑈)
16		dmexg 7044	. . . . . . . 8 ⊢ (𝑊 ∈ Word 𝑈 → dom 𝑊 ∈ V)
17	15, 16	syl 17	. . . . . . 7 ⊢ (𝜑 → dom 𝑊 ∈ V)
18		eqid 2621	. . . . . . . 8 ⊢ (0_g‘𝐻) = (0_g‘𝐻)
19	18	gsumz 17295	. . . . . . 7 ⊢ ((𝐻 ∈ Mnd ∧ dom 𝑊 ∈ V) → (𝐻 Σ_g (𝑎 ∈ dom 𝑊 ↦ (0_g‘𝐻))) = (0_g‘𝐻))
20	14, 17, 19	syl2anc 692	. . . . . 6 ⊢ (𝜑 → (𝐻 Σ_g (𝑎 ∈ dom 𝑊 ↦ (0_g‘𝐻))) = (0_g‘𝐻))
21		dchrpt.1	. . . . . . . . . 10 ⊢ 1 = (1_r‘𝑍)
22	9, 10, 21	unitgrpid 18590	. . . . . . . . 9 ⊢ (𝑍 ∈ Ring → 1 = (0_g‘𝐻))
23	8, 22	syl 17	. . . . . . . 8 ⊢ (𝜑 → 1 = (0_g‘𝐻))
24	23	mpteq2dv 4705	. . . . . . 7 ⊢ (𝜑 → (𝑎 ∈ dom 𝑊 ↦ 1 ) = (𝑎 ∈ dom 𝑊 ↦ (0_g‘𝐻)))
25	24	oveq2d 6620	. . . . . 6 ⊢ (𝜑 → (𝐻 Σ_g (𝑎 ∈ dom 𝑊 ↦ 1 )) = (𝐻 Σ_g (𝑎 ∈ dom 𝑊 ↦ (0_g‘𝐻))))
26	20, 25, 23	3eqtr4d 2665	. . . . 5 ⊢ (𝜑 → (𝐻 Σ_g (𝑎 ∈ dom 𝑊 ↦ 1 )) = 1 )
27	1, 26	neeqtrrd 2864	. . . 4 ⊢ (𝜑 → 𝐴 ≠ (𝐻 Σ_g (𝑎 ∈ dom 𝑊 ↦ 1 )))
28		dchrpt.2	. . . . . 6 ⊢ (𝜑 → 𝐻dom DProd 𝑆)
29		zex 11330	. . . . . . . . . 10 ⊢ ℤ ∈ V
30	29	mptex 6440	. . . . . . . . 9 ⊢ (𝑛 ∈ ℤ ↦ (𝑛 · (𝑊‘𝑘))) ∈ V
31	30	rnex 7047	. . . . . . . 8 ⊢ ran (𝑛 ∈ ℤ ↦ (𝑛 · (𝑊‘𝑘))) ∈ V
32		dchrpt.s	. . . . . . . 8 ⊢ 𝑆 = (𝑘 ∈ dom 𝑊 ↦ ran (𝑛 ∈ ℤ ↦ (𝑛 · (𝑊‘𝑘))))
33	31, 32	dmmpti 5980	. . . . . . 7 ⊢ dom 𝑆 = dom 𝑊
34	33	a1i 11	. . . . . 6 ⊢ (𝜑 → dom 𝑆 = dom 𝑊)
35		eqid 2621	. . . . . 6 ⊢ (𝐻dProj𝑆) = (𝐻dProj𝑆)
36		dchrpt.au	. . . . . . 7 ⊢ (𝜑 → 𝐴 ∈ 𝑈)
37		dchrpt.3	. . . . . . 7 ⊢ (𝜑 → (𝐻 DProd 𝑆) = 𝑈)
38	36, 37	eleqtrrd 2701	. . . . . 6 ⊢ (𝜑 → 𝐴 ∈ (𝐻 DProd 𝑆))
39		eqid 2621	. . . . . 6 ⊢ {ℎ ∈ X𝑖 ∈ dom 𝑊(𝑆‘𝑖) ∣ ℎ finSupp (0_g‘𝐻)} = {ℎ ∈ X𝑖 ∈ dom 𝑊(𝑆‘𝑖) ∣ ℎ finSupp (0_g‘𝐻)}
40	23	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑎 ∈ dom 𝑊) → 1 = (0_g‘𝐻))
41	28, 34	dprdf2 18327	. . . . . . . . . 10 ⊢ (𝜑 → 𝑆:dom 𝑊⟶(SubGrp‘𝐻))
42	41	ffvelrnda 6315	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑎 ∈ dom 𝑊) → (𝑆‘𝑎) ∈ (SubGrp‘𝐻))
43	18	subg0cl 17523	. . . . . . . . 9 ⊢ ((𝑆‘𝑎) ∈ (SubGrp‘𝐻) → (0_g‘𝐻) ∈ (𝑆‘𝑎))
44	42, 43	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑎 ∈ dom 𝑊) → (0_g‘𝐻) ∈ (𝑆‘𝑎))
45	40, 44	eqeltrd 2698	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑎 ∈ dom 𝑊) → 1 ∈ (𝑆‘𝑎))
46		fvex 6158	. . . . . . . . . . 11 ⊢ (1_r‘𝑍) ∈ V
47	21, 46	eqeltri 2694	. . . . . . . . . 10 ⊢ 1 ∈ V
48	47	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → 1 ∈ V)
49	17, 48	fczfsuppd 8237	. . . . . . . 8 ⊢ (𝜑 → (dom 𝑊 × { 1 }) finSupp 1 )
50		fconstmpt 5123	. . . . . . . . . 10 ⊢ (dom 𝑊 × { 1 }) = (𝑎 ∈ dom 𝑊 ↦ 1 )
51	50	eqcomi 2630	. . . . . . . . 9 ⊢ (𝑎 ∈ dom 𝑊 ↦ 1 ) = (dom 𝑊 × { 1 })
52	51	a1i 11	. . . . . . . 8 ⊢ (𝜑 → (𝑎 ∈ dom 𝑊 ↦ 1 ) = (dom 𝑊 × { 1 }))
53	23	eqcomd 2627	. . . . . . . 8 ⊢ (𝜑 → (0_g‘𝐻) = 1 )
54	49, 52, 53	3brtr4d 4645	. . . . . . 7 ⊢ (𝜑 → (𝑎 ∈ dom 𝑊 ↦ 1 ) finSupp (0_g‘𝐻))
55	39, 28, 34, 45, 54	dprdwd 18331	. . . . . 6 ⊢ (𝜑 → (𝑎 ∈ dom 𝑊 ↦ 1 ) ∈ {ℎ ∈ X𝑖 ∈ dom 𝑊(𝑆‘𝑖) ∣ ℎ finSupp (0_g‘𝐻)})
56	28, 34, 35, 38, 18, 39, 55	dpjeq 18379	. . . . 5 ⊢ (𝜑 → (𝐴 = (𝐻 Σ_g (𝑎 ∈ dom 𝑊 ↦ 1 )) ↔ ∀𝑎 ∈ dom 𝑊(((𝐻dProj𝑆)‘𝑎)‘𝐴) = 1 ))
57	56	necon3abid 2826	. . . 4 ⊢ (𝜑 → (𝐴 ≠ (𝐻 Σ_g (𝑎 ∈ dom 𝑊 ↦ 1 )) ↔ ¬ ∀𝑎 ∈ dom 𝑊(((𝐻dProj𝑆)‘𝑎)‘𝐴) = 1 ))
58	27, 57	mpbid 222	. . 3 ⊢ (𝜑 → ¬ ∀𝑎 ∈ dom 𝑊(((𝐻dProj𝑆)‘𝑎)‘𝐴) = 1 )
59		rexnal 2989	. . 3 ⊢ (∃𝑎 ∈ dom 𝑊 ¬ (((𝐻dProj𝑆)‘𝑎)‘𝐴) = 1 ↔ ¬ ∀𝑎 ∈ dom 𝑊(((𝐻dProj𝑆)‘𝑎)‘𝐴) = 1 )
60	58, 59	sylibr 224	. 2 ⊢ (𝜑 → ∃𝑎 ∈ dom 𝑊 ¬ (((𝐻dProj𝑆)‘𝑎)‘𝐴) = 1 )
61		df-ne 2791	. . . 4 ⊢ ((((𝐻dProj𝑆)‘𝑎)‘𝐴) ≠ 1 ↔ ¬ (((𝐻dProj𝑆)‘𝑎)‘𝐴) = 1 )
62		dchrpt.g	. . . . . 6 ⊢ 𝐺 = (DChr‘𝑁)
63		dchrpt.d	. . . . . 6 ⊢ 𝐷 = (Base‘𝐺)
64		dchrpt.b	. . . . . 6 ⊢ 𝐵 = (Base‘𝑍)
65	2	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ dom 𝑊 ∧ (((𝐻dProj𝑆)‘𝑎)‘𝐴) ≠ 1 )) → 𝑁 ∈ ℕ)
66	1	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ dom 𝑊 ∧ (((𝐻dProj𝑆)‘𝑎)‘𝐴) ≠ 1 )) → 𝐴 ≠ 1 )
67		dchrpt.m	. . . . . 6 ⊢ · = (._g‘𝐻)
68	36	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ dom 𝑊 ∧ (((𝐻dProj𝑆)‘𝑎)‘𝐴) ≠ 1 )) → 𝐴 ∈ 𝑈)
69	15	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ dom 𝑊 ∧ (((𝐻dProj𝑆)‘𝑎)‘𝐴) ≠ 1 )) → 𝑊 ∈ Word 𝑈)
70	28	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ dom 𝑊 ∧ (((𝐻dProj𝑆)‘𝑎)‘𝐴) ≠ 1 )) → 𝐻dom DProd 𝑆)
71	37	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ dom 𝑊 ∧ (((𝐻dProj𝑆)‘𝑎)‘𝐴) ≠ 1 )) → (𝐻 DProd 𝑆) = 𝑈)
72		eqid 2621	. . . . . 6 ⊢ (od‘𝐻) = (od‘𝐻)
73		eqid 2621	. . . . . 6 ⊢ (-1↑_𝑐(2 / ((od‘𝐻)‘(𝑊‘𝑎)))) = (-1↑_𝑐(2 / ((od‘𝐻)‘(𝑊‘𝑎))))
74		simprl 793	. . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ dom 𝑊 ∧ (((𝐻dProj𝑆)‘𝑎)‘𝐴) ≠ 1 )) → 𝑎 ∈ dom 𝑊)
75		simprr 795	. . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ dom 𝑊 ∧ (((𝐻dProj𝑆)‘𝑎)‘𝐴) ≠ 1 )) → (((𝐻dProj𝑆)‘𝑎)‘𝐴) ≠ 1 )
76		eqid 2621	. . . . . 6 ⊢ (𝑢 ∈ 𝑈 ↦ (℩ℎ∃𝑚 ∈ ℤ ((((𝐻dProj𝑆)‘𝑎)‘𝑢) = (𝑚 · (𝑊‘𝑎)) ∧ ℎ = ((-1↑_𝑐(2 / ((od‘𝐻)‘(𝑊‘𝑎))))↑𝑚)))) = (𝑢 ∈ 𝑈 ↦ (℩ℎ∃𝑚 ∈ ℤ ((((𝐻dProj𝑆)‘𝑎)‘𝑢) = (𝑚 · (𝑊‘𝑎)) ∧ ℎ = ((-1↑_𝑐(2 / ((od‘𝐻)‘(𝑊‘𝑎))))↑𝑚))))
77	62, 4, 63, 64, 21, 65, 66, 9, 10, 67, 32, 68, 69, 70, 71, 35, 72, 73, 74, 75, 76	dchrptlem2 24890	. . . . 5 ⊢ ((𝜑 ∧ (𝑎 ∈ dom 𝑊 ∧ (((𝐻dProj𝑆)‘𝑎)‘𝐴) ≠ 1 )) → ∃𝑥 ∈ 𝐷 (𝑥‘𝐴) ≠ 1)
78	77	expr 642	. . . 4 ⊢ ((𝜑 ∧ 𝑎 ∈ dom 𝑊) → ((((𝐻dProj𝑆)‘𝑎)‘𝐴) ≠ 1 → ∃𝑥 ∈ 𝐷 (𝑥‘𝐴) ≠ 1))
79	61, 78	syl5bir 233	. . 3 ⊢ ((𝜑 ∧ 𝑎 ∈ dom 𝑊) → (¬ (((𝐻dProj𝑆)‘𝑎)‘𝐴) = 1 → ∃𝑥 ∈ 𝐷 (𝑥‘𝐴) ≠ 1))
80	79	rexlimdva 3024	. 2 ⊢ (𝜑 → (∃𝑎 ∈ dom 𝑊 ¬ (((𝐻dProj𝑆)‘𝑎)‘𝐴) = 1 → ∃𝑥 ∈ 𝐷 (𝑥‘𝐴) ≠ 1))
81	60, 80	mpd 15	1 ⊢ (𝜑 → ∃𝑥 ∈ 𝐷 (𝑥‘𝐴) ≠ 1)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 384 = wceq 1480 ∈ wcel 1987 ≠ wne 2790 ∀wral 2907 ∃wrex 2908 {crab 2911 Vcvv 3186 {csn 4148 class class class wbr 4613 ↦ cmpt 4673 × cxp 5072 dom cdm 5074 ran crn 5075 ℩cio 5808 ‘cfv 5847 (class class class)co 6604 Xcixp 7852 finSupp cfsupp 8219 1c1 9881 -cneg 10211 / cdiv 10628 ℕcn 10964 2c2 11014 ℕ₀cn0 11236 ℤcz 11321 ↑cexp 12800 Word cword 13230 Basecbs 15781 ↾_s cress 15782 0_gc0g 16021 Σ_g cgsu 16022 Mndcmnd 17215 Grpcgrp 17343 ._gcmg 17461 SubGrpcsubg 17509 odcod 17865 DProd cdprd 18313 dProjcdpj 18314 mulGrpcmgp 18410 1_rcur 18422 Ringcrg 18468 CRingccrg 18469 Unitcui 18560 ℤ/nℤczn 19770 ↑_𝑐ccxp 24206 DChrcdchr 24857

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1719 ax-4 1734 ax-5 1836 ax-6 1885 ax-7 1932 ax-8 1989 ax-9 1996 ax-10 2016 ax-11 2031 ax-12 2044 ax-13 2245 ax-ext 2601 ax-rep 4731 ax-sep 4741 ax-nul 4749 ax-pow 4803 ax-pr 4867 ax-un 6902 ax-inf2 8482 ax-cnex 9936 ax-resscn 9937 ax-1cn 9938 ax-icn 9939 ax-addcl 9940 ax-addrcl 9941 ax-mulcl 9942 ax-mulrcl 9943 ax-mulcom 9944 ax-addass 9945 ax-mulass 9946 ax-distr 9947 ax-i2m1 9948 ax-1ne0 9949 ax-1rid 9950 ax-rnegex 9951 ax-rrecex 9952 ax-cnre 9953 ax-pre-lttri 9954 ax-pre-lttrn 9955 ax-pre-ltadd 9956 ax-pre-mulgt0 9957 ax-pre-sup 9958 ax-addf 9959 ax-mulf 9960

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1037 df-3an 1038 df-tru 1483 df-fal 1486 df-ex 1702 df-nf 1707 df-sb 1878 df-eu 2473 df-mo 2474 df-clab 2608 df-cleq 2614 df-clel 2617 df-nfc 2750 df-ne 2791 df-nel 2894 df-ral 2912 df-rex 2913 df-reu 2914 df-rmo 2915 df-rab 2916 df-v 3188 df-sbc 3418 df-csb 3515 df-dif 3558 df-un 3560 df-in 3562 df-ss 3569 df-pss 3571 df-nul 3892 df-if 4059 df-pw 4132 df-sn 4149 df-pr 4151 df-tp 4153 df-op 4155 df-uni 4403 df-int 4441 df-iun 4487 df-iin 4488 df-br 4614 df-opab 4674 df-mpt 4675 df-tr 4713 df-eprel 4985 df-id 4989 df-po 4995 df-so 4996 df-fr 5033 df-se 5034 df-we 5035 df-xp 5080 df-rel 5081 df-cnv 5082 df-co 5083 df-dm 5084 df-rn 5085 df-res 5086 df-ima 5087 df-pred 5639 df-ord 5685 df-on 5686 df-lim 5687 df-suc 5688 df-iota 5810 df-fun 5849 df-fn 5850 df-f 5851 df-f1 5852 df-fo 5853 df-f1o 5854 df-fv 5855 df-isom 5856 df-riota 6565 df-ov 6607 df-oprab 6608 df-mpt2 6609 df-of 6850 df-om 7013 df-1st 7113 df-2nd 7114 df-supp 7241 df-tpos 7297 df-wrecs 7352 df-recs 7413 df-rdg 7451 df-1o 7505 df-2o 7506 df-oadd 7509 df-omul 7510 df-er 7687 df-ec 7689 df-qs 7693 df-map 7804 df-pm 7805 df-ixp 7853 df-en 7900 df-dom 7901 df-sdom 7902 df-fin 7903 df-fsupp 8220 df-fi 8261 df-sup 8292 df-inf 8293 df-oi 8359 df-card 8709 df-acn 8712 df-cda 8934 df-pnf 10020 df-mnf 10021 df-xr 10022 df-ltxr 10023 df-le 10024 df-sub 10212 df-neg 10213 df-div 10629 df-nn 10965 df-2 11023 df-3 11024 df-4 11025 df-5 11026 df-6 11027 df-7 11028 df-8 11029 df-9 11030 df-n0 11237 df-z 11322 df-dec 11438 df-uz 11632 df-q 11733 df-rp 11777 df-xneg 11890 df-xadd 11891 df-xmul 11892 df-ioo 12121 df-ioc 12122 df-ico 12123 df-icc 12124 df-fz 12269 df-fzo 12407 df-fl 12533 df-mod 12609 df-seq 12742 df-exp 12801 df-fac 13001 df-bc 13030 df-hash 13058 df-word 13238 df-shft 13741 df-cj 13773 df-re 13774 df-im 13775 df-sqrt 13909 df-abs 13910 df-limsup 14136 df-clim 14153 df-rlim 14154 df-sum 14351 df-ef 14723 df-sin 14725 df-cos 14726 df-pi 14728 df-dvds 14908 df-struct 15783 df-ndx 15784 df-slot 15785 df-base 15786 df-sets 15787 df-ress 15788 df-plusg 15875 df-mulr 15876 df-starv 15877 df-sca 15878 df-vsca 15879 df-ip 15880 df-tset 15881 df-ple 15882 df-ds 15885 df-unif 15886 df-hom 15887 df-cco 15888 df-rest 16004 df-topn 16005 df-0g 16023 df-gsum 16024 df-topgen 16025 df-pt 16026 df-prds 16029 df-xrs 16083 df-qtop 16088 df-imas 16089 df-qus 16090 df-xps 16091 df-mre 16167 df-mrc 16168 df-acs 16170 df-mgm 17163 df-sgrp 17205 df-mnd 17216 df-mhm 17256 df-submnd 17257 df-grp 17346 df-minusg 17347 df-sbg 17348 df-mulg 17462 df-subg 17512 df-nsg 17513 df-eqg 17514 df-ghm 17579 df-gim 17622 df-cntz 17671 df-oppg 17697 df-od 17869 df-lsm 17972 df-pj1 17973 df-cmn 18116 df-abl 18117 df-dprd 18315 df-dpj 18316 df-mgp 18411 df-ur 18423 df-ring 18470 df-cring 18471 df-oppr 18544 df-dvdsr 18562 df-unit 18563 df-rnghom 18636 df-subrg 18699 df-lmod 18786 df-lss 18852 df-lsp 18891 df-sra 19091 df-rgmod 19092 df-lidl 19093 df-rsp 19094 df-2idl 19151 df-psmet 19657 df-xmet 19658 df-met 19659 df-bl 19660 df-mopn 19661 df-fbas 19662 df-fg 19663 df-cnfld 19666 df-zring 19738 df-zrh 19771 df-zn 19774 df-top 20621 df-bases 20622 df-topon 20623 df-topsp 20624 df-cld 20733 df-ntr 20734 df-cls 20735 df-nei 20812 df-lp 20850 df-perf 20851 df-cn 20941 df-cnp 20942 df-haus 21029 df-tx 21275 df-hmeo 21468 df-fil 21560 df-fm 21652 df-flim 21653 df-flf 21654 df-xms 22035 df-ms 22036 df-tms 22037 df-cncf 22589 df-limc 23536 df-dv 23537 df-log 24207 df-cxp 24208 df-dchr 24858

This theorem is referenced by: dchrpt 24892

W3C validator