crctcshwlkn0

Description: Cyclically shifting the indices of a circuit <. F , P >. results in a walk <. H , Q >. . (Contributed by AV, 10-Mar-2021)

	Ref	Expression
Hypotheses	crctcsh.v	$⊢ V = Vtx (G)$
	crctcsh.i	$⊢ I = iEdg (G)$
	crctcsh.d	$⊢ φ \to F Circuits (G) P$
	crctcsh.n	$⊢ N = \|F\|$
	crctcsh.s	$⊢ φ \to S \in (0 ..^N)$
	crctcsh.h	$⊢ H = F cyclShift S$
	crctcsh.q	$⊢ Q = (x \in (0 \dots N) ⟼ if (x \leq N - S, P (x + S), P (x + S - N)))$
Assertion	crctcshwlkn0	$⊢ (φ \land S \neq 0) \to H Walks (G) Q$

Proof

Step	Hyp	Ref	Expression
1		crctcsh.v	$⊢ V = Vtx (G)$
2		crctcsh.i	$⊢ I = iEdg (G)$
3		crctcsh.d	$⊢ φ \to F Circuits (G) P$
4		crctcsh.n	$⊢ N = \|F\|$
5		crctcsh.s	$⊢ φ \to S \in (0 ..^N)$
6		crctcsh.h	$⊢ H = F cyclShift S$
7		crctcsh.q	$⊢ Q = (x \in (0 \dots N) ⟼ if (x \leq N - S, P (x + S), P (x + S - N)))$
8		crctiswlk	$⊢ F Circuits (G) P \to F Walks (G) P$
9	2	wlkf	$⊢ F Walks (G) P \to F \in Word dom I$
10	3 8 9	3syl	$⊢ φ \to F \in Word dom I$
11		cshwcl	$⊢ F \in Word dom I \to F cyclShift S \in Word dom I$
12	10 11	syl	$⊢ φ \to F cyclShift S \in Word dom I$
13	6 12	eqeltrid	$⊢ φ \to H \in Word dom I$
14	13	adantr	$⊢ (φ \land S \neq 0) \to H \in Word dom I$
15	3 8	syl	$⊢ φ \to F Walks (G) P$
16	1	wlkp	$⊢ F Walks (G) P \to P : (0 \dots \|F\|) ⟶ V$
17		simpll	$⊢ ((P : (0 \dots \|F\|) ⟶ V \land (φ \land x \in (0 \dots N))) \land x \leq N - S) \to P : (0 \dots \|F\|) ⟶ V$
18		elfznn0	$⊢ x \in (0 \dots N) \to x \in ℕ_{0}$
19	18	adantl	$⊢ (S \in (0 ..^N) \land x \in (0 \dots N)) \to x \in ℕ_{0}$
20		elfzonn0	$⊢ S \in (0 ..^N) \to S \in ℕ_{0}$
21	20	adantr	$⊢ (S \in (0 ..^N) \land x \in (0 \dots N)) \to S \in ℕ_{0}$
22	19 21	nn0addcld	$⊢ (S \in (0 ..^N) \land x \in (0 \dots N)) \to x + S \in ℕ_{0}$
23	22	adantr	$⊢ ((S \in (0 ..^N) \land x \in (0 \dots N)) \land x \leq N - S) \to x + S \in ℕ_{0}$
24		elfz3nn0	$⊢ x \in (0 \dots N) \to N \in ℕ_{0}$
25	4 24	eqeltrrid	$⊢ x \in (0 \dots N) \to \|F\| \in ℕ_{0}$
26	25	ad2antlr	$⊢ ((S \in (0 ..^N) \land x \in (0 \dots N)) \land x \leq N - S) \to \|F\| \in ℕ_{0}$
27		elfzelz	$⊢ x \in (0 \dots N) \to x \in ℤ$
28	27	zred	$⊢ x \in (0 \dots N) \to x \in ℝ$
29	28	adantl	$⊢ (S \in (0 ..^N) \land x \in (0 \dots N)) \to x \in ℝ$
30		elfzoelz	$⊢ S \in (0 ..^N) \to S \in ℤ$
31	30	zred	$⊢ S \in (0 ..^N) \to S \in ℝ$
32	31	adantr	$⊢ (S \in (0 ..^N) \land x \in (0 \dots N)) \to S \in ℝ$
33		elfzel2	$⊢ x \in (0 \dots N) \to N \in ℤ$
34	33	zred	$⊢ x \in (0 \dots N) \to N \in ℝ$
35	34	adantl	$⊢ (S \in (0 ..^N) \land x \in (0 \dots N)) \to N \in ℝ$
36		leaddsub	$⊢ (x \in ℝ \land S \in ℝ \land N \in ℝ) \to (x + S \leq N \leftrightarrow x \leq N - S)$
37	29 32 35 36	syl3anc	$⊢ (S \in (0 ..^N) \land x \in (0 \dots N)) \to (x + S \leq N \leftrightarrow x \leq N - S)$
38	37	biimpar	$⊢ ((S \in (0 ..^N) \land x \in (0 \dots N)) \land x \leq N - S) \to x + S \leq N$
39	38 4	breqtrdi	$⊢ ((S \in (0 ..^N) \land x \in (0 \dots N)) \land x \leq N - S) \to x + S \leq \|F\|$
40	23 26 39	3jca	$⊢ ((S \in (0 ..^N) \land x \in (0 \dots N)) \land x \leq N - S) \to (x + S \in ℕ_{0} \land \|F\| \in ℕ_{0} \land x + S \leq \|F\|)$
41	5 40	sylanl1	$⊢ ((φ \land x \in (0 \dots N)) \land x \leq N - S) \to (x + S \in ℕ_{0} \land \|F\| \in ℕ_{0} \land x + S \leq \|F\|)$
42		elfz2nn0	$⊢ x + S \in (0 \dots \|F\|) \leftrightarrow (x + S \in ℕ_{0} \land \|F\| \in ℕ_{0} \land x + S \leq \|F\|)$
43	41 42	sylibr	$⊢ ((φ \land x \in (0 \dots N)) \land x \leq N - S) \to x + S \in (0 \dots \|F\|)$
44	43	adantll	$⊢ ((P : (0 \dots \|F\|) ⟶ V \land (φ \land x \in (0 \dots N))) \land x \leq N - S) \to x + S \in (0 \dots \|F\|)$
45	17 44	ffvelcdmd	$⊢ ((P : (0 \dots \|F\|) ⟶ V \land (φ \land x \in (0 \dots N))) \land x \leq N - S) \to P (x + S) \in V$
46		simpll	$⊢ ((P : (0 \dots \|F\|) ⟶ V \land (φ \land x \in (0 \dots N))) \land \neg x \leq N - S) \to P : (0 \dots \|F\|) ⟶ V$
47		elfzoel2	$⊢ S \in (0 ..^N) \to N \in ℤ$
48		zaddcl	$⊢ (x \in ℤ \land S \in ℤ) \to x + S \in ℤ$
49	48	adantrr	$⊢ (x \in ℤ \land (S \in ℤ \land N \in ℤ)) \to x + S \in ℤ$
50		simprr	$⊢ (x \in ℤ \land (S \in ℤ \land N \in ℤ)) \to N \in ℤ$
51	49 50	zsubcld	$⊢ (x \in ℤ \land (S \in ℤ \land N \in ℤ)) \to x + S - N \in ℤ$
52	51	adantr	$⊢ ((x \in ℤ \land (S \in ℤ \land N \in ℤ)) \land \neg x \leq N - S) \to x + S - N \in ℤ$
53		zsubcl	$⊢ (N \in ℤ \land S \in ℤ) \to N - S \in ℤ$
54	53	ancoms	$⊢ (S \in ℤ \land N \in ℤ) \to N - S \in ℤ$
55	54	zred	$⊢ (S \in ℤ \land N \in ℤ) \to N - S \in ℝ$
56		zre	$⊢ x \in ℤ \to x \in ℝ$
57		ltnle	$⊢ (N - S \in ℝ \land x \in ℝ) \to (N - S < x \leftrightarrow \neg x \leq N - S)$
58	55 56 57	syl2anr	$⊢ (x \in ℤ \land (S \in ℤ \land N \in ℤ)) \to (N - S < x \leftrightarrow \neg x \leq N - S)$
59		zre	$⊢ N \in ℤ \to N \in ℝ$
60	59	adantl	$⊢ (S \in ℤ \land N \in ℤ) \to N \in ℝ$
61		zre	$⊢ S \in ℤ \to S \in ℝ$
62	61	adantr	$⊢ (S \in ℤ \land N \in ℤ) \to S \in ℝ$
63	56	adantr	$⊢ (x \in ℤ \land (S \in ℤ \land N \in ℤ)) \to x \in ℝ$
64		ltsubadd	$⊢ (N \in ℝ \land S \in ℝ \land x \in ℝ) \to (N - S < x \leftrightarrow N < x + S)$
65	60 62 63 64	syl2an23an	$⊢ (x \in ℤ \land (S \in ℤ \land N \in ℤ)) \to (N - S < x \leftrightarrow N < x + S)$
66	60	adantl	$⊢ (x \in ℤ \land (S \in ℤ \land N \in ℤ)) \to N \in ℝ$
67	49	zred	$⊢ (x \in ℤ \land (S \in ℤ \land N \in ℤ)) \to x + S \in ℝ$
68	66 67	posdifd	$⊢ (x \in ℤ \land (S \in ℤ \land N \in ℤ)) \to (N < x + S \leftrightarrow 0 < x + S - N)$
69		0red	$⊢ (x \in ℤ \land (S \in ℤ \land N \in ℤ)) \to 0 \in ℝ$
70	51	zred	$⊢ (x \in ℤ \land (S \in ℤ \land N \in ℤ)) \to x + S - N \in ℝ$
71		ltle	$⊢ (0 \in ℝ \land x + S - N \in ℝ) \to (0 < x + S - N \to 0 \leq x + S - N)$
72	69 70 71	syl2anc	$⊢ (x \in ℤ \land (S \in ℤ \land N \in ℤ)) \to (0 < x + S - N \to 0 \leq x + S - N)$
73	68 72	sylbid	$⊢ (x \in ℤ \land (S \in ℤ \land N \in ℤ)) \to (N < x + S \to 0 \leq x + S - N)$
74	65 73	sylbid	$⊢ (x \in ℤ \land (S \in ℤ \land N \in ℤ)) \to (N - S < x \to 0 \leq x + S - N)$
75	58 74	sylbird	$⊢ (x \in ℤ \land (S \in ℤ \land N \in ℤ)) \to (\neg x \leq N - S \to 0 \leq x + S - N)$
76	75	imp	$⊢ ((x \in ℤ \land (S \in ℤ \land N \in ℤ)) \land \neg x \leq N - S) \to 0 \leq x + S - N$
77	52 76	jca	$⊢ ((x \in ℤ \land (S \in ℤ \land N \in ℤ)) \land \neg x \leq N - S) \to (x + S - N \in ℤ \land 0 \leq x + S - N)$
78	77	exp31	$⊢ x \in ℤ \to ((S \in ℤ \land N \in ℤ) \to (\neg x \leq N - S \to (x + S - N \in ℤ \land 0 \leq x + S - N)))$
79	78 27	syl11	$⊢ (S \in ℤ \land N \in ℤ) \to (x \in (0 \dots N) \to (\neg x \leq N - S \to (x + S - N \in ℤ \land 0 \leq x + S - N)))$
80	30 47 79	syl2anc	$⊢ S \in (0 ..^N) \to (x \in (0 \dots N) \to (\neg x \leq N - S \to (x + S - N \in ℤ \land 0 \leq x + S - N)))$
81	80	imp31	$⊢ ((S \in (0 ..^N) \land x \in (0 \dots N)) \land \neg x \leq N - S) \to (x + S - N \in ℤ \land 0 \leq x + S - N)$
82		elnn0z	$⊢ x + S - N \in ℕ_{0} \leftrightarrow (x + S - N \in ℤ \land 0 \leq x + S - N)$
83	81 82	sylibr	$⊢ ((S \in (0 ..^N) \land x \in (0 \dots N)) \land \neg x \leq N - S) \to x + S - N \in ℕ_{0}$
84	25	ad2antlr	$⊢ ((S \in (0 ..^N) \land x \in (0 \dots N)) \land \neg x \leq N - S) \to \|F\| \in ℕ_{0}$
85		elfzo0	$⊢ S \in (0 ..^N) \leftrightarrow (S \in ℕ_{0} \land N \in ℕ \land S < N)$
86		elfz2nn0	$⊢ x \in (0 \dots N) \leftrightarrow (x \in ℕ_{0} \land N \in ℕ_{0} \land x \leq N)$
87		nn0re	$⊢ S \in ℕ_{0} \to S \in ℝ$
88	87	3ad2ant1	$⊢ (S \in ℕ_{0} \land N \in ℕ \land S < N) \to S \in ℝ$
89		nn0re	$⊢ x \in ℕ_{0} \to x \in ℝ$
90	89	3ad2ant1	$⊢ (x \in ℕ_{0} \land N \in ℕ_{0} \land x \leq N) \to x \in ℝ$
91	88 90	anim12ci	$⊢ ((S \in ℕ_{0} \land N \in ℕ \land S < N) \land (x \in ℕ_{0} \land N \in ℕ_{0} \land x \leq N)) \to (x \in ℝ \land S \in ℝ)$
92		nnre	$⊢ N \in ℕ \to N \in ℝ$
93	92 92	jca	$⊢ N \in ℕ \to (N \in ℝ \land N \in ℝ)$
94	93	3ad2ant2	$⊢ (S \in ℕ_{0} \land N \in ℕ \land S < N) \to (N \in ℝ \land N \in ℝ)$
95	94	adantr	$⊢ ((S \in ℕ_{0} \land N \in ℕ \land S < N) \land (x \in ℕ_{0} \land N \in ℕ_{0} \land x \leq N)) \to (N \in ℝ \land N \in ℝ)$
96	91 95	jca	$⊢ ((S \in ℕ_{0} \land N \in ℕ \land S < N) \land (x \in ℕ_{0} \land N \in ℕ_{0} \land x \leq N)) \to ((x \in ℝ \land S \in ℝ) \land (N \in ℝ \land N \in ℝ))$
97		simpr3	$⊢ ((S \in ℕ_{0} \land N \in ℕ \land S < N) \land (x \in ℕ_{0} \land N \in ℕ_{0} \land x \leq N)) \to x \leq N$
98		ltle	$⊢ (S \in ℝ \land N \in ℝ) \to (S < N \to S \leq N)$
99	87 92 98	syl2an	$⊢ (S \in ℕ_{0} \land N \in ℕ) \to (S < N \to S \leq N)$
100	99	3impia	$⊢ (S \in ℕ_{0} \land N \in ℕ \land S < N) \to S \leq N$
101	100	adantr	$⊢ ((S \in ℕ_{0} \land N \in ℕ \land S < N) \land (x \in ℕ_{0} \land N \in ℕ_{0} \land x \leq N)) \to S \leq N$
102	96 97 101	jca32	$⊢ ((S \in ℕ_{0} \land N \in ℕ \land S < N) \land (x \in ℕ_{0} \land N \in ℕ_{0} \land x \leq N)) \to (((x \in ℝ \land S \in ℝ) \land (N \in ℝ \land N \in ℝ)) \land (x \leq N \land S \leq N))$
103	85 86 102	syl2anb	$⊢ (S \in (0 ..^N) \land x \in (0 \dots N)) \to (((x \in ℝ \land S \in ℝ) \land (N \in ℝ \land N \in ℝ)) \land (x \leq N \land S \leq N))$
104		le2add	$⊢ ((x \in ℝ \land S \in ℝ) \land (N \in ℝ \land N \in ℝ)) \to ((x \leq N \land S \leq N) \to x + S \leq N + N)$
105	104	imp	$⊢ (((x \in ℝ \land S \in ℝ) \land (N \in ℝ \land N \in ℝ)) \land (x \leq N \land S \leq N)) \to x + S \leq N + N$
106	103 105	syl	$⊢ (S \in (0 ..^N) \land x \in (0 \dots N)) \to x + S \leq N + N$
107	67 66 66	3jca	$⊢ (x \in ℤ \land (S \in ℤ \land N \in ℤ)) \to (x + S \in ℝ \land N \in ℝ \land N \in ℝ)$
108	107	ex	$⊢ x \in ℤ \to ((S \in ℤ \land N \in ℤ) \to (x + S \in ℝ \land N \in ℝ \land N \in ℝ))$
109	108 27	syl11	$⊢ (S \in ℤ \land N \in ℤ) \to (x \in (0 \dots N) \to (x + S \in ℝ \land N \in ℝ \land N \in ℝ))$
110	30 47 109	syl2anc	$⊢ S \in (0 ..^N) \to (x \in (0 \dots N) \to (x + S \in ℝ \land N \in ℝ \land N \in ℝ))$
111	110	imp	$⊢ (S \in (0 ..^N) \land x \in (0 \dots N)) \to (x + S \in ℝ \land N \in ℝ \land N \in ℝ)$
112		lesubadd	$⊢ (x + S \in ℝ \land N \in ℝ \land N \in ℝ) \to (x + S - N \leq N \leftrightarrow x + S \leq N + N)$
113	111 112	syl	$⊢ (S \in (0 ..^N) \land x \in (0 \dots N)) \to (x + S - N \leq N \leftrightarrow x + S \leq N + N)$
114	106 113	mpbird	$⊢ (S \in (0 ..^N) \land x \in (0 \dots N)) \to x + S - N \leq N$
115	114	adantr	$⊢ ((S \in (0 ..^N) \land x \in (0 \dots N)) \land \neg x \leq N - S) \to x + S - N \leq N$
116	115 4	breqtrdi	$⊢ ((S \in (0 ..^N) \land x \in (0 \dots N)) \land \neg x \leq N - S) \to x + S - N \leq \|F\|$
117	83 84 116	3jca	$⊢ ((S \in (0 ..^N) \land x \in (0 \dots N)) \land \neg x \leq N - S) \to (x + S - N \in ℕ_{0} \land \|F\| \in ℕ_{0} \land x + S - N \leq \|F\|)$
118	5 117	sylanl1	$⊢ ((φ \land x \in (0 \dots N)) \land \neg x \leq N - S) \to (x + S - N \in ℕ_{0} \land \|F\| \in ℕ_{0} \land x + S - N \leq \|F\|)$
119		elfz2nn0	$⊢ x + S - N \in (0 \dots \|F\|) \leftrightarrow (x + S - N \in ℕ_{0} \land \|F\| \in ℕ_{0} \land x + S - N \leq \|F\|)$
120	118 119	sylibr	$⊢ ((φ \land x \in (0 \dots N)) \land \neg x \leq N - S) \to x + S - N \in (0 \dots \|F\|)$
121	120	adantll	$⊢ ((P : (0 \dots \|F\|) ⟶ V \land (φ \land x \in (0 \dots N))) \land \neg x \leq N - S) \to x + S - N \in (0 \dots \|F\|)$
122	46 121	ffvelcdmd	$⊢ ((P : (0 \dots \|F\|) ⟶ V \land (φ \land x \in (0 \dots N))) \land \neg x \leq N - S) \to P (x + S - N) \in V$
123	45 122	ifclda	$⊢ (P : (0 \dots \|F\|) ⟶ V \land (φ \land x \in (0 \dots N))) \to if (x \leq N - S, P (x + S), P (x + S - N)) \in V$
124	123	exp32	$⊢ P : (0 \dots \|F\|) ⟶ V \to (φ \to (x \in (0 \dots N) \to if (x \leq N - S, P (x + S), P (x + S - N)) \in V))$
125	16 124	syl	$⊢ F Walks (G) P \to (φ \to (x \in (0 \dots N) \to if (x \leq N - S, P (x + S), P (x + S - N)) \in V))$
126	15 125	mpcom	$⊢ φ \to (x \in (0 \dots N) \to if (x \leq N - S, P (x + S), P (x + S - N)) \in V)$
127	126	imp	$⊢ (φ \land x \in (0 \dots N)) \to if (x \leq N - S, P (x + S), P (x + S - N)) \in V$
128	127 7	fmptd	$⊢ φ \to Q : (0 \dots N) ⟶ V$
129	1 2 3 4 5 6	crctcshlem2	$⊢ φ \to \|H\| = N$
130	129	oveq2d	$⊢ φ \to (0 \dots \|H\|) = (0 \dots N)$
131	130	feq2d	$⊢ φ \to (Q : (0 \dots \|H\|) ⟶ V \leftrightarrow Q : (0 \dots N) ⟶ V)$
132	128 131	mpbird	$⊢ φ \to Q : (0 \dots \|H\|) ⟶ V$
133	132	adantr	$⊢ (φ \land S \neq 0) \to Q : (0 \dots \|H\|) ⟶ V$
134	1 2	wlkprop	$⊢ F Walks (G) P \to (F \in Word dom I \land P : (0 \dots \|F\|) ⟶ V \land \forall i \in (0 ..^\|F\|) if- (P (i) = P (i + 1), I (F (i)) = \{P (i)\}, \{P (i), P (i + 1)\} \subseteq I (F (i))))$
135	3 8 134	3syl	$⊢ φ \to (F \in Word dom I \land P : (0 \dots \|F\|) ⟶ V \land \forall i \in (0 ..^\|F\|) if- (P (i) = P (i + 1), I (F (i)) = \{P (i)\}, \{P (i), P (i + 1)\} \subseteq I (F (i))))$
136	135	adantr	$⊢ (φ \land S \neq 0) \to (F \in Word dom I \land P : (0 \dots \|F\|) ⟶ V \land \forall i \in (0 ..^\|F\|) if- (P (i) = P (i + 1), I (F (i)) = \{P (i)\}, \{P (i), P (i + 1)\} \subseteq I (F (i))))$
137	4	eqcomi	$⊢ \|F\| = N$
138	137	oveq2i	$⊢ (0 ..^\|F\|) = (0 ..^N)$
139	138	raleqi	$⊢ \forall i \in (0 ..^\|F\|) if- (P (i) = P (i + 1), I (F (i)) = \{P (i)\}, \{P (i), P (i + 1)\} \subseteq I (F (i))) \leftrightarrow \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)))$
140		fzo1fzo0n0	$⊢ S \in (1 ..^N) \leftrightarrow (S \in (0 ..^N) \land S \neq 0)$
141	140	simplbi2	$⊢ S \in (0 ..^N) \to (S \neq 0 \to S \in (1 ..^N))$
142	5 141	syl	$⊢ φ \to (S \neq 0 \to S \in (1 ..^N))$
143	142	imp	$⊢ (φ \land S \neq 0) \to S \in (1 ..^N)$
144	143	ad2antlr	$⊢ (((F \in Word dom I \land P : (0 \dots \|F\|) ⟶ V) \land (φ \land S \neq 0)) \land \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 S \in (1 ..^N)$
145		simplll	$⊢ (((F \in Word dom I \land P : (0 \dots \|F\|) ⟶ V) \land (φ \land S \neq 0)) \land \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 F \in Word dom I$
146		wkslem1	$⊢ i = k \to (if- (P (i) = P (i + 1), I (F (i)) = \{P (i)\}, \{P (i), P (i + 1)\} \subseteq I (F (i))) \leftrightarrow if- (P (k) = P (k + 1), I (F (k)) = \{P (k)\}, \{P (k), P (k + 1)\} \subseteq I (F (k))))$
147	146	cbvralvw	$⊢ \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))) \leftrightarrow \forall k \in (0 ..^N) if- (P (k) = P (k + 1), I (F (k)) = \{P (k)\}, \{P (k), P (k + 1)\} \subseteq I (F (k)))$
148	147	biimpi	$⊢ \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 \forall k \in (0 ..^N) if- (P (k) = P (k + 1), I (F (k)) = \{P (k)\}, \{P (k), P (k + 1)\} \subseteq I (F (k)))$
149	148	adantl	$⊢ (((F \in Word dom I \land P : (0 \dots \|F\|) ⟶ V) \land (φ \land S \neq 0)) \land \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 \forall k \in (0 ..^N) if- (P (k) = P (k + 1), I (F (k)) = \{P (k)\}, \{P (k), P (k + 1)\} \subseteq I (F (k)))$
150		crctprop	$⊢ F Circuits (G) P \to (F Trails (G) P \land P (0) = P (\|F\|))$
151	137	fveq2i	$⊢ P (\|F\|) = P (N)$
152	151	eqeq2i	$⊢ P (0) = P (\|F\|) \leftrightarrow P (0) = P (N)$
153	152	biimpi	$⊢ P (0) = P (\|F\|) \to P (0) = P (N)$
154	153	eqcomd	$⊢ P (0) = P (\|F\|) \to P (N) = P (0)$
155	154	adantl	$⊢ (F Trails (G) P \land P (0) = P (\|F\|)) \to P (N) = P (0)$
156	3 150 155	3syl	$⊢ φ \to P (N) = P (0)$
157	156	ad2antrl	$⊢ ((F \in Word dom I \land P : (0 \dots \|F\|) ⟶ V) \land (φ \land S \neq 0)) \to P (N) = P (0)$
158	157	adantr	$⊢ (((F \in Word dom I \land P : (0 \dots \|F\|) ⟶ V) \land (φ \land S \neq 0)) \land \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 P (N) = P (0)$
159	144 7 6 4 145 149 158	crctcshwlkn0lem7	$⊢ (((F \in Word dom I \land P : (0 \dots \|F\|) ⟶ V) \land (φ \land S \neq 0)) \land \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 \forall j \in (0 ..^N) if- (Q (j) = Q (j + 1), I (H (j)) = \{Q (j)\}, \{Q (j), Q (j + 1)\} \subseteq I (H (j)))$
160	129	oveq2d	$⊢ φ \to (0 ..^\|H\|) = (0 ..^N)$
161	160	raleqdv	$⊢ φ \to (\forall j \in (0 ..^\|H\|) if- (Q (j) = Q (j + 1), I (H (j)) = \{Q (j)\}, \{Q (j), Q (j + 1)\} \subseteq I (H (j))) \leftrightarrow \forall j \in (0 ..^N) if- (Q (j) = Q (j + 1), I (H (j)) = \{Q (j)\}, \{Q (j), Q (j + 1)\} \subseteq I (H (j))))$
162	161	ad2antrl	$⊢ ((F \in Word dom I \land P : (0 \dots \|F\|) ⟶ V) \land (φ \land S \neq 0)) \to (\forall j \in (0 ..^\|H\|) if- (Q (j) = Q (j + 1), I (H (j)) = \{Q (j)\}, \{Q (j), Q (j + 1)\} \subseteq I (H (j))) \leftrightarrow \forall j \in (0 ..^N) if- (Q (j) = Q (j + 1), I (H (j)) = \{Q (j)\}, \{Q (j), Q (j + 1)\} \subseteq I (H (j))))$
163	162	adantr	$⊢ (((F \in Word dom I \land P : (0 \dots \|F\|) ⟶ V) \land (φ \land S \neq 0)) \land \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 (\forall j \in (0 ..^\|H\|) if- (Q (j) = Q (j + 1), I (H (j)) = \{Q (j)\}, \{Q (j), Q (j + 1)\} \subseteq I (H (j))) \leftrightarrow \forall j \in (0 ..^N) if- (Q (j) = Q (j + 1), I (H (j)) = \{Q (j)\}, \{Q (j), Q (j + 1)\} \subseteq I (H (j))))$
164	159 163	mpbird	$⊢ (((F \in Word dom I \land P : (0 \dots \|F\|) ⟶ V) \land (φ \land S \neq 0)) \land \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 \forall j \in (0 ..^\|H\|) if- (Q (j) = Q (j + 1), I (H (j)) = \{Q (j)\}, \{Q (j), Q (j + 1)\} \subseteq I (H (j)))$
165	164	ex	$⊢ ((F \in Word dom I \land P : (0 \dots \|F\|) ⟶ V) \land (φ \land S \neq 0)) \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 \forall j \in (0 ..^\|H\|) if- (Q (j) = Q (j + 1), I (H (j)) = \{Q (j)\}, \{Q (j), Q (j + 1)\} \subseteq I (H (j))))$
166	139 165	biimtrid	$⊢ ((F \in Word dom I \land P : (0 \dots \|F\|) ⟶ V) \land (φ \land S \neq 0)) \to (\forall i \in (0 ..^\|F\|) if- (P (i) = P (i + 1), I (F (i)) = \{P (i)\}, \{P (i), P (i + 1)\} \subseteq I (F (i))) \to \forall j \in (0 ..^\|H\|) if- (Q (j) = Q (j + 1), I (H (j)) = \{Q (j)\}, \{Q (j), Q (j + 1)\} \subseteq I (H (j))))$
167	166	ex	$⊢ (F \in Word dom I \land P : (0 \dots \|F\|) ⟶ V) \to ((φ \land S \neq 0) \to (\forall i \in (0 ..^\|F\|) if- (P (i) = P (i + 1), I (F (i)) = \{P (i)\}, \{P (i), P (i + 1)\} \subseteq I (F (i))) \to \forall j \in (0 ..^\|H\|) if- (Q (j) = Q (j + 1), I (H (j)) = \{Q (j)\}, \{Q (j), Q (j + 1)\} \subseteq I (H (j)))))$
168	167	com23	$⊢ (F \in Word dom I \land P : (0 \dots \|F\|) ⟶ V) \to (\forall i \in (0 ..^\|F\|) if- (P (i) = P (i + 1), I (F (i)) = \{P (i)\}, \{P (i), P (i + 1)\} \subseteq I (F (i))) \to ((φ \land S \neq 0) \to \forall j \in (0 ..^\|H\|) if- (Q (j) = Q (j + 1), I (H (j)) = \{Q (j)\}, \{Q (j), Q (j + 1)\} \subseteq I (H (j)))))$
169	168	3impia	$⊢ (F \in Word dom I \land P : (0 \dots \|F\|) ⟶ V \land \forall i \in (0 ..^\|F\|) if- (P (i) = P (i + 1), I (F (i)) = \{P (i)\}, \{P (i), P (i + 1)\} \subseteq I (F (i)))) \to ((φ \land S \neq 0) \to \forall j \in (0 ..^\|H\|) if- (Q (j) = Q (j + 1), I (H (j)) = \{Q (j)\}, \{Q (j), Q (j + 1)\} \subseteq I (H (j))))$
170	136 169	mpcom	$⊢ (φ \land S \neq 0) \to \forall j \in (0 ..^\|H\|) if- (Q (j) = Q (j + 1), I (H (j)) = \{Q (j)\}, \{Q (j), Q (j + 1)\} \subseteq I (H (j)))$
171	14 133 170	3jca	$⊢ (φ \land S \neq 0) \to (H \in Word dom I \land Q : (0 \dots \|H\|) ⟶ V \land \forall j \in (0 ..^\|H\|) if- (Q (j) = Q (j + 1), I (H (j)) = \{Q (j)\}, \{Q (j), Q (j + 1)\} \subseteq I (H (j))))$
172	1 2 3 4 5 6 7	crctcshlem3	$⊢ φ \to (G \in V \land H \in V \land Q \in V)$
173	172	adantr	$⊢ (φ \land S \neq 0) \to (G \in V \land H \in V \land Q \in V)$
174	1 2	iswlk	$⊢ (G \in V \land H \in V \land Q \in V) \to (H Walks (G) Q \leftrightarrow (H \in Word dom I \land Q : (0 \dots \|H\|) ⟶ V \land \forall j \in (0 ..^\|H\|) if- (Q (j) = Q (j + 1), I (H (j)) = \{Q (j)\}, \{Q (j), Q (j + 1)\} \subseteq I (H (j)))))$
175	173 174	syl	$⊢ (φ \land S \neq 0) \to (H Walks (G) Q \leftrightarrow (H \in Word dom I \land Q : (0 \dots \|H\|) ⟶ V \land \forall j \in (0 ..^\|H\|) if- (Q (j) = Q (j + 1), I (H (j)) = \{Q (j)\}, \{Q (j), Q (j + 1)\} \subseteq I (H (j)))))$
176	171 175	mpbird	$⊢ (φ \land S \neq 0) \to H Walks (G) Q$

Metamath Proof Explorer

Theorem crctcshwlkn0

Proof