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

Metamath Proof Explorer

Theorem cshfn

Description: Perform a cyclical shift for a function over a half-open range of nonnegative integers. (Contributed by AV, 20-May-2018) (Revised by AV, 17-Nov-2018) (Revised by AV, 4-Nov-2022)

Ref Expression
Assertion cshfn ( ( 𝑊 ∈ { 𝑓 ∣ ∃ 𝑙 ∈ ℕ0 𝑓 Fn ( 0 ..^ 𝑙 ) } ∧ 𝑁 ∈ ℤ ) → ( 𝑊 cyclShift 𝑁 ) = if ( 𝑊 = ∅ , ∅ , ( ( 𝑊 substr ⟨ ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) , ( ♯ ‘ 𝑊 ) ⟩ ) ++ ( 𝑊 prefix ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 eqeq1 ⊢ ( 𝑤 = 𝑊 → ( 𝑤 = ∅ ↔ 𝑊 = ∅ ) )
2 1 adantr ⊢ ( ( 𝑤 = 𝑊 ∧ 𝑛 = 𝑁 ) → ( 𝑤 = ∅ ↔ 𝑊 = ∅ ) )
3 simpl ⊢ ( ( 𝑤 = 𝑊 ∧ 𝑛 = 𝑁 ) → 𝑤 = 𝑊 )
4 simpr ⊢ ( ( 𝑤 = 𝑊 ∧ 𝑛 = 𝑁 ) → 𝑛 = 𝑁 )
5 fveq2 ⊢ ( 𝑤 = 𝑊 → ( ♯ ‘ 𝑤 ) = ( ♯ ‘ 𝑊 ) )
6 5 adantr ⊢ ( ( 𝑤 = 𝑊 ∧ 𝑛 = 𝑁 ) → ( ♯ ‘ 𝑤 ) = ( ♯ ‘ 𝑊 ) )
7 4 6 oveq12d ⊢ ( ( 𝑤 = 𝑊 ∧ 𝑛 = 𝑁 ) → ( 𝑛 mod ( ♯ ‘ 𝑤 ) ) = ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) )
8 7 6 opeq12d ⊢ ( ( 𝑤 = 𝑊 ∧ 𝑛 = 𝑁 ) → ⟨ ( 𝑛 mod ( ♯ ‘ 𝑤 ) ) , ( ♯ ‘ 𝑤 ) ⟩ = ⟨ ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) , ( ♯ ‘ 𝑊 ) ⟩ )
9 3 8 oveq12d ⊢ ( ( 𝑤 = 𝑊 ∧ 𝑛 = 𝑁 ) → ( 𝑤 substr ⟨ ( 𝑛 mod ( ♯ ‘ 𝑤 ) ) , ( ♯ ‘ 𝑤 ) ⟩ ) = ( 𝑊 substr ⟨ ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) , ( ♯ ‘ 𝑊 ) ⟩ ) )
10 3 7 oveq12d ⊢ ( ( 𝑤 = 𝑊 ∧ 𝑛 = 𝑁 ) → ( 𝑤 prefix ( 𝑛 mod ( ♯ ‘ 𝑤 ) ) ) = ( 𝑊 prefix ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) )
11 9 10 oveq12d ⊢ ( ( 𝑤 = 𝑊 ∧ 𝑛 = 𝑁 ) → ( ( 𝑤 substr ⟨ ( 𝑛 mod ( ♯ ‘ 𝑤 ) ) , ( ♯ ‘ 𝑤 ) ⟩ ) ++ ( 𝑤 prefix ( 𝑛 mod ( ♯ ‘ 𝑤 ) ) ) ) = ( ( 𝑊 substr ⟨ ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) , ( ♯ ‘ 𝑊 ) ⟩ ) ++ ( 𝑊 prefix ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) )
12 2 11 ifbieq2d ⊢ ( ( 𝑤 = 𝑊 ∧ 𝑛 = 𝑁 ) → if ( 𝑤 = ∅ , ∅ , ( ( 𝑤 substr ⟨ ( 𝑛 mod ( ♯ ‘ 𝑤 ) ) , ( ♯ ‘ 𝑤 ) ⟩ ) ++ ( 𝑤 prefix ( 𝑛 mod ( ♯ ‘ 𝑤 ) ) ) ) ) = if ( 𝑊 = ∅ , ∅ , ( ( 𝑊 substr ⟨ ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) , ( ♯ ‘ 𝑊 ) ⟩ ) ++ ( 𝑊 prefix ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) ) )
13 df-csh ⊢ cyclShift = ( 𝑤 ∈ { 𝑓 ∣ ∃ 𝑙 ∈ ℕ0 𝑓 Fn ( 0 ..^ 𝑙 ) } , 𝑛 ∈ ℤ ↦ if ( 𝑤 = ∅ , ∅ , ( ( 𝑤 substr ⟨ ( 𝑛 mod ( ♯ ‘ 𝑤 ) ) , ( ♯ ‘ 𝑤 ) ⟩ ) ++ ( 𝑤 prefix ( 𝑛 mod ( ♯ ‘ 𝑤 ) ) ) ) ) )
14 0ex ⊢ ∅ ∈ V
15 ovex ⊢ ( ( 𝑊 substr ⟨ ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) , ( ♯ ‘ 𝑊 ) ⟩ ) ++ ( 𝑊 prefix ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) ∈ V
16 14 15 ifex ⊢ if ( 𝑊 = ∅ , ∅ , ( ( 𝑊 substr ⟨ ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) , ( ♯ ‘ 𝑊 ) ⟩ ) ++ ( 𝑊 prefix ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) ) ∈ V
17 12 13 16 ovmpoa ⊢ ( ( 𝑊 ∈ { 𝑓 ∣ ∃ 𝑙 ∈ ℕ0 𝑓 Fn ( 0 ..^ 𝑙 ) } ∧ 𝑁 ∈ ℤ ) → ( 𝑊 cyclShift 𝑁 ) = if ( 𝑊 = ∅ , ∅ , ( ( 𝑊 substr ⟨ ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) , ( ♯ ‘ 𝑊 ) ⟩ ) ++ ( 𝑊 prefix ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) ) )