Metamath Proof Explorer

Theorem 0csh0

Description: Cyclically shifting an empty set/word always results in the empty word/set. (Contributed by AV, 25-Oct-2018) (Revised by AV, 17-Nov-2018)

Ref Expression
Assertion 0csh0 
|- ( (/) cyclShift N ) = (/)

Proof

Step Hyp Ref Expression
1 df-csh 
 |-  cyclShift = ( w e. { f | E. l e. NN0 f Fn ( 0 ..^ l ) } , n e. ZZ |-> if ( w = (/) , (/) , ( ( w substr <. ( n mod ( # ` w ) ) , ( # ` w ) >. ) ++ ( w prefix ( n mod ( # ` w ) ) ) ) ) )
2 1 a1i 
 |-  ( N e. ZZ -> cyclShift = ( w e. { f | E. l e. NN0 f Fn ( 0 ..^ l ) } , n e. ZZ |-> if ( w = (/) , (/) , ( ( w substr <. ( n mod ( # ` w ) ) , ( # ` w ) >. ) ++ ( w prefix ( n mod ( # ` w ) ) ) ) ) ) )
3 iftrue 
 |-  ( w = (/) -> if ( w = (/) , (/) , ( ( w substr <. ( n mod ( # ` w ) ) , ( # ` w ) >. ) ++ ( w prefix ( n mod ( # ` w ) ) ) ) ) = (/) )
4 3 ad2antrl 
 |-  ( ( N e. ZZ /\ ( w = (/) /\ n = N ) ) -> if ( w = (/) , (/) , ( ( w substr <. ( n mod ( # ` w ) ) , ( # ` w ) >. ) ++ ( w prefix ( n mod ( # ` w ) ) ) ) ) = (/) )
5 0nn0 
 |-  0 e. NN0
6 f0 
 |-  (/) : (/) --> _V
7 ffn 
 |-  ( (/) : (/) --> _V -> (/) Fn (/) )
8 fzo0 
 |-  ( 0 ..^ 0 ) = (/)
9 8 eqcomi 
 |-  (/) = ( 0 ..^ 0 )
10 9 fneq2i 
 |-  ( (/) Fn (/) <-> (/) Fn ( 0 ..^ 0 ) )
11 7 10 sylib 
 |-  ( (/) : (/) --> _V -> (/) Fn ( 0 ..^ 0 ) )
12 6 11 ax-mp 
 |-  (/) Fn ( 0 ..^ 0 )
13 id 
 |-  ( 0 e. NN0 -> 0 e. NN0 )
14 oveq2 
 |-  ( l = 0 -> ( 0 ..^ l ) = ( 0 ..^ 0 ) )
15 14 fneq2d 
 |-  ( l = 0 -> ( (/) Fn ( 0 ..^ l ) <-> (/) Fn ( 0 ..^ 0 ) ) )
16 15 adantl 
 |-  ( ( 0 e. NN0 /\ l = 0 ) -> ( (/) Fn ( 0 ..^ l ) <-> (/) Fn ( 0 ..^ 0 ) ) )
17 13 16 rspcedv 
 |-  ( 0 e. NN0 -> ( (/) Fn ( 0 ..^ 0 ) -> E. l e. NN0 (/) Fn ( 0 ..^ l ) ) )
18 5 12 17 mp2 
 |-  E. l e. NN0 (/) Fn ( 0 ..^ l )
19 0ex 
 |-  (/) e. _V
20 fneq1 
 |-  ( f = (/) -> ( f Fn ( 0 ..^ l ) <-> (/) Fn ( 0 ..^ l ) ) )
21 20 rexbidv 
 |-  ( f = (/) -> ( E. l e. NN0 f Fn ( 0 ..^ l ) <-> E. l e. NN0 (/) Fn ( 0 ..^ l ) ) )
22 19 21 elab 
 |-  ( (/) e. { f | E. l e. NN0 f Fn ( 0 ..^ l ) } <-> E. l e. NN0 (/) Fn ( 0 ..^ l ) )
23 18 22 mpbir 
 |-  (/) e. { f | E. l e. NN0 f Fn ( 0 ..^ l ) }
24 23 a1i 
 |-  ( N e. ZZ -> (/) e. { f | E. l e. NN0 f Fn ( 0 ..^ l ) } )
25 id 
 |-  ( N e. ZZ -> N e. ZZ )
26 19 a1i 
 |-  ( N e. ZZ -> (/) e. _V )
27 2 4 24 25 26 ovmpod 
 |-  ( N e. ZZ -> ( (/) cyclShift N ) = (/) )
28 cshnz 
 |-  ( -. N e. ZZ -> ( (/) cyclShift N ) = (/) )
29 27 28 pm2.61i 
 |-  ( (/) cyclShift N ) = (/)