cygznlem2a - Metamath Proof Explorer

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

Theorem cygznlem2a 19964

Description: Lemma for cygzn 19967. (Contributed by Mario Carneiro, 23-Dec-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	⊢ (𝜑 → 𝑋 ∈ 𝐸)
cygzn.f	⊢ 𝐹 = ran (𝑚 ∈ ℤ ↦ ⟨(𝐿‘𝑚), (𝑚 · 𝑋)⟩)

**Assertion**
Ref	Expression
cygznlem2a	⊢ (𝜑 → 𝐹:(Base‘𝑌)⟶𝐵)

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

Proof of Theorem cygznlem2a Dummy variable 𝑘 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		cygzn.f	. . . 4 ⊢ 𝐹 = ran (𝑚 ∈ ℤ ↦ ⟨(𝐿‘𝑚), (𝑚 · 𝑋)⟩)
2		fvexd 6241	. . . 4 ⊢ ((𝜑 ∧ 𝑚 ∈ ℤ) → (𝐿‘𝑚) ∈ V)
3		cygzn.g	. . . . . . 7 ⊢ (𝜑 → 𝐺 ∈ CycGrp)
4		cyggrp 18337	. . . . . . 7 ⊢ (𝐺 ∈ CycGrp → 𝐺 ∈ Grp)
5	3, 4	syl 17	. . . . . 6 ⊢ (𝜑 → 𝐺 ∈ Grp)
6	5	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑚 ∈ ℤ) → 𝐺 ∈ Grp)
7		simpr 476	. . . . 5 ⊢ ((𝜑 ∧ 𝑚 ∈ ℤ) → 𝑚 ∈ ℤ)
8		cygzn.e	. . . . . . . 8 ⊢ 𝐸 = {𝑥 ∈ 𝐵 ∣ ran (𝑛 ∈ ℤ ↦ (𝑛 · 𝑥)) = 𝐵}
9		ssrab2 3720	. . . . . . . 8 ⊢ {𝑥 ∈ 𝐵 ∣ ran (𝑛 ∈ ℤ ↦ (𝑛 · 𝑥)) = 𝐵} ⊆ 𝐵
10	8, 9	eqsstri 3668	. . . . . . 7 ⊢ 𝐸 ⊆ 𝐵
11		cygzn.x	. . . . . . 7 ⊢ (𝜑 → 𝑋 ∈ 𝐸)
12	10, 11	sseldi 3634	. . . . . 6 ⊢ (𝜑 → 𝑋 ∈ 𝐵)
13	12	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑚 ∈ ℤ) → 𝑋 ∈ 𝐵)
14		cygzn.b	. . . . . 6 ⊢ 𝐵 = (Base‘𝐺)
15		cygzn.m	. . . . . 6 ⊢ · = (._g‘𝐺)
16	14, 15	mulgcl 17606	. . . . 5 ⊢ ((𝐺 ∈ Grp ∧ 𝑚 ∈ ℤ ∧ 𝑋 ∈ 𝐵) → (𝑚 · 𝑋) ∈ 𝐵)
17	6, 7, 13, 16	syl3anc 1366	. . . 4 ⊢ ((𝜑 ∧ 𝑚 ∈ ℤ) → (𝑚 · 𝑋) ∈ 𝐵)
18		fveq2 6229	. . . 4 ⊢ (𝑚 = 𝑘 → (𝐿‘𝑚) = (𝐿‘𝑘))
19		oveq1 6697	. . . 4 ⊢ (𝑚 = 𝑘 → (𝑚 · 𝑋) = (𝑘 · 𝑋))
20		cygzn.n	. . . . . . . 8 ⊢ 𝑁 = if(𝐵 ∈ Fin, (#‘𝐵), 0)
21		cygzn.y	. . . . . . . 8 ⊢ 𝑌 = (ℤ/nℤ‘𝑁)
22		cygzn.l	. . . . . . . 8 ⊢ 𝐿 = (ℤRHom‘𝑌)
23	14, 20, 21, 15, 22, 8, 3, 11	cygznlem1 19963	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑘 ∈ ℤ)) → ((𝐿‘𝑚) = (𝐿‘𝑘) ↔ (𝑚 · 𝑋) = (𝑘 · 𝑋)))
24	23	biimpd 219	. . . . . 6 ⊢ ((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑘 ∈ ℤ)) → ((𝐿‘𝑚) = (𝐿‘𝑘) → (𝑚 · 𝑋) = (𝑘 · 𝑋)))
25	24	exp32 630	. . . . 5 ⊢ (𝜑 → (𝑚 ∈ ℤ → (𝑘 ∈ ℤ → ((𝐿‘𝑚) = (𝐿‘𝑘) → (𝑚 · 𝑋) = (𝑘 · 𝑋)))))
26	25	3imp2 1304	. . . 4 ⊢ ((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑘 ∈ ℤ ∧ (𝐿‘𝑚) = (𝐿‘𝑘))) → (𝑚 · 𝑋) = (𝑘 · 𝑋))
27	1, 2, 17, 18, 19, 26	fliftfund 6603	. . 3 ⊢ (𝜑 → Fun 𝐹)
28	1, 2, 17	fliftf 6605	. . 3 ⊢ (𝜑 → (Fun 𝐹 ↔ 𝐹:ran (𝑚 ∈ ℤ ↦ (𝐿‘𝑚))⟶𝐵))
29	27, 28	mpbid 222	. 2 ⊢ (𝜑 → 𝐹:ran (𝑚 ∈ ℤ ↦ (𝐿‘𝑚))⟶𝐵)
30		hashcl 13185	. . . . . . . . . . 11 ⊢ (𝐵 ∈ Fin → (#‘𝐵) ∈ ℕ₀)
31	30	adantl 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐵 ∈ Fin) → (#‘𝐵) ∈ ℕ₀)
32		0nn0 11345	. . . . . . . . . . 11 ⊢ 0 ∈ ℕ₀
33	32	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ¬ 𝐵 ∈ Fin) → 0 ∈ ℕ₀)
34	31, 33	ifclda 4153	. . . . . . . . 9 ⊢ (𝜑 → if(𝐵 ∈ Fin, (#‘𝐵), 0) ∈ ℕ₀)
35	20, 34	syl5eqel 2734	. . . . . . . 8 ⊢ (𝜑 → 𝑁 ∈ ℕ₀)
36		eqid 2651	. . . . . . . . 9 ⊢ (Base‘𝑌) = (Base‘𝑌)
37	21, 36, 22	znzrhfo 19944	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ₀ → 𝐿:ℤ–onto→(Base‘𝑌))
38	35, 37	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝐿:ℤ–onto→(Base‘𝑌))
39		fof 6153	. . . . . . 7 ⊢ (𝐿:ℤ–onto→(Base‘𝑌) → 𝐿:ℤ⟶(Base‘𝑌))
40	38, 39	syl 17	. . . . . 6 ⊢ (𝜑 → 𝐿:ℤ⟶(Base‘𝑌))
41	40	feqmptd 6288	. . . . 5 ⊢ (𝜑 → 𝐿 = (𝑚 ∈ ℤ ↦ (𝐿‘𝑚)))
42	41	rneqd 5385	. . . 4 ⊢ (𝜑 → ran 𝐿 = ran (𝑚 ∈ ℤ ↦ (𝐿‘𝑚)))
43		forn 6156	. . . . 5 ⊢ (𝐿:ℤ–onto→(Base‘𝑌) → ran 𝐿 = (Base‘𝑌))
44	38, 43	syl 17	. . . 4 ⊢ (𝜑 → ran 𝐿 = (Base‘𝑌))
45	42, 44	eqtr3d 2687	. . 3 ⊢ (𝜑 → ran (𝑚 ∈ ℤ ↦ (𝐿‘𝑚)) = (Base‘𝑌))
46	45	feq2d 6069	. 2 ⊢ (𝜑 → (𝐹:ran (𝑚 ∈ ℤ ↦ (𝐿‘𝑚))⟶𝐵 ↔ 𝐹:(Base‘𝑌)⟶𝐵))
47	29, 46	mpbid 222	1 ⊢ (𝜑 → 𝐹:(Base‘𝑌)⟶𝐵)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 383 = wceq 1523 ∈ wcel 2030 {crab 2945 Vcvv 3231 ifcif 4119 ⟨cop 4216 ↦ cmpt 4762 ran crn 5144 Fun wfun 5920 ⟶wf 5922 –onto→wfo 5924 ‘cfv 5926 (class class class)co 6690 Fincfn 7997 0cc0 9974 ℕ₀cn0 11330 ℤcz 11415 #chash 13157 Basecbs 15904 Grpcgrp 17469 ._gcmg 17587 CycGrpccyg 18325 ℤRHomczrh 19896 ℤ/nℤczn 19899

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 ax-6 1945 ax-7 1981 ax-8 2032 ax-9 2039 ax-10 2059 ax-11 2074 ax-12 2087 ax-13 2282 ax-ext 2631 ax-rep 4804 ax-sep 4814 ax-nul 4822 ax-pow 4873 ax-pr 4936 ax-un 6991 ax-inf2 8576 ax-cnex 10030 ax-resscn 10031 ax-1cn 10032 ax-icn 10033 ax-addcl 10034 ax-addrcl 10035 ax-mulcl 10036 ax-mulrcl 10037 ax-mulcom 10038 ax-addass 10039 ax-mulass 10040 ax-distr 10041 ax-i2m1 10042 ax-1ne0 10043 ax-1rid 10044 ax-rnegex 10045 ax-rrecex 10046 ax-cnre 10047 ax-pre-lttri 10048 ax-pre-lttrn 10049 ax-pre-ltadd 10050 ax-pre-mulgt0 10051 ax-pre-sup 10052 ax-addf 10053 ax-mulf 10054

This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3or 1055 df-3an 1056 df-tru 1526 df-ex 1745 df-nf 1750 df-sb 1938 df-eu 2502 df-mo 2503 df-clab 2638 df-cleq 2644 df-clel 2647 df-nfc 2782 df-ne 2824 df-nel 2927 df-ral 2946 df-rex 2947 df-reu 2948 df-rmo 2949 df-rab 2950 df-v 3233 df-sbc 3469 df-csb 3567 df-dif 3610 df-un 3612 df-in 3614 df-ss 3621 df-pss 3623 df-nul 3949 df-if 4120 df-pw 4193 df-sn 4211 df-pr 4213 df-tp 4215 df-op 4217 df-uni 4469 df-int 4508 df-iun 4554 df-br 4686 df-opab 4746 df-mpt 4763 df-tr 4786 df-id 5053 df-eprel 5058 df-po 5064 df-so 5065 df-fr 5102 df-se 5103 df-we 5104 df-xp 5149 df-rel 5150 df-cnv 5151 df-co 5152 df-dm 5153 df-rn 5154 df-res 5155 df-ima 5156 df-pred 5718 df-ord 5764 df-on 5765 df-lim 5766 df-suc 5767 df-iota 5889 df-fun 5928 df-fn 5929 df-f 5930 df-f1 5931 df-fo 5932 df-f1o 5933 df-fv 5934 df-isom 5935 df-riota 6651 df-ov 6693 df-oprab 6694 df-mpt2 6695 df-om 7108 df-1st 7210 df-2nd 7211 df-tpos 7397 df-wrecs 7452 df-recs 7513 df-rdg 7551 df-1o 7605 df-oadd 7609 df-omul 7610 df-er 7787 df-ec 7789 df-qs 7793 df-map 7901 df-en 7998 df-dom 7999 df-sdom 8000 df-fin 8001 df-sup 8389 df-inf 8390 df-oi 8456 df-card 8803 df-acn 8806 df-pnf 10114 df-mnf 10115 df-xr 10116 df-ltxr 10117 df-le 10118 df-sub 10306 df-neg 10307 df-div 10723 df-nn 11059 df-2 11117 df-3 11118 df-4 11119 df-5 11120 df-6 11121 df-7 11122 df-8 11123 df-9 11124 df-n0 11331 df-z 11416 df-dec 11532 df-uz 11726 df-rp 11871 df-fz 12365 df-fl 12633 df-mod 12709 df-seq 12842 df-exp 12901 df-hash 13158 df-cj 13883 df-re 13884 df-im 13885 df-sqrt 14019 df-abs 14020 df-dvds 15028 df-struct 15906 df-ndx 15907 df-slot 15908 df-base 15910 df-sets 15911 df-ress 15912 df-plusg 16001 df-mulr 16002 df-starv 16003 df-sca 16004 df-vsca 16005 df-ip 16006 df-tset 16007 df-ple 16008 df-ds 16011 df-unif 16012 df-0g 16149 df-imas 16215 df-qus 16216 df-mgm 17289 df-sgrp 17331 df-mnd 17342 df-mhm 17382 df-grp 17472 df-minusg 17473 df-sbg 17474 df-mulg 17588 df-subg 17638 df-nsg 17639 df-eqg 17640 df-ghm 17705 df-od 17994 df-cmn 18241 df-abl 18242 df-cyg 18326 df-mgp 18536 df-ur 18548 df-ring 18595 df-cring 18596 df-oppr 18669 df-dvdsr 18687 df-rnghom 18763 df-subrg 18826 df-lmod 18913 df-lss 18981 df-lsp 19020 df-sra 19220 df-rgmod 19221 df-lidl 19222 df-rsp 19223 df-2idl 19280 df-cnfld 19795 df-zring 19867 df-zrh 19900 df-zn 19903

This theorem is referenced by: cygznlem2 19965 cygznlem3 19966

W3C validator