This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cshnz

Description: A cyclical shift is the empty set if the number of shifts is not an integer. (Contributed by Alexander van der Vekens, 21-May-2018) (Revised by AV, 17-Nov-2018)

Ref Expression
Assertion cshnz ( ¬ 𝑁 ∈ ℤ → ( 𝑊 cyclShift 𝑁 ) = ∅ )

Proof

Step Hyp Ref Expression
1 df-csh ⊢ cyclShift = ( 𝑤 ∈ { 𝑓 ∣ ∃ 𝑙 ∈ ℕ0 𝑓 Fn ( 0 ..^ 𝑙 ) } , 𝑛 ∈ ℤ ↦ if ( 𝑤 = ∅ , ∅ , ( ( 𝑤 substr ⟨ ( 𝑛 mod ( ♯ ‘ 𝑤 ) ) , ( ♯ ‘ 𝑤 ) ⟩ ) ++ ( 𝑤 prefix ( 𝑛 mod ( ♯ ‘ 𝑤 ) ) ) ) ) )
2 0ex ⊢ ∅ ∈ V
3 ovex ⊢ ( ( 𝑤 substr ⟨ ( 𝑛 mod ( ♯ ‘ 𝑤 ) ) , ( ♯ ‘ 𝑤 ) ⟩ ) ++ ( 𝑤 prefix ( 𝑛 mod ( ♯ ‘ 𝑤 ) ) ) ) ∈ V
4 2 3 ifex ⊢ if ( 𝑤 = ∅ , ∅ , ( ( 𝑤 substr ⟨ ( 𝑛 mod ( ♯ ‘ 𝑤 ) ) , ( ♯ ‘ 𝑤 ) ⟩ ) ++ ( 𝑤 prefix ( 𝑛 mod ( ♯ ‘ 𝑤 ) ) ) ) ) ∈ V
5 1 4 dmmpo ⊢ dom cyclShift = ( { 𝑓 ∣ ∃ 𝑙 ∈ ℕ0 𝑓 Fn ( 0 ..^ 𝑙 ) } × ℤ )
6 id ⊢ ( ¬ 𝑁 ∈ ℤ → ¬ 𝑁 ∈ ℤ )
7 6 intnand ⊢ ( ¬ 𝑁 ∈ ℤ → ¬ ( 𝑊 ∈ { 𝑓 ∣ ∃ 𝑙 ∈ ℕ0 𝑓 Fn ( 0 ..^ 𝑙 ) } ∧ 𝑁 ∈ ℤ ) )
8 ndmovg ⊢ ( ( dom cyclShift = ( { 𝑓 ∣ ∃ 𝑙 ∈ ℕ0 𝑓 Fn ( 0 ..^ 𝑙 ) } × ℤ ) ∧ ¬ ( 𝑊 ∈ { 𝑓 ∣ ∃ 𝑙 ∈ ℕ0 𝑓 Fn ( 0 ..^ 𝑙 ) } ∧ 𝑁 ∈ ℤ ) ) → ( 𝑊 cyclShift 𝑁 ) = ∅ )
9 5 7 8 sylancr ⊢ ( ¬ 𝑁 ∈ ℤ → ( 𝑊 cyclShift 𝑁 ) = ∅ )