![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > dchrptlem3 | Structured version Visualization version GIF version |
Description: Lemma for dchrpt 25535. (Contributed by Mario Carneiro, 28-Apr-2016.) |
Ref | Expression |
---|---|
dchrpt.g | ⊢ 𝐺 = (DChr‘𝑁) |
dchrpt.z | ⊢ 𝑍 = (ℤ/nℤ‘𝑁) |
dchrpt.d | ⊢ 𝐷 = (Base‘𝐺) |
dchrpt.b | ⊢ 𝐵 = (Base‘𝑍) |
dchrpt.1 | ⊢ 1 = (1r‘𝑍) |
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 𝑆) = 𝑈) |
Ref | Expression |
---|---|
dchrptlem3 | ⊢ (𝜑 → ∃𝑥 ∈ 𝐷 (𝑥‘𝐴) ≠ 1) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dchrpt.n1 | . . . . 5 ⊢ (𝜑 → 𝐴 ≠ 1 ) | |
2 | dchrpt.n | . . . . . . . . . . . 12 ⊢ (𝜑 → 𝑁 ∈ ℕ) | |
3 | 2 | nnnn0d 11760 | . . . . . . . . . . 11 ⊢ (𝜑 → 𝑁 ∈ ℕ0) |
4 | dchrpt.z | . . . . . . . . . . . 12 ⊢ 𝑍 = (ℤ/nℤ‘𝑁) | |
5 | 4 | zncrng 20383 | . . . . . . . . . . 11 ⊢ (𝑁 ∈ ℕ0 → 𝑍 ∈ CRing) |
6 | 3, 5 | syl 17 | . . . . . . . . . 10 ⊢ (𝜑 → 𝑍 ∈ CRing) |
7 | crngring 19021 | . . . . . . . . . 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 19130 | . . . . . . . . 9 ⊢ (𝑍 ∈ Ring → 𝐻 ∈ Grp) |
12 | 8, 11 | syl 17 | . . . . . . . 8 ⊢ (𝜑 → 𝐻 ∈ Grp) |
13 | grpmnd 17888 | . . . . . . . 8 ⊢ (𝐻 ∈ Grp → 𝐻 ∈ Mnd) | |
14 | 12, 13 | syl 17 | . . . . . . 7 ⊢ (𝜑 → 𝐻 ∈ Mnd) |
15 | dchrpt.w | . . . . . . . 8 ⊢ (𝜑 → 𝑊 ∈ Word 𝑈) | |
16 | 15 | dmexd 7424 | . . . . . . 7 ⊢ (𝜑 → dom 𝑊 ∈ V) |
17 | eqid 2772 | . . . . . . . 8 ⊢ (0g‘𝐻) = (0g‘𝐻) | |
18 | 17 | gsumz 17832 | . . . . . . 7 ⊢ ((𝐻 ∈ Mnd ∧ dom 𝑊 ∈ V) → (𝐻 Σg (𝑎 ∈ dom 𝑊 ↦ (0g‘𝐻))) = (0g‘𝐻)) |
19 | 14, 16, 18 | syl2anc 576 | . . . . . 6 ⊢ (𝜑 → (𝐻 Σg (𝑎 ∈ dom 𝑊 ↦ (0g‘𝐻))) = (0g‘𝐻)) |
20 | dchrpt.1 | . . . . . . . . . 10 ⊢ 1 = (1r‘𝑍) | |
21 | 9, 10, 20 | unitgrpid 19132 | . . . . . . . . 9 ⊢ (𝑍 ∈ Ring → 1 = (0g‘𝐻)) |
22 | 8, 21 | syl 17 | . . . . . . . 8 ⊢ (𝜑 → 1 = (0g‘𝐻)) |
23 | 22 | mpteq2dv 5017 | . . . . . . 7 ⊢ (𝜑 → (𝑎 ∈ dom 𝑊 ↦ 1 ) = (𝑎 ∈ dom 𝑊 ↦ (0g‘𝐻))) |
24 | 23 | oveq2d 6986 | . . . . . 6 ⊢ (𝜑 → (𝐻 Σg (𝑎 ∈ dom 𝑊 ↦ 1 )) = (𝐻 Σg (𝑎 ∈ dom 𝑊 ↦ (0g‘𝐻)))) |
25 | 19, 24, 22 | 3eqtr4d 2818 | . . . . 5 ⊢ (𝜑 → (𝐻 Σg (𝑎 ∈ dom 𝑊 ↦ 1 )) = 1 ) |
26 | 1, 25 | neeqtrrd 3035 | . . . 4 ⊢ (𝜑 → 𝐴 ≠ (𝐻 Σg (𝑎 ∈ dom 𝑊 ↦ 1 ))) |
27 | dchrpt.2 | . . . . . 6 ⊢ (𝜑 → 𝐻dom DProd 𝑆) | |
28 | zex 11795 | . . . . . . . . . 10 ⊢ ℤ ∈ V | |
29 | 28 | mptex 6806 | . . . . . . . . 9 ⊢ (𝑛 ∈ ℤ ↦ (𝑛 · (𝑊‘𝑘))) ∈ V |
30 | 29 | rnex 7426 | . . . . . . . 8 ⊢ ran (𝑛 ∈ ℤ ↦ (𝑛 · (𝑊‘𝑘))) ∈ V |
31 | dchrpt.s | . . . . . . . 8 ⊢ 𝑆 = (𝑘 ∈ dom 𝑊 ↦ ran (𝑛 ∈ ℤ ↦ (𝑛 · (𝑊‘𝑘)))) | |
32 | 30, 31 | dmmpti 6316 | . . . . . . 7 ⊢ dom 𝑆 = dom 𝑊 |
33 | 32 | a1i 11 | . . . . . 6 ⊢ (𝜑 → dom 𝑆 = dom 𝑊) |
34 | eqid 2772 | . . . . . 6 ⊢ (𝐻dProj𝑆) = (𝐻dProj𝑆) | |
35 | dchrpt.au | . . . . . . 7 ⊢ (𝜑 → 𝐴 ∈ 𝑈) | |
36 | dchrpt.3 | . . . . . . 7 ⊢ (𝜑 → (𝐻 DProd 𝑆) = 𝑈) | |
37 | 35, 36 | eleqtrrd 2863 | . . . . . 6 ⊢ (𝜑 → 𝐴 ∈ (𝐻 DProd 𝑆)) |
38 | eqid 2772 | . . . . . 6 ⊢ {ℎ ∈ X𝑖 ∈ dom 𝑊(𝑆‘𝑖) ∣ ℎ finSupp (0g‘𝐻)} = {ℎ ∈ X𝑖 ∈ dom 𝑊(𝑆‘𝑖) ∣ ℎ finSupp (0g‘𝐻)} | |
39 | 22 | adantr 473 | . . . . . . . 8 ⊢ ((𝜑 ∧ 𝑎 ∈ dom 𝑊) → 1 = (0g‘𝐻)) |
40 | 27, 33 | dprdf2 18869 | . . . . . . . . . 10 ⊢ (𝜑 → 𝑆:dom 𝑊⟶(SubGrp‘𝐻)) |
41 | 40 | ffvelrnda 6670 | . . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑎 ∈ dom 𝑊) → (𝑆‘𝑎) ∈ (SubGrp‘𝐻)) |
42 | 17 | subg0cl 18061 | . . . . . . . . 9 ⊢ ((𝑆‘𝑎) ∈ (SubGrp‘𝐻) → (0g‘𝐻) ∈ (𝑆‘𝑎)) |
43 | 41, 42 | syl 17 | . . . . . . . 8 ⊢ ((𝜑 ∧ 𝑎 ∈ dom 𝑊) → (0g‘𝐻) ∈ (𝑆‘𝑎)) |
44 | 39, 43 | eqeltrd 2860 | . . . . . . 7 ⊢ ((𝜑 ∧ 𝑎 ∈ dom 𝑊) → 1 ∈ (𝑆‘𝑎)) |
45 | 20 | fvexi 6507 | . . . . . . . . . 10 ⊢ 1 ∈ V |
46 | 45 | a1i 11 | . . . . . . . . 9 ⊢ (𝜑 → 1 ∈ V) |
47 | 16, 46 | fczfsuppd 8638 | . . . . . . . 8 ⊢ (𝜑 → (dom 𝑊 × { 1 }) finSupp 1 ) |
48 | fconstmpt 5457 | . . . . . . . . . 10 ⊢ (dom 𝑊 × { 1 }) = (𝑎 ∈ dom 𝑊 ↦ 1 ) | |
49 | 48 | eqcomi 2781 | . . . . . . . . 9 ⊢ (𝑎 ∈ dom 𝑊 ↦ 1 ) = (dom 𝑊 × { 1 }) |
50 | 49 | a1i 11 | . . . . . . . 8 ⊢ (𝜑 → (𝑎 ∈ dom 𝑊 ↦ 1 ) = (dom 𝑊 × { 1 })) |
51 | 22 | eqcomd 2778 | . . . . . . . 8 ⊢ (𝜑 → (0g‘𝐻) = 1 ) |
52 | 47, 50, 51 | 3brtr4d 4955 | . . . . . . 7 ⊢ (𝜑 → (𝑎 ∈ dom 𝑊 ↦ 1 ) finSupp (0g‘𝐻)) |
53 | 38, 27, 33, 44, 52 | dprdwd 18873 | . . . . . 6 ⊢ (𝜑 → (𝑎 ∈ dom 𝑊 ↦ 1 ) ∈ {ℎ ∈ X𝑖 ∈ dom 𝑊(𝑆‘𝑖) ∣ ℎ finSupp (0g‘𝐻)}) |
54 | 27, 33, 34, 37, 17, 38, 53 | dpjeq 18921 | . . . . 5 ⊢ (𝜑 → (𝐴 = (𝐻 Σg (𝑎 ∈ dom 𝑊 ↦ 1 )) ↔ ∀𝑎 ∈ dom 𝑊(((𝐻dProj𝑆)‘𝑎)‘𝐴) = 1 )) |
55 | 54 | necon3abid 2997 | . . . 4 ⊢ (𝜑 → (𝐴 ≠ (𝐻 Σg (𝑎 ∈ dom 𝑊 ↦ 1 )) ↔ ¬ ∀𝑎 ∈ dom 𝑊(((𝐻dProj𝑆)‘𝑎)‘𝐴) = 1 )) |
56 | 26, 55 | mpbid 224 | . . 3 ⊢ (𝜑 → ¬ ∀𝑎 ∈ dom 𝑊(((𝐻dProj𝑆)‘𝑎)‘𝐴) = 1 ) |
57 | rexnal 3179 | . . 3 ⊢ (∃𝑎 ∈ dom 𝑊 ¬ (((𝐻dProj𝑆)‘𝑎)‘𝐴) = 1 ↔ ¬ ∀𝑎 ∈ dom 𝑊(((𝐻dProj𝑆)‘𝑎)‘𝐴) = 1 ) | |
58 | 56, 57 | sylibr 226 | . 2 ⊢ (𝜑 → ∃𝑎 ∈ dom 𝑊 ¬ (((𝐻dProj𝑆)‘𝑎)‘𝐴) = 1 ) |
59 | df-ne 2962 | . . . 4 ⊢ ((((𝐻dProj𝑆)‘𝑎)‘𝐴) ≠ 1 ↔ ¬ (((𝐻dProj𝑆)‘𝑎)‘𝐴) = 1 ) | |
60 | dchrpt.g | . . . . . 6 ⊢ 𝐺 = (DChr‘𝑁) | |
61 | dchrpt.d | . . . . . 6 ⊢ 𝐷 = (Base‘𝐺) | |
62 | dchrpt.b | . . . . . 6 ⊢ 𝐵 = (Base‘𝑍) | |
63 | 2 | adantr 473 | . . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ dom 𝑊 ∧ (((𝐻dProj𝑆)‘𝑎)‘𝐴) ≠ 1 )) → 𝑁 ∈ ℕ) |
64 | 1 | adantr 473 | . . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ dom 𝑊 ∧ (((𝐻dProj𝑆)‘𝑎)‘𝐴) ≠ 1 )) → 𝐴 ≠ 1 ) |
65 | dchrpt.m | . . . . . 6 ⊢ · = (.g‘𝐻) | |
66 | 35 | adantr 473 | . . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ dom 𝑊 ∧ (((𝐻dProj𝑆)‘𝑎)‘𝐴) ≠ 1 )) → 𝐴 ∈ 𝑈) |
67 | 15 | adantr 473 | . . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ dom 𝑊 ∧ (((𝐻dProj𝑆)‘𝑎)‘𝐴) ≠ 1 )) → 𝑊 ∈ Word 𝑈) |
68 | 27 | adantr 473 | . . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ dom 𝑊 ∧ (((𝐻dProj𝑆)‘𝑎)‘𝐴) ≠ 1 )) → 𝐻dom DProd 𝑆) |
69 | 36 | adantr 473 | . . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ dom 𝑊 ∧ (((𝐻dProj𝑆)‘𝑎)‘𝐴) ≠ 1 )) → (𝐻 DProd 𝑆) = 𝑈) |
70 | eqid 2772 | . . . . . 6 ⊢ (od‘𝐻) = (od‘𝐻) | |
71 | eqid 2772 | . . . . . 6 ⊢ (-1↑𝑐(2 / ((od‘𝐻)‘(𝑊‘𝑎)))) = (-1↑𝑐(2 / ((od‘𝐻)‘(𝑊‘𝑎)))) | |
72 | simprl 758 | . . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ dom 𝑊 ∧ (((𝐻dProj𝑆)‘𝑎)‘𝐴) ≠ 1 )) → 𝑎 ∈ dom 𝑊) | |
73 | simprr 760 | . . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ dom 𝑊 ∧ (((𝐻dProj𝑆)‘𝑎)‘𝐴) ≠ 1 )) → (((𝐻dProj𝑆)‘𝑎)‘𝐴) ≠ 1 ) | |
74 | eqid 2772 | . . . . . 6 ⊢ (𝑢 ∈ 𝑈 ↦ (℩ℎ∃𝑚 ∈ ℤ ((((𝐻dProj𝑆)‘𝑎)‘𝑢) = (𝑚 · (𝑊‘𝑎)) ∧ ℎ = ((-1↑𝑐(2 / ((od‘𝐻)‘(𝑊‘𝑎))))↑𝑚)))) = (𝑢 ∈ 𝑈 ↦ (℩ℎ∃𝑚 ∈ ℤ ((((𝐻dProj𝑆)‘𝑎)‘𝑢) = (𝑚 · (𝑊‘𝑎)) ∧ ℎ = ((-1↑𝑐(2 / ((od‘𝐻)‘(𝑊‘𝑎))))↑𝑚)))) | |
75 | 60, 4, 61, 62, 20, 63, 64, 9, 10, 65, 31, 66, 67, 68, 69, 34, 70, 71, 72, 73, 74 | dchrptlem2 25533 | . . . . 5 ⊢ ((𝜑 ∧ (𝑎 ∈ dom 𝑊 ∧ (((𝐻dProj𝑆)‘𝑎)‘𝐴) ≠ 1 )) → ∃𝑥 ∈ 𝐷 (𝑥‘𝐴) ≠ 1) |
76 | 75 | expr 449 | . . . 4 ⊢ ((𝜑 ∧ 𝑎 ∈ dom 𝑊) → ((((𝐻dProj𝑆)‘𝑎)‘𝐴) ≠ 1 → ∃𝑥 ∈ 𝐷 (𝑥‘𝐴) ≠ 1)) |
77 | 59, 76 | syl5bir 235 | . . 3 ⊢ ((𝜑 ∧ 𝑎 ∈ dom 𝑊) → (¬ (((𝐻dProj𝑆)‘𝑎)‘𝐴) = 1 → ∃𝑥 ∈ 𝐷 (𝑥‘𝐴) ≠ 1)) |
78 | 77 | rexlimdva 3223 | . 2 ⊢ (𝜑 → (∃𝑎 ∈ dom 𝑊 ¬ (((𝐻dProj𝑆)‘𝑎)‘𝐴) = 1 → ∃𝑥 ∈ 𝐷 (𝑥‘𝐴) ≠ 1)) |
79 | 58, 78 | mpd 15 | 1 ⊢ (𝜑 → ∃𝑥 ∈ 𝐷 (𝑥‘𝐴) ≠ 1) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 387 = wceq 1507 ∈ wcel 2048 ≠ wne 2961 ∀wral 3082 ∃wrex 3083 {crab 3086 Vcvv 3409 {csn 4435 class class class wbr 4923 ↦ cmpt 5002 × cxp 5398 dom cdm 5400 ran crn 5401 ℩cio 6144 ‘cfv 6182 (class class class)co 6970 Xcixp 8251 finSupp cfsupp 8620 1c1 10328 -cneg 10663 / cdiv 11090 ℕcn 11431 2c2 11488 ℕ0cn0 11700 ℤcz 11786 ↑cexp 13237 Word cword 13662 Basecbs 16329 ↾s cress 16330 0gc0g 16559 Σg cgsu 16560 Mndcmnd 17752 Grpcgrp 17881 .gcmg 18001 SubGrpcsubg 18047 odcod 18404 DProd cdprd 18855 dProjcdpj 18856 mulGrpcmgp 18952 1rcur 18964 Ringcrg 19010 CRingccrg 19011 Unitcui 19102 ℤ/nℤczn 20342 ↑𝑐ccxp 24830 DChrcdchr 25500 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1964 ax-8 2050 ax-9 2057 ax-10 2077 ax-11 2091 ax-12 2104 ax-13 2299 ax-ext 2745 ax-rep 5043 ax-sep 5054 ax-nul 5061 ax-pow 5113 ax-pr 5180 ax-un 7273 ax-inf2 8890 ax-cnex 10383 ax-resscn 10384 ax-1cn 10385 ax-icn 10386 ax-addcl 10387 ax-addrcl 10388 ax-mulcl 10389 ax-mulrcl 10390 ax-mulcom 10391 ax-addass 10392 ax-mulass 10393 ax-distr 10394 ax-i2m1 10395 ax-1ne0 10396 ax-1rid 10397 ax-rnegex 10398 ax-rrecex 10399 ax-cnre 10400 ax-pre-lttri 10401 ax-pre-lttrn 10402 ax-pre-ltadd 10403 ax-pre-mulgt0 10404 ax-pre-sup 10405 ax-addf 10406 ax-mulf 10407 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-3or 1069 df-3an 1070 df-tru 1510 df-fal 1520 df-ex 1743 df-nf 1747 df-sb 2014 df-mo 2544 df-eu 2580 df-clab 2754 df-cleq 2765 df-clel 2840 df-nfc 2912 df-ne 2962 df-nel 3068 df-ral 3087 df-rex 3088 df-reu 3089 df-rmo 3090 df-rab 3091 df-v 3411 df-sbc 3678 df-csb 3783 df-dif 3828 df-un 3830 df-in 3832 df-ss 3839 df-pss 3841 df-nul 4174 df-if 4345 df-pw 4418 df-sn 4436 df-pr 4438 df-tp 4440 df-op 4442 df-uni 4707 df-int 4744 df-iun 4788 df-iin 4789 df-br 4924 df-opab 4986 df-mpt 5003 df-tr 5025 df-id 5305 df-eprel 5310 df-po 5319 df-so 5320 df-fr 5359 df-se 5360 df-we 5361 df-xp 5406 df-rel 5407 df-cnv 5408 df-co 5409 df-dm 5410 df-rn 5411 df-res 5412 df-ima 5413 df-pred 5980 df-ord 6026 df-on 6027 df-lim 6028 df-suc 6029 df-iota 6146 df-fun 6184 df-fn 6185 df-f 6186 df-f1 6187 df-fo 6188 df-f1o 6189 df-fv 6190 df-isom 6191 df-riota 6931 df-ov 6973 df-oprab 6974 df-mpo 6975 df-of 7221 df-om 7391 df-1st 7494 df-2nd 7495 df-supp 7627 df-tpos 7688 df-wrecs 7743 df-recs 7805 df-rdg 7843 df-1o 7897 df-2o 7898 df-oadd 7901 df-omul 7902 df-er 8081 df-ec 8083 df-qs 8087 df-map 8200 df-pm 8201 df-ixp 8252 df-en 8299 df-dom 8300 df-sdom 8301 df-fin 8302 df-fsupp 8621 df-fi 8662 df-sup 8693 df-inf 8694 df-oi 8761 df-card 9154 df-acn 9157 df-cda 9380 df-pnf 10468 df-mnf 10469 df-xr 10470 df-ltxr 10471 df-le 10472 df-sub 10664 df-neg 10665 df-div 11091 df-nn 11432 df-2 11496 df-3 11497 df-4 11498 df-5 11499 df-6 11500 df-7 11501 df-8 11502 df-9 11503 df-n0 11701 df-z 11787 df-dec 11905 df-uz 12052 df-q 12156 df-rp 12198 df-xneg 12317 df-xadd 12318 df-xmul 12319 df-ioo 12551 df-ioc 12552 df-ico 12553 df-icc 12554 df-fz 12702 df-fzo 12843 df-fl 12970 df-mod 13046 df-seq 13178 df-exp 13238 df-fac 13442 df-bc 13471 df-hash 13499 df-word 13663 df-shft 14277 df-cj 14309 df-re 14310 df-im 14311 df-sqrt 14445 df-abs 14446 df-limsup 14679 df-clim 14696 df-rlim 14697 df-sum 14894 df-ef 15271 df-sin 15273 df-cos 15274 df-pi 15276 df-dvds 15458 df-struct 16331 df-ndx 16332 df-slot 16333 df-base 16335 df-sets 16336 df-ress 16337 df-plusg 16424 df-mulr 16425 df-starv 16426 df-sca 16427 df-vsca 16428 df-ip 16429 df-tset 16430 df-ple 16431 df-ds 16433 df-unif 16434 df-hom 16435 df-cco 16436 df-rest 16542 df-topn 16543 df-0g 16561 df-gsum 16562 df-topgen 16563 df-pt 16564 df-prds 16567 df-xrs 16621 df-qtop 16626 df-imas 16627 df-qus 16628 df-xps 16629 df-mre 16705 df-mrc 16706 df-acs 16708 df-mgm 17700 df-sgrp 17742 df-mnd 17753 df-mhm 17793 df-submnd 17794 df-grp 17884 df-minusg 17885 df-sbg 17886 df-mulg 18002 df-subg 18050 df-nsg 18051 df-eqg 18052 df-ghm 18117 df-gim 18160 df-cntz 18208 df-oppg 18235 df-od 18408 df-lsm 18512 df-pj1 18513 df-cmn 18658 df-abl 18659 df-dprd 18857 df-dpj 18858 df-mgp 18953 df-ur 18965 df-ring 19012 df-cring 19013 df-oppr 19086 df-dvdsr 19104 df-unit 19105 df-rnghom 19180 df-subrg 19246 df-lmod 19348 df-lss 19416 df-lsp 19456 df-sra 19656 df-rgmod 19657 df-lidl 19658 df-rsp 19659 df-2idl 19716 df-psmet 20229 df-xmet 20230 df-met 20231 df-bl 20232 df-mopn 20233 df-fbas 20234 df-fg 20235 df-cnfld 20238 df-zring 20310 df-zrh 20343 df-zn 20346 df-top 21196 df-topon 21213 df-topsp 21235 df-bases 21248 df-cld 21321 df-ntr 21322 df-cls 21323 df-nei 21400 df-lp 21438 df-perf 21439 df-cn 21529 df-cnp 21530 df-haus 21617 df-tx 21864 df-hmeo 22057 df-fil 22148 df-fm 22240 df-flim 22241 df-flf 22242 df-xms 22623 df-ms 22624 df-tms 22625 df-cncf 23179 df-limc 24157 df-dv 24158 df-log 24831 df-cxp 24832 df-dchr 25501 |
This theorem is referenced by: dchrpt 25535 |
Copyright terms: Public domain | W3C validator |