crctcshwlkn0lem4

	Ref	Expression
Hypotheses	crctcshwlkn0lem.s	$⊢ φ \to S \in (1 ..^N)$
	crctcshwlkn0lem.q	$⊢ Q = (x \in (0 \dots N) ⟼ if (x \leq N - S, P (x + S), P (x + S - N)))$
	crctcshwlkn0lem.h	$⊢ H = F cyclShift S$
	crctcshwlkn0lem.n	$⊢ N = \|F\|$
	crctcshwlkn0lem.f	$⊢ φ \to F \in Word A$
	crctcshwlkn0lem.p	$⊢ φ \to \forall i \in (0 ..^N) if- (P (i) = P (i + 1), I (F (i)) = \{P (i)\}, \{P (i), P (i + 1)\} \subseteq I (F (i)))$
Assertion	crctcshwlkn0lem4	$⊢ φ \to \forall j \in (0 ..^N - S) if- (Q (j) = Q (j + 1), I (H (j)) = \{Q (j)\}, \{Q (j), Q (j + 1)\} \subseteq I (H (j)))$

Proof

Step	Hyp	Ref	Expression
1		crctcshwlkn0lem.s	$⊢ φ \to S \in (1 ..^N)$
2		crctcshwlkn0lem.q	$⊢ Q = (x \in (0 \dots N) ⟼ if (x \leq N - S, P (x + S), P (x + S - N)))$
3		crctcshwlkn0lem.h	$⊢ H = F cyclShift S$
4		crctcshwlkn0lem.n	$⊢ N = \|F\|$
5		crctcshwlkn0lem.f	$⊢ φ \to F \in Word A$
6		crctcshwlkn0lem.p	$⊢ φ \to \forall i \in (0 ..^N) if- (P (i) = P (i + 1), I (F (i)) = \{P (i)\}, \{P (i), P (i + 1)\} \subseteq I (F (i)))$
7		elfzoelz	$⊢ j \in (0 ..^N - S) \to j \in ℤ$
8	7	zcnd	$⊢ j \in (0 ..^N - S) \to j \in ℂ$
9	8	adantl	$⊢ (S \in (1 ..^N) \land j \in (0 ..^N - S)) \to j \in ℂ$
10		elfzoelz	$⊢ S \in (1 ..^N) \to S \in ℤ$
11	10	zcnd	$⊢ S \in (1 ..^N) \to S \in ℂ$
12	11	adantr	$⊢ (S \in (1 ..^N) \land j \in (0 ..^N - S)) \to S \in ℂ$
13		1cnd	$⊢ (S \in (1 ..^N) \land j \in (0 ..^N - S)) \to 1 \in ℂ$
14	9 12 13	add32d	$⊢ (S \in (1 ..^N) \land j \in (0 ..^N - S)) \to j + S + 1 = j + 1 + S$
15		elfzo1	$⊢ S \in (1 ..^N) \leftrightarrow (S \in ℕ \land N \in ℕ \land S < N)$
16		elfzonn0	$⊢ j \in (0 ..^N - S) \to j \in ℕ_{0}$
17		nnnn0	$⊢ S \in ℕ \to S \in ℕ_{0}$
18		nn0addcl	$⊢ (j \in ℕ_{0} \land S \in ℕ_{0}) \to j + S \in ℕ_{0}$
19	18	ex	$⊢ j \in ℕ_{0} \to (S \in ℕ_{0} \to j + S \in ℕ_{0})$
20	16 17 19	syl2imc	$⊢ S \in ℕ \to (j \in (0 ..^N - S) \to j + S \in ℕ_{0})$
21	20	3ad2ant1	$⊢ (S \in ℕ \land N \in ℕ \land S < N) \to (j \in (0 ..^N - S) \to j + S \in ℕ_{0})$
22	15 21	sylbi	$⊢ S \in (1 ..^N) \to (j \in (0 ..^N - S) \to j + S \in ℕ_{0})$
23	22	imp	$⊢ (S \in (1 ..^N) \land j \in (0 ..^N - S)) \to j + S \in ℕ_{0}$
24		fzo0ss1	$⊢ (1 ..^N) \subseteq (0 ..^N)$
25	24	sseli	$⊢ S \in (1 ..^N) \to S \in (0 ..^N)$
26		elfzo0	$⊢ S \in (0 ..^N) \leftrightarrow (S \in ℕ_{0} \land N \in ℕ \land S < N)$
27	26	simp2bi	$⊢ S \in (0 ..^N) \to N \in ℕ$
28	25 27	syl	$⊢ S \in (1 ..^N) \to N \in ℕ$
29	28	adantr	$⊢ (S \in (1 ..^N) \land j \in (0 ..^N - S)) \to N \in ℕ$
30		elfzo0	$⊢ j \in (0 ..^N - S) \leftrightarrow (j \in ℕ_{0} \land N - S \in ℕ \land j < N - S)$
31		nn0re	$⊢ j \in ℕ_{0} \to j \in ℝ$
32		nnre	$⊢ S \in ℕ \to S \in ℝ$
33		nnre	$⊢ N \in ℕ \to N \in ℝ$
34	32 33	anim12i	$⊢ (S \in ℕ \land N \in ℕ) \to (S \in ℝ \land N \in ℝ)$
35	34	3adant3	$⊢ (S \in ℕ \land N \in ℕ \land S < N) \to (S \in ℝ \land N \in ℝ)$
36	15 35	sylbi	$⊢ S \in (1 ..^N) \to (S \in ℝ \land N \in ℝ)$
37	31 36	anim12i	$⊢ (j \in ℕ_{0} \land S \in (1 ..^N)) \to (j \in ℝ \land (S \in ℝ \land N \in ℝ))$
38		3anass	$⊢ (j \in ℝ \land S \in ℝ \land N \in ℝ) \leftrightarrow (j \in ℝ \land (S \in ℝ \land N \in ℝ))$
39	37 38	sylibr	$⊢ (j \in ℕ_{0} \land S \in (1 ..^N)) \to (j \in ℝ \land S \in ℝ \land N \in ℝ)$
40		ltaddsub	$⊢ (j \in ℝ \land S \in ℝ \land N \in ℝ) \to (j + S < N \leftrightarrow j < N - S)$
41	40	bicomd	$⊢ (j \in ℝ \land S \in ℝ \land N \in ℝ) \to (j < N - S \leftrightarrow j + S < N)$
42	39 41	syl	$⊢ (j \in ℕ_{0} \land S \in (1 ..^N)) \to (j < N - S \leftrightarrow j + S < N)$
43	42	biimpd	$⊢ (j \in ℕ_{0} \land S \in (1 ..^N)) \to (j < N - S \to j + S < N)$
44	43	ex	$⊢ j \in ℕ_{0} \to (S \in (1 ..^N) \to (j < N - S \to j + S < N))$
45	44	com23	$⊢ j \in ℕ_{0} \to (j < N - S \to (S \in (1 ..^N) \to j + S < N))$
46	45	a1d	$⊢ j \in ℕ_{0} \to (N - S \in ℕ \to (j < N - S \to (S \in (1 ..^N) \to j + S < N)))$
47	46	3imp	$⊢ (j \in ℕ_{0} \land N - S \in ℕ \land j < N - S) \to (S \in (1 ..^N) \to j + S < N)$
48	30 47	sylbi	$⊢ j \in (0 ..^N - S) \to (S \in (1 ..^N) \to j + S < N)$
49	48	impcom	$⊢ (S \in (1 ..^N) \land j \in (0 ..^N - S)) \to j + S < N$
50		elfzo0	$⊢ j + S \in (0 ..^N) \leftrightarrow (j + S \in ℕ_{0} \land N \in ℕ \land j + S < N)$
51	23 29 49 50	syl3anbrc	$⊢ (S \in (1 ..^N) \land j \in (0 ..^N - S)) \to j + S \in (0 ..^N)$
52	51	adantr	$⊢ ((S \in (1 ..^N) \land j \in (0 ..^N - S)) \land j + S + 1 = j + 1 + S) \to j + S \in (0 ..^N)$
53		fveq2	$⊢ i = j + S \to P (i) = P (j + S)$
54	53	adantl	$⊢ (((S \in (1 ..^N) \land j \in (0 ..^N - S)) \land j + S + 1 = j + 1 + S) \land i = j + S) \to P (i) = P (j + S)$
55		fvoveq1	$⊢ i = j + S \to P (i + 1) = P (j + S + 1)$
56		simpr	$⊢ ((S \in (1 ..^N) \land j \in (0 ..^N - S)) \land j + S + 1 = j + 1 + S) \to j + S + 1 = j + 1 + S$
57	56	fveq2d	$⊢ ((S \in (1 ..^N) \land j \in (0 ..^N - S)) \land j + S + 1 = j + 1 + S) \to P (j + S + 1) = P (j + 1 + S)$
58	55 57	sylan9eqr	$⊢ (((S \in (1 ..^N) \land j \in (0 ..^N - S)) \land j + S + 1 = j + 1 + S) \land i = j + S) \to P (i + 1) = P (j + 1 + S)$
59	54 58	eqeq12d	$⊢ (((S \in (1 ..^N) \land j \in (0 ..^N - S)) \land j + S + 1 = j + 1 + S) \land i = j + S) \to (P (i) = P (i + 1) \leftrightarrow P (j + S) = P (j + 1 + S))$
60		2fveq3	$⊢ i = j + S \to I (F (i)) = I (F (j + S))$
61	53	sneqd	$⊢ i = j + S \to \{P (i)\} = \{P (j + S)\}$
62	60 61	eqeq12d	$⊢ i = j + S \to (I (F (i)) = \{P (i)\} \leftrightarrow I (F (j + S)) = \{P (j + S)\})$
63	62	adantl	$⊢ (((S \in (1 ..^N) \land j \in (0 ..^N - S)) \land j + S + 1 = j + 1 + S) \land i = j + S) \to (I (F (i)) = \{P (i)\} \leftrightarrow I (F (j + S)) = \{P (j + S)\})$
64	54 58	preq12d	$⊢ (((S \in (1 ..^N) \land j \in (0 ..^N - S)) \land j + S + 1 = j + 1 + S) \land i = j + S) \to \{P (i), P (i + 1)\} = \{P (j + S), P (j + 1 + S)\}$
65	60	adantl	$⊢ (((S \in (1 ..^N) \land j \in (0 ..^N - S)) \land j + S + 1 = j + 1 + S) \land i = j + S) \to I (F (i)) = I (F (j + S))$
66	64 65	sseq12d	$⊢ (((S \in (1 ..^N) \land j \in (0 ..^N - S)) \land j + S + 1 = j + 1 + S) \land i = j + S) \to (\{P (i), P (i + 1)\} \subseteq I (F (i)) \leftrightarrow \{P (j + S), P (j + 1 + S)\} \subseteq I (F (j + S)))$
67	59 63 66	ifpbi123d	$⊢ (((S \in (1 ..^N) \land j \in (0 ..^N - S)) \land j + S + 1 = j + 1 + S) \land i = j + S) \to (if- (P (i) = P (i + 1), I (F (i)) = \{P (i)\}, \{P (i), P (i + 1)\} \subseteq I (F (i))) \leftrightarrow if- (P (j + S) = P (j + 1 + S), I (F (j + S)) = \{P (j + S)\}, \{P (j + S), P (j + 1 + S)\} \subseteq I (F (j + S))))$
68	52 67	rspcdv	$⊢ ((S \in (1 ..^N) \land j \in (0 ..^N - S)) \land j + S + 1 = j + 1 + S) \to (\forall i \in (0 ..^N) if- (P (i) = P (i + 1), I (F (i)) = \{P (i)\}, \{P (i), P (i + 1)\} \subseteq I (F (i))) \to if- (P (j + S) = P (j + 1 + S), I (F (j + S)) = \{P (j + S)\}, \{P (j + S), P (j + 1 + S)\} \subseteq I (F (j + S))))$
69	14 68	mpdan	$⊢ (S \in (1 ..^N) \land j \in (0 ..^N - S)) \to (\forall i \in (0 ..^N) if- (P (i) = P (i + 1), I (F (i)) = \{P (i)\}, \{P (i), P (i + 1)\} \subseteq I (F (i))) \to if- (P (j + S) = P (j + 1 + S), I (F (j + S)) = \{P (j + S)\}, \{P (j + S), P (j + 1 + S)\} \subseteq I (F (j + S))))$
70	1 69	sylan	$⊢ (φ \land j \in (0 ..^N - S)) \to (\forall i \in (0 ..^N) if- (P (i) = P (i + 1), I (F (i)) = \{P (i)\}, \{P (i), P (i + 1)\} \subseteq I (F (i))) \to if- (P (j + S) = P (j + 1 + S), I (F (j + S)) = \{P (j + S)\}, \{P (j + S), P (j + 1 + S)\} \subseteq I (F (j + S))))$
71	70	ex	$⊢ φ \to (j \in (0 ..^N - S) \to (\forall i \in (0 ..^N) if- (P (i) = P (i + 1), I (F (i)) = \{P (i)\}, \{P (i), P (i + 1)\} \subseteq I (F (i))) \to if- (P (j + S) = P (j + 1 + S), I (F (j + S)) = \{P (j + S)\}, \{P (j + S), P (j + 1 + S)\} \subseteq I (F (j + S)))))$
72	6 71	mpid	$⊢ φ \to (j \in (0 ..^N - S) \to if- (P (j + S) = P (j + 1 + S), I (F (j + S)) = \{P (j + S)\}, \{P (j + S), P (j + 1 + S)\} \subseteq I (F (j + S))))$
73	72	imp	$⊢ (φ \land j \in (0 ..^N - S)) \to if- (P (j + S) = P (j + 1 + S), I (F (j + S)) = \{P (j + S)\}, \{P (j + S), P (j + 1 + S)\} \subseteq I (F (j + S)))$
74		elfzofz	$⊢ j \in (0 ..^N - S) \to j \in (0 \dots N - S)$
75	1 2	crctcshwlkn0lem2	$⊢ (φ \land j \in (0 \dots N - S)) \to Q (j) = P (j + S)$
76	74 75	sylan2	$⊢ (φ \land j \in (0 ..^N - S)) \to Q (j) = P (j + S)$
77		fzofzp1	$⊢ j \in (0 ..^N - S) \to j + 1 \in (0 \dots N - S)$
78	1 2	crctcshwlkn0lem2	$⊢ (φ \land j + 1 \in (0 \dots N - S)) \to Q (j + 1) = P (j + 1 + S)$
79	77 78	sylan2	$⊢ (φ \land j \in (0 ..^N - S)) \to Q (j + 1) = P (j + 1 + S)$
80	3	fveq1i	$⊢ H (j) = (F cyclShift S) (j)$
81	5	adantr	$⊢ (φ \land j \in (0 ..^N - S)) \to F \in Word A$
82	1 10	syl	$⊢ φ \to S \in ℤ$
83	82	adantr	$⊢ (φ \land j \in (0 ..^N - S)) \to S \in ℤ$
84		nnz	$⊢ N \in ℕ \to N \in ℤ$
85	84	adantl	$⊢ (S \in ℕ \land N \in ℕ) \to N \in ℤ$
86		nnz	$⊢ S \in ℕ \to S \in ℤ$
87	86	adantr	$⊢ (S \in ℕ \land N \in ℕ) \to S \in ℤ$
88	85 87	zsubcld	$⊢ (S \in ℕ \land N \in ℕ) \to N - S \in ℤ$
89	17	nn0ge0d	$⊢ S \in ℕ \to 0 \leq S$
90	89	adantr	$⊢ (S \in ℕ \land N \in ℕ) \to 0 \leq S$
91		subge02	$⊢ (N \in ℝ \land S \in ℝ) \to (0 \leq S \leftrightarrow N - S \leq N)$
92	33 32 91	syl2anr	$⊢ (S \in ℕ \land N \in ℕ) \to (0 \leq S \leftrightarrow N - S \leq N)$
93	90 92	mpbid	$⊢ (S \in ℕ \land N \in ℕ) \to N - S \leq N$
94	88 85 93	3jca	$⊢ (S \in ℕ \land N \in ℕ) \to (N - S \in ℤ \land N \in ℤ \land N - S \leq N)$
95	94	3adant3	$⊢ (S \in ℕ \land N \in ℕ \land S < N) \to (N - S \in ℤ \land N \in ℤ \land N - S \leq N)$
96	15 95	sylbi	$⊢ S \in (1 ..^N) \to (N - S \in ℤ \land N \in ℤ \land N - S \leq N)$
97		eluz2	$⊢ N \in ℤ_{\geq (N - S)} \leftrightarrow (N - S \in ℤ \land N \in ℤ \land N - S \leq N)$
98	96 97	sylibr	$⊢ S \in (1 ..^N) \to N \in ℤ_{\geq (N - S)}$
99		fzoss2	$⊢ N \in ℤ_{\geq (N - S)} \to (0 ..^N - S) \subseteq (0 ..^N)$
100	1 98 99	3syl	$⊢ φ \to (0 ..^N - S) \subseteq (0 ..^N)$
101	100	sselda	$⊢ (φ \land j \in (0 ..^N - S)) \to j \in (0 ..^N)$
102	4	oveq2i	$⊢ (0 ..^N) = (0 ..^\|F\|)$
103	101 102	eleqtrdi	$⊢ (φ \land j \in (0 ..^N - S)) \to j \in (0 ..^\|F\|)$
104		cshwidxmod	$⊢ (F \in Word A \land S \in ℤ \land j \in (0 ..^\|F\|)) \to (F cyclShift S) (j) = F ((j + S) \mod \|F\|)$
105	81 83 103 104	syl3anc	$⊢ (φ \land j \in (0 ..^N - S)) \to (F cyclShift S) (j) = F ((j + S) \mod \|F\|)$
106	4	eqcomi	$⊢ \|F\| = N$
107	106	oveq2i	$⊢ (j + S) \mod \|F\| = (j + S) \mod N$
108	21	imp	$⊢ ((S \in ℕ \land N \in ℕ \land S < N) \land j \in (0 ..^N - S)) \to j + S \in ℕ_{0}$
109		nnm1nn0	$⊢ N \in ℕ \to N - 1 \in ℕ_{0}$
110	109	3ad2ant2	$⊢ (S \in ℕ \land N \in ℕ \land S < N) \to N - 1 \in ℕ_{0}$
111	110	adantr	$⊢ ((S \in ℕ \land N \in ℕ \land S < N) \land j \in (0 ..^N - S)) \to N - 1 \in ℕ_{0}$
112	31 35	anim12i	$⊢ (j \in ℕ_{0} \land (S \in ℕ \land N \in ℕ \land S < N)) \to (j \in ℝ \land (S \in ℝ \land N \in ℝ))$
113	112 38	sylibr	$⊢ (j \in ℕ_{0} \land (S \in ℕ \land N \in ℕ \land S < N)) \to (j \in ℝ \land S \in ℝ \land N \in ℝ)$
114	113 41	syl	$⊢ (j \in ℕ_{0} \land (S \in ℕ \land N \in ℕ \land S < N)) \to (j < N - S \leftrightarrow j + S < N)$
115	17	3ad2ant1	$⊢ (S \in ℕ \land N \in ℕ \land S < N) \to S \in ℕ_{0}$
116	115 18	sylan2	$⊢ (j \in ℕ_{0} \land (S \in ℕ \land N \in ℕ \land S < N)) \to j + S \in ℕ_{0}$
117	116	nn0zd	$⊢ (j \in ℕ_{0} \land (S \in ℕ \land N \in ℕ \land S < N)) \to j + S \in ℤ$
118	84	3ad2ant2	$⊢ (S \in ℕ \land N \in ℕ \land S < N) \to N \in ℤ$
119	118	adantl	$⊢ (j \in ℕ_{0} \land (S \in ℕ \land N \in ℕ \land S < N)) \to N \in ℤ$
120		zltlem1	$⊢ (j + S \in ℤ \land N \in ℤ) \to (j + S < N \leftrightarrow j + S \leq N - 1)$
121	117 119 120	syl2anc	$⊢ (j \in ℕ_{0} \land (S \in ℕ \land N \in ℕ \land S < N)) \to (j + S < N \leftrightarrow j + S \leq N - 1)$
122	121	biimpd	$⊢ (j \in ℕ_{0} \land (S \in ℕ \land N \in ℕ \land S < N)) \to (j + S < N \to j + S \leq N - 1)$
123	114 122	sylbid	$⊢ (j \in ℕ_{0} \land (S \in ℕ \land N \in ℕ \land S < N)) \to (j < N - S \to j + S \leq N - 1)$
124	123	impancom	$⊢ (j \in ℕ_{0} \land j < N - S) \to ((S \in ℕ \land N \in ℕ \land S < N) \to j + S \leq N - 1)$
125	124	3adant2	$⊢ (j \in ℕ_{0} \land N - S \in ℕ \land j < N - S) \to ((S \in ℕ \land N \in ℕ \land S < N) \to j + S \leq N - 1)$
126	30 125	sylbi	$⊢ j \in (0 ..^N - S) \to ((S \in ℕ \land N \in ℕ \land S < N) \to j + S \leq N - 1)$
127	126	impcom	$⊢ ((S \in ℕ \land N \in ℕ \land S < N) \land j \in (0 ..^N - S)) \to j + S \leq N - 1$
128	108 111 127	3jca	$⊢ ((S \in ℕ \land N \in ℕ \land S < N) \land j \in (0 ..^N - S)) \to (j + S \in ℕ_{0} \land N - 1 \in ℕ_{0} \land j + S \leq N - 1)$
129	15 128	sylanb	$⊢ (S \in (1 ..^N) \land j \in (0 ..^N - S)) \to (j + S \in ℕ_{0} \land N - 1 \in ℕ_{0} \land j + S \leq N - 1)$
130		elfz2nn0	$⊢ j + S \in (0 \dots N - 1) \leftrightarrow (j + S \in ℕ_{0} \land N - 1 \in ℕ_{0} \land j + S \leq N - 1)$
131	129 130	sylibr	$⊢ (S \in (1 ..^N) \land j \in (0 ..^N - S)) \to j + S \in (0 \dots N - 1)$
132		zaddcl	$⊢ (j \in ℤ \land S \in ℤ) \to j + S \in ℤ$
133	7 10 132	syl2anr	$⊢ (S \in (1 ..^N) \land j \in (0 ..^N - S)) \to j + S \in ℤ$
134		zmodid2	$⊢ (j + S \in ℤ \land N \in ℕ) \to ((j + S) \mod N = j + S \leftrightarrow j + S \in (0 \dots N - 1))$
135	133 29 134	syl2anc	$⊢ (S \in (1 ..^N) \land j \in (0 ..^N - S)) \to ((j + S) \mod N = j + S \leftrightarrow j + S \in (0 \dots N - 1))$
136	131 135	mpbird	$⊢ (S \in (1 ..^N) \land j \in (0 ..^N - S)) \to (j + S) \mod N = j + S$
137	1 136	sylan	$⊢ (φ \land j \in (0 ..^N - S)) \to (j + S) \mod N = j + S$
138	107 137	syl5eq	$⊢ (φ \land j \in (0 ..^N - S)) \to (j + S) \mod \|F\| = j + S$
139	138	fveq2d	$⊢ (φ \land j \in (0 ..^N - S)) \to F ((j + S) \mod \|F\|) = F (j + S)$
140	105 139	eqtrd	$⊢ (φ \land j \in (0 ..^N - S)) \to (F cyclShift S) (j) = F (j + S)$
141	80 140	syl5eq	$⊢ (φ \land j \in (0 ..^N - S)) \to H (j) = F (j + S)$
142	141	fveq2d	$⊢ (φ \land j \in (0 ..^N - S)) \to I (H (j)) = I (F (j + S))$
143		simp1	$⊢ (Q (j) = P (j + S) \land Q (j + 1) = P (j + 1 + S) \land I (H (j)) = I (F (j + S))) \to Q (j) = P (j + S)$
144		simp2	$⊢ (Q (j) = P (j + S) \land Q (j + 1) = P (j + 1 + S) \land I (H (j)) = I (F (j + S))) \to Q (j + 1) = P (j + 1 + S)$
145	143 144	eqeq12d	$⊢ (Q (j) = P (j + S) \land Q (j + 1) = P (j + 1 + S) \land I (H (j)) = I (F (j + S))) \to (Q (j) = Q (j + 1) \leftrightarrow P (j + S) = P (j + 1 + S))$
146		simp3	$⊢ (Q (j) = P (j + S) \land Q (j + 1) = P (j + 1 + S) \land I (H (j)) = I (F (j + S))) \to I (H (j)) = I (F (j + S))$
147	143	sneqd	$⊢ (Q (j) = P (j + S) \land Q (j + 1) = P (j + 1 + S) \land I (H (j)) = I (F (j + S))) \to \{Q (j)\} = \{P (j + S)\}$
148	146 147	eqeq12d	$⊢ (Q (j) = P (j + S) \land Q (j + 1) = P (j + 1 + S) \land I (H (j)) = I (F (j + S))) \to (I (H (j)) = \{Q (j)\} \leftrightarrow I (F (j + S)) = \{P (j + S)\})$
149	143 144	preq12d	$⊢ (Q (j) = P (j + S) \land Q (j + 1) = P (j + 1 + S) \land I (H (j)) = I (F (j + S))) \to \{Q (j), Q (j + 1)\} = \{P (j + S), P (j + 1 + S)\}$
150	149 146	sseq12d	$⊢ (Q (j) = P (j + S) \land Q (j + 1) = P (j + 1 + S) \land I (H (j)) = I (F (j + S))) \to (\{Q (j), Q (j + 1)\} \subseteq I (H (j)) \leftrightarrow \{P (j + S), P (j + 1 + S)\} \subseteq I (F (j + S)))$
151	145 148 150	ifpbi123d	$⊢ (Q (j) = P (j + S) \land Q (j + 1) = P (j + 1 + S) \land I (H (j)) = I (F (j + S))) \to (if- (Q (j) = Q (j + 1), I (H (j)) = \{Q (j)\}, \{Q (j), Q (j + 1)\} \subseteq I (H (j))) \leftrightarrow if- (P (j + S) = P (j + 1 + S), I (F (j + S)) = \{P (j + S)\}, \{P (j + S), P (j + 1 + S)\} \subseteq I (F (j + S))))$
152	76 79 142 151	syl3anc	$⊢ (φ \land j \in (0 ..^N - S)) \to (if- (Q (j) = Q (j + 1), I (H (j)) = \{Q (j)\}, \{Q (j), Q (j + 1)\} \subseteq I (H (j))) \leftrightarrow if- (P (j + S) = P (j + 1 + S), I (F (j + S)) = \{P (j + S)\}, \{P (j + S), P (j + 1 + S)\} \subseteq I (F (j + S))))$
153	73 152	mpbird	$⊢ (φ \land j \in (0 ..^N - S)) \to if- (Q (j) = Q (j + 1), I (H (j)) = \{Q (j)\}, \{Q (j), Q (j + 1)\} \subseteq I (H (j)))$
154	153	ralrimiva	$⊢ φ \to \forall j \in (0 ..^N - S) if- (Q (j) = Q (j + 1), I (H (j)) = \{Q (j)\}, \{Q (j), Q (j + 1)\} \subseteq I (H (j)))$

Metamath Proof Explorer

Theorem crctcshwlkn0lem4

Proof