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 29904

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 29879	. . . . . 6 ⊢ (𝐹(Circuits‘𝐺)𝑃 → 𝐹(Walks‘𝐺)𝑃)
4		crctcsh.i	. . . . . . 7 ⊢ 𝐼 = (iEdg‘𝐺)
5	4	wlkf 29698	. . . . . 6 ⊢ (𝐹(Walks‘𝐺)𝑃 → 𝐹 ∈ Word dom 𝐼)
6		cshwcl 14751	. . . . . 6 ⊢ (𝐹 ∈ Word dom 𝐼 → (𝐹 cyclShift 𝑆) ∈ Word dom 𝐼)
7	2, 3, 5, 6	4syl 19	. . . . 5 ⊢ (𝜑 → (𝐹 cyclShift 𝑆) ∈ Word dom 𝐼)
8	1, 7	eqeltrid 2841	. . . 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 29700	. . . . . . . . 9 ⊢ (𝐹(Walks‘𝐺)𝑃 → 𝑃:(0...(♯‘𝐹))⟶𝑉)
13		simpll 767	. . . . . . . . . . . 12 ⊢ (((𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ (𝜑 ∧ 𝑥 ∈ (0...𝑁))) ∧ 𝑥 ≤ (𝑁 − 𝑆)) → 𝑃:(0...(♯‘𝐹))⟶𝑉)
14		crctcsh.s	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑆 ∈ (0..^𝑁))
15		elfznn0 13565	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ (0...𝑁) → 𝑥 ∈ ℕ₀)
16	15	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) → 𝑥 ∈ ℕ₀)
17		elfzonn0 13653	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑆 ∈ (0..^𝑁) → 𝑆 ∈ ℕ₀)
18	17	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) → 𝑆 ∈ ℕ₀)
19	16, 18	nn0addcld 12493	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) → (𝑥 + 𝑆) ∈ ℕ₀)
20	19	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) ∧ 𝑥 ≤ (𝑁 − 𝑆)) → (𝑥 + 𝑆) ∈ ℕ₀)
21		crctcsh.n	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑁 = (♯‘𝐹)
22		elfz3nn0 13566	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (0...𝑁) → 𝑁 ∈ ℕ₀)
23	21, 22	eqeltrrid 2842	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ (0...𝑁) → (♯‘𝐹) ∈ ℕ₀)
24	23	ad2antlr 728	. . . . . . . . . . . . . . . 16 ⊢ (((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) ∧ 𝑥 ≤ (𝑁 − 𝑆)) → (♯‘𝐹) ∈ ℕ₀)
25		elfzelz 13469	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ (0...𝑁) → 𝑥 ∈ ℤ)
26	25	zred 12624	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ (0...𝑁) → 𝑥 ∈ ℝ)
27	26	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) → 𝑥 ∈ ℝ)
28		elfzoelz 13604	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑆 ∈ (0..^𝑁) → 𝑆 ∈ ℤ)
29	28	zred 12624	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑆 ∈ (0..^𝑁) → 𝑆 ∈ ℝ)
30	29	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) → 𝑆 ∈ ℝ)
31		elfzel2 13467	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ (0...𝑁) → 𝑁 ∈ ℤ)
32	31	zred 12624	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ (0...𝑁) → 𝑁 ∈ ℝ)
33	32	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) → 𝑁 ∈ ℝ)
34		leaddsub 11617	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ ℝ ∧ 𝑆 ∈ ℝ ∧ 𝑁 ∈ ℝ) → ((𝑥 + 𝑆) ≤ 𝑁 ↔ 𝑥 ≤ (𝑁 − 𝑆)))
35	27, 30, 33, 34	syl3anc 1374	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) → ((𝑥 + 𝑆) ≤ 𝑁 ↔ 𝑥 ≤ (𝑁 − 𝑆)))
36	35	biimpar 477	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) ∧ 𝑥 ≤ (𝑁 − 𝑆)) → (𝑥 + 𝑆) ≤ 𝑁)
37	36, 21	breqtrdi 5127	. . . . . . . . . . . . . . . 16 ⊢ (((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) ∧ 𝑥 ≤ (𝑁 − 𝑆)) → (𝑥 + 𝑆) ≤ (♯‘𝐹))
38	20, 24, 37	3jca 1129	. . . . . . . . . . . . . . 15 ⊢ (((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) ∧ 𝑥 ≤ (𝑁 − 𝑆)) → ((𝑥 + 𝑆) ∈ ℕ₀ ∧ (♯‘𝐹) ∈ ℕ₀ ∧ (𝑥 + 𝑆) ≤ (♯‘𝐹)))
39	14, 38	sylanl1 681	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (0...𝑁)) ∧ 𝑥 ≤ (𝑁 − 𝑆)) → ((𝑥 + 𝑆) ∈ ℕ₀ ∧ (♯‘𝐹) ∈ ℕ₀ ∧ (𝑥 + 𝑆) ≤ (♯‘𝐹)))
40		elfz2nn0 13563	. . . . . . . . . . . . . 14 ⊢ ((𝑥 + 𝑆) ∈ (0...(♯‘𝐹)) ↔ ((𝑥 + 𝑆) ∈ ℕ₀ ∧ (♯‘𝐹) ∈ ℕ₀ ∧ (𝑥 + 𝑆) ≤ (♯‘𝐹)))
41	39, 40	sylibr 234	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (0...𝑁)) ∧ 𝑥 ≤ (𝑁 − 𝑆)) → (𝑥 + 𝑆) ∈ (0...(♯‘𝐹)))
42	41	adantll 715	. . . . . . . . . . . 12 ⊢ (((𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ (𝜑 ∧ 𝑥 ∈ (0...𝑁))) ∧ 𝑥 ≤ (𝑁 − 𝑆)) → (𝑥 + 𝑆) ∈ (0...(♯‘𝐹)))
43	13, 42	ffvelcdmd 7031	. . . . . . . . . . 11 ⊢ (((𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ (𝜑 ∧ 𝑥 ∈ (0...𝑁))) ∧ 𝑥 ≤ (𝑁 − 𝑆)) → (𝑃‘(𝑥 + 𝑆)) ∈ 𝑉)
44		simpll 767	. . . . . . . . . . . 12 ⊢ (((𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ (𝜑 ∧ 𝑥 ∈ (0...𝑁))) ∧ ¬ 𝑥 ≤ (𝑁 − 𝑆)) → 𝑃:(0...(♯‘𝐹))⟶𝑉)
45		elfzoel2 13603	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑆 ∈ (0..^𝑁) → 𝑁 ∈ ℤ)
46		zaddcl 12558	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑥 ∈ ℤ ∧ 𝑆 ∈ ℤ) → (𝑥 + 𝑆) ∈ ℤ)
47	46	adantrr 718	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑥 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → (𝑥 + 𝑆) ∈ ℤ)
48		simprr 773	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑥 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → 𝑁 ∈ ℤ)
49	47, 48	zsubcld 12629	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑥 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → ((𝑥 + 𝑆) − 𝑁) ∈ ℤ)
50	49	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑥 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ)) ∧ ¬ 𝑥 ≤ (𝑁 − 𝑆)) → ((𝑥 + 𝑆) − 𝑁) ∈ ℤ)
51		zsubcl 12560	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑁 ∈ ℤ ∧ 𝑆 ∈ ℤ) → (𝑁 − 𝑆) ∈ ℤ)
52	51	ancoms 458	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 − 𝑆) ∈ ℤ)
53	52	zred 12624	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 − 𝑆) ∈ ℝ)
54		zre 12519	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 ∈ ℤ → 𝑥 ∈ ℝ)
55		ltnle 11216	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑁 − 𝑆) ∈ ℝ ∧ 𝑥 ∈ ℝ) → ((𝑁 − 𝑆) < 𝑥 ↔ ¬ 𝑥 ≤ (𝑁 − 𝑆)))
56	53, 54, 55	syl2anr 598	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑥 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → ((𝑁 − 𝑆) < 𝑥 ↔ ¬ 𝑥 ≤ (𝑁 − 𝑆)))
57		zre 12519	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℝ)
58	57	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑁 ∈ ℝ)
59		zre 12519	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑆 ∈ ℤ → 𝑆 ∈ ℝ)
60	59	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑆 ∈ ℝ)
61	54	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑥 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → 𝑥 ∈ ℝ)
62		ltsubadd 11611	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑁 ∈ ℝ ∧ 𝑆 ∈ ℝ ∧ 𝑥 ∈ ℝ) → ((𝑁 − 𝑆) < 𝑥 ↔ 𝑁 < (𝑥 + 𝑆)))
63	58, 60, 61, 62	syl2an23an 1426	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑥 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → ((𝑁 − 𝑆) < 𝑥 ↔ 𝑁 < (𝑥 + 𝑆)))
64	58	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑥 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → 𝑁 ∈ ℝ)
65	47	zred 12624	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑥 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → (𝑥 + 𝑆) ∈ ℝ)
66	64, 65	posdifd 11728	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑥 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → (𝑁 < (𝑥 + 𝑆) ↔ 0 < ((𝑥 + 𝑆) − 𝑁)))
67		0red 11138	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑥 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → 0 ∈ ℝ)
68	49	zred 12624	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑥 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → ((𝑥 + 𝑆) − 𝑁) ∈ ℝ)
69		ltle 11225	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((0 ∈ ℝ ∧ ((𝑥 + 𝑆) − 𝑁) ∈ ℝ) → (0 < ((𝑥 + 𝑆) − 𝑁) → 0 ≤ ((𝑥 + 𝑆) − 𝑁)))
70	67, 68, 69	syl2anc 585	. . . . . . . . . . . . . . . . . . . . . . . . . 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 585	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑆 ∈ (0..^𝑁) → (𝑥 ∈ (0...𝑁) → (¬ 𝑥 ≤ (𝑁 − 𝑆) → (((𝑥 + 𝑆) − 𝑁) ∈ ℤ ∧ 0 ≤ ((𝑥 + 𝑆) − 𝑁)))))
79	78	imp31 417	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) ∧ ¬ 𝑥 ≤ (𝑁 − 𝑆)) → (((𝑥 + 𝑆) − 𝑁) ∈ ℤ ∧ 0 ≤ ((𝑥 + 𝑆) − 𝑁)))
80		elnn0z 12528	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑥 + 𝑆) − 𝑁) ∈ ℕ₀ ↔ (((𝑥 + 𝑆) − 𝑁) ∈ ℤ ∧ 0 ≤ ((𝑥 + 𝑆) − 𝑁)))
81	79, 80	sylibr 234	. . . . . . . . . . . . . . . 16 ⊢ (((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) ∧ ¬ 𝑥 ≤ (𝑁 − 𝑆)) → ((𝑥 + 𝑆) − 𝑁) ∈ ℕ₀)
82	23	ad2antlr 728	. . . . . . . . . . . . . . . 16 ⊢ (((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) ∧ ¬ 𝑥 ≤ (𝑁 − 𝑆)) → (♯‘𝐹) ∈ ℕ₀)
83		elfzo0 13646	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑆 ∈ (0..^𝑁) ↔ (𝑆 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁))
84		elfz2nn0 13563	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ (0...𝑁) ↔ (𝑥 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀ ∧ 𝑥 ≤ 𝑁))
85		nn0re 12437	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑆 ∈ ℕ₀ → 𝑆 ∈ ℝ)
86	85	3ad2ant1 1134	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑆 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) → 𝑆 ∈ ℝ)
87		nn0re 12437	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 ∈ ℕ₀ → 𝑥 ∈ ℝ)
88	87	3ad2ant1 1134	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑥 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀ ∧ 𝑥 ≤ 𝑁) → 𝑥 ∈ ℝ)
89	86, 88	anim12ci 615	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑆 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) ∧ (𝑥 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀ ∧ 𝑥 ≤ 𝑁)) → (𝑥 ∈ ℝ ∧ 𝑆 ∈ ℝ))
90		nnre 12172	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℝ)
91	90, 90	jca 511	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑁 ∈ ℕ → (𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ))
92	91	3ad2ant2 1135	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑆 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) → (𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ))
93	92	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑆 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) ∧ (𝑥 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀ ∧ 𝑥 ≤ 𝑁)) → (𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ))
94	89, 93	jca 511	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑆 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) ∧ (𝑥 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀ ∧ 𝑥 ≤ 𝑁)) → ((𝑥 ∈ ℝ ∧ 𝑆 ∈ ℝ) ∧ (𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ)))
95		simpr3 1198	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑆 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) ∧ (𝑥 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀ ∧ 𝑥 ≤ 𝑁)) → 𝑥 ≤ 𝑁)
96		ltle 11225	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑆 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (𝑆 < 𝑁 → 𝑆 ≤ 𝑁))
97	85, 90, 96	syl2an 597	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑆 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ) → (𝑆 < 𝑁 → 𝑆 ≤ 𝑁))
98	97	3impia 1118	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑆 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) → 𝑆 ≤ 𝑁)
99	98	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑆 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) ∧ (𝑥 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀ ∧ 𝑥 ≤ 𝑁)) → 𝑆 ≤ 𝑁)
100	94, 95, 99	jca32 515	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑆 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) ∧ (𝑥 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀ ∧ 𝑥 ≤ 𝑁)) → (((𝑥 ∈ ℝ ∧ 𝑆 ∈ ℝ) ∧ (𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ)) ∧ (𝑥 ≤ 𝑁 ∧ 𝑆 ≤ 𝑁)))
101	83, 84, 100	syl2anb 599	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) → (((𝑥 ∈ ℝ ∧ 𝑆 ∈ ℝ) ∧ (𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ)) ∧ (𝑥 ≤ 𝑁 ∧ 𝑆 ≤ 𝑁)))
102		le2add 11623	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑥 ∈ ℝ ∧ 𝑆 ∈ ℝ) ∧ (𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ)) → ((𝑥 ≤ 𝑁 ∧ 𝑆 ≤ 𝑁) → (𝑥 + 𝑆) ≤ (𝑁 + 𝑁)))
103	102	imp 406	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑥 ∈ ℝ ∧ 𝑆 ∈ ℝ) ∧ (𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ)) ∧ (𝑥 ≤ 𝑁 ∧ 𝑆 ≤ 𝑁)) → (𝑥 + 𝑆) ≤ (𝑁 + 𝑁))
104	101, 103	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) → (𝑥 + 𝑆) ≤ (𝑁 + 𝑁))
105	65, 64, 64	3jca 1129	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑥 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → ((𝑥 + 𝑆) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ))
106	105	ex 412	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 ∈ ℤ → ((𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑥 + 𝑆) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ)))
107	106, 25	syl11 33	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑥 ∈ (0...𝑁) → ((𝑥 + 𝑆) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ)))
108	28, 45, 107	syl2anc 585	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑆 ∈ (0..^𝑁) → (𝑥 ∈ (0...𝑁) → ((𝑥 + 𝑆) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ)))
109	108	imp 406	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) → ((𝑥 + 𝑆) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ))
110		lesubadd 11613	. . . . . . . . . . . . . . . . . . . 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 5127	. . . . . . . . . . . . . . . 16 ⊢ (((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) ∧ ¬ 𝑥 ≤ (𝑁 − 𝑆)) → ((𝑥 + 𝑆) − 𝑁) ≤ (♯‘𝐹))
115	81, 82, 114	3jca 1129	. . . . . . . . . . . . . . 15 ⊢ (((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) ∧ ¬ 𝑥 ≤ (𝑁 − 𝑆)) → (((𝑥 + 𝑆) − 𝑁) ∈ ℕ₀ ∧ (♯‘𝐹) ∈ ℕ₀ ∧ ((𝑥 + 𝑆) − 𝑁) ≤ (♯‘𝐹)))
116	14, 115	sylanl1 681	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (0...𝑁)) ∧ ¬ 𝑥 ≤ (𝑁 − 𝑆)) → (((𝑥 + 𝑆) − 𝑁) ∈ ℕ₀ ∧ (♯‘𝐹) ∈ ℕ₀ ∧ ((𝑥 + 𝑆) − 𝑁) ≤ (♯‘𝐹)))
117		elfz2nn0 13563	. . . . . . . . . . . . . 14 ⊢ (((𝑥 + 𝑆) − 𝑁) ∈ (0...(♯‘𝐹)) ↔ (((𝑥 + 𝑆) − 𝑁) ∈ ℕ₀ ∧ (♯‘𝐹) ∈ ℕ₀ ∧ ((𝑥 + 𝑆) − 𝑁) ≤ (♯‘𝐹)))
118	116, 117	sylibr 234	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (0...𝑁)) ∧ ¬ 𝑥 ≤ (𝑁 − 𝑆)) → ((𝑥 + 𝑆) − 𝑁) ∈ (0...(♯‘𝐹)))
119	118	adantll 715	. . . . . . . . . . . 12 ⊢ (((𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ (𝜑 ∧ 𝑥 ∈ (0...𝑁))) ∧ ¬ 𝑥 ≤ (𝑁 − 𝑆)) → ((𝑥 + 𝑆) − 𝑁) ∈ (0...(♯‘𝐹)))
120	44, 119	ffvelcdmd 7031	. . . . . . . . . . 11 ⊢ (((𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ (𝜑 ∧ 𝑥 ∈ (0...𝑁))) ∧ ¬ 𝑥 ≤ (𝑁 − 𝑆)) → (𝑃‘((𝑥 + 𝑆) − 𝑁)) ∈ 𝑉)
121	43, 120	ifclda 4503	. . . . . . . . . 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 7060	. . . . 5 ⊢ (𝜑 → 𝑄:(0...𝑁)⟶𝑉)
128	11, 4, 2, 21, 14, 1	crctcshlem2 29901	. . . . . . 7 ⊢ (𝜑 → (♯‘𝐻) = 𝑁)
129	128	oveq2d 7376	. . . . . 6 ⊢ (𝜑 → (0...(♯‘𝐻)) = (0...𝑁))
130	129	feq2d 6646	. . . . 5 ⊢ (𝜑 → (𝑄:(0...(♯‘𝐻))⟶𝑉 ↔ 𝑄:(0...𝑁)⟶𝑉))
131	127, 130	mpbird 257	. . . 4 ⊢ (𝜑 → 𝑄:(0...(♯‘𝐻))⟶𝑉)
132	131	adantr 480	. . 3 ⊢ ((𝜑 ∧ 𝑆 ≠ 0) → 𝑄:(0...(♯‘𝐻))⟶𝑉)
133	11, 4	wlkprop 29695	. . . . . 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 2746	. . . . . . . . . 10 ⊢ (♯‘𝐹) = 𝑁
137	136	oveq2i 7371	. . . . . . . . 9 ⊢ (0..^(♯‘𝐹)) = (0..^𝑁)
138	137	raleqi 3294	. . . . . . . 8 ⊢ (∀𝑖 ∈ (0..^(♯‘𝐹))if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖))) ↔ ∀𝑖 ∈ (0..^𝑁)if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖))))
139		fzo1fzo0n0 13661	. . . . . . . . . . . . . . 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 728	. . . . . . . . . . 11 ⊢ ((((𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉) ∧ (𝜑 ∧ 𝑆 ≠ 0)) ∧ ∀𝑖 ∈ (0..^𝑁)if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖)))) → 𝑆 ∈ (1..^𝑁))
144		simplll 775	. . . . . . . . . . 11 ⊢ ((((𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉) ∧ (𝜑 ∧ 𝑆 ≠ 0)) ∧ ∀𝑖 ∈ (0..^𝑁)if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖)))) → 𝐹 ∈ Word dom 𝐼)
145		wkslem1 29691	. . . . . . . . . . . . . 14 ⊢ (𝑖 = 𝑘 → (if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖))) ↔ if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘)))))
146	145	cbvralvw 3216	. . . . . . . . . . . . 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 29875	. . . . . . . . . . . . . 14 ⊢ (𝐹(Circuits‘𝐺)𝑃 → (𝐹(Trails‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))))
150	136	fveq2i 6837	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑃‘(♯‘𝐹)) = (𝑃‘𝑁)
151	150	eqeq2i 2750	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑃‘0) = (𝑃‘(♯‘𝐹)) ↔ (𝑃‘0) = (𝑃‘𝑁))
152	151	biimpi 216	. . . . . . . . . . . . . . . 16 ⊢ ((𝑃‘0) = (𝑃‘(♯‘𝐹)) → (𝑃‘0) = (𝑃‘𝑁))
153	152	eqcomd 2743	. . . . . . . . . . . . . . 15 ⊢ ((𝑃‘0) = (𝑃‘(♯‘𝐹)) → (𝑃‘𝑁) = (𝑃‘0))
154	153	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((𝐹(Trails‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) → (𝑃‘𝑁) = (𝑃‘0))
155	2, 149, 154	3syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑃‘𝑁) = (𝑃‘0))
156	155	ad2antrl 729	. . . . . . . . . . . 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 29899	. . . . . . . . . 10 ⊢ ((((𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉) ∧ (𝜑 ∧ 𝑆 ≠ 0)) ∧ ∀𝑖 ∈ (0..^𝑁)if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖)))) → ∀𝑗 ∈ (0..^𝑁)if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗))))
159	128	oveq2d 7376	. . . . . . . . . . . . 13 ⊢ (𝜑 → (0..^(♯‘𝐻)) = (0..^𝑁))
160	159	raleqdv 3296	. . . . . . . . . . . 12 ⊢ (𝜑 → (∀𝑗 ∈ (0..^(♯‘𝐻))if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗))) ↔ ∀𝑗 ∈ (0..^𝑁)if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗)))))
161	160	ad2antrl 729	. . . . . . . . . . 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 1118	. . . 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 1129	. 2 ⊢ ((𝜑 ∧ 𝑆 ≠ 0) → (𝐻 ∈ Word dom 𝐼 ∧ 𝑄:(0...(♯‘𝐻))⟶𝑉 ∧ ∀𝑗 ∈ (0..^(♯‘𝐻))if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗)))))
171	11, 4, 2, 21, 14, 1, 126	crctcshlem3 29902	. . . 4 ⊢ (𝜑 → (𝐺 ∈ V ∧ 𝐻 ∈ V ∧ 𝑄 ∈ V))
172	171	adantr 480	. . 3 ⊢ ((𝜑 ∧ 𝑆 ≠ 0) → (𝐺 ∈ V ∧ 𝐻 ∈ V ∧ 𝑄 ∈ V))
173	11, 4	iswlk 29694	. . 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 1063 ∧ w3a 1087 = wceq 1542 ∈ wcel 2114 ≠ wne 2933 ∀wral 3052 Vcvv 3430 ⊆ wss 3890 ifcif 4467 {csn 4568 {cpr 4570 class class class wbr 5086 ↦ cmpt 5167 dom cdm 5624 ⟶wf 6488 ‘cfv 6492 (class class class)co 7360 ℝcr 11028 0cc0 11029 1c1 11030 + caddc 11032 < clt 11170 ≤ cle 11171 − cmin 11368 ℕcn 12165 ℕ₀cn0 12428 ℤcz 12515 ...cfz 13452 ..^cfzo 13599 ♯chash 14283 Word cword 14466 cyclShift ccsh 14741 Vtxcvtx 29079 iEdgciedg 29080 Walkscwlks 29680 Trailsctrls 29772 Circuitsccrcts 29867

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-rep 5212 ax-sep 5231 ax-nul 5241 ax-pow 5302 ax-pr 5370 ax-un 7682 ax-cnex 11085 ax-resscn 11086 ax-1cn 11087 ax-icn 11088 ax-addcl 11089 ax-addrcl 11090 ax-mulcl 11091 ax-mulrcl 11092 ax-mulcom 11093 ax-addass 11094 ax-mulass 11095 ax-distr 11096 ax-i2m1 11097 ax-1ne0 11098 ax-1rid 11099 ax-rnegex 11100 ax-rrecex 11101 ax-cnre 11102 ax-pre-lttri 11103 ax-pre-lttrn 11104 ax-pre-ltadd 11105 ax-pre-mulgt0 11106 ax-pre-sup 11107

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-ifp 1064 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3063 df-rmo 3343 df-reu 3344 df-rab 3391 df-v 3432 df-sbc 3730 df-csb 3839 df-dif 3893 df-un 3895 df-in 3897 df-ss 3907 df-pss 3910 df-nul 4275 df-if 4468 df-pw 4544 df-sn 4569 df-pr 4571 df-op 4575 df-uni 4852 df-int 4891 df-iun 4936 df-br 5087 df-opab 5149 df-mpt 5168 df-tr 5194 df-id 5519 df-eprel 5524 df-po 5532 df-so 5533 df-fr 5577 df-we 5579 df-xp 5630 df-rel 5631 df-cnv 5632 df-co 5633 df-dm 5634 df-rn 5635 df-res 5636 df-ima 5637 df-pred 6259 df-ord 6320 df-on 6321 df-lim 6322 df-suc 6323 df-iota 6448 df-fun 6494 df-fn 6495 df-f 6496 df-f1 6497 df-fo 6498 df-f1o 6499 df-fv 6500 df-riota 7317 df-ov 7363 df-oprab 7364 df-mpo 7365 df-om 7811 df-1st 7935 df-2nd 7936 df-frecs 8224 df-wrecs 8255 df-recs 8304 df-rdg 8342 df-1o 8398 df-er 8636 df-map 8768 df-en 8887 df-dom 8888 df-sdom 8889 df-fin 8890 df-sup 9348 df-inf 9349 df-card 9854 df-pnf 11172 df-mnf 11173 df-xr 11174 df-ltxr 11175 df-le 11176 df-sub 11370 df-neg 11371 df-div 11799 df-nn 12166 df-2 12235 df-n0 12429 df-z 12516 df-uz 12780 df-rp 12934 df-fz 13453 df-fzo 13600 df-fl 13742 df-mod 13820 df-hash 14284 df-word 14467 df-concat 14524 df-substr 14595 df-pfx 14625 df-csh 14742 df-wlks 29683 df-trls 29774 df-crcts 29869

This theorem is referenced by: crctcshwlk 29905

W3C validator