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 30730
Description: Lemma for cycpmconjs 30731 (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 13337 . . . . 5 (0..^𝑁) ∈ Fin
2 diffi 8744 . . . . 5 ((0..^𝑁) ∈ Fin → ((0..^𝑁) ∖ dom 𝑢) ∈ Fin)
31, 2mp1i 13 . . . 4 (((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) → ((0..^𝑁) ∖ dom 𝑢) ∈ Fin)
4 cycpmconjs.d . . . . . 6 (𝜑𝐷 ∈ Fin)
5 diffi 8744 . . . . . 6 (𝐷 ∈ Fin → (𝐷 ∖ ran 𝑢) ∈ Fin)
64, 5syl 17 . . . . 5 (𝜑 → (𝐷 ∖ ran 𝑢) ∈ Fin)
76ad2antrr 722 . . . 4 (((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) → (𝐷 ∖ ran 𝑢) ∈ Fin)
8 cycpmconjs.n . . . . . . . . . 10 𝑁 = (♯‘𝐷)
9 hashcl 13712 . . . . . . . . . . 11 (𝐷 ∈ Fin → (♯‘𝐷) ∈ ℕ0)
104, 9syl 17 . . . . . . . . . 10 (𝜑 → (♯‘𝐷) ∈ ℕ0)
118, 10eqeltrid 2922 . . . . . . . . 9 (𝜑𝑁 ∈ ℕ0)
12 hashfzo0 13786 . . . . . . . . 9 (𝑁 ∈ ℕ0 → (♯‘(0..^𝑁)) = 𝑁)
1311, 12syl 17 . . . . . . . 8 (𝜑 → (♯‘(0..^𝑁)) = 𝑁)
1413, 8syl6eq 2877 . . . . . . 7 (𝜑 → (♯‘(0..^𝑁)) = (♯‘𝐷))
1514ad2antrr 722 . . . . . 6 (((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) → (♯‘(0..^𝑁)) = (♯‘𝐷))
16 simplr 765 . . . . . . . . . 10 (((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) → 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃})))
1716elin1d 4179 . . . . . . . . 9 (((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) → 𝑢 ∈ {𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷})
18 elrabi 3679 . . . . . . . . 9 (𝑢 ∈ {𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} → 𝑢 ∈ Word 𝐷)
19 wrdfin 13877 . . . . . . . . 9 (𝑢 ∈ Word 𝐷𝑢 ∈ Fin)
2017, 18, 193syl 18 . . . . . . . 8 (((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) → 𝑢 ∈ Fin)
21 id 22 . . . . . . . . . . . . 13 (𝑤 = 𝑢𝑤 = 𝑢)
22 dmeq 5771 . . . . . . . . . . . . 13 (𝑤 = 𝑢 → dom 𝑤 = dom 𝑢)
23 eqidd 2827 . . . . . . . . . . . . 13 (𝑤 = 𝑢𝐷 = 𝐷)
2421, 22, 23f1eq123d 6607 . . . . . . . . . . . 12 (𝑤 = 𝑢 → (𝑤:dom 𝑤1-1𝐷𝑢:dom 𝑢1-1𝐷))
2524elrab 3684 . . . . . . . . . . 11 (𝑢 ∈ {𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ↔ (𝑢 ∈ Word 𝐷𝑢:dom 𝑢1-1𝐷))
2625simprbi 497 . . . . . . . . . 10 (𝑢 ∈ {𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} → 𝑢:dom 𝑢1-1𝐷)
2717, 26syl 17 . . . . . . . . 9 (((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) → 𝑢:dom 𝑢1-1𝐷)
28 f1fun 6576 . . . . . . . . 9 (𝑢:dom 𝑢1-1𝐷 → Fun 𝑢)
2927, 28syl 17 . . . . . . . 8 (((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) → Fun 𝑢)
30 hashfun 13793 . . . . . . . . 9 (𝑢 ∈ Fin → (Fun 𝑢 ↔ (♯‘𝑢) = (♯‘dom 𝑢)))
3130biimpa 477 . . . . . . . 8 ((𝑢 ∈ Fin ∧ Fun 𝑢) → (♯‘𝑢) = (♯‘dom 𝑢))
3220, 29, 31syl2anc 584 . . . . . . 7 (((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) → (♯‘𝑢) = (♯‘dom 𝑢))
3316dmexd 7608 . . . . . . . 8 (((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) → dom 𝑢 ∈ V)
34 hashf1rn 13708 . . . . . . . 8 ((dom 𝑢 ∈ V ∧ 𝑢:dom 𝑢1-1𝐷) → (♯‘𝑢) = (♯‘ran 𝑢))
3533, 27, 34syl2anc 584 . . . . . . 7 (((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) → (♯‘𝑢) = (♯‘ran 𝑢))
3632, 35eqtr3d 2863 . . . . . 6 (((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) → (♯‘dom 𝑢) = (♯‘ran 𝑢))
3715, 36oveq12d 7168 . . . . 5 (((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) → ((♯‘(0..^𝑁)) − (♯‘dom 𝑢)) = ((♯‘𝐷) − (♯‘ran 𝑢)))
381a1i 11 . . . . . 6 (((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) → (0..^𝑁) ∈ Fin)
39 wrddm 13863 . . . . . . . 8 (𝑢 ∈ Word 𝐷 → dom 𝑢 = (0..^(♯‘𝑢)))
4017, 18, 393syl 18 . . . . . . 7 (((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) → dom 𝑢 = (0..^(♯‘𝑢)))
41 hashcl 13712 . . . . . . . . . . 11 (𝑢 ∈ Fin → (♯‘𝑢) ∈ ℕ0)
4217, 18, 19, 414syl 19 . . . . . . . . . 10 (((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) → (♯‘𝑢) ∈ ℕ0)
4342nn0zd 12079 . . . . . . . . 9 (((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) → (♯‘𝑢) ∈ ℤ)
4410nn0zd 12079 . . . . . . . . . . 11 (𝜑 → (♯‘𝐷) ∈ ℤ)
458, 44eqeltrid 2922 . . . . . . . . . 10 (𝜑𝑁 ∈ ℤ)
4645ad2antrr 722 . . . . . . . . 9 (((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) → 𝑁 ∈ ℤ)
474ad2antrr 722 . . . . . . . . . . 11 (((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) → 𝐷 ∈ Fin)
48 wrdf 13861 . . . . . . . . . . . . 13 (𝑢 ∈ Word 𝐷𝑢:(0..^(♯‘𝑢))⟶𝐷)
4948frnd 6520 . . . . . . . . . . . 12 (𝑢 ∈ Word 𝐷 → ran 𝑢𝐷)
5017, 18, 493syl 18 . . . . . . . . . . 11 (((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) → ran 𝑢𝐷)
51 hashss 13765 . . . . . . . . . . 11 ((𝐷 ∈ Fin ∧ ran 𝑢𝐷) → (♯‘ran 𝑢) ≤ (♯‘𝐷))
5247, 50, 51syl2anc 584 . . . . . . . . . 10 (((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) → (♯‘ran 𝑢) ≤ (♯‘𝐷))
538a1i 11 . . . . . . . . . 10 (((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) → 𝑁 = (♯‘𝐷))
5452, 35, 533brtr4d 5095 . . . . . . . . 9 (((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) → (♯‘𝑢) ≤ 𝑁)
55 eluz1 12241 . . . . . . . . . 10 ((♯‘𝑢) ∈ ℤ → (𝑁 ∈ (ℤ‘(♯‘𝑢)) ↔ (𝑁 ∈ ℤ ∧ (♯‘𝑢) ≤ 𝑁)))
5655biimpar 478 . . . . . . . . 9 (((♯‘𝑢) ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ (♯‘𝑢) ≤ 𝑁)) → 𝑁 ∈ (ℤ‘(♯‘𝑢)))
5743, 46, 54, 56syl12anc 834 . . . . . . . 8 (((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) → 𝑁 ∈ (ℤ‘(♯‘𝑢)))
58 fzoss2 13060 . . . . . . . 8 (𝑁 ∈ (ℤ‘(♯‘𝑢)) → (0..^(♯‘𝑢)) ⊆ (0..^𝑁))
5957, 58syl 17 . . . . . . 7 (((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) → (0..^(♯‘𝑢)) ⊆ (0..^𝑁))
6040, 59eqsstrd 4009 . . . . . 6 (((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) → dom 𝑢 ⊆ (0..^𝑁))
61 hashssdif 13768 . . . . . 6 (((0..^𝑁) ∈ Fin ∧ dom 𝑢 ⊆ (0..^𝑁)) → (♯‘((0..^𝑁) ∖ dom 𝑢)) = ((♯‘(0..^𝑁)) − (♯‘dom 𝑢)))
6238, 60, 61syl2anc 584 . . . . 5 (((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) → (♯‘((0..^𝑁) ∖ dom 𝑢)) = ((♯‘(0..^𝑁)) − (♯‘dom 𝑢)))
63 hashssdif 13768 . . . . . 6 ((𝐷 ∈ Fin ∧ ran 𝑢𝐷) → (♯‘(𝐷 ∖ ran 𝑢)) = ((♯‘𝐷) − (♯‘ran 𝑢)))
6447, 50, 63syl2anc 584 . . . . 5 (((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) → (♯‘(𝐷 ∖ ran 𝑢)) = ((♯‘𝐷) − (♯‘ran 𝑢)))
6537, 62, 643eqtr4d 2871 . . . 4 (((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) → (♯‘((0..^𝑁) ∖ dom 𝑢)) = (♯‘(𝐷 ∖ ran 𝑢)))
66 hasheqf1o 13704 . . . . 5 ((((0..^𝑁) ∖ dom 𝑢) ∈ Fin ∧ (𝐷 ∖ ran 𝑢) ∈ Fin) → ((♯‘((0..^𝑁) ∖ dom 𝑢)) = (♯‘(𝐷 ∖ ran 𝑢)) ↔ ∃𝑓 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)))
6766biimpa 477 . . . 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 481 . . . . . . 7 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → 𝑢:dom 𝑢1-1𝐷)
70 f1f1orn 6625 . . . . . . 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 485 . . . . . 6 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢))
73 disjdif 4424 . . . . . . 7 (dom 𝑢 ∩ ((0..^𝑁) ∖ dom 𝑢)) = ∅
7473a1i 11 . . . . . 6 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (dom 𝑢 ∩ ((0..^𝑁) ∖ dom 𝑢)) = ∅)
75 disjdif 4424 . . . . . . 7 (ran 𝑢 ∩ (𝐷 ∖ ran 𝑢)) = ∅
7675a1i 11 . . . . . 6 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (ran 𝑢 ∩ (𝐷 ∖ ran 𝑢)) = ∅)
77 f1oun 6633 . . . . . 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 2827 . . . . . 6 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (𝑢𝑓) = (𝑢𝑓))
8060adantr 481 . . . . . . 7 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → dom 𝑢 ⊆ (0..^𝑁))
81 undif 4433 . . . . . . 7 (dom 𝑢 ⊆ (0..^𝑁) ↔ (dom 𝑢 ∪ ((0..^𝑁) ∖ dom 𝑢)) = (0..^𝑁))
8280, 81sylib 219 . . . . . 6 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (dom 𝑢 ∪ ((0..^𝑁) ∖ dom 𝑢)) = (0..^𝑁))
83 undif 4433 . . . . . . . 8 (ran 𝑢𝐷 ↔ (ran 𝑢 ∪ (𝐷 ∖ ran 𝑢)) = 𝐷)
8450, 83sylib 219 . . . . . . 7 (((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) → (ran 𝑢 ∪ (𝐷 ∖ ran 𝑢)) = 𝐷)
8584adantr 481 . . . . . 6 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (ran 𝑢 ∪ (𝐷 ∖ ran 𝑢)) = 𝐷)
8679, 82, 85f1oeq123d 6609 . . . . 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 233 . . . 4 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (𝑢𝑓):(0..^𝑁)–1-1-onto𝐷)
88 f1ocnv 6626 . . . . . . . . . 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 30728 . . . . . . . . . . . . 13 ((𝐷 ∈ Fin ∧ 𝑃 ∈ (0...𝑁)) → 𝐶𝐵)
964, 90, 95syl2anc 584 . . . . . . . . . . . 12 (𝜑𝐶𝐵)
97 cycpmconjs.q . . . . . . . . . . . 12 (𝜑𝑄𝐶)
9896, 97sseldd 3972 . . . . . . . . . . 11 (𝜑𝑄𝐵)
9992, 94symgbasf1o 18446 . . . . . . . . . . 11 (𝑄𝐵𝑄:𝐷1-1-onto𝐷)
10098, 99syl 17 . . . . . . . . . 10 (𝜑𝑄:𝐷1-1-onto𝐷)
101100ad3antrrr 726 . . . . . . . . 9 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → 𝑄:𝐷1-1-onto𝐷)
102 f1oco 6636 . . . . . . . . 9 (((𝑢𝑓):𝐷1-1-onto→(0..^𝑁) ∧ 𝑄:𝐷1-1-onto𝐷) → ((𝑢𝑓) ∘ 𝑄):𝐷1-1-onto→(0..^𝑁))
10389, 101, 102syl2anc 584 . . . . . . . 8 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((𝑢𝑓) ∘ 𝑄):𝐷1-1-onto→(0..^𝑁))
104 f1oco 6636 . . . . . . . 8 ((((𝑢𝑓) ∘ 𝑄):𝐷1-1-onto→(0..^𝑁) ∧ (𝑢𝑓):(0..^𝑁)–1-1-onto𝐷) → (((𝑢𝑓) ∘ 𝑄) ∘ (𝑢𝑓)):(0..^𝑁)–1-1-onto→(0..^𝑁))
105103, 87, 104syl2anc 584 . . . . . . 7 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (((𝑢𝑓) ∘ 𝑄) ∘ (𝑢𝑓)):(0..^𝑁)–1-1-onto→(0..^𝑁))
106 f1ofun 6616 . . . . . . 7 ((((𝑢𝑓) ∘ 𝑄) ∘ (𝑢𝑓)):(0..^𝑁)–1-1-onto→(0..^𝑁) → Fun (((𝑢𝑓) ∘ 𝑄) ∘ (𝑢𝑓)))
107 funrel 6371 . . . . . . 7 (Fun (((𝑢𝑓) ∘ 𝑄) ∘ (𝑢𝑓)) → Rel (((𝑢𝑓) ∘ 𝑄) ∘ (𝑢𝑓)))
108105, 106, 1073syl 18 . . . . . 6 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → Rel (((𝑢𝑓) ∘ 𝑄) ∘ (𝑢𝑓)))
109 f1odm 6618 . . . . . . . 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 13065 . . . . . . . . 9 (𝑃 ∈ (0...𝑁) → (0..^𝑁) = ((0..^𝑃) ∪ (𝑃..^𝑁)))
11290, 111syl 17 . . . . . . . 8 (𝜑 → (0..^𝑁) = ((0..^𝑃) ∪ (𝑃..^𝑁)))
113112ad3antrrr 726 . . . . . . 7 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (0..^𝑁) = ((0..^𝑃) ∪ (𝑃..^𝑁)))
114110, 113eqtrd 2861 . . . . . 6 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → dom (((𝑢𝑓) ∘ 𝑄) ∘ (𝑢𝑓)) = ((0..^𝑃) ∪ (𝑃..^𝑁)))
115 fzodisj 13066 . . . . . . 7 ((0..^𝑃) ∩ (𝑃..^𝑁)) = ∅
116 reldisjun 30287 . . . . . . 7 ((Rel (((𝑢𝑓) ∘ 𝑄) ∘ (𝑢𝑓)) ∧ dom (((𝑢𝑓) ∘ 𝑄) ∘ (𝑢𝑓)) = ((0..^𝑃) ∪ (𝑃..^𝑁)) ∧ ((0..^𝑃) ∩ (𝑃..^𝑁)) = ∅) → (((𝑢𝑓) ∘ 𝑄) ∘ (𝑢𝑓)) = (((((𝑢𝑓) ∘ 𝑄) ∘ (𝑢𝑓)) ↾ (0..^𝑃)) ∪ ((((𝑢𝑓) ∘ 𝑄) ∘ (𝑢𝑓)) ↾ (𝑃..^𝑁))))
117115, 116mp3an3 1443 . . . . . 6 ((Rel (((𝑢𝑓) ∘ 𝑄) ∘ (𝑢𝑓)) ∧ dom (((𝑢𝑓) ∘ 𝑄) ∘ (𝑢𝑓)) = ((0..^𝑃) ∪ (𝑃..^𝑁))) → (((𝑢𝑓) ∘ 𝑄) ∘ (𝑢𝑓)) = (((((𝑢𝑓) ∘ 𝑄) ∘ (𝑢𝑓)) ↾ (0..^𝑃)) ∪ ((((𝑢𝑓) ∘ 𝑄) ∘ (𝑢𝑓)) ↾ (𝑃..^𝑁))))
118108, 114, 117syl2anc 584 . . . . 5 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (((𝑢𝑓) ∘ 𝑄) ∘ (𝑢𝑓)) = (((((𝑢𝑓) ∘ 𝑄) ∘ (𝑢𝑓)) ↾ (0..^𝑃)) ∪ ((((𝑢𝑓) ∘ 𝑄) ∘ (𝑢𝑓)) ↾ (𝑃..^𝑁))))
119 resco 6102 . . . . . . . 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 13871 . . . . . . . . . . . 12 (𝑢 ∈ Word 𝐷𝑢 Fn (0..^(♯‘𝑢)))
123121, 122syl 17 . . . . . . . . . . 11 (((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) → 𝑢 Fn (0..^(♯‘𝑢)))
12416elin2d 4180 . . . . . . . . . . . . . 14 (((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) → 𝑢 ∈ (♯ “ {𝑃}))
125 hashf 13693 . . . . . . . . . . . . . . . 16 ♯:V⟶(ℕ0 ∪ {+∞})
126 ffn 6513 . . . . . . . . . . . . . . . 16 (♯:V⟶(ℕ0 ∪ {+∞}) → ♯ Fn V)
127 fniniseg 6828 . . . . . . . . . . . . . . . 16 (♯ Fn V → (𝑢 ∈ (♯ “ {𝑃}) ↔ (𝑢 ∈ V ∧ (♯‘𝑢) = 𝑃)))
128125, 126, 127mp2b 10 . . . . . . . . . . . . . . 15 (𝑢 ∈ (♯ “ {𝑃}) ↔ (𝑢 ∈ V ∧ (♯‘𝑢) = 𝑃))
129128simprbi 497 . . . . . . . . . . . . . 14 (𝑢 ∈ (♯ “ {𝑃}) → (♯‘𝑢) = 𝑃)
130124, 129syl 17 . . . . . . . . . . . . 13 (((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) → (♯‘𝑢) = 𝑃)
131130oveq2d 7166 . . . . . . . . . . . 12 (((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) → (0..^(♯‘𝑢)) = (0..^𝑃))
132131fneq2d 6446 . . . . . . . . . . 11 (((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) → (𝑢 Fn (0..^(♯‘𝑢)) ↔ 𝑢 Fn (0..^𝑃)))
133123, 132mpbid 233 . . . . . . . . . 10 (((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) → 𝑢 Fn (0..^𝑃))
134133adantr 481 . . . . . . . . 9 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → 𝑢 Fn (0..^𝑃))
135 f1ofn 6615 . . . . . . . . . 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 2861 . . . . . . . . . . . 12 (((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) → dom 𝑢 = (0..^𝑃))
138137ineq1d 4192 . . . . . . . . . . 11 (((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) → (dom 𝑢 ∩ ((0..^𝑁) ∖ dom 𝑢)) = ((0..^𝑃) ∩ ((0..^𝑁) ∖ dom 𝑢)))
13973a1i 11 . . . . . . . . . . 11 (((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) → (dom 𝑢 ∩ ((0..^𝑁) ∖ dom 𝑢)) = ∅)
140138, 139eqtr3d 2863 . . . . . . . . . 10 (((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) → ((0..^𝑃) ∩ ((0..^𝑁) ∖ dom 𝑢)) = ∅)
141140adantr 481 . . . . . . . . 9 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((0..^𝑃) ∩ ((0..^𝑁) ∖ dom 𝑢)) = ∅)
142 fnunres1 30290 . . . . . . . . 9 ((𝑢 Fn (0..^𝑃) ∧ 𝑓 Fn ((0..^𝑁) ∖ dom 𝑢) ∧ ((0..^𝑃) ∩ ((0..^𝑁) ∖ dom 𝑢)) = ∅) → ((𝑢𝑓) ↾ (0..^𝑃)) = 𝑢)
143134, 136, 141, 142syl3anc 1365 . . . . . . . 8 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((𝑢𝑓) ↾ (0..^𝑃)) = 𝑢)
144143coeq2d 5732 . . . . . . 7 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (((𝑢𝑓) ∘ 𝑄) ∘ ((𝑢𝑓) ↾ (0..^𝑃))) = (((𝑢𝑓) ∘ 𝑄) ∘ 𝑢))
145 resco 6102 . . . . . . . . . . 11 (((𝑢𝑓) ∘ 𝑄) ↾ ran 𝑢) = ((𝑢𝑓) ∘ (𝑄 ↾ ran 𝑢))
146 resco 6102 . . . . . . . . . . . . 13 ((𝑢 ∘ (𝑀𝑢)) ↾ ran 𝑢) = (𝑢 ∘ ((𝑀𝑢) ↾ ran 𝑢))
147146a1i 11 . . . . . . . . . . . 12 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((𝑢 ∘ (𝑀𝑢)) ↾ ran 𝑢) = (𝑢 ∘ ((𝑀𝑢) ↾ ran 𝑢)))
148 cnvun 6000 . . . . . . . . . . . . . . 15 (𝑢𝑓) = (𝑢𝑓)
149148reseq1i 5848 . . . . . . . . . . . . . 14 ((𝑢𝑓) ↾ ran 𝑢) = ((𝑢𝑓) ↾ ran 𝑢)
150 f1ocnv 6626 . . . . . . . . . . . . . . . 16 (𝑢:dom 𝑢1-1-onto→ran 𝑢𝑢:ran 𝑢1-1-onto→dom 𝑢)
151 f1ofn 6615 . . . . . . . . . . . . . . . 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 6626 . . . . . . . . . . . . . . . 16 (𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢) → 𝑓:(𝐷 ∖ ran 𝑢)–1-1-onto→((0..^𝑁) ∖ dom 𝑢))
154 f1ofn 6615 . . . . . . . . . . . . . . . 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 30290 . . . . . . . . . . . . . . 15 ((𝑢 Fn ran 𝑢𝑓 Fn (𝐷 ∖ ran 𝑢) ∧ (ran 𝑢 ∩ (𝐷 ∖ ran 𝑢)) = ∅) → ((𝑢𝑓) ↾ ran 𝑢) = 𝑢)
157152, 155, 76, 156syl3anc 1365 . . . . . . . . . . . . . 14 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((𝑢𝑓) ↾ ran 𝑢) = 𝑢)
158149, 157syl5req 2874 . . . . . . . . . . . . 13 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → 𝑢 = ((𝑢𝑓) ↾ ran 𝑢))
159 simplr 765 . . . . . . . . . . . . . 14 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (𝑀𝑢) = 𝑄)
160159reseq1d 5851 . . . . . . . . . . . . 13 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((𝑀𝑢) ↾ ran 𝑢) = (𝑄 ↾ ran 𝑢))
161158, 160coeq12d 5734 . . . . . . . . . . . 12 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (𝑢 ∘ ((𝑀𝑢) ↾ ran 𝑢)) = (((𝑢𝑓) ↾ ran 𝑢) ∘ (𝑄 ↾ ran 𝑢)))
16247adantr 481 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → 𝐷 ∈ Fin)
163121adantr 481 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → 𝑢 ∈ Word 𝐷)
16493, 162, 163, 69tocycfvres1 30685 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((𝑀𝑢) ↾ ran 𝑢) = ((𝑢 cyclShift 1) ∘ 𝑢))
165160, 164eqtr3d 2863 . . . . . . . . . . . . . . . 16 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (𝑄 ↾ ran 𝑢) = ((𝑢 cyclShift 1) ∘ 𝑢))
166165rneqd 5807 . . . . . . . . . . . . . . 15 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ran (𝑄 ↾ ran 𝑢) = ran ((𝑢 cyclShift 1) ∘ 𝑢))
167 1zzd 12007 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → 1 ∈ ℤ)
168 cshf1o 30569 . . . . . . . . . . . . . . . . . 18 ((𝑢 ∈ Word 𝐷𝑢:dom 𝑢1-1𝐷 ∧ 1 ∈ ℤ) → (𝑢 cyclShift 1):dom 𝑢1-1-onto→ran 𝑢)
169163, 69, 167, 168syl3anc 1365 . . . . . . . . . . . . . . . . 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 6636 . . . . . . . . . . . . . . . . 17 (((𝑢 cyclShift 1):dom 𝑢1-1-onto→ran 𝑢𝑢:ran 𝑢1-1-onto→dom 𝑢) → ((𝑢 cyclShift 1) ∘ 𝑢):ran 𝑢1-1-onto→ran 𝑢)
172169, 170, 171syl2anc 584 . . . . . . . . . . . . . . . 16 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((𝑢 cyclShift 1) ∘ 𝑢):ran 𝑢1-1-onto→ran 𝑢)
173 f1ofo 6621 . . . . . . . . . . . . . . . 16 (((𝑢 cyclShift 1) ∘ 𝑢):ran 𝑢1-1-onto→ran 𝑢 → ((𝑢 cyclShift 1) ∘ 𝑢):ran 𝑢onto→ran 𝑢)
174 forn 6592 . . . . . . . . . . . . . . . 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 2861 . . . . . . . . . . . . . 14 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ran (𝑄 ↾ ran 𝑢) = ran 𝑢)
177 ssid 3993 . . . . . . . . . . . . . 14 ran 𝑢 ⊆ ran 𝑢
178176, 177eqsstrdi 4025 . . . . . . . . . . . . 13 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ran (𝑄 ↾ ran 𝑢) ⊆ ran 𝑢)
179 cores 6101 . . . . . . . . . . . . 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 2866 . . . . . . . . . . 11 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((𝑢𝑓) ∘ (𝑄 ↾ ran 𝑢)) = ((𝑢 ∘ (𝑀𝑢)) ↾ ran 𝑢))
182145, 181syl5eq 2873 . . . . . . . . . 10 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (((𝑢𝑓) ∘ 𝑄) ↾ ran 𝑢) = ((𝑢 ∘ (𝑀𝑢)) ↾ ran 𝑢))
183182coeq1d 5731 . . . . . . . . 9 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((((𝑢𝑓) ∘ 𝑄) ↾ ran 𝑢) ∘ 𝑢) = (((𝑢 ∘ (𝑀𝑢)) ↾ ran 𝑢) ∘ 𝑢))
184 cores 6101 . . . . . . . . . 10 (ran 𝑢 ⊆ ran 𝑢 → (((𝑢 ∘ (𝑀𝑢)) ↾ ran 𝑢) ∘ 𝑢) = ((𝑢 ∘ (𝑀𝑢)) ∘ 𝑢))
185177, 184mp1i 13 . . . . . . . . 9 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (((𝑢 ∘ (𝑀𝑢)) ↾ ran 𝑢) ∘ 𝑢) = ((𝑢 ∘ (𝑀𝑢)) ∘ 𝑢))
186183, 185eqtrd 2861 . . . . . . . 8 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((((𝑢𝑓) ∘ 𝑄) ↾ ran 𝑢) ∘ 𝑢) = ((𝑢 ∘ (𝑀𝑢)) ∘ 𝑢))
187 cores 6101 . . . . . . . . 9 (ran 𝑢 ⊆ ran 𝑢 → ((((𝑢𝑓) ∘ 𝑄) ↾ ran 𝑢) ∘ 𝑢) = (((𝑢𝑓) ∘ 𝑄) ∘ 𝑢))
188177, 187mp1i 13 . . . . . . . 8 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((((𝑢𝑓) ∘ 𝑄) ↾ ran 𝑢) ∘ 𝑢) = (((𝑢𝑓) ∘ 𝑄) ∘ 𝑢))
189130adantr 481 . . . . . . . . 9 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (♯‘𝑢) = 𝑃)
19091, 92, 8, 93, 162, 163, 69, 189cycpmconjslem1 30729 . . . . . . . 8 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((𝑢 ∘ (𝑀𝑢)) ∘ 𝑢) = (( I ↾ (0..^𝑃)) cyclShift 1))
191186, 188, 1903eqtr3d 2869 . . . . . . 7 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (((𝑢𝑓) ∘ 𝑄) ∘ 𝑢) = (( I ↾ (0..^𝑃)) cyclShift 1))
192120, 144, 1913eqtrd 2865 . . . . . 6 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((((𝑢𝑓) ∘ 𝑄) ∘ (𝑢𝑓)) ↾ (0..^𝑃)) = (( I ↾ (0..^𝑃)) cyclShift 1))
193 resco 6102 . . . . . . . 8 ((((𝑢𝑓) ∘ 𝑄) ∘ (𝑢𝑓)) ↾ (𝑃..^𝑁)) = (((𝑢𝑓) ∘ 𝑄) ∘ ((𝑢𝑓) ↾ (𝑃..^𝑁)))
194137adantr 481 . . . . . . . . . . . . 13 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → dom 𝑢 = (0..^𝑃))
195194difeq2d 4103 . . . . . . . . . . . 12 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((0..^𝑁) ∖ dom 𝑢) = ((0..^𝑁) ∖ (0..^𝑃)))
196 fzodif1 30448 . . . . . . . . . . . . . 14 (𝑃 ∈ (0...𝑁) → ((0..^𝑁) ∖ (0..^𝑃)) = (𝑃..^𝑁))
19790, 196syl 17 . . . . . . . . . . . . 13 (𝜑 → ((0..^𝑁) ∖ (0..^𝑃)) = (𝑃..^𝑁))
198197ad3antrrr 726 . . . . . . . . . . . 12 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((0..^𝑁) ∖ (0..^𝑃)) = (𝑃..^𝑁))
199195, 198eqtrd 2861 . . . . . . . . . . 11 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((0..^𝑁) ∖ dom 𝑢) = (𝑃..^𝑁))
200199reseq2d 5852 . . . . . . . . . 10 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((𝑢𝑓) ↾ ((0..^𝑁) ∖ dom 𝑢)) = ((𝑢𝑓) ↾ (𝑃..^𝑁)))
201 fnunres2 30358 . . . . . . . . . . 11 ((𝑢 Fn (0..^𝑃) ∧ 𝑓 Fn ((0..^𝑁) ∖ dom 𝑢) ∧ ((0..^𝑃) ∩ ((0..^𝑁) ∖ dom 𝑢)) = ∅) → ((𝑢𝑓) ↾ ((0..^𝑁) ∖ dom 𝑢)) = 𝑓)
202134, 136, 141, 201syl3anc 1365 . . . . . . . . . 10 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((𝑢𝑓) ↾ ((0..^𝑁) ∖ dom 𝑢)) = 𝑓)
203200, 202eqtr3d 2863 . . . . . . . . 9 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((𝑢𝑓) ↾ (𝑃..^𝑁)) = 𝑓)
204203coeq2d 5732 . . . . . . . 8 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (((𝑢𝑓) ∘ 𝑄) ∘ ((𝑢𝑓) ↾ (𝑃..^𝑁))) = (((𝑢𝑓) ∘ 𝑄) ∘ 𝑓))
205193, 204syl5eq 2873 . . . . . . 7 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((((𝑢𝑓) ∘ 𝑄) ∘ (𝑢𝑓)) ↾ (𝑃..^𝑁)) = (((𝑢𝑓) ∘ 𝑄) ∘ 𝑓))
206148reseq1i 5848 . . . . . . . . . . . 12 ((𝑢𝑓) ↾ (𝐷 ∖ ran 𝑢)) = ((𝑢𝑓) ↾ (𝐷 ∖ ran 𝑢))
207 fnunres2 30358 . . . . . . . . . . . . 13 ((𝑢 Fn ran 𝑢𝑓 Fn (𝐷 ∖ ran 𝑢) ∧ (ran 𝑢 ∩ (𝐷 ∖ ran 𝑢)) = ∅) → ((𝑢𝑓) ↾ (𝐷 ∖ ran 𝑢)) = 𝑓)
208152, 155, 76, 207syl3anc 1365 . . . . . . . . . . . 12 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((𝑢𝑓) ↾ (𝐷 ∖ ran 𝑢)) = 𝑓)
209206, 208syl5eq 2873 . . . . . . . . . . 11 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((𝑢𝑓) ↾ (𝐷 ∖ ran 𝑢)) = 𝑓)
210159reseq1d 5851 . . . . . . . . . . . 12 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((𝑀𝑢) ↾ (𝐷 ∖ ran 𝑢)) = (𝑄 ↾ (𝐷 ∖ ran 𝑢)))
21193, 162, 163, 69tocycfvres2 30686 . . . . . . . . . . . 12 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((𝑀𝑢) ↾ (𝐷 ∖ ran 𝑢)) = ( I ↾ (𝐷 ∖ ran 𝑢)))
212210, 211eqtr3d 2863 . . . . . . . . . . 11 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (𝑄 ↾ (𝐷 ∖ ran 𝑢)) = ( I ↾ (𝐷 ∖ ran 𝑢)))
213209, 212coeq12d 5734 . . . . . . . . . 10 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (((𝑢𝑓) ↾ (𝐷 ∖ ran 𝑢)) ∘ (𝑄 ↾ (𝐷 ∖ ran 𝑢))) = (𝑓 ∘ ( I ↾ (𝐷 ∖ ran 𝑢))))
214212rneqd 5807 . . . . . . . . . . . . 13 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ran (𝑄 ↾ (𝐷 ∖ ran 𝑢)) = ran ( I ↾ (𝐷 ∖ ran 𝑢)))
215 rnresi 5942 . . . . . . . . . . . . . 14 ran ( I ↾ (𝐷 ∖ ran 𝑢)) = (𝐷 ∖ ran 𝑢)
216215eqimssi 4029 . . . . . . . . . . . . 13 ran ( I ↾ (𝐷 ∖ ran 𝑢)) ⊆ (𝐷 ∖ ran 𝑢)
217214, 216eqsstrdi 4025 . . . . . . . . . . . 12 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ran (𝑄 ↾ (𝐷 ∖ ran 𝑢)) ⊆ (𝐷 ∖ ran 𝑢))
218 cores 6101 . . . . . . . . . . . 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 6102 . . . . . . . . . . 11 (((𝑢𝑓) ∘ 𝑄) ↾ (𝐷 ∖ ran 𝑢)) = ((𝑢𝑓) ∘ (𝑄 ↾ (𝐷 ∖ ran 𝑢)))
221219, 220syl6eqr 2879 . . . . . . . . . 10 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (((𝑢𝑓) ↾ (𝐷 ∖ ran 𝑢)) ∘ (𝑄 ↾ (𝐷 ∖ ran 𝑢))) = (((𝑢𝑓) ∘ 𝑄) ↾ (𝐷 ∖ ran 𝑢)))
222213, 221eqtr3d 2863 . . . . . . . . 9 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (𝑓 ∘ ( I ↾ (𝐷 ∖ ran 𝑢))) = (((𝑢𝑓) ∘ 𝑄) ↾ (𝐷 ∖ ran 𝑢)))
223222coeq1d 5731 . . . . . . . 8 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((𝑓 ∘ ( I ↾ (𝐷 ∖ ran 𝑢))) ∘ 𝑓) = ((((𝑢𝑓) ∘ 𝑄) ↾ (𝐷 ∖ ran 𝑢)) ∘ 𝑓))
224 f1of 6614 . . . . . . . . . . . 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 6551 . . . . . . . . . . 11 (𝑓:(𝐷 ∖ ran 𝑢)⟶((0..^𝑁) ∖ dom 𝑢) → (𝑓 ∘ ( I ↾ (𝐷 ∖ ran 𝑢))) = 𝑓)
227225, 226syl 17 . . . . . . . . . 10 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (𝑓 ∘ ( I ↾ (𝐷 ∖ ran 𝑢))) = 𝑓)
228227coeq1d 5731 . . . . . . . . 9 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((𝑓 ∘ ( I ↾ (𝐷 ∖ ran 𝑢))) ∘ 𝑓) = (𝑓𝑓))
229 f1ococnv1 6642 . . . . . . . . . 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 5852 . . . . . . . . 9 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ( I ↾ ((0..^𝑁) ∖ dom 𝑢)) = ( I ↾ (𝑃..^𝑁)))
232228, 230, 2313eqtrd 2865 . . . . . . . 8 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((𝑓 ∘ ( I ↾ (𝐷 ∖ ran 𝑢))) ∘ 𝑓) = ( I ↾ (𝑃..^𝑁)))
233 f1of 6614 . . . . . . . . . 10 (𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢) → 𝑓:((0..^𝑁) ∖ dom 𝑢)⟶(𝐷 ∖ ran 𝑢))
234 frn 6519 . . . . . . . . . 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 6101 . . . . . . . . 9 (ran 𝑓 ⊆ (𝐷 ∖ ran 𝑢) → ((((𝑢𝑓) ∘ 𝑄) ↾ (𝐷 ∖ ran 𝑢)) ∘ 𝑓) = (((𝑢𝑓) ∘ 𝑄) ∘ 𝑓))
237235, 236syl 17 . . . . . . . 8 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((((𝑢𝑓) ∘ 𝑄) ↾ (𝐷 ∖ ran 𝑢)) ∘ 𝑓) = (((𝑢𝑓) ∘ 𝑄) ∘ 𝑓))
238223, 232, 2373eqtr3rd 2870 . . . . . . 7 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (((𝑢𝑓) ∘ 𝑄) ∘ 𝑓) = ( I ↾ (𝑃..^𝑁)))
239205, 238eqtrd 2861 . . . . . 6 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((((𝑢𝑓) ∘ 𝑄) ∘ (𝑢𝑓)) ↾ (𝑃..^𝑁)) = ( I ↾ (𝑃..^𝑁)))
240192, 239uneq12d 4144 . . . . 5 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (((((𝑢𝑓) ∘ 𝑄) ∘ (𝑢𝑓)) ↾ (0..^𝑃)) ∪ ((((𝑢𝑓) ∘ 𝑄) ∘ (𝑢𝑓)) ↾ (𝑃..^𝑁))) = ((( I ↾ (0..^𝑃)) cyclShift 1) ∪ ( I ↾ (𝑃..^𝑁))))
241118, 240eqtrd 2861 . . . 4 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (((𝑢𝑓) ∘ 𝑄) ∘ (𝑢𝑓)) = ((( I ↾ (0..^𝑃)) cyclShift 1) ∪ ( I ↾ (𝑃..^𝑁))))
242 vex 3503 . . . . . 6 𝑢 ∈ V
243 vex 3503 . . . . . 6 𝑓 ∈ V
244242, 243unex 7462 . . . . 5 (𝑢𝑓) ∈ V
245 f1oeq1 6603 . . . . . 6 (𝑞 = (𝑢𝑓) → (𝑞:(0..^𝑁)–1-1-onto𝐷 ↔ (𝑢𝑓):(0..^𝑁)–1-1-onto𝐷))
246 cnveq 5743 . . . . . . . . 9 (𝑞 = (𝑢𝑓) → 𝑞 = (𝑢𝑓))
247246coeq1d 5731 . . . . . . . 8 (𝑞 = (𝑢𝑓) → (𝑞𝑄) = ((𝑢𝑓) ∘ 𝑄))
248 id 22 . . . . . . . 8 (𝑞 = (𝑢𝑓) → 𝑞 = (𝑢𝑓))
249247, 248coeq12d 5734 . . . . . . 7 (𝑞 = (𝑢𝑓) → ((𝑞𝑄) ∘ 𝑞) = (((𝑢𝑓) ∘ 𝑄) ∘ (𝑢𝑓)))
250249eqeq1d 2828 . . . . . 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 3611 . . . 4 (((𝑢𝑓):(0..^𝑁)–1-1-onto𝐷 ∧ (((𝑢𝑓) ∘ 𝑄) ∘ (𝑢𝑓)) = ((( I ↾ (0..^𝑃)) cyclShift 1) ∪ ( I ↾ (𝑃..^𝑁)))) → ∃𝑞(𝑞:(0..^𝑁)–1-1-onto𝐷 ∧ ((𝑞𝑄) ∘ 𝑞) = ((( I ↾ (0..^𝑃)) cyclShift 1) ∪ ( I ↾ (𝑃..^𝑁)))))
25387, 241, 252syl2anc 584 . . 3 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ∃𝑞(𝑞:(0..^𝑁)–1-1-onto𝐷 ∧ ((𝑞𝑄) ∘ 𝑞) = ((( I ↾ (0..^𝑃)) cyclShift 1) ∪ ( I ↾ (𝑃..^𝑁)))))
25468, 253exlimddv 1929 . 2 (((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) → ∃𝑞(𝑞:(0..^𝑁)–1-1-onto𝐷 ∧ ((𝑞𝑄) ∘ 𝑞) = ((( I ↾ (0..^𝑃)) cyclShift 1) ∪ ( I ↾ (𝑃..^𝑁)))))
255 nfcv 2982 . . 3 𝑢𝑀
25693, 92, 94tocycf 30692 . . . 4 (𝐷 ∈ Fin → 𝑀:{𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷}⟶𝐵)
257 ffn 6513 . . . 4 (𝑀:{𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷}⟶𝐵𝑀 Fn {𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷})
2584, 256, 2573syl 18 . . 3 (𝜑𝑀 Fn {𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷})
25997, 91syl6eleq 2928 . . 3 (𝜑𝑄 ∈ (𝑀 “ (♯ “ {𝑃})))
260255, 258, 259fvelimad 6731 . 2 (𝜑 → ∃𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))(𝑀𝑢) = 𝑄)
261254, 260r19.29a 3294 1 (𝜑 → ∃𝑞(𝑞:(0..^𝑁)–1-1-onto𝐷 ∧ ((𝑞𝑄) ∘ 𝑞) = ((( I ↾ (0..^𝑃)) cyclShift 1) ∪ ( I ↾ (𝑃..^𝑁)))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396   = wceq 1530  wex 1773  wcel 2107  {crab 3147  Vcvv 3500  cdif 3937  cun 3938  cin 3939  wss 3940  c0 4295  {csn 4564   class class class wbr 5063   I cid 5458  ccnv 5553  dom cdm 5554  ran crn 5555  cres 5556  cima 5557  ccom 5558  Rel wrel 5559  Fun wfun 6348   Fn wfn 6349  wf 6350  1-1wf1 6351  ontowfo 6352  1-1-ontowf1o 6353  cfv 6354  (class class class)co 7150  Fincfn 8503  0cc0 10531  1c1 10532  +∞cpnf 10666  cle 10670  cmin 10864  0cn0 11891  cz 11975  cuz 12237  ...cfz 12887  ..^cfzo 13028  chash 13685  Word cword 13856   cyclShift ccsh 14145  Basecbs 16478  +gcplusg 16560  -gcsg 18050  SymGrpcsymg 18440  toCycctocyc 30681
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 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798  ax-rep 5187  ax-sep 5200  ax-nul 5207  ax-pow 5263  ax-pr 5326  ax-un 7455  ax-cnex 10587  ax-resscn 10588  ax-1cn 10589  ax-icn 10590  ax-addcl 10591  ax-addrcl 10592  ax-mulcl 10593  ax-mulrcl 10594  ax-mulcom 10595  ax-addass 10596  ax-mulass 10597  ax-distr 10598  ax-i2m1 10599  ax-1ne0 10600  ax-1rid 10601  ax-rnegex 10602  ax-rrecex 10603  ax-cnre 10604  ax-pre-lttri 10605  ax-pre-lttrn 10606  ax-pre-ltadd 10607  ax-pre-mulgt0 10608  ax-pre-sup 10609
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3or 1082  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2620  df-eu 2652  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-ne 3022  df-nel 3129  df-ral 3148  df-rex 3149  df-reu 3150  df-rmo 3151  df-rab 3152  df-v 3502  df-sbc 3777  df-csb 3888  df-dif 3943  df-un 3945  df-in 3947  df-ss 3956  df-pss 3958  df-nul 4296  df-if 4471  df-pw 4544  df-sn 4565  df-pr 4567  df-tp 4569  df-op 4571  df-uni 4838  df-int 4875  df-iun 4919  df-br 5064  df-opab 5126  df-mpt 5144  df-tr 5170  df-id 5459  df-eprel 5464  df-po 5473  df-so 5474  df-fr 5513  df-we 5515  df-xp 5560  df-rel 5561  df-cnv 5562  df-co 5563  df-dm 5564  df-rn 5565  df-res 5566  df-ima 5567  df-pred 6147  df-ord 6193  df-on 6194  df-lim 6195  df-suc 6196  df-iota 6313  df-fun 6356  df-fn 6357  df-f 6358  df-f1 6359  df-fo 6360  df-f1o 6361  df-fv 6362  df-riota 7108  df-ov 7153  df-oprab 7154  df-mpo 7155  df-om 7574  df-1st 7685  df-2nd 7686  df-wrecs 7943  df-recs 8004  df-rdg 8042  df-1o 8098  df-oadd 8102  df-er 8284  df-map 8403  df-en 8504  df-dom 8505  df-sdom 8506  df-fin 8507  df-sup 8900  df-inf 8901  df-dju 9324  df-card 9362  df-pnf 10671  df-mnf 10672  df-xr 10673  df-ltxr 10674  df-le 10675  df-sub 10866  df-neg 10867  df-div 11292  df-nn 11633  df-2 11694  df-3 11695  df-4 11696  df-5 11697  df-6 11698  df-7 11699  df-8 11700  df-9 11701  df-n0 11892  df-xnn0 11962  df-z 11976  df-uz 12238  df-rp 12385  df-fz 12888  df-fzo 13029  df-fl 13157  df-mod 13233  df-hash 13686  df-word 13857  df-concat 13918  df-substr 13998  df-pfx 14028  df-csh 14146  df-struct 16480  df-ndx 16481  df-slot 16482  df-base 16484  df-plusg 16573  df-tset 16579  df-symg 18441  df-tocyc 30682
This theorem is referenced by:  cycpmconjs  30731
  Copyright terms: Public domain W3C validator