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 30416

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 30389	. . . . . 6 ⊢ (𝐹(Circuits‘𝐺)𝑃 → 𝐹(Walks‘𝐺)𝑃)
4		crctcsh.i	. . . . . . 7 ⊢ 𝐼 = (iEdg‘𝐺)
5	4	wlkf 30201	. . . . . 6 ⊢ (𝐹(Walks‘𝐺)𝑃 → 𝐹 ∈ Word dom 𝐼)
6		cshwcl 14954	. . . . . 6 ⊢ (𝐹 ∈ Word dom 𝐼 → (𝐹 cyclShift 𝑆) ∈ Word dom 𝐼)
7	2, 3, 5, 6	4syl 20	. . . . 5 ⊢ (𝜑 → (𝐹 cyclShift 𝑆) ∈ Word dom 𝐼)
8	1, 7	eqeltrid 2864	. . . 4 ⊢ (𝜑 → 𝐻 ∈ Word dom 𝐼)
9	8	adantr 486	. . 3 ⊢ ((𝜑 ∧ 𝑆 ≠ 0) → 𝐻 ∈ Word dom 𝐼)
10	2, 3	syl 18	. . . . . . . 8 ⊢ (𝜑 → 𝐹(Walks‘𝐺)𝑃)
11		crctcsh.v	. . . . . . . . . 10 ⊢ 𝑉 = (Vtx‘𝐺)
12	11	wlkp 30203	. . . . . . . . 9 ⊢ (𝐹(Walks‘𝐺)𝑃 → 𝑃:(0...(♯‘𝐹))⟶𝑉)
13		simpll 779	. . . . . . . . . . . 12 ⊢ (((𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ (𝜑 ∧ 𝑥 ∈ (0...𝑁))) ∧ 𝑥 ≤ (𝑁 − 𝑆)) → 𝑃:(0...(♯‘𝐹))⟶𝑉)
14		crctcsh.s	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑆 ∈ (0..^𝑁))
15		elfznn0 13758	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ (0...𝑁) → 𝑥 ∈ ℕ₀)
16	15	adantl 487	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) → 𝑥 ∈ ℕ₀)
17		elfzonn0 13846	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑆 ∈ (0..^𝑁) → 𝑆 ∈ ℕ₀)
18	17	adantr 486	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) → 𝑆 ∈ ℕ₀)
19	16, 18	nn0addcld 12675	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) → (𝑥 + 𝑆) ∈ ℕ₀)
20	19	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ (((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) ∧ 𝑥 ≤ (𝑁 − 𝑆)) → (𝑥 + 𝑆) ∈ ℕ₀)
21		crctcsh.n	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑁 = (♯‘𝐹)
22		elfz3nn0 13759	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (0...𝑁) → 𝑁 ∈ ℕ₀)
23	21, 22	eqeltrrid 2865	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ (0...𝑁) → (♯‘𝐹) ∈ ℕ₀)
24	23	ad2antlr 740	. . . . . . . . . . . . . . . 16 ⊢ (((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) ∧ 𝑥 ≤ (𝑁 − 𝑆)) → (♯‘𝐹) ∈ ℕ₀)
25		elfzelz 13660	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ (0...𝑁) → 𝑥 ∈ ℤ)
26	25	zred 12807	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ (0...𝑁) → 𝑥 ∈ ℝ)
27	26	adantl 487	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) → 𝑥 ∈ ℝ)
28		elfzoelz 13797	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑆 ∈ (0..^𝑁) → 𝑆 ∈ ℤ)
29	28	zred 12807	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑆 ∈ (0..^𝑁) → 𝑆 ∈ ℝ)
30	29	adantr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) → 𝑆 ∈ ℝ)
31		elfzel2 13658	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ (0...𝑁) → 𝑁 ∈ ℤ)
32	31	zred 12807	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ (0...𝑁) → 𝑁 ∈ ℝ)
33	32	adantl 487	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) → 𝑁 ∈ ℝ)
34		leaddsub 11796	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ ℝ ∧ 𝑆 ∈ ℝ ∧ 𝑁 ∈ ℝ) → ((𝑥 + 𝑆) ≤ 𝑁 ↔ 𝑥 ≤ (𝑁 − 𝑆)))
35	27, 30, 33, 34	syl3anc 1398	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) → ((𝑥 + 𝑆) ≤ 𝑁 ↔ 𝑥 ≤ (𝑁 − 𝑆)))
36	35	biimpar 483	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) ∧ 𝑥 ≤ (𝑁 − 𝑆)) → (𝑥 + 𝑆) ≤ 𝑁)
37	36, 21	breqtrdi 5145	. . . . . . . . . . . . . . . 16 ⊢ (((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) ∧ 𝑥 ≤ (𝑁 − 𝑆)) → (𝑥 + 𝑆) ≤ (♯‘𝐹))
38	20, 24, 37	3jca 1146	. . . . . . . . . . . . . . 15 ⊢ (((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) ∧ 𝑥 ≤ (𝑁 − 𝑆)) → ((𝑥 + 𝑆) ∈ ℕ₀ ∧ (♯‘𝐹) ∈ ℕ₀ ∧ (𝑥 + 𝑆) ≤ (♯‘𝐹)))
39	14, 38	sylanl1 693	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (0...𝑁)) ∧ 𝑥 ≤ (𝑁 − 𝑆)) → ((𝑥 + 𝑆) ∈ ℕ₀ ∧ (♯‘𝐹) ∈ ℕ₀ ∧ (𝑥 + 𝑆) ≤ (♯‘𝐹)))
40		elfz2nn0 13756	. . . . . . . . . . . . . 14 ⊢ ((𝑥 + 𝑆) ∈ (0...(♯‘𝐹)) ↔ ((𝑥 + 𝑆) ∈ ℕ₀ ∧ (♯‘𝐹) ∈ ℕ₀ ∧ (𝑥 + 𝑆) ≤ (♯‘𝐹)))
41	39, 40	sylibr 237	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (0...𝑁)) ∧ 𝑥 ≤ (𝑁 − 𝑆)) → (𝑥 + 𝑆) ∈ (0...(♯‘𝐹)))
42	41	adantll 727	. . . . . . . . . . . 12 ⊢ (((𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ (𝜑 ∧ 𝑥 ∈ (0...𝑁))) ∧ 𝑥 ≤ (𝑁 − 𝑆)) → (𝑥 + 𝑆) ∈ (0...(♯‘𝐹)))
43	13, 42	ffvelcdmd 7086	. . . . . . . . . . 11 ⊢ (((𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ (𝜑 ∧ 𝑥 ∈ (0...𝑁))) ∧ 𝑥 ≤ (𝑁 − 𝑆)) → (𝑃‘(𝑥 + 𝑆)) ∈ 𝑉)
44		simpll 779	. . . . . . . . . . . 12 ⊢ (((𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ (𝜑 ∧ 𝑥 ∈ (0...𝑁))) ∧ ¬ 𝑥 ≤ (𝑁 − 𝑆)) → 𝑃:(0...(♯‘𝐹))⟶𝑉)
45		elfzoel2 13796	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑆 ∈ (0..^𝑁) → 𝑁 ∈ ℤ)
46		zaddcl 12740	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑥 ∈ ℤ ∧ 𝑆 ∈ ℤ) → (𝑥 + 𝑆) ∈ ℤ)
47	46	adantrr 730	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑥 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → (𝑥 + 𝑆) ∈ ℤ)
48		simprr 785	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑥 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → 𝑁 ∈ ℤ)
49	47, 48	zsubcld 12812	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑥 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → ((𝑥 + 𝑆) − 𝑁) ∈ ℤ)
50	49	adantr 486	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑥 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ)) ∧ ¬ 𝑥 ≤ (𝑁 − 𝑆)) → ((𝑥 + 𝑆) − 𝑁) ∈ ℤ)
51		zsubcl 12742	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑁 ∈ ℤ ∧ 𝑆 ∈ ℤ) → (𝑁 − 𝑆) ∈ ℤ)
52	51	ancoms 464	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 − 𝑆) ∈ ℤ)
53	52	zred 12807	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 − 𝑆) ∈ ℝ)
54		zre 12701	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 ∈ ℤ → 𝑥 ∈ ℝ)
55		ltnle 11393	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑁 − 𝑆) ∈ ℝ ∧ 𝑥 ∈ ℝ) → ((𝑁 − 𝑆) < 𝑥 ↔ ¬ 𝑥 ≤ (𝑁 − 𝑆)))
56	53, 54, 55	syl2anr 609	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑥 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → ((𝑁 − 𝑆) < 𝑥 ↔ ¬ 𝑥 ≤ (𝑁 − 𝑆)))
57		zre 12701	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℝ)
58	57	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑁 ∈ ℝ)
59		zre 12701	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑆 ∈ ℤ → 𝑆 ∈ ℝ)
60	59	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑆 ∈ ℝ)
61	54	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑥 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → 𝑥 ∈ ℝ)
62		ltsubadd 11790	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑁 ∈ ℝ ∧ 𝑆 ∈ ℝ ∧ 𝑥 ∈ ℝ) → ((𝑁 − 𝑆) < 𝑥 ↔ 𝑁 < (𝑥 + 𝑆)))
63	58, 60, 61, 62	syl2an23an 1450	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑥 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → ((𝑁 − 𝑆) < 𝑥 ↔ 𝑁 < (𝑥 + 𝑆)))
64	58	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑥 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → 𝑁 ∈ ℝ)
65	47	zred 12807	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑥 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → (𝑥 + 𝑆) ∈ ℝ)
66	64, 65	posdifd 11907	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑥 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → (𝑁 < (𝑥 + 𝑆) ↔ 0 < ((𝑥 + 𝑆) − 𝑁)))
67		0red 11315	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑥 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → 0 ∈ ℝ)
68	49	zred 12807	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑥 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → ((𝑥 + 𝑆) − 𝑁) ∈ ℝ)
69		ltle 11402	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((0 ∈ ℝ ∧ ((𝑥 + 𝑆) − 𝑁) ∈ ℝ) → (0 < ((𝑥 + 𝑆) − 𝑁) → 0 ≤ ((𝑥 + 𝑆) − 𝑁)))
70	67, 68, 69	syl2anc 596	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑥 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → (0 < ((𝑥 + 𝑆) − 𝑁) → 0 ≤ ((𝑥 + 𝑆) − 𝑁)))
71	66, 70	sylbid 243	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑥 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → (𝑁 < (𝑥 + 𝑆) → 0 ≤ ((𝑥 + 𝑆) − 𝑁)))
72	63, 71	sylbid 243	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑥 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → ((𝑁 − 𝑆) < 𝑥 → 0 ≤ ((𝑥 + 𝑆) − 𝑁)))
73	56, 72	sylbird 263	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑥 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → (¬ 𝑥 ≤ (𝑁 − 𝑆) → 0 ≤ ((𝑥 + 𝑆) − 𝑁)))
74	73	imp 412	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑥 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ)) ∧ ¬ 𝑥 ≤ (𝑁 − 𝑆)) → 0 ≤ ((𝑥 + 𝑆) − 𝑁))
75	50, 74	jca 521	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑥 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ)) ∧ ¬ 𝑥 ≤ (𝑁 − 𝑆)) → (((𝑥 + 𝑆) − 𝑁) ∈ ℤ ∧ 0 ≤ ((𝑥 + 𝑆) − 𝑁)))
76	75	exp31 425	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ ℤ → ((𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (¬ 𝑥 ≤ (𝑁 − 𝑆) → (((𝑥 + 𝑆) − 𝑁) ∈ ℤ ∧ 0 ≤ ((𝑥 + 𝑆) − 𝑁)))))
77	76, 25	syl11 34	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑥 ∈ (0...𝑁) → (¬ 𝑥 ≤ (𝑁 − 𝑆) → (((𝑥 + 𝑆) − 𝑁) ∈ ℤ ∧ 0 ≤ ((𝑥 + 𝑆) − 𝑁)))))
78	28, 45, 77	syl2anc 596	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑆 ∈ (0..^𝑁) → (𝑥 ∈ (0...𝑁) → (¬ 𝑥 ≤ (𝑁 − 𝑆) → (((𝑥 + 𝑆) − 𝑁) ∈ ℤ ∧ 0 ≤ ((𝑥 + 𝑆) − 𝑁)))))
79	78	imp31 423	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) ∧ ¬ 𝑥 ≤ (𝑁 − 𝑆)) → (((𝑥 + 𝑆) − 𝑁) ∈ ℤ ∧ 0 ≤ ((𝑥 + 𝑆) − 𝑁)))
80		elnn0z 12710	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑥 + 𝑆) − 𝑁) ∈ ℕ₀ ↔ (((𝑥 + 𝑆) − 𝑁) ∈ ℤ ∧ 0 ≤ ((𝑥 + 𝑆) − 𝑁)))
81	79, 80	sylibr 237	. . . . . . . . . . . . . . . 16 ⊢ (((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) ∧ ¬ 𝑥 ≤ (𝑁 − 𝑆)) → ((𝑥 + 𝑆) − 𝑁) ∈ ℕ₀)
82	23	ad2antlr 740	. . . . . . . . . . . . . . . 16 ⊢ (((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) ∧ ¬ 𝑥 ≤ (𝑁 − 𝑆)) → (♯‘𝐹) ∈ ℕ₀)
83		elfzo0 13839	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑆 ∈ (0..^𝑁) ↔ (𝑆 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁))
84		elfz2nn0 13756	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ (0...𝑁) ↔ (𝑥 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀ ∧ 𝑥 ≤ 𝑁))
85		nn0re 12619	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑆 ∈ ℕ₀ → 𝑆 ∈ ℝ)
86	85	3ad2ant1 1151	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑆 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) → 𝑆 ∈ ℝ)
87		nn0re 12619	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 ∈ ℕ₀ → 𝑥 ∈ ℝ)
88	87	3ad2ant1 1151	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑥 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀ ∧ 𝑥 ≤ 𝑁) → 𝑥 ∈ ℝ)
89	86, 88	anim12ci 626	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑆 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) ∧ (𝑥 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀ ∧ 𝑥 ≤ 𝑁)) → (𝑥 ∈ ℝ ∧ 𝑆 ∈ ℝ))
90		nnre 12346	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℝ)
91	90, 90	jca 521	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑁 ∈ ℕ → (𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ))
92	91	3ad2ant2 1152	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑆 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) → (𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ))
93	92	adantr 486	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑆 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) ∧ (𝑥 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀ ∧ 𝑥 ≤ 𝑁)) → (𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ))
94	89, 93	jca 521	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑆 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) ∧ (𝑥 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀ ∧ 𝑥 ≤ 𝑁)) → ((𝑥 ∈ ℝ ∧ 𝑆 ∈ ℝ) ∧ (𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ)))
95		simpr3 1215	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑆 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) ∧ (𝑥 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀ ∧ 𝑥 ≤ 𝑁)) → 𝑥 ≤ 𝑁)
96		ltle 11402	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑆 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (𝑆 < 𝑁 → 𝑆 ≤ 𝑁))
97	85, 90, 96	syl2an 608	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑆 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ) → (𝑆 < 𝑁 → 𝑆 ≤ 𝑁))
98	97	3impia 1135	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑆 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) → 𝑆 ≤ 𝑁)
99	98	adantr 486	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑆 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) ∧ (𝑥 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀ ∧ 𝑥 ≤ 𝑁)) → 𝑆 ≤ 𝑁)
100	94, 95, 99	jca32 525	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑆 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) ∧ (𝑥 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀ ∧ 𝑥 ≤ 𝑁)) → (((𝑥 ∈ ℝ ∧ 𝑆 ∈ ℝ) ∧ (𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ)) ∧ (𝑥 ≤ 𝑁 ∧ 𝑆 ≤ 𝑁)))
101	83, 84, 100	syl2anb 610	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) → (((𝑥 ∈ ℝ ∧ 𝑆 ∈ ℝ) ∧ (𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ)) ∧ (𝑥 ≤ 𝑁 ∧ 𝑆 ≤ 𝑁)))
102		le2add 11802	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑥 ∈ ℝ ∧ 𝑆 ∈ ℝ) ∧ (𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ)) → ((𝑥 ≤ 𝑁 ∧ 𝑆 ≤ 𝑁) → (𝑥 + 𝑆) ≤ (𝑁 + 𝑁)))
103	102	imp 412	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑥 ∈ ℝ ∧ 𝑆 ∈ ℝ) ∧ (𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ)) ∧ (𝑥 ≤ 𝑁 ∧ 𝑆 ≤ 𝑁)) → (𝑥 + 𝑆) ≤ (𝑁 + 𝑁))
104	101, 103	syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) → (𝑥 + 𝑆) ≤ (𝑁 + 𝑁))
105	65, 64, 64	3jca 1146	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑥 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → ((𝑥 + 𝑆) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ))
106	105	ex 418	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 ∈ ℤ → ((𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑥 + 𝑆) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ)))
107	106, 25	syl11 34	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑥 ∈ (0...𝑁) → ((𝑥 + 𝑆) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ)))
108	28, 45, 107	syl2anc 596	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑆 ∈ (0..^𝑁) → (𝑥 ∈ (0...𝑁) → ((𝑥 + 𝑆) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ)))
109	108	imp 412	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) → ((𝑥 + 𝑆) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ))
110		lesubadd 11792	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑥 + 𝑆) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (((𝑥 + 𝑆) − 𝑁) ≤ 𝑁 ↔ (𝑥 + 𝑆) ≤ (𝑁 + 𝑁)))
111	109, 110	syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) → (((𝑥 + 𝑆) − 𝑁) ≤ 𝑁 ↔ (𝑥 + 𝑆) ≤ (𝑁 + 𝑁)))
112	104, 111	mpbird 260	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) → ((𝑥 + 𝑆) − 𝑁) ≤ 𝑁)
113	112	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) ∧ ¬ 𝑥 ≤ (𝑁 − 𝑆)) → ((𝑥 + 𝑆) − 𝑁) ≤ 𝑁)
114	113, 21	breqtrdi 5145	. . . . . . . . . . . . . . . 16 ⊢ (((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) ∧ ¬ 𝑥 ≤ (𝑁 − 𝑆)) → ((𝑥 + 𝑆) − 𝑁) ≤ (♯‘𝐹))
115	81, 82, 114	3jca 1146	. . . . . . . . . . . . . . 15 ⊢ (((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) ∧ ¬ 𝑥 ≤ (𝑁 − 𝑆)) → (((𝑥 + 𝑆) − 𝑁) ∈ ℕ₀ ∧ (♯‘𝐹) ∈ ℕ₀ ∧ ((𝑥 + 𝑆) − 𝑁) ≤ (♯‘𝐹)))
116	14, 115	sylanl1 693	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (0...𝑁)) ∧ ¬ 𝑥 ≤ (𝑁 − 𝑆)) → (((𝑥 + 𝑆) − 𝑁) ∈ ℕ₀ ∧ (♯‘𝐹) ∈ ℕ₀ ∧ ((𝑥 + 𝑆) − 𝑁) ≤ (♯‘𝐹)))
117		elfz2nn0 13756	. . . . . . . . . . . . . 14 ⊢ (((𝑥 + 𝑆) − 𝑁) ∈ (0...(♯‘𝐹)) ↔ (((𝑥 + 𝑆) − 𝑁) ∈ ℕ₀ ∧ (♯‘𝐹) ∈ ℕ₀ ∧ ((𝑥 + 𝑆) − 𝑁) ≤ (♯‘𝐹)))
118	116, 117	sylibr 237	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (0...𝑁)) ∧ ¬ 𝑥 ≤ (𝑁 − 𝑆)) → ((𝑥 + 𝑆) − 𝑁) ∈ (0...(♯‘𝐹)))
119	118	adantll 727	. . . . . . . . . . . 12 ⊢ (((𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ (𝜑 ∧ 𝑥 ∈ (0...𝑁))) ∧ ¬ 𝑥 ≤ (𝑁 − 𝑆)) → ((𝑥 + 𝑆) − 𝑁) ∈ (0...(♯‘𝐹)))
120	44, 119	ffvelcdmd 7086	. . . . . . . . . . 11 ⊢ (((𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ (𝜑 ∧ 𝑥 ∈ (0...𝑁))) ∧ ¬ 𝑥 ≤ (𝑁 − 𝑆)) → (𝑃‘((𝑥 + 𝑆) − 𝑁)) ∈ 𝑉)
121	43, 120	ifclda 4517	. . . . . . . . . 10 ⊢ ((𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ (𝜑 ∧ 𝑥 ∈ (0...𝑁))) → if(𝑥 ≤ (𝑁 − 𝑆), (𝑃‘(𝑥 + 𝑆)), (𝑃‘((𝑥 + 𝑆) − 𝑁))) ∈ 𝑉)
122	121	exp32 426	. . . . . . . . 9 ⊢ (𝑃:(0...(♯‘𝐹))⟶𝑉 → (𝜑 → (𝑥 ∈ (0...𝑁) → if(𝑥 ≤ (𝑁 − 𝑆), (𝑃‘(𝑥 + 𝑆)), (𝑃‘((𝑥 + 𝑆) − 𝑁))) ∈ 𝑉)))
123	12, 122	syl 18	. . . . . . . 8 ⊢ (𝐹(Walks‘𝐺)𝑃 → (𝜑 → (𝑥 ∈ (0...𝑁) → if(𝑥 ≤ (𝑁 − 𝑆), (𝑃‘(𝑥 + 𝑆)), (𝑃‘((𝑥 + 𝑆) − 𝑁))) ∈ 𝑉)))
124	10, 123	mpcom 39	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ (0...𝑁) → if(𝑥 ≤ (𝑁 − 𝑆), (𝑃‘(𝑥 + 𝑆)), (𝑃‘((𝑥 + 𝑆) − 𝑁))) ∈ 𝑉))
125	124	imp 412	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (0...𝑁)) → if(𝑥 ≤ (𝑁 − 𝑆), (𝑃‘(𝑥 + 𝑆)), (𝑃‘((𝑥 + 𝑆) − 𝑁))) ∈ 𝑉)
126		crctcsh.q	. . . . . 6 ⊢ 𝑄 = (𝑥 ∈ (0...𝑁) ↦ if(𝑥 ≤ (𝑁 − 𝑆), (𝑃‘(𝑥 + 𝑆)), (𝑃‘((𝑥 + 𝑆) − 𝑁))))
127	125, 126	fmptd 7115	. . . . 5 ⊢ (𝜑 → 𝑄:(0...𝑁)⟶𝑉)
128	11, 4, 2, 21, 14, 1	crctcshlem2 30413	. . . . . . 7 ⊢ (𝜑 → (♯‘𝐻) = 𝑁)
129	128	oveq2d 7437	. . . . . 6 ⊢ (𝜑 → (0...(♯‘𝐻)) = (0...𝑁))
130	129	feq2d 6694	. . . . 5 ⊢ (𝜑 → (𝑄:(0...(♯‘𝐻))⟶𝑉 ↔ 𝑄:(0...𝑁)⟶𝑉))
131	127, 130	mpbird 260	. . . 4 ⊢ (𝜑 → 𝑄:(0...(♯‘𝐻))⟶𝑉)
132	131	adantr 486	. . 3 ⊢ ((𝜑 ∧ 𝑆 ≠ 0) → 𝑄:(0...(♯‘𝐻))⟶𝑉)
133	11, 4	wlkprop 30198	. . . . . 6 ⊢ (𝐹(Walks‘𝐺)𝑃 → (𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(♯‘𝐹))if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖)))))
134	2, 3, 133	3syl 19	. . . . 5 ⊢ (𝜑 → (𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(♯‘𝐹))if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖)))))
135	134	adantr 486	. . . 4 ⊢ ((𝜑 ∧ 𝑆 ≠ 0) → (𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(♯‘𝐹))if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖)))))
136	21	eqcomi 2769	. . . . . . . . . 10 ⊢ (♯‘𝐹) = 𝑁
137	136	oveq2i 7432	. . . . . . . . 9 ⊢ (0..^(♯‘𝐹)) = (0..^𝑁)
138	137	raleqi 3317	. . . . . . . 8 ⊢ (∀𝑖 ∈ (0..^(♯‘𝐹))if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖))) ↔ ∀𝑖 ∈ (0..^𝑁)if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖))))
139		fzo1fzo0n0 13854	. . . . . . . . . . . . . . 15 ⊢ (𝑆 ∈ (1..^𝑁) ↔ (𝑆 ∈ (0..^𝑁) ∧ 𝑆 ≠ 0))
140	139	simplbi2 506	. . . . . . . . . . . . . 14 ⊢ (𝑆 ∈ (0..^𝑁) → (𝑆 ≠ 0 → 𝑆 ∈ (1..^𝑁)))
141	14, 140	syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑆 ≠ 0 → 𝑆 ∈ (1..^𝑁)))
142	141	imp 412	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑆 ≠ 0) → 𝑆 ∈ (1..^𝑁))
143	142	ad2antlr 740	. . . . . . . . . . 11 ⊢ ((((𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉) ∧ (𝜑 ∧ 𝑆 ≠ 0)) ∧ ∀𝑖 ∈ (0..^𝑁)if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖)))) → 𝑆 ∈ (1..^𝑁))
144		simplll 787	. . . . . . . . . . 11 ⊢ ((((𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉) ∧ (𝜑 ∧ 𝑆 ≠ 0)) ∧ ∀𝑖 ∈ (0..^𝑁)if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖)))) → 𝐹 ∈ Word dom 𝐼)
145		wkslem1 30194	. . . . . . . . . . . . 13 ⊢ (𝑖 = 𝑘 → (if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖))) ↔ if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘)))))
146	145	cbvralvw 3240	. . . . . . . . . . . 12 ⊢ (∀𝑖 ∈ (0..^𝑁)if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖))) ↔ ∀𝑘 ∈ (0..^𝑁)if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘))))
147	146	bilani 510	. . . . . . . . . . 11 ⊢ ((((𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉) ∧ (𝜑 ∧ 𝑆 ≠ 0)) ∧ ∀𝑖 ∈ (0..^𝑁)if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖)))) → ∀𝑘 ∈ (0..^𝑁)if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘))))
148		crctprop 30385	. . . . . . . . . . . . . 14 ⊢ (𝐹(Circuits‘𝐺)𝑃 → (𝐹(Trails‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))))
149	136	fveq2i 6889	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑃‘(♯‘𝐹)) = (𝑃‘𝑁)
150	149	eqeq2i 2773	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑃‘0) = (𝑃‘(♯‘𝐹)) ↔ (𝑃‘0) = (𝑃‘𝑁))
151	150	biimpi 219	. . . . . . . . . . . . . . . 16 ⊢ ((𝑃‘0) = (𝑃‘(♯‘𝐹)) → (𝑃‘0) = (𝑃‘𝑁))
152	151	eqcomd 2766	. . . . . . . . . . . . . . 15 ⊢ ((𝑃‘0) = (𝑃‘(♯‘𝐹)) → (𝑃‘𝑁) = (𝑃‘0))
153	152	adantl 487	. . . . . . . . . . . . . 14 ⊢ ((𝐹(Trails‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) → (𝑃‘𝑁) = (𝑃‘0))
154	2, 148, 153	3syl 19	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑃‘𝑁) = (𝑃‘0))
155	154	ad2antrl 741	. . . . . . . . . . . 12 ⊢ (((𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉) ∧ (𝜑 ∧ 𝑆 ≠ 0)) → (𝑃‘𝑁) = (𝑃‘0))
156	155	adantr 486	. . . . . . . . . . 11 ⊢ ((((𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉) ∧ (𝜑 ∧ 𝑆 ≠ 0)) ∧ ∀𝑖 ∈ (0..^𝑁)if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖)))) → (𝑃‘𝑁) = (𝑃‘0))
157	143, 126, 1, 21, 144, 147, 156	crctcshwlkn0lem7 30411	. . . . . . . . . 10 ⊢ ((((𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉) ∧ (𝜑 ∧ 𝑆 ≠ 0)) ∧ ∀𝑖 ∈ (0..^𝑁)if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖)))) → ∀𝑗 ∈ (0..^𝑁)if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗))))
158	128	oveq2d 7437	. . . . . . . . . . . . 13 ⊢ (𝜑 → (0..^(♯‘𝐻)) = (0..^𝑁))
159	158	raleqdv 3319	. . . . . . . . . . . 12 ⊢ (𝜑 → (∀𝑗 ∈ (0..^(♯‘𝐻))if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗))) ↔ ∀𝑗 ∈ (0..^𝑁)if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗)))))
160	159	ad2antrl 741	. . . . . . . . . . 11 ⊢ (((𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉) ∧ (𝜑 ∧ 𝑆 ≠ 0)) → (∀𝑗 ∈ (0..^(♯‘𝐻))if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗))) ↔ ∀𝑗 ∈ (0..^𝑁)if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗)))))
161	160	adantr 486	. . . . . . . . . 10 ⊢ ((((𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉) ∧ (𝜑 ∧ 𝑆 ≠ 0)) ∧ ∀𝑖 ∈ (0..^𝑁)if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖)))) → (∀𝑗 ∈ (0..^(♯‘𝐻))if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗))) ↔ ∀𝑗 ∈ (0..^𝑁)if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗)))))
162	157, 161	mpbird 260	. . . . . . . . 9 ⊢ ((((𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉) ∧ (𝜑 ∧ 𝑆 ≠ 0)) ∧ ∀𝑖 ∈ (0..^𝑁)if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖)))) → ∀𝑗 ∈ (0..^(♯‘𝐻))if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗))))
163	162	ex 418	. . . . . . . 8 ⊢ (((𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉) ∧ (𝜑 ∧ 𝑆 ≠ 0)) → (∀𝑖 ∈ (0..^𝑁)if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖))) → ∀𝑗 ∈ (0..^(♯‘𝐻))if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗)))))
164	138, 163	biimtrid 245	. . . . . . 7 ⊢ (((𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉) ∧ (𝜑 ∧ 𝑆 ≠ 0)) → (∀𝑖 ∈ (0..^(♯‘𝐹))if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖))) → ∀𝑗 ∈ (0..^(♯‘𝐻))if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗)))))
165	164	ex 418	. . . . . 6 ⊢ ((𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉) → ((𝜑 ∧ 𝑆 ≠ 0) → (∀𝑖 ∈ (0..^(♯‘𝐹))if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖))) → ∀𝑗 ∈ (0..^(♯‘𝐻))if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗))))))
166	165	com23 87	. . . . 5 ⊢ ((𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉) → (∀𝑖 ∈ (0..^(♯‘𝐹))if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖))) → ((𝜑 ∧ 𝑆 ≠ 0) → ∀𝑗 ∈ (0..^(♯‘𝐻))if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗))))))
167	166	3impia 1135	. . . 4 ⊢ ((𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(♯‘𝐹))if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖)))) → ((𝜑 ∧ 𝑆 ≠ 0) → ∀𝑗 ∈ (0..^(♯‘𝐻))if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗)))))
168	135, 167	mpcom 39	. . 3 ⊢ ((𝜑 ∧ 𝑆 ≠ 0) → ∀𝑗 ∈ (0..^(♯‘𝐻))if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗))))
169	9, 132, 168	3jca 1146	. 2 ⊢ ((𝜑 ∧ 𝑆 ≠ 0) → (𝐻 ∈ Word dom 𝐼 ∧ 𝑄:(0...(♯‘𝐻))⟶𝑉 ∧ ∀𝑗 ∈ (0..^(♯‘𝐻))if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗)))))
170	11, 4, 2, 21, 14, 1, 126	crctcshlem3 30414	. . . 4 ⊢ (𝜑 → (𝐺 ∈ V ∧ 𝐻 ∈ V ∧ 𝑄 ∈ V))
171	170	adantr 486	. . 3 ⊢ ((𝜑 ∧ 𝑆 ≠ 0) → (𝐺 ∈ V ∧ 𝐻 ∈ V ∧ 𝑄 ∈ V))
172	11, 4	iswlk 30197	. . 3 ⊢ ((𝐺 ∈ V ∧ 𝐻 ∈ V ∧ 𝑄 ∈ V) → (𝐻(Walks‘𝐺)𝑄 ↔ (𝐻 ∈ Word dom 𝐼 ∧ 𝑄:(0...(♯‘𝐻))⟶𝑉 ∧ ∀𝑗 ∈ (0..^(♯‘𝐻))if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗))))))
173	171, 172	syl 18	. 2 ⊢ ((𝜑 ∧ 𝑆 ≠ 0) → (𝐻(Walks‘𝐺)𝑄 ↔ (𝐻 ∈ Word dom 𝐼 ∧ 𝑄:(0...(♯‘𝐻))⟶𝑉 ∧ ∀𝑗 ∈ (0..^(♯‘𝐻))if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗))))))
174	169, 173	mpbird 260	1 ⊢ ((𝜑 ∧ 𝑆 ≠ 0) → 𝐻(Walks‘𝐺)𝑄)

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 401 if-wif 1078 ∧ w3a 1103 = wceq 1569 ∈ wcel 2144 ≠ wne 2955 ∀wral 3076 Vcvv 3450 ⊆ wss 3895 ifcif 4481 {csn 4584 {cpr 4586 class class class wbr 5102 ↦ cmpt 5185 dom cdm 5650 ⟶wf 6535 ‘cfv 6539 (class class class)co 7421 ℝcr 11203 0cc0 11204 1c1 11205 + caddc 11207 < clt 11347 ≤ cle 11348 − cmin 11545 ℕcn 12339 ℕ₀cn0 12610 ℤcz 12697 ...cfz 13643 ..^cfzo 13792 ♯chash 14478 Word cword 14662 cyclShift ccsh 14944 Vtxcvtx 29580 iEdgciedg 29581 Walkscwlks 30183 Trailsctrls 30279 Circuitsccrcts 30377

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1942 ax-6 1999 ax-7 2040 ax-8 2146 ax-9 2154 ax-10 2177 ax-11 2193 ax-12 2212 ax-ext 2732 ax-rep 5231 ax-sep 5248 ax-nul 5259 ax-pow 5326 ax-pr 5390 ax-un 7752 ax-cnex 11260 ax-resscn 11261 ax-1cn 11262 ax-icn 11263 ax-addcl 11264 ax-addrcl 11265 ax-mulcl 11266 ax-mulrcl 11267 ax-mulcom 11268 ax-addass 11269 ax-mulass 11270 ax-distr 11271 ax-i2m1 11272 ax-1ne0 11273 ax-1rid 11274 ax-rnegex 11275 ax-rrecex 11276 ax-cnre 11277 ax-pre-lttri 11278 ax-pre-lttrn 11279 ax-pre-ltadd 11280 ax-pre-mulgt0 11281 ax-pre-sup 11282

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-ifp 1079 df-3or 1104 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-nf 1816 df-sb 2099 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-nel 3062 df-ral 3077 df-rex 3087 df-rmo 3365 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3739 df-csb 3847 df-ss 3896 df-pss 4014 df-dif 4047 df-in 4091 df-un 4151 df-nul 4279 df-if 4482 df-pw 4558 df-sn 4585 df-pr 4587 df-op 4835 df-uni 4867 df-int 4907 df-iun 4952 df-br 5103 df-opab 5167 df-mpt 5186 df-tr 5212 df-id 5545 df-eprel 5550 df-po 5558 df-so 5559 df-fr 5603 df-we 5605 df-xp 5656 df-rel 5657 df-cnv 5658 df-co 5659 df-dm 5660 df-rn 5661 df-res 5662 df-ima 5663 df-pred 6304 df-ord 6365 df-on 6366 df-lim 6367 df-suc 6368 df-iota 6494 df-fun 6541 df-fn 6542 df-f 6543 df-f1 6544 df-fo 6545 df-f1o 6546 df-fv 6547 df-riota 7378 df-ov 7424 df-oprab 7425 df-mpo 7426 df-om 7879 df-1st 8002 df-2nd 8003 df-frecs 8303 df-wrecs 8334 df-recs 8383 df-rdg 8422 df-1o 8480 df-er 8721 df-map 8853 df-en 8978 df-dom 8979 df-sdom 8980 df-fin 8981 df-sup 9438 df-inf 9439 df-card 10024 df-pnf 11349 df-mnf 11350 df-xr 11351 df-ltxr 11352 df-le 11353 df-sub 11547 df-neg 11548 df-div 11978 df-nn 12340 df-2 12409 df-n0 12611 df-z 12698 df-uz 12970 df-rp 13125 df-fz 13644 df-fzo 13793 df-fl 13936 df-mod 14014 df-hash 14479 df-word 14663 df-concat 14720 df-substr 14794 df-pfx 14826 df-csh 14945 df-wlks 30186 df-trls 30281 df-crcts 30379

This theorem is used by: crctcshwlk 30417

W3C validator