![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > cygznlem2a | Structured version Visualization version GIF version |
Description: Lemma for cygzn 21099. (Contributed by Mario Carneiro, 23-Dec-2016.) |
Ref | Expression |
---|---|
cygzn.b | ⊢ 𝐵 = (Base‘𝐺) |
cygzn.n | ⊢ 𝑁 = if(𝐵 ∈ Fin, (♯‘𝐵), 0) |
cygzn.y | ⊢ 𝑌 = (ℤ/nℤ‘𝑁) |
cygzn.m | ⊢ · = (.g‘𝐺) |
cygzn.l | ⊢ 𝐿 = (ℤRHom‘𝑌) |
cygzn.e | ⊢ 𝐸 = {𝑥 ∈ 𝐵 ∣ ran (𝑛 ∈ ℤ ↦ (𝑛 · 𝑥)) = 𝐵} |
cygzn.g | ⊢ (𝜑 → 𝐺 ∈ CycGrp) |
cygzn.x | ⊢ (𝜑 → 𝑋 ∈ 𝐸) |
cygzn.f | ⊢ 𝐹 = ran (𝑚 ∈ ℤ ↦ 〈(𝐿‘𝑚), (𝑚 · 𝑋)〉) |
Ref | Expression |
---|---|
cygznlem2a | ⊢ (𝜑 → 𝐹:(Base‘𝑌)⟶𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cygzn.f | . . . 4 ⊢ 𝐹 = ran (𝑚 ∈ ℤ ↦ 〈(𝐿‘𝑚), (𝑚 · 𝑋)〉) | |
2 | fvexd 6896 | . . . 4 ⊢ ((𝜑 ∧ 𝑚 ∈ ℤ) → (𝐿‘𝑚) ∈ V) | |
3 | cygzn.g | . . . . . . 7 ⊢ (𝜑 → 𝐺 ∈ CycGrp) | |
4 | cyggrp 19741 | . . . . . . 7 ⊢ (𝐺 ∈ CycGrp → 𝐺 ∈ Grp) | |
5 | 3, 4 | syl 17 | . . . . . 6 ⊢ (𝜑 → 𝐺 ∈ Grp) |
6 | 5 | adantr 482 | . . . . 5 ⊢ ((𝜑 ∧ 𝑚 ∈ ℤ) → 𝐺 ∈ Grp) |
7 | simpr 486 | . . . . 5 ⊢ ((𝜑 ∧ 𝑚 ∈ ℤ) → 𝑚 ∈ ℤ) | |
8 | cygzn.e | . . . . . . . 8 ⊢ 𝐸 = {𝑥 ∈ 𝐵 ∣ ran (𝑛 ∈ ℤ ↦ (𝑛 · 𝑥)) = 𝐵} | |
9 | 8 | ssrab3 4078 | . . . . . . 7 ⊢ 𝐸 ⊆ 𝐵 |
10 | cygzn.x | . . . . . . 7 ⊢ (𝜑 → 𝑋 ∈ 𝐸) | |
11 | 9, 10 | sselid 3978 | . . . . . 6 ⊢ (𝜑 → 𝑋 ∈ 𝐵) |
12 | 11 | adantr 482 | . . . . 5 ⊢ ((𝜑 ∧ 𝑚 ∈ ℤ) → 𝑋 ∈ 𝐵) |
13 | cygzn.b | . . . . . 6 ⊢ 𝐵 = (Base‘𝐺) | |
14 | cygzn.m | . . . . . 6 ⊢ · = (.g‘𝐺) | |
15 | 13, 14 | mulgcl 18956 | . . . . 5 ⊢ ((𝐺 ∈ Grp ∧ 𝑚 ∈ ℤ ∧ 𝑋 ∈ 𝐵) → (𝑚 · 𝑋) ∈ 𝐵) |
16 | 6, 7, 12, 15 | syl3anc 1372 | . . . 4 ⊢ ((𝜑 ∧ 𝑚 ∈ ℤ) → (𝑚 · 𝑋) ∈ 𝐵) |
17 | fveq2 6881 | . . . 4 ⊢ (𝑚 = 𝑘 → (𝐿‘𝑚) = (𝐿‘𝑘)) | |
18 | oveq1 7403 | . . . 4 ⊢ (𝑚 = 𝑘 → (𝑚 · 𝑋) = (𝑘 · 𝑋)) | |
19 | cygzn.n | . . . . . . . 8 ⊢ 𝑁 = if(𝐵 ∈ Fin, (♯‘𝐵), 0) | |
20 | cygzn.y | . . . . . . . 8 ⊢ 𝑌 = (ℤ/nℤ‘𝑁) | |
21 | cygzn.l | . . . . . . . 8 ⊢ 𝐿 = (ℤRHom‘𝑌) | |
22 | 13, 19, 20, 14, 21, 8, 3, 10 | cygznlem1 21095 | . . . . . . 7 ⊢ ((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑘 ∈ ℤ)) → ((𝐿‘𝑚) = (𝐿‘𝑘) ↔ (𝑚 · 𝑋) = (𝑘 · 𝑋))) |
23 | 22 | biimpd 228 | . . . . . 6 ⊢ ((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑘 ∈ ℤ)) → ((𝐿‘𝑚) = (𝐿‘𝑘) → (𝑚 · 𝑋) = (𝑘 · 𝑋))) |
24 | 23 | exp32 422 | . . . . 5 ⊢ (𝜑 → (𝑚 ∈ ℤ → (𝑘 ∈ ℤ → ((𝐿‘𝑚) = (𝐿‘𝑘) → (𝑚 · 𝑋) = (𝑘 · 𝑋))))) |
25 | 24 | 3imp2 1350 | . . . 4 ⊢ ((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑘 ∈ ℤ ∧ (𝐿‘𝑚) = (𝐿‘𝑘))) → (𝑚 · 𝑋) = (𝑘 · 𝑋)) |
26 | 1, 2, 16, 17, 18, 25 | fliftfund 7297 | . . 3 ⊢ (𝜑 → Fun 𝐹) |
27 | 1, 2, 16 | fliftf 7299 | . . 3 ⊢ (𝜑 → (Fun 𝐹 ↔ 𝐹:ran (𝑚 ∈ ℤ ↦ (𝐿‘𝑚))⟶𝐵)) |
28 | 26, 27 | mpbid 231 | . 2 ⊢ (𝜑 → 𝐹:ran (𝑚 ∈ ℤ ↦ (𝐿‘𝑚))⟶𝐵) |
29 | hashcl 14303 | . . . . . . . . . . 11 ⊢ (𝐵 ∈ Fin → (♯‘𝐵) ∈ ℕ0) | |
30 | 29 | adantl 483 | . . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐵 ∈ Fin) → (♯‘𝐵) ∈ ℕ0) |
31 | 0nn0 12474 | . . . . . . . . . . 11 ⊢ 0 ∈ ℕ0 | |
32 | 31 | a1i 11 | . . . . . . . . . 10 ⊢ ((𝜑 ∧ ¬ 𝐵 ∈ Fin) → 0 ∈ ℕ0) |
33 | 30, 32 | ifclda 4559 | . . . . . . . . 9 ⊢ (𝜑 → if(𝐵 ∈ Fin, (♯‘𝐵), 0) ∈ ℕ0) |
34 | 19, 33 | eqeltrid 2838 | . . . . . . . 8 ⊢ (𝜑 → 𝑁 ∈ ℕ0) |
35 | eqid 2733 | . . . . . . . . 9 ⊢ (Base‘𝑌) = (Base‘𝑌) | |
36 | 20, 35, 21 | znzrhfo 21076 | . . . . . . . 8 ⊢ (𝑁 ∈ ℕ0 → 𝐿:ℤ–onto→(Base‘𝑌)) |
37 | 34, 36 | syl 17 | . . . . . . 7 ⊢ (𝜑 → 𝐿:ℤ–onto→(Base‘𝑌)) |
38 | fof 6795 | . . . . . . 7 ⊢ (𝐿:ℤ–onto→(Base‘𝑌) → 𝐿:ℤ⟶(Base‘𝑌)) | |
39 | 37, 38 | syl 17 | . . . . . 6 ⊢ (𝜑 → 𝐿:ℤ⟶(Base‘𝑌)) |
40 | 39 | feqmptd 6949 | . . . . 5 ⊢ (𝜑 → 𝐿 = (𝑚 ∈ ℤ ↦ (𝐿‘𝑚))) |
41 | 40 | rneqd 5932 | . . . 4 ⊢ (𝜑 → ran 𝐿 = ran (𝑚 ∈ ℤ ↦ (𝐿‘𝑚))) |
42 | forn 6798 | . . . . 5 ⊢ (𝐿:ℤ–onto→(Base‘𝑌) → ran 𝐿 = (Base‘𝑌)) | |
43 | 37, 42 | syl 17 | . . . 4 ⊢ (𝜑 → ran 𝐿 = (Base‘𝑌)) |
44 | 41, 43 | eqtr3d 2775 | . . 3 ⊢ (𝜑 → ran (𝑚 ∈ ℤ ↦ (𝐿‘𝑚)) = (Base‘𝑌)) |
45 | 44 | feq2d 6693 | . 2 ⊢ (𝜑 → (𝐹:ran (𝑚 ∈ ℤ ↦ (𝐿‘𝑚))⟶𝐵 ↔ 𝐹:(Base‘𝑌)⟶𝐵)) |
46 | 28, 45 | mpbid 231 | 1 ⊢ (𝜑 → 𝐹:(Base‘𝑌)⟶𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 397 = wceq 1542 ∈ wcel 2107 {crab 3433 Vcvv 3475 ifcif 4524 〈cop 4630 ↦ cmpt 5227 ran crn 5673 Fun wfun 6529 ⟶wf 6531 –onto→wfo 6533 ‘cfv 6535 (class class class)co 7396 Fincfn 8927 0cc0 11097 ℕ0cn0 12459 ℤcz 12545 ♯chash 14277 Basecbs 17131 Grpcgrp 18806 .gcmg 18935 CycGrpccyg 19728 ℤRHomczrh 21022 ℤ/nℤczn 21025 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2704 ax-rep 5281 ax-sep 5295 ax-nul 5302 ax-pow 5359 ax-pr 5423 ax-un 7712 ax-inf2 9623 ax-cnex 11153 ax-resscn 11154 ax-1cn 11155 ax-icn 11156 ax-addcl 11157 ax-addrcl 11158 ax-mulcl 11159 ax-mulrcl 11160 ax-mulcom 11161 ax-addass 11162 ax-mulass 11163 ax-distr 11164 ax-i2m1 11165 ax-1ne0 11166 ax-1rid 11167 ax-rnegex 11168 ax-rrecex 11169 ax-cnre 11170 ax-pre-lttri 11171 ax-pre-lttrn 11172 ax-pre-ltadd 11173 ax-pre-mulgt0 11174 ax-pre-sup 11175 ax-addf 11176 ax-mulf 11177 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2535 df-eu 2564 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2886 df-ne 2942 df-nel 3048 df-ral 3063 df-rex 3072 df-rmo 3377 df-reu 3378 df-rab 3434 df-v 3477 df-sbc 3776 df-csb 3892 df-dif 3949 df-un 3951 df-in 3953 df-ss 3963 df-pss 3965 df-nul 4321 df-if 4525 df-pw 4600 df-sn 4625 df-pr 4627 df-tp 4629 df-op 4631 df-uni 4905 df-int 4947 df-iun 4995 df-br 5145 df-opab 5207 df-mpt 5228 df-tr 5262 df-id 5570 df-eprel 5576 df-po 5584 df-so 5585 df-fr 5627 df-se 5628 df-we 5629 df-xp 5678 df-rel 5679 df-cnv 5680 df-co 5681 df-dm 5682 df-rn 5683 df-res 5684 df-ima 5685 df-pred 6292 df-ord 6359 df-on 6360 df-lim 6361 df-suc 6362 df-iota 6487 df-fun 6537 df-fn 6538 df-f 6539 df-f1 6540 df-fo 6541 df-f1o 6542 df-fv 6543 df-isom 6544 df-riota 7352 df-ov 7399 df-oprab 7400 df-mpo 7401 df-om 7843 df-1st 7962 df-2nd 7963 df-tpos 8198 df-frecs 8253 df-wrecs 8284 df-recs 8358 df-rdg 8397 df-1o 8453 df-oadd 8457 df-omul 8458 df-er 8691 df-ec 8693 df-qs 8697 df-map 8810 df-en 8928 df-dom 8929 df-sdom 8930 df-fin 8931 df-sup 9424 df-inf 9425 df-oi 9492 df-card 9921 df-acn 9924 df-pnf 11237 df-mnf 11238 df-xr 11239 df-ltxr 11240 df-le 11241 df-sub 11433 df-neg 11434 df-div 11859 df-nn 12200 df-2 12262 df-3 12263 df-4 12264 df-5 12265 df-6 12266 df-7 12267 df-8 12268 df-9 12269 df-n0 12460 df-z 12546 df-dec 12665 df-uz 12810 df-rp 12962 df-fz 13472 df-fl 13744 df-mod 13822 df-seq 13954 df-exp 14015 df-hash 14278 df-cj 15033 df-re 15034 df-im 15035 df-sqrt 15169 df-abs 15170 df-dvds 16185 df-struct 17067 df-sets 17084 df-slot 17102 df-ndx 17114 df-base 17132 df-ress 17161 df-plusg 17197 df-mulr 17198 df-starv 17199 df-sca 17200 df-vsca 17201 df-ip 17202 df-tset 17203 df-ple 17204 df-ds 17206 df-unif 17207 df-0g 17374 df-imas 17441 df-qus 17442 df-mgm 18548 df-sgrp 18597 df-mnd 18613 df-mhm 18658 df-grp 18809 df-minusg 18810 df-sbg 18811 df-mulg 18936 df-subg 18988 df-nsg 18989 df-eqg 18990 df-ghm 19075 df-od 19380 df-cmn 19634 df-abl 19635 df-cyg 19729 df-mgp 19971 df-ur 19988 df-ring 20040 df-cring 20041 df-oppr 20128 df-dvdsr 20149 df-rnghom 20229 df-subrg 20338 df-lmod 20450 df-lss 20520 df-lsp 20560 df-sra 20762 df-rgmod 20763 df-lidl 20764 df-rsp 20765 df-2idl 20833 df-cnfld 20919 df-zring 20992 df-zrh 21026 df-zn 21029 |
This theorem is referenced by: cygznlem2 21097 cygznlem3 21098 |
Copyright terms: Public domain | W3C validator |