Metamath Proof Explorer


Theorem cshwsdisj

Description: The singletons resulting by cyclically shifting a given word of length being a prime number and not consisting of identical symbols is a disjoint collection. (Contributed by Alexander van der Vekens, 19-May-2018) (Revised by Alexander van der Vekens, 8-Jun-2018)

Ref Expression
Hypothesis cshwshash.0 φWWordVW
Assertion cshwsdisj φi0..^WWiW0Disjn0..^WWcyclShiftn

Proof

Step Hyp Ref Expression
1 cshwshash.0 φWWordVW
2 orc n=jn=jWcyclShiftnWcyclShiftj=
3 2 a1d n=jφi0..^WWiW0n0..^Wj0..^Wn=jWcyclShiftnWcyclShiftj=
4 simprl njφi0..^WWiW0n0..^Wj0..^Wφi0..^WWiW0
5 simprrl njφi0..^WWiW0n0..^Wj0..^Wn0..^W
6 simprrr njφi0..^WWiW0n0..^Wj0..^Wj0..^W
7 necom njjn
8 7 biimpi njjn
9 8 adantr njφi0..^WWiW0n0..^Wj0..^Wjn
10 1 cshwshashlem3 φi0..^WWiW0n0..^Wj0..^WjnWcyclShiftnWcyclShiftj
11 10 imp φi0..^WWiW0n0..^Wj0..^WjnWcyclShiftnWcyclShiftj
12 4 5 6 9 11 syl13anc njφi0..^WWiW0n0..^Wj0..^WWcyclShiftnWcyclShiftj
13 disjsn2 WcyclShiftnWcyclShiftjWcyclShiftnWcyclShiftj=
14 12 13 syl njφi0..^WWiW0n0..^Wj0..^WWcyclShiftnWcyclShiftj=
15 14 olcd njφi0..^WWiW0n0..^Wj0..^Wn=jWcyclShiftnWcyclShiftj=
16 15 ex njφi0..^WWiW0n0..^Wj0..^Wn=jWcyclShiftnWcyclShiftj=
17 3 16 pm2.61ine φi0..^WWiW0n0..^Wj0..^Wn=jWcyclShiftnWcyclShiftj=
18 17 ralrimivva φi0..^WWiW0n0..^Wj0..^Wn=jWcyclShiftnWcyclShiftj=
19 oveq2 n=jWcyclShiftn=WcyclShiftj
20 19 sneqd n=jWcyclShiftn=WcyclShiftj
21 20 disjor Disjn0..^WWcyclShiftnn0..^Wj0..^Wn=jWcyclShiftnWcyclShiftj=
22 18 21 sylibr φi0..^WWiW0Disjn0..^WWcyclShiftn