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 \circ 1^{st}), (ℕ_{0} \times \{A\}))$
	alginv.2	$⊢ F : S ⟶ S$
	alginv.3	$⊢ x \in S \to I (F (x)) = I (x)$
Assertion	alginv	$⊢ (A \in S \land K \in ℕ_{0}) \to I (R (K)) = I (R (0))$

Proof

Step	Hyp	Ref	Expression
1		alginv.1	$⊢ R = seq 0 ((F \circ 1^{st}), (ℕ_{0} \times \{A\}))$
2		alginv.2	$⊢ F : S ⟶ S$
3		alginv.3	$⊢ x \in S \to I (F (x)) = I (x)$
4		2fveq3	$⊢ z = 0 \to I (R (z)) = I (R (0))$
5	4	eqeq1d	$⊢ z = 0 \to (I (R (z)) = I (R (0)) \leftrightarrow I (R (0)) = I (R (0)))$
6	5	imbi2d	$⊢ z = 0 \to ((A \in S \to I (R (z)) = I (R (0))) \leftrightarrow (A \in S \to I (R (0)) = I (R (0))))$
7		2fveq3	$⊢ z = k \to I (R (z)) = I (R (k))$
8	7	eqeq1d	$⊢ z = k \to (I (R (z)) = I (R (0)) \leftrightarrow I (R (k)) = I (R (0)))$
9	8	imbi2d	$⊢ z = k \to ((A \in S \to I (R (z)) = I (R (0))) \leftrightarrow (A \in S \to I (R (k)) = I (R (0))))$
10		2fveq3	$⊢ z = k + 1 \to I (R (z)) = I (R (k + 1))$
11	10	eqeq1d	$⊢ z = k + 1 \to (I (R (z)) = I (R (0)) \leftrightarrow I (R (k + 1)) = I (R (0)))$
12	11	imbi2d	$⊢ z = k + 1 \to ((A \in S \to I (R (z)) = I (R (0))) \leftrightarrow (A \in S \to I (R (k + 1)) = I (R (0))))$
13		2fveq3	$⊢ z = K \to I (R (z)) = I (R (K))$
14	13	eqeq1d	$⊢ z = K \to (I (R (z)) = I (R (0)) \leftrightarrow I (R (K)) = I (R (0)))$
15	14	imbi2d	$⊢ z = K \to ((A \in S \to I (R (z)) = I (R (0))) \leftrightarrow (A \in S \to I (R (K)) = I (R (0))))$
16		eqidd	$⊢ A \in S \to I (R (0)) = I (R (0))$
17		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
18		0zd	$⊢ A \in S \to 0 \in ℤ$
19		id	$⊢ A \in S \to A \in S$
20	2	a1i	$⊢ A \in S \to F : S ⟶ S$
21	17 1 18 19 20	algrp1	$⊢ (A \in S \land k \in ℕ_{0}) \to R (k + 1) = F (R (k))$
22	21	fveq2d	$⊢ (A \in S \land k \in ℕ_{0}) \to I (R (k + 1)) = I (F (R (k)))$
23	17 1 18 19 20	algrf	$⊢ A \in S \to R : ℕ_{0} ⟶ S$
24	23	ffvelcdmda	$⊢ (A \in S \land k \in ℕ_{0}) \to R (k) \in S$
25		2fveq3	$⊢ x = R (k) \to I (F (x)) = I (F (R (k)))$
26		fveq2	$⊢ x = R (k) \to I (x) = I (R (k))$
27	25 26	eqeq12d	$⊢ x = R (k) \to (I (F (x)) = I (x) \leftrightarrow I (F (R (k))) = I (R (k)))$
28	27 3	vtoclga	$⊢ R (k) \in S \to I (F (R (k))) = I (R (k))$
29	24 28	syl	$⊢ (A \in S \land k \in ℕ_{0}) \to I (F (R (k))) = I (R (k))$
30	22 29	eqtrd	$⊢ (A \in S \land k \in ℕ_{0}) \to I (R (k + 1)) = I (R (k))$
31	30	eqeq1d	$⊢ (A \in S \land k \in ℕ_{0}) \to (I (R (k + 1)) = I (R (0)) \leftrightarrow I (R (k)) = I (R (0)))$
32	31	biimprd	$⊢ (A \in S \land k \in ℕ_{0}) \to (I (R (k)) = I (R (0)) \to I (R (k + 1)) = I (R (0)))$
33	32	expcom	$⊢ k \in ℕ_{0} \to (A \in S \to (I (R (k)) = I (R (0)) \to I (R (k + 1)) = I (R (0))))$
34	33	a2d	$⊢ k \in ℕ_{0} \to ((A \in S \to I (R (k)) = I (R (0))) \to (A \in S \to I (R (k + 1)) = I (R (0))))$
35	6 9 12 15 16 34	nn0ind	$⊢ K \in ℕ_{0} \to (A \in S \to I (R (K)) = I (R (0)))$
36	35	impcom	$⊢ (A \in S \land K \in ℕ_{0}) \to I (R (K)) = I (R (0))$

Metamath Proof Explorer

Theorem alginv

Proof