Metamath Proof Explorer

Theorem alginv

Description: If I is an invariant of F , then its value is unchanged after any number of iterations of F . (Contributed by Paul Chapman, 31-Mar-2011)

Ref Expression
Hypotheses alginv.1 
|- R = seq 0 ( ( F o. 1st ) , ( NN0 X. { A } ) )
alginv.2 
|- F : S --> S
alginv.3 
|- ( x e. S -> ( I ` ( F ` x ) ) = ( I ` x ) )
Assertion alginv 
|- ( ( A e. S /\ K e. NN0 ) -> ( I ` ( R ` K ) ) = ( I ` ( R ` 0 ) ) )

Proof

Step Hyp Ref Expression
1 alginv.1 
 |-  R = seq 0 ( ( F o. 1st ) , ( NN0 X. { A } ) )
2 alginv.2 
 |-  F : S --> S
3 alginv.3 
 |-  ( x e. S -> ( I ` ( F ` x ) ) = ( I ` x ) )
4 2fveq3 
 |-  ( z = 0 -> ( I ` ( R ` z ) ) = ( I ` ( R ` 0 ) ) )
5 4 eqeq1d 
 |-  ( z = 0 -> ( ( I ` ( R ` z ) ) = ( I ` ( R ` 0 ) ) <-> ( I ` ( R ` 0 ) ) = ( I ` ( R ` 0 ) ) ) )
6 5 imbi2d 
 |-  ( z = 0 -> ( ( A e. S -> ( I ` ( R ` z ) ) = ( I ` ( R ` 0 ) ) ) <-> ( A e. S -> ( I ` ( R ` 0 ) ) = ( I ` ( R ` 0 ) ) ) ) )
7 2fveq3 
 |-  ( z = k -> ( I ` ( R ` z ) ) = ( I ` ( R ` k ) ) )
8 7 eqeq1d 
 |-  ( z = k -> ( ( I ` ( R ` z ) ) = ( I ` ( R ` 0 ) ) <-> ( I ` ( R ` k ) ) = ( I ` ( R ` 0 ) ) ) )
9 8 imbi2d 
 |-  ( z = k -> ( ( A e. S -> ( I ` ( R ` z ) ) = ( I ` ( R ` 0 ) ) ) <-> ( A e. S -> ( I ` ( R ` k ) ) = ( I ` ( R ` 0 ) ) ) ) )
10 2fveq3 
 |-  ( z = ( k + 1 ) -> ( I ` ( R ` z ) ) = ( I ` ( R ` ( k + 1 ) ) ) )
11 10 eqeq1d 
 |-  ( z = ( k + 1 ) -> ( ( I ` ( R ` z ) ) = ( I ` ( R ` 0 ) ) <-> ( I ` ( R ` ( k + 1 ) ) ) = ( I ` ( R ` 0 ) ) ) )
12 11 imbi2d 
 |-  ( z = ( k + 1 ) -> ( ( A e. S -> ( I ` ( R ` z ) ) = ( I ` ( R ` 0 ) ) ) <-> ( A e. S -> ( I ` ( R ` ( k + 1 ) ) ) = ( I ` ( R ` 0 ) ) ) ) )
13 2fveq3 
 |-  ( z = K -> ( I ` ( R ` z ) ) = ( I ` ( R ` K ) ) )
14 13 eqeq1d 
 |-  ( z = K -> ( ( I ` ( R ` z ) ) = ( I ` ( R ` 0 ) ) <-> ( I ` ( R ` K ) ) = ( I ` ( R ` 0 ) ) ) )
15 14 imbi2d 
 |-  ( z = K -> ( ( A e. S -> ( I ` ( R ` z ) ) = ( I ` ( R ` 0 ) ) ) <-> ( A e. S -> ( I ` ( R ` K ) ) = ( I ` ( R ` 0 ) ) ) ) )
16 eqidd 
 |-  ( A e. S -> ( I ` ( R ` 0 ) ) = ( I ` ( R ` 0 ) ) )
17 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
18 0zd 
 |-  ( A e. S -> 0 e. ZZ )
19 id 
 |-  ( A e. S -> A e. S )
20 2 a1i 
 |-  ( A e. S -> F : S --> S )
21 17 1 18 19 20 algrp1 
 |-  ( ( A e. S /\ k e. NN0 ) -> ( R ` ( k + 1 ) ) = ( F ` ( R ` k ) ) )
22 21 fveq2d 
 |-  ( ( A e. S /\ k e. NN0 ) -> ( I ` ( R ` ( k + 1 ) ) ) = ( I ` ( F ` ( R ` k ) ) ) )
23 17 1 18 19 20 algrf 
 |-  ( A e. S -> R : NN0 --> S )
24 23 ffvelcdmda 
 |-  ( ( A e. S /\ k e. NN0 ) -> ( R ` k ) e. S )
25 2fveq3 
 |-  ( x = ( R ` k ) -> ( I ` ( F ` x ) ) = ( I ` ( F ` ( R ` k ) ) ) )
26 fveq2 
 |-  ( x = ( R ` k ) -> ( I ` x ) = ( I ` ( R ` k ) ) )
27 25 26 eqeq12d 
 |-  ( x = ( R ` k ) -> ( ( I ` ( F ` x ) ) = ( I ` x ) <-> ( I ` ( F ` ( R ` k ) ) ) = ( I ` ( R ` k ) ) ) )
28 27 3 vtoclga 
 |-  ( ( R ` k ) e. S -> ( I ` ( F ` ( R ` k ) ) ) = ( I ` ( R ` k ) ) )
29 24 28 syl 
 |-  ( ( A e. S /\ k e. NN0 ) -> ( I ` ( F ` ( R ` k ) ) ) = ( I ` ( R ` k ) ) )
30 22 29 eqtrd 
 |-  ( ( A e. S /\ k e. NN0 ) -> ( I ` ( R ` ( k + 1 ) ) ) = ( I ` ( R ` k ) ) )
31 30 eqeq1d 
 |-  ( ( A e. S /\ k e. NN0 ) -> ( ( I ` ( R ` ( k + 1 ) ) ) = ( I ` ( R ` 0 ) ) <-> ( I ` ( R ` k ) ) = ( I ` ( R ` 0 ) ) ) )
32 31 biimprd 
 |-  ( ( A e. S /\ k e. NN0 ) -> ( ( I ` ( R ` k ) ) = ( I ` ( R ` 0 ) ) -> ( I ` ( R ` ( k + 1 ) ) ) = ( I ` ( R ` 0 ) ) ) )
33 32 expcom 
 |-  ( k e. NN0 -> ( A e. S -> ( ( I ` ( R ` k ) ) = ( I ` ( R ` 0 ) ) -> ( I ` ( R ` ( k + 1 ) ) ) = ( I ` ( R ` 0 ) ) ) ) )
34 33 a2d 
 |-  ( k e. NN0 -> ( ( A e. S -> ( I ` ( R ` k ) ) = ( I ` ( R ` 0 ) ) ) -> ( A e. S -> ( I ` ( R ` ( k + 1 ) ) ) = ( I ` ( R ` 0 ) ) ) ) )
35 6 9 12 15 16 34 nn0ind 
 |-  ( K e. NN0 -> ( A e. S -> ( I ` ( R ` K ) ) = ( I ` ( R ` 0 ) ) ) )
36 35 impcom 
 |-  ( ( A e. S /\ K e. NN0 ) -> ( I ` ( R ` K ) ) = ( I ` ( R ` 0 ) ) )