Metamath Proof Explorer

Theorem cycpmconjs

Description: All cycles of the same length are conjugate in the symmetric group. (Contributed by Thierry Arnoux, 14-Oct-2023)

Ref Expression
Hypotheses 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 ⊢ ( 𝜑 → 𝑄 ∈ 𝐶 )
cycpmconjs.t ⊢ ( 𝜑 → 𝑇 ∈ 𝐶 )
Assertion cycpmconjs ( 𝜑 → ∃ 𝑝 ∈ 𝐵 𝑄 = ( ( 𝑝 + 𝑇 ) − 𝑝 ) )

Proof

Step Hyp Ref Expression
1 cycpmconjs.c ⊢ 𝐶 = ( 𝑀 “ ( ◡ ♯ “ { 𝑃 } ) )
2 cycpmconjs.s ⊢ 𝑆 = ( SymGrp ‘ 𝐷 )
3 cycpmconjs.n ⊢ 𝑁 = ( ♯ ‘ 𝐷 )
4 cycpmconjs.m ⊢ 𝑀 = ( toCyc ‘ 𝐷 )
5 cycpmconjs.b ⊢ 𝐵 = ( Base ‘ 𝑆 )
6 cycpmconjs.a ⊢ + = ( +g ‘ 𝑆 )
7 cycpmconjs.l ⊢ − = ( -g ‘ 𝑆 )
8 cycpmconjs.p ⊢ ( 𝜑 → 𝑃 ∈ ( 0 ... 𝑁 ) )
9 cycpmconjs.d ⊢ ( 𝜑 → 𝐷 ∈ Fin )
10 cycpmconjs.q ⊢ ( 𝜑 → 𝑄 ∈ 𝐶 )
11 cycpmconjs.t ⊢ ( 𝜑 → 𝑇 ∈ 𝐶 )
12 1 2 3 4 5 6 7 8 9 10 cycpmconjslem2 ⊢ ( 𝜑 → ∃ 𝑞 ( 𝑞 : ( 0 ..^ 𝑁 ) –1-1-onto→ 𝐷 ∧ ( ( ◡ 𝑞 ∘ 𝑄 ) ∘ 𝑞 ) = ( ( ( I ↾ ( 0 ..^ 𝑃 ) ) cyclShift 1 ) ∪ ( I ↾ ( 𝑃 ..^ 𝑁 ) ) ) ) )
13 1 2 3 4 5 6 7 8 9 11 cycpmconjslem2 ⊢ ( 𝜑 → ∃ 𝑡 ( 𝑡 : ( 0 ..^ 𝑁 ) –1-1-onto→ 𝐷 ∧ ( ( ◡ 𝑡 ∘ 𝑇 ) ∘ 𝑡 ) = ( ( ( I ↾ ( 0 ..^ 𝑃 ) ) cyclShift 1 ) ∪ ( I ↾ ( 𝑃 ..^ 𝑁 ) ) ) ) )
14 13 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑞 : ( 0 ..^ 𝑁 ) –1-1-onto→ 𝐷 ) ∧ ( ( ◡ 𝑞 ∘ 𝑄 ) ∘ 𝑞 ) = ( ( ( I ↾ ( 0 ..^ 𝑃 ) ) cyclShift 1 ) ∪ ( I ↾ ( 𝑃 ..^ 𝑁 ) ) ) ) → ∃ 𝑡 ( 𝑡 : ( 0 ..^ 𝑁 ) –1-1-onto→ 𝐷 ∧ ( ( ◡ 𝑡 ∘ 𝑇 ) ∘ 𝑡 ) = ( ( ( I ↾ ( 0 ..^ 𝑃 ) ) cyclShift 1 ) ∪ ( I ↾ ( 𝑃 ..^ 𝑁 ) ) ) ) )
15 9 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑞 : ( 0 ..^ 𝑁 ) –1-1-onto→ 𝐷 ) ∧ ( ( ◡ 𝑞 ∘ 𝑄 ) ∘ 𝑞 ) = ( ( ( I ↾ ( 0 ..^ 𝑃 ) ) cyclShift 1 ) ∪ ( I ↾ ( 𝑃 ..^ 𝑁 ) ) ) ) ∧ 𝑡 : ( 0 ..^ 𝑁 ) –1-1-onto→ 𝐷 ) ∧ ( ( ◡ 𝑡 ∘ 𝑇 ) ∘ 𝑡 ) = ( ( ( I ↾ ( 0 ..^ 𝑃 ) ) cyclShift 1 ) ∪ ( I ↾ ( 𝑃 ..^ 𝑁 ) ) ) ) → 𝐷 ∈ Fin )
16 simp-4r ⊢ ( ( ( ( ( 𝜑 ∧ 𝑞 : ( 0 ..^ 𝑁 ) –1-1-onto→ 𝐷 ) ∧ ( ( ◡ 𝑞 ∘ 𝑄 ) ∘ 𝑞 ) = ( ( ( I ↾ ( 0 ..^ 𝑃 ) ) cyclShift 1 ) ∪ ( I ↾ ( 𝑃 ..^ 𝑁 ) ) ) ) ∧ 𝑡 : ( 0 ..^ 𝑁 ) –1-1-onto→ 𝐷 ) ∧ ( ( ◡ 𝑡 ∘ 𝑇 ) ∘ 𝑡 ) = ( ( ( I ↾ ( 0 ..^ 𝑃 ) ) cyclShift 1 ) ∪ ( I ↾ ( 𝑃 ..^ 𝑁 ) ) ) ) → 𝑞 : ( 0 ..^ 𝑁 ) –1-1-onto→ 𝐷 )
17 f1ocnv ⊢ ( 𝑡 : ( 0 ..^ 𝑁 ) –1-1-onto→ 𝐷 → ◡ 𝑡 : 𝐷 –1-1-onto→ ( 0 ..^ 𝑁 ) )
18 17 ad2antlr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑞 : ( 0 ..^ 𝑁 ) –1-1-onto→ 𝐷 ) ∧ ( ( ◡ 𝑞 ∘ 𝑄 ) ∘ 𝑞 ) = ( ( ( I ↾ ( 0 ..^ 𝑃 ) ) cyclShift 1 ) ∪ ( I ↾ ( 𝑃 ..^ 𝑁 ) ) ) ) ∧ 𝑡 : ( 0 ..^ 𝑁 ) –1-1-onto→ 𝐷 ) ∧ ( ( ◡ 𝑡 ∘ 𝑇 ) ∘ 𝑡 ) = ( ( ( I ↾ ( 0 ..^ 𝑃 ) ) cyclShift 1 ) ∪ ( I ↾ ( 𝑃 ..^ 𝑁 ) ) ) ) → ◡ 𝑡 : 𝐷 –1-1-onto→ ( 0 ..^ 𝑁 ) )
19 f1oco ⊢ ( ( 𝑞 : ( 0 ..^ 𝑁 ) –1-1-onto→ 𝐷 ∧ ◡ 𝑡 : 𝐷 –1-1-onto→ ( 0 ..^ 𝑁 ) ) → ( 𝑞 ∘ ◡ 𝑡 ) : 𝐷 –1-1-onto→ 𝐷 )
20 16 18 19 syl2anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑞 : ( 0 ..^ 𝑁 ) –1-1-onto→ 𝐷 ) ∧ ( ( ◡ 𝑞 ∘ 𝑄 ) ∘ 𝑞 ) = ( ( ( I ↾ ( 0 ..^ 𝑃 ) ) cyclShift 1 ) ∪ ( I ↾ ( 𝑃 ..^ 𝑁 ) ) ) ) ∧ 𝑡 : ( 0 ..^ 𝑁 ) –1-1-onto→ 𝐷 ) ∧ ( ( ◡ 𝑡 ∘ 𝑇 ) ∘ 𝑡 ) = ( ( ( I ↾ ( 0 ..^ 𝑃 ) ) cyclShift 1 ) ∪ ( I ↾ ( 𝑃 ..^ 𝑁 ) ) ) ) → ( 𝑞 ∘ ◡ 𝑡 ) : 𝐷 –1-1-onto→ 𝐷 )
21 2 5 elsymgbas ⊢ ( 𝐷 ∈ Fin → ( ( 𝑞 ∘ ◡ 𝑡 ) ∈ 𝐵 ↔ ( 𝑞 ∘ ◡ 𝑡 ) : 𝐷 –1-1-onto→ 𝐷 ) )
22 21 biimpar ⊢ ( ( 𝐷 ∈ Fin ∧ ( 𝑞 ∘ ◡ 𝑡 ) : 𝐷 –1-1-onto→ 𝐷 ) → ( 𝑞 ∘ ◡ 𝑡 ) ∈ 𝐵 )
23 15 20 22 syl2anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑞 : ( 0 ..^ 𝑁 ) –1-1-onto→ 𝐷 ) ∧ ( ( ◡ 𝑞 ∘ 𝑄 ) ∘ 𝑞 ) = ( ( ( I ↾ ( 0 ..^ 𝑃 ) ) cyclShift 1 ) ∪ ( I ↾ ( 𝑃 ..^ 𝑁 ) ) ) ) ∧ 𝑡 : ( 0 ..^ 𝑁 ) –1-1-onto→ 𝐷 ) ∧ ( ( ◡ 𝑡 ∘ 𝑇 ) ∘ 𝑡 ) = ( ( ( I ↾ ( 0 ..^ 𝑃 ) ) cyclShift 1 ) ∪ ( I ↾ ( 𝑃 ..^ 𝑁 ) ) ) ) → ( 𝑞 ∘ ◡ 𝑡 ) ∈ 𝐵 )
24 simpr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑞 : ( 0 ..^ 𝑁 ) –1-1-onto→ 𝐷 ) ∧ ( ( ◡ 𝑞 ∘ 𝑄 ) ∘ 𝑞 ) = ( ( ( I ↾ ( 0 ..^ 𝑃 ) ) cyclShift 1 ) ∪ ( I ↾ ( 𝑃 ..^ 𝑁 ) ) ) ) ∧ 𝑡 : ( 0 ..^ 𝑁 ) –1-1-onto→ 𝐷 ) ∧ ( ( ◡ 𝑡 ∘ 𝑇 ) ∘ 𝑡 ) = ( ( ( I ↾ ( 0 ..^ 𝑃 ) ) cyclShift 1 ) ∪ ( I ↾ ( 𝑃 ..^ 𝑁 ) ) ) ) ∧ 𝑝 = ( 𝑞 ∘ ◡ 𝑡 ) ) → 𝑝 = ( 𝑞 ∘ ◡ 𝑡 ) )
25 24 oveq1d ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑞 : ( 0 ..^ 𝑁 ) –1-1-onto→ 𝐷 ) ∧ ( ( ◡ 𝑞 ∘ 𝑄 ) ∘ 𝑞 ) = ( ( ( I ↾ ( 0 ..^ 𝑃 ) ) cyclShift 1 ) ∪ ( I ↾ ( 𝑃 ..^ 𝑁 ) ) ) ) ∧ 𝑡 : ( 0 ..^ 𝑁 ) –1-1-onto→ 𝐷 ) ∧ ( ( ◡ 𝑡 ∘ 𝑇 ) ∘ 𝑡 ) = ( ( ( I ↾ ( 0 ..^ 𝑃 ) ) cyclShift 1 ) ∪ ( I ↾ ( 𝑃 ..^ 𝑁 ) ) ) ) ∧ 𝑝 = ( 𝑞 ∘ ◡ 𝑡 ) ) → ( 𝑝 + 𝑇 ) = ( ( 𝑞 ∘ ◡ 𝑡 ) + 𝑇 ) )
26 25 24 oveq12d ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑞 : ( 0 ..^ 𝑁 ) –1-1-onto→ 𝐷 ) ∧ ( ( ◡ 𝑞 ∘ 𝑄 ) ∘ 𝑞 ) = ( ( ( I ↾ ( 0 ..^ 𝑃 ) ) cyclShift 1 ) ∪ ( I ↾ ( 𝑃 ..^ 𝑁 ) ) ) ) ∧ 𝑡 : ( 0 ..^ 𝑁 ) –1-1-onto→ 𝐷 ) ∧ ( ( ◡ 𝑡 ∘ 𝑇 ) ∘ 𝑡 ) = ( ( ( I ↾ ( 0 ..^ 𝑃 ) ) cyclShift 1 ) ∪ ( I ↾ ( 𝑃 ..^ 𝑁 ) ) ) ) ∧ 𝑝 = ( 𝑞 ∘ ◡ 𝑡 ) ) → ( ( 𝑝 + 𝑇 ) − 𝑝 ) = ( ( ( 𝑞 ∘ ◡ 𝑡 ) + 𝑇 ) − ( 𝑞 ∘ ◡ 𝑡 ) ) )
27 26 eqeq2d ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑞 : ( 0 ..^ 𝑁 ) –1-1-onto→ 𝐷 ) ∧ ( ( ◡ 𝑞 ∘ 𝑄 ) ∘ 𝑞 ) = ( ( ( I ↾ ( 0 ..^ 𝑃 ) ) cyclShift 1 ) ∪ ( I ↾ ( 𝑃 ..^ 𝑁 ) ) ) ) ∧ 𝑡 : ( 0 ..^ 𝑁 ) –1-1-onto→ 𝐷 ) ∧ ( ( ◡ 𝑡 ∘ 𝑇 ) ∘ 𝑡 ) = ( ( ( I ↾ ( 0 ..^ 𝑃 ) ) cyclShift 1 ) ∪ ( I ↾ ( 𝑃 ..^ 𝑁 ) ) ) ) ∧ 𝑝 = ( 𝑞 ∘ ◡ 𝑡 ) ) → ( 𝑄 = ( ( 𝑝 + 𝑇 ) − 𝑝 ) ↔ 𝑄 = ( ( ( 𝑞 ∘ ◡ 𝑡 ) + 𝑇 ) − ( 𝑞 ∘ ◡ 𝑡 ) ) ) )
28 simpllr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑞 : ( 0 ..^ 𝑁 ) –1-1-onto→ 𝐷 ) ∧ ( ( ◡ 𝑞 ∘ 𝑄 ) ∘ 𝑞 ) = ( ( ( I ↾ ( 0 ..^ 𝑃 ) ) cyclShift 1 ) ∪ ( I ↾ ( 𝑃 ..^ 𝑁 ) ) ) ) ∧ 𝑡 : ( 0 ..^ 𝑁 ) –1-1-onto→ 𝐷 ) ∧ ( ( ◡ 𝑡 ∘ 𝑇 ) ∘ 𝑡 ) = ( ( ( I ↾ ( 0 ..^ 𝑃 ) ) cyclShift 1 ) ∪ ( I ↾ ( 𝑃 ..^ 𝑁 ) ) ) ) → ( ( ◡ 𝑞 ∘ 𝑄 ) ∘ 𝑞 ) = ( ( ( I ↾ ( 0 ..^ 𝑃 ) ) cyclShift 1 ) ∪ ( I ↾ ( 𝑃 ..^ 𝑁 ) ) ) )
29 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑞 : ( 0 ..^ 𝑁 ) –1-1-onto→ 𝐷 ) ∧ ( ( ◡ 𝑞 ∘ 𝑄 ) ∘ 𝑞 ) = ( ( ( I ↾ ( 0 ..^ 𝑃 ) ) cyclShift 1 ) ∪ ( I ↾ ( 𝑃 ..^ 𝑁 ) ) ) ) ∧ 𝑡 : ( 0 ..^ 𝑁 ) –1-1-onto→ 𝐷 ) ∧ ( ( ◡ 𝑡 ∘ 𝑇 ) ∘ 𝑡 ) = ( ( ( I ↾ ( 0 ..^ 𝑃 ) ) cyclShift 1 ) ∪ ( I ↾ ( 𝑃 ..^ 𝑁 ) ) ) ) → ( ( ◡ 𝑡 ∘ 𝑇 ) ∘ 𝑡 ) = ( ( ( I ↾ ( 0 ..^ 𝑃 ) ) cyclShift 1 ) ∪ ( I ↾ ( 𝑃 ..^ 𝑁 ) ) ) )
30 28 29 eqtr4d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑞 : ( 0 ..^ 𝑁 ) –1-1-onto→ 𝐷 ) ∧ ( ( ◡ 𝑞 ∘ 𝑄 ) ∘ 𝑞 ) = ( ( ( I ↾ ( 0 ..^ 𝑃 ) ) cyclShift 1 ) ∪ ( I ↾ ( 𝑃 ..^ 𝑁 ) ) ) ) ∧ 𝑡 : ( 0 ..^ 𝑁 ) –1-1-onto→ 𝐷 ) ∧ ( ( ◡ 𝑡 ∘ 𝑇 ) ∘ 𝑡 ) = ( ( ( I ↾ ( 0 ..^ 𝑃 ) ) cyclShift 1 ) ∪ ( I ↾ ( 𝑃 ..^ 𝑁 ) ) ) ) → ( ( ◡ 𝑞 ∘ 𝑄 ) ∘ 𝑞 ) = ( ( ◡ 𝑡 ∘ 𝑇 ) ∘ 𝑡 ) )
31 30 coeq1d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑞 : ( 0 ..^ 𝑁 ) –1-1-onto→ 𝐷 ) ∧ ( ( ◡ 𝑞 ∘ 𝑄 ) ∘ 𝑞 ) = ( ( ( I ↾ ( 0 ..^ 𝑃 ) ) cyclShift 1 ) ∪ ( I ↾ ( 𝑃 ..^ 𝑁 ) ) ) ) ∧ 𝑡 : ( 0 ..^ 𝑁 ) –1-1-onto→ 𝐷 ) ∧ ( ( ◡ 𝑡 ∘ 𝑇 ) ∘ 𝑡 ) = ( ( ( I ↾ ( 0 ..^ 𝑃 ) ) cyclShift 1 ) ∪ ( I ↾ ( 𝑃 ..^ 𝑁 ) ) ) ) → ( ( ( ◡ 𝑞 ∘ 𝑄 ) ∘ 𝑞 ) ∘ ◡ 𝑞 ) = ( ( ( ◡ 𝑡 ∘ 𝑇 ) ∘ 𝑡 ) ∘ ◡ 𝑞 ) )
32 31 coeq2d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑞 : ( 0 ..^ 𝑁 ) –1-1-onto→ 𝐷 ) ∧ ( ( ◡ 𝑞 ∘ 𝑄 ) ∘ 𝑞 ) = ( ( ( I ↾ ( 0 ..^ 𝑃 ) ) cyclShift 1 ) ∪ ( I ↾ ( 𝑃 ..^ 𝑁 ) ) ) ) ∧ 𝑡 : ( 0 ..^ 𝑁 ) –1-1-onto→ 𝐷 ) ∧ ( ( ◡ 𝑡 ∘ 𝑇 ) ∘ 𝑡 ) = ( ( ( I ↾ ( 0 ..^ 𝑃 ) ) cyclShift 1 ) ∪ ( I ↾ ( 𝑃 ..^ 𝑁 ) ) ) ) → ( 𝑞 ∘ ( ( ( ◡ 𝑞 ∘ 𝑄 ) ∘ 𝑞 ) ∘ ◡ 𝑞 ) ) = ( 𝑞 ∘ ( ( ( ◡ 𝑡 ∘ 𝑇 ) ∘ 𝑡 ) ∘ ◡ 𝑞 ) ) )
33 coass ⊢ ( ( 𝑞 ∘ ( ◡ 𝑞 ∘ 𝑄 ) ) ∘ ( 𝑞 ∘ ◡ 𝑞 ) ) = ( 𝑞 ∘ ( ( ◡ 𝑞 ∘ 𝑄 ) ∘ ( 𝑞 ∘ ◡ 𝑞 ) ) )
34 coass ⊢ ( ( 𝑞 ∘ ◡ 𝑞 ) ∘ 𝑄 ) = ( 𝑞 ∘ ( ◡ 𝑞 ∘ 𝑄 ) )
35 34 coeq1i ⊢ ( ( ( 𝑞 ∘ ◡ 𝑞 ) ∘ 𝑄 ) ∘ ( 𝑞 ∘ ◡ 𝑞 ) ) = ( ( 𝑞 ∘ ( ◡ 𝑞 ∘ 𝑄 ) ) ∘ ( 𝑞 ∘ ◡ 𝑞 ) )
36 coass ⊢ ( ( ( ◡ 𝑞 ∘ 𝑄 ) ∘ 𝑞 ) ∘ ◡ 𝑞 ) = ( ( ◡ 𝑞 ∘ 𝑄 ) ∘ ( 𝑞 ∘ ◡ 𝑞 ) )
37 36 coeq2i ⊢ ( 𝑞 ∘ ( ( ( ◡ 𝑞 ∘ 𝑄 ) ∘ 𝑞 ) ∘ ◡ 𝑞 ) ) = ( 𝑞 ∘ ( ( ◡ 𝑞 ∘ 𝑄 ) ∘ ( 𝑞 ∘ ◡ 𝑞 ) ) )
38 33 35 37 3eqtr4ri ⊢ ( 𝑞 ∘ ( ( ( ◡ 𝑞 ∘ 𝑄 ) ∘ 𝑞 ) ∘ ◡ 𝑞 ) ) = ( ( ( 𝑞 ∘ ◡ 𝑞 ) ∘ 𝑄 ) ∘ ( 𝑞 ∘ ◡ 𝑞 ) )
39 f1ococnv2 ⊢ ( 𝑞 : ( 0 ..^ 𝑁 ) –1-1-onto→ 𝐷 → ( 𝑞 ∘ ◡ 𝑞 ) = ( I ↾ 𝐷 ) )
40 16 39 syl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑞 : ( 0 ..^ 𝑁 ) –1-1-onto→ 𝐷 ) ∧ ( ( ◡ 𝑞 ∘ 𝑄 ) ∘ 𝑞 ) = ( ( ( I ↾ ( 0 ..^ 𝑃 ) ) cyclShift 1 ) ∪ ( I ↾ ( 𝑃 ..^ 𝑁 ) ) ) ) ∧ 𝑡 : ( 0 ..^ 𝑁 ) –1-1-onto→ 𝐷 ) ∧ ( ( ◡ 𝑡 ∘ 𝑇 ) ∘ 𝑡 ) = ( ( ( I ↾ ( 0 ..^ 𝑃 ) ) cyclShift 1 ) ∪ ( I ↾ ( 𝑃 ..^ 𝑁 ) ) ) ) → ( 𝑞 ∘ ◡ 𝑞 ) = ( I ↾ 𝐷 ) )
41 40 coeq1d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑞 : ( 0 ..^ 𝑁 ) –1-1-onto→ 𝐷 ) ∧ ( ( ◡ 𝑞 ∘ 𝑄 ) ∘ 𝑞 ) = ( ( ( I ↾ ( 0 ..^ 𝑃 ) ) cyclShift 1 ) ∪ ( I ↾ ( 𝑃 ..^ 𝑁 ) ) ) ) ∧ 𝑡 : ( 0 ..^ 𝑁 ) –1-1-onto→ 𝐷 ) ∧ ( ( ◡ 𝑡 ∘ 𝑇 ) ∘ 𝑡 ) = ( ( ( I ↾ ( 0 ..^ 𝑃 ) ) cyclShift 1 ) ∪ ( I ↾ ( 𝑃 ..^ 𝑁 ) ) ) ) → ( ( 𝑞 ∘ ◡ 𝑞 ) ∘ 𝑄 ) = ( ( I ↾ 𝐷 ) ∘ 𝑄 ) )
42 1 2 3 4 5 cycpmgcl ⊢ ( ( 𝐷 ∈ Fin ∧ 𝑃 ∈ ( 0 ... 𝑁 ) ) → 𝐶 ⊆ 𝐵 )
43 9 8 42 syl2anc ⊢ ( 𝜑 → 𝐶 ⊆ 𝐵 )
44 43 10 sseldd ⊢ ( 𝜑 → 𝑄 ∈ 𝐵 )
45 2 5 elsymgbas ⊢ ( 𝐷 ∈ Fin → ( 𝑄 ∈ 𝐵 ↔ 𝑄 : 𝐷 –1-1-onto→ 𝐷 ) )
46 45 biimpa ⊢ ( ( 𝐷 ∈ Fin ∧ 𝑄 ∈ 𝐵 ) → 𝑄 : 𝐷 –1-1-onto→ 𝐷 )
47 9 44 46 syl2anc ⊢ ( 𝜑 → 𝑄 : 𝐷 –1-1-onto→ 𝐷 )
48 f1of ⊢ ( 𝑄 : 𝐷 –1-1-onto→ 𝐷 → 𝑄 : 𝐷 ⟶ 𝐷 )
49 fcoi2 ⊢ ( 𝑄 : 𝐷 ⟶ 𝐷 → ( ( I ↾ 𝐷 ) ∘ 𝑄 ) = 𝑄 )
50 47 48 49 3syl ⊢ ( 𝜑 → ( ( I ↾ 𝐷 ) ∘ 𝑄 ) = 𝑄 )
51 50 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑞 : ( 0 ..^ 𝑁 ) –1-1-onto→ 𝐷 ) ∧ ( ( ◡ 𝑞 ∘ 𝑄 ) ∘ 𝑞 ) = ( ( ( I ↾ ( 0 ..^ 𝑃 ) ) cyclShift 1 ) ∪ ( I ↾ ( 𝑃 ..^ 𝑁 ) ) ) ) ∧ 𝑡 : ( 0 ..^ 𝑁 ) –1-1-onto→ 𝐷 ) ∧ ( ( ◡ 𝑡 ∘ 𝑇 ) ∘ 𝑡 ) = ( ( ( I ↾ ( 0 ..^ 𝑃 ) ) cyclShift 1 ) ∪ ( I ↾ ( 𝑃 ..^ 𝑁 ) ) ) ) → ( ( I ↾ 𝐷 ) ∘ 𝑄 ) = 𝑄 )
52 41 51 eqtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑞 : ( 0 ..^ 𝑁 ) –1-1-onto→ 𝐷 ) ∧ ( ( ◡ 𝑞 ∘ 𝑄 ) ∘ 𝑞 ) = ( ( ( I ↾ ( 0 ..^ 𝑃 ) ) cyclShift 1 ) ∪ ( I ↾ ( 𝑃 ..^ 𝑁 ) ) ) ) ∧ 𝑡 : ( 0 ..^ 𝑁 ) –1-1-onto→ 𝐷 ) ∧ ( ( ◡ 𝑡 ∘ 𝑇 ) ∘ 𝑡 ) = ( ( ( I ↾ ( 0 ..^ 𝑃 ) ) cyclShift 1 ) ∪ ( I ↾ ( 𝑃 ..^ 𝑁 ) ) ) ) → ( ( 𝑞 ∘ ◡ 𝑞 ) ∘ 𝑄 ) = 𝑄 )
53 52 40 coeq12d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑞 : ( 0 ..^ 𝑁 ) –1-1-onto→ 𝐷 ) ∧ ( ( ◡ 𝑞 ∘ 𝑄 ) ∘ 𝑞 ) = ( ( ( I ↾ ( 0 ..^ 𝑃 ) ) cyclShift 1 ) ∪ ( I ↾ ( 𝑃 ..^ 𝑁 ) ) ) ) ∧ 𝑡 : ( 0 ..^ 𝑁 ) –1-1-onto→ 𝐷 ) ∧ ( ( ◡ 𝑡 ∘ 𝑇 ) ∘ 𝑡 ) = ( ( ( I ↾ ( 0 ..^ 𝑃 ) ) cyclShift 1 ) ∪ ( I ↾ ( 𝑃 ..^ 𝑁 ) ) ) ) → ( ( ( 𝑞 ∘ ◡ 𝑞 ) ∘ 𝑄 ) ∘ ( 𝑞 ∘ ◡ 𝑞 ) ) = ( 𝑄 ∘ ( I ↾ 𝐷 ) ) )
54 fcoi1 ⊢ ( 𝑄 : 𝐷 ⟶ 𝐷 → ( 𝑄 ∘ ( I ↾ 𝐷 ) ) = 𝑄 )
55 47 48 54 3syl ⊢ ( 𝜑 → ( 𝑄 ∘ ( I ↾ 𝐷 ) ) = 𝑄 )
56 55 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑞 : ( 0 ..^ 𝑁 ) –1-1-onto→ 𝐷 ) ∧ ( ( ◡ 𝑞 ∘ 𝑄 ) ∘ 𝑞 ) = ( ( ( I ↾ ( 0 ..^ 𝑃 ) ) cyclShift 1 ) ∪ ( I ↾ ( 𝑃 ..^ 𝑁 ) ) ) ) ∧ 𝑡 : ( 0 ..^ 𝑁 ) –1-1-onto→ 𝐷 ) ∧ ( ( ◡ 𝑡 ∘ 𝑇 ) ∘ 𝑡 ) = ( ( ( I ↾ ( 0 ..^ 𝑃 ) ) cyclShift 1 ) ∪ ( I ↾ ( 𝑃 ..^ 𝑁 ) ) ) ) → ( 𝑄 ∘ ( I ↾ 𝐷 ) ) = 𝑄 )
57 53 56 eqtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑞 : ( 0 ..^ 𝑁 ) –1-1-onto→ 𝐷 ) ∧ ( ( ◡ 𝑞 ∘ 𝑄 ) ∘ 𝑞 ) = ( ( ( I ↾ ( 0 ..^ 𝑃 ) ) cyclShift 1 ) ∪ ( I ↾ ( 𝑃 ..^ 𝑁 ) ) ) ) ∧ 𝑡 : ( 0 ..^ 𝑁 ) –1-1-onto→ 𝐷 ) ∧ ( ( ◡ 𝑡 ∘ 𝑇 ) ∘ 𝑡 ) = ( ( ( I ↾ ( 0 ..^ 𝑃 ) ) cyclShift 1 ) ∪ ( I ↾ ( 𝑃 ..^ 𝑁 ) ) ) ) → ( ( ( 𝑞 ∘ ◡ 𝑞 ) ∘ 𝑄 ) ∘ ( 𝑞 ∘ ◡ 𝑞 ) ) = 𝑄 )
58 38 57 syl5eq ⊢ ( ( ( ( ( 𝜑 ∧ 𝑞 : ( 0 ..^ 𝑁 ) –1-1-onto→ 𝐷 ) ∧ ( ( ◡ 𝑞 ∘ 𝑄 ) ∘ 𝑞 ) = ( ( ( I ↾ ( 0 ..^ 𝑃 ) ) cyclShift 1 ) ∪ ( I ↾ ( 𝑃 ..^ 𝑁 ) ) ) ) ∧ 𝑡 : ( 0 ..^ 𝑁 ) –1-1-onto→ 𝐷 ) ∧ ( ( ◡ 𝑡 ∘ 𝑇 ) ∘ 𝑡 ) = ( ( ( I ↾ ( 0 ..^ 𝑃 ) ) cyclShift 1 ) ∪ ( I ↾ ( 𝑃 ..^ 𝑁 ) ) ) ) → ( 𝑞 ∘ ( ( ( ◡ 𝑞 ∘ 𝑄 ) ∘ 𝑞 ) ∘ ◡ 𝑞 ) ) = 𝑄 )
59 coass ⊢ ( ( 𝑞 ∘ ( ◡ 𝑡 ∘ 𝑇 ) ) ∘ ( 𝑡 ∘ ◡ 𝑞 ) ) = ( 𝑞 ∘ ( ( ◡ 𝑡 ∘ 𝑇 ) ∘ ( 𝑡 ∘ ◡ 𝑞 ) ) )
60 coass ⊢ ( ( 𝑞 ∘ ◡ 𝑡 ) ∘ 𝑇 ) = ( 𝑞 ∘ ( ◡ 𝑡 ∘ 𝑇 ) )
61 60 coeq1i ⊢ ( ( ( 𝑞 ∘ ◡ 𝑡 ) ∘ 𝑇 ) ∘ ( 𝑡 ∘ ◡ 𝑞 ) ) = ( ( 𝑞 ∘ ( ◡ 𝑡 ∘ 𝑇 ) ) ∘ ( 𝑡 ∘ ◡ 𝑞 ) )
62 coass ⊢ ( ( ( ◡ 𝑡 ∘ 𝑇 ) ∘ 𝑡 ) ∘ ◡ 𝑞 ) = ( ( ◡ 𝑡 ∘ 𝑇 ) ∘ ( 𝑡 ∘ ◡ 𝑞 ) )
63 62 coeq2i ⊢ ( 𝑞 ∘ ( ( ( ◡ 𝑡 ∘ 𝑇 ) ∘ 𝑡 ) ∘ ◡ 𝑞 ) ) = ( 𝑞 ∘ ( ( ◡ 𝑡 ∘ 𝑇 ) ∘ ( 𝑡 ∘ ◡ 𝑞 ) ) )
64 59 61 63 3eqtr4i ⊢ ( ( ( 𝑞 ∘ ◡ 𝑡 ) ∘ 𝑇 ) ∘ ( 𝑡 ∘ ◡ 𝑞 ) ) = ( 𝑞 ∘ ( ( ( ◡ 𝑡 ∘ 𝑇 ) ∘ 𝑡 ) ∘ ◡ 𝑞 ) )
65 43 11 sseldd ⊢ ( 𝜑 → 𝑇 ∈ 𝐵 )
66 65 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑞 : ( 0 ..^ 𝑁 ) –1-1-onto→ 𝐷 ) ∧ ( ( ◡ 𝑞 ∘ 𝑄 ) ∘ 𝑞 ) = ( ( ( I ↾ ( 0 ..^ 𝑃 ) ) cyclShift 1 ) ∪ ( I ↾ ( 𝑃 ..^ 𝑁 ) ) ) ) ∧ 𝑡 : ( 0 ..^ 𝑁 ) –1-1-onto→ 𝐷 ) ∧ ( ( ◡ 𝑡 ∘ 𝑇 ) ∘ 𝑡 ) = ( ( ( I ↾ ( 0 ..^ 𝑃 ) ) cyclShift 1 ) ∪ ( I ↾ ( 𝑃 ..^ 𝑁 ) ) ) ) → 𝑇 ∈ 𝐵 )
67 2 5 6 symgov ⊢ ( ( ( 𝑞 ∘ ◡ 𝑡 ) ∈ 𝐵 ∧ 𝑇 ∈ 𝐵 ) → ( ( 𝑞 ∘ ◡ 𝑡 ) + 𝑇 ) = ( ( 𝑞 ∘ ◡ 𝑡 ) ∘ 𝑇 ) )
68 23 66 67 syl2anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑞 : ( 0 ..^ 𝑁 ) –1-1-onto→ 𝐷 ) ∧ ( ( ◡ 𝑞 ∘ 𝑄 ) ∘ 𝑞 ) = ( ( ( I ↾ ( 0 ..^ 𝑃 ) ) cyclShift 1 ) ∪ ( I ↾ ( 𝑃 ..^ 𝑁 ) ) ) ) ∧ 𝑡 : ( 0 ..^ 𝑁 ) –1-1-onto→ 𝐷 ) ∧ ( ( ◡ 𝑡 ∘ 𝑇 ) ∘ 𝑡 ) = ( ( ( I ↾ ( 0 ..^ 𝑃 ) ) cyclShift 1 ) ∪ ( I ↾ ( 𝑃 ..^ 𝑁 ) ) ) ) → ( ( 𝑞 ∘ ◡ 𝑡 ) + 𝑇 ) = ( ( 𝑞 ∘ ◡ 𝑡 ) ∘ 𝑇 ) )
69 68 oveq1d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑞 : ( 0 ..^ 𝑁 ) –1-1-onto→ 𝐷 ) ∧ ( ( ◡ 𝑞 ∘ 𝑄 ) ∘ 𝑞 ) = ( ( ( I ↾ ( 0 ..^ 𝑃 ) ) cyclShift 1 ) ∪ ( I ↾ ( 𝑃 ..^ 𝑁 ) ) ) ) ∧ 𝑡 : ( 0 ..^ 𝑁 ) –1-1-onto→ 𝐷 ) ∧ ( ( ◡ 𝑡 ∘ 𝑇 ) ∘ 𝑡 ) = ( ( ( I ↾ ( 0 ..^ 𝑃 ) ) cyclShift 1 ) ∪ ( I ↾ ( 𝑃 ..^ 𝑁 ) ) ) ) → ( ( ( 𝑞 ∘ ◡ 𝑡 ) + 𝑇 ) − ( 𝑞 ∘ ◡ 𝑡 ) ) = ( ( ( 𝑞 ∘ ◡ 𝑡 ) ∘ 𝑇 ) − ( 𝑞 ∘ ◡ 𝑡 ) ) )
70 2 symggrp ⊢ ( 𝐷 ∈ Fin → 𝑆 ∈ Grp )
71 9 70 syl ⊢ ( 𝜑 → 𝑆 ∈ Grp )
72 71 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑞 : ( 0 ..^ 𝑁 ) –1-1-onto→ 𝐷 ) ∧ ( ( ◡ 𝑞 ∘ 𝑄 ) ∘ 𝑞 ) = ( ( ( I ↾ ( 0 ..^ 𝑃 ) ) cyclShift 1 ) ∪ ( I ↾ ( 𝑃 ..^ 𝑁 ) ) ) ) ∧ 𝑡 : ( 0 ..^ 𝑁 ) –1-1-onto→ 𝐷 ) ∧ ( ( ◡ 𝑡 ∘ 𝑇 ) ∘ 𝑡 ) = ( ( ( I ↾ ( 0 ..^ 𝑃 ) ) cyclShift 1 ) ∪ ( I ↾ ( 𝑃 ..^ 𝑁 ) ) ) ) → 𝑆 ∈ Grp )
73 5 6 grpcl ⊢ ( ( 𝑆 ∈ Grp ∧ ( 𝑞 ∘ ◡ 𝑡 ) ∈ 𝐵 ∧ 𝑇 ∈ 𝐵 ) → ( ( 𝑞 ∘ ◡ 𝑡 ) + 𝑇 ) ∈ 𝐵 )
74 72 23 66 73 syl3anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑞 : ( 0 ..^ 𝑁 ) –1-1-onto→ 𝐷 ) ∧ ( ( ◡ 𝑞 ∘ 𝑄 ) ∘ 𝑞 ) = ( ( ( I ↾ ( 0 ..^ 𝑃 ) ) cyclShift 1 ) ∪ ( I ↾ ( 𝑃 ..^ 𝑁 ) ) ) ) ∧ 𝑡 : ( 0 ..^ 𝑁 ) –1-1-onto→ 𝐷 ) ∧ ( ( ◡ 𝑡 ∘ 𝑇 ) ∘ 𝑡 ) = ( ( ( I ↾ ( 0 ..^ 𝑃 ) ) cyclShift 1 ) ∪ ( I ↾ ( 𝑃 ..^ 𝑁 ) ) ) ) → ( ( 𝑞 ∘ ◡ 𝑡 ) + 𝑇 ) ∈ 𝐵 )
75 68 74 eqeltrrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑞 : ( 0 ..^ 𝑁 ) –1-1-onto→ 𝐷 ) ∧ ( ( ◡ 𝑞 ∘ 𝑄 ) ∘ 𝑞 ) = ( ( ( I ↾ ( 0 ..^ 𝑃 ) ) cyclShift 1 ) ∪ ( I ↾ ( 𝑃 ..^ 𝑁 ) ) ) ) ∧ 𝑡 : ( 0 ..^ 𝑁 ) –1-1-onto→ 𝐷 ) ∧ ( ( ◡ 𝑡 ∘ 𝑇 ) ∘ 𝑡 ) = ( ( ( I ↾ ( 0 ..^ 𝑃 ) ) cyclShift 1 ) ∪ ( I ↾ ( 𝑃 ..^ 𝑁 ) ) ) ) → ( ( 𝑞 ∘ ◡ 𝑡 ) ∘ 𝑇 ) ∈ 𝐵 )
76 2 5 7 symgsubg ⊢ ( ( ( ( 𝑞 ∘ ◡ 𝑡 ) ∘ 𝑇 ) ∈ 𝐵 ∧ ( 𝑞 ∘ ◡ 𝑡 ) ∈ 𝐵 ) → ( ( ( 𝑞 ∘ ◡ 𝑡 ) ∘ 𝑇 ) − ( 𝑞 ∘ ◡ 𝑡 ) ) = ( ( ( 𝑞 ∘ ◡ 𝑡 ) ∘ 𝑇 ) ∘ ◡ ( 𝑞 ∘ ◡ 𝑡 ) ) )
77 75 23 76 syl2anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑞 : ( 0 ..^ 𝑁 ) –1-1-onto→ 𝐷 ) ∧ ( ( ◡ 𝑞 ∘ 𝑄 ) ∘ 𝑞 ) = ( ( ( I ↾ ( 0 ..^ 𝑃 ) ) cyclShift 1 ) ∪ ( I ↾ ( 𝑃 ..^ 𝑁 ) ) ) ) ∧ 𝑡 : ( 0 ..^ 𝑁 ) –1-1-onto→ 𝐷 ) ∧ ( ( ◡ 𝑡 ∘ 𝑇 ) ∘ 𝑡 ) = ( ( ( I ↾ ( 0 ..^ 𝑃 ) ) cyclShift 1 ) ∪ ( I ↾ ( 𝑃 ..^ 𝑁 ) ) ) ) → ( ( ( 𝑞 ∘ ◡ 𝑡 ) ∘ 𝑇 ) − ( 𝑞 ∘ ◡ 𝑡 ) ) = ( ( ( 𝑞 ∘ ◡ 𝑡 ) ∘ 𝑇 ) ∘ ◡ ( 𝑞 ∘ ◡ 𝑡 ) ) )
78 cnvco ⊢ ◡ ( 𝑞 ∘ ◡ 𝑡 ) = ( ◡ ◡ 𝑡 ∘ ◡ 𝑞 )
79 f1orel ⊢ ( 𝑡 : ( 0 ..^ 𝑁 ) –1-1-onto→ 𝐷 → Rel 𝑡 )
80 dfrel2 ⊢ ( Rel 𝑡 ↔ ◡ ◡ 𝑡 = 𝑡 )
81 79 80 sylib ⊢ ( 𝑡 : ( 0 ..^ 𝑁 ) –1-1-onto→ 𝐷 → ◡ ◡ 𝑡 = 𝑡 )
82 81 coeq1d ⊢ ( 𝑡 : ( 0 ..^ 𝑁 ) –1-1-onto→ 𝐷 → ( ◡ ◡ 𝑡 ∘ ◡ 𝑞 ) = ( 𝑡 ∘ ◡ 𝑞 ) )
83 78 82 syl5eq ⊢ ( 𝑡 : ( 0 ..^ 𝑁 ) –1-1-onto→ 𝐷 → ◡ ( 𝑞 ∘ ◡ 𝑡 ) = ( 𝑡 ∘ ◡ 𝑞 ) )
84 83 coeq2d ⊢ ( 𝑡 : ( 0 ..^ 𝑁 ) –1-1-onto→ 𝐷 → ( ( ( 𝑞 ∘ ◡ 𝑡 ) ∘ 𝑇 ) ∘ ◡ ( 𝑞 ∘ ◡ 𝑡 ) ) = ( ( ( 𝑞 ∘ ◡ 𝑡 ) ∘ 𝑇 ) ∘ ( 𝑡 ∘ ◡ 𝑞 ) ) )
85 84 ad2antlr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑞 : ( 0 ..^ 𝑁 ) –1-1-onto→ 𝐷 ) ∧ ( ( ◡ 𝑞 ∘ 𝑄 ) ∘ 𝑞 ) = ( ( ( I ↾ ( 0 ..^ 𝑃 ) ) cyclShift 1 ) ∪ ( I ↾ ( 𝑃 ..^ 𝑁 ) ) ) ) ∧ 𝑡 : ( 0 ..^ 𝑁 ) –1-1-onto→ 𝐷 ) ∧ ( ( ◡ 𝑡 ∘ 𝑇 ) ∘ 𝑡 ) = ( ( ( I ↾ ( 0 ..^ 𝑃 ) ) cyclShift 1 ) ∪ ( I ↾ ( 𝑃 ..^ 𝑁 ) ) ) ) → ( ( ( 𝑞 ∘ ◡ 𝑡 ) ∘ 𝑇 ) ∘ ◡ ( 𝑞 ∘ ◡ 𝑡 ) ) = ( ( ( 𝑞 ∘ ◡ 𝑡 ) ∘ 𝑇 ) ∘ ( 𝑡 ∘ ◡ 𝑞 ) ) )
86 69 77 85 3eqtrrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑞 : ( 0 ..^ 𝑁 ) –1-1-onto→ 𝐷 ) ∧ ( ( ◡ 𝑞 ∘ 𝑄 ) ∘ 𝑞 ) = ( ( ( I ↾ ( 0 ..^ 𝑃 ) ) cyclShift 1 ) ∪ ( I ↾ ( 𝑃 ..^ 𝑁 ) ) ) ) ∧ 𝑡 : ( 0 ..^ 𝑁 ) –1-1-onto→ 𝐷 ) ∧ ( ( ◡ 𝑡 ∘ 𝑇 ) ∘ 𝑡 ) = ( ( ( I ↾ ( 0 ..^ 𝑃 ) ) cyclShift 1 ) ∪ ( I ↾ ( 𝑃 ..^ 𝑁 ) ) ) ) → ( ( ( 𝑞 ∘ ◡ 𝑡 ) ∘ 𝑇 ) ∘ ( 𝑡 ∘ ◡ 𝑞 ) ) = ( ( ( 𝑞 ∘ ◡ 𝑡 ) + 𝑇 ) − ( 𝑞 ∘ ◡ 𝑡 ) ) )
87 64 86 eqtr3id ⊢ ( ( ( ( ( 𝜑 ∧ 𝑞 : ( 0 ..^ 𝑁 ) –1-1-onto→ 𝐷 ) ∧ ( ( ◡ 𝑞 ∘ 𝑄 ) ∘ 𝑞 ) = ( ( ( I ↾ ( 0 ..^ 𝑃 ) ) cyclShift 1 ) ∪ ( I ↾ ( 𝑃 ..^ 𝑁 ) ) ) ) ∧ 𝑡 : ( 0 ..^ 𝑁 ) –1-1-onto→ 𝐷 ) ∧ ( ( ◡ 𝑡 ∘ 𝑇 ) ∘ 𝑡 ) = ( ( ( I ↾ ( 0 ..^ 𝑃 ) ) cyclShift 1 ) ∪ ( I ↾ ( 𝑃 ..^ 𝑁 ) ) ) ) → ( 𝑞 ∘ ( ( ( ◡ 𝑡 ∘ 𝑇 ) ∘ 𝑡 ) ∘ ◡ 𝑞 ) ) = ( ( ( 𝑞 ∘ ◡ 𝑡 ) + 𝑇 ) − ( 𝑞 ∘ ◡ 𝑡 ) ) )
88 32 58 87 3eqtr3d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑞 : ( 0 ..^ 𝑁 ) –1-1-onto→ 𝐷 ) ∧ ( ( ◡ 𝑞 ∘ 𝑄 ) ∘ 𝑞 ) = ( ( ( I ↾ ( 0 ..^ 𝑃 ) ) cyclShift 1 ) ∪ ( I ↾ ( 𝑃 ..^ 𝑁 ) ) ) ) ∧ 𝑡 : ( 0 ..^ 𝑁 ) –1-1-onto→ 𝐷 ) ∧ ( ( ◡ 𝑡 ∘ 𝑇 ) ∘ 𝑡 ) = ( ( ( I ↾ ( 0 ..^ 𝑃 ) ) cyclShift 1 ) ∪ ( I ↾ ( 𝑃 ..^ 𝑁 ) ) ) ) → 𝑄 = ( ( ( 𝑞 ∘ ◡ 𝑡 ) + 𝑇 ) − ( 𝑞 ∘ ◡ 𝑡 ) ) )
89 23 27 88 rspcedvd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑞 : ( 0 ..^ 𝑁 ) –1-1-onto→ 𝐷 ) ∧ ( ( ◡ 𝑞 ∘ 𝑄 ) ∘ 𝑞 ) = ( ( ( I ↾ ( 0 ..^ 𝑃 ) ) cyclShift 1 ) ∪ ( I ↾ ( 𝑃 ..^ 𝑁 ) ) ) ) ∧ 𝑡 : ( 0 ..^ 𝑁 ) –1-1-onto→ 𝐷 ) ∧ ( ( ◡ 𝑡 ∘ 𝑇 ) ∘ 𝑡 ) = ( ( ( I ↾ ( 0 ..^ 𝑃 ) ) cyclShift 1 ) ∪ ( I ↾ ( 𝑃 ..^ 𝑁 ) ) ) ) → ∃ 𝑝 ∈ 𝐵 𝑄 = ( ( 𝑝 + 𝑇 ) − 𝑝 ) )
90 89 anasss ⊢ ( ( ( ( 𝜑 ∧ 𝑞 : ( 0 ..^ 𝑁 ) –1-1-onto→ 𝐷 ) ∧ ( ( ◡ 𝑞 ∘ 𝑄 ) ∘ 𝑞 ) = ( ( ( I ↾ ( 0 ..^ 𝑃 ) ) cyclShift 1 ) ∪ ( I ↾ ( 𝑃 ..^ 𝑁 ) ) ) ) ∧ ( 𝑡 : ( 0 ..^ 𝑁 ) –1-1-onto→ 𝐷 ∧ ( ( ◡ 𝑡 ∘ 𝑇 ) ∘ 𝑡 ) = ( ( ( I ↾ ( 0 ..^ 𝑃 ) ) cyclShift 1 ) ∪ ( I ↾ ( 𝑃 ..^ 𝑁 ) ) ) ) ) → ∃ 𝑝 ∈ 𝐵 𝑄 = ( ( 𝑝 + 𝑇 ) − 𝑝 ) )
91 14 90 exlimddv ⊢ ( ( ( 𝜑 ∧ 𝑞 : ( 0 ..^ 𝑁 ) –1-1-onto→ 𝐷 ) ∧ ( ( ◡ 𝑞 ∘ 𝑄 ) ∘ 𝑞 ) = ( ( ( I ↾ ( 0 ..^ 𝑃 ) ) cyclShift 1 ) ∪ ( I ↾ ( 𝑃 ..^ 𝑁 ) ) ) ) → ∃ 𝑝 ∈ 𝐵 𝑄 = ( ( 𝑝 + 𝑇 ) − 𝑝 ) )
92 91 anasss ⊢ ( ( 𝜑 ∧ ( 𝑞 : ( 0 ..^ 𝑁 ) –1-1-onto→ 𝐷 ∧ ( ( ◡ 𝑞 ∘ 𝑄 ) ∘ 𝑞 ) = ( ( ( I ↾ ( 0 ..^ 𝑃 ) ) cyclShift 1 ) ∪ ( I ↾ ( 𝑃 ..^ 𝑁 ) ) ) ) ) → ∃ 𝑝 ∈ 𝐵 𝑄 = ( ( 𝑝 + 𝑇 ) − 𝑝 ) )
93 12 92 exlimddv ⊢ ( 𝜑 → ∃ 𝑝 ∈ 𝐵 𝑄 = ( ( 𝑝 + 𝑇 ) − 𝑝 ) )