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 27759

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	. . . . . . 7 ⊢ (𝜑 → 𝐹(Circuits‘𝐺)𝑃)
3		crctiswlk 27737	. . . . . . 7 ⊢ (𝐹(Circuits‘𝐺)𝑃 → 𝐹(Walks‘𝐺)𝑃)
4		crctcsh.i	. . . . . . . 8 ⊢ 𝐼 = (iEdg‘𝐺)
5	4	wlkf 27556	. . . . . . 7 ⊢ (𝐹(Walks‘𝐺)𝑃 → 𝐹 ∈ Word dom 𝐼)
6	2, 3, 5	3syl 18	. . . . . 6 ⊢ (𝜑 → 𝐹 ∈ Word dom 𝐼)
7		cshwcl 14249	. . . . . 6 ⊢ (𝐹 ∈ Word dom 𝐼 → (𝐹 cyclShift 𝑆) ∈ Word dom 𝐼)
8	6, 7	syl 17	. . . . 5 ⊢ (𝜑 → (𝐹 cyclShift 𝑆) ∈ Word dom 𝐼)
9	1, 8	eqeltrid 2837	. . . 4 ⊢ (𝜑 → 𝐻 ∈ Word dom 𝐼)
10	9	adantr 484	. . 3 ⊢ ((𝜑 ∧ 𝑆 ≠ 0) → 𝐻 ∈ Word dom 𝐼)
11	2, 3	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝐹(Walks‘𝐺)𝑃)
12		crctcsh.v	. . . . . . . . . 10 ⊢ 𝑉 = (Vtx‘𝐺)
13	12	wlkp 27558	. . . . . . . . 9 ⊢ (𝐹(Walks‘𝐺)𝑃 → 𝑃:(0...(♯‘𝐹))⟶𝑉)
14		simpll 767	. . . . . . . . . . . 12 ⊢ (((𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ (𝜑 ∧ 𝑥 ∈ (0...𝑁))) ∧ 𝑥 ≤ (𝑁 − 𝑆)) → 𝑃:(0...(♯‘𝐹))⟶𝑉)
15		crctcsh.s	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑆 ∈ (0..^𝑁))
16		elfznn0 13091	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ (0...𝑁) → 𝑥 ∈ ℕ₀)
17	16	adantl 485	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) → 𝑥 ∈ ℕ₀)
18		elfzonn0 13173	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑆 ∈ (0..^𝑁) → 𝑆 ∈ ℕ₀)
19	18	adantr 484	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) → 𝑆 ∈ ℕ₀)
20	17, 19	nn0addcld 12040	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) → (𝑥 + 𝑆) ∈ ℕ₀)
21	20	adantr 484	. . . . . . . . . . . . . . . 16 ⊢ (((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) ∧ 𝑥 ≤ (𝑁 − 𝑆)) → (𝑥 + 𝑆) ∈ ℕ₀)
22		crctcsh.n	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑁 = (♯‘𝐹)
23		elfz3nn0 13092	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (0...𝑁) → 𝑁 ∈ ℕ₀)
24	22, 23	eqeltrrid 2838	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ (0...𝑁) → (♯‘𝐹) ∈ ℕ₀)
25	24	ad2antlr 727	. . . . . . . . . . . . . . . 16 ⊢ (((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) ∧ 𝑥 ≤ (𝑁 − 𝑆)) → (♯‘𝐹) ∈ ℕ₀)
26		elfzelz 12998	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ (0...𝑁) → 𝑥 ∈ ℤ)
27	26	zred 12168	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ (0...𝑁) → 𝑥 ∈ ℝ)
28	27	adantl 485	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) → 𝑥 ∈ ℝ)
29		elfzoelz 13129	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑆 ∈ (0..^𝑁) → 𝑆 ∈ ℤ)
30	29	zred 12168	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑆 ∈ (0..^𝑁) → 𝑆 ∈ ℝ)
31	30	adantr 484	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) → 𝑆 ∈ ℝ)
32		elfzel2 12996	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ (0...𝑁) → 𝑁 ∈ ℤ)
33	32	zred 12168	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ (0...𝑁) → 𝑁 ∈ ℝ)
34	33	adantl 485	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) → 𝑁 ∈ ℝ)
35		leaddsub 11194	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ ℝ ∧ 𝑆 ∈ ℝ ∧ 𝑁 ∈ ℝ) → ((𝑥 + 𝑆) ≤ 𝑁 ↔ 𝑥 ≤ (𝑁 − 𝑆)))
36	28, 31, 34, 35	syl3anc 1372	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) → ((𝑥 + 𝑆) ≤ 𝑁 ↔ 𝑥 ≤ (𝑁 − 𝑆)))
37	36	biimpar 481	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) ∧ 𝑥 ≤ (𝑁 − 𝑆)) → (𝑥 + 𝑆) ≤ 𝑁)
38	37, 22	breqtrdi 5071	. . . . . . . . . . . . . . . 16 ⊢ (((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) ∧ 𝑥 ≤ (𝑁 − 𝑆)) → (𝑥 + 𝑆) ≤ (♯‘𝐹))
39	21, 25, 38	3jca 1129	. . . . . . . . . . . . . . 15 ⊢ (((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) ∧ 𝑥 ≤ (𝑁 − 𝑆)) → ((𝑥 + 𝑆) ∈ ℕ₀ ∧ (♯‘𝐹) ∈ ℕ₀ ∧ (𝑥 + 𝑆) ≤ (♯‘𝐹)))
40	15, 39	sylanl1 680	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (0...𝑁)) ∧ 𝑥 ≤ (𝑁 − 𝑆)) → ((𝑥 + 𝑆) ∈ ℕ₀ ∧ (♯‘𝐹) ∈ ℕ₀ ∧ (𝑥 + 𝑆) ≤ (♯‘𝐹)))
41		elfz2nn0 13089	. . . . . . . . . . . . . 14 ⊢ ((𝑥 + 𝑆) ∈ (0...(♯‘𝐹)) ↔ ((𝑥 + 𝑆) ∈ ℕ₀ ∧ (♯‘𝐹) ∈ ℕ₀ ∧ (𝑥 + 𝑆) ≤ (♯‘𝐹)))
42	40, 41	sylibr 237	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (0...𝑁)) ∧ 𝑥 ≤ (𝑁 − 𝑆)) → (𝑥 + 𝑆) ∈ (0...(♯‘𝐹)))
43	42	adantll 714	. . . . . . . . . . . 12 ⊢ (((𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ (𝜑 ∧ 𝑥 ∈ (0...𝑁))) ∧ 𝑥 ≤ (𝑁 − 𝑆)) → (𝑥 + 𝑆) ∈ (0...(♯‘𝐹)))
44	14, 43	ffvelrnd 6862	. . . . . . . . . . 11 ⊢ (((𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ (𝜑 ∧ 𝑥 ∈ (0...𝑁))) ∧ 𝑥 ≤ (𝑁 − 𝑆)) → (𝑃‘(𝑥 + 𝑆)) ∈ 𝑉)
45		simpll 767	. . . . . . . . . . . 12 ⊢ (((𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ (𝜑 ∧ 𝑥 ∈ (0...𝑁))) ∧ ¬ 𝑥 ≤ (𝑁 − 𝑆)) → 𝑃:(0...(♯‘𝐹))⟶𝑉)
46		elfzoel2 13128	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑆 ∈ (0..^𝑁) → 𝑁 ∈ ℤ)
47		zaddcl 12103	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑥 ∈ ℤ ∧ 𝑆 ∈ ℤ) → (𝑥 + 𝑆) ∈ ℤ)
48	47	adantrr 717	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑥 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → (𝑥 + 𝑆) ∈ ℤ)
49		simprr 773	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑥 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → 𝑁 ∈ ℤ)
50	48, 49	zsubcld 12173	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑥 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → ((𝑥 + 𝑆) − 𝑁) ∈ ℤ)
51	50	adantr 484	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑥 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ)) ∧ ¬ 𝑥 ≤ (𝑁 − 𝑆)) → ((𝑥 + 𝑆) − 𝑁) ∈ ℤ)
52		zsubcl 12105	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑁 ∈ ℤ ∧ 𝑆 ∈ ℤ) → (𝑁 − 𝑆) ∈ ℤ)
53	52	ancoms 462	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 − 𝑆) ∈ ℤ)
54	53	zred 12168	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 − 𝑆) ∈ ℝ)
55		zre 12066	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 ∈ ℤ → 𝑥 ∈ ℝ)
56		ltnle 10798	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑁 − 𝑆) ∈ ℝ ∧ 𝑥 ∈ ℝ) → ((𝑁 − 𝑆) < 𝑥 ↔ ¬ 𝑥 ≤ (𝑁 − 𝑆)))
57	54, 55, 56	syl2anr 600	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑥 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → ((𝑁 − 𝑆) < 𝑥 ↔ ¬ 𝑥 ≤ (𝑁 − 𝑆)))
58		zre 12066	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℝ)
59	58	adantl 485	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑁 ∈ ℝ)
60		zre 12066	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑆 ∈ ℤ → 𝑆 ∈ ℝ)
61	60	adantr 484	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑆 ∈ ℝ)
62	55	adantr 484	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑥 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → 𝑥 ∈ ℝ)
63		ltsubadd 11188	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑁 ∈ ℝ ∧ 𝑆 ∈ ℝ ∧ 𝑥 ∈ ℝ) → ((𝑁 − 𝑆) < 𝑥 ↔ 𝑁 < (𝑥 + 𝑆)))
64	59, 61, 62, 63	syl2an23an 1424	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑥 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → ((𝑁 − 𝑆) < 𝑥 ↔ 𝑁 < (𝑥 + 𝑆)))
65	59	adantl 485	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑥 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → 𝑁 ∈ ℝ)
66	48	zred 12168	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑥 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → (𝑥 + 𝑆) ∈ ℝ)
67	65, 66	posdifd 11305	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑥 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → (𝑁 < (𝑥 + 𝑆) ↔ 0 < ((𝑥 + 𝑆) − 𝑁)))
68		0red 10722	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑥 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → 0 ∈ ℝ)
69	50	zred 12168	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑥 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → ((𝑥 + 𝑆) − 𝑁) ∈ ℝ)
70		ltle 10807	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((0 ∈ ℝ ∧ ((𝑥 + 𝑆) − 𝑁) ∈ ℝ) → (0 < ((𝑥 + 𝑆) − 𝑁) → 0 ≤ ((𝑥 + 𝑆) − 𝑁)))
71	68, 69, 70	syl2anc 587	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑥 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → (0 < ((𝑥 + 𝑆) − 𝑁) → 0 ≤ ((𝑥 + 𝑆) − 𝑁)))
72	67, 71	sylbid 243	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑥 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → (𝑁 < (𝑥 + 𝑆) → 0 ≤ ((𝑥 + 𝑆) − 𝑁)))
73	64, 72	sylbid 243	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑥 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → ((𝑁 − 𝑆) < 𝑥 → 0 ≤ ((𝑥 + 𝑆) − 𝑁)))
74	57, 73	sylbird 263	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑥 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → (¬ 𝑥 ≤ (𝑁 − 𝑆) → 0 ≤ ((𝑥 + 𝑆) − 𝑁)))
75	74	imp 410	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑥 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ)) ∧ ¬ 𝑥 ≤ (𝑁 − 𝑆)) → 0 ≤ ((𝑥 + 𝑆) − 𝑁))
76	51, 75	jca 515	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑥 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ)) ∧ ¬ 𝑥 ≤ (𝑁 − 𝑆)) → (((𝑥 + 𝑆) − 𝑁) ∈ ℤ ∧ 0 ≤ ((𝑥 + 𝑆) − 𝑁)))
77	76	exp31 423	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ ℤ → ((𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (¬ 𝑥 ≤ (𝑁 − 𝑆) → (((𝑥 + 𝑆) − 𝑁) ∈ ℤ ∧ 0 ≤ ((𝑥 + 𝑆) − 𝑁)))))
78	77, 26	syl11 33	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑥 ∈ (0...𝑁) → (¬ 𝑥 ≤ (𝑁 − 𝑆) → (((𝑥 + 𝑆) − 𝑁) ∈ ℤ ∧ 0 ≤ ((𝑥 + 𝑆) − 𝑁)))))
79	29, 46, 78	syl2anc 587	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑆 ∈ (0..^𝑁) → (𝑥 ∈ (0...𝑁) → (¬ 𝑥 ≤ (𝑁 − 𝑆) → (((𝑥 + 𝑆) − 𝑁) ∈ ℤ ∧ 0 ≤ ((𝑥 + 𝑆) − 𝑁)))))
80	79	imp31 421	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) ∧ ¬ 𝑥 ≤ (𝑁 − 𝑆)) → (((𝑥 + 𝑆) − 𝑁) ∈ ℤ ∧ 0 ≤ ((𝑥 + 𝑆) − 𝑁)))
81		elnn0z 12075	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑥 + 𝑆) − 𝑁) ∈ ℕ₀ ↔ (((𝑥 + 𝑆) − 𝑁) ∈ ℤ ∧ 0 ≤ ((𝑥 + 𝑆) − 𝑁)))
82	80, 81	sylibr 237	. . . . . . . . . . . . . . . 16 ⊢ (((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) ∧ ¬ 𝑥 ≤ (𝑁 − 𝑆)) → ((𝑥 + 𝑆) − 𝑁) ∈ ℕ₀)
83	24	ad2antlr 727	. . . . . . . . . . . . . . . 16 ⊢ (((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) ∧ ¬ 𝑥 ≤ (𝑁 − 𝑆)) → (♯‘𝐹) ∈ ℕ₀)
84		elfzo0 13169	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑆 ∈ (0..^𝑁) ↔ (𝑆 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁))
85		elfz2nn0 13089	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ (0...𝑁) ↔ (𝑥 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀ ∧ 𝑥 ≤ 𝑁))
86		nn0re 11985	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑆 ∈ ℕ₀ → 𝑆 ∈ ℝ)
87	86	3ad2ant1 1134	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑆 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) → 𝑆 ∈ ℝ)
88		nn0re 11985	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 ∈ ℕ₀ → 𝑥 ∈ ℝ)
89	88	3ad2ant1 1134	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑥 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀ ∧ 𝑥 ≤ 𝑁) → 𝑥 ∈ ℝ)
90	87, 89	anim12ci 617	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑆 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) ∧ (𝑥 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀ ∧ 𝑥 ≤ 𝑁)) → (𝑥 ∈ ℝ ∧ 𝑆 ∈ ℝ))
91		nnre 11723	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℝ)
92	91, 91	jca 515	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑁 ∈ ℕ → (𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ))
93	92	3ad2ant2 1135	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑆 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) → (𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ))
94	93	adantr 484	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑆 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) ∧ (𝑥 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀ ∧ 𝑥 ≤ 𝑁)) → (𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ))
95	90, 94	jca 515	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑆 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) ∧ (𝑥 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀ ∧ 𝑥 ≤ 𝑁)) → ((𝑥 ∈ ℝ ∧ 𝑆 ∈ ℝ) ∧ (𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ)))
96		simpr3 1197	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑆 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) ∧ (𝑥 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀ ∧ 𝑥 ≤ 𝑁)) → 𝑥 ≤ 𝑁)
97		ltle 10807	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑆 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (𝑆 < 𝑁 → 𝑆 ≤ 𝑁))
98	86, 91, 97	syl2an 599	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑆 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ) → (𝑆 < 𝑁 → 𝑆 ≤ 𝑁))
99	98	3impia 1118	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑆 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) → 𝑆 ≤ 𝑁)
100	99	adantr 484	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑆 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) ∧ (𝑥 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀ ∧ 𝑥 ≤ 𝑁)) → 𝑆 ≤ 𝑁)
101	95, 96, 100	jca32 519	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑆 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) ∧ (𝑥 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀ ∧ 𝑥 ≤ 𝑁)) → (((𝑥 ∈ ℝ ∧ 𝑆 ∈ ℝ) ∧ (𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ)) ∧ (𝑥 ≤ 𝑁 ∧ 𝑆 ≤ 𝑁)))
102	84, 85, 101	syl2anb 601	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) → (((𝑥 ∈ ℝ ∧ 𝑆 ∈ ℝ) ∧ (𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ)) ∧ (𝑥 ≤ 𝑁 ∧ 𝑆 ≤ 𝑁)))
103		le2add 11200	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑥 ∈ ℝ ∧ 𝑆 ∈ ℝ) ∧ (𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ)) → ((𝑥 ≤ 𝑁 ∧ 𝑆 ≤ 𝑁) → (𝑥 + 𝑆) ≤ (𝑁 + 𝑁)))
104	103	imp 410	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑥 ∈ ℝ ∧ 𝑆 ∈ ℝ) ∧ (𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ)) ∧ (𝑥 ≤ 𝑁 ∧ 𝑆 ≤ 𝑁)) → (𝑥 + 𝑆) ≤ (𝑁 + 𝑁))
105	102, 104	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) → (𝑥 + 𝑆) ≤ (𝑁 + 𝑁))
106	66, 65, 65	3jca 1129	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑥 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → ((𝑥 + 𝑆) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ))
107	106	ex 416	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 ∈ ℤ → ((𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑥 + 𝑆) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ)))
108	107, 26	syl11 33	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑥 ∈ (0...𝑁) → ((𝑥 + 𝑆) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ)))
109	29, 46, 108	syl2anc 587	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑆 ∈ (0..^𝑁) → (𝑥 ∈ (0...𝑁) → ((𝑥 + 𝑆) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ)))
110	109	imp 410	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) → ((𝑥 + 𝑆) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ))
111		lesubadd 11190	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑥 + 𝑆) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (((𝑥 + 𝑆) − 𝑁) ≤ 𝑁 ↔ (𝑥 + 𝑆) ≤ (𝑁 + 𝑁)))
112	110, 111	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) → (((𝑥 + 𝑆) − 𝑁) ≤ 𝑁 ↔ (𝑥 + 𝑆) ≤ (𝑁 + 𝑁)))
113	105, 112	mpbird 260	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) → ((𝑥 + 𝑆) − 𝑁) ≤ 𝑁)
114	113	adantr 484	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) ∧ ¬ 𝑥 ≤ (𝑁 − 𝑆)) → ((𝑥 + 𝑆) − 𝑁) ≤ 𝑁)
115	114, 22	breqtrdi 5071	. . . . . . . . . . . . . . . 16 ⊢ (((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) ∧ ¬ 𝑥 ≤ (𝑁 − 𝑆)) → ((𝑥 + 𝑆) − 𝑁) ≤ (♯‘𝐹))
116	82, 83, 115	3jca 1129	. . . . . . . . . . . . . . 15 ⊢ (((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) ∧ ¬ 𝑥 ≤ (𝑁 − 𝑆)) → (((𝑥 + 𝑆) − 𝑁) ∈ ℕ₀ ∧ (♯‘𝐹) ∈ ℕ₀ ∧ ((𝑥 + 𝑆) − 𝑁) ≤ (♯‘𝐹)))
117	15, 116	sylanl1 680	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (0...𝑁)) ∧ ¬ 𝑥 ≤ (𝑁 − 𝑆)) → (((𝑥 + 𝑆) − 𝑁) ∈ ℕ₀ ∧ (♯‘𝐹) ∈ ℕ₀ ∧ ((𝑥 + 𝑆) − 𝑁) ≤ (♯‘𝐹)))
118		elfz2nn0 13089	. . . . . . . . . . . . . 14 ⊢ (((𝑥 + 𝑆) − 𝑁) ∈ (0...(♯‘𝐹)) ↔ (((𝑥 + 𝑆) − 𝑁) ∈ ℕ₀ ∧ (♯‘𝐹) ∈ ℕ₀ ∧ ((𝑥 + 𝑆) − 𝑁) ≤ (♯‘𝐹)))
119	117, 118	sylibr 237	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (0...𝑁)) ∧ ¬ 𝑥 ≤ (𝑁 − 𝑆)) → ((𝑥 + 𝑆) − 𝑁) ∈ (0...(♯‘𝐹)))
120	119	adantll 714	. . . . . . . . . . . 12 ⊢ (((𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ (𝜑 ∧ 𝑥 ∈ (0...𝑁))) ∧ ¬ 𝑥 ≤ (𝑁 − 𝑆)) → ((𝑥 + 𝑆) − 𝑁) ∈ (0...(♯‘𝐹)))
121	45, 120	ffvelrnd 6862	. . . . . . . . . . 11 ⊢ (((𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ (𝜑 ∧ 𝑥 ∈ (0...𝑁))) ∧ ¬ 𝑥 ≤ (𝑁 − 𝑆)) → (𝑃‘((𝑥 + 𝑆) − 𝑁)) ∈ 𝑉)
122	44, 121	ifclda 4449	. . . . . . . . . 10 ⊢ ((𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ (𝜑 ∧ 𝑥 ∈ (0...𝑁))) → if(𝑥 ≤ (𝑁 − 𝑆), (𝑃‘(𝑥 + 𝑆)), (𝑃‘((𝑥 + 𝑆) − 𝑁))) ∈ 𝑉)
123	122	exp32 424	. . . . . . . . 9 ⊢ (𝑃:(0...(♯‘𝐹))⟶𝑉 → (𝜑 → (𝑥 ∈ (0...𝑁) → if(𝑥 ≤ (𝑁 − 𝑆), (𝑃‘(𝑥 + 𝑆)), (𝑃‘((𝑥 + 𝑆) − 𝑁))) ∈ 𝑉)))
124	13, 123	syl 17	. . . . . . . 8 ⊢ (𝐹(Walks‘𝐺)𝑃 → (𝜑 → (𝑥 ∈ (0...𝑁) → if(𝑥 ≤ (𝑁 − 𝑆), (𝑃‘(𝑥 + 𝑆)), (𝑃‘((𝑥 + 𝑆) − 𝑁))) ∈ 𝑉)))
125	11, 124	mpcom 38	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ (0...𝑁) → if(𝑥 ≤ (𝑁 − 𝑆), (𝑃‘(𝑥 + 𝑆)), (𝑃‘((𝑥 + 𝑆) − 𝑁))) ∈ 𝑉))
126	125	imp 410	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (0...𝑁)) → if(𝑥 ≤ (𝑁 − 𝑆), (𝑃‘(𝑥 + 𝑆)), (𝑃‘((𝑥 + 𝑆) − 𝑁))) ∈ 𝑉)
127		crctcsh.q	. . . . . 6 ⊢ 𝑄 = (𝑥 ∈ (0...𝑁) ↦ if(𝑥 ≤ (𝑁 − 𝑆), (𝑃‘(𝑥 + 𝑆)), (𝑃‘((𝑥 + 𝑆) − 𝑁))))
128	126, 127	fmptd 6888	. . . . 5 ⊢ (𝜑 → 𝑄:(0...𝑁)⟶𝑉)
129	12, 4, 2, 22, 15, 1	crctcshlem2 27756	. . . . . . 7 ⊢ (𝜑 → (♯‘𝐻) = 𝑁)
130	129	oveq2d 7186	. . . . . 6 ⊢ (𝜑 → (0...(♯‘𝐻)) = (0...𝑁))
131	130	feq2d 6490	. . . . 5 ⊢ (𝜑 → (𝑄:(0...(♯‘𝐻))⟶𝑉 ↔ 𝑄:(0...𝑁)⟶𝑉))
132	128, 131	mpbird 260	. . . 4 ⊢ (𝜑 → 𝑄:(0...(♯‘𝐻))⟶𝑉)
133	132	adantr 484	. . 3 ⊢ ((𝜑 ∧ 𝑆 ≠ 0) → 𝑄:(0...(♯‘𝐻))⟶𝑉)
134	12, 4	wlkprop 27553	. . . . . 6 ⊢ (𝐹(Walks‘𝐺)𝑃 → (𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(♯‘𝐹))if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖)))))
135	2, 3, 134	3syl 18	. . . . 5 ⊢ (𝜑 → (𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(♯‘𝐹))if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖)))))
136	135	adantr 484	. . . 4 ⊢ ((𝜑 ∧ 𝑆 ≠ 0) → (𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(♯‘𝐹))if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖)))))
137	22	eqcomi 2747	. . . . . . . . . 10 ⊢ (♯‘𝐹) = 𝑁
138	137	oveq2i 7181	. . . . . . . . 9 ⊢ (0..^(♯‘𝐹)) = (0..^𝑁)
139	138	raleqi 3314	. . . . . . . 8 ⊢ (∀𝑖 ∈ (0..^(♯‘𝐹))if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖))) ↔ ∀𝑖 ∈ (0..^𝑁)if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖))))
140		fzo1fzo0n0 13179	. . . . . . . . . . . . . . 15 ⊢ (𝑆 ∈ (1..^𝑁) ↔ (𝑆 ∈ (0..^𝑁) ∧ 𝑆 ≠ 0))
141	140	simplbi2 504	. . . . . . . . . . . . . 14 ⊢ (𝑆 ∈ (0..^𝑁) → (𝑆 ≠ 0 → 𝑆 ∈ (1..^𝑁)))
142	15, 141	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑆 ≠ 0 → 𝑆 ∈ (1..^𝑁)))
143	142	imp 410	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑆 ≠ 0) → 𝑆 ∈ (1..^𝑁))
144	143	ad2antlr 727	. . . . . . . . . . 11 ⊢ ((((𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉) ∧ (𝜑 ∧ 𝑆 ≠ 0)) ∧ ∀𝑖 ∈ (0..^𝑁)if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖)))) → 𝑆 ∈ (1..^𝑁))
145		simplll 775	. . . . . . . . . . 11 ⊢ ((((𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉) ∧ (𝜑 ∧ 𝑆 ≠ 0)) ∧ ∀𝑖 ∈ (0..^𝑁)if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖)))) → 𝐹 ∈ Word dom 𝐼)
146		wkslem1 27549	. . . . . . . . . . . . . 14 ⊢ (𝑖 = 𝑘 → (if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖))) ↔ if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘)))))
147	146	cbvralvw 3349	. . . . . . . . . . . . 13 ⊢ (∀𝑖 ∈ (0..^𝑁)if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖))) ↔ ∀𝑘 ∈ (0..^𝑁)if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘))))
148	147	biimpi 219	. . . . . . . . . . . 12 ⊢ (∀𝑖 ∈ (0..^𝑁)if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖))) → ∀𝑘 ∈ (0..^𝑁)if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘))))
149	148	adantl 485	. . . . . . . . . . 11 ⊢ ((((𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉) ∧ (𝜑 ∧ 𝑆 ≠ 0)) ∧ ∀𝑖 ∈ (0..^𝑁)if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖)))) → ∀𝑘 ∈ (0..^𝑁)if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘))))
150		crctprop 27733	. . . . . . . . . . . . . 14 ⊢ (𝐹(Circuits‘𝐺)𝑃 → (𝐹(Trails‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))))
151	137	fveq2i 6677	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑃‘(♯‘𝐹)) = (𝑃‘𝑁)
152	151	eqeq2i 2751	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑃‘0) = (𝑃‘(♯‘𝐹)) ↔ (𝑃‘0) = (𝑃‘𝑁))
153	152	biimpi 219	. . . . . . . . . . . . . . . 16 ⊢ ((𝑃‘0) = (𝑃‘(♯‘𝐹)) → (𝑃‘0) = (𝑃‘𝑁))
154	153	eqcomd 2744	. . . . . . . . . . . . . . 15 ⊢ ((𝑃‘0) = (𝑃‘(♯‘𝐹)) → (𝑃‘𝑁) = (𝑃‘0))
155	154	adantl 485	. . . . . . . . . . . . . 14 ⊢ ((𝐹(Trails‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) → (𝑃‘𝑁) = (𝑃‘0))
156	2, 150, 155	3syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑃‘𝑁) = (𝑃‘0))
157	156	ad2antrl 728	. . . . . . . . . . . 12 ⊢ (((𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉) ∧ (𝜑 ∧ 𝑆 ≠ 0)) → (𝑃‘𝑁) = (𝑃‘0))
158	157	adantr 484	. . . . . . . . . . 11 ⊢ ((((𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉) ∧ (𝜑 ∧ 𝑆 ≠ 0)) ∧ ∀𝑖 ∈ (0..^𝑁)if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖)))) → (𝑃‘𝑁) = (𝑃‘0))
159	144, 127, 1, 22, 145, 149, 158	crctcshwlkn0lem7 27754	. . . . . . . . . 10 ⊢ ((((𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉) ∧ (𝜑 ∧ 𝑆 ≠ 0)) ∧ ∀𝑖 ∈ (0..^𝑁)if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖)))) → ∀𝑗 ∈ (0..^𝑁)if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗))))
160	129	oveq2d 7186	. . . . . . . . . . . . 13 ⊢ (𝜑 → (0..^(♯‘𝐻)) = (0..^𝑁))
161	160	raleqdv 3316	. . . . . . . . . . . 12 ⊢ (𝜑 → (∀𝑗 ∈ (0..^(♯‘𝐻))if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗))) ↔ ∀𝑗 ∈ (0..^𝑁)if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗)))))
162	161	ad2antrl 728	. . . . . . . . . . 11 ⊢ (((𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉) ∧ (𝜑 ∧ 𝑆 ≠ 0)) → (∀𝑗 ∈ (0..^(♯‘𝐻))if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗))) ↔ ∀𝑗 ∈ (0..^𝑁)if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗)))))
163	162	adantr 484	. . . . . . . . . 10 ⊢ ((((𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉) ∧ (𝜑 ∧ 𝑆 ≠ 0)) ∧ ∀𝑖 ∈ (0..^𝑁)if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖)))) → (∀𝑗 ∈ (0..^(♯‘𝐻))if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗))) ↔ ∀𝑗 ∈ (0..^𝑁)if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗)))))
164	159, 163	mpbird 260	. . . . . . . . 9 ⊢ ((((𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉) ∧ (𝜑 ∧ 𝑆 ≠ 0)) ∧ ∀𝑖 ∈ (0..^𝑁)if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖)))) → ∀𝑗 ∈ (0..^(♯‘𝐻))if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗))))
165	164	ex 416	. . . . . . . 8 ⊢ (((𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉) ∧ (𝜑 ∧ 𝑆 ≠ 0)) → (∀𝑖 ∈ (0..^𝑁)if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖))) → ∀𝑗 ∈ (0..^(♯‘𝐻))if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗)))))
166	139, 165	syl5bi 245	. . . . . . 7 ⊢ (((𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉) ∧ (𝜑 ∧ 𝑆 ≠ 0)) → (∀𝑖 ∈ (0..^(♯‘𝐹))if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖))) → ∀𝑗 ∈ (0..^(♯‘𝐻))if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗)))))
167	166	ex 416	. . . . . 6 ⊢ ((𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉) → ((𝜑 ∧ 𝑆 ≠ 0) → (∀𝑖 ∈ (0..^(♯‘𝐹))if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖))) → ∀𝑗 ∈ (0..^(♯‘𝐻))if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗))))))
168	167	com23 86	. . . . 5 ⊢ ((𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉) → (∀𝑖 ∈ (0..^(♯‘𝐹))if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖))) → ((𝜑 ∧ 𝑆 ≠ 0) → ∀𝑗 ∈ (0..^(♯‘𝐻))if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗))))))
169	168	3impia 1118	. . . 4 ⊢ ((𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(♯‘𝐹))if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖)))) → ((𝜑 ∧ 𝑆 ≠ 0) → ∀𝑗 ∈ (0..^(♯‘𝐻))if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗)))))
170	136, 169	mpcom 38	. . 3 ⊢ ((𝜑 ∧ 𝑆 ≠ 0) → ∀𝑗 ∈ (0..^(♯‘𝐻))if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗))))
171	10, 133, 170	3jca 1129	. 2 ⊢ ((𝜑 ∧ 𝑆 ≠ 0) → (𝐻 ∈ Word dom 𝐼 ∧ 𝑄:(0...(♯‘𝐻))⟶𝑉 ∧ ∀𝑗 ∈ (0..^(♯‘𝐻))if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗)))))
172	12, 4, 2, 22, 15, 1, 127	crctcshlem3 27757	. . . 4 ⊢ (𝜑 → (𝐺 ∈ V ∧ 𝐻 ∈ V ∧ 𝑄 ∈ V))
173	172	adantr 484	. . 3 ⊢ ((𝜑 ∧ 𝑆 ≠ 0) → (𝐺 ∈ V ∧ 𝐻 ∈ V ∧ 𝑄 ∈ V))
174	12, 4	iswlk 27552	. . 3 ⊢ ((𝐺 ∈ V ∧ 𝐻 ∈ V ∧ 𝑄 ∈ V) → (𝐻(Walks‘𝐺)𝑄 ↔ (𝐻 ∈ Word dom 𝐼 ∧ 𝑄:(0...(♯‘𝐻))⟶𝑉 ∧ ∀𝑗 ∈ (0..^(♯‘𝐻))if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗))))))
175	173, 174	syl 17	. 2 ⊢ ((𝜑 ∧ 𝑆 ≠ 0) → (𝐻(Walks‘𝐺)𝑄 ↔ (𝐻 ∈ Word dom 𝐼 ∧ 𝑄:(0...(♯‘𝐻))⟶𝑉 ∧ ∀𝑗 ∈ (0..^(♯‘𝐻))if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗))))))
176	171, 175	mpbird 260	1 ⊢ ((𝜑 ∧ 𝑆 ≠ 0) → 𝐻(Walks‘𝐺)𝑄)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 399 if-wif 1062 ∧ w3a 1088 = wceq 1542 ∈ wcel 2114 ≠ wne 2934 ∀wral 3053 Vcvv 3398 ⊆ wss 3843 ifcif 4414 {csn 4516 {cpr 4518 class class class wbr 5030 ↦ cmpt 5110 dom cdm 5525 ⟶wf 6335 ‘cfv 6339 (class class class)co 7170 ℝcr 10614 0cc0 10615 1c1 10616 + caddc 10618 < clt 10753 ≤ cle 10754 − cmin 10948 ℕcn 11716 ℕ₀cn0 11976 ℤcz 12062 ...cfz 12981 ..^cfzo 13124 ♯chash 13782 Word cword 13955 cyclShift ccsh 14239 Vtxcvtx 26941 iEdgciedg 26942 Walkscwlks 27538 Trailsctrls 27632 Circuitsccrcts 27725

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1975 ax-7 2020 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2162 ax-12 2179 ax-ext 2710 ax-rep 5154 ax-sep 5167 ax-nul 5174 ax-pow 5232 ax-pr 5296 ax-un 7479 ax-cnex 10671 ax-resscn 10672 ax-1cn 10673 ax-icn 10674 ax-addcl 10675 ax-addrcl 10676 ax-mulcl 10677 ax-mulrcl 10678 ax-mulcom 10679 ax-addass 10680 ax-mulass 10681 ax-distr 10682 ax-i2m1 10683 ax-1ne0 10684 ax-1rid 10685 ax-rnegex 10686 ax-rrecex 10687 ax-cnre 10688 ax-pre-lttri 10689 ax-pre-lttrn 10690 ax-pre-ltadd 10691 ax-pre-mulgt0 10692 ax-pre-sup 10693

This theorem depends on definitions: df-bi 210 df-an 400 df-or 847 df-ifp 1063 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1787 df-nf 1791 df-sb 2075 df-mo 2540 df-eu 2570 df-clab 2717 df-cleq 2730 df-clel 2811 df-nfc 2881 df-ne 2935 df-nel 3039 df-ral 3058 df-rex 3059 df-reu 3060 df-rmo 3061 df-rab 3062 df-v 3400 df-sbc 3681 df-csb 3791 df-dif 3846 df-un 3848 df-in 3850 df-ss 3860 df-pss 3862 df-nul 4212 df-if 4415 df-pw 4490 df-sn 4517 df-pr 4519 df-tp 4521 df-op 4523 df-uni 4797 df-int 4837 df-iun 4883 df-br 5031 df-opab 5093 df-mpt 5111 df-tr 5137 df-id 5429 df-eprel 5434 df-po 5442 df-so 5443 df-fr 5483 df-we 5485 df-xp 5531 df-rel 5532 df-cnv 5533 df-co 5534 df-dm 5535 df-rn 5536 df-res 5537 df-ima 5538 df-pred 6129 df-ord 6175 df-on 6176 df-lim 6177 df-suc 6178 df-iota 6297 df-fun 6341 df-fn 6342 df-f 6343 df-f1 6344 df-fo 6345 df-f1o 6346 df-fv 6347 df-riota 7127 df-ov 7173 df-oprab 7174 df-mpo 7175 df-om 7600 df-1st 7714 df-2nd 7715 df-wrecs 7976 df-recs 8037 df-rdg 8075 df-1o 8131 df-er 8320 df-map 8439 df-en 8556 df-dom 8557 df-sdom 8558 df-fin 8559 df-sup 8979 df-inf 8980 df-card 9441 df-pnf 10755 df-mnf 10756 df-xr 10757 df-ltxr 10758 df-le 10759 df-sub 10950 df-neg 10951 df-div 11376 df-nn 11717 df-2 11779 df-n0 11977 df-z 12063 df-uz 12325 df-rp 12473 df-fz 12982 df-fzo 13125 df-fl 13253 df-mod 13329 df-hash 13783 df-word 13956 df-concat 14012 df-substr 14092 df-pfx 14122 df-csh 14240 df-wlks 27541 df-trls 27634 df-crcts 27727

This theorem is referenced by: crctcshwlk 27760

W3C validator