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

Theorem cycpmconjslem2 30949
 Description: Lemma for cycpmconjs 30950. (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 13392 . . . . 5 (0..^𝑁) ∈ Fin
2 diffi 8787 . . . . 5 ((0..^𝑁) ∈ Fin → ((0..^𝑁) ∖ dom 𝑢) ∈ Fin)
31, 2mp1i 13 . . . 4 (((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) → ((0..^𝑁) ∖ dom 𝑢) ∈ Fin)
4 cycpmconjs.d . . . . . 6 (𝜑𝐷 ∈ Fin)
5 diffi 8787 . . . . . 6 (𝐷 ∈ Fin → (𝐷 ∖ ran 𝑢) ∈ Fin)
64, 5syl 17 . . . . 5 (𝜑 → (𝐷 ∖ ran 𝑢) ∈ Fin)
76ad2antrr 726 . . . 4 (((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) → (𝐷 ∖ ran 𝑢) ∈ Fin)
8 cycpmconjs.n . . . . . . . . . 10 𝑁 = (♯‘𝐷)
9 hashcl 13768 . . . . . . . . . . 11 (𝐷 ∈ Fin → (♯‘𝐷) ∈ ℕ0)
104, 9syl 17 . . . . . . . . . 10 (𝜑 → (♯‘𝐷) ∈ ℕ0)
118, 10eqeltrid 2857 . . . . . . . . 9 (𝜑𝑁 ∈ ℕ0)
12 hashfzo0 13842 . . . . . . . . 9 (𝑁 ∈ ℕ0 → (♯‘(0..^𝑁)) = 𝑁)
1311, 12syl 17 . . . . . . . 8 (𝜑 → (♯‘(0..^𝑁)) = 𝑁)
1413, 8eqtrdi 2810 . . . . . . 7 (𝜑 → (♯‘(0..^𝑁)) = (♯‘𝐷))
1514ad2antrr 726 . . . . . 6 (((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) → (♯‘(0..^𝑁)) = (♯‘𝐷))
16 simplr 769 . . . . . . . . . 10 (((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) → 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃})))
1716elin1d 4104 . . . . . . . . 9 (((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) → 𝑢 ∈ {𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷})
18 elrabi 3597 . . . . . . . . 9 (𝑢 ∈ {𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} → 𝑢 ∈ Word 𝐷)
19 wrdfin 13932 . . . . . . . . 9 (𝑢 ∈ Word 𝐷𝑢 ∈ Fin)
2017, 18, 193syl 18 . . . . . . . 8 (((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) → 𝑢 ∈ Fin)
21 id 22 . . . . . . . . . . . . 13 (𝑤 = 𝑢𝑤 = 𝑢)
22 dmeq 5744 . . . . . . . . . . . . 13 (𝑤 = 𝑢 → dom 𝑤 = dom 𝑢)
23 eqidd 2760 . . . . . . . . . . . . 13 (𝑤 = 𝑢𝐷 = 𝐷)
2421, 22, 23f1eq123d 6595 . . . . . . . . . . . 12 (𝑤 = 𝑢 → (𝑤:dom 𝑤1-1𝐷𝑢:dom 𝑢1-1𝐷))
2524elrab 3603 . . . . . . . . . . 11 (𝑢 ∈ {𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ↔ (𝑢 ∈ Word 𝐷𝑢:dom 𝑢1-1𝐷))
2625simprbi 501 . . . . . . . . . 10 (𝑢 ∈ {𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} → 𝑢:dom 𝑢1-1𝐷)
2717, 26syl 17 . . . . . . . . 9 (((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) → 𝑢:dom 𝑢1-1𝐷)
28 f1fun 6563 . . . . . . . . 9 (𝑢:dom 𝑢1-1𝐷 → Fun 𝑢)
2927, 28syl 17 . . . . . . . 8 (((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) → Fun 𝑢)
30 hashfun 13849 . . . . . . . . 9 (𝑢 ∈ Fin → (Fun 𝑢 ↔ (♯‘𝑢) = (♯‘dom 𝑢)))
3130biimpa 481 . . . . . . . 8 ((𝑢 ∈ Fin ∧ Fun 𝑢) → (♯‘𝑢) = (♯‘dom 𝑢))
3220, 29, 31syl2anc 588 . . . . . . 7 (((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) → (♯‘𝑢) = (♯‘dom 𝑢))
3316dmexd 7616 . . . . . . . 8 (((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) → dom 𝑢 ∈ V)
34 hashf1rn 13764 . . . . . . . 8 ((dom 𝑢 ∈ V ∧ 𝑢:dom 𝑢1-1𝐷) → (♯‘𝑢) = (♯‘ran 𝑢))
3533, 27, 34syl2anc 588 . . . . . . 7 (((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) → (♯‘𝑢) = (♯‘ran 𝑢))
3632, 35eqtr3d 2796 . . . . . 6 (((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) → (♯‘dom 𝑢) = (♯‘ran 𝑢))
3715, 36oveq12d 7169 . . . . 5 (((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) → ((♯‘(0..^𝑁)) − (♯‘dom 𝑢)) = ((♯‘𝐷) − (♯‘ran 𝑢)))
381a1i 11 . . . . . 6 (((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) → (0..^𝑁) ∈ Fin)
39 wrddm 13921 . . . . . . . 8 (𝑢 ∈ Word 𝐷 → dom 𝑢 = (0..^(♯‘𝑢)))
4017, 18, 393syl 18 . . . . . . 7 (((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) → dom 𝑢 = (0..^(♯‘𝑢)))
41 hashcl 13768 . . . . . . . . . . 11 (𝑢 ∈ Fin → (♯‘𝑢) ∈ ℕ0)
4217, 18, 19, 414syl 19 . . . . . . . . . 10 (((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) → (♯‘𝑢) ∈ ℕ0)
4342nn0zd 12125 . . . . . . . . 9 (((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) → (♯‘𝑢) ∈ ℤ)
4410nn0zd 12125 . . . . . . . . . . 11 (𝜑 → (♯‘𝐷) ∈ ℤ)
458, 44eqeltrid 2857 . . . . . . . . . 10 (𝜑𝑁 ∈ ℤ)
4645ad2antrr 726 . . . . . . . . 9 (((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) → 𝑁 ∈ ℤ)
474ad2antrr 726 . . . . . . . . . . 11 (((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) → 𝐷 ∈ Fin)
48 wrdf 13919 . . . . . . . . . . . . 13 (𝑢 ∈ Word 𝐷𝑢:(0..^(♯‘𝑢))⟶𝐷)
4948frnd 6506 . . . . . . . . . . . 12 (𝑢 ∈ Word 𝐷 → ran 𝑢𝐷)
5017, 18, 493syl 18 . . . . . . . . . . 11 (((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) → ran 𝑢𝐷)
51 hashss 13821 . . . . . . . . . . 11 ((𝐷 ∈ Fin ∧ ran 𝑢𝐷) → (♯‘ran 𝑢) ≤ (♯‘𝐷))
5247, 50, 51syl2anc 588 . . . . . . . . . 10 (((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) → (♯‘ran 𝑢) ≤ (♯‘𝐷))
538a1i 11 . . . . . . . . . 10 (((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) → 𝑁 = (♯‘𝐷))
5452, 35, 533brtr4d 5065 . . . . . . . . 9 (((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) → (♯‘𝑢) ≤ 𝑁)
55 eluz1 12287 . . . . . . . . . 10 ((♯‘𝑢) ∈ ℤ → (𝑁 ∈ (ℤ‘(♯‘𝑢)) ↔ (𝑁 ∈ ℤ ∧ (♯‘𝑢) ≤ 𝑁)))
5655biimpar 482 . . . . . . . . 9 (((♯‘𝑢) ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ (♯‘𝑢) ≤ 𝑁)) → 𝑁 ∈ (ℤ‘(♯‘𝑢)))
5743, 46, 54, 56syl12anc 836 . . . . . . . 8 (((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) → 𝑁 ∈ (ℤ‘(♯‘𝑢)))
58 fzoss2 13115 . . . . . . . 8 (𝑁 ∈ (ℤ‘(♯‘𝑢)) → (0..^(♯‘𝑢)) ⊆ (0..^𝑁))
5957, 58syl 17 . . . . . . 7 (((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) → (0..^(♯‘𝑢)) ⊆ (0..^𝑁))
6040, 59eqsstrd 3931 . . . . . 6 (((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) → dom 𝑢 ⊆ (0..^𝑁))
61 hashssdif 13824 . . . . . 6 (((0..^𝑁) ∈ Fin ∧ dom 𝑢 ⊆ (0..^𝑁)) → (♯‘((0..^𝑁) ∖ dom 𝑢)) = ((♯‘(0..^𝑁)) − (♯‘dom 𝑢)))
6238, 60, 61syl2anc 588 . . . . 5 (((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) → (♯‘((0..^𝑁) ∖ dom 𝑢)) = ((♯‘(0..^𝑁)) − (♯‘dom 𝑢)))
63 hashssdif 13824 . . . . . 6 ((𝐷 ∈ Fin ∧ ran 𝑢𝐷) → (♯‘(𝐷 ∖ ran 𝑢)) = ((♯‘𝐷) − (♯‘ran 𝑢)))
6447, 50, 63syl2anc 588 . . . . 5 (((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) → (♯‘(𝐷 ∖ ran 𝑢)) = ((♯‘𝐷) − (♯‘ran 𝑢)))
6537, 62, 643eqtr4d 2804 . . . 4 (((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) → (♯‘((0..^𝑁) ∖ dom 𝑢)) = (♯‘(𝐷 ∖ ran 𝑢)))
66 hasheqf1o 13760 . . . . 5 ((((0..^𝑁) ∖ dom 𝑢) ∈ Fin ∧ (𝐷 ∖ ran 𝑢) ∈ Fin) → ((♯‘((0..^𝑁) ∖ dom 𝑢)) = (♯‘(𝐷 ∖ ran 𝑢)) ↔ ∃𝑓 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)))
6766biimpa 481 . . . 4 (((((0..^𝑁) ∖ dom 𝑢) ∈ Fin ∧ (𝐷 ∖ ran 𝑢) ∈ Fin) ∧ (♯‘((0..^𝑁) ∖ dom 𝑢)) = (♯‘(𝐷 ∖ ran 𝑢))) → ∃𝑓 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢))
683, 7, 65, 67syl21anc 837 . . 3 (((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) → ∃𝑓 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢))
6927adantr 485 . . . . . . 7 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → 𝑢:dom 𝑢1-1𝐷)
70 f1f1orn 6614 . . . . . . 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 489 . . . . . 6 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢))
73 disjdif 4369 . . . . . . 7 (dom 𝑢 ∩ ((0..^𝑁) ∖ dom 𝑢)) = ∅
7473a1i 11 . . . . . 6 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (dom 𝑢 ∩ ((0..^𝑁) ∖ dom 𝑢)) = ∅)
75 disjdif 4369 . . . . . . 7 (ran 𝑢 ∩ (𝐷 ∖ ran 𝑢)) = ∅
7675a1i 11 . . . . . 6 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (ran 𝑢 ∩ (𝐷 ∖ ran 𝑢)) = ∅)
77 f1oun 6622 . . . . . 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 838 . . . . 5 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (𝑢𝑓):(dom 𝑢 ∪ ((0..^𝑁) ∖ dom 𝑢))–1-1-onto→(ran 𝑢 ∪ (𝐷 ∖ ran 𝑢)))
79 eqidd 2760 . . . . . 6 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (𝑢𝑓) = (𝑢𝑓))
8060adantr 485 . . . . . . 7 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → dom 𝑢 ⊆ (0..^𝑁))
81 undif 4379 . . . . . . 7 (dom 𝑢 ⊆ (0..^𝑁) ↔ (dom 𝑢 ∪ ((0..^𝑁) ∖ dom 𝑢)) = (0..^𝑁))
8280, 81sylib 221 . . . . . 6 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (dom 𝑢 ∪ ((0..^𝑁) ∖ dom 𝑢)) = (0..^𝑁))
83 undif 4379 . . . . . . . 8 (ran 𝑢𝐷 ↔ (ran 𝑢 ∪ (𝐷 ∖ ran 𝑢)) = 𝐷)
8450, 83sylib 221 . . . . . . 7 (((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) → (ran 𝑢 ∪ (𝐷 ∖ ran 𝑢)) = 𝐷)
8584adantr 485 . . . . . 6 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (ran 𝑢 ∪ (𝐷 ∖ ran 𝑢)) = 𝐷)
8679, 82, 85f1oeq123d 6597 . . . . 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 235 . . . 4 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (𝑢𝑓):(0..^𝑁)–1-1-onto𝐷)
88 f1ocnv 6615 . . . . . . . . . 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 30947 . . . . . . . . . . . . 13 ((𝐷 ∈ Fin ∧ 𝑃 ∈ (0...𝑁)) → 𝐶𝐵)
964, 90, 95syl2anc 588 . . . . . . . . . . . 12 (𝜑𝐶𝐵)
97 cycpmconjs.q . . . . . . . . . . . 12 (𝜑𝑄𝐶)
9896, 97sseldd 3894 . . . . . . . . . . 11 (𝜑𝑄𝐵)
9992, 94symgbasf1o 18571 . . . . . . . . . . 11 (𝑄𝐵𝑄:𝐷1-1-onto𝐷)
10098, 99syl 17 . . . . . . . . . 10 (𝜑𝑄:𝐷1-1-onto𝐷)
101100ad3antrrr 730 . . . . . . . . 9 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → 𝑄:𝐷1-1-onto𝐷)
102 f1oco 6625 . . . . . . . . 9 (((𝑢𝑓):𝐷1-1-onto→(0..^𝑁) ∧ 𝑄:𝐷1-1-onto𝐷) → ((𝑢𝑓) ∘ 𝑄):𝐷1-1-onto→(0..^𝑁))
10389, 101, 102syl2anc 588 . . . . . . . 8 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((𝑢𝑓) ∘ 𝑄):𝐷1-1-onto→(0..^𝑁))
104 f1oco 6625 . . . . . . . 8 ((((𝑢𝑓) ∘ 𝑄):𝐷1-1-onto→(0..^𝑁) ∧ (𝑢𝑓):(0..^𝑁)–1-1-onto𝐷) → (((𝑢𝑓) ∘ 𝑄) ∘ (𝑢𝑓)):(0..^𝑁)–1-1-onto→(0..^𝑁))
105103, 87, 104syl2anc 588 . . . . . . 7 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (((𝑢𝑓) ∘ 𝑄) ∘ (𝑢𝑓)):(0..^𝑁)–1-1-onto→(0..^𝑁))
106 f1ofun 6605 . . . . . . 7 ((((𝑢𝑓) ∘ 𝑄) ∘ (𝑢𝑓)):(0..^𝑁)–1-1-onto→(0..^𝑁) → Fun (((𝑢𝑓) ∘ 𝑄) ∘ (𝑢𝑓)))
107 funrel 6353 . . . . . . 7 (Fun (((𝑢𝑓) ∘ 𝑄) ∘ (𝑢𝑓)) → Rel (((𝑢𝑓) ∘ 𝑄) ∘ (𝑢𝑓)))
108105, 106, 1073syl 18 . . . . . 6 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → Rel (((𝑢𝑓) ∘ 𝑄) ∘ (𝑢𝑓)))
109 f1odm 6607 . . . . . . . 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 13120 . . . . . . . . 9 (𝑃 ∈ (0...𝑁) → (0..^𝑁) = ((0..^𝑃) ∪ (𝑃..^𝑁)))
11290, 111syl 17 . . . . . . . 8 (𝜑 → (0..^𝑁) = ((0..^𝑃) ∪ (𝑃..^𝑁)))
113112ad3antrrr 730 . . . . . . 7 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (0..^𝑁) = ((0..^𝑃) ∪ (𝑃..^𝑁)))
114110, 113eqtrd 2794 . . . . . 6 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → dom (((𝑢𝑓) ∘ 𝑄) ∘ (𝑢𝑓)) = ((0..^𝑃) ∪ (𝑃..^𝑁)))
115 fzodisj 13121 . . . . . . 7 ((0..^𝑃) ∩ (𝑃..^𝑁)) = ∅
116 reldisjun 30465 . . . . . . 7 ((Rel (((𝑢𝑓) ∘ 𝑄) ∘ (𝑢𝑓)) ∧ dom (((𝑢𝑓) ∘ 𝑄) ∘ (𝑢𝑓)) = ((0..^𝑃) ∪ (𝑃..^𝑁)) ∧ ((0..^𝑃) ∩ (𝑃..^𝑁)) = ∅) → (((𝑢𝑓) ∘ 𝑄) ∘ (𝑢𝑓)) = (((((𝑢𝑓) ∘ 𝑄) ∘ (𝑢𝑓)) ↾ (0..^𝑃)) ∪ ((((𝑢𝑓) ∘ 𝑄) ∘ (𝑢𝑓)) ↾ (𝑃..^𝑁))))
117115, 116mp3an3 1448 . . . . . 6 ((Rel (((𝑢𝑓) ∘ 𝑄) ∘ (𝑢𝑓)) ∧ dom (((𝑢𝑓) ∘ 𝑄) ∘ (𝑢𝑓)) = ((0..^𝑃) ∪ (𝑃..^𝑁))) → (((𝑢𝑓) ∘ 𝑄) ∘ (𝑢𝑓)) = (((((𝑢𝑓) ∘ 𝑄) ∘ (𝑢𝑓)) ↾ (0..^𝑃)) ∪ ((((𝑢𝑓) ∘ 𝑄) ∘ (𝑢𝑓)) ↾ (𝑃..^𝑁))))
118108, 114, 117syl2anc 588 . . . . 5 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (((𝑢𝑓) ∘ 𝑄) ∘ (𝑢𝑓)) = (((((𝑢𝑓) ∘ 𝑄) ∘ (𝑢𝑓)) ↾ (0..^𝑃)) ∪ ((((𝑢𝑓) ∘ 𝑄) ∘ (𝑢𝑓)) ↾ (𝑃..^𝑁))))
119 resco 6081 . . . . . . . 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 13928 . . . . . . . . . . . 12 (𝑢 ∈ Word 𝐷𝑢 Fn (0..^(♯‘𝑢)))
123121, 122syl 17 . . . . . . . . . . 11 (((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) → 𝑢 Fn (0..^(♯‘𝑢)))
12416elin2d 4105 . . . . . . . . . . . . . 14 (((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) → 𝑢 ∈ (♯ “ {𝑃}))
125 hashf 13749 . . . . . . . . . . . . . . . 16 ♯:V⟶(ℕ0 ∪ {+∞})
126 ffn 6499 . . . . . . . . . . . . . . . 16 (♯:V⟶(ℕ0 ∪ {+∞}) → ♯ Fn V)
127 fniniseg 6822 . . . . . . . . . . . . . . . 16 (♯ Fn V → (𝑢 ∈ (♯ “ {𝑃}) ↔ (𝑢 ∈ V ∧ (♯‘𝑢) = 𝑃)))
128125, 126, 127mp2b 10 . . . . . . . . . . . . . . 15 (𝑢 ∈ (♯ “ {𝑃}) ↔ (𝑢 ∈ V ∧ (♯‘𝑢) = 𝑃))
129128simprbi 501 . . . . . . . . . . . . . 14 (𝑢 ∈ (♯ “ {𝑃}) → (♯‘𝑢) = 𝑃)
130124, 129syl 17 . . . . . . . . . . . . 13 (((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) → (♯‘𝑢) = 𝑃)
131130oveq2d 7167 . . . . . . . . . . . 12 (((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) → (0..^(♯‘𝑢)) = (0..^𝑃))
132131fneq2d 6429 . . . . . . . . . . 11 (((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) → (𝑢 Fn (0..^(♯‘𝑢)) ↔ 𝑢 Fn (0..^𝑃)))
133123, 132mpbid 235 . . . . . . . . . 10 (((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) → 𝑢 Fn (0..^𝑃))
134133adantr 485 . . . . . . . . 9 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → 𝑢 Fn (0..^𝑃))
135 f1ofn 6604 . . . . . . . . . 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 2794 . . . . . . . . . . . 12 (((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) → dom 𝑢 = (0..^𝑃))
138137ineq1d 4117 . . . . . . . . . . 11 (((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) → (dom 𝑢 ∩ ((0..^𝑁) ∖ dom 𝑢)) = ((0..^𝑃) ∩ ((0..^𝑁) ∖ dom 𝑢)))
13973a1i 11 . . . . . . . . . . 11 (((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) → (dom 𝑢 ∩ ((0..^𝑁) ∖ dom 𝑢)) = ∅)
140138, 139eqtr3d 2796 . . . . . . . . . 10 (((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) → ((0..^𝑃) ∩ ((0..^𝑁) ∖ dom 𝑢)) = ∅)
141140adantr 485 . . . . . . . . 9 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((0..^𝑃) ∩ ((0..^𝑁) ∖ dom 𝑢)) = ∅)
142 fnunres1 30468 . . . . . . . . 9 ((𝑢 Fn (0..^𝑃) ∧ 𝑓 Fn ((0..^𝑁) ∖ dom 𝑢) ∧ ((0..^𝑃) ∩ ((0..^𝑁) ∖ dom 𝑢)) = ∅) → ((𝑢𝑓) ↾ (0..^𝑃)) = 𝑢)
143134, 136, 141, 142syl3anc 1369 . . . . . . . 8 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((𝑢𝑓) ↾ (0..^𝑃)) = 𝑢)
144143coeq2d 5703 . . . . . . 7 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (((𝑢𝑓) ∘ 𝑄) ∘ ((𝑢𝑓) ↾ (0..^𝑃))) = (((𝑢𝑓) ∘ 𝑄) ∘ 𝑢))
145 resco 6081 . . . . . . . . . . 11 (((𝑢𝑓) ∘ 𝑄) ↾ ran 𝑢) = ((𝑢𝑓) ∘ (𝑄 ↾ ran 𝑢))
146 resco 6081 . . . . . . . . . . . . 13 ((𝑢 ∘ (𝑀𝑢)) ↾ ran 𝑢) = (𝑢 ∘ ((𝑀𝑢) ↾ ran 𝑢))
147146a1i 11 . . . . . . . . . . . 12 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((𝑢 ∘ (𝑀𝑢)) ↾ ran 𝑢) = (𝑢 ∘ ((𝑀𝑢) ↾ ran 𝑢)))
148 cnvun 5974 . . . . . . . . . . . . . . 15 (𝑢𝑓) = (𝑢𝑓)
149148reseq1i 5820 . . . . . . . . . . . . . 14 ((𝑢𝑓) ↾ ran 𝑢) = ((𝑢𝑓) ↾ ran 𝑢)
150 f1ocnv 6615 . . . . . . . . . . . . . . . 16 (𝑢:dom 𝑢1-1-onto→ran 𝑢𝑢:ran 𝑢1-1-onto→dom 𝑢)
151 f1ofn 6604 . . . . . . . . . . . . . . . 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 6615 . . . . . . . . . . . . . . . 16 (𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢) → 𝑓:(𝐷 ∖ ran 𝑢)–1-1-onto→((0..^𝑁) ∖ dom 𝑢))
154 f1ofn 6604 . . . . . . . . . . . . . . . 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 30468 . . . . . . . . . . . . . . 15 ((𝑢 Fn ran 𝑢𝑓 Fn (𝐷 ∖ ran 𝑢) ∧ (ran 𝑢 ∩ (𝐷 ∖ ran 𝑢)) = ∅) → ((𝑢𝑓) ↾ ran 𝑢) = 𝑢)
157152, 155, 76, 156syl3anc 1369 . . . . . . . . . . . . . 14 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((𝑢𝑓) ↾ ran 𝑢) = 𝑢)
158149, 157syl5req 2807 . . . . . . . . . . . . 13 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → 𝑢 = ((𝑢𝑓) ↾ ran 𝑢))
159 simplr 769 . . . . . . . . . . . . . 14 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (𝑀𝑢) = 𝑄)
160159reseq1d 5823 . . . . . . . . . . . . 13 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((𝑀𝑢) ↾ ran 𝑢) = (𝑄 ↾ ran 𝑢))
161158, 160coeq12d 5705 . . . . . . . . . . . 12 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (𝑢 ∘ ((𝑀𝑢) ↾ ran 𝑢)) = (((𝑢𝑓) ↾ ran 𝑢) ∘ (𝑄 ↾ ran 𝑢)))
16247adantr 485 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → 𝐷 ∈ Fin)
163121adantr 485 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → 𝑢 ∈ Word 𝐷)
16493, 162, 163, 69tocycfvres1 30904 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((𝑀𝑢) ↾ ran 𝑢) = ((𝑢 cyclShift 1) ∘ 𝑢))
165160, 164eqtr3d 2796 . . . . . . . . . . . . . . . 16 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (𝑄 ↾ ran 𝑢) = ((𝑢 cyclShift 1) ∘ 𝑢))
166165rneqd 5780 . . . . . . . . . . . . . . 15 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ran (𝑄 ↾ ran 𝑢) = ran ((𝑢 cyclShift 1) ∘ 𝑢))
167 1zzd 12053 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → 1 ∈ ℤ)
168 cshf1o 30759 . . . . . . . . . . . . . . . . . 18 ((𝑢 ∈ Word 𝐷𝑢:dom 𝑢1-1𝐷 ∧ 1 ∈ ℤ) → (𝑢 cyclShift 1):dom 𝑢1-1-onto→ran 𝑢)
169163, 69, 167, 168syl3anc 1369 . . . . . . . . . . . . . . . . 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 6625 . . . . . . . . . . . . . . . . 17 (((𝑢 cyclShift 1):dom 𝑢1-1-onto→ran 𝑢𝑢:ran 𝑢1-1-onto→dom 𝑢) → ((𝑢 cyclShift 1) ∘ 𝑢):ran 𝑢1-1-onto→ran 𝑢)
172169, 170, 171syl2anc 588 . . . . . . . . . . . . . . . 16 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((𝑢 cyclShift 1) ∘ 𝑢):ran 𝑢1-1-onto→ran 𝑢)
173 f1ofo 6610 . . . . . . . . . . . . . . . 16 (((𝑢 cyclShift 1) ∘ 𝑢):ran 𝑢1-1-onto→ran 𝑢 → ((𝑢 cyclShift 1) ∘ 𝑢):ran 𝑢onto→ran 𝑢)
174 forn 6580 . . . . . . . . . . . . . . . 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 2794 . . . . . . . . . . . . . 14 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ran (𝑄 ↾ ran 𝑢) = ran 𝑢)
177 ssid 3915 . . . . . . . . . . . . . 14 ran 𝑢 ⊆ ran 𝑢
178176, 177eqsstrdi 3947 . . . . . . . . . . . . 13 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ran (𝑄 ↾ ran 𝑢) ⊆ ran 𝑢)
179 cores 6080 . . . . . . . . . . . . 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 2799 . . . . . . . . . . 11 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((𝑢𝑓) ∘ (𝑄 ↾ ran 𝑢)) = ((𝑢 ∘ (𝑀𝑢)) ↾ ran 𝑢))
182145, 181syl5eq 2806 . . . . . . . . . 10 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (((𝑢𝑓) ∘ 𝑄) ↾ ran 𝑢) = ((𝑢 ∘ (𝑀𝑢)) ↾ ran 𝑢))
183182coeq1d 5702 . . . . . . . . 9 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((((𝑢𝑓) ∘ 𝑄) ↾ ran 𝑢) ∘ 𝑢) = (((𝑢 ∘ (𝑀𝑢)) ↾ ran 𝑢) ∘ 𝑢))
184 cores 6080 . . . . . . . . . 10 (ran 𝑢 ⊆ ran 𝑢 → (((𝑢 ∘ (𝑀𝑢)) ↾ ran 𝑢) ∘ 𝑢) = ((𝑢 ∘ (𝑀𝑢)) ∘ 𝑢))
185177, 184mp1i 13 . . . . . . . . 9 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (((𝑢 ∘ (𝑀𝑢)) ↾ ran 𝑢) ∘ 𝑢) = ((𝑢 ∘ (𝑀𝑢)) ∘ 𝑢))
186183, 185eqtrd 2794 . . . . . . . 8 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((((𝑢𝑓) ∘ 𝑄) ↾ ran 𝑢) ∘ 𝑢) = ((𝑢 ∘ (𝑀𝑢)) ∘ 𝑢))
187 cores 6080 . . . . . . . . 9 (ran 𝑢 ⊆ ran 𝑢 → ((((𝑢𝑓) ∘ 𝑄) ↾ ran 𝑢) ∘ 𝑢) = (((𝑢𝑓) ∘ 𝑄) ∘ 𝑢))
188177, 187mp1i 13 . . . . . . . 8 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((((𝑢𝑓) ∘ 𝑄) ↾ ran 𝑢) ∘ 𝑢) = (((𝑢𝑓) ∘ 𝑄) ∘ 𝑢))
189130adantr 485 . . . . . . . . 9 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (♯‘𝑢) = 𝑃)
19091, 92, 8, 93, 162, 163, 69, 189cycpmconjslem1 30948 . . . . . . . 8 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((𝑢 ∘ (𝑀𝑢)) ∘ 𝑢) = (( I ↾ (0..^𝑃)) cyclShift 1))
191186, 188, 1903eqtr3d 2802 . . . . . . 7 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (((𝑢𝑓) ∘ 𝑄) ∘ 𝑢) = (( I ↾ (0..^𝑃)) cyclShift 1))
192120, 144, 1913eqtrd 2798 . . . . . 6 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((((𝑢𝑓) ∘ 𝑄) ∘ (𝑢𝑓)) ↾ (0..^𝑃)) = (( I ↾ (0..^𝑃)) cyclShift 1))
193 resco 6081 . . . . . . . 8 ((((𝑢𝑓) ∘ 𝑄) ∘ (𝑢𝑓)) ↾ (𝑃..^𝑁)) = (((𝑢𝑓) ∘ 𝑄) ∘ ((𝑢𝑓) ↾ (𝑃..^𝑁)))
194137adantr 485 . . . . . . . . . . . . 13 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → dom 𝑢 = (0..^𝑃))
195194difeq2d 4029 . . . . . . . . . . . 12 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((0..^𝑁) ∖ dom 𝑢) = ((0..^𝑁) ∖ (0..^𝑃)))
196 fzodif1 30639 . . . . . . . . . . . . . 14 (𝑃 ∈ (0...𝑁) → ((0..^𝑁) ∖ (0..^𝑃)) = (𝑃..^𝑁))
19790, 196syl 17 . . . . . . . . . . . . 13 (𝜑 → ((0..^𝑁) ∖ (0..^𝑃)) = (𝑃..^𝑁))
198197ad3antrrr 730 . . . . . . . . . . . 12 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((0..^𝑁) ∖ (0..^𝑃)) = (𝑃..^𝑁))
199195, 198eqtrd 2794 . . . . . . . . . . 11 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((0..^𝑁) ∖ dom 𝑢) = (𝑃..^𝑁))
200199reseq2d 5824 . . . . . . . . . 10 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((𝑢𝑓) ↾ ((0..^𝑁) ∖ dom 𝑢)) = ((𝑢𝑓) ↾ (𝑃..^𝑁)))
201 fnunres2 30540 . . . . . . . . . . 11 ((𝑢 Fn (0..^𝑃) ∧ 𝑓 Fn ((0..^𝑁) ∖ dom 𝑢) ∧ ((0..^𝑃) ∩ ((0..^𝑁) ∖ dom 𝑢)) = ∅) → ((𝑢𝑓) ↾ ((0..^𝑁) ∖ dom 𝑢)) = 𝑓)
202134, 136, 141, 201syl3anc 1369 . . . . . . . . . 10 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((𝑢𝑓) ↾ ((0..^𝑁) ∖ dom 𝑢)) = 𝑓)
203200, 202eqtr3d 2796 . . . . . . . . 9 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((𝑢𝑓) ↾ (𝑃..^𝑁)) = 𝑓)
204203coeq2d 5703 . . . . . . . 8 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (((𝑢𝑓) ∘ 𝑄) ∘ ((𝑢𝑓) ↾ (𝑃..^𝑁))) = (((𝑢𝑓) ∘ 𝑄) ∘ 𝑓))
205193, 204syl5eq 2806 . . . . . . 7 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((((𝑢𝑓) ∘ 𝑄) ∘ (𝑢𝑓)) ↾ (𝑃..^𝑁)) = (((𝑢𝑓) ∘ 𝑄) ∘ 𝑓))
206148reseq1i 5820 . . . . . . . . . . . 12 ((𝑢𝑓) ↾ (𝐷 ∖ ran 𝑢)) = ((𝑢𝑓) ↾ (𝐷 ∖ ran 𝑢))
207 fnunres2 30540 . . . . . . . . . . . . 13 ((𝑢 Fn ran 𝑢𝑓 Fn (𝐷 ∖ ran 𝑢) ∧ (ran 𝑢 ∩ (𝐷 ∖ ran 𝑢)) = ∅) → ((𝑢𝑓) ↾ (𝐷 ∖ ran 𝑢)) = 𝑓)
208152, 155, 76, 207syl3anc 1369 . . . . . . . . . . . 12 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((𝑢𝑓) ↾ (𝐷 ∖ ran 𝑢)) = 𝑓)
209206, 208syl5eq 2806 . . . . . . . . . . 11 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((𝑢𝑓) ↾ (𝐷 ∖ ran 𝑢)) = 𝑓)
210159reseq1d 5823 . . . . . . . . . . . 12 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((𝑀𝑢) ↾ (𝐷 ∖ ran 𝑢)) = (𝑄 ↾ (𝐷 ∖ ran 𝑢)))
21193, 162, 163, 69tocycfvres2 30905 . . . . . . . . . . . 12 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((𝑀𝑢) ↾ (𝐷 ∖ ran 𝑢)) = ( I ↾ (𝐷 ∖ ran 𝑢)))
212210, 211eqtr3d 2796 . . . . . . . . . . 11 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (𝑄 ↾ (𝐷 ∖ ran 𝑢)) = ( I ↾ (𝐷 ∖ ran 𝑢)))
213209, 212coeq12d 5705 . . . . . . . . . 10 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (((𝑢𝑓) ↾ (𝐷 ∖ ran 𝑢)) ∘ (𝑄 ↾ (𝐷 ∖ ran 𝑢))) = (𝑓 ∘ ( I ↾ (𝐷 ∖ ran 𝑢))))
214212rneqd 5780 . . . . . . . . . . . . 13 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ran (𝑄 ↾ (𝐷 ∖ ran 𝑢)) = ran ( I ↾ (𝐷 ∖ ran 𝑢)))
215 rnresi 5916 . . . . . . . . . . . . . 14 ran ( I ↾ (𝐷 ∖ ran 𝑢)) = (𝐷 ∖ ran 𝑢)
216215eqimssi 3951 . . . . . . . . . . . . 13 ran ( I ↾ (𝐷 ∖ ran 𝑢)) ⊆ (𝐷 ∖ ran 𝑢)
217214, 216eqsstrdi 3947 . . . . . . . . . . . 12 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ran (𝑄 ↾ (𝐷 ∖ ran 𝑢)) ⊆ (𝐷 ∖ ran 𝑢))
218 cores 6080 . . . . . . . . . . . 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 6081 . . . . . . . . . . 11 (((𝑢𝑓) ∘ 𝑄) ↾ (𝐷 ∖ ran 𝑢)) = ((𝑢𝑓) ∘ (𝑄 ↾ (𝐷 ∖ ran 𝑢)))
221219, 220eqtr4di 2812 . . . . . . . . . 10 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (((𝑢𝑓) ↾ (𝐷 ∖ ran 𝑢)) ∘ (𝑄 ↾ (𝐷 ∖ ran 𝑢))) = (((𝑢𝑓) ∘ 𝑄) ↾ (𝐷 ∖ ran 𝑢)))
222213, 221eqtr3d 2796 . . . . . . . . 9 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (𝑓 ∘ ( I ↾ (𝐷 ∖ ran 𝑢))) = (((𝑢𝑓) ∘ 𝑄) ↾ (𝐷 ∖ ran 𝑢)))
223222coeq1d 5702 . . . . . . . 8 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((𝑓 ∘ ( I ↾ (𝐷 ∖ ran 𝑢))) ∘ 𝑓) = ((((𝑢𝑓) ∘ 𝑄) ↾ (𝐷 ∖ ran 𝑢)) ∘ 𝑓))
224 f1of 6603 . . . . . . . . . . . 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 6538 . . . . . . . . . . 11 (𝑓:(𝐷 ∖ ran 𝑢)⟶((0..^𝑁) ∖ dom 𝑢) → (𝑓 ∘ ( I ↾ (𝐷 ∖ ran 𝑢))) = 𝑓)
227225, 226syl 17 . . . . . . . . . 10 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (𝑓 ∘ ( I ↾ (𝐷 ∖ ran 𝑢))) = 𝑓)
228227coeq1d 5702 . . . . . . . . 9 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((𝑓 ∘ ( I ↾ (𝐷 ∖ ran 𝑢))) ∘ 𝑓) = (𝑓𝑓))
229 f1ococnv1 6631 . . . . . . . . . 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 5824 . . . . . . . . 9 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ( I ↾ ((0..^𝑁) ∖ dom 𝑢)) = ( I ↾ (𝑃..^𝑁)))
232228, 230, 2313eqtrd 2798 . . . . . . . 8 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((𝑓 ∘ ( I ↾ (𝐷 ∖ ran 𝑢))) ∘ 𝑓) = ( I ↾ (𝑃..^𝑁)))
233 f1of 6603 . . . . . . . . . 10 (𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢) → 𝑓:((0..^𝑁) ∖ dom 𝑢)⟶(𝐷 ∖ ran 𝑢))
234 frn 6505 . . . . . . . . . 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 6080 . . . . . . . . 9 (ran 𝑓 ⊆ (𝐷 ∖ ran 𝑢) → ((((𝑢𝑓) ∘ 𝑄) ↾ (𝐷 ∖ ran 𝑢)) ∘ 𝑓) = (((𝑢𝑓) ∘ 𝑄) ∘ 𝑓))
237235, 236syl 17 . . . . . . . 8 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((((𝑢𝑓) ∘ 𝑄) ↾ (𝐷 ∖ ran 𝑢)) ∘ 𝑓) = (((𝑢𝑓) ∘ 𝑄) ∘ 𝑓))
238223, 232, 2373eqtr3rd 2803 . . . . . . 7 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (((𝑢𝑓) ∘ 𝑄) ∘ 𝑓) = ( I ↾ (𝑃..^𝑁)))
239205, 238eqtrd 2794 . . . . . 6 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ((((𝑢𝑓) ∘ 𝑄) ∘ (𝑢𝑓)) ↾ (𝑃..^𝑁)) = ( I ↾ (𝑃..^𝑁)))
240192, 239uneq12d 4070 . . . . 5 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (((((𝑢𝑓) ∘ 𝑄) ∘ (𝑢𝑓)) ↾ (0..^𝑃)) ∪ ((((𝑢𝑓) ∘ 𝑄) ∘ (𝑢𝑓)) ↾ (𝑃..^𝑁))) = ((( I ↾ (0..^𝑃)) cyclShift 1) ∪ ( I ↾ (𝑃..^𝑁))))
241118, 240eqtrd 2794 . . . 4 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → (((𝑢𝑓) ∘ 𝑄) ∘ (𝑢𝑓)) = ((( I ↾ (0..^𝑃)) cyclShift 1) ∪ ( I ↾ (𝑃..^𝑁))))
242 vex 3414 . . . . . 6 𝑢 ∈ V
243 vex 3414 . . . . . 6 𝑓 ∈ V
244242, 243unex 7468 . . . . 5 (𝑢𝑓) ∈ V
245 f1oeq1 6591 . . . . . 6 (𝑞 = (𝑢𝑓) → (𝑞:(0..^𝑁)–1-1-onto𝐷 ↔ (𝑢𝑓):(0..^𝑁)–1-1-onto𝐷))
246 cnveq 5714 . . . . . . . . 9 (𝑞 = (𝑢𝑓) → 𝑞 = (𝑢𝑓))
247246coeq1d 5702 . . . . . . . 8 (𝑞 = (𝑢𝑓) → (𝑞𝑄) = ((𝑢𝑓) ∘ 𝑄))
248 id 22 . . . . . . . 8 (𝑞 = (𝑢𝑓) → 𝑞 = (𝑢𝑓))
249247, 248coeq12d 5705 . . . . . . 7 (𝑞 = (𝑢𝑓) → ((𝑞𝑄) ∘ 𝑞) = (((𝑢𝑓) ∘ 𝑄) ∘ (𝑢𝑓)))
250249eqeq1d 2761 . . . . . 6 (𝑞 = (𝑢𝑓) → (((𝑞𝑄) ∘ 𝑞) = ((( I ↾ (0..^𝑃)) cyclShift 1) ∪ ( I ↾ (𝑃..^𝑁))) ↔ (((𝑢𝑓) ∘ 𝑄) ∘ (𝑢𝑓)) = ((( I ↾ (0..^𝑃)) cyclShift 1) ∪ ( I ↾ (𝑃..^𝑁)))))
251245, 250anbi12d 634 . . . . 5 (𝑞 = (𝑢𝑓) → ((𝑞:(0..^𝑁)–1-1-onto𝐷 ∧ ((𝑞𝑄) ∘ 𝑞) = ((( I ↾ (0..^𝑃)) cyclShift 1) ∪ ( I ↾ (𝑃..^𝑁)))) ↔ ((𝑢𝑓):(0..^𝑁)–1-1-onto𝐷 ∧ (((𝑢𝑓) ∘ 𝑄) ∘ (𝑢𝑓)) = ((( I ↾ (0..^𝑃)) cyclShift 1) ∪ ( I ↾ (𝑃..^𝑁))))))
252244, 251spcev 3526 . . . 4 (((𝑢𝑓):(0..^𝑁)–1-1-onto𝐷 ∧ (((𝑢𝑓) ∘ 𝑄) ∘ (𝑢𝑓)) = ((( I ↾ (0..^𝑃)) cyclShift 1) ∪ ( I ↾ (𝑃..^𝑁)))) → ∃𝑞(𝑞:(0..^𝑁)–1-1-onto𝐷 ∧ ((𝑞𝑄) ∘ 𝑞) = ((( I ↾ (0..^𝑃)) cyclShift 1) ∪ ( I ↾ (𝑃..^𝑁)))))
25387, 241, 252syl2anc 588 . . 3 ((((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) ∧ 𝑓:((0..^𝑁) ∖ dom 𝑢)–1-1-onto→(𝐷 ∖ ran 𝑢)) → ∃𝑞(𝑞:(0..^𝑁)–1-1-onto𝐷 ∧ ((𝑞𝑄) ∘ 𝑞) = ((( I ↾ (0..^𝑃)) cyclShift 1) ∪ ( I ↾ (𝑃..^𝑁)))))
25468, 253exlimddv 1937 . 2 (((𝜑𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))) ∧ (𝑀𝑢) = 𝑄) → ∃𝑞(𝑞:(0..^𝑁)–1-1-onto𝐷 ∧ ((𝑞𝑄) ∘ 𝑞) = ((( I ↾ (0..^𝑃)) cyclShift 1) ∪ ( I ↾ (𝑃..^𝑁)))))
255 nfcv 2920 . . 3 𝑢𝑀
25693, 92, 94tocycf 30911 . . . 4 (𝐷 ∈ Fin → 𝑀:{𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷}⟶𝐵)
257 ffn 6499 . . . 4 (𝑀:{𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷}⟶𝐵𝑀 Fn {𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷})
2584, 256, 2573syl 18 . . 3 (𝜑𝑀 Fn {𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷})
25997, 91eleqtrdi 2863 . . 3 (𝜑𝑄 ∈ (𝑀 “ (♯ “ {𝑃})))
260255, 258, 259fvelimad 6721 . 2 (𝜑 → ∃𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {𝑃}))(𝑀𝑢) = 𝑄)
261254, 260r19.29a 3214 1 (𝜑 → ∃𝑞(𝑞:(0..^𝑁)–1-1-onto𝐷 ∧ ((𝑞𝑄) ∘ 𝑞) = ((( I ↾ (0..^𝑃)) cyclShift 1) ∪ ( I ↾ (𝑃..^𝑁)))))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   = wceq 1539  ∃wex 1782   ∈ wcel 2112  {crab 3075  Vcvv 3410   ∖ cdif 3856   ∪ cun 3857   ∩ cin 3858   ⊆ wss 3859  ∅c0 4226  {csn 4523   class class class wbr 5033   I cid 5430  ◡ccnv 5524  dom cdm 5525  ran crn 5526   ↾ cres 5527   “ cima 5528   ∘ ccom 5529  Rel wrel 5530  Fun wfun 6330   Fn wfn 6331  ⟶wf 6332  –1-1→wf1 6333  –onto→wfo 6334  –1-1-onto→wf1o 6335  ‘cfv 6336  (class class class)co 7151  Fincfn 8528  0cc0 10576  1c1 10577  +∞cpnf 10711   ≤ cle 10715   − cmin 10909  ℕ0cn0 11935  ℤcz 12021  ℤ≥cuz 12283  ...cfz 12940  ..^cfzo 13083  ♯chash 13741  Word cword 13914   cyclShift ccsh 14198  Basecbs 16542  +gcplusg 16624  -gcsg 18172  SymGrpcsymg 18563  toCycctocyc 30900 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2730  ax-rep 5157  ax-sep 5170  ax-nul 5177  ax-pow 5235  ax-pr 5299  ax-un 7460  ax-cnex 10632  ax-resscn 10633  ax-1cn 10634  ax-icn 10635  ax-addcl 10636  ax-addrcl 10637  ax-mulcl 10638  ax-mulrcl 10639  ax-mulcom 10640  ax-addass 10641  ax-mulass 10642  ax-distr 10643  ax-i2m1 10644  ax-1ne0 10645  ax-1rid 10646  ax-rnegex 10647  ax-rrecex 10648  ax-cnre 10649  ax-pre-lttri 10650  ax-pre-lttrn 10651  ax-pre-ltadd 10652  ax-pre-mulgt0 10653  ax-pre-sup 10654 This theorem depends on definitions:  df-bi 210  df-an 401  df-or 846  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2071  df-mo 2558  df-eu 2589  df-clab 2737  df-cleq 2751  df-clel 2831  df-nfc 2902  df-ne 2953  df-nel 3057  df-ral 3076  df-rex 3077  df-reu 3078  df-rmo 3079  df-rab 3080  df-v 3412  df-sbc 3698  df-csb 3807  df-dif 3862  df-un 3864  df-in 3866  df-ss 3876  df-pss 3878  df-nul 4227  df-if 4422  df-pw 4497  df-sn 4524  df-pr 4526  df-tp 4528  df-op 4530  df-uni 4800  df-int 4840  df-iun 4886  df-br 5034  df-opab 5096  df-mpt 5114  df-tr 5140  df-id 5431  df-eprel 5436  df-po 5444  df-so 5445  df-fr 5484  df-we 5486  df-xp 5531  df-rel 5532  df-cnv 5533  df-co 5534  df-dm 5535  df-rn 5536  df-res 5537  df-ima 5538  df-pred 6127  df-ord 6173  df-on 6174  df-lim 6175  df-suc 6176  df-iota 6295  df-fun 6338  df-fn 6339  df-f 6340  df-f1 6341  df-fo 6342  df-f1o 6343  df-fv 6344  df-riota 7109  df-ov 7154  df-oprab 7155  df-mpo 7156  df-om 7581  df-1st 7694  df-2nd 7695  df-wrecs 7958  df-recs 8019  df-rdg 8057  df-1o 8113  df-oadd 8117  df-er 8300  df-map 8419  df-en 8529  df-dom 8530  df-sdom 8531  df-fin 8532  df-sup 8940  df-inf 8941  df-dju 9364  df-card 9402  df-pnf 10716  df-mnf 10717  df-xr 10718  df-ltxr 10719  df-le 10720  df-sub 10911  df-neg 10912  df-div 11337  df-nn 11676  df-2 11738  df-3 11739  df-4 11740  df-5 11741  df-6 11742  df-7 11743  df-8 11744  df-9 11745  df-n0 11936  df-xnn0 12008  df-z 12022  df-uz 12284  df-rp 12432  df-fz 12941  df-fzo 13084  df-fl 13212  df-mod 13288  df-hash 13742  df-word 13915  df-concat 13971  df-substr 14051  df-pfx 14081  df-csh 14199  df-struct 16544  df-ndx 16545  df-slot 16546  df-base 16548  df-sets 16549  df-ress 16550  df-plusg 16637  df-tset 16643  df-efmnd 18101  df-symg 18564  df-tocyc 30901 This theorem is referenced by:  cycpmconjs  30950
 Copyright terms: Public domain W3C validator