Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > dchrptlem3 | Structured version Visualization version GIF version |
Description: Lemma for dchrpt 26120. (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 12133 | . . . . . . . . . . 11 ⊢ (𝜑 → 𝑁 ∈ ℕ0) |
4 | dchrpt.z | . . . . . . . . . . . 12 ⊢ 𝑍 = (ℤ/nℤ‘𝑁) | |
5 | 4 | zncrng 20481 | . . . . . . . . . . 11 ⊢ (𝑁 ∈ ℕ0 → 𝑍 ∈ CRing) |
6 | 3, 5 | syl 17 | . . . . . . . . . 10 ⊢ (𝜑 → 𝑍 ∈ CRing) |
7 | crngring 19546 | . . . . . . . . . 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 19657 | . . . . . . . . 9 ⊢ (𝑍 ∈ Ring → 𝐻 ∈ Grp) |
12 | 8, 11 | syl 17 | . . . . . . . 8 ⊢ (𝜑 → 𝐻 ∈ Grp) |
13 | 12 | grpmndd 18349 | . . . . . . 7 ⊢ (𝜑 → 𝐻 ∈ Mnd) |
14 | dchrpt.w | . . . . . . . 8 ⊢ (𝜑 → 𝑊 ∈ Word 𝑈) | |
15 | 14 | dmexd 7672 | . . . . . . 7 ⊢ (𝜑 → dom 𝑊 ∈ V) |
16 | eqid 2734 | . . . . . . . 8 ⊢ (0g‘𝐻) = (0g‘𝐻) | |
17 | 16 | gsumz 18234 | . . . . . . 7 ⊢ ((𝐻 ∈ Mnd ∧ dom 𝑊 ∈ V) → (𝐻 Σg (𝑎 ∈ dom 𝑊 ↦ (0g‘𝐻))) = (0g‘𝐻)) |
18 | 13, 15, 17 | syl2anc 587 | . . . . . 6 ⊢ (𝜑 → (𝐻 Σg (𝑎 ∈ dom 𝑊 ↦ (0g‘𝐻))) = (0g‘𝐻)) |
19 | dchrpt.1 | . . . . . . . . . 10 ⊢ 1 = (1r‘𝑍) | |
20 | 9, 10, 19 | unitgrpid 19659 | . . . . . . . . 9 ⊢ (𝑍 ∈ Ring → 1 = (0g‘𝐻)) |
21 | 8, 20 | syl 17 | . . . . . . . 8 ⊢ (𝜑 → 1 = (0g‘𝐻)) |
22 | 21 | mpteq2dv 5140 | . . . . . . 7 ⊢ (𝜑 → (𝑎 ∈ dom 𝑊 ↦ 1 ) = (𝑎 ∈ dom 𝑊 ↦ (0g‘𝐻))) |
23 | 22 | oveq2d 7218 | . . . . . 6 ⊢ (𝜑 → (𝐻 Σg (𝑎 ∈ dom 𝑊 ↦ 1 )) = (𝐻 Σg (𝑎 ∈ dom 𝑊 ↦ (0g‘𝐻)))) |
24 | 18, 23, 21 | 3eqtr4d 2784 | . . . . 5 ⊢ (𝜑 → (𝐻 Σg (𝑎 ∈ dom 𝑊 ↦ 1 )) = 1 ) |
25 | 1, 24 | neeqtrrd 3009 | . . . 4 ⊢ (𝜑 → 𝐴 ≠ (𝐻 Σg (𝑎 ∈ dom 𝑊 ↦ 1 ))) |
26 | dchrpt.2 | . . . . . 6 ⊢ (𝜑 → 𝐻dom DProd 𝑆) | |
27 | zex 12168 | . . . . . . . . . 10 ⊢ ℤ ∈ V | |
28 | 27 | mptex 7028 | . . . . . . . . 9 ⊢ (𝑛 ∈ ℤ ↦ (𝑛 · (𝑊‘𝑘))) ∈ V |
29 | 28 | rnex 7679 | . . . . . . . 8 ⊢ ran (𝑛 ∈ ℤ ↦ (𝑛 · (𝑊‘𝑘))) ∈ V |
30 | dchrpt.s | . . . . . . . 8 ⊢ 𝑆 = (𝑘 ∈ dom 𝑊 ↦ ran (𝑛 ∈ ℤ ↦ (𝑛 · (𝑊‘𝑘)))) | |
31 | 29, 30 | dmmpti 6511 | . . . . . . 7 ⊢ dom 𝑆 = dom 𝑊 |
32 | 31 | a1i 11 | . . . . . 6 ⊢ (𝜑 → dom 𝑆 = dom 𝑊) |
33 | eqid 2734 | . . . . . 6 ⊢ (𝐻dProj𝑆) = (𝐻dProj𝑆) | |
34 | dchrpt.au | . . . . . . 7 ⊢ (𝜑 → 𝐴 ∈ 𝑈) | |
35 | dchrpt.3 | . . . . . . 7 ⊢ (𝜑 → (𝐻 DProd 𝑆) = 𝑈) | |
36 | 34, 35 | eleqtrrd 2837 | . . . . . 6 ⊢ (𝜑 → 𝐴 ∈ (𝐻 DProd 𝑆)) |
37 | eqid 2734 | . . . . . 6 ⊢ {ℎ ∈ X𝑖 ∈ dom 𝑊(𝑆‘𝑖) ∣ ℎ finSupp (0g‘𝐻)} = {ℎ ∈ X𝑖 ∈ dom 𝑊(𝑆‘𝑖) ∣ ℎ finSupp (0g‘𝐻)} | |
38 | 21 | adantr 484 | . . . . . . . 8 ⊢ ((𝜑 ∧ 𝑎 ∈ dom 𝑊) → 1 = (0g‘𝐻)) |
39 | 26, 32 | dprdf2 19366 | . . . . . . . . . 10 ⊢ (𝜑 → 𝑆:dom 𝑊⟶(SubGrp‘𝐻)) |
40 | 39 | ffvelrnda 6893 | . . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑎 ∈ dom 𝑊) → (𝑆‘𝑎) ∈ (SubGrp‘𝐻)) |
41 | 16 | subg0cl 18523 | . . . . . . . . 9 ⊢ ((𝑆‘𝑎) ∈ (SubGrp‘𝐻) → (0g‘𝐻) ∈ (𝑆‘𝑎)) |
42 | 40, 41 | syl 17 | . . . . . . . 8 ⊢ ((𝜑 ∧ 𝑎 ∈ dom 𝑊) → (0g‘𝐻) ∈ (𝑆‘𝑎)) |
43 | 38, 42 | eqeltrd 2834 | . . . . . . 7 ⊢ ((𝜑 ∧ 𝑎 ∈ dom 𝑊) → 1 ∈ (𝑆‘𝑎)) |
44 | 19 | fvexi 6720 | . . . . . . . . . 10 ⊢ 1 ∈ V |
45 | 44 | a1i 11 | . . . . . . . . 9 ⊢ (𝜑 → 1 ∈ V) |
46 | 15, 45 | fczfsuppd 8992 | . . . . . . . 8 ⊢ (𝜑 → (dom 𝑊 × { 1 }) finSupp 1 ) |
47 | fconstmpt 5600 | . . . . . . . . . 10 ⊢ (dom 𝑊 × { 1 }) = (𝑎 ∈ dom 𝑊 ↦ 1 ) | |
48 | 47 | eqcomi 2743 | . . . . . . . . 9 ⊢ (𝑎 ∈ dom 𝑊 ↦ 1 ) = (dom 𝑊 × { 1 }) |
49 | 48 | a1i 11 | . . . . . . . 8 ⊢ (𝜑 → (𝑎 ∈ dom 𝑊 ↦ 1 ) = (dom 𝑊 × { 1 })) |
50 | 21 | eqcomd 2740 | . . . . . . . 8 ⊢ (𝜑 → (0g‘𝐻) = 1 ) |
51 | 46, 49, 50 | 3brtr4d 5075 | . . . . . . 7 ⊢ (𝜑 → (𝑎 ∈ dom 𝑊 ↦ 1 ) finSupp (0g‘𝐻)) |
52 | 37, 26, 32, 43, 51 | dprdwd 19370 | . . . . . 6 ⊢ (𝜑 → (𝑎 ∈ dom 𝑊 ↦ 1 ) ∈ {ℎ ∈ X𝑖 ∈ dom 𝑊(𝑆‘𝑖) ∣ ℎ finSupp (0g‘𝐻)}) |
53 | 26, 32, 33, 36, 16, 37, 52 | dpjeq 19418 | . . . . 5 ⊢ (𝜑 → (𝐴 = (𝐻 Σg (𝑎 ∈ dom 𝑊 ↦ 1 )) ↔ ∀𝑎 ∈ dom 𝑊(((𝐻dProj𝑆)‘𝑎)‘𝐴) = 1 )) |
54 | 53 | necon3abid 2971 | . . . 4 ⊢ (𝜑 → (𝐴 ≠ (𝐻 Σg (𝑎 ∈ dom 𝑊 ↦ 1 )) ↔ ¬ ∀𝑎 ∈ dom 𝑊(((𝐻dProj𝑆)‘𝑎)‘𝐴) = 1 )) |
55 | 25, 54 | mpbid 235 | . . 3 ⊢ (𝜑 → ¬ ∀𝑎 ∈ dom 𝑊(((𝐻dProj𝑆)‘𝑎)‘𝐴) = 1 ) |
56 | rexnal 3153 | . . 3 ⊢ (∃𝑎 ∈ dom 𝑊 ¬ (((𝐻dProj𝑆)‘𝑎)‘𝐴) = 1 ↔ ¬ ∀𝑎 ∈ dom 𝑊(((𝐻dProj𝑆)‘𝑎)‘𝐴) = 1 ) | |
57 | 55, 56 | sylibr 237 | . 2 ⊢ (𝜑 → ∃𝑎 ∈ dom 𝑊 ¬ (((𝐻dProj𝑆)‘𝑎)‘𝐴) = 1 ) |
58 | df-ne 2936 | . . . 4 ⊢ ((((𝐻dProj𝑆)‘𝑎)‘𝐴) ≠ 1 ↔ ¬ (((𝐻dProj𝑆)‘𝑎)‘𝐴) = 1 ) | |
59 | dchrpt.g | . . . . . 6 ⊢ 𝐺 = (DChr‘𝑁) | |
60 | dchrpt.d | . . . . . 6 ⊢ 𝐷 = (Base‘𝐺) | |
61 | dchrpt.b | . . . . . 6 ⊢ 𝐵 = (Base‘𝑍) | |
62 | 2 | adantr 484 | . . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ dom 𝑊 ∧ (((𝐻dProj𝑆)‘𝑎)‘𝐴) ≠ 1 )) → 𝑁 ∈ ℕ) |
63 | 1 | adantr 484 | . . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ dom 𝑊 ∧ (((𝐻dProj𝑆)‘𝑎)‘𝐴) ≠ 1 )) → 𝐴 ≠ 1 ) |
64 | dchrpt.m | . . . . . 6 ⊢ · = (.g‘𝐻) | |
65 | 34 | adantr 484 | . . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ dom 𝑊 ∧ (((𝐻dProj𝑆)‘𝑎)‘𝐴) ≠ 1 )) → 𝐴 ∈ 𝑈) |
66 | 14 | adantr 484 | . . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ dom 𝑊 ∧ (((𝐻dProj𝑆)‘𝑎)‘𝐴) ≠ 1 )) → 𝑊 ∈ Word 𝑈) |
67 | 26 | adantr 484 | . . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ dom 𝑊 ∧ (((𝐻dProj𝑆)‘𝑎)‘𝐴) ≠ 1 )) → 𝐻dom DProd 𝑆) |
68 | 35 | adantr 484 | . . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ dom 𝑊 ∧ (((𝐻dProj𝑆)‘𝑎)‘𝐴) ≠ 1 )) → (𝐻 DProd 𝑆) = 𝑈) |
69 | eqid 2734 | . . . . . 6 ⊢ (od‘𝐻) = (od‘𝐻) | |
70 | eqid 2734 | . . . . . 6 ⊢ (-1↑𝑐(2 / ((od‘𝐻)‘(𝑊‘𝑎)))) = (-1↑𝑐(2 / ((od‘𝐻)‘(𝑊‘𝑎)))) | |
71 | simprl 771 | . . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ dom 𝑊 ∧ (((𝐻dProj𝑆)‘𝑎)‘𝐴) ≠ 1 )) → 𝑎 ∈ dom 𝑊) | |
72 | simprr 773 | . . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ dom 𝑊 ∧ (((𝐻dProj𝑆)‘𝑎)‘𝐴) ≠ 1 )) → (((𝐻dProj𝑆)‘𝑎)‘𝐴) ≠ 1 ) | |
73 | eqid 2734 | . . . . . 6 ⊢ (𝑢 ∈ 𝑈 ↦ (℩ℎ∃𝑚 ∈ ℤ ((((𝐻dProj𝑆)‘𝑎)‘𝑢) = (𝑚 · (𝑊‘𝑎)) ∧ ℎ = ((-1↑𝑐(2 / ((od‘𝐻)‘(𝑊‘𝑎))))↑𝑚)))) = (𝑢 ∈ 𝑈 ↦ (℩ℎ∃𝑚 ∈ ℤ ((((𝐻dProj𝑆)‘𝑎)‘𝑢) = (𝑚 · (𝑊‘𝑎)) ∧ ℎ = ((-1↑𝑐(2 / ((od‘𝐻)‘(𝑊‘𝑎))))↑𝑚)))) | |
74 | 59, 4, 60, 61, 19, 62, 63, 9, 10, 64, 30, 65, 66, 67, 68, 33, 69, 70, 71, 72, 73 | dchrptlem2 26118 | . . . . 5 ⊢ ((𝜑 ∧ (𝑎 ∈ dom 𝑊 ∧ (((𝐻dProj𝑆)‘𝑎)‘𝐴) ≠ 1 )) → ∃𝑥 ∈ 𝐷 (𝑥‘𝐴) ≠ 1) |
75 | 74 | expr 460 | . . . 4 ⊢ ((𝜑 ∧ 𝑎 ∈ dom 𝑊) → ((((𝐻dProj𝑆)‘𝑎)‘𝐴) ≠ 1 → ∃𝑥 ∈ 𝐷 (𝑥‘𝐴) ≠ 1)) |
76 | 58, 75 | syl5bir 246 | . . 3 ⊢ ((𝜑 ∧ 𝑎 ∈ dom 𝑊) → (¬ (((𝐻dProj𝑆)‘𝑎)‘𝐴) = 1 → ∃𝑥 ∈ 𝐷 (𝑥‘𝐴) ≠ 1)) |
77 | 76 | rexlimdva 3196 | . 2 ⊢ (𝜑 → (∃𝑎 ∈ dom 𝑊 ¬ (((𝐻dProj𝑆)‘𝑎)‘𝐴) = 1 → ∃𝑥 ∈ 𝐷 (𝑥‘𝐴) ≠ 1)) |
78 | 57, 77 | mpd 15 | 1 ⊢ (𝜑 → ∃𝑥 ∈ 𝐷 (𝑥‘𝐴) ≠ 1) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 399 = wceq 1543 ∈ wcel 2110 ≠ wne 2935 ∀wral 3054 ∃wrex 3055 {crab 3058 Vcvv 3401 {csn 4531 class class class wbr 5043 ↦ cmpt 5124 × cxp 5538 dom cdm 5540 ran crn 5541 ℩cio 6325 ‘cfv 6369 (class class class)co 7202 Xcixp 8567 finSupp cfsupp 8974 1c1 10713 -cneg 11046 / cdiv 11472 ℕcn 11813 2c2 11868 ℕ0cn0 12073 ℤcz 12159 ↑cexp 13618 Word cword 14052 Basecbs 16684 ↾s cress 16685 0gc0g 16916 Σg cgsu 16917 Mndcmnd 18145 Grpcgrp 18337 .gcmg 18460 SubGrpcsubg 18509 odcod 18888 DProd cdprd 19352 dProjcdpj 19353 mulGrpcmgp 19476 1rcur 19488 Ringcrg 19534 CRingccrg 19535 Unitcui 19629 ℤ/nℤczn 20441 ↑𝑐ccxp 25416 DChrcdchr 26085 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2158 ax-12 2175 ax-ext 2706 ax-rep 5168 ax-sep 5181 ax-nul 5188 ax-pow 5247 ax-pr 5311 ax-un 7512 ax-inf2 9245 ax-cnex 10768 ax-resscn 10769 ax-1cn 10770 ax-icn 10771 ax-addcl 10772 ax-addrcl 10773 ax-mulcl 10774 ax-mulrcl 10775 ax-mulcom 10776 ax-addass 10777 ax-mulass 10778 ax-distr 10779 ax-i2m1 10780 ax-1ne0 10781 ax-1rid 10782 ax-rnegex 10783 ax-rrecex 10784 ax-cnre 10785 ax-pre-lttri 10786 ax-pre-lttrn 10787 ax-pre-ltadd 10788 ax-pre-mulgt0 10789 ax-pre-sup 10790 ax-addf 10791 ax-mulf 10792 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-3or 1090 df-3an 1091 df-tru 1546 df-fal 1556 df-ex 1788 df-nf 1792 df-sb 2071 df-mo 2537 df-eu 2566 df-clab 2713 df-cleq 2726 df-clel 2812 df-nfc 2882 df-ne 2936 df-nel 3040 df-ral 3059 df-rex 3060 df-reu 3061 df-rmo 3062 df-rab 3063 df-v 3403 df-sbc 3688 df-csb 3803 df-dif 3860 df-un 3862 df-in 3864 df-ss 3874 df-pss 3876 df-nul 4228 df-if 4430 df-pw 4505 df-sn 4532 df-pr 4534 df-tp 4536 df-op 4538 df-uni 4810 df-int 4850 df-iun 4896 df-iin 4897 df-br 5044 df-opab 5106 df-mpt 5125 df-tr 5151 df-id 5444 df-eprel 5449 df-po 5457 df-so 5458 df-fr 5498 df-se 5499 df-we 5500 df-xp 5546 df-rel 5547 df-cnv 5548 df-co 5549 df-dm 5550 df-rn 5551 df-res 5552 df-ima 5553 df-pred 6149 df-ord 6205 df-on 6206 df-lim 6207 df-suc 6208 df-iota 6327 df-fun 6371 df-fn 6372 df-f 6373 df-f1 6374 df-fo 6375 df-f1o 6376 df-fv 6377 df-isom 6378 df-riota 7159 df-ov 7205 df-oprab 7206 df-mpo 7207 df-of 7458 df-om 7634 df-1st 7750 df-2nd 7751 df-supp 7893 df-tpos 7957 df-wrecs 8036 df-recs 8097 df-rdg 8135 df-1o 8191 df-2o 8192 df-oadd 8195 df-omul 8196 df-er 8380 df-ec 8382 df-qs 8386 df-map 8499 df-pm 8500 df-ixp 8568 df-en 8616 df-dom 8617 df-sdom 8618 df-fin 8619 df-fsupp 8975 df-fi 9016 df-sup 9047 df-inf 9048 df-oi 9115 df-card 9538 df-acn 9541 df-pnf 10852 df-mnf 10853 df-xr 10854 df-ltxr 10855 df-le 10856 df-sub 11047 df-neg 11048 df-div 11473 df-nn 11814 df-2 11876 df-3 11877 df-4 11878 df-5 11879 df-6 11880 df-7 11881 df-8 11882 df-9 11883 df-n0 12074 df-z 12160 df-dec 12277 df-uz 12422 df-q 12528 df-rp 12570 df-xneg 12687 df-xadd 12688 df-xmul 12689 df-ioo 12922 df-ioc 12923 df-ico 12924 df-icc 12925 df-fz 13079 df-fzo 13222 df-fl 13350 df-mod 13426 df-seq 13558 df-exp 13619 df-fac 13823 df-bc 13852 df-hash 13880 df-word 14053 df-shft 14613 df-cj 14645 df-re 14646 df-im 14647 df-sqrt 14781 df-abs 14782 df-limsup 15015 df-clim 15032 df-rlim 15033 df-sum 15233 df-ef 15610 df-sin 15612 df-cos 15613 df-pi 15615 df-dvds 15797 df-struct 16686 df-ndx 16687 df-slot 16688 df-base 16690 df-sets 16691 df-ress 16692 df-plusg 16780 df-mulr 16781 df-starv 16782 df-sca 16783 df-vsca 16784 df-ip 16785 df-tset 16786 df-ple 16787 df-ds 16789 df-unif 16790 df-hom 16791 df-cco 16792 df-rest 16899 df-topn 16900 df-0g 16918 df-gsum 16919 df-topgen 16920 df-pt 16921 df-prds 16924 df-xrs 16979 df-qtop 16984 df-imas 16985 df-qus 16986 df-xps 16987 df-mre 17061 df-mrc 17062 df-acs 17064 df-mgm 18086 df-sgrp 18135 df-mnd 18146 df-mhm 18190 df-submnd 18191 df-grp 18340 df-minusg 18341 df-sbg 18342 df-mulg 18461 df-subg 18512 df-nsg 18513 df-eqg 18514 df-ghm 18592 df-gim 18635 df-cntz 18683 df-oppg 18710 df-od 18892 df-lsm 18997 df-pj1 18998 df-cmn 19144 df-abl 19145 df-dprd 19354 df-dpj 19355 df-mgp 19477 df-ur 19489 df-ring 19536 df-cring 19537 df-oppr 19613 df-dvdsr 19631 df-unit 19632 df-rnghom 19707 df-subrg 19770 df-lmod 19873 df-lss 19941 df-lsp 19981 df-sra 20181 df-rgmod 20182 df-lidl 20183 df-rsp 20184 df-2idl 20242 df-psmet 20327 df-xmet 20328 df-met 20329 df-bl 20330 df-mopn 20331 df-fbas 20332 df-fg 20333 df-cnfld 20336 df-zring 20408 df-zrh 20442 df-zn 20445 df-top 21763 df-topon 21780 df-topsp 21802 df-bases 21815 df-cld 21888 df-ntr 21889 df-cls 21890 df-nei 21967 df-lp 22005 df-perf 22006 df-cn 22096 df-cnp 22097 df-haus 22184 df-tx 22431 df-hmeo 22624 df-fil 22715 df-fm 22807 df-flim 22808 df-flf 22809 df-xms 23190 df-ms 23191 df-tms 23192 df-cncf 23747 df-limc 24735 df-dv 24736 df-log 25417 df-cxp 25418 df-dchr 26086 |
This theorem is referenced by: dchrpt 26120 |
Copyright terms: Public domain | W3C validator |