crctcshwlkn0 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > crctcshwlkn0		Structured version Visualization version GIF version

Theorem crctcshwlkn0 29801

Description: Cyclically shifting the indices of a circuit ⟨𝐹, 𝑃⟩ results in a walk ⟨𝐻, 𝑄⟩. (Contributed by AV, 10-Mar-2021.)

**Hypotheses**
Ref	Expression
crctcsh.v	⊢ 𝑉 = (Vtx‘𝐺)
crctcsh.i	⊢ 𝐼 = (iEdg‘𝐺)
crctcsh.d	⊢ (𝜑 → 𝐹(Circuits‘𝐺)𝑃)
crctcsh.n	⊢ 𝑁 = (♯‘𝐹)
crctcsh.s	⊢ (𝜑 → 𝑆 ∈ (0..^𝑁))
crctcsh.h	⊢ 𝐻 = (𝐹 cyclShift 𝑆)
crctcsh.q	⊢ 𝑄 = (𝑥 ∈ (0...𝑁) ↦ if(𝑥 ≤ (𝑁 − 𝑆), (𝑃‘(𝑥 + 𝑆)), (𝑃‘((𝑥 + 𝑆) − 𝑁))))

**Assertion**
Ref	Expression
crctcshwlkn0	⊢ ((𝜑 ∧ 𝑆 ≠ 0) → 𝐻(Walks‘𝐺)𝑄)

Distinct variable groups: 𝑥,𝑁 𝑥,𝑃 𝑥,𝑆 𝜑,𝑥 𝑥,𝐹 𝑥,𝐼 𝑥,𝑉 Allowed substitution hints: 𝑄(𝑥) 𝐺(𝑥) 𝐻(𝑥)

