dchrptlem1 - Metamath Proof Explorer

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

Theorem dchrptlem1 27501

Description: Lemma for dchrpt 27504. (Contributed by Mario Carneiro, 28-Apr-2016.)

**Hypotheses**
Ref	Expression
dchrpt.g	⊢ 𝐺 = (DChr‘𝑁)
dchrpt.z	⊢ 𝑍 = (ℤ/nℤ‘𝑁)
dchrpt.d	⊢ 𝐷 = (Base‘𝐺)
dchrpt.b	⊢ 𝐵 = (Base‘𝑍)
dchrpt.1	⊢ 1 = (1_r‘𝑍)
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 𝑆) = 𝑈)
dchrpt.p	⊢ 𝑃 = (𝐻dProj𝑆)
dchrpt.o	⊢ 𝑂 = (od‘𝐻)
dchrpt.t	⊢ 𝑇 = (-1↑_𝑐(2 / (𝑂‘(𝑊‘𝐼))))
dchrpt.i	⊢ (𝜑 → 𝐼 ∈ dom 𝑊)
dchrpt.4	⊢ (𝜑 → ((𝑃‘𝐼)‘𝐴) ≠ 1 )
dchrpt.5	⊢ 𝑋 = (𝑢 ∈ 𝑈 ↦ (℩ℎ∃𝑚 ∈ ℤ (((𝑃‘𝐼)‘𝑢) = (𝑚 · (𝑊‘𝐼)) ∧ ℎ = (𝑇↑𝑚))))

**Assertion**
Ref	Expression
dchrptlem1	⊢ (((𝜑 ∧ 𝐶 ∈ 𝑈) ∧ (𝑀 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐶) = (𝑀 · (𝑊‘𝐼)))) → (𝑋‘𝐶) = (𝑇↑𝑀))

Distinct variable groups: ℎ,𝑘,𝑚,𝑛, 1 𝑢,ℎ,𝐴,𝑘,𝑚,𝑛 ℎ,𝐼,𝑘,𝑚,𝑢 𝐶,ℎ,𝑚,𝑢 ℎ,𝐻,𝑘,𝑚,𝑛,𝑢 ℎ,𝑊,𝑘,𝑚,𝑛,𝑢 · ,ℎ,𝑘,𝑚,𝑛,𝑢 𝑃,ℎ,𝑚,𝑢 𝑆,ℎ,𝑘,𝑚,𝑛,𝑢 ℎ,𝑍,𝑘,𝑚,𝑛,𝑢 ℎ,𝑀,𝑚 𝜑,ℎ,𝑘,𝑚,𝑛 𝑇,ℎ,𝑚,𝑢 𝑈,ℎ,𝑚,𝑢 Allowed substitution hints: 𝜑(𝑢) 𝐵(𝑢, ℎ, 𝑘, 𝑚, 𝑛) 𝐶(𝑘, 𝑛) 𝐷(𝑢, ℎ, 𝑘, 𝑚, 𝑛) 𝑃(𝑘, 𝑛) 𝑇(𝑘, 𝑛) 𝑈(𝑘, 𝑛) 1 (𝑢) 𝐺(𝑢, ℎ, 𝑘, 𝑚, 𝑛) 𝐼(𝑛) 𝑀(𝑢, 𝑘, 𝑛) 𝑁(𝑢, ℎ, 𝑘, 𝑚, 𝑛) 𝑂(𝑢, ℎ, 𝑘, 𝑚, 𝑛) 𝑋(𝑢, ℎ, 𝑘, 𝑚, 𝑛)

