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 27291

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 27269	. . . . . . 7 ⊢ (𝐹(Circuits‘𝐺)𝑃 → 𝐹(Walks‘𝐺)𝑃)
4		crctcsh.i	. . . . . . . 8 ⊢ 𝐼 = (iEdg‘𝐺)
5	4	wlkf 27084	. . . . . . 7 ⊢ (𝐹(Walks‘𝐺)𝑃 → 𝐹 ∈ Word dom 𝐼)
6	2, 3, 5	3syl 18	. . . . . 6 ⊢ (𝜑 → 𝐹 ∈ Word dom 𝐼)
7		cshwcl 14001	. . . . . 6 ⊢ (𝐹 ∈ Word dom 𝐼 → (𝐹 cyclShift 𝑆) ∈ Word dom 𝐼)
8	6, 7	syl 17	. . . . 5 ⊢ (𝜑 → (𝐹 cyclShift 𝑆) ∈ Word dom 𝐼)
9	1, 8	syl5eqel 2887	. . . 4 ⊢ (𝜑 → 𝐻 ∈ Word dom 𝐼)
10	9	adantr 481	. . 3 ⊢ ((𝜑 ∧ 𝑆 ≠ 0) → 𝐻 ∈ Word dom 𝐼)
11	2, 3	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝐹(Walks‘𝐺)𝑃)
12		crctcsh.v	. . . . . . . . . 10 ⊢ 𝑉 = (Vtx‘𝐺)
13	12	wlkp 27086	. . . . . . . . 9 ⊢ (𝐹(Walks‘𝐺)𝑃 → 𝑃:(0...(♯‘𝐹))⟶𝑉)
14		simpll 763	. . . . . . . . . . . 12 ⊢ (((𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ (𝜑 ∧ 𝑥 ∈ (0...𝑁))) ∧ 𝑥 ≤ (𝑁 − 𝑆)) → 𝑃:(0...(♯‘𝐹))⟶𝑉)
15		crctcsh.s	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑆 ∈ (0..^𝑁))
16		elfznn0 12855	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ (0...𝑁) → 𝑥 ∈ ℕ₀)
17	16	adantl 482	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) → 𝑥 ∈ ℕ₀)
18		elfzonn0 12937	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑆 ∈ (0..^𝑁) → 𝑆 ∈ ℕ₀)
19	18	adantr 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) → 𝑆 ∈ ℕ₀)
20	17, 19	nn0addcld 11812	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) → (𝑥 + 𝑆) ∈ ℕ₀)
21	20	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ (((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) ∧ 𝑥 ≤ (𝑁 − 𝑆)) → (𝑥 + 𝑆) ∈ ℕ₀)
22		crctcsh.n	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑁 = (♯‘𝐹)
23		elfz3nn0 12856	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (0...𝑁) → 𝑁 ∈ ℕ₀)
24	22, 23	syl5eqelr 2888	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ (0...𝑁) → (♯‘𝐹) ∈ ℕ₀)
25	24	ad2antlr 723	. . . . . . . . . . . . . . . 16 ⊢ (((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) ∧ 𝑥 ≤ (𝑁 − 𝑆)) → (♯‘𝐹) ∈ ℕ₀)
26		elfzelz 12763	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ (0...𝑁) → 𝑥 ∈ ℤ)
27	26	zred 11941	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ (0...𝑁) → 𝑥 ∈ ℝ)
28	27	adantl 482	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) → 𝑥 ∈ ℝ)
29		elfzoelz 12893	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑆 ∈ (0..^𝑁) → 𝑆 ∈ ℤ)
30	29	zred 11941	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑆 ∈ (0..^𝑁) → 𝑆 ∈ ℝ)
31	30	adantr 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) → 𝑆 ∈ ℝ)
32		elfzel2 12761	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ (0...𝑁) → 𝑁 ∈ ℤ)
33	32	zred 11941	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ (0...𝑁) → 𝑁 ∈ ℝ)
34	33	adantl 482	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) → 𝑁 ∈ ℝ)
35		leaddsub 10969	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ ℝ ∧ 𝑆 ∈ ℝ ∧ 𝑁 ∈ ℝ) → ((𝑥 + 𝑆) ≤ 𝑁 ↔ 𝑥 ≤ (𝑁 − 𝑆)))
36	28, 31, 34, 35	syl3anc 1364	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) → ((𝑥 + 𝑆) ≤ 𝑁 ↔ 𝑥 ≤ (𝑁 − 𝑆)))
37	36	biimpar 478	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) ∧ 𝑥 ≤ (𝑁 − 𝑆)) → (𝑥 + 𝑆) ≤ 𝑁)
38	37, 22	syl6breq 5007	. . . . . . . . . . . . . . . 16 ⊢ (((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) ∧ 𝑥 ≤ (𝑁 − 𝑆)) → (𝑥 + 𝑆) ≤ (♯‘𝐹))
39	21, 25, 38	3jca 1121	. . . . . . . . . . . . . . 15 ⊢ (((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) ∧ 𝑥 ≤ (𝑁 − 𝑆)) → ((𝑥 + 𝑆) ∈ ℕ₀ ∧ (♯‘𝐹) ∈ ℕ₀ ∧ (𝑥 + 𝑆) ≤ (♯‘𝐹)))
40	15, 39	sylanl1 676	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (0...𝑁)) ∧ 𝑥 ≤ (𝑁 − 𝑆)) → ((𝑥 + 𝑆) ∈ ℕ₀ ∧ (♯‘𝐹) ∈ ℕ₀ ∧ (𝑥 + 𝑆) ≤ (♯‘𝐹)))
41		elfz2nn0 12853	. . . . . . . . . . . . . 14 ⊢ ((𝑥 + 𝑆) ∈ (0...(♯‘𝐹)) ↔ ((𝑥 + 𝑆) ∈ ℕ₀ ∧ (♯‘𝐹) ∈ ℕ₀ ∧ (𝑥 + 𝑆) ≤ (♯‘𝐹)))
42	40, 41	sylibr 235	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (0...𝑁)) ∧ 𝑥 ≤ (𝑁 − 𝑆)) → (𝑥 + 𝑆) ∈ (0...(♯‘𝐹)))
43	42	adantll 710	. . . . . . . . . . . 12 ⊢ (((𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ (𝜑 ∧ 𝑥 ∈ (0...𝑁))) ∧ 𝑥 ≤ (𝑁 − 𝑆)) → (𝑥 + 𝑆) ∈ (0...(♯‘𝐹)))
44	14, 43	ffvelrnd 6722	. . . . . . . . . . 11 ⊢ (((𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ (𝜑 ∧ 𝑥 ∈ (0...𝑁))) ∧ 𝑥 ≤ (𝑁 − 𝑆)) → (𝑃‘(𝑥 + 𝑆)) ∈ 𝑉)
45		simpll 763	. . . . . . . . . . . 12 ⊢ (((𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ (𝜑 ∧ 𝑥 ∈ (0...𝑁))) ∧ ¬ 𝑥 ≤ (𝑁 − 𝑆)) → 𝑃:(0...(♯‘𝐹))⟶𝑉)
46		elfzoel2 12892	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑆 ∈ (0..^𝑁) → 𝑁 ∈ ℤ)
47		zaddcl 11876	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑥 ∈ ℤ ∧ 𝑆 ∈ ℤ) → (𝑥 + 𝑆) ∈ ℤ)
48	47	adantrr 713	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑥 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → (𝑥 + 𝑆) ∈ ℤ)
49		simprr 769	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑥 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → 𝑁 ∈ ℤ)
50	48, 49	zsubcld 11946	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑥 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → ((𝑥 + 𝑆) − 𝑁) ∈ ℤ)
51	50	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑥 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ)) ∧ ¬ 𝑥 ≤ (𝑁 − 𝑆)) → ((𝑥 + 𝑆) − 𝑁) ∈ ℤ)
52		zsubcl 11878	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑁 ∈ ℤ ∧ 𝑆 ∈ ℤ) → (𝑁 − 𝑆) ∈ ℤ)
53	52	ancoms 459	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 − 𝑆) ∈ ℤ)
54	53	zred 11941	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 − 𝑆) ∈ ℝ)
55		zre 11838	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 ∈ ℤ → 𝑥 ∈ ℝ)
56		ltnle 10572	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑁 − 𝑆) ∈ ℝ ∧ 𝑥 ∈ ℝ) → ((𝑁 − 𝑆) < 𝑥 ↔ ¬ 𝑥 ≤ (𝑁 − 𝑆)))
57	54, 55, 56	syl2anr 596	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑥 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → ((𝑁 − 𝑆) < 𝑥 ↔ ¬ 𝑥 ≤ (𝑁 − 𝑆)))
58		zre 11838	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℝ)
59	58	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑁 ∈ ℝ)
60		zre 11838	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑆 ∈ ℤ → 𝑆 ∈ ℝ)
61	60	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑆 ∈ ℝ)
62	55	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑥 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → 𝑥 ∈ ℝ)
63		ltsubadd 10963	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑁 ∈ ℝ ∧ 𝑆 ∈ ℝ ∧ 𝑥 ∈ ℝ) → ((𝑁 − 𝑆) < 𝑥 ↔ 𝑁 < (𝑥 + 𝑆)))
64	59, 61, 62, 63	syl2an23an 1416	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑥 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → ((𝑁 − 𝑆) < 𝑥 ↔ 𝑁 < (𝑥 + 𝑆)))
65	59	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑥 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → 𝑁 ∈ ℝ)
66	48	zred 11941	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑥 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → (𝑥 + 𝑆) ∈ ℝ)
67	65, 66	posdifd 11080	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑥 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → (𝑁 < (𝑥 + 𝑆) ↔ 0 < ((𝑥 + 𝑆) − 𝑁)))
68		0red 10495	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑥 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → 0 ∈ ℝ)
69	50	zred 11941	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑥 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → ((𝑥 + 𝑆) − 𝑁) ∈ ℝ)
70		ltle 10581	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((0 ∈ ℝ ∧ ((𝑥 + 𝑆) − 𝑁) ∈ ℝ) → (0 < ((𝑥 + 𝑆) − 𝑁) → 0 ≤ ((𝑥 + 𝑆) − 𝑁)))
71	68, 69, 70	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑥 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → (0 < ((𝑥 + 𝑆) − 𝑁) → 0 ≤ ((𝑥 + 𝑆) − 𝑁)))
72	67, 71	sylbid 241	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑥 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → (𝑁 < (𝑥 + 𝑆) → 0 ≤ ((𝑥 + 𝑆) − 𝑁)))
73	64, 72	sylbid 241	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑥 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → ((𝑁 − 𝑆) < 𝑥 → 0 ≤ ((𝑥 + 𝑆) − 𝑁)))
74	57, 73	sylbird 261	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑥 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → (¬ 𝑥 ≤ (𝑁 − 𝑆) → 0 ≤ ((𝑥 + 𝑆) − 𝑁)))
75	74	imp 407	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑥 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ)) ∧ ¬ 𝑥 ≤ (𝑁 − 𝑆)) → 0 ≤ ((𝑥 + 𝑆) − 𝑁))
76	51, 75	jca 512	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑥 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ)) ∧ ¬ 𝑥 ≤ (𝑁 − 𝑆)) → (((𝑥 + 𝑆) − 𝑁) ∈ ℤ ∧ 0 ≤ ((𝑥 + 𝑆) − 𝑁)))
77	76	exp31 420	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ ℤ → ((𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (¬ 𝑥 ≤ (𝑁 − 𝑆) → (((𝑥 + 𝑆) − 𝑁) ∈ ℤ ∧ 0 ≤ ((𝑥 + 𝑆) − 𝑁)))))
78	77, 26	syl11 33	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑥 ∈ (0...𝑁) → (¬ 𝑥 ≤ (𝑁 − 𝑆) → (((𝑥 + 𝑆) − 𝑁) ∈ ℤ ∧ 0 ≤ ((𝑥 + 𝑆) − 𝑁)))))
79	29, 46, 78	syl2anc 584	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑆 ∈ (0..^𝑁) → (𝑥 ∈ (0...𝑁) → (¬ 𝑥 ≤ (𝑁 − 𝑆) → (((𝑥 + 𝑆) − 𝑁) ∈ ℤ ∧ 0 ≤ ((𝑥 + 𝑆) − 𝑁)))))
80	79	imp31 418	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) ∧ ¬ 𝑥 ≤ (𝑁 − 𝑆)) → (((𝑥 + 𝑆) − 𝑁) ∈ ℤ ∧ 0 ≤ ((𝑥 + 𝑆) − 𝑁)))
81		elnn0z 11847	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑥 + 𝑆) − 𝑁) ∈ ℕ₀ ↔ (((𝑥 + 𝑆) − 𝑁) ∈ ℤ ∧ 0 ≤ ((𝑥 + 𝑆) − 𝑁)))
82	80, 81	sylibr 235	. . . . . . . . . . . . . . . 16 ⊢ (((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) ∧ ¬ 𝑥 ≤ (𝑁 − 𝑆)) → ((𝑥 + 𝑆) − 𝑁) ∈ ℕ₀)
83	24	ad2antlr 723	. . . . . . . . . . . . . . . 16 ⊢ (((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) ∧ ¬ 𝑥 ≤ (𝑁 − 𝑆)) → (♯‘𝐹) ∈ ℕ₀)
84		elfzo0 12933	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑆 ∈ (0..^𝑁) ↔ (𝑆 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁))
85		elfz2nn0 12853	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ (0...𝑁) ↔ (𝑥 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀ ∧ 𝑥 ≤ 𝑁))
86		nn0re 11759	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑆 ∈ ℕ₀ → 𝑆 ∈ ℝ)
87	86	3ad2ant1 1126	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑆 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) → 𝑆 ∈ ℝ)
88		nn0re 11759	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 ∈ ℕ₀ → 𝑥 ∈ ℝ)
89	88	3ad2ant1 1126	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑥 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀ ∧ 𝑥 ≤ 𝑁) → 𝑥 ∈ ℝ)
90	87, 89	anim12ci 613	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑆 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) ∧ (𝑥 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀ ∧ 𝑥 ≤ 𝑁)) → (𝑥 ∈ ℝ ∧ 𝑆 ∈ ℝ))
91		nnre 11498	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℝ)
92	91, 91	jca 512	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑁 ∈ ℕ → (𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ))
93	92	3ad2ant2 1127	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑆 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) → (𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ))
94	93	adantr 481	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑆 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) ∧ (𝑥 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀ ∧ 𝑥 ≤ 𝑁)) → (𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ))
95	90, 94	jca 512	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑆 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) ∧ (𝑥 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀ ∧ 𝑥 ≤ 𝑁)) → ((𝑥 ∈ ℝ ∧ 𝑆 ∈ ℝ) ∧ (𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ)))
96		simpr3 1189	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑆 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) ∧ (𝑥 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀ ∧ 𝑥 ≤ 𝑁)) → 𝑥 ≤ 𝑁)
97		ltle 10581	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑆 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (𝑆 < 𝑁 → 𝑆 ≤ 𝑁))
98	86, 91, 97	syl2an 595	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑆 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ) → (𝑆 < 𝑁 → 𝑆 ≤ 𝑁))
99	98	3impia 1110	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑆 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) → 𝑆 ≤ 𝑁)
100	99	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑆 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) ∧ (𝑥 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀ ∧ 𝑥 ≤ 𝑁)) → 𝑆 ≤ 𝑁)
101	95, 96, 100	jca32 516	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑆 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) ∧ (𝑥 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀ ∧ 𝑥 ≤ 𝑁)) → (((𝑥 ∈ ℝ ∧ 𝑆 ∈ ℝ) ∧ (𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ)) ∧ (𝑥 ≤ 𝑁 ∧ 𝑆 ≤ 𝑁)))
102	84, 85, 101	syl2anb 597	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) → (((𝑥 ∈ ℝ ∧ 𝑆 ∈ ℝ) ∧ (𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ)) ∧ (𝑥 ≤ 𝑁 ∧ 𝑆 ≤ 𝑁)))
103		le2add 10975	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑥 ∈ ℝ ∧ 𝑆 ∈ ℝ) ∧ (𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ)) → ((𝑥 ≤ 𝑁 ∧ 𝑆 ≤ 𝑁) → (𝑥 + 𝑆) ≤ (𝑁 + 𝑁)))
104	103	imp 407	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑥 ∈ ℝ ∧ 𝑆 ∈ ℝ) ∧ (𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ)) ∧ (𝑥 ≤ 𝑁 ∧ 𝑆 ≤ 𝑁)) → (𝑥 + 𝑆) ≤ (𝑁 + 𝑁))
105	102, 104	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) → (𝑥 + 𝑆) ≤ (𝑁 + 𝑁))
106	66, 65, 65	3jca 1121	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑥 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → ((𝑥 + 𝑆) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ))
107	106	ex 413	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 ∈ ℤ → ((𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑥 + 𝑆) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ)))
108	107, 26	syl11 33	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑥 ∈ (0...𝑁) → ((𝑥 + 𝑆) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ)))
109	29, 46, 108	syl2anc 584	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑆 ∈ (0..^𝑁) → (𝑥 ∈ (0...𝑁) → ((𝑥 + 𝑆) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ)))
110	109	imp 407	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) → ((𝑥 + 𝑆) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ))
111		lesubadd 10965	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑥 + 𝑆) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (((𝑥 + 𝑆) − 𝑁) ≤ 𝑁 ↔ (𝑥 + 𝑆) ≤ (𝑁 + 𝑁)))
112	110, 111	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) → (((𝑥 + 𝑆) − 𝑁) ≤ 𝑁 ↔ (𝑥 + 𝑆) ≤ (𝑁 + 𝑁)))
113	105, 112	mpbird 258	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) → ((𝑥 + 𝑆) − 𝑁) ≤ 𝑁)
114	113	adantr 481	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) ∧ ¬ 𝑥 ≤ (𝑁 − 𝑆)) → ((𝑥 + 𝑆) − 𝑁) ≤ 𝑁)
115	114, 22	syl6breq 5007	. . . . . . . . . . . . . . . 16 ⊢ (((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) ∧ ¬ 𝑥 ≤ (𝑁 − 𝑆)) → ((𝑥 + 𝑆) − 𝑁) ≤ (♯‘𝐹))
116	82, 83, 115	3jca 1121	. . . . . . . . . . . . . . 15 ⊢ (((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) ∧ ¬ 𝑥 ≤ (𝑁 − 𝑆)) → (((𝑥 + 𝑆) − 𝑁) ∈ ℕ₀ ∧ (♯‘𝐹) ∈ ℕ₀ ∧ ((𝑥 + 𝑆) − 𝑁) ≤ (♯‘𝐹)))
117	15, 116	sylanl1 676	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (0...𝑁)) ∧ ¬ 𝑥 ≤ (𝑁 − 𝑆)) → (((𝑥 + 𝑆) − 𝑁) ∈ ℕ₀ ∧ (♯‘𝐹) ∈ ℕ₀ ∧ ((𝑥 + 𝑆) − 𝑁) ≤ (♯‘𝐹)))
118		elfz2nn0 12853	. . . . . . . . . . . . . 14 ⊢ (((𝑥 + 𝑆) − 𝑁) ∈ (0...(♯‘𝐹)) ↔ (((𝑥 + 𝑆) − 𝑁) ∈ ℕ₀ ∧ (♯‘𝐹) ∈ ℕ₀ ∧ ((𝑥 + 𝑆) − 𝑁) ≤ (♯‘𝐹)))
119	117, 118	sylibr 235	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (0...𝑁)) ∧ ¬ 𝑥 ≤ (𝑁 − 𝑆)) → ((𝑥 + 𝑆) − 𝑁) ∈ (0...(♯‘𝐹)))
120	119	adantll 710	. . . . . . . . . . . 12 ⊢ (((𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ (𝜑 ∧ 𝑥 ∈ (0...𝑁))) ∧ ¬ 𝑥 ≤ (𝑁 − 𝑆)) → ((𝑥 + 𝑆) − 𝑁) ∈ (0...(♯‘𝐹)))
121	45, 120	ffvelrnd 6722	. . . . . . . . . . 11 ⊢ (((𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ (𝜑 ∧ 𝑥 ∈ (0...𝑁))) ∧ ¬ 𝑥 ≤ (𝑁 − 𝑆)) → (𝑃‘((𝑥 + 𝑆) − 𝑁)) ∈ 𝑉)
122	44, 121	ifclda 4419	. . . . . . . . . 10 ⊢ ((𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ (𝜑 ∧ 𝑥 ∈ (0...𝑁))) → if(𝑥 ≤ (𝑁 − 𝑆), (𝑃‘(𝑥 + 𝑆)), (𝑃‘((𝑥 + 𝑆) − 𝑁))) ∈ 𝑉)
123	122	exp32 421	. . . . . . . . 9 ⊢ (𝑃:(0...(♯‘𝐹))⟶𝑉 → (𝜑 → (𝑥 ∈ (0...𝑁) → if(𝑥 ≤ (𝑁 − 𝑆), (𝑃‘(𝑥 + 𝑆)), (𝑃‘((𝑥 + 𝑆) − 𝑁))) ∈ 𝑉)))
124	13, 123	syl 17	. . . . . . . 8 ⊢ (𝐹(Walks‘𝐺)𝑃 → (𝜑 → (𝑥 ∈ (0...𝑁) → if(𝑥 ≤ (𝑁 − 𝑆), (𝑃‘(𝑥 + 𝑆)), (𝑃‘((𝑥 + 𝑆) − 𝑁))) ∈ 𝑉)))
125	11, 124	mpcom 38	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ (0...𝑁) → if(𝑥 ≤ (𝑁 − 𝑆), (𝑃‘(𝑥 + 𝑆)), (𝑃‘((𝑥 + 𝑆) − 𝑁))) ∈ 𝑉))
126	125	imp 407	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (0...𝑁)) → if(𝑥 ≤ (𝑁 − 𝑆), (𝑃‘(𝑥 + 𝑆)), (𝑃‘((𝑥 + 𝑆) − 𝑁))) ∈ 𝑉)
127		crctcsh.q	. . . . . 6 ⊢ 𝑄 = (𝑥 ∈ (0...𝑁) ↦ if(𝑥 ≤ (𝑁 − 𝑆), (𝑃‘(𝑥 + 𝑆)), (𝑃‘((𝑥 + 𝑆) − 𝑁))))
128	126, 127	fmptd 6746	. . . . 5 ⊢ (𝜑 → 𝑄:(0...𝑁)⟶𝑉)
129	12, 4, 2, 22, 15, 1	crctcshlem2 27288	. . . . . . 7 ⊢ (𝜑 → (♯‘𝐻) = 𝑁)
130	129	oveq2d 7037	. . . . . 6 ⊢ (𝜑 → (0...(♯‘𝐻)) = (0...𝑁))
131	130	feq2d 6373	. . . . 5 ⊢ (𝜑 → (𝑄:(0...(♯‘𝐻))⟶𝑉 ↔ 𝑄:(0...𝑁)⟶𝑉))
132	128, 131	mpbird 258	. . . 4 ⊢ (𝜑 → 𝑄:(0...(♯‘𝐻))⟶𝑉)
133	132	adantr 481	. . 3 ⊢ ((𝜑 ∧ 𝑆 ≠ 0) → 𝑄:(0...(♯‘𝐻))⟶𝑉)
134	12, 4	wlkprop 27081	. . . . . 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 481	. . . 4 ⊢ ((𝜑 ∧ 𝑆 ≠ 0) → (𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(♯‘𝐹))if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖)))))
137	22	eqcomi 2804	. . . . . . . . . 10 ⊢ (♯‘𝐹) = 𝑁
138	137	oveq2i 7032	. . . . . . . . 9 ⊢ (0..^(♯‘𝐹)) = (0..^𝑁)
139	138	raleqi 3373	. . . . . . . 8 ⊢ (∀𝑖 ∈ (0..^(♯‘𝐹))if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖))) ↔ ∀𝑖 ∈ (0..^𝑁)if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖))))
140		fzo1fzo0n0 12943	. . . . . . . . . . . . . . 15 ⊢ (𝑆 ∈ (1..^𝑁) ↔ (𝑆 ∈ (0..^𝑁) ∧ 𝑆 ≠ 0))
141	140	simplbi2 501	. . . . . . . . . . . . . 14 ⊢ (𝑆 ∈ (0..^𝑁) → (𝑆 ≠ 0 → 𝑆 ∈ (1..^𝑁)))
142	15, 141	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑆 ≠ 0 → 𝑆 ∈ (1..^𝑁)))
143	142	imp 407	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑆 ≠ 0) → 𝑆 ∈ (1..^𝑁))
144	143	ad2antlr 723	. . . . . . . . . . 11 ⊢ ((((𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉) ∧ (𝜑 ∧ 𝑆 ≠ 0)) ∧ ∀𝑖 ∈ (0..^𝑁)if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖)))) → 𝑆 ∈ (1..^𝑁))
145		simplll 771	. . . . . . . . . . 11 ⊢ ((((𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉) ∧ (𝜑 ∧ 𝑆 ≠ 0)) ∧ ∀𝑖 ∈ (0..^𝑁)if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖)))) → 𝐹 ∈ Word dom 𝐼)
146		wkslem1 27077	. . . . . . . . . . . . . 14 ⊢ (𝑖 = 𝑘 → (if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖))) ↔ if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘)))))
147	146	cbvralv 3403	. . . . . . . . . . . . 13 ⊢ (∀𝑖 ∈ (0..^𝑁)if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖))) ↔ ∀𝑘 ∈ (0..^𝑁)if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘))))
148	147	biimpi 217	. . . . . . . . . . . 12 ⊢ (∀𝑖 ∈ (0..^𝑁)if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖))) → ∀𝑘 ∈ (0..^𝑁)if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘))))
149	148	adantl 482	. . . . . . . . . . 11 ⊢ ((((𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉) ∧ (𝜑 ∧ 𝑆 ≠ 0)) ∧ ∀𝑖 ∈ (0..^𝑁)if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖)))) → ∀𝑘 ∈ (0..^𝑁)if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘))))
150		crctprop 27265	. . . . . . . . . . . . . 14 ⊢ (𝐹(Circuits‘𝐺)𝑃 → (𝐹(Trails‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))))
151	137	fveq2i 6546	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑃‘(♯‘𝐹)) = (𝑃‘𝑁)
152	151	eqeq2i 2807	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑃‘0) = (𝑃‘(♯‘𝐹)) ↔ (𝑃‘0) = (𝑃‘𝑁))
153	152	biimpi 217	. . . . . . . . . . . . . . . 16 ⊢ ((𝑃‘0) = (𝑃‘(♯‘𝐹)) → (𝑃‘0) = (𝑃‘𝑁))
154	153	eqcomd 2801	. . . . . . . . . . . . . . 15 ⊢ ((𝑃‘0) = (𝑃‘(♯‘𝐹)) → (𝑃‘𝑁) = (𝑃‘0))
155	154	adantl 482	. . . . . . . . . . . . . 14 ⊢ ((𝐹(Trails‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) → (𝑃‘𝑁) = (𝑃‘0))
156	2, 150, 155	3syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑃‘𝑁) = (𝑃‘0))
157	156	ad2antrl 724	. . . . . . . . . . . 12 ⊢ (((𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉) ∧ (𝜑 ∧ 𝑆 ≠ 0)) → (𝑃‘𝑁) = (𝑃‘0))
158	157	adantr 481	. . . . . . . . . . 11 ⊢ ((((𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉) ∧ (𝜑 ∧ 𝑆 ≠ 0)) ∧ ∀𝑖 ∈ (0..^𝑁)if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖)))) → (𝑃‘𝑁) = (𝑃‘0))
159	144, 127, 1, 22, 145, 149, 158	crctcshwlkn0lem7 27286	. . . . . . . . . 10 ⊢ ((((𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉) ∧ (𝜑 ∧ 𝑆 ≠ 0)) ∧ ∀𝑖 ∈ (0..^𝑁)if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖)))) → ∀𝑗 ∈ (0..^𝑁)if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗))))
160	129	oveq2d 7037	. . . . . . . . . . . . 13 ⊢ (𝜑 → (0..^(♯‘𝐻)) = (0..^𝑁))
161	160	raleqdv 3375	. . . . . . . . . . . 12 ⊢ (𝜑 → (∀𝑗 ∈ (0..^(♯‘𝐻))if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗))) ↔ ∀𝑗 ∈ (0..^𝑁)if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗)))))
162	161	ad2antrl 724	. . . . . . . . . . 11 ⊢ (((𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉) ∧ (𝜑 ∧ 𝑆 ≠ 0)) → (∀𝑗 ∈ (0..^(♯‘𝐻))if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗))) ↔ ∀𝑗 ∈ (0..^𝑁)if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗)))))
163	162	adantr 481	. . . . . . . . . 10 ⊢ ((((𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉) ∧ (𝜑 ∧ 𝑆 ≠ 0)) ∧ ∀𝑖 ∈ (0..^𝑁)if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖)))) → (∀𝑗 ∈ (0..^(♯‘𝐻))if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗))) ↔ ∀𝑗 ∈ (0..^𝑁)if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗)))))
164	159, 163	mpbird 258	. . . . . . . . 9 ⊢ ((((𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉) ∧ (𝜑 ∧ 𝑆 ≠ 0)) ∧ ∀𝑖 ∈ (0..^𝑁)if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖)))) → ∀𝑗 ∈ (0..^(♯‘𝐻))if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗))))
165	164	ex 413	. . . . . . . 8 ⊢ (((𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉) ∧ (𝜑 ∧ 𝑆 ≠ 0)) → (∀𝑖 ∈ (0..^𝑁)if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖))) → ∀𝑗 ∈ (0..^(♯‘𝐻))if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗)))))
166	139, 165	syl5bi 243	. . . . . . 7 ⊢ (((𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉) ∧ (𝜑 ∧ 𝑆 ≠ 0)) → (∀𝑖 ∈ (0..^(♯‘𝐹))if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖))) → ∀𝑗 ∈ (0..^(♯‘𝐻))if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗)))))
167	166	ex 413	. . . . . 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 1110	. . . 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 1121	. 2 ⊢ ((𝜑 ∧ 𝑆 ≠ 0) → (𝐻 ∈ Word dom 𝐼 ∧ 𝑄:(0...(♯‘𝐻))⟶𝑉 ∧ ∀𝑗 ∈ (0..^(♯‘𝐻))if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗)))))
172	12, 4, 2, 22, 15, 1, 127	crctcshlem3 27289	. . . 4 ⊢ (𝜑 → (𝐺 ∈ V ∧ 𝐻 ∈ V ∧ 𝑄 ∈ V))
173	172	adantr 481	. . 3 ⊢ ((𝜑 ∧ 𝑆 ≠ 0) → (𝐺 ∈ V ∧ 𝐻 ∈ V ∧ 𝑄 ∈ V))
174	12, 4	iswlk 27080	. . 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 258	1 ⊢ ((𝜑 ∧ 𝑆 ≠ 0) → 𝐻(Walks‘𝐺)𝑄)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 207 ∧ wa 396 if-wif 1055 ∧ w3a 1080 = wceq 1522 ∈ wcel 2081 ≠ wne 2984 ∀wral 3105 Vcvv 3437 ⊆ wss 3863 ifcif 4385 {csn 4476 {cpr 4478 class class class wbr 4966 ↦ cmpt 5045 dom cdm 5448 ⟶wf 6226 ‘cfv 6230 (class class class)co 7021 ℝcr 10387 0cc0 10388 1c1 10389 + caddc 10391 < clt 10526 ≤ cle 10527 − cmin 10722 ℕcn 11491 ℕ₀cn0 11750 ℤcz 11834 ...cfz 12747 ..^cfzo 12888 ♯chash 13545 Word cword 13712 cyclShift ccsh 13991 Vtxcvtx 26469 iEdgciedg 26470 Walkscwlks 27066 Trailsctrls 27162 Circuitsccrcts 27257

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1777 ax-4 1791 ax-5 1888 ax-6 1947 ax-7 1992 ax-8 2083 ax-9 2091 ax-10 2112 ax-11 2126 ax-12 2141 ax-13 2344 ax-ext 2769 ax-rep 5086 ax-sep 5099 ax-nul 5106 ax-pow 5162 ax-pr 5226 ax-un 7324 ax-cnex 10444 ax-resscn 10445 ax-1cn 10446 ax-icn 10447 ax-addcl 10448 ax-addrcl 10449 ax-mulcl 10450 ax-mulrcl 10451 ax-mulcom 10452 ax-addass 10453 ax-mulass 10454 ax-distr 10455 ax-i2m1 10456 ax-1ne0 10457 ax-1rid 10458 ax-rnegex 10459 ax-rrecex 10460 ax-cnre 10461 ax-pre-lttri 10462 ax-pre-lttrn 10463 ax-pre-ltadd 10464 ax-pre-mulgt0 10465 ax-pre-sup 10466

This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-ifp 1056 df-3or 1081 df-3an 1082 df-tru 1525 df-ex 1762 df-nf 1766 df-sb 2043 df-mo 2576 df-eu 2612 df-clab 2776 df-cleq 2788 df-clel 2863 df-nfc 2935 df-ne 2985 df-nel 3091 df-ral 3110 df-rex 3111 df-reu 3112 df-rmo 3113 df-rab 3114 df-v 3439 df-sbc 3710 df-csb 3816 df-dif 3866 df-un 3868 df-in 3870 df-ss 3878 df-pss 3880 df-nul 4216 df-if 4386 df-pw 4459 df-sn 4477 df-pr 4479 df-tp 4481 df-op 4483 df-uni 4750 df-int 4787 df-iun 4831 df-br 4967 df-opab 5029 df-mpt 5046 df-tr 5069 df-id 5353 df-eprel 5358 df-po 5367 df-so 5368 df-fr 5407 df-we 5409 df-xp 5454 df-rel 5455 df-cnv 5456 df-co 5457 df-dm 5458 df-rn 5459 df-res 5460 df-ima 5461 df-pred 6028 df-ord 6074 df-on 6075 df-lim 6076 df-suc 6077 df-iota 6194 df-fun 6232 df-fn 6233 df-f 6234 df-f1 6235 df-fo 6236 df-f1o 6237 df-fv 6238 df-riota 6982 df-ov 7024 df-oprab 7025 df-mpo 7026 df-om 7442 df-1st 7550 df-2nd 7551 df-wrecs 7803 df-recs 7865 df-rdg 7903 df-1o 7958 df-oadd 7962 df-er 8144 df-map 8263 df-en 8363 df-dom 8364 df-sdom 8365 df-fin 8366 df-sup 8757 df-inf 8758 df-card 9219 df-pnf 10528 df-mnf 10529 df-xr 10530 df-ltxr 10531 df-le 10532 df-sub 10724 df-neg 10725 df-div 11151 df-nn 11492 df-2 11553 df-n0 11751 df-z 11835 df-uz 12099 df-rp 12245 df-fz 12748 df-fzo 12889 df-fl 13017 df-mod 13093 df-hash 13546 df-word 13713 df-concat 13774 df-substr 13844 df-pfx 13874 df-csh 13992 df-wlks 27069 df-trls 27164 df-crcts 27259

This theorem is referenced by: crctcshwlk 27292

W3C validator