cygznlem1 - Metamath Proof Explorer

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

Theorem cygznlem1 21687

Description: Lemma for cygzn 21691. (Contributed by Mario Carneiro, 21-Apr-2016.)

**Hypotheses**
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	⊢ (𝜑 → 𝑋 ∈ 𝐸)

**Assertion**
Ref	Expression
cygznlem1	⊢ ((𝜑 ∧ (𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ)) → ((𝐿‘𝐾) = (𝐿‘𝑀) ↔ (𝐾 · 𝑋) = (𝑀 · 𝑋)))

Distinct variable groups: 𝑥,𝑛,𝐵 𝑛,𝐺,𝑥 · ,𝑛,𝑥 𝑛,𝑌,𝑥 𝑛,𝐿,𝑥 𝑥,𝑁 𝑛,𝑋,𝑥 Allowed substitution hints: 𝜑(𝑥,𝑛) 𝐸(𝑥,𝑛) 𝐾(𝑥,𝑛) 𝑀(𝑥,𝑛) 𝑁(𝑛)

**Proof of Theorem cygznlem1**
Step	Hyp	Ref	Expression
1		cygzn.n	. . . . 5 ⊢ 𝑁 = if(𝐵 ∈ Fin, (♯‘𝐵), 0)
2		hashcl 14394	. . . . . . 7 ⊢ (𝐵 ∈ Fin → (♯‘𝐵) ∈ ℕ₀)
3	2	adantl 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝐵 ∈ Fin) → (♯‘𝐵) ∈ ℕ₀)
4		0nn0 12521	. . . . . . 7 ⊢ 0 ∈ ℕ₀
5	4	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ ¬ 𝐵 ∈ Fin) → 0 ∈ ℕ₀)
6	3, 5	ifclda 4528	. . . . 5 ⊢ (𝜑 → if(𝐵 ∈ Fin, (♯‘𝐵), 0) ∈ ℕ₀)
7	1, 6	eqeltrid 2873	. . . 4 ⊢ (𝜑 → 𝑁 ∈ ℕ₀)
8	7	adantr 485	. . 3 ⊢ ((𝜑 ∧ (𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ)) → 𝑁 ∈ ℕ₀)
9		simprl 782	. . 3 ⊢ ((𝜑 ∧ (𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ)) → 𝐾 ∈ ℤ)
10		simprr 784	. . 3 ⊢ ((𝜑 ∧ (𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ)) → 𝑀 ∈ ℤ)
11		cygzn.y	. . . 4 ⊢ 𝑌 = (ℤ/nℤ‘𝑁)
12		cygzn.l	. . . 4 ⊢ 𝐿 = (ℤRHom‘𝑌)
13	11, 12	zndvds 21670	. . 3 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((𝐿‘𝐾) = (𝐿‘𝑀) ↔ 𝑁 ∥ (𝐾 − 𝑀)))
14	8, 9, 10, 13	syl3anc 1396	. 2 ⊢ ((𝜑 ∧ (𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ)) → ((𝐿‘𝐾) = (𝐿‘𝑀) ↔ 𝑁 ∥ (𝐾 − 𝑀)))
15		cygzn.g	. . . . . . 7 ⊢ (𝜑 → 𝐺 ∈ CycGrp)
16		cyggrp 19962	. . . . . . 7 ⊢ (𝐺 ∈ CycGrp → 𝐺 ∈ Grp)
17	15, 16	syl 18	. . . . . 6 ⊢ (𝜑 → 𝐺 ∈ Grp)
18		cygzn.x	. . . . . 6 ⊢ (𝜑 → 𝑋 ∈ 𝐸)
19		cygzn.b	. . . . . . 7 ⊢ 𝐵 = (Base‘𝐺)
20		cygzn.m	. . . . . . 7 ⊢ · = (._g‘𝐺)
21		cygzn.e	. . . . . . 7 ⊢ 𝐸 = {𝑥 ∈ 𝐵 ∣ ran (𝑛 ∈ ℤ ↦ (𝑛 · 𝑥)) = 𝐵}
22		eqid 2769	. . . . . . 7 ⊢ (od‘𝐺) = (od‘𝐺)
23	19, 20, 21, 22	cyggenod2 19957	. . . . . 6 ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐸) → ((od‘𝐺)‘𝑋) = if(𝐵 ∈ Fin, (♯‘𝐵), 0))
24	17, 18, 23	syl2anc 595	. . . . 5 ⊢ (𝜑 → ((od‘𝐺)‘𝑋) = if(𝐵 ∈ Fin, (♯‘𝐵), 0))
25	24, 1	eqtr4di 2822	. . . 4 ⊢ (𝜑 → ((od‘𝐺)‘𝑋) = 𝑁)
26	25	adantr 485	. . 3 ⊢ ((𝜑 ∧ (𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ)) → ((od‘𝐺)‘𝑋) = 𝑁)
27	26	breq1d 5123	. 2 ⊢ ((𝜑 ∧ (𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ)) → (((od‘𝐺)‘𝑋) ∥ (𝐾 − 𝑀) ↔ 𝑁 ∥ (𝐾 − 𝑀)))
28	17	adantr 485	. . 3 ⊢ ((𝜑 ∧ (𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ)) → 𝐺 ∈ Grp)
29	19, 20, 21	iscyggen 19952	. . . . . 6 ⊢ (𝑋 ∈ 𝐸 ↔ (𝑋 ∈ 𝐵 ∧ ran (𝑛 ∈ ℤ ↦ (𝑛 · 𝑋)) = 𝐵))
30	29	simplbi 501	. . . . 5 ⊢ (𝑋 ∈ 𝐸 → 𝑋 ∈ 𝐵)
31	18, 30	syl 18	. . . 4 ⊢ (𝜑 → 𝑋 ∈ 𝐵)
32	31	adantr 485	. . 3 ⊢ ((𝜑 ∧ (𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ)) → 𝑋 ∈ 𝐵)
33		eqid 2769	. . . 4 ⊢ (0_g‘𝐺) = (0_g‘𝐺)
34	19, 22, 20, 33	odcong 19621	. . 3 ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ (𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ)) → (((od‘𝐺)‘𝑋) ∥ (𝐾 − 𝑀) ↔ (𝐾 · 𝑋) = (𝑀 · 𝑋)))
35	28, 32, 9, 10, 34	syl112anc 1399	. 2 ⊢ ((𝜑 ∧ (𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ)) → (((od‘𝐺)‘𝑋) ∥ (𝐾 − 𝑀) ↔ (𝐾 · 𝑋) = (𝑀 · 𝑋)))
36	14, 27, 35	3bitr2d 310	1 ⊢ ((𝜑 ∧ (𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ)) → ((𝐿‘𝐾) = (𝐿‘𝑀) ↔ (𝐾 · 𝑋) = (𝑀 · 𝑋)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 400 = wceq 1567 ∈ wcel 2149 {crab 3423 ifcif 4492 class class class wbr 5113 ↦ cmpt 5196 ran crn 5665 ‘cfv 6539 (class class class)co 7413 Fincfn 8945 0cc0 11102 − cmin 11443 ℕ₀cn0 12506 ℤcz 12593 ♯chash 14368 ∥ cdvds 16312 Basecbs 17271 0_gc0g 17494 Grpcgrp 19002 ._gcmg 19135 odcod 19596 CycGrpccyg 19949 ℤRHomczrh 21620 ℤ/nℤczn 21623

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1822 ax-4 1836 ax-5 1937 ax-6 1994 ax-7 2035 ax-8 2151 ax-9 2159 ax-10 2182 ax-11 2198 ax-12 2219 ax-ext 2741 ax-rep 5242 ax-sep 5261 ax-nul 5273 ax-pow 5339 ax-pr 5407 ax-un 7735 ax-inf2 9612 ax-cnex 11158 ax-resscn 11159 ax-1cn 11160 ax-icn 11161 ax-addcl 11162 ax-addrcl 11163 ax-mulcl 11164 ax-mulrcl 11165 ax-mulcom 11166 ax-addass 11167 ax-mulass 11168 ax-distr 11169 ax-i2m1 11170 ax-1ne0 11171 ax-1rid 11172 ax-rnegex 11173 ax-rrecex 11174 ax-cnre 11175 ax-pre-lttri 11176 ax-pre-lttrn 11177 ax-pre-ltadd 11178 ax-pre-mulgt0 11179 ax-pre-sup 11180 ax-addf 11181 ax-mulf 11182

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1102 df-3an 1103 df-tru 1570 df-fal 1580 df-ex 1807 df-nf 1811 df-sb 2098 df-mo 2573 df-eu 2603 df-clab 2748 df-cleq 2761 df-clel 2844 df-nfc 2918 df-ne 2965 df-nel 3071 df-ral 3086 df-rex 3096 df-rmo 3376 df-reu 3377 df-rab 3424 df-v 3465 df-sbc 3754 df-csb 3862 df-dif 3916 df-un 3918 df-in 3920 df-ss 3930 df-pss 3933 df-nul 4295 df-if 4493 df-pw 4569 df-sn 4595 df-pr 4597 df-tp 4599 df-op 4601 df-uni 4877 df-int 4917 df-iun 4962 df-br 5114 df-opab 5178 df-mpt 5197 df-tr 5223 df-id 5559 df-eprel 5564 df-po 5572 df-so 5573 df-fr 5617 df-se 5618 df-we 5619 df-xp 5670 df-rel 5671 df-cnv 5672 df-co 5673 df-dm 5674 df-rn 5675 df-res 5676 df-ima 5677 df-pred 6305 df-ord 6366 df-on 6367 df-lim 6368 df-suc 6369 df-iota 6495 df-fun 6541 df-fn 6542 df-f 6543 df-f1 6544 df-fo 6545 df-f1o 6546 df-fv 6547 df-isom 6548 df-riota 7370 df-ov 7416 df-oprab 7417 df-mpo 7418 df-om 7865 df-1st 7988 df-2nd 7989 df-tpos 8224 df-frecs 8280 df-wrecs 8311 df-recs 8360 df-rdg 8399 df-1o 8455 df-oadd 8459 df-omul 8460 df-er 8696 df-ec 8698 df-qs 8702 df-map 8828 df-en 8946 df-dom 8947 df-sdom 8948 df-fin 8949 df-sup 9404 df-inf 9405 df-oi 9474 df-card 9927 df-acn 9930 df-pnf 11247 df-mnf 11248 df-xr 11249 df-ltxr 11250 df-le 11251 df-sub 11445 df-neg 11446 df-div 11874 df-nn 12236 df-2 12305 df-3 12306 df-4 12307 df-5 12308 df-6 12309 df-7 12310 df-8 12311 df-9 12312 df-n0 12507 df-z 12594 df-dec 12714 df-uz 12865 df-rp 13019 df-fz 13538 df-fl 13827 df-mod 13905 df-seq 14040 df-exp 14100 df-hash 14369 df-cj 15152 df-re 15153 df-im 15154 df-sqrt 15288 df-abs 15289 df-dvds 16313 df-struct 17209 df-sets 17226 df-slot 17244 df-ndx 17256 df-base 17272 df-ress 17293 df-plusg 17325 df-mulr 17326 df-starv 17327 df-sca 17328 df-vsca 17329 df-ip 17330 df-tset 17331 df-ple 17332 df-ds 17334 df-unif 17335 df-0g 17496 df-imas 17564 df-qus 17565 df-mgm 18700 df-sgrp 18779 df-mnd 18795 df-mhm 18843 df-grp 19005 df-minusg 19006 df-sbg 19007 df-mulg 19136 df-subg 19191 df-nsg 19192 df-eqg 19193 df-ghm 19286 df-od 19600 df-cmn 19854 df-abl 19855 df-cyg 19950 df-mgp 20219 df-rng 20233 df-ur 20266 df-ring 20319 df-cring 20320 df-oppr 20421 df-dvdsr 20441 df-rhm 20556 df-subrng 20633 df-subrg 20657 df-lmod 20963 df-lss 21033 df-lsp 21073 df-sra 21274 df-rgmod 21275 df-lidl 21312 df-rsp 21313 df-2idl 21362 df-cnfld 21494 df-zring 21568 df-zrh 21624 df-zn 21627

This theorem is referenced by: cygznlem2a 21688 cygznlem3 21690

W3C validator