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 ( ♯ ‘ 𝑊 ) ) ) ) ) )