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 ⊢ 𝑅 = seq 0 ( ( 𝐹 ∘ 1st ) , ( ℕ0 × { 𝐴 } ) )
alginv.2 ⊢ 𝐹 : 𝑆 ⟶ 𝑆
alginv.3 ⊢ ( 𝑥 ∈ 𝑆 → ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) = ( 𝐼 ‘ 𝑥 ) )
Assertion alginv ( ( 𝐴 ∈ 𝑆 ∧ 𝐾 ∈ ℕ0 ) → ( 𝐼 ‘ ( 𝑅 ‘ 𝐾 ) ) = ( 𝐼 ‘ ( 𝑅 ‘ 0 ) ) )

Proof

Step Hyp Ref Expression
1 alginv.1 ⊢ 𝑅 = seq 0 ( ( 𝐹 ∘ 1st ) , ( ℕ0 × { 𝐴 } ) )
2 alginv.2 ⊢ 𝐹 : 𝑆 ⟶ 𝑆
3 alginv.3 ⊢ ( 𝑥 ∈ 𝑆 → ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) = ( 𝐼 ‘ 𝑥 ) )
4 2fveq3 ⊢ ( 𝑧 = 0 → ( 𝐼 ‘ ( 𝑅 ‘ 𝑧 ) ) = ( 𝐼 ‘ ( 𝑅 ‘ 0 ) ) )
5 4 eqeq1d ⊢ ( 𝑧 = 0 → ( ( 𝐼 ‘ ( 𝑅 ‘ 𝑧 ) ) = ( 𝐼 ‘ ( 𝑅 ‘ 0 ) ) ↔ ( 𝐼 ‘ ( 𝑅 ‘ 0 ) ) = ( 𝐼 ‘ ( 𝑅 ‘ 0 ) ) ) )
6 5 imbi2d ⊢ ( 𝑧 = 0 → ( ( 𝐴 ∈ 𝑆 → ( 𝐼 ‘ ( 𝑅 ‘ 𝑧 ) ) = ( 𝐼 ‘ ( 𝑅 ‘ 0 ) ) ) ↔ ( 𝐴 ∈ 𝑆 → ( 𝐼 ‘ ( 𝑅 ‘ 0 ) ) = ( 𝐼 ‘ ( 𝑅 ‘ 0 ) ) ) ) )
7 2fveq3 ⊢ ( 𝑧 = 𝑘 → ( 𝐼 ‘ ( 𝑅 ‘ 𝑧 ) ) = ( 𝐼 ‘ ( 𝑅 ‘ 𝑘 ) ) )
8 7 eqeq1d ⊢ ( 𝑧 = 𝑘 → ( ( 𝐼 ‘ ( 𝑅 ‘ 𝑧 ) ) = ( 𝐼 ‘ ( 𝑅 ‘ 0 ) ) ↔ ( 𝐼 ‘ ( 𝑅 ‘ 𝑘 ) ) = ( 𝐼 ‘ ( 𝑅 ‘ 0 ) ) ) )
9 8 imbi2d ⊢ ( 𝑧 = 𝑘 → ( ( 𝐴 ∈ 𝑆 → ( 𝐼 ‘ ( 𝑅 ‘ 𝑧 ) ) = ( 𝐼 ‘ ( 𝑅 ‘ 0 ) ) ) ↔ ( 𝐴 ∈ 𝑆 → ( 𝐼 ‘ ( 𝑅 ‘ 𝑘 ) ) = ( 𝐼 ‘ ( 𝑅 ‘ 0 ) ) ) ) )
10 2fveq3 ⊢ ( 𝑧 = ( 𝑘 + 1 ) → ( 𝐼 ‘ ( 𝑅 ‘ 𝑧 ) ) = ( 𝐼 ‘ ( 𝑅 ‘ ( 𝑘 + 1 ) ) ) )
11 10 eqeq1d ⊢ ( 𝑧 = ( 𝑘 + 1 ) → ( ( 𝐼 ‘ ( 𝑅 ‘ 𝑧 ) ) = ( 𝐼 ‘ ( 𝑅 ‘ 0 ) ) ↔ ( 𝐼 ‘ ( 𝑅 ‘ ( 𝑘 + 1 ) ) ) = ( 𝐼 ‘ ( 𝑅 ‘ 0 ) ) ) )
12 11 imbi2d ⊢ ( 𝑧 = ( 𝑘 + 1 ) → ( ( 𝐴 ∈ 𝑆 → ( 𝐼 ‘ ( 𝑅 ‘ 𝑧 ) ) = ( 𝐼 ‘ ( 𝑅 ‘ 0 ) ) ) ↔ ( 𝐴 ∈ 𝑆 → ( 𝐼 ‘ ( 𝑅 ‘ ( 𝑘 + 1 ) ) ) = ( 𝐼 ‘ ( 𝑅 ‘ 0 ) ) ) ) )
13 2fveq3 ⊢ ( 𝑧 = 𝐾 → ( 𝐼 ‘ ( 𝑅 ‘ 𝑧 ) ) = ( 𝐼 ‘ ( 𝑅 ‘ 𝐾 ) ) )
14 13 eqeq1d ⊢ ( 𝑧 = 𝐾 → ( ( 𝐼 ‘ ( 𝑅 ‘ 𝑧 ) ) = ( 𝐼 ‘ ( 𝑅 ‘ 0 ) ) ↔ ( 𝐼 ‘ ( 𝑅 ‘ 𝐾 ) ) = ( 𝐼 ‘ ( 𝑅 ‘ 0 ) ) ) )
15 14 imbi2d ⊢ ( 𝑧 = 𝐾 → ( ( 𝐴 ∈ 𝑆 → ( 𝐼 ‘ ( 𝑅 ‘ 𝑧 ) ) = ( 𝐼 ‘ ( 𝑅 ‘ 0 ) ) ) ↔ ( 𝐴 ∈ 𝑆 → ( 𝐼 ‘ ( 𝑅 ‘ 𝐾 ) ) = ( 𝐼 ‘ ( 𝑅 ‘ 0 ) ) ) ) )
16 eqidd ⊢ ( 𝐴 ∈ 𝑆 → ( 𝐼 ‘ ( 𝑅 ‘ 0 ) ) = ( 𝐼 ‘ ( 𝑅 ‘ 0 ) ) )
17 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
18 0zd ⊢ ( 𝐴 ∈ 𝑆 → 0 ∈ ℤ )
19 id ⊢ ( 𝐴 ∈ 𝑆 → 𝐴 ∈ 𝑆 )
20 2 a1i ⊢ ( 𝐴 ∈ 𝑆 → 𝐹 : 𝑆 ⟶ 𝑆 )
21 17 1 18 19 20 algrp1 ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝑘 ∈ ℕ0 ) → ( 𝑅 ‘ ( 𝑘 + 1 ) ) = ( 𝐹 ‘ ( 𝑅 ‘ 𝑘 ) ) )
22 21 fveq2d ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐼 ‘ ( 𝑅 ‘ ( 𝑘 + 1 ) ) ) = ( 𝐼 ‘ ( 𝐹 ‘ ( 𝑅 ‘ 𝑘 ) ) ) )
23 17 1 18 19 20 algrf ⊢ ( 𝐴 ∈ 𝑆 → 𝑅 : ℕ0 ⟶ 𝑆 )
24 23 ffvelcdmda ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝑘 ∈ ℕ0 ) → ( 𝑅 ‘ 𝑘 ) ∈ 𝑆 )
25 2fveq3 ⊢ ( 𝑥 = ( 𝑅 ‘ 𝑘 ) → ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) = ( 𝐼 ‘ ( 𝐹 ‘ ( 𝑅 ‘ 𝑘 ) ) ) )
26 fveq2 ⊢ ( 𝑥 = ( 𝑅 ‘ 𝑘 ) → ( 𝐼 ‘ 𝑥 ) = ( 𝐼 ‘ ( 𝑅 ‘ 𝑘 ) ) )
27 25 26 eqeq12d ⊢ ( 𝑥 = ( 𝑅 ‘ 𝑘 ) → ( ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) = ( 𝐼 ‘ 𝑥 ) ↔ ( 𝐼 ‘ ( 𝐹 ‘ ( 𝑅 ‘ 𝑘 ) ) ) = ( 𝐼 ‘ ( 𝑅 ‘ 𝑘 ) ) ) )
28 27 3 vtoclga ⊢ ( ( 𝑅 ‘ 𝑘 ) ∈ 𝑆 → ( 𝐼 ‘ ( 𝐹 ‘ ( 𝑅 ‘ 𝑘 ) ) ) = ( 𝐼 ‘ ( 𝑅 ‘ 𝑘 ) ) )
29 24 28 syl ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐼 ‘ ( 𝐹 ‘ ( 𝑅 ‘ 𝑘 ) ) ) = ( 𝐼 ‘ ( 𝑅 ‘ 𝑘 ) ) )
30 22 29 eqtrd ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐼 ‘ ( 𝑅 ‘ ( 𝑘 + 1 ) ) ) = ( 𝐼 ‘ ( 𝑅 ‘ 𝑘 ) ) )
31 30 eqeq1d ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐼 ‘ ( 𝑅 ‘ ( 𝑘 + 1 ) ) ) = ( 𝐼 ‘ ( 𝑅 ‘ 0 ) ) ↔ ( 𝐼 ‘ ( 𝑅 ‘ 𝑘 ) ) = ( 𝐼 ‘ ( 𝑅 ‘ 0 ) ) ) )
32 31 biimprd ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐼 ‘ ( 𝑅 ‘ 𝑘 ) ) = ( 𝐼 ‘ ( 𝑅 ‘ 0 ) ) → ( 𝐼 ‘ ( 𝑅 ‘ ( 𝑘 + 1 ) ) ) = ( 𝐼 ‘ ( 𝑅 ‘ 0 ) ) ) )
33 32 expcom ⊢ ( 𝑘 ∈ ℕ0 → ( 𝐴 ∈ 𝑆 → ( ( 𝐼 ‘ ( 𝑅 ‘ 𝑘 ) ) = ( 𝐼 ‘ ( 𝑅 ‘ 0 ) ) → ( 𝐼 ‘ ( 𝑅 ‘ ( 𝑘 + 1 ) ) ) = ( 𝐼 ‘ ( 𝑅 ‘ 0 ) ) ) ) )
34 33 a2d ⊢ ( 𝑘 ∈ ℕ0 → ( ( 𝐴 ∈ 𝑆 → ( 𝐼 ‘ ( 𝑅 ‘ 𝑘 ) ) = ( 𝐼 ‘ ( 𝑅 ‘ 0 ) ) ) → ( 𝐴 ∈ 𝑆 → ( 𝐼 ‘ ( 𝑅 ‘ ( 𝑘 + 1 ) ) ) = ( 𝐼 ‘ ( 𝑅 ‘ 0 ) ) ) ) )
35 6 9 12 15 16 34 nn0ind ⊢ ( 𝐾 ∈ ℕ0 → ( 𝐴 ∈ 𝑆 → ( 𝐼 ‘ ( 𝑅 ‘ 𝐾 ) ) = ( 𝐼 ‘ ( 𝑅 ‘ 0 ) ) ) )
36 35 impcom ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐾 ∈ ℕ0 ) → ( 𝐼 ‘ ( 𝑅 ‘ 𝐾 ) ) = ( 𝐼 ‘ ( 𝑅 ‘ 0 ) ) )