Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  cycpmconjslem2 Structured version   Visualization version   GIF version

Theorem cycpmconjslem2 32782
Description: Lemma for cycpmconjs 32783. (Contributed by Thierry Arnoux, 14-Oct-2023.)
Hypotheses
Ref Expression
cycpmconjs.c 𝐶 = (𝑀 “ (♯ “ {𝑃}))
cycpmconjs.s 𝑆 = (SymGrp‘𝐷)
cycpmconjs.n 𝑁 = (♯‘𝐷)
cycpmconjs.m 𝑀 = (toCyc‘𝐷)
cycpmconjs.b 𝐵 = (Base‘𝑆)
cycpmconjs.a + = (+g𝑆)
cycpmconjs.l = (-g𝑆)
cycpmconjs.p (𝜑𝑃 ∈ (0...𝑁))
cycpmconjs.d (𝜑𝐷 ∈ Fin)
cycpmconjs.q (𝜑𝑄𝐶)
Assertion
Ref Expression
cycpmconjslem2 (𝜑 → ∃𝑞(𝑞:(0..^𝑁)–1-1-onto𝐷 ∧ ((𝑞𝑄) ∘ 𝑞) = ((( I ↾ (0..^𝑃)) cyclShift 1) ∪ ( I ↾ (𝑃..^𝑁)))))
Distinct variable groups:   + ,𝑞   𝐷,𝑞   𝑀,𝑞   𝑁,𝑞   𝑃,𝑞   𝑄,𝑞
Allowed substitution hints:   𝜑(𝑞)   𝐵(𝑞)   𝐶(𝑞)   𝑆(𝑞)   (𝑞)

