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

Metamath Proof Explorer

Theorem crctcshwlkn0

Proof