**Proof of Theorem dchrptlem1**
Step	Hyp	Ref	Expression
1		fveqeq2 6891	. . . . . . 7 ⊢ (𝑢 = 𝐶 → (((𝑃‘𝐼)‘𝑢) = (𝑚 · (𝑊‘𝐼)) ↔ ((𝑃‘𝐼)‘𝐶) = (𝑚 · (𝑊‘𝐼))))
2	1	anbi1d 643	. . . . . 6 ⊢ (𝑢 = 𝐶 → ((((𝑃‘𝐼)‘𝑢) = (𝑚 · (𝑊‘𝐼)) ∧ ℎ = (𝑇↑𝑚)) ↔ (((𝑃‘𝐼)‘𝐶) = (𝑚 · (𝑊‘𝐼)) ∧ ℎ = (𝑇↑𝑚))))
3	2	rexbidv 3188	. . . . 5 ⊢ (𝑢 = 𝐶 → (∃𝑚 ∈ ℤ (((𝑃‘𝐼)‘𝑢) = (𝑚 · (𝑊‘𝐼)) ∧ ℎ = (𝑇↑𝑚)) ↔ ∃𝑚 ∈ ℤ (((𝑃‘𝐼)‘𝐶) = (𝑚 · (𝑊‘𝐼)) ∧ ℎ = (𝑇↑𝑚))))
4	3	iotabidv 6521	. . . 4 ⊢ (𝑢 = 𝐶 → (℩ℎ∃𝑚 ∈ ℤ (((𝑃‘𝐼)‘𝑢) = (𝑚 · (𝑊‘𝐼)) ∧ ℎ = (𝑇↑𝑚))) = (℩ℎ∃𝑚 ∈ ℤ (((𝑃‘𝐼)‘𝐶) = (𝑚 · (𝑊‘𝐼)) ∧ ℎ = (𝑇↑𝑚))))
5		dchrpt.5	. . . 4 ⊢ 𝑋 = (𝑢 ∈ 𝑈 ↦ (℩ℎ∃𝑚 ∈ ℤ (((𝑃‘𝐼)‘𝑢) = (𝑚 · (𝑊‘𝐼)) ∧ ℎ = (𝑇↑𝑚))))
6		iotaex 6513	. . . 4 ⊢ (℩ℎ∃𝑚 ∈ ℤ (((𝑃‘𝐼)‘𝑢) = (𝑚 · (𝑊‘𝐼)) ∧ ℎ = (𝑇↑𝑚))) ∈ V
7	4, 5, 6	fvmpt3i 6996	. . 3 ⊢ (𝐶 ∈ 𝑈 → (𝑋‘𝐶) = (℩ℎ∃𝑚 ∈ ℤ (((𝑃‘𝐼)‘𝐶) = (𝑚 · (𝑊‘𝐼)) ∧ ℎ = (𝑇↑𝑚))))
8	7	ad2antlr 740	. 2 ⊢ (((𝜑 ∧ 𝐶 ∈ 𝑈) ∧ (𝑀 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐶) = (𝑀 · (𝑊‘𝐼)))) → (𝑋‘𝐶) = (℩ℎ∃𝑚 ∈ ℤ (((𝑃‘𝐼)‘𝐶) = (𝑚 · (𝑊‘𝐼)) ∧ ℎ = (𝑇↑𝑚))))
9		ovex 7449	. . 3 ⊢ (𝑇↑𝑀) ∈ V
10		simpr 490	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝐶 ∈ 𝑈) ∧ (𝑀 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐶) = (𝑀 · (𝑊‘𝐼)))) ∧ 𝑚 ∈ ℤ) ∧ ((𝑃‘𝐼)‘𝐶) = (𝑚 · (𝑊‘𝐼))) → ((𝑃‘𝐼)‘𝐶) = (𝑚 · (𝑊‘𝐼)))
11		simpllr 788	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝐶 ∈ 𝑈) ∧ (𝑀 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐶) = (𝑀 · (𝑊‘𝐼)))) ∧ 𝑚 ∈ ℤ) ∧ ((𝑃‘𝐼)‘𝐶) = (𝑚 · (𝑊‘𝐼))) → (𝑀 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐶) = (𝑀 · (𝑊‘𝐼))))
12	11	simprd 501	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝐶 ∈ 𝑈) ∧ (𝑀 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐶) = (𝑀 · (𝑊‘𝐼)))) ∧ 𝑚 ∈ ℤ) ∧ ((𝑃‘𝐼)‘𝐶) = (𝑚 · (𝑊‘𝐼))) → ((𝑃‘𝐼)‘𝐶) = (𝑀 · (𝑊‘𝐼)))
13	10, 12	eqtr3d 2799	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝐶 ∈ 𝑈) ∧ (𝑀 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐶) = (𝑀 · (𝑊‘𝐼)))) ∧ 𝑚 ∈ ℤ) ∧ ((𝑃‘𝐼)‘𝐶) = (𝑚 · (𝑊‘𝐼))) → (𝑚 · (𝑊‘𝐼)) = (𝑀 · (𝑊‘𝐼)))
14		simp-4l 795	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝐶 ∈ 𝑈) ∧ (𝑀 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐶) = (𝑀 · (𝑊‘𝐼)))) ∧ 𝑚 ∈ ℤ) ∧ ((𝑃‘𝐼)‘𝐶) = (𝑚 · (𝑊‘𝐼))) → 𝜑)
15		simplr 781	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝐶 ∈ 𝑈) ∧ (𝑀 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐶) = (𝑀 · (𝑊‘𝐼)))) ∧ 𝑚 ∈ ℤ) ∧ ((𝑃‘𝐼)‘𝐶) = (𝑚 · (𝑊‘𝐼))) → 𝑚 ∈ ℤ)
16	11	simpld 500	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝐶 ∈ 𝑈) ∧ (𝑀 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐶) = (𝑀 · (𝑊‘𝐼)))) ∧ 𝑚 ∈ ℤ) ∧ ((𝑃‘𝐼)‘𝐶) = (𝑚 · (𝑊‘𝐼))) → 𝑀 ∈ ℤ)
17		dchrpt.n	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑁 ∈ ℕ)
18	17	nnnn0d 12592	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑁 ∈ ℕ₀)
19		dchrpt.z	. . . . . . . . . . . . . . . . 17 ⊢ 𝑍 = (ℤ/nℤ‘𝑁)
20	19	zncrng 21761	. . . . . . . . . . . . . . . 16 ⊢ (𝑁 ∈ ℕ₀ → 𝑍 ∈ CRing)
21		crngring 20388	. . . . . . . . . . . . . . . 16 ⊢ (𝑍 ∈ CRing → 𝑍 ∈ Ring)
22		dchrpt.u	. . . . . . . . . . . . . . . . 17 ⊢ 𝑈 = (Unit‘𝑍)
23		dchrpt.h	. . . . . . . . . . . . . . . . 17 ⊢ 𝐻 = ((mulGrp‘𝑍) ↾_s 𝑈)
24	22, 23	unitgrp 20528	. . . . . . . . . . . . . . . 16 ⊢ (𝑍 ∈ Ring → 𝐻 ∈ Grp)
25	18, 20, 21, 24	4syl 20	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐻 ∈ Grp)
26	25	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑀 ∈ ℤ)) → 𝐻 ∈ Grp)
27		dchrpt.w	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑊 ∈ Word 𝑈)
28		wrdf 14585	. . . . . . . . . . . . . . . . 17 ⊢ (𝑊 ∈ Word 𝑈 → 𝑊:(0..^(♯‘𝑊))⟶𝑈)
29	27, 28	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑊:(0..^(♯‘𝑊))⟶𝑈)
30		dchrpt.i	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐼 ∈ dom 𝑊)
31	29	fdmd 6717	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → dom 𝑊 = (0..^(♯‘𝑊)))
32	30, 31	eleqtrd 2864	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐼 ∈ (0..^(♯‘𝑊)))
33	29, 32	ffvelcdmd 7081	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑊‘𝐼) ∈ 𝑈)
34	33	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑀 ∈ ℤ)) → (𝑊‘𝐼) ∈ 𝑈)
35		simprl 783	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑀 ∈ ℤ)) → 𝑚 ∈ ℤ)
36		simprr 785	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑀 ∈ ℤ)) → 𝑀 ∈ ℤ)
37	22, 23	unitgrpbas 20527	. . . . . . . . . . . . . . 15 ⊢ 𝑈 = (Base‘𝐻)
38		dchrpt.o	. . . . . . . . . . . . . . 15 ⊢ 𝑂 = (od‘𝐻)
39		dchrpt.m	. . . . . . . . . . . . . . 15 ⊢ · = (._g‘𝐻)
40		eqid 2762	. . . . . . . . . . . . . . 15 ⊢ (0_g‘𝐻) = (0_g‘𝐻)
41	37, 38, 39, 40	odcong 19680	. . . . . . . . . . . . . 14 ⊢ ((𝐻 ∈ Grp ∧ (𝑊‘𝐼) ∈ 𝑈 ∧ (𝑚 ∈ ℤ ∧ 𝑀 ∈ ℤ)) → ((𝑂‘(𝑊‘𝐼)) ∥ (𝑚 − 𝑀) ↔ (𝑚 · (𝑊‘𝐼)) = (𝑀 · (𝑊‘𝐼))))
42	26, 34, 35, 36, 41	syl112anc 1401	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑀 ∈ ℤ)) → ((𝑂‘(𝑊‘𝐼)) ∥ (𝑚 − 𝑀) ↔ (𝑚 · (𝑊‘𝐼)) = (𝑀 · (𝑊‘𝐼))))
43		dchrpt.t	. . . . . . . . . . . . . . . . 17 ⊢ 𝑇 = (-1↑_𝑐(2 / (𝑂‘(𝑊‘𝐼))))
44		neg1cn 12230	. . . . . . . . . . . . . . . . . 18 ⊢ -1 ∈ ℂ
45		2re 12342	. . . . . . . . . . . . . . . . . . . 20 ⊢ 2 ∈ ℝ
46		dchrpt.b	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 𝐵 = (Base‘𝑍)
47	19, 46	znfi 21776	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑁 ∈ ℕ → 𝐵 ∈ Fin)
48	17, 47	syl 18	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝐵 ∈ Fin)
49	46, 22	unitss 20521	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝑈 ⊆ 𝐵
50		ssfi 9170	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐵 ∈ Fin ∧ 𝑈 ⊆ 𝐵) → 𝑈 ∈ Fin)
51	48, 49, 50	sylancl 598	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝑈 ∈ Fin)
52	37, 38	odcl2 19696	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐻 ∈ Grp ∧ 𝑈 ∈ Fin ∧ (𝑊‘𝐼) ∈ 𝑈) → (𝑂‘(𝑊‘𝐼)) ∈ ℕ)
53	25, 51, 33, 52	syl3anc 1398	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑂‘(𝑊‘𝐼)) ∈ ℕ)
54	53	ad2antrr 739	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑂‘(𝑊‘𝐼)) ∥ (𝑚 − 𝑀)) → (𝑂‘(𝑊‘𝐼)) ∈ ℕ)
55		nndivre 12304	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((2 ∈ ℝ ∧ (𝑂‘(𝑊‘𝐼)) ∈ ℕ) → (2 / (𝑂‘(𝑊‘𝐼))) ∈ ℝ)
56	45, 54, 55	sylancr 599	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑂‘(𝑊‘𝐼)) ∥ (𝑚 − 𝑀)) → (2 / (𝑂‘(𝑊‘𝐼))) ∈ ℝ)
57	56	recnd 11264	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑂‘(𝑊‘𝐼)) ∥ (𝑚 − 𝑀)) → (2 / (𝑂‘(𝑊‘𝐼))) ∈ ℂ)
58		cxpcl 26912	. . . . . . . . . . . . . . . . . 18 ⊢ ((-1 ∈ ℂ ∧ (2 / (𝑂‘(𝑊‘𝐼))) ∈ ℂ) → (-1↑_𝑐(2 / (𝑂‘(𝑊‘𝐼)))) ∈ ℂ)
59	44, 57, 58	sylancr 599	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑂‘(𝑊‘𝐼)) ∥ (𝑚 − 𝑀)) → (-1↑_𝑐(2 / (𝑂‘(𝑊‘𝐼)))) ∈ ℂ)
60	43, 59	eqeltrid 2866	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑂‘(𝑊‘𝐼)) ∥ (𝑚 − 𝑀)) → 𝑇 ∈ ℂ)
61	44	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑂‘(𝑊‘𝐼)) ∥ (𝑚 − 𝑀)) → -1 ∈ ℂ)
62		neg1ne0 12232	. . . . . . . . . . . . . . . . . . 19 ⊢ -1 ≠ 0
63	62	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑂‘(𝑊‘𝐼)) ∥ (𝑚 − 𝑀)) → -1 ≠ 0)
64	61, 63, 57	cxpne0d 26951	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑂‘(𝑊‘𝐼)) ∥ (𝑚 − 𝑀)) → (-1↑_𝑐(2 / (𝑂‘(𝑊‘𝐼)))) ≠ 0)
65	43	neeq1i 3021	. . . . . . . . . . . . . . . . 17 ⊢ (𝑇 ≠ 0 ↔ (-1↑_𝑐(2 / (𝑂‘(𝑊‘𝐼)))) ≠ 0)
66	64, 65	sylibr 237	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑂‘(𝑊‘𝐼)) ∥ (𝑚 − 𝑀)) → 𝑇 ≠ 0)
67		zsubcl 12663	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑚 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑚 − 𝑀) ∈ ℤ)
68	67	ad2antlr 740	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑂‘(𝑊‘𝐼)) ∥ (𝑚 − 𝑀)) → (𝑚 − 𝑀) ∈ ℤ)
69	36	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑂‘(𝑊‘𝐼)) ∥ (𝑚 − 𝑀)) → 𝑀 ∈ ℤ)
70		expaddz 14172	. . . . . . . . . . . . . . . 16 ⊢ (((𝑇 ∈ ℂ ∧ 𝑇 ≠ 0) ∧ ((𝑚 − 𝑀) ∈ ℤ ∧ 𝑀 ∈ ℤ)) → (𝑇↑((𝑚 − 𝑀) + 𝑀)) = ((𝑇↑(𝑚 − 𝑀)) · (𝑇↑𝑀)))
71	60, 66, 68, 69, 70	syl22anc 852	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑂‘(𝑊‘𝐼)) ∥ (𝑚 − 𝑀)) → (𝑇↑((𝑚 − 𝑀) + 𝑀)) = ((𝑇↑(𝑚 − 𝑀)) · (𝑇↑𝑀)))
72	35	adantr 486	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑂‘(𝑊‘𝐼)) ∥ (𝑚 − 𝑀)) → 𝑚 ∈ ℤ)
73	72	zcnd 12729	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑂‘(𝑊‘𝐼)) ∥ (𝑚 − 𝑀)) → 𝑚 ∈ ℂ)
74	69	zcnd 12729	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑂‘(𝑊‘𝐼)) ∥ (𝑚 − 𝑀)) → 𝑀 ∈ ℂ)
75	73, 74	npcand 11600	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑂‘(𝑊‘𝐼)) ∥ (𝑚 − 𝑀)) → ((𝑚 − 𝑀) + 𝑀) = 𝑚)
76	75	oveq2d 7432	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑂‘(𝑊‘𝐼)) ∥ (𝑚 − 𝑀)) → (𝑇↑((𝑚 − 𝑀) + 𝑀)) = (𝑇↑𝑚))
77	43	oveq1i 7426	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑇↑(𝑚 − 𝑀)) = ((-1↑_𝑐(2 / (𝑂‘(𝑊‘𝐼))))↑(𝑚 − 𝑀))
78		root1eq1 26993	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑂‘(𝑊‘𝐼)) ∈ ℕ ∧ (𝑚 − 𝑀) ∈ ℤ) → (((-1↑_𝑐(2 / (𝑂‘(𝑊‘𝐼))))↑(𝑚 − 𝑀)) = 1 ↔ (𝑂‘(𝑊‘𝐼)) ∥ (𝑚 − 𝑀)))
79	53, 67, 78	syl2an 608	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑀 ∈ ℤ)) → (((-1↑_𝑐(2 / (𝑂‘(𝑊‘𝐼))))↑(𝑚 − 𝑀)) = 1 ↔ (𝑂‘(𝑊‘𝐼)) ∥ (𝑚 − 𝑀)))
80	79	biimpar 483	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑂‘(𝑊‘𝐼)) ∥ (𝑚 − 𝑀)) → ((-1↑_𝑐(2 / (𝑂‘(𝑊‘𝐼))))↑(𝑚 − 𝑀)) = 1)
81	77, 80	eqtrid 2809	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑂‘(𝑊‘𝐼)) ∥ (𝑚 − 𝑀)) → (𝑇↑(𝑚 − 𝑀)) = 1)
82	81	oveq1d 7431	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑂‘(𝑊‘𝐼)) ∥ (𝑚 − 𝑀)) → ((𝑇↑(𝑚 − 𝑀)) · (𝑇↑𝑀)) = (1 · (𝑇↑𝑀)))
83	60, 66, 69	expclzd 14217	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑂‘(𝑊‘𝐼)) ∥ (𝑚 − 𝑀)) → (𝑇↑𝑀) ∈ ℂ)
84	83	mullidd 11254	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑂‘(𝑊‘𝐼)) ∥ (𝑚 − 𝑀)) → (1 · (𝑇↑𝑀)) = (𝑇↑𝑀))
85	82, 84	eqtrd 2797	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑂‘(𝑊‘𝐼)) ∥ (𝑚 − 𝑀)) → ((𝑇↑(𝑚 − 𝑀)) · (𝑇↑𝑀)) = (𝑇↑𝑀))
86	71, 76, 85	3eqtr3d 2805	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑂‘(𝑊‘𝐼)) ∥ (𝑚 − 𝑀)) → (𝑇↑𝑚) = (𝑇↑𝑀))
87	86	ex 418	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑀 ∈ ℤ)) → ((𝑂‘(𝑊‘𝐼)) ∥ (𝑚 − 𝑀) → (𝑇↑𝑚) = (𝑇↑𝑀)))
88	42, 87	sylbird 263	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑀 ∈ ℤ)) → ((𝑚 · (𝑊‘𝐼)) = (𝑀 · (𝑊‘𝐼)) → (𝑇↑𝑚) = (𝑇↑𝑀)))
89	14, 15, 16, 88	syl12anc 850	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝐶 ∈ 𝑈) ∧ (𝑀 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐶) = (𝑀 · (𝑊‘𝐼)))) ∧ 𝑚 ∈ ℤ) ∧ ((𝑃‘𝐼)‘𝐶) = (𝑚 · (𝑊‘𝐼))) → ((𝑚 · (𝑊‘𝐼)) = (𝑀 · (𝑊‘𝐼)) → (𝑇↑𝑚) = (𝑇↑𝑀)))
90	13, 89	mpd 16	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝐶 ∈ 𝑈) ∧ (𝑀 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐶) = (𝑀 · (𝑊‘𝐼)))) ∧ 𝑚 ∈ ℤ) ∧ ((𝑃‘𝐼)‘𝐶) = (𝑚 · (𝑊‘𝐼))) → (𝑇↑𝑚) = (𝑇↑𝑀))
91	90	eqeq2d 2773	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝐶 ∈ 𝑈) ∧ (𝑀 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐶) = (𝑀 · (𝑊‘𝐼)))) ∧ 𝑚 ∈ ℤ) ∧ ((𝑃‘𝐼)‘𝐶) = (𝑚 · (𝑊‘𝐼))) → (ℎ = (𝑇↑𝑚) ↔ ℎ = (𝑇↑𝑀)))
92	91	biimpd 232	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝐶 ∈ 𝑈) ∧ (𝑀 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐶) = (𝑀 · (𝑊‘𝐼)))) ∧ 𝑚 ∈ ℤ) ∧ ((𝑃‘𝐼)‘𝐶) = (𝑚 · (𝑊‘𝐼))) → (ℎ = (𝑇↑𝑚) → ℎ = (𝑇↑𝑀)))
93	92	expimpd 459	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝐶 ∈ 𝑈) ∧ (𝑀 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐶) = (𝑀 · (𝑊‘𝐼)))) ∧ 𝑚 ∈ ℤ) → ((((𝑃‘𝐼)‘𝐶) = (𝑚 · (𝑊‘𝐼)) ∧ ℎ = (𝑇↑𝑚)) → ℎ = (𝑇↑𝑀)))
94	93	rexlimdva 3165	. . . . . 6 ⊢ (((𝜑 ∧ 𝐶 ∈ 𝑈) ∧ (𝑀 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐶) = (𝑀 · (𝑊‘𝐼)))) → (∃𝑚 ∈ ℤ (((𝑃‘𝐼)‘𝐶) = (𝑚 · (𝑊‘𝐼)) ∧ ℎ = (𝑇↑𝑚)) → ℎ = (𝑇↑𝑀)))
95		oveq1 7423	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑀 → (𝑚 · (𝑊‘𝐼)) = (𝑀 · (𝑊‘𝐼)))
96	95	eqeq2d 2773	. . . . . . . . . 10 ⊢ (𝑚 = 𝑀 → (((𝑃‘𝐼)‘𝐶) = (𝑚 · (𝑊‘𝐼)) ↔ ((𝑃‘𝐼)‘𝐶) = (𝑀 · (𝑊‘𝐼))))
97		oveq2 7424	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑀 → (𝑇↑𝑚) = (𝑇↑𝑀))
98	97	eqeq2d 2773	. . . . . . . . . 10 ⊢ (𝑚 = 𝑀 → (ℎ = (𝑇↑𝑚) ↔ ℎ = (𝑇↑𝑀)))
99	96, 98	anbi12d 644	. . . . . . . . 9 ⊢ (𝑚 = 𝑀 → ((((𝑃‘𝐼)‘𝐶) = (𝑚 · (𝑊‘𝐼)) ∧ ℎ = (𝑇↑𝑚)) ↔ (((𝑃‘𝐼)‘𝐶) = (𝑀 · (𝑊‘𝐼)) ∧ ℎ = (𝑇↑𝑀))))
100	99	rspcev 3579	. . . . . . . 8 ⊢ ((𝑀 ∈ ℤ ∧ (((𝑃‘𝐼)‘𝐶) = (𝑀 · (𝑊‘𝐼)) ∧ ℎ = (𝑇↑𝑀))) → ∃𝑚 ∈ ℤ (((𝑃‘𝐼)‘𝐶) = (𝑚 · (𝑊‘𝐼)) ∧ ℎ = (𝑇↑𝑚)))
101	100	expr 462	. . . . . . 7 ⊢ ((𝑀 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐶) = (𝑀 · (𝑊‘𝐼))) → (ℎ = (𝑇↑𝑀) → ∃𝑚 ∈ ℤ (((𝑃‘𝐼)‘𝐶) = (𝑚 · (𝑊‘𝐼)) ∧ ℎ = (𝑇↑𝑚))))
102	101	adantl 487	. . . . . 6 ⊢ (((𝜑 ∧ 𝐶 ∈ 𝑈) ∧ (𝑀 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐶) = (𝑀 · (𝑊‘𝐼)))) → (ℎ = (𝑇↑𝑀) → ∃𝑚 ∈ ℤ (((𝑃‘𝐼)‘𝐶) = (𝑚 · (𝑊‘𝐼)) ∧ ℎ = (𝑇↑𝑚))))
103	94, 102	impbid 215	. . . . 5 ⊢ (((𝜑 ∧ 𝐶 ∈ 𝑈) ∧ (𝑀 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐶) = (𝑀 · (𝑊‘𝐼)))) → (∃𝑚 ∈ ℤ (((𝑃‘𝐼)‘𝐶) = (𝑚 · (𝑊‘𝐼)) ∧ ℎ = (𝑇↑𝑚)) ↔ ℎ = (𝑇↑𝑀)))
104	103	adantr 486	. . . 4 ⊢ ((((𝜑 ∧ 𝐶 ∈ 𝑈) ∧ (𝑀 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐶) = (𝑀 · (𝑊‘𝐼)))) ∧ (𝑇↑𝑀) ∈ V) → (∃𝑚 ∈ ℤ (((𝑃‘𝐼)‘𝐶) = (𝑚 · (𝑊‘𝐼)) ∧ ℎ = (𝑇↑𝑚)) ↔ ℎ = (𝑇↑𝑀)))
105	104	iota5 6520	. . 3 ⊢ ((((𝜑 ∧ 𝐶 ∈ 𝑈) ∧ (𝑀 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐶) = (𝑀 · (𝑊‘𝐼)))) ∧ (𝑇↑𝑀) ∈ V) → (℩ℎ∃𝑚 ∈ ℤ (((𝑃‘𝐼)‘𝐶) = (𝑚 · (𝑊‘𝐼)) ∧ ℎ = (𝑇↑𝑚))) = (𝑇↑𝑀))
106	9, 105	mpan2 704	. 2 ⊢ (((𝜑 ∧ 𝐶 ∈ 𝑈) ∧ (𝑀 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐶) = (𝑀 · (𝑊‘𝐼)))) → (℩ℎ∃𝑚 ∈ ℤ (((𝑃‘𝐼)‘𝐶) = (𝑚 · (𝑊‘𝐼)) ∧ ℎ = (𝑇↑𝑚))) = (𝑇↑𝑀))
107	8, 106	eqtrd 2797	1 ⊢ (((𝜑 ∧ 𝐶 ∈ 𝑈) ∧ (𝑀 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐶) = (𝑀 · (𝑊‘𝐼)))) → (𝑋‘𝐶) = (𝑇↑𝑀))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 = wceq 1570 ∈ wcel 2145 ≠ wne 2957 ∃wrex 3088 Vcvv 3453 ⊆ wss 3902 class class class wbr 5107 ↦ cmpt 5190 dom cdm 5659 ran crn 5660 ℩cio 6491 ⟶wf 6533 ‘cfv 6537 (class class class)co 7416 Fincfn 8955 ℂcc 11125 ℝcr 11126 0cc0 11127 1c1 11128 + caddc 11130 · cmul 11132 − cmin 11468 -cneg 11469 / cdiv 11898 ℕcn 12260 2c2 12322 ℕ₀cn0 12531 ℤcz 12618 ..^cfzo 13711 ↑cexp 14127 ♯chash 14396 Word cword 14580 ∥ cdvds 16346 Basecbs 17305 ↾_s cress 17326 0_gc0g 17528 Grpcgrp 19061 ._gcmg 19194 odcod 19655 DProd cdprd 20126 dProjcdpj 20127 mulGrpcmgp 20277 1_rcur 20324 Ringcrg 20376 CRingccrg 20377 Unitcui 20500 ℤ/nℤczn 21719 ↑_𝑐ccxp 26793 DChrcdchr 27469

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2215 ax-ext 2734 ax-rep 5236 ax-sep 5255 ax-nul 5267 ax-pow 5334 ax-pr 5402 ax-un 7739 ax-inf2 9623 ax-cnex 11183 ax-resscn 11184 ax-1cn 11185 ax-icn 11186 ax-addcl 11187 ax-addrcl 11188 ax-mulcl 11189 ax-mulrcl 11190 ax-mulcom 11191 ax-addass 11192 ax-mulass 11193 ax-distr 11194 ax-i2m1 11195 ax-1ne0 11196 ax-1rid 11197 ax-rnegex 11198 ax-rrecex 11199 ax-cnre 11200 ax-pre-lttri 11201 ax-pre-lttrn 11202 ax-pre-ltadd 11203 ax-pre-mulgt0 11204 ax-pre-sup 11205 ax-addf 11206 ax-mulf 11207

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2566 df-eu 2596 df-clab 2741 df-cleq 2754 df-clel 2837 df-nfc 2911 df-ne 2958 df-nel 3064 df-ral 3079 df-rex 3089 df-rmo 3367 df-reu 3368 df-rab 3415 df-v 3455 df-sbc 3743 df-csb 3851 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-pss 3922 df-nul 4283 df-if 4486 df-pw 4562 df-sn 4588 df-pr 4590 df-tp 4592 df-op 4594 df-uni 4871 df-int 4911 df-iun 4956 df-iin 4957 df-br 5108 df-opab 5172 df-mpt 5191 df-tr 5217 df-id 5554 df-eprel 5559 df-po 5567 df-so 5568 df-fr 5612 df-se 5613 df-we 5614 df-xp 5665 df-rel 5666 df-cnv 5667 df-co 5668 df-dm 5669 df-rn 5670 df-res 5671 df-ima 5672 df-pred 6303 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6493 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-isom 6546 df-riota 7373 df-ov 7419 df-oprab 7420 df-mpo 7421 df-of 7681 df-om 7866 df-1st 7989 df-2nd 7990 df-supp 8162 df-tpos 8227 df-frecs 8283 df-wrecs 8314 df-recs 8363 df-rdg 8402 df-1o 8458 df-2o 8459 df-oadd 8462 df-omul 8463 df-er 8699 df-ec 8701 df-qs 8705 df-map 8831 df-pm 8832 df-ixp 8908 df-en 8956 df-dom 8957 df-sdom 8958 df-fin 8959 df-fsupp 9335 df-fi 9384 df-sup 9415 df-inf 9416 df-oi 9485 df-card 9947 df-acn 9950 df-pnf 11272 df-mnf 11273 df-xr 11274 df-ltxr 11275 df-le 11276 df-sub 11470 df-neg 11471 df-div 11899 df-nn 12261 df-2 12330 df-3 12331 df-4 12332 df-5 12333 df-6 12334 df-7 12335 df-8 12336 df-9 12337 df-n0 12532 df-z 12619 df-dec 12740 df-uz 12891 df-q 13001 df-rp 13045 df-xneg 13165 df-xadd 13166 df-xmul 13167 df-ioo 13404 df-ioc 13405 df-ico 13406 df-icc 13407 df-fz 13564 df-fzo 13712 df-fl 13855 df-mod 13933 df-seq 14068 df-exp 14128 df-fac 14340 df-bc 14369 df-hash 14397 df-word 14581 df-shft 15142 df-cj 15188 df-re 15189 df-im 15190 df-sqrt 15324 df-abs 15325 df-limsup 15560 df-clim 15577 df-rlim 15578 df-sum 15776 df-ef 16157 df-sin 16159 df-cos 16160 df-pi 16162 df-dvds 16347 df-struct 17243 df-sets 17260 df-slot 17278 df-ndx 17290 df-base 17306 df-ress 17327 df-plusg 17359 df-mulr 17360 df-starv 17361 df-sca 17362 df-vsca 17363 df-ip 17364 df-tset 17365 df-ple 17366 df-ds 17368 df-unif 17369 df-hom 17370 df-cco 17371 df-rest 17511 df-topn 17512 df-0g 17530 df-gsum 17531 df-topgen 17532 df-pt 17533 df-prds 17536 df-xrs 17592 df-qtop 17597 df-imas 17598 df-qus 17599 df-xps 17600 df-mre 17674 df-mrc 17675 df-acs 17677 df-mgm 18734 df-sgrp 18825 df-mnd 18841 df-mhm 18895 df-submnd 18896 df-grp 19064 df-minusg 19065 df-sbg 19066 df-mulg 19195 df-subg 19250 df-nsg 19251 df-eqg 19252 df-ghm 19345 df-cntz 19448 df-od 19659 df-cmn 19913 df-abl 19914 df-mgp 20278 df-rng 20292 df-ur 20325 df-ring 20378 df-cring 20379 df-oppr 20482 df-dvdsr 20502 df-unit 20503 df-rhm 20617 df-subrng 20712 df-subrg 20736 df-lmod 21050 df-lss 21120 df-lsp 21160 df-sra 21361 df-rgmod 21362 df-lidl 21399 df-rsp 21400 df-2idl 21456 df-psmet 21581 df-xmet 21582 df-met 21583 df-bl 21584 df-mopn 21585 df-fbas 21586 df-fg 21587 df-cnfld 21590 df-zring 21664 df-zrh 21720 df-zn 21723 df-top 23123 df-topon 23140 df-topsp 23162 df-bases 23175 df-cld 23248 df-ntr 23249 df-cls 23250 df-nei 23327 df-lp 23365 df-perf 23366 df-cn 23456 df-cnp 23457 df-haus 23544 df-tx 23792 df-hmeo 23985 df-fil 24076 df-fm 24168 df-flim 24169 df-flf 24170 df-xms 24550 df-ms 24551 df-tms 24552 df-cncf 25110 df-limc 26098 df-dv 26099 df-log 26794 df-cxp 26795

This theorem is used by: dchrptlem2 27502

W3C validator