Proof of Theorem crctcshwlkn0 Dummy variables 𝑖 𝑗 𝑘 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		crctcsh.h	. . . . 5 ⊢ 𝐻 = (𝐹 cyclShift 𝑆)
2		crctcsh.d	. . . . . 6 ⊢ (𝜑 → 𝐹(Circuits‘𝐺)𝑃)
3		crctiswlk 29776	. . . . . 6 ⊢ (𝐹(Circuits‘𝐺)𝑃 → 𝐹(Walks‘𝐺)𝑃)
4		crctcsh.i	. . . . . . 7 ⊢ 𝐼 = (iEdg‘𝐺)
5	4	wlkf 29595	. . . . . 6 ⊢ (𝐹(Walks‘𝐺)𝑃 → 𝐹 ∈ Word dom 𝐼)
6		cshwcl 14707	. . . . . 6 ⊢ (𝐹 ∈ Word dom 𝐼 → (𝐹 cyclShift 𝑆) ∈ Word dom 𝐼)
7	2, 3, 5, 6	4syl 19	. . . . 5 ⊢ (𝜑 → (𝐹 cyclShift 𝑆) ∈ Word dom 𝐼)
8	1, 7	eqeltrid 2837	. . . 4 ⊢ (𝜑 → 𝐻 ∈ Word dom 𝐼)
9	8	adantr 480	. . 3 ⊢ ((𝜑 ∧ 𝑆 ≠ 0) → 𝐻 ∈ Word dom 𝐼)
10	2, 3	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝐹(Walks‘𝐺)𝑃)
11		crctcsh.v	. . . . . . . . . 10 ⊢ 𝑉 = (Vtx‘𝐺)
12	11	wlkp 29597	. . . . . . . . 9 ⊢ (𝐹(Walks‘𝐺)𝑃 → 𝑃:(0...(♯‘𝐹))⟶𝑉)
13		simpll 766	. . . . . . . . . . . 12 ⊢ (((𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ (𝜑 ∧ 𝑥 ∈ (0...𝑁))) ∧ 𝑥 ≤ (𝑁 − 𝑆)) → 𝑃:(0...(♯‘𝐹))⟶𝑉)
14		crctcsh.s	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑆 ∈ (0..^𝑁))
15		elfznn0 13522	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ (0...𝑁) → 𝑥 ∈ ℕ₀)
16	15	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) → 𝑥 ∈ ℕ₀)
17		elfzonn0 13609	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑆 ∈ (0..^𝑁) → 𝑆 ∈ ℕ₀)
18	17	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) → 𝑆 ∈ ℕ₀)
19	16, 18	nn0addcld 12453	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) → (𝑥 + 𝑆) ∈ ℕ₀)
20	19	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) ∧ 𝑥 ≤ (𝑁 − 𝑆)) → (𝑥 + 𝑆) ∈ ℕ₀)
21		crctcsh.n	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑁 = (♯‘𝐹)
22		elfz3nn0 13523	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (0...𝑁) → 𝑁 ∈ ℕ₀)
23	21, 22	eqeltrrid 2838	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ (0...𝑁) → (♯‘𝐹) ∈ ℕ₀)
24	23	ad2antlr 727	. . . . . . . . . . . . . . . 16 ⊢ (((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) ∧ 𝑥 ≤ (𝑁 − 𝑆)) → (♯‘𝐹) ∈ ℕ₀)
25		elfzelz 13426	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ (0...𝑁) → 𝑥 ∈ ℤ)
26	25	zred 12583	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ (0...𝑁) → 𝑥 ∈ ℝ)
27	26	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) → 𝑥 ∈ ℝ)
28		elfzoelz 13561	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑆 ∈ (0..^𝑁) → 𝑆 ∈ ℤ)
29	28	zred 12583	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑆 ∈ (0..^𝑁) → 𝑆 ∈ ℝ)
30	29	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) → 𝑆 ∈ ℝ)
31		elfzel2 13424	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ (0...𝑁) → 𝑁 ∈ ℤ)
32	31	zred 12583	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ (0...𝑁) → 𝑁 ∈ ℝ)
33	32	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) → 𝑁 ∈ ℝ)
34		leaddsub 11600	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ ℝ ∧ 𝑆 ∈ ℝ ∧ 𝑁 ∈ ℝ) → ((𝑥 + 𝑆) ≤ 𝑁 ↔ 𝑥 ≤ (𝑁 − 𝑆)))
35	27, 30, 33, 34	syl3anc 1373	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) → ((𝑥 + 𝑆) ≤ 𝑁 ↔ 𝑥 ≤ (𝑁 − 𝑆)))
36	35	biimpar 477	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) ∧ 𝑥 ≤ (𝑁 − 𝑆)) → (𝑥 + 𝑆) ≤ 𝑁)
37	36, 21	breqtrdi 5134	. . . . . . . . . . . . . . . 16 ⊢ (((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) ∧ 𝑥 ≤ (𝑁 − 𝑆)) → (𝑥 + 𝑆) ≤ (♯‘𝐹))
38	20, 24, 37	3jca 1128	. . . . . . . . . . . . . . 15 ⊢ (((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) ∧ 𝑥 ≤ (𝑁 − 𝑆)) → ((𝑥 + 𝑆) ∈ ℕ₀ ∧ (♯‘𝐹) ∈ ℕ₀ ∧ (𝑥 + 𝑆) ≤ (♯‘𝐹)))
39	14, 38	sylanl1 680	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (0...𝑁)) ∧ 𝑥 ≤ (𝑁 − 𝑆)) → ((𝑥 + 𝑆) ∈ ℕ₀ ∧ (♯‘𝐹) ∈ ℕ₀ ∧ (𝑥 + 𝑆) ≤ (♯‘𝐹)))
40		elfz2nn0 13520	. . . . . . . . . . . . . 14 ⊢ ((𝑥 + 𝑆) ∈ (0...(♯‘𝐹)) ↔ ((𝑥 + 𝑆) ∈ ℕ₀ ∧ (♯‘𝐹) ∈ ℕ₀ ∧ (𝑥 + 𝑆) ≤ (♯‘𝐹)))
41	39, 40	sylibr 234	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (0...𝑁)) ∧ 𝑥 ≤ (𝑁 − 𝑆)) → (𝑥 + 𝑆) ∈ (0...(♯‘𝐹)))
42	41	adantll 714	. . . . . . . . . . . 12 ⊢ (((𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ (𝜑 ∧ 𝑥 ∈ (0...𝑁))) ∧ 𝑥 ≤ (𝑁 − 𝑆)) → (𝑥 + 𝑆) ∈ (0...(♯‘𝐹)))
43	13, 42	ffvelcdmd 7024	. . . . . . . . . . 11 ⊢ (((𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ (𝜑 ∧ 𝑥 ∈ (0...𝑁))) ∧ 𝑥 ≤ (𝑁 − 𝑆)) → (𝑃‘(𝑥 + 𝑆)) ∈ 𝑉)
44		simpll 766	. . . . . . . . . . . 12 ⊢ (((𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ (𝜑 ∧ 𝑥 ∈ (0...𝑁))) ∧ ¬ 𝑥 ≤ (𝑁 − 𝑆)) → 𝑃:(0...(♯‘𝐹))⟶𝑉)
45		elfzoel2 13560	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑆 ∈ (0..^𝑁) → 𝑁 ∈ ℤ)
46		zaddcl 12518	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑥 ∈ ℤ ∧ 𝑆 ∈ ℤ) → (𝑥 + 𝑆) ∈ ℤ)
47	46	adantrr 717	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑥 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → (𝑥 + 𝑆) ∈ ℤ)
48		simprr 772	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑥 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → 𝑁 ∈ ℤ)
49	47, 48	zsubcld 12588	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑥 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → ((𝑥 + 𝑆) − 𝑁) ∈ ℤ)
50	49	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑥 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ)) ∧ ¬ 𝑥 ≤ (𝑁 − 𝑆)) → ((𝑥 + 𝑆) − 𝑁) ∈ ℤ)
51		zsubcl 12520	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑁 ∈ ℤ ∧ 𝑆 ∈ ℤ) → (𝑁 − 𝑆) ∈ ℤ)
52	51	ancoms 458	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 − 𝑆) ∈ ℤ)
53	52	zred 12583	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 − 𝑆) ∈ ℝ)
54		zre 12479	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 ∈ ℤ → 𝑥 ∈ ℝ)
55		ltnle 11199	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑁 − 𝑆) ∈ ℝ ∧ 𝑥 ∈ ℝ) → ((𝑁 − 𝑆) < 𝑥 ↔ ¬ 𝑥 ≤ (𝑁 − 𝑆)))
56	53, 54, 55	syl2anr 597	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑥 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → ((𝑁 − 𝑆) < 𝑥 ↔ ¬ 𝑥 ≤ (𝑁 − 𝑆)))
57		zre 12479	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℝ)
58	57	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑁 ∈ ℝ)
59		zre 12479	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑆 ∈ ℤ → 𝑆 ∈ ℝ)
60	59	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑆 ∈ ℝ)
61	54	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑥 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → 𝑥 ∈ ℝ)
62		ltsubadd 11594	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑁 ∈ ℝ ∧ 𝑆 ∈ ℝ ∧ 𝑥 ∈ ℝ) → ((𝑁 − 𝑆) < 𝑥 ↔ 𝑁 < (𝑥 + 𝑆)))
63	58, 60, 61, 62	syl2an23an 1425	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑥 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → ((𝑁 − 𝑆) < 𝑥 ↔ 𝑁 < (𝑥 + 𝑆)))
64	58	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑥 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → 𝑁 ∈ ℝ)
65	47	zred 12583	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑥 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → (𝑥 + 𝑆) ∈ ℝ)
66	64, 65	posdifd 11711	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑥 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → (𝑁 < (𝑥 + 𝑆) ↔ 0 < ((𝑥 + 𝑆) − 𝑁)))
67		0red 11122	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑥 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → 0 ∈ ℝ)
68	49	zred 12583	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑥 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → ((𝑥 + 𝑆) − 𝑁) ∈ ℝ)
69		ltle 11208	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((0 ∈ ℝ ∧ ((𝑥 + 𝑆) − 𝑁) ∈ ℝ) → (0 < ((𝑥 + 𝑆) − 𝑁) → 0 ≤ ((𝑥 + 𝑆) − 𝑁)))
70	67, 68, 69	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑥 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → (0 < ((𝑥 + 𝑆) − 𝑁) → 0 ≤ ((𝑥 + 𝑆) − 𝑁)))
71	66, 70	sylbid 240	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑥 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → (𝑁 < (𝑥 + 𝑆) → 0 ≤ ((𝑥 + 𝑆) − 𝑁)))
72	63, 71	sylbid 240	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑥 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → ((𝑁 − 𝑆) < 𝑥 → 0 ≤ ((𝑥 + 𝑆) − 𝑁)))
73	56, 72	sylbird 260	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑥 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → (¬ 𝑥 ≤ (𝑁 − 𝑆) → 0 ≤ ((𝑥 + 𝑆) − 𝑁)))
74	73	imp 406	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑥 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ)) ∧ ¬ 𝑥 ≤ (𝑁 − 𝑆)) → 0 ≤ ((𝑥 + 𝑆) − 𝑁))
75	50, 74	jca 511	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑥 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ)) ∧ ¬ 𝑥 ≤ (𝑁 − 𝑆)) → (((𝑥 + 𝑆) − 𝑁) ∈ ℤ ∧ 0 ≤ ((𝑥 + 𝑆) − 𝑁)))
76	75	exp31 419	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ ℤ → ((𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (¬ 𝑥 ≤ (𝑁 − 𝑆) → (((𝑥 + 𝑆) − 𝑁) ∈ ℤ ∧ 0 ≤ ((𝑥 + 𝑆) − 𝑁)))))
77	76, 25	syl11 33	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑥 ∈ (0...𝑁) → (¬ 𝑥 ≤ (𝑁 − 𝑆) → (((𝑥 + 𝑆) − 𝑁) ∈ ℤ ∧ 0 ≤ ((𝑥 + 𝑆) − 𝑁)))))
78	28, 45, 77	syl2anc 584	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑆 ∈ (0..^𝑁) → (𝑥 ∈ (0...𝑁) → (¬ 𝑥 ≤ (𝑁 − 𝑆) → (((𝑥 + 𝑆) − 𝑁) ∈ ℤ ∧ 0 ≤ ((𝑥 + 𝑆) − 𝑁)))))
79	78	imp31 417	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) ∧ ¬ 𝑥 ≤ (𝑁 − 𝑆)) → (((𝑥 + 𝑆) − 𝑁) ∈ ℤ ∧ 0 ≤ ((𝑥 + 𝑆) − 𝑁)))
80		elnn0z 12488	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑥 + 𝑆) − 𝑁) ∈ ℕ₀ ↔ (((𝑥 + 𝑆) − 𝑁) ∈ ℤ ∧ 0 ≤ ((𝑥 + 𝑆) − 𝑁)))
81	79, 80	sylibr 234	. . . . . . . . . . . . . . . 16 ⊢ (((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) ∧ ¬ 𝑥 ≤ (𝑁 − 𝑆)) → ((𝑥 + 𝑆) − 𝑁) ∈ ℕ₀)
82	23	ad2antlr 727	. . . . . . . . . . . . . . . 16 ⊢ (((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) ∧ ¬ 𝑥 ≤ (𝑁 − 𝑆)) → (♯‘𝐹) ∈ ℕ₀)
83		elfzo0 13602	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑆 ∈ (0..^𝑁) ↔ (𝑆 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁))
84		elfz2nn0 13520	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ (0...𝑁) ↔ (𝑥 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀ ∧ 𝑥 ≤ 𝑁))
85		nn0re 12397	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑆 ∈ ℕ₀ → 𝑆 ∈ ℝ)
86	85	3ad2ant1 1133	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑆 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) → 𝑆 ∈ ℝ)
87		nn0re 12397	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 ∈ ℕ₀ → 𝑥 ∈ ℝ)
88	87	3ad2ant1 1133	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑥 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀ ∧ 𝑥 ≤ 𝑁) → 𝑥 ∈ ℝ)
89	86, 88	anim12ci 614	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑆 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) ∧ (𝑥 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀ ∧ 𝑥 ≤ 𝑁)) → (𝑥 ∈ ℝ ∧ 𝑆 ∈ ℝ))
90		nnre 12139	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℝ)
91	90, 90	jca 511	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑁 ∈ ℕ → (𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ))
92	91	3ad2ant2 1134	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑆 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) → (𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ))
93	92	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑆 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) ∧ (𝑥 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀ ∧ 𝑥 ≤ 𝑁)) → (𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ))
94	89, 93	jca 511	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑆 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) ∧ (𝑥 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀ ∧ 𝑥 ≤ 𝑁)) → ((𝑥 ∈ ℝ ∧ 𝑆 ∈ ℝ) ∧ (𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ)))
95		simpr3 1197	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑆 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) ∧ (𝑥 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀ ∧ 𝑥 ≤ 𝑁)) → 𝑥 ≤ 𝑁)
96		ltle 11208	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑆 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (𝑆 < 𝑁 → 𝑆 ≤ 𝑁))
97	85, 90, 96	syl2an 596	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑆 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ) → (𝑆 < 𝑁 → 𝑆 ≤ 𝑁))
98	97	3impia 1117	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑆 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) → 𝑆 ≤ 𝑁)
99	98	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑆 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) ∧ (𝑥 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀ ∧ 𝑥 ≤ 𝑁)) → 𝑆 ≤ 𝑁)
100	94, 95, 99	jca32 515	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑆 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) ∧ (𝑥 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀ ∧ 𝑥 ≤ 𝑁)) → (((𝑥 ∈ ℝ ∧ 𝑆 ∈ ℝ) ∧ (𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ)) ∧ (𝑥 ≤ 𝑁 ∧ 𝑆 ≤ 𝑁)))
101	83, 84, 100	syl2anb 598	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) → (((𝑥 ∈ ℝ ∧ 𝑆 ∈ ℝ) ∧ (𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ)) ∧ (𝑥 ≤ 𝑁 ∧ 𝑆 ≤ 𝑁)))
102		le2add 11606	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑥 ∈ ℝ ∧ 𝑆 ∈ ℝ) ∧ (𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ)) → ((𝑥 ≤ 𝑁 ∧ 𝑆 ≤ 𝑁) → (𝑥 + 𝑆) ≤ (𝑁 + 𝑁)))
103	102	imp 406	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑥 ∈ ℝ ∧ 𝑆 ∈ ℝ) ∧ (𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ)) ∧ (𝑥 ≤ 𝑁 ∧ 𝑆 ≤ 𝑁)) → (𝑥 + 𝑆) ≤ (𝑁 + 𝑁))
104	101, 103	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) → (𝑥 + 𝑆) ≤ (𝑁 + 𝑁))
105	65, 64, 64	3jca 1128	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑥 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → ((𝑥 + 𝑆) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ))
106	105	ex 412	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 ∈ ℤ → ((𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑥 + 𝑆) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ)))
107	106, 25	syl11 33	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑥 ∈ (0...𝑁) → ((𝑥 + 𝑆) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ)))
108	28, 45, 107	syl2anc 584	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑆 ∈ (0..^𝑁) → (𝑥 ∈ (0...𝑁) → ((𝑥 + 𝑆) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ)))
109	108	imp 406	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) → ((𝑥 + 𝑆) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ))
110		lesubadd 11596	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑥 + 𝑆) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (((𝑥 + 𝑆) − 𝑁) ≤ 𝑁 ↔ (𝑥 + 𝑆) ≤ (𝑁 + 𝑁)))
111	109, 110	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) → (((𝑥 + 𝑆) − 𝑁) ≤ 𝑁 ↔ (𝑥 + 𝑆) ≤ (𝑁 + 𝑁)))
112	104, 111	mpbird 257	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) → ((𝑥 + 𝑆) − 𝑁) ≤ 𝑁)
113	112	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) ∧ ¬ 𝑥 ≤ (𝑁 − 𝑆)) → ((𝑥 + 𝑆) − 𝑁) ≤ 𝑁)
114	113, 21	breqtrdi 5134	. . . . . . . . . . . . . . . 16 ⊢ (((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) ∧ ¬ 𝑥 ≤ (𝑁 − 𝑆)) → ((𝑥 + 𝑆) − 𝑁) ≤ (♯‘𝐹))
115	81, 82, 114	3jca 1128	. . . . . . . . . . . . . . 15 ⊢ (((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) ∧ ¬ 𝑥 ≤ (𝑁 − 𝑆)) → (((𝑥 + 𝑆) − 𝑁) ∈ ℕ₀ ∧ (♯‘𝐹) ∈ ℕ₀ ∧ ((𝑥 + 𝑆) − 𝑁) ≤ (♯‘𝐹)))
116	14, 115	sylanl1 680	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (0...𝑁)) ∧ ¬ 𝑥 ≤ (𝑁 − 𝑆)) → (((𝑥 + 𝑆) − 𝑁) ∈ ℕ₀ ∧ (♯‘𝐹) ∈ ℕ₀ ∧ ((𝑥 + 𝑆) − 𝑁) ≤ (♯‘𝐹)))
117		elfz2nn0 13520	. . . . . . . . . . . . . 14 ⊢ (((𝑥 + 𝑆) − 𝑁) ∈ (0...(♯‘𝐹)) ↔ (((𝑥 + 𝑆) − 𝑁) ∈ ℕ₀ ∧ (♯‘𝐹) ∈ ℕ₀ ∧ ((𝑥 + 𝑆) − 𝑁) ≤ (♯‘𝐹)))
118	116, 117	sylibr 234	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (0...𝑁)) ∧ ¬ 𝑥 ≤ (𝑁 − 𝑆)) → ((𝑥 + 𝑆) − 𝑁) ∈ (0...(♯‘𝐹)))
119	118	adantll 714	. . . . . . . . . . . 12 ⊢ (((𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ (𝜑 ∧ 𝑥 ∈ (0...𝑁))) ∧ ¬ 𝑥 ≤ (𝑁 − 𝑆)) → ((𝑥 + 𝑆) − 𝑁) ∈ (0...(♯‘𝐹)))
120	44, 119	ffvelcdmd 7024	. . . . . . . . . . 11 ⊢ (((𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ (𝜑 ∧ 𝑥 ∈ (0...𝑁))) ∧ ¬ 𝑥 ≤ (𝑁 − 𝑆)) → (𝑃‘((𝑥 + 𝑆) − 𝑁)) ∈ 𝑉)
121	43, 120	ifclda 4510	. . . . . . . . . 10 ⊢ ((𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ (𝜑 ∧ 𝑥 ∈ (0...𝑁))) → if(𝑥 ≤ (𝑁 − 𝑆), (𝑃‘(𝑥 + 𝑆)), (𝑃‘((𝑥 + 𝑆) − 𝑁))) ∈ 𝑉)
122	121	exp32 420	. . . . . . . . 9 ⊢ (𝑃:(0...(♯‘𝐹))⟶𝑉 → (𝜑 → (𝑥 ∈ (0...𝑁) → if(𝑥 ≤ (𝑁 − 𝑆), (𝑃‘(𝑥 + 𝑆)), (𝑃‘((𝑥 + 𝑆) − 𝑁))) ∈ 𝑉)))
123	12, 122	syl 17	. . . . . . . 8 ⊢ (𝐹(Walks‘𝐺)𝑃 → (𝜑 → (𝑥 ∈ (0...𝑁) → if(𝑥 ≤ (𝑁 − 𝑆), (𝑃‘(𝑥 + 𝑆)), (𝑃‘((𝑥 + 𝑆) − 𝑁))) ∈ 𝑉)))
124	10, 123	mpcom 38	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ (0...𝑁) → if(𝑥 ≤ (𝑁 − 𝑆), (𝑃‘(𝑥 + 𝑆)), (𝑃‘((𝑥 + 𝑆) − 𝑁))) ∈ 𝑉))
125	124	imp 406	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (0...𝑁)) → if(𝑥 ≤ (𝑁 − 𝑆), (𝑃‘(𝑥 + 𝑆)), (𝑃‘((𝑥 + 𝑆) − 𝑁))) ∈ 𝑉)
126		crctcsh.q	. . . . . 6 ⊢ 𝑄 = (𝑥 ∈ (0...𝑁) ↦ if(𝑥 ≤ (𝑁 − 𝑆), (𝑃‘(𝑥 + 𝑆)), (𝑃‘((𝑥 + 𝑆) − 𝑁))))
127	125, 126	fmptd 7053	. . . . 5 ⊢ (𝜑 → 𝑄:(0...𝑁)⟶𝑉)
128	11, 4, 2, 21, 14, 1	crctcshlem2 29798	. . . . . . 7 ⊢ (𝜑 → (♯‘𝐻) = 𝑁)
129	128	oveq2d 7368	. . . . . 6 ⊢ (𝜑 → (0...(♯‘𝐻)) = (0...𝑁))
130	129	feq2d 6640	. . . . 5 ⊢ (𝜑 → (𝑄:(0...(♯‘𝐻))⟶𝑉 ↔ 𝑄:(0...𝑁)⟶𝑉))
131	127, 130	mpbird 257	. . . 4 ⊢ (𝜑 → 𝑄:(0...(♯‘𝐻))⟶𝑉)
132	131	adantr 480	. . 3 ⊢ ((𝜑 ∧ 𝑆 ≠ 0) → 𝑄:(0...(♯‘𝐻))⟶𝑉)
133	11, 4	wlkprop 29592	. . . . . 6 ⊢ (𝐹(Walks‘𝐺)𝑃 → (𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(♯‘𝐹))if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖)))))
134	2, 3, 133	3syl 18	. . . . 5 ⊢ (𝜑 → (𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(♯‘𝐹))if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖)))))
135	134	adantr 480	. . . 4 ⊢ ((𝜑 ∧ 𝑆 ≠ 0) → (𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(♯‘𝐹))if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖)))))
136	21	eqcomi 2742	. . . . . . . . . 10 ⊢ (♯‘𝐹) = 𝑁
137	136	oveq2i 7363	. . . . . . . . 9 ⊢ (0..^(♯‘𝐹)) = (0..^𝑁)
138	137	raleqi 3291	. . . . . . . 8 ⊢ (∀𝑖 ∈ (0..^(♯‘𝐹))if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖))) ↔ ∀𝑖 ∈ (0..^𝑁)if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖))))
139		fzo1fzo0n0 13617	. . . . . . . . . . . . . . 15 ⊢ (𝑆 ∈ (1..^𝑁) ↔ (𝑆 ∈ (0..^𝑁) ∧ 𝑆 ≠ 0))
140	139	simplbi2 500	. . . . . . . . . . . . . 14 ⊢ (𝑆 ∈ (0..^𝑁) → (𝑆 ≠ 0 → 𝑆 ∈ (1..^𝑁)))
141	14, 140	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑆 ≠ 0 → 𝑆 ∈ (1..^𝑁)))
142	141	imp 406	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑆 ≠ 0) → 𝑆 ∈ (1..^𝑁))
143	142	ad2antlr 727	. . . . . . . . . . 11 ⊢ ((((𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉) ∧ (𝜑 ∧ 𝑆 ≠ 0)) ∧ ∀𝑖 ∈ (0..^𝑁)if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖)))) → 𝑆 ∈ (1..^𝑁))
144		simplll 774	. . . . . . . . . . 11 ⊢ ((((𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉) ∧ (𝜑 ∧ 𝑆 ≠ 0)) ∧ ∀𝑖 ∈ (0..^𝑁)if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖)))) → 𝐹 ∈ Word dom 𝐼)
145		wkslem1 29588	. . . . . . . . . . . . . 14 ⊢ (𝑖 = 𝑘 → (if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖))) ↔ if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘)))))
146	145	cbvralvw 3211	. . . . . . . . . . . . 13 ⊢ (∀𝑖 ∈ (0..^𝑁)if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖))) ↔ ∀𝑘 ∈ (0..^𝑁)if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘))))
147	146	biimpi 216	. . . . . . . . . . . 12 ⊢ (∀𝑖 ∈ (0..^𝑁)if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖))) → ∀𝑘 ∈ (0..^𝑁)if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘))))
148	147	adantl 481	. . . . . . . . . . 11 ⊢ ((((𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉) ∧ (𝜑 ∧ 𝑆 ≠ 0)) ∧ ∀𝑖 ∈ (0..^𝑁)if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖)))) → ∀𝑘 ∈ (0..^𝑁)if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘))))
149		crctprop 29772	. . . . . . . . . . . . . 14 ⊢ (𝐹(Circuits‘𝐺)𝑃 → (𝐹(Trails‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))))
150	136	fveq2i 6831	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑃‘(♯‘𝐹)) = (𝑃‘𝑁)
151	150	eqeq2i 2746	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑃‘0) = (𝑃‘(♯‘𝐹)) ↔ (𝑃‘0) = (𝑃‘𝑁))
152	151	biimpi 216	. . . . . . . . . . . . . . . 16 ⊢ ((𝑃‘0) = (𝑃‘(♯‘𝐹)) → (𝑃‘0) = (𝑃‘𝑁))
153	152	eqcomd 2739	. . . . . . . . . . . . . . 15 ⊢ ((𝑃‘0) = (𝑃‘(♯‘𝐹)) → (𝑃‘𝑁) = (𝑃‘0))
154	153	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((𝐹(Trails‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) → (𝑃‘𝑁) = (𝑃‘0))
155	2, 149, 154	3syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑃‘𝑁) = (𝑃‘0))
156	155	ad2antrl 728	. . . . . . . . . . . 12 ⊢ (((𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉) ∧ (𝜑 ∧ 𝑆 ≠ 0)) → (𝑃‘𝑁) = (𝑃‘0))
157	156	adantr 480	. . . . . . . . . . 11 ⊢ ((((𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉) ∧ (𝜑 ∧ 𝑆 ≠ 0)) ∧ ∀𝑖 ∈ (0..^𝑁)if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖)))) → (𝑃‘𝑁) = (𝑃‘0))
158	143, 126, 1, 21, 144, 148, 157	crctcshwlkn0lem7 29796	. . . . . . . . . 10 ⊢ ((((𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉) ∧ (𝜑 ∧ 𝑆 ≠ 0)) ∧ ∀𝑖 ∈ (0..^𝑁)if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖)))) → ∀𝑗 ∈ (0..^𝑁)if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗))))
159	128	oveq2d 7368	. . . . . . . . . . . . 13 ⊢ (𝜑 → (0..^(♯‘𝐻)) = (0..^𝑁))
160	159	raleqdv 3293	. . . . . . . . . . . 12 ⊢ (𝜑 → (∀𝑗 ∈ (0..^(♯‘𝐻))if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗))) ↔ ∀𝑗 ∈ (0..^𝑁)if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗)))))
161	160	ad2antrl 728	. . . . . . . . . . 11 ⊢ (((𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉) ∧ (𝜑 ∧ 𝑆 ≠ 0)) → (∀𝑗 ∈ (0..^(♯‘𝐻))if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗))) ↔ ∀𝑗 ∈ (0..^𝑁)if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗)))))
162	161	adantr 480	. . . . . . . . . 10 ⊢ ((((𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉) ∧ (𝜑 ∧ 𝑆 ≠ 0)) ∧ ∀𝑖 ∈ (0..^𝑁)if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖)))) → (∀𝑗 ∈ (0..^(♯‘𝐻))if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗))) ↔ ∀𝑗 ∈ (0..^𝑁)if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗)))))
163	158, 162	mpbird 257	. . . . . . . . 9 ⊢ ((((𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉) ∧ (𝜑 ∧ 𝑆 ≠ 0)) ∧ ∀𝑖 ∈ (0..^𝑁)if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖)))) → ∀𝑗 ∈ (0..^(♯‘𝐻))if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗))))
164	163	ex 412	. . . . . . . 8 ⊢ (((𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉) ∧ (𝜑 ∧ 𝑆 ≠ 0)) → (∀𝑖 ∈ (0..^𝑁)if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖))) → ∀𝑗 ∈ (0..^(♯‘𝐻))if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗)))))
165	138, 164	biimtrid 242	. . . . . . 7 ⊢ (((𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉) ∧ (𝜑 ∧ 𝑆 ≠ 0)) → (∀𝑖 ∈ (0..^(♯‘𝐹))if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖))) → ∀𝑗 ∈ (0..^(♯‘𝐻))if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗)))))
166	165	ex 412	. . . . . 6 ⊢ ((𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉) → ((𝜑 ∧ 𝑆 ≠ 0) → (∀𝑖 ∈ (0..^(♯‘𝐹))if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖))) → ∀𝑗 ∈ (0..^(♯‘𝐻))if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗))))))
167	166	com23 86	. . . . 5 ⊢ ((𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉) → (∀𝑖 ∈ (0..^(♯‘𝐹))if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖))) → ((𝜑 ∧ 𝑆 ≠ 0) → ∀𝑗 ∈ (0..^(♯‘𝐻))if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗))))))
168	167	3impia 1117	. . . 4 ⊢ ((𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(♯‘𝐹))if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖)))) → ((𝜑 ∧ 𝑆 ≠ 0) → ∀𝑗 ∈ (0..^(♯‘𝐻))if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗)))))
169	135, 168	mpcom 38	. . 3 ⊢ ((𝜑 ∧ 𝑆 ≠ 0) → ∀𝑗 ∈ (0..^(♯‘𝐻))if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗))))
170	9, 132, 169	3jca 1128	. 2 ⊢ ((𝜑 ∧ 𝑆 ≠ 0) → (𝐻 ∈ Word dom 𝐼 ∧ 𝑄:(0...(♯‘𝐻))⟶𝑉 ∧ ∀𝑗 ∈ (0..^(♯‘𝐻))if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗)))))
171	11, 4, 2, 21, 14, 1, 126	crctcshlem3 29799	. . . 4 ⊢ (𝜑 → (𝐺 ∈ V ∧ 𝐻 ∈ V ∧ 𝑄 ∈ V))
172	171	adantr 480	. . 3 ⊢ ((𝜑 ∧ 𝑆 ≠ 0) → (𝐺 ∈ V ∧ 𝐻 ∈ V ∧ 𝑄 ∈ V))
173	11, 4	iswlk 29591	. . 3 ⊢ ((𝐺 ∈ V ∧ 𝐻 ∈ V ∧ 𝑄 ∈ V) → (𝐻(Walks‘𝐺)𝑄 ↔ (𝐻 ∈ Word dom 𝐼 ∧ 𝑄:(0...(♯‘𝐻))⟶𝑉 ∧ ∀𝑗 ∈ (0..^(♯‘𝐻))if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗))))))
174	172, 173	syl 17	. 2 ⊢ ((𝜑 ∧ 𝑆 ≠ 0) → (𝐻(Walks‘𝐺)𝑄 ↔ (𝐻 ∈ Word dom 𝐼 ∧ 𝑄:(0...(♯‘𝐻))⟶𝑉 ∧ ∀𝑗 ∈ (0..^(♯‘𝐻))if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗))))))
175	170, 174	mpbird 257	1 ⊢ ((𝜑 ∧ 𝑆 ≠ 0) → 𝐻(Walks‘𝐺)𝑄)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 if-wif 1062 ∧ w3a 1086 = wceq 1541 ∈ wcel 2113 ≠ wne 2929 ∀wral 3048 Vcvv 3437 ⊆ wss 3898 ifcif 4474 {csn 4575 {cpr 4577 class class class wbr 5093 ↦ cmpt 5174 dom cdm 5619 ⟶wf 6482 ‘cfv 6486 (class class class)co 7352 ℝcr 11012 0cc0 11013 1c1 11014 + caddc 11016 < clt 11153 ≤ cle 11154 − cmin 11351 ℕcn 12132 ℕ₀cn0 12388 ℤcz 12475 ...cfz 13409 ..^cfzo 13556 ♯chash 14239 Word cword 14422 cyclShift ccsh 14697 Vtxcvtx 28976 iEdgciedg 28977 Walkscwlks 29577 Trailsctrls 29669 Circuitsccrcts 29764

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2115 ax-9 2123 ax-10 2146 ax-11 2162 ax-12 2182 ax-ext 2705 ax-rep 5219 ax-sep 5236 ax-nul 5246 ax-pow 5305 ax-pr 5372 ax-un 7674 ax-cnex 11069 ax-resscn 11070 ax-1cn 11071 ax-icn 11072 ax-addcl 11073 ax-addrcl 11074 ax-mulcl 11075 ax-mulrcl 11076 ax-mulcom 11077 ax-addass 11078 ax-mulass 11079 ax-distr 11080 ax-i2m1 11081 ax-1ne0 11082 ax-1rid 11083 ax-rnegex 11084 ax-rrecex 11085 ax-cnre 11086 ax-pre-lttri 11087 ax-pre-lttrn 11088 ax-pre-ltadd 11089 ax-pre-mulgt0 11090 ax-pre-sup 11091

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-ifp 1063 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2537 df-eu 2566 df-clab 2712 df-cleq 2725 df-clel 2808 df-nfc 2882 df-ne 2930 df-nel 3034 df-ral 3049 df-rex 3058 df-rmo 3347 df-reu 3348 df-rab 3397 df-v 3439 df-sbc 3738 df-csb 3847 df-dif 3901 df-un 3903 df-in 3905 df-ss 3915 df-pss 3918 df-nul 4283 df-if 4475 df-pw 4551 df-sn 4576 df-pr 4578 df-op 4582 df-uni 4859 df-int 4898 df-iun 4943 df-br 5094 df-opab 5156 df-mpt 5175 df-tr 5201 df-id 5514 df-eprel 5519 df-po 5527 df-so 5528 df-fr 5572 df-we 5574 df-xp 5625 df-rel 5626 df-cnv 5627 df-co 5628 df-dm 5629 df-rn 5630 df-res 5631 df-ima 5632 df-pred 6253 df-ord 6314 df-on 6315 df-lim 6316 df-suc 6317 df-iota 6442 df-fun 6488 df-fn 6489 df-f 6490 df-f1 6491 df-fo 6492 df-f1o 6493 df-fv 6494 df-riota 7309 df-ov 7355 df-oprab 7356 df-mpo 7357 df-om 7803 df-1st 7927 df-2nd 7928 df-frecs 8217 df-wrecs 8248 df-recs 8297 df-rdg 8335 df-1o 8391 df-er 8628 df-map 8758 df-en 8876 df-dom 8877 df-sdom 8878 df-fin 8879 df-sup 9333 df-inf 9334 df-card 9839 df-pnf 11155 df-mnf 11156 df-xr 11157 df-ltxr 11158 df-le 11159 df-sub 11353 df-neg 11354 df-div 11782 df-nn 12133 df-2 12195 df-n0 12389 df-z 12476 df-uz 12739 df-rp 12893 df-fz 13410 df-fzo 13557 df-fl 13698 df-mod 13776 df-hash 14240 df-word 14423 df-concat 14480 df-substr 14551 df-pfx 14581 df-csh 14698 df-wlks 29580 df-trls 29671 df-crcts 29766

This theorem is referenced by: crctcshwlk 29802

W3C validator