Proof of Theorem cycpmconjslem2
Dummy variables 𝑓 𝑢 𝑤 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fzofi 13936 . . . . 5 (0..^𝑁) ∈ Fin
2 diffi 9175 . . . . 5 ((0..^𝑁) ∈ Fin → ((0..^𝑁) ∖ dom 𝑢) ∈ Fin)
31, 2mp1i 13 . . . 4 (((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) → ((0..^𝑁) ∖ dom 𝑢) ∈ Fin)
4 cycpmconjs.d . . . . . 6 (𝜑𝐷 ∈ Fin)
5 diffi 9175 . . . . . 6 (𝐷 ∈ Fin → (𝐷 ∖ ran 𝑢) ∈ Fin)
64, 5syl 17 . . . . 5 (𝜑 → (𝐷 ∖ ran 𝑢) ∈ Fin)
76ad2antrr 723 . . . 4 (((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) → (𝐷 ∖ ran 𝑢) ∈ Fin)
8 cycpmconjs.n . . . . . . . . . 10 𝑁 = (♯‘𝐷)
9 hashcl 14313 . . . . . . . . . . 11 (𝐷 ∈ Fin → (♯‘𝐷) ∈ ℕ0)
104, 9syl 17 . . . . . . . . . 10 (𝜑 → (♯‘𝐷) ∈ ℕ0)
118, 10eqeltrid 2829 . . . . . . . . 9 (𝜑𝑁 ∈ ℕ0)
12 hashfzo0 14387 . . . . . . . . 9 (𝑁 ∈ ℕ0 → (♯‘(0..^𝑁)) = 𝑁)
1311, 12syl 17 . . . . . . . 8 (𝜑 → (♯‘(0..^𝑁)) = 𝑁)
1413, 8eqtrdi 2780 . . . . . . 7 (𝜑 → (♯‘(0..^𝑁)) = (♯‘𝐷))
1514ad2antrr 723 . . . . . 6 (((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) → (♯‘(0..^𝑁)) = (♯‘𝐷))
16 simplr 766 . . . . . . . . . 10 (((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) → 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃})))
1716elin1d 4190 . . . . . . . . 9 (((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) → 𝑢 ∈ {𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷})
18 elrabi 3669 . . . . . . . . 9 (𝑢 ∈ {𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} → 𝑢 ∈ Word 𝐷)
19 wrdfin 14479 . . . . . . . . 9 (𝑢 ∈ Word 𝐷𝑢 ∈ Fin)
2017, 18, 193syl 18 . . . . . . . 8 (((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) → 𝑢 ∈ Fin)
21 id 22 . . . . . . . . . . . . 13 (𝑤 = 𝑢𝑤 = 𝑢)
22 dmeq 5893 . . . . . . . . . . . . 13 (𝑤 = 𝑢 → dom 𝑤 = dom 𝑢)
23 eqidd 2725 . . . . . . . . . . . . 13 (𝑤 = 𝑢𝐷 = 𝐷)
2421, 22, 23f1eq123d 6815 . . . . . . . . . . . 12 (𝑤 = 𝑢 → (𝑤:dom 𝑤1-1𝐷𝑢:dom 𝑢1-1𝐷))
2524elrab 3675 . . . . . . . . . . 11 (𝑢 ∈ {𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ↔ (𝑢 ∈ Word 𝐷𝑢:dom 𝑢1-1𝐷))
2625simprbi 496 . . . . . . . . . 10 (𝑢 ∈ {𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} → 𝑢:dom 𝑢1-1𝐷)
2717, 26syl 17 . . . . . . . . 9 (((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) → 𝑢:dom 𝑢1-1𝐷)
28 f1fun 6779 . . . . . . . . 9 (𝑢:dom 𝑢1-1𝐷 → Fun 𝑢)
2927, 28syl 17 . . . . . . . 8 (((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) → Fun 𝑢)
30 hashfun 14394 . . . . . . . . 9 (𝑢 ∈ Fin → (Fun 𝑢 ↔ (♯‘𝑢) = (♯‘dom 𝑢)))
3130biimpa 476 . . . . . . . 8 ((𝑢 ∈ Fin ∧ Fun 𝑢) → (♯‘𝑢) = (♯‘dom 𝑢))
3220, 29, 31syl2anc 583 . . . . . . 7 (((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) → (♯‘𝑢) = (♯‘dom 𝑢))
3316dmexd 7889 . . . . . . . 8 (((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) → dom 𝑢 ∈ V)
34 hashf1rn 14309 . . . . . . . 8 ((dom 𝑢 ∈ V ∧ 𝑢:dom 𝑢1-1𝐷) → (♯‘𝑢) = (♯‘ran 𝑢))
3533, 27, 34syl2anc 583 . . . . . . 7 (((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) → (♯‘𝑢) = (♯‘ran 𝑢))
3632, 35eqtr3d 2766 . . . . . 6 (((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) → (♯‘dom 𝑢) = (♯‘ran 𝑢))
3715, 36oveq12d 7419 . . . . 5 (((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) → ((♯‘(0..^𝑁)) − (♯‘dom 𝑢)) = ((♯‘𝐷) − (♯‘ran 𝑢)))
381a1i 11 . . . . . 6 (((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) → (0..^𝑁) ∈ Fin)
39 wrddm 14468 . . . . . . . 8 (𝑢 ∈ Word 𝐷 → dom 𝑢 = (0..^(♯‘𝑢)))
4017, 18, 393syl 18 . . . . . . 7 (((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) → dom 𝑢 = (0..^(♯‘𝑢)))
41 hashcl 14313 . . . . . . . . . . 11 (𝑢 ∈ Fin → (♯‘𝑢) ∈ ℕ0)
4217, 18, 19, 414syl 19 . . . . . . . . . 10 (((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) → (♯‘𝑢) ∈ ℕ0)
4342nn0zd 12581 . . . . . . . . 9 (((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) → (♯‘𝑢) ∈ ℤ)
4410nn0zd 12581 . . . . . . . . . . 11 (𝜑 → (♯‘𝐷) ∈ ℤ)
458, 44eqeltrid 2829 . . . . . . . . . 10 (𝜑𝑁 ∈ ℤ)
4645ad2antrr 723 . . . . . . . . 9 (((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) → 𝑁 ∈ ℤ)
474ad2antrr 723 . . . . . . . . . . 11 (((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) → 𝐷 ∈ Fin)
48 wrdf 14466 . . . . . . . . . . . . 13 (𝑢 ∈ Word 𝐷𝑢:(0..^(♯‘𝑢))⟶𝐷)
4948frnd 6715 . . . . . . . . . . . 12 (𝑢 ∈ Word 𝐷 → ran 𝑢𝐷)
5017, 18, 493syl 18 . . . . . . . . . . 11 (((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) → ran 𝑢𝐷)
51 hashss 14366 . . . . . . . . . . 11 ((𝐷 ∈ Fin ∧ ran 𝑢𝐷) → (♯‘ran 𝑢) ≤ (♯‘𝐷))
5247, 50, 51syl2anc 583 . . . . . . . . . 10 (((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) → (♯‘ran 𝑢) ≤ (♯‘𝐷))
538a1i 11 . . . . . . . . . 10 (((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) → 𝑁 = (♯‘𝐷))
5452, 35, 533brtr4d 5170 . . . . . . . . 9 (((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) → (♯‘𝑢) ≤ 𝑁)
55 eluz1 12823 . . . . . . . . . 10 ((♯‘𝑢) ∈ ℤ → (𝑁 ∈ (ℤ‘(♯‘𝑢)) ↔ (𝑁 ∈ ℤ ∧ (♯‘𝑢) ≤ 𝑁)))
5655biimpar 477 . . . . . . . . 9 (((♯‘𝑢) ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ (♯‘𝑢) ≤ 𝑁)) → 𝑁 ∈ (ℤ‘(♯‘𝑢)))
5743, 46, 54, 56syl12anc 834 . . . . . . . 8 (((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) → 𝑁 ∈ (ℤ‘(♯‘𝑢)))
58 fzoss2 13657 . . . . . . . 8 (𝑁 ∈ (ℤ‘(♯‘𝑢)) → (0..^(♯‘𝑢)) ⊆ (0..^𝑁))
5957, 58syl 17 . . . . . . 7 (((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) → (0..^(♯‘𝑢)) ⊆ (0..^𝑁))
6040, 59eqsstrd 4012 . . . . . 6 (((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) → dom 𝑢 ⊆ (0..^𝑁))
61 hashssdif 14369 . . . . . 6 (((0..^𝑁) ∈ Fin ∧ dom 𝑢 ⊆ (0..^𝑁)) → (♯‘((0..^𝑁) ∖ dom 𝑢)) = ((♯‘(0..^𝑁)) − (♯‘dom 𝑢)))
6238, 60, 61syl2anc 583 . . . . 5 (((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) → (♯‘((0..^𝑁) ∖ dom 𝑢)) = ((♯‘(0..^𝑁)) − (♯‘dom 𝑢)))
63 hashssdif 14369 . . . . . 6 ((𝐷 ∈ Fin ∧ ran 𝑢𝐷) → (♯‘(𝐷 ∖ ran 𝑢)) = ((♯‘𝐷) − (♯‘ran 𝑢)))
6447, 50, 63syl2anc 583 . . . . 5 (((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) → (♯‘(𝐷 ∖ ran 𝑢)) = ((♯‘𝐷) − (♯‘ran 𝑢)))
6537, 62, 643eqtr4d 2774 . . . 4 (((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) → (♯‘((0..^𝑁) ∖ dom 𝑢)) = (♯‘(𝐷 ∖ ran 𝑢)))
66 hasheqf1o 14306 . . . . 5 ((((0..^𝑁) ∖ dom 𝑢) ∈ Fin ∧ (𝐷 ∖ ran 𝑢) ∈ Fin) → ((♯‘((0..^𝑁) ∖ dom 𝑢)) = (♯‘(𝐷 ∖ ran 𝑢)) ↔ ∃𝑓 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)))
6766biimpa 476 . . . 4 (((((0..^𝑁) ∖ dom 𝑢) ∈ Fin ∧ (𝐷 ∖ ran 𝑢) ∈ Fin) ∧ (♯‘((0..^𝑁) ∖ dom 𝑢)) = (♯‘(𝐷 ∖ ran 𝑢))) → ∃𝑓 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢))
683, 7, 65, 67syl21anc 835 . . 3 (((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) → ∃𝑓 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢))
6927adantr 480 . . . . . . 7 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → 𝑢:dom 𝑢1-1𝐷)
70 f1f1orn 6834 . . . . . . 7 (𝑢:dom 𝑢1-1𝐷𝑢:dom 𝑢1-1-onto→ran 𝑢)
7169, 70syl 17 . . . . . 6 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → 𝑢:dom 𝑢1-1-onto→ran 𝑢)
72 simpr 484 . . . . . 6 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢))
73 disjdif 4463 . . . . . . 7 (dom 𝑢 ∩ ((0..^𝑁) ∖ dom 𝑢)) = ∅
7473a1i 11 . . . . . 6 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (dom 𝑢 ∩ ((0..^𝑁) ∖ dom 𝑢)) = ∅)
75 disjdif 4463 . . . . . . 7 (ran 𝑢 ∩ (𝐷 ∖ ran 𝑢)) = ∅
7675a1i 11 . . . . . 6 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (ran 𝑢 ∩ (𝐷 ∖ ran 𝑢)) = ∅)
77 f1oun 6842 . . . . . 6 (((𝑢:dom 𝑢1-1-onto→ran 𝑢𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) ∧ ((dom 𝑢 ∩ ((0..^𝑁) ∖ dom 𝑢)) = ∅ ∧ (ran 𝑢 ∩ (𝐷 ∖ ran 𝑢)) = ∅)) → (𝑢𝑓):(dom 𝑢 ∪ ((0..^𝑁) ∖ dom 𝑢))–1-1-onto→(ran 𝑢 ∪ (𝐷 ∖ ran 𝑢)))
7871, 72, 74, 76, 77syl22anc 836 . . . . 5 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (𝑢𝑓):(dom 𝑢 ∪ ((0..^𝑁) ∖ dom 𝑢))–1-1-onto→(ran 𝑢 ∪ (𝐷 ∖ ran 𝑢)))
79 eqidd 2725 . . . . . 6 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (𝑢𝑓) = (𝑢𝑓))
8060adantr 480 . . . . . . 7 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → dom 𝑢 ⊆ (0..^𝑁))
81 undif 4473 . . . . . . 7 (dom 𝑢 ⊆ (0..^𝑁) ↔ (dom 𝑢 ∪ ((0..^𝑁) ∖ dom 𝑢)) = (0..^𝑁))
8280, 81sylib 217 . . . . . 6 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (dom 𝑢 ∪ ((0..^𝑁) ∖ dom 𝑢)) = (0..^𝑁))
83 undif 4473 . . . . . . . 8 (ran 𝑢𝐷 ↔ (ran 𝑢 ∪ (𝐷 ∖ ran 𝑢)) = 𝐷)
8450, 83sylib 217 . . . . . . 7 (((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) → (ran 𝑢 ∪ (𝐷 ∖ ran 𝑢)) = 𝐷)
8584adantr 480 . . . . . 6 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (ran 𝑢 ∪ (𝐷 ∖ ran 𝑢)) = 𝐷)
8679, 82, 85f1oeq123d 6817 . . . . 5 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((𝑢𝑓):(dom 𝑢 ∪ ((0..^𝑁) ∖ dom 𝑢))–1-1-onto→(ran 𝑢 ∪ (𝐷 ∖ ran 𝑢)) ↔ (𝑢𝑓):(0..^𝑁)–1-1-onto𝐷))
8778, 86mpbid 231 . . . 4 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (𝑢𝑓):(0..^𝑁)–1-1-onto𝐷)
88 f1ocnv 6835 . . . . . . . . . 10 ((𝑢𝑓):(0..^𝑁)–1-1-onto𝐷(𝑢𝑓):𝐷1-1-onto→(0..^𝑁))
8987, 88syl 17 . . . . . . . . 9 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (𝑢𝑓):𝐷1-1-onto→(0..^𝑁))
90 cycpmconjs.p . . . . . . . . . . . . 13 (𝜑𝑃 ∈ (0...𝑁))
91 cycpmconjs.c . . . . . . . . . . . . . 14 𝐶 = (𝑀 “ (♯ “ {𝑃}))
92 cycpmconjs.s . . . . . . . . . . . . . 14 𝑆 = (SymGrp‘𝐷)
93 cycpmconjs.m . . . . . . . . . . . . . 14 𝑀 = (toCyc‘𝐷)
94 cycpmconjs.b . . . . . . . . . . . . . 14 𝐵 = (Base‘𝑆)
9591, 92, 8, 93, 94cycpmgcl 32780 . . . . . . . . . . . . 13 ((𝐷 ∈ Fin ∧ 𝑃 ∈ (0...𝑁)) → 𝐶𝐵)
964, 90, 95syl2anc 583 . . . . . . . . . . . 12 (𝜑𝐶𝐵)
97 cycpmconjs.q . . . . . . . . . . . 12 (𝜑𝑄𝐶)
9896, 97sseldd 3975 . . . . . . . . . . 11 (𝜑𝑄𝐵)
9992, 94symgbasf1o 19284 . . . . . . . . . . 11 (𝑄𝐵𝑄:𝐷1-1-onto𝐷)
10098, 99syl 17 . . . . . . . . . 10 (𝜑𝑄:𝐷1-1-onto𝐷)
101100ad3antrrr 727 . . . . . . . . 9 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → 𝑄:𝐷1-1-onto𝐷)
102 f1oco 6846 . . . . . . . . 9 (((𝑢𝑓):𝐷1-1-onto→(0..^𝑁) ∧ 𝑄:𝐷1-1-onto𝐷) → ((𝑢𝑓) ∘ 𝑄):𝐷1-1-onto→(0..^𝑁))
10389, 101, 102syl2anc 583 . . . . . . . 8 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((𝑢𝑓) ∘ 𝑄):𝐷1-1-onto→(0..^𝑁))
104 f1oco 6846 . . . . . . . 8 ((((𝑢𝑓) ∘ 𝑄):𝐷1-1-onto→(0..^𝑁) ∧ (𝑢𝑓):(0..^𝑁)–1-1-onto𝐷) → (((𝑢𝑓) ∘ 𝑄) ∘ (𝑢𝑓)):(0..^𝑁)–1-1-onto→(0..^𝑁))
105103, 87, 104syl2anc 583 . . . . . . 7 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (((𝑢𝑓) ∘ 𝑄) ∘ (𝑢𝑓)):(0..^𝑁)–1-1-onto→(0..^𝑁))
106 f1ofun 6825 . . . . . . 7 ((((𝑢𝑓) ∘ 𝑄) ∘ (𝑢𝑓)):(0..^𝑁)–1-1-onto→(0..^𝑁) → Fun (((𝑢𝑓) ∘ 𝑄) ∘ (𝑢𝑓)))
107 funrel 6555 . . . . . . 7 (Fun (((𝑢𝑓) ∘ 𝑄) ∘ (𝑢𝑓)) → Rel (((𝑢𝑓) ∘ 𝑄) ∘ (𝑢𝑓)))
108105, 106, 1073syl 18 . . . . . 6 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → Rel (((𝑢𝑓) ∘ 𝑄) ∘ (𝑢𝑓)))
109 f1odm 6827 . . . . . . . 8 ((((𝑢𝑓) ∘ 𝑄) ∘ (𝑢𝑓)):(0..^𝑁)–1-1-onto→(0..^𝑁) → dom (((𝑢𝑓) ∘ 𝑄) ∘ (𝑢𝑓)) = (0..^𝑁))
110105, 109syl 17 . . . . . . 7 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → dom (((𝑢𝑓) ∘ 𝑄) ∘ (𝑢𝑓)) = (0..^𝑁))
111 fzosplit 13662 . . . . . . . . 9 (𝑃 ∈ (0...𝑁) → (0..^𝑁) = ((0..^𝑃) ∪ (𝑃..^𝑁)))
11290, 111syl 17 . . . . . . . 8 (𝜑 → (0..^𝑁) = ((0..^𝑃) ∪ (𝑃..^𝑁)))
113112ad3antrrr 727 . . . . . . 7 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (0..^𝑁) = ((0..^𝑃) ∪ (𝑃..^𝑁)))
114110, 113eqtrd 2764 . . . . . 6 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → dom (((𝑢𝑓) ∘ 𝑄) ∘ (𝑢𝑓)) = ((0..^𝑃) ∪ (𝑃..^𝑁)))
115 fzodisj 13663 . . . . . . 7 ((0..^𝑃) ∩ (𝑃..^𝑁)) = ∅
116 reldisjun 6022 . . . . . . 7 ((Rel (((𝑢𝑓) ∘ 𝑄) ∘ (𝑢𝑓)) ∧ dom (((𝑢𝑓) ∘ 𝑄) ∘ (𝑢𝑓)) = ((0..^𝑃) ∪ (𝑃..^𝑁)) ∧ ((0..^𝑃) ∩ (𝑃..^𝑁)) = ∅) → (((𝑢𝑓) ∘ 𝑄) ∘ (𝑢𝑓)) = (((((𝑢𝑓) ∘ 𝑄) ∘ (𝑢𝑓)) ↾ (0..^𝑃)) ∪ ((((𝑢𝑓) ∘ 𝑄) ∘ (𝑢𝑓)) ↾ (𝑃..^𝑁))))
117115, 116mp3an3 1446 . . . . . 6 ((Rel (((𝑢𝑓) ∘ 𝑄) ∘ (𝑢𝑓)) ∧ dom (((𝑢𝑓) ∘ 𝑄) ∘ (𝑢𝑓)) = ((0..^𝑃) ∪ (𝑃..^𝑁))) → (((𝑢𝑓) ∘ 𝑄) ∘ (𝑢𝑓)) = (((((𝑢𝑓) ∘ 𝑄) ∘ (𝑢𝑓)) ↾ (0..^𝑃)) ∪ ((((𝑢𝑓) ∘ 𝑄) ∘ (𝑢𝑓)) ↾ (𝑃..^𝑁))))
118108, 114, 117syl2anc 583 . . . . 5 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (((𝑢𝑓) ∘ 𝑄) ∘ (𝑢𝑓)) = (((((𝑢𝑓) ∘ 𝑄) ∘ (𝑢𝑓)) ↾ (0..^𝑃)) ∪ ((((𝑢𝑓) ∘ 𝑄) ∘ (𝑢𝑓)) ↾ (𝑃..^𝑁))))
119 resco 6239 . . . . . . . 8 ((((𝑢𝑓) ∘ 𝑄) ∘ (𝑢𝑓)) ↾ (0..^𝑃)) = (((𝑢𝑓) ∘ 𝑄) ∘ ((𝑢𝑓) ↾ (0..^𝑃)))
120119a1i 11 . . . . . . 7 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((((𝑢𝑓) ∘ 𝑄) ∘ (𝑢𝑓)) ↾ (0..^𝑃)) = (((𝑢𝑓) ∘ 𝑄) ∘ ((𝑢𝑓) ↾ (0..^𝑃))))
12117, 18syl 17 . . . . . . . . . . . 12 (((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) → 𝑢 ∈ Word 𝐷)
122 wrdfn 14475 . . . . . . . . . . . 12 (𝑢 ∈ Word 𝐷𝑢 Fn (0..^(♯‘𝑢)))
123121, 122syl 17 . . . . . . . . . . 11 (((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) → 𝑢 Fn (0..^(♯‘𝑢)))
12416elin2d 4191 . . . . . . . . . . . . . 14 (((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) → 𝑢 ∈ (♯ “ {𝑃}))
125 hashf 14295 . . . . . . . . . . . . . . . 16 ♯:V⟶(ℕ0 ∪ {+∞})
126 ffn 6707 . . . . . . . . . . . . . . . 16 (♯:V⟶(ℕ0 ∪ {+∞}) → ♯ Fn V)
127 fniniseg 7051 . . . . . . . . . . . . . . . 16 (♯ Fn V → (𝑢 ∈ (♯ “ {𝑃}) ↔ (𝑢 ∈ V ∧ (♯‘𝑢) = 𝑃)))
128125, 126, 127mp2b 10 . . . . . . . . . . . . . . 15 (𝑢 ∈ (♯ “ {𝑃}) ↔ (𝑢 ∈ V ∧ (♯‘𝑢) = 𝑃))
129128simprbi 496 . . . . . . . . . . . . . 14 (𝑢 ∈ (♯ “ {𝑃}) → (♯‘𝑢) = 𝑃)
130124, 129syl 17 . . . . . . . . . . . . 13 (((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) → (♯‘𝑢) = 𝑃)
131130oveq2d 7417 . . . . . . . . . . . 12 (((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) → (0..^(♯‘𝑢)) = (0..^𝑃))
132131fneq2d 6633 . . . . . . . . . . 11 (((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) → (𝑢 Fn (0..^(♯‘𝑢)) ↔ 𝑢 Fn (0..^𝑃)))
133123, 132mpbid 231 . . . . . . . . . 10 (((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) → 𝑢 Fn (0..^𝑃))
134133adantr 480 . . . . . . . . 9 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → 𝑢 Fn (0..^𝑃))
135 f1ofn 6824 . . . . . . . . . 10 (𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢) → 𝑓 Fn ((0..^𝑁) ∖ dom 𝑢))
13672, 135syl 17 . . . . . . . . 9 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → 𝑓 Fn ((0..^𝑁) ∖ dom 𝑢))
13740, 131eqtrd 2764 . . . . . . . . . . . 12 (((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) → dom 𝑢 = (0..^𝑃))
138137ineq1d 4203 . . . . . . . . . . 11 (((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) → (dom 𝑢 ∩ ((0..^𝑁) ∖ dom 𝑢)) = ((0..^𝑃) ∩ ((0..^𝑁) ∖ dom 𝑢)))
13973a1i 11 . . . . . . . . . . 11 (((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) → (dom 𝑢 ∩ ((0..^𝑁) ∖ dom 𝑢)) = ∅)
140138, 139eqtr3d 2766 . . . . . . . . . 10 (((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) → ((0..^𝑃) ∩ ((0..^𝑁) ∖ dom 𝑢)) = ∅)
141140adantr 480 . . . . . . . . 9 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((0..^𝑃) ∩ ((0..^𝑁) ∖ dom 𝑢)) = ∅)
142 fnunres1 6651 . . . . . . . . 9 ((𝑢 Fn (0..^𝑃) ∧ 𝑓 Fn ((0..^𝑁) ∖ dom 𝑢) ∧ ((0..^𝑃) ∩ ((0..^𝑁) ∖ dom 𝑢)) = ∅) → ((𝑢𝑓) ↾ (0..^𝑃)) = 𝑢)
143134, 136, 141, 142syl3anc 1368 . . . . . . . 8 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((𝑢𝑓) ↾ (0..^𝑃)) = 𝑢)
144143coeq2d 5852 . . . . . . 7 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (((𝑢𝑓) ∘ 𝑄) ∘ ((𝑢𝑓) ↾ (0..^𝑃))) = (((𝑢𝑓) ∘ 𝑄) ∘ 𝑢))
145 resco 6239 . . . . . . . . . . 11 (((𝑢𝑓) ∘ 𝑄) ↾ ran 𝑢) = ((𝑢𝑓) ∘ (𝑄 ↾ ran 𝑢))
146 resco 6239 . . . . . . . . . . . . 13 ((𝑢 ∘ (𝑀𝑢)) ↾ ran 𝑢) = (𝑢 ∘ ((𝑀𝑢) ↾ ran 𝑢))
147146a1i 11 . . . . . . . . . . . 12 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((𝑢 ∘ (𝑀𝑢)) ↾ ran 𝑢) = (𝑢 ∘ ((𝑀𝑢) ↾ ran 𝑢)))
148 cnvun 6132 . . . . . . . . . . . . . . 15 (𝑢𝑓) = (𝑢𝑓)
149148reseq1i 5967 . . . . . . . . . . . . . 14 ((𝑢𝑓) ↾ ran 𝑢) = ((𝑢𝑓) ↾ ran 𝑢)
150 f1ocnv 6835 . . . . . . . . . . . . . . . 16 (𝑢:dom 𝑢1-1-onto→ran 𝑢𝑢:ran 𝑢1-1-onto→dom 𝑢)
151 f1ofn 6824 . . . . . . . . . . . . . . . 16 (𝑢:ran 𝑢1-1-onto→dom 𝑢𝑢 Fn ran 𝑢)
15271, 150, 1513syl 18 . . . . . . . . . . . . . . 15 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → 𝑢 Fn ran 𝑢)
153 f1ocnv 6835 . . . . . . . . . . . . . . . 16 (𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢) → 𝑓:(𝐷 ∖ ran 𝑢)–1-1-onto→((0..^𝑁) ∖ dom 𝑢))
154 f1ofn 6824 . . . . . . . . . . . . . . . 16 (𝑓:(𝐷 ∖ ran 𝑢)–1-1-onto→((0..^𝑁) ∖ dom 𝑢) → 𝑓 Fn (𝐷 ∖ ran 𝑢))
15572, 153, 1543syl 18 . . . . . . . . . . . . . . 15 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → 𝑓 Fn (𝐷 ∖ ran 𝑢))
156 fnunres1 6651 . . . . . . . . . . . . . . 15 ((𝑢 Fn ran 𝑢𝑓 Fn (𝐷 ∖ ran 𝑢) ∧ (ran 𝑢 ∩ (𝐷 ∖ ran 𝑢)) = ∅) → ((𝑢𝑓) ↾ ran 𝑢) = 𝑢)
157152, 155, 76, 156syl3anc 1368 . . . . . . . . . . . . . 14 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((𝑢𝑓) ↾ ran 𝑢) = 𝑢)
158149, 157eqtr2id 2777 . . . . . . . . . . . . 13 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → 𝑢 = ((𝑢𝑓) ↾ ran 𝑢))
159 simplr 766 . . . . . . . . . . . . . 14 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (𝑀𝑢) = 𝑄)
160159reseq1d 5970 . . . . . . . . . . . . 13 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((𝑀𝑢) ↾ ran 𝑢) = (𝑄 ↾ ran 𝑢))
161158, 160coeq12d 5854 . . . . . . . . . . . 12 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (𝑢 ∘ ((𝑀𝑢) ↾ ran 𝑢)) = (((𝑢𝑓) ↾ ran 𝑢) ∘ (𝑄 ↾ ran 𝑢)))
16247adantr 480 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → 𝐷 ∈ Fin)
163121adantr 480 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → 𝑢 ∈ Word 𝐷)
16493, 162, 163, 69tocycfvres1 32737 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((𝑀𝑢) ↾ ran 𝑢) = ((𝑢 cyclShift 1) ∘ 𝑢))
165160, 164eqtr3d 2766 . . . . . . . . . . . . . . . 16 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (𝑄 ↾ ran 𝑢) = ((𝑢 cyclShift 1) ∘ 𝑢))
166165rneqd 5927 . . . . . . . . . . . . . . 15 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ran (𝑄 ↾ ran 𝑢) = ran ((𝑢 cyclShift 1) ∘ 𝑢))
167 1zzd 12590 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → 1 ∈ ℤ)
168 cshf1o 32593 . . . . . . . . . . . . . . . . . 18 ((𝑢 ∈ Word 𝐷𝑢:dom 𝑢1-1𝐷 ∧ 1 ∈ ℤ) → (𝑢 cyclShift 1):dom 𝑢1-1-onto→ran 𝑢)
169163, 69, 167, 168syl3anc 1368 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (𝑢 cyclShift 1):dom 𝑢1-1-onto→ran 𝑢)
17071, 150syl 17 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → 𝑢:ran 𝑢1-1-onto→dom 𝑢)
171 f1oco 6846 . . . . . . . . . . . . . . . . 17 (((𝑢 cyclShift 1):dom 𝑢1-1-onto→ran 𝑢𝑢:ran 𝑢1-1-onto→dom 𝑢) → ((𝑢 cyclShift 1) ∘ 𝑢):ran 𝑢1-1-onto→ran 𝑢)
172169, 170, 171syl2anc 583 . . . . . . . . . . . . . . . 16 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((𝑢 cyclShift 1) ∘ 𝑢):ran 𝑢1-1-onto→ran 𝑢)
173 f1ofo 6830 . . . . . . . . . . . . . . . 16 (((𝑢 cyclShift 1) ∘ 𝑢):ran 𝑢1-1-onto→ran 𝑢 → ((𝑢 cyclShift 1) ∘ 𝑢):ran 𝑢onto→ran 𝑢)
174 forn 6798 . . . . . . . . . . . . . . . 16 (((𝑢 cyclShift 1) ∘ 𝑢):ran 𝑢onto→ran 𝑢 → ran ((𝑢 cyclShift 1) ∘ 𝑢) = ran 𝑢)
175172, 173, 1743syl 18 . . . . . . . . . . . . . . 15 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ran ((𝑢 cyclShift 1) ∘ 𝑢) = ran 𝑢)
176166, 175eqtrd 2764 . . . . . . . . . . . . . 14 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ran (𝑄 ↾ ran 𝑢) = ran 𝑢)
177 ssid 3996 . . . . . . . . . . . . . 14 ran 𝑢 ⊆ ran 𝑢
178176, 177eqsstrdi 4028 . . . . . . . . . . . . 13 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ran (𝑄 ↾ ran 𝑢) ⊆ ran 𝑢)
179 cores 6238 . . . . . . . . . . . . 13 (ran (𝑄 ↾ ran 𝑢) ⊆ ran 𝑢 → (((𝑢𝑓) ↾ ran 𝑢) ∘ (𝑄 ↾ ran 𝑢)) = ((𝑢𝑓) ∘ (𝑄 ↾ ran 𝑢)))
180178, 179syl 17 . . . . . . . . . . . 12 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (((𝑢𝑓) ↾ ran 𝑢) ∘ (𝑄 ↾ ran 𝑢)) = ((𝑢𝑓) ∘ (𝑄 ↾ ran 𝑢)))
181147, 161, 1803eqtrrd 2769 . . . . . . . . . . 11 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((𝑢𝑓) ∘ (𝑄 ↾ ran 𝑢)) = ((𝑢 ∘ (𝑀𝑢)) ↾ ran 𝑢))
182145, 181eqtrid 2776 . . . . . . . . . 10 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (((𝑢𝑓) ∘ 𝑄) ↾ ran 𝑢) = ((𝑢 ∘ (𝑀𝑢)) ↾ ran 𝑢))
183182coeq1d 5851 . . . . . . . . 9 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((((𝑢𝑓) ∘ 𝑄) ↾ ran 𝑢) ∘ 𝑢) = (((𝑢 ∘ (𝑀𝑢)) ↾ ran 𝑢) ∘ 𝑢))
184 cores 6238 . . . . . . . . . 10 (ran 𝑢 ⊆ ran 𝑢 → (((𝑢 ∘ (𝑀𝑢)) ↾ ran 𝑢) ∘ 𝑢) = ((𝑢 ∘ (𝑀𝑢)) ∘ 𝑢))
185177, 184mp1i 13 . . . . . . . . 9 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (((𝑢 ∘ (𝑀𝑢)) ↾ ran 𝑢) ∘ 𝑢) = ((𝑢 ∘ (𝑀𝑢)) ∘ 𝑢))
186183, 185eqtrd 2764 . . . . . . . 8 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((((𝑢𝑓) ∘ 𝑄) ↾ ran 𝑢) ∘ 𝑢) = ((𝑢 ∘ (𝑀𝑢)) ∘ 𝑢))
187 cores 6238 . . . . . . . . 9 (ran 𝑢 ⊆ ran 𝑢 → ((((𝑢𝑓) ∘ 𝑄) ↾ ran 𝑢) ∘ 𝑢) = (((𝑢𝑓) ∘ 𝑄) ∘ 𝑢))
188177, 187mp1i 13 . . . . . . . 8 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((((𝑢𝑓) ∘ 𝑄) ↾ ran 𝑢) ∘ 𝑢) = (((𝑢𝑓) ∘ 𝑄) ∘ 𝑢))
189130adantr 480 . . . . . . . . 9 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (♯‘𝑢) = 𝑃)
19091, 92, 8, 93, 162, 163, 69, 189cycpmconjslem1 32781 . . . . . . . 8 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((𝑢 ∘ (𝑀𝑢)) ∘ 𝑢) = (( I ↾ (0..^𝑃)) cyclShift 1))
191186, 188, 1903eqtr3d 2772 . . . . . . 7 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (((𝑢𝑓) ∘ 𝑄) ∘ 𝑢) = (( I ↾ (0..^𝑃)) cyclShift 1))
192120, 144, 1913eqtrd 2768 . . . . . 6 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((((𝑢𝑓) ∘ 𝑄) ∘ (𝑢𝑓)) ↾ (0..^𝑃)) = (( I ↾ (0..^𝑃)) cyclShift 1))
193 resco 6239 . . . . . . . 8 ((((𝑢𝑓) ∘ 𝑄) ∘ (𝑢𝑓)) ↾ (𝑃..^𝑁)) = (((𝑢𝑓) ∘ 𝑄) ∘ ((𝑢𝑓) ↾ (𝑃..^𝑁)))
194137adantr 480 . . . . . . . . . . . . 13 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → dom 𝑢 = (0..^𝑃))
195194difeq2d 4114 . . . . . . . . . . . 12 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((0..^𝑁) ∖ dom 𝑢) = ((0..^𝑁) ∖ (0..^𝑃)))
196 fzodif1 32473 . . . . . . . . . . . . . 14 (𝑃 ∈ (0...𝑁) → ((0..^𝑁) ∖ (0..^𝑃)) = (𝑃..^𝑁))
19790, 196syl 17 . . . . . . . . . . . . 13 (𝜑 → ((0..^𝑁) ∖ (0..^𝑃)) = (𝑃..^𝑁))
198197ad3antrrr 727 . . . . . . . . . . . 12 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((0..^𝑁) ∖ (0..^𝑃)) = (𝑃..^𝑁))
199195, 198eqtrd 2764 . . . . . . . . . . 11 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((0..^𝑁) ∖ dom 𝑢) = (𝑃..^𝑁))
200199reseq2d 5971 . . . . . . . . . 10 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((𝑢𝑓) ↾ ((0..^𝑁) ∖ dom 𝑢)) = ((𝑢𝑓) ↾ (𝑃..^𝑁)))
201 fnunres2 6652 . . . . . . . . . . 11 ((𝑢 Fn (0..^𝑃) ∧ 𝑓 Fn ((0..^𝑁) ∖ dom 𝑢) ∧ ((0..^𝑃) ∩ ((0..^𝑁) ∖ dom 𝑢)) = ∅) → ((𝑢𝑓) ↾ ((0..^𝑁) ∖ dom 𝑢)) = 𝑓)
202134, 136, 141, 201syl3anc 1368 . . . . . . . . . 10 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((𝑢𝑓) ↾ ((0..^𝑁) ∖ dom 𝑢)) = 𝑓)
203200, 202eqtr3d 2766 . . . . . . . . 9 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((𝑢𝑓) ↾ (𝑃..^𝑁)) = 𝑓)
204203coeq2d 5852 . . . . . . . 8 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (((𝑢𝑓) ∘ 𝑄) ∘ ((𝑢𝑓) ↾ (𝑃..^𝑁))) = (((𝑢𝑓) ∘ 𝑄) ∘ 𝑓))
205193, 204eqtrid 2776 . . . . . . 7 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((((𝑢𝑓) ∘ 𝑄) ∘ (𝑢𝑓)) ↾ (𝑃..^𝑁)) = (((𝑢𝑓) ∘ 𝑄) ∘ 𝑓))
206148reseq1i 5967 . . . . . . . . . . . 12 ((𝑢𝑓) ↾ (𝐷 ∖ ran 𝑢)) = ((𝑢𝑓) ↾ (𝐷 ∖ ran 𝑢))
207 fnunres2 6652 . . . . . . . . . . . . 13 ((𝑢 Fn ran 𝑢𝑓 Fn (𝐷 ∖ ran 𝑢) ∧ (ran 𝑢 ∩ (𝐷 ∖ ran 𝑢)) = ∅) → ((𝑢𝑓) ↾ (𝐷 ∖ ran 𝑢)) = 𝑓)
208152, 155, 76, 207syl3anc 1368 . . . . . . . . . . . 12 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((𝑢𝑓) ↾ (𝐷 ∖ ran 𝑢)) = 𝑓)
209206, 208eqtrid 2776 . . . . . . . . . . 11 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((𝑢𝑓) ↾ (𝐷 ∖ ran 𝑢)) = 𝑓)
210159reseq1d 5970 . . . . . . . . . . . 12 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((𝑀𝑢) ↾ (𝐷 ∖ ran 𝑢)) = (𝑄 ↾ (𝐷 ∖ ran 𝑢)))
21193, 162, 163, 69tocycfvres2 32738 . . . . . . . . . . . 12 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((𝑀𝑢) ↾ (𝐷 ∖ ran 𝑢)) = ( I ↾ (𝐷 ∖ ran 𝑢)))
212210, 211eqtr3d 2766 . . . . . . . . . . 11 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (𝑄 ↾ (𝐷 ∖ ran 𝑢)) = ( I ↾ (𝐷 ∖ ran 𝑢)))
213209, 212coeq12d 5854 . . . . . . . . . 10 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (((𝑢𝑓) ↾ (𝐷 ∖ ran 𝑢)) ∘ (𝑄 ↾ (𝐷 ∖ ran 𝑢))) = (𝑓 ∘ ( I ↾ (𝐷 ∖ ran 𝑢))))
214212rneqd 5927 . . . . . . . . . . . . 13 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ran (𝑄 ↾ (𝐷 ∖ ran 𝑢)) = ran ( I ↾ (𝐷 ∖ ran 𝑢)))
215 rnresi 6064 . . . . . . . . . . . . . 14 ran ( I ↾ (𝐷 ∖ ran 𝑢)) = (𝐷 ∖ ran 𝑢)
216215eqimssi 4034 . . . . . . . . . . . . 13 ran ( I ↾ (𝐷 ∖ ran 𝑢)) ⊆ (𝐷 ∖ ran 𝑢)
217214, 216eqsstrdi 4028 . . . . . . . . . . . 12 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ran (𝑄 ↾ (𝐷 ∖ ran 𝑢)) ⊆ (𝐷 ∖ ran 𝑢))
218 cores 6238 . . . . . . . . . . . 12 (ran (𝑄 ↾ (𝐷 ∖ ran 𝑢)) ⊆ (𝐷 ∖ ran 𝑢) → (((𝑢𝑓) ↾ (𝐷 ∖ ran 𝑢)) ∘ (𝑄 ↾ (𝐷 ∖ ran 𝑢))) = ((𝑢𝑓) ∘ (𝑄 ↾ (𝐷 ∖ ran 𝑢))))
219217, 218syl 17 . . . . . . . . . . 11 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (((𝑢𝑓) ↾ (𝐷 ∖ ran 𝑢)) ∘ (𝑄 ↾ (𝐷 ∖ ran 𝑢))) = ((𝑢𝑓) ∘ (𝑄 ↾ (𝐷 ∖ ran 𝑢))))
220 resco 6239 . . . . . . . . . . 11 (((𝑢𝑓) ∘ 𝑄) ↾ (𝐷 ∖ ran 𝑢)) = ((𝑢𝑓) ∘ (𝑄 ↾ (𝐷 ∖ ran 𝑢)))
221219, 220eqtr4di 2782 . . . . . . . . . 10 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (((𝑢𝑓) ↾ (𝐷 ∖ ran 𝑢)) ∘ (𝑄 ↾ (𝐷 ∖ ran 𝑢))) = (((𝑢𝑓) ∘ 𝑄) ↾ (𝐷 ∖ ran 𝑢)))
222213, 221eqtr3d 2766 . . . . . . . . 9 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (𝑓 ∘ ( I ↾ (𝐷 ∖ ran 𝑢))) = (((𝑢𝑓) ∘ 𝑄) ↾ (𝐷 ∖ ran 𝑢)))
223222coeq1d 5851 . . . . . . . 8 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((𝑓 ∘ ( I ↾ (𝐷 ∖ ran 𝑢))) ∘ 𝑓) = ((((𝑢𝑓) ∘ 𝑄) ↾ (𝐷 ∖ ran 𝑢)) ∘ 𝑓))
224 f1of 6823 . . . . . . . . . . . 12 (𝑓:(𝐷 ∖ ran 𝑢)–1-1-onto→((0..^𝑁) ∖ dom 𝑢) → 𝑓:(𝐷 ∖ ran 𝑢)⟶((0..^𝑁) ∖ dom 𝑢))
22572, 153, 2243syl 18 . . . . . . . . . . 11 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → 𝑓:(𝐷 ∖ ran 𝑢)⟶((0..^𝑁) ∖ dom 𝑢))
226 fcoi1 6755 . . . . . . . . . . 11 (𝑓:(𝐷 ∖ ran 𝑢)⟶((0..^𝑁) ∖ dom 𝑢) → (𝑓 ∘ ( I ↾ (𝐷 ∖ ran 𝑢))) = 𝑓)
227225, 226syl 17 . . . . . . . . . 10 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (𝑓 ∘ ( I ↾ (𝐷 ∖ ran 𝑢))) = 𝑓)
228227coeq1d 5851 . . . . . . . . 9 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((𝑓 ∘ ( I ↾ (𝐷 ∖ ran 𝑢))) ∘ 𝑓) = (𝑓𝑓))
229 f1ococnv1 6852 . . . . . . . . . 10 (𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢) → (𝑓𝑓) = ( I ↾ ((0..^𝑁) ∖ dom 𝑢)))
23072, 229syl 17 . . . . . . . . 9 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (𝑓𝑓) = ( I ↾ ((0..^𝑁) ∖ dom 𝑢)))
231199reseq2d 5971 . . . . . . . . 9 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ( I ↾ ((0..^𝑁) ∖ dom 𝑢)) = ( I ↾ (𝑃..^𝑁)))
232228, 230, 2313eqtrd 2768 . . . . . . . 8 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((𝑓 ∘ ( I ↾ (𝐷 ∖ ran 𝑢))) ∘ 𝑓) = ( I ↾ (𝑃..^𝑁)))
233 f1of 6823 . . . . . . . . . 10 (𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢) → 𝑓:((0..^𝑁) ∖ dom 𝑢)⟶(𝐷 ∖ ran 𝑢))
234 frn 6714 . . . . . . . . . 10 (𝑓:((0..^𝑁) ∖ dom 𝑢)⟶(𝐷 ∖ ran 𝑢) → ran 𝑓 ⊆ (𝐷 ∖ ran 𝑢))
23572, 233, 2343syl 18 . . . . . . . . 9 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ran 𝑓 ⊆ (𝐷 ∖ ran 𝑢))
236 cores 6238 . . . . . . . . 9 (ran 𝑓 ⊆ (𝐷 ∖ ran 𝑢) → ((((𝑢𝑓) ∘ 𝑄) ↾ (𝐷 ∖ ran 𝑢)) ∘ 𝑓) = (((𝑢𝑓) ∘ 𝑄) ∘ 𝑓))
237235, 236syl 17 . . . . . . . 8 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((((𝑢𝑓) ∘ 𝑄) ↾ (𝐷 ∖ ran 𝑢)) ∘ 𝑓) = (((𝑢𝑓) ∘ 𝑄) ∘ 𝑓))
238223, 232, 2373eqtr3rd 2773 . . . . . . 7 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (((𝑢𝑓) ∘ 𝑄) ∘ 𝑓) = ( I ↾ (𝑃..^𝑁)))
239205, 238eqtrd 2764 . . . . . 6 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((((𝑢𝑓) ∘ 𝑄) ∘ (𝑢𝑓)) ↾ (𝑃..^𝑁)) = ( I ↾ (𝑃..^𝑁)))
240192, 239uneq12d 4156 . . . . 5 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (((((𝑢𝑓) ∘ 𝑄) ∘ (𝑢𝑓)) ↾ (0..^𝑃)) ∪ ((((𝑢𝑓) ∘ 𝑄) ∘ (𝑢𝑓)) ↾ (𝑃..^𝑁))) = ((( I ↾ (0..^𝑃)) cyclShift 1) ∪ ( I ↾ (𝑃..^𝑁))))
241118, 240eqtrd 2764 . . . 4 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (((𝑢𝑓) ∘ 𝑄) ∘ (𝑢𝑓)) = ((( I ↾ (0..^𝑃)) cyclShift 1) ∪ ( I ↾ (𝑃..^𝑁))))
242 vex 3470 . . . . . 6 𝑢 ∈ V
243 vex 3470 . . . . . 6 𝑓 ∈ V
244242, 243unex 7726 . . . . 5 (𝑢𝑓) ∈ V
245 f1oeq1 6811 . . . . . 6 (𝑞 = (𝑢𝑓) → (𝑞:(0..^𝑁)–1-1-onto𝐷 ↔ (𝑢𝑓):(0..^𝑁)–1-1-onto𝐷))
246 cnveq 5863 . . . . . . . . 9 (𝑞 = (𝑢𝑓) → 𝑞 = (𝑢𝑓))
247246coeq1d 5851 . . . . . . . 8 (𝑞 = (𝑢𝑓) → (𝑞𝑄) = ((𝑢𝑓) ∘ 𝑄))
248 id 22 . . . . . . . 8 (𝑞 = (𝑢𝑓) → 𝑞 = (𝑢𝑓))
249247, 248coeq12d 5854 . . . . . . 7 (𝑞 = (𝑢𝑓) → ((𝑞𝑄) ∘ 𝑞) = (((𝑢𝑓) ∘ 𝑄) ∘ (𝑢𝑓)))
250249eqeq1d 2726 . . . . . 6 (𝑞 = (𝑢𝑓) → (((𝑞𝑄) ∘ 𝑞) = ((( I ↾ (0..^𝑃)) cyclShift 1) ∪ ( I ↾ (𝑃..^𝑁))) ↔ (((𝑢𝑓) ∘ 𝑄) ∘ (𝑢𝑓)) = ((( I ↾ (0..^𝑃)) cyclShift 1) ∪ ( I ↾ (𝑃..^𝑁)))))
251245, 250anbi12d 630 . . . . 5 (𝑞 = (𝑢𝑓) → ((𝑞:(0..^𝑁)–1-1-onto𝐷 ∧ ((𝑞𝑄) ∘ 𝑞) = ((( I ↾ (0..^𝑃)) cyclShift 1) ∪ ( I ↾ (𝑃..^𝑁)))) ↔ ((𝑢𝑓):(0..^𝑁)–1-1-onto𝐷 ∧ (((𝑢𝑓) ∘ 𝑄) ∘ (𝑢𝑓)) = ((( I ↾ (0..^𝑃)) cyclShift 1) ∪ ( I ↾ (𝑃..^𝑁))))))
252244, 251spcev 3588 . . . 4 (((𝑢𝑓):(0..^𝑁)–1-1-onto𝐷 ∧ (((𝑢𝑓) ∘ 𝑄) ∘ (𝑢𝑓)) = ((( I ↾ (0..^𝑃)) cyclShift 1) ∪ ( I ↾ (𝑃..^𝑁)))) → ∃𝑞(𝑞:(0..^𝑁)–1-1-onto𝐷 ∧ ((𝑞𝑄) ∘ 𝑞) = ((( I ↾ (0..^𝑃)) cyclShift 1) ∪ ( I ↾ (𝑃..^𝑁)))))
25387, 241, 252syl2anc 583 . . 3 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ∃𝑞(𝑞:(0..^𝑁)–1-1-onto𝐷 ∧ ((𝑞𝑄) ∘ 𝑞) = ((( I ↾ (0..^𝑃)) cyclShift 1) ∪ ( I ↾ (𝑃..^𝑁)))))
25468, 253exlimddv 1930 . 2 (((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) → ∃𝑞(𝑞:(0..^𝑁)–1-1-onto𝐷 ∧ ((𝑞𝑄) ∘ 𝑞) = ((( I ↾ (0..^𝑃)) cyclShift 1) ∪ ( I ↾ (𝑃..^𝑁)))))
255 nfcv 2895 . . 3 𝑢𝑀
25693, 92, 94tocycf 32744 . . . 4 (𝐷 ∈ Fin → 𝑀:{𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷}⟶𝐵)
257 ffn 6707 . . . 4 (𝑀:{𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷}⟶𝐵𝑀 Fn {𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷})
2584, 256, 2573syl 18 . . 3 (𝜑𝑀 Fn {𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷})
25997, 91eleqtrdi 2835 . . 3 (𝜑𝑄 ∈ (𝑀 “ (♯ “ {𝑃})))
260255, 258, 259fvelimad 6949 . 2 (𝜑 → ∃𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))(𝑀𝑢) = 𝑄)
261254, 260r19.29a 3154 1 (𝜑 → ∃𝑞(𝑞:(0..^𝑁)–1-1-onto𝐷 ∧ ((𝑞𝑄) ∘ 𝑞) = ((( I ↾ (0..^𝑃)) cyclShift 1) ∪ ( I ↾ (𝑃..^𝑁)))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 395   = wceq 1533  wex 1773  wcel 2098  {crab 3424  Vcvv 3466  cdif 3937  cun 3938  cin 3939  wss 3940  c0 4314  {csn 4620   class class class wbr 5138   I cid 5563  ccnv 5665  dom cdm 5666  ran crn 5667  cres 5668  cima 5669  ccom 5670  Rel wrel 5671  Fun wfun 6527   Fn wfn 6528  wf 6529  1-1wf1 6530  ontowfo 6531  1-1-ontowf1o 6532  cfv 6533  (class class class)co 7401  Fincfn 8935  0cc0 11106  1c1 11107  +∞cpnf 11242  cle 11246  cmin 11441  0cn0 12469  cz 12555  cuz 12819  ...cfz 13481  ..^cfzo 13624  chash 14287  Word cword 14461   cyclShift ccsh 14735  Basecbs 17143  +gcplusg 17196  -gcsg 18855  SymGrpcsymg 19276  toCycctocyc 32733
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-rep 5275  ax-sep 5289  ax-nul 5296  ax-pow 5353  ax-pr 5417  ax-un 7718  ax-cnex 11162  ax-resscn 11163  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-addrcl 11167  ax-mulcl 11168  ax-mulrcl 11169  ax-mulcom 11170  ax-addass 11171  ax-mulass 11172  ax-distr 11173  ax-i2m1 11174  ax-1ne0 11175  ax-1rid 11176  ax-rnegex 11177  ax-rrecex 11178  ax-cnre 11179  ax-pre-lttri 11180  ax-pre-lttrn 11181  ax-pre-ltadd 11182  ax-pre-mulgt0 11183  ax-pre-sup 11184
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ne 2933  df-nel 3039  df-ral 3054  df-rex 3063  df-rmo 3368  df-reu 3369  df-rab 3425  df-v 3468  df-sbc 3770  df-csb 3886  df-dif 3943  df-un 3945  df-in 3947  df-ss 3957  df-pss 3959  df-nul 4315  df-if 4521  df-pw 4596  df-sn 4621  df-pr 4623  df-tp 4625  df-op 4627  df-uni 4900  df-int 4941  df-iun 4989  df-br 5139  df-opab 5201  df-mpt 5222  df-tr 5256  df-id 5564  df-eprel 5570  df-po 5578  df-so 5579  df-fr 5621  df-we 5623  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-pred 6290  df-ord 6357  df-on 6358  df-lim 6359  df-suc 6360  df-iota 6485  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-riota 7357  df-ov 7404  df-oprab 7405  df-mpo 7406  df-om 7849  df-1st 7968  df-2nd 7969  df-frecs 8261  df-wrecs 8292  df-recs 8366  df-rdg 8405  df-1o 8461  df-oadd 8465  df-er 8699  df-map 8818  df-en 8936  df-dom 8937  df-sdom 8938  df-fin 8939  df-sup 9433  df-inf 9434  df-dju 9892  df-card 9930  df-pnf 11247  df-mnf 11248  df-xr 11249  df-ltxr 11250  df-le 11251  df-sub 11443  df-neg 11444  df-div 11869  df-nn 12210  df-2 12272  df-3 12273  df-4 12274  df-5 12275  df-6 12276  df-7 12277  df-8 12278  df-9 12279  df-n0 12470  df-xnn0 12542  df-z 12556  df-uz 12820  df-rp 12972  df-fz 13482  df-fzo 13625  df-fl 13754  df-mod 13832  df-hash 14288  df-word 14462  df-concat 14518  df-substr 14588  df-pfx 14618  df-csh 14736  df-struct 17079  df-sets 17096  df-slot 17114  df-ndx 17126  df-base 17144  df-ress 17173  df-plusg 17209  df-tset 17215  df-efmnd 18784  df-symg 19277  df-tocyc 32734
This theorem is referenced by:  cycpmconjs  32783
  Copyright terms: Public domain W3C validator