Users' Mathboxes Mathbox for Alexander van der Vekens < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  clwlksfclwwlk Structured version   Visualization version   GIF version

Theorem clwlksfclwwlk 41267
Description: There is a function between the set of closed walks (defined as words) of length n and the set of closed walks of length n. (Contributed by Alexander van der Vekens, 25-Jun-2018.) (Revised by AV, 2-May-2021.)
Hypotheses
Ref Expression
clwlksfclwwlk.1 𝐴 = (1st𝑐)
clwlksfclwwlk.2 𝐵 = (2nd𝑐)
clwlksfclwwlk.c 𝐶 = {𝑐 ∈ (ClWalkS‘𝐺) ∣ (#‘𝐴) = 𝑁}
clwlksfclwwlk.f 𝐹 = (𝑐𝐶 ↦ (𝐵 substr ⟨0, (#‘𝐴)⟩))
Assertion
Ref Expression
clwlksfclwwlk ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → 𝐹:𝐶⟶(𝑁 ClWWalkSN 𝐺))
Distinct variable groups:   𝐺,𝑐   𝑁,𝑐   𝐶,𝑐
Allowed substitution hints:   𝐴(𝑐)   𝐵(𝑐)   𝐹(𝑐)

Proof of Theorem clwlksfclwwlk
Dummy variables 𝑖 𝑥 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 clwlksfclwwlk.c . . . . . 6 𝐶 = {𝑐 ∈ (ClWalkS‘𝐺) ∣ (#‘𝐴) = 𝑁}
21rabeq2i 3165 . . . . 5 (𝑐𝐶 ↔ (𝑐 ∈ (ClWalkS‘𝐺) ∧ (#‘𝐴) = 𝑁))
3 fusgrusgr 40539 . . . . . . . . . . . 12 (𝐺 ∈ FinUSGraph → 𝐺 ∈ USGraph )
4 usgrupgr 40410 . . . . . . . . . . . 12 (𝐺 ∈ USGraph → 𝐺 ∈ UPGraph )
53, 4syl 17 . . . . . . . . . . 11 (𝐺 ∈ FinUSGraph → 𝐺 ∈ UPGraph )
65adantr 479 . . . . . . . . . 10 ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → 𝐺 ∈ UPGraph )
7 eqid 2605 . . . . . . . . . . 11 (Vtx‘𝐺) = (Vtx‘𝐺)
8 eqid 2605 . . . . . . . . . . 11 (iEdg‘𝐺) = (iEdg‘𝐺)
9 clwlksfclwwlk.1 . . . . . . . . . . 11 𝐴 = (1st𝑐)
10 clwlksfclwwlk.2 . . . . . . . . . . 11 𝐵 = (2nd𝑐)
117, 8, 9, 10upgrclwlkcompim 40986 . . . . . . . . . 10 ((𝐺 ∈ UPGraph ∧ 𝑐 ∈ (ClWalkS‘𝐺)) → ((𝐴 ∈ Word dom (iEdg‘𝐺) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ ∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴))))
126, 11sylan 486 . . . . . . . . 9 (((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) ∧ 𝑐 ∈ (ClWalkS‘𝐺)) → ((𝐴 ∈ Word dom (iEdg‘𝐺) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ ∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴))))
13 lencl 13121 . . . . . . . . . . . . . . 15 (𝐴 ∈ Word dom (iEdg‘𝐺) → (#‘𝐴) ∈ ℕ0)
14 clwlksfclwwlk.f . . . . . . . . . . . . . . . . . . . . . . . . 25 𝐹 = (𝑐𝐶 ↦ (𝐵 substr ⟨0, (#‘𝐴)⟩))
159, 10, 1, 14clwlksfclwwlk2wrd 41263 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑐𝐶𝐵 ∈ Word (Vtx‘𝐺))
1615ad2antlr 758 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((((#‘𝐴) ∈ ℕ0𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → 𝐵 ∈ Word (Vtx‘𝐺))
17 swrdcl 13213 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐵 ∈ Word (Vtx‘𝐺) → (𝐵 substr ⟨0, (#‘𝐴)⟩) ∈ Word (Vtx‘𝐺))
1816, 17syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((((((((#‘𝐴) ∈ ℕ0𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → (𝐵 substr ⟨0, (#‘𝐴)⟩) ∈ Word (Vtx‘𝐺))
19 ffz0iswrd 13129 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺) → 𝐵 ∈ Word (Vtx‘𝐺))
20193ad2ant1 1074 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺) ∧ (#‘𝐴) = 𝑁 ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → 𝐵 ∈ Word (Vtx‘𝐺))
21 prmnn 15168 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑁 ∈ ℙ → 𝑁 ∈ ℕ)
2221adantl 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → 𝑁 ∈ ℕ)
23223ad2ant3 1076 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺) ∧ (#‘𝐴) = 𝑁 ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → 𝑁 ∈ ℕ)
24 oveq2 6531 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((#‘𝐴) = 𝑁 → (0...(#‘𝐴)) = (0...𝑁))
2524feq2d 5926 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((#‘𝐴) = 𝑁 → (𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺) ↔ 𝐵:(0...𝑁)⟶(Vtx‘𝐺)))
2622nnnn0d 11194 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → 𝑁 ∈ ℕ0)
27 ffz0hash 13036 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑁 ∈ ℕ0𝐵:(0...𝑁)⟶(Vtx‘𝐺)) → (#‘𝐵) = (𝑁 + 1))
2826, 27sylan 486 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) ∧ 𝐵:(0...𝑁)⟶(Vtx‘𝐺)) → (#‘𝐵) = (𝑁 + 1))
2928ex 448 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (𝐵:(0...𝑁)⟶(Vtx‘𝐺) → (#‘𝐵) = (𝑁 + 1)))
3021nnred 10878 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑁 ∈ ℙ → 𝑁 ∈ ℝ)
3130adantr 479 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑁 ∈ ℙ ∧ (#‘𝐵) = (𝑁 + 1)) → 𝑁 ∈ ℝ)
3231lep1d 10800 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑁 ∈ ℙ ∧ (#‘𝐵) = (𝑁 + 1)) → 𝑁 ≤ (𝑁 + 1))
33 breq2 4577 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((#‘𝐵) = (𝑁 + 1) → (𝑁 ≤ (#‘𝐵) ↔ 𝑁 ≤ (𝑁 + 1)))
3433adantl 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑁 ∈ ℙ ∧ (#‘𝐵) = (𝑁 + 1)) → (𝑁 ≤ (#‘𝐵) ↔ 𝑁 ≤ (𝑁 + 1)))
3532, 34mpbird 245 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑁 ∈ ℙ ∧ (#‘𝐵) = (𝑁 + 1)) → 𝑁 ≤ (#‘𝐵))
3635ex 448 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑁 ∈ ℙ → ((#‘𝐵) = (𝑁 + 1) → 𝑁 ≤ (#‘𝐵)))
3736adantl 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → ((#‘𝐵) = (𝑁 + 1) → 𝑁 ≤ (#‘𝐵)))
3829, 37syld 45 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (𝐵:(0...𝑁)⟶(Vtx‘𝐺) → 𝑁 ≤ (#‘𝐵)))
3938com12 32 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝐵:(0...𝑁)⟶(Vtx‘𝐺) → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → 𝑁 ≤ (#‘𝐵)))
4025, 39syl6bi 241 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((#‘𝐴) = 𝑁 → (𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺) → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → 𝑁 ≤ (#‘𝐵))))
41403imp21 1268 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺) ∧ (#‘𝐴) = 𝑁 ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → 𝑁 ≤ (#‘𝐵))
42 swrdn0 13224 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ ℕ ∧ 𝑁 ≤ (#‘𝐵)) → (𝐵 substr ⟨0, 𝑁⟩) ≠ ∅)
4320, 23, 41, 42syl3anc 1317 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺) ∧ (#‘𝐴) = 𝑁 ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → (𝐵 substr ⟨0, 𝑁⟩) ≠ ∅)
44 opeq2 4331 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((#‘𝐴) = 𝑁 → ⟨0, (#‘𝐴)⟩ = ⟨0, 𝑁⟩)
4544oveq2d 6539 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((#‘𝐴) = 𝑁 → (𝐵 substr ⟨0, (#‘𝐴)⟩) = (𝐵 substr ⟨0, 𝑁⟩))
4645neeq1d 2836 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((#‘𝐴) = 𝑁 → ((𝐵 substr ⟨0, (#‘𝐴)⟩) ≠ ∅ ↔ (𝐵 substr ⟨0, 𝑁⟩) ≠ ∅))
47463ad2ant2 1075 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺) ∧ (#‘𝐴) = 𝑁 ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → ((𝐵 substr ⟨0, (#‘𝐴)⟩) ≠ ∅ ↔ (𝐵 substr ⟨0, 𝑁⟩) ≠ ∅))
4843, 47mpbird 245 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺) ∧ (#‘𝐴) = 𝑁 ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → (𝐵 substr ⟨0, (#‘𝐴)⟩) ≠ ∅)
49483exp 1255 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺) → ((#‘𝐴) = 𝑁 → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (𝐵 substr ⟨0, (#‘𝐴)⟩) ≠ ∅)))
5049ad2antlr 758 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((#‘𝐴) ∈ ℕ0𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) → ((#‘𝐴) = 𝑁 → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (𝐵 substr ⟨0, (#‘𝐴)⟩) ≠ ∅)))
5150imp 443 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((#‘𝐴) ∈ ℕ0𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (𝐵 substr ⟨0, (#‘𝐴)⟩) ≠ ∅))
5251adantr 479 . . . . . . . . . . . . . . . . . . . . . . 23 (((((((#‘𝐴) ∈ ℕ0𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐𝐶) → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (𝐵 substr ⟨0, (#‘𝐴)⟩) ≠ ∅))
5352imp 443 . . . . . . . . . . . . . . . . . . . . . 22 ((((((((#‘𝐴) ∈ ℕ0𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → (𝐵 substr ⟨0, (#‘𝐴)⟩) ≠ ∅)
5418, 53jca 552 . . . . . . . . . . . . . . . . . . . . 21 ((((((((#‘𝐴) ∈ ℕ0𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → ((𝐵 substr ⟨0, (#‘𝐴)⟩) ∈ Word (Vtx‘𝐺) ∧ (𝐵 substr ⟨0, (#‘𝐴)⟩) ≠ ∅))
55 simp-5r 804 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((((#‘𝐴) ∈ ℕ0𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐𝐶) → 𝐴 ∈ Word dom (iEdg‘𝐺))
563adantr 479 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → 𝐺 ∈ USGraph )
5755, 56anim12ci 588 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((((#‘𝐴) ∈ ℕ0𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → (𝐺 ∈ USGraph ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)))
58 simp-5r 804 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((((#‘𝐴) ∈ ℕ0𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺))
59 prmuz2 15188 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑁 ∈ ℙ → 𝑁 ∈ (ℤ‘2))
60 ffz0hash 13036 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((#‘𝐴) ∈ ℕ0𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) → (#‘𝐵) = ((#‘𝐴) + 1))
6160adantlr 746 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((#‘𝐴) ∈ ℕ0𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) → (#‘𝐵) = ((#‘𝐴) + 1))
62 eluz2 11521 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((#‘𝐴) ∈ (ℤ‘2) ↔ (2 ∈ ℤ ∧ (#‘𝐴) ∈ ℤ ∧ 2 ≤ (#‘𝐴)))
63 2re 10933 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 2 ∈ ℝ
6463a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((#‘𝐴) ∈ ℤ → 2 ∈ ℝ)
65 zre 11210 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((#‘𝐴) ∈ ℤ → (#‘𝐴) ∈ ℝ)
66 peano2re 10056 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((#‘𝐴) ∈ ℝ → ((#‘𝐴) + 1) ∈ ℝ)
6765, 66syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((#‘𝐴) ∈ ℤ → ((#‘𝐴) + 1) ∈ ℝ)
6864, 65, 673jca 1234 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((#‘𝐴) ∈ ℤ → (2 ∈ ℝ ∧ (#‘𝐴) ∈ ℝ ∧ ((#‘𝐴) + 1) ∈ ℝ))
6968adantr 479 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((#‘𝐴) ∈ ℤ ∧ 2 ≤ (#‘𝐴)) → (2 ∈ ℝ ∧ (#‘𝐴) ∈ ℝ ∧ ((#‘𝐴) + 1) ∈ ℝ))
70 simpr 475 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((#‘𝐴) ∈ ℤ ∧ 2 ≤ (#‘𝐴)) → 2 ≤ (#‘𝐴))
7165lep1d 10800 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((#‘𝐴) ∈ ℤ → (#‘𝐴) ≤ ((#‘𝐴) + 1))
7271adantr 479 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((#‘𝐴) ∈ ℤ ∧ 2 ≤ (#‘𝐴)) → (#‘𝐴) ≤ ((#‘𝐴) + 1))
73 letr 9978 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((2 ∈ ℝ ∧ (#‘𝐴) ∈ ℝ ∧ ((#‘𝐴) + 1) ∈ ℝ) → ((2 ≤ (#‘𝐴) ∧ (#‘𝐴) ≤ ((#‘𝐴) + 1)) → 2 ≤ ((#‘𝐴) + 1)))
7473imp 443 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((2 ∈ ℝ ∧ (#‘𝐴) ∈ ℝ ∧ ((#‘𝐴) + 1) ∈ ℝ) ∧ (2 ≤ (#‘𝐴) ∧ (#‘𝐴) ≤ ((#‘𝐴) + 1))) → 2 ≤ ((#‘𝐴) + 1))
7569, 70, 72, 74syl12anc 1315 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((#‘𝐴) ∈ ℤ ∧ 2 ≤ (#‘𝐴)) → 2 ≤ ((#‘𝐴) + 1))
76753adant1 1071 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((2 ∈ ℤ ∧ (#‘𝐴) ∈ ℤ ∧ 2 ≤ (#‘𝐴)) → 2 ≤ ((#‘𝐴) + 1))
7762, 76sylbi 205 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((#‘𝐴) ∈ (ℤ‘2) → 2 ≤ ((#‘𝐴) + 1))
7877a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((#‘𝐵) = ((#‘𝐴) + 1) ∧ (#‘𝐴) = 𝑁) → ((#‘𝐴) ∈ (ℤ‘2) → 2 ≤ ((#‘𝐴) + 1)))
79 eleq1 2671 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑁 = (#‘𝐴) → (𝑁 ∈ (ℤ‘2) ↔ (#‘𝐴) ∈ (ℤ‘2)))
8079eqcoms 2613 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((#‘𝐴) = 𝑁 → (𝑁 ∈ (ℤ‘2) ↔ (#‘𝐴) ∈ (ℤ‘2)))
8180adantl 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((#‘𝐵) = ((#‘𝐴) + 1) ∧ (#‘𝐴) = 𝑁) → (𝑁 ∈ (ℤ‘2) ↔ (#‘𝐴) ∈ (ℤ‘2)))
82 breq2 4577 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((#‘𝐵) = ((#‘𝐴) + 1) → (2 ≤ (#‘𝐵) ↔ 2 ≤ ((#‘𝐴) + 1)))
8382adantr 479 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((#‘𝐵) = ((#‘𝐴) + 1) ∧ (#‘𝐴) = 𝑁) → (2 ≤ (#‘𝐵) ↔ 2 ≤ ((#‘𝐴) + 1)))
8478, 81, 833imtr4d 281 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((#‘𝐵) = ((#‘𝐴) + 1) ∧ (#‘𝐴) = 𝑁) → (𝑁 ∈ (ℤ‘2) → 2 ≤ (#‘𝐵)))
8584ex 448 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((#‘𝐵) = ((#‘𝐴) + 1) → ((#‘𝐴) = 𝑁 → (𝑁 ∈ (ℤ‘2) → 2 ≤ (#‘𝐵))))
8661, 85syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((#‘𝐴) ∈ ℕ0𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) → ((#‘𝐴) = 𝑁 → (𝑁 ∈ (ℤ‘2) → 2 ≤ (#‘𝐵))))
8786adantr 479 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((#‘𝐴) ∈ ℕ0𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) → ((#‘𝐴) = 𝑁 → (𝑁 ∈ (ℤ‘2) → 2 ≤ (#‘𝐵))))
8887imp 443 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((#‘𝐴) ∈ ℕ0𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) → (𝑁 ∈ (ℤ‘2) → 2 ≤ (#‘𝐵)))
8988adantr 479 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((((#‘𝐴) ∈ ℕ0𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐𝐶) → (𝑁 ∈ (ℤ‘2) → 2 ≤ (#‘𝐵)))
9059, 89syl5com 31 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑁 ∈ ℙ → (((((((#‘𝐴) ∈ ℕ0𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐𝐶) → 2 ≤ (#‘𝐵)))
9190adantl 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (((((((#‘𝐴) ∈ ℕ0𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐𝐶) → 2 ≤ (#‘𝐵)))
9291impcom 444 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((((#‘𝐴) ∈ ℕ0𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → 2 ≤ (#‘𝐵))
93 simp-4r 802 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((((#‘𝐴) ∈ ℕ0𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴))))
947, 8usgrf 40383 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝐺 ∈ USGraph → (iEdg‘𝐺):dom (iEdg‘𝐺)–1-1→{𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣ (#‘𝑥) = 2})
9594anim1i 589 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐺 ∈ USGraph ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) → ((iEdg‘𝐺):dom (iEdg‘𝐺)–1-1→{𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣ (#‘𝑥) = 2} ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)))
96 clwlkclwwlklem2 41207 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((iEdg‘𝐺):dom (iEdg‘𝐺)–1-1→{𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣ (#‘𝑥) = 2} ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ (𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺) ∧ 2 ≤ (#‘𝐵)) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) → (( lastS ‘𝐵) = (𝐵‘0) ∧ ∀𝑖 ∈ (0..^((#‘𝐴) − 1)){(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∈ ran (iEdg‘𝐺) ∧ {(𝐵‘((#‘𝐴) − 1)), (𝐵‘0)} ∈ ran (iEdg‘𝐺)))
9795, 96syl3an1 1350 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝐺 ∈ USGraph ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ (𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺) ∧ 2 ≤ (#‘𝐵)) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) → (( lastS ‘𝐵) = (𝐵‘0) ∧ ∀𝑖 ∈ (0..^((#‘𝐴) − 1)){(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∈ ran (iEdg‘𝐺) ∧ {(𝐵‘((#‘𝐴) − 1)), (𝐵‘0)} ∈ ran (iEdg‘𝐺)))
98 edgaval 40351 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝐺 ∈ USGraph → (Edg‘𝐺) = ran (iEdg‘𝐺))
9998eleq2d 2668 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝐺 ∈ USGraph → ({(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∈ ran (iEdg‘𝐺)))
10099ralbidv 2964 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝐺 ∈ USGraph → (∀𝑖 ∈ (0..^((#‘𝐴) − 1)){(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ (0..^((#‘𝐴) − 1)){(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∈ ran (iEdg‘𝐺)))
10198eleq2d 2668 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝐺 ∈ USGraph → ({(𝐵‘((#‘𝐴) − 1)), (𝐵‘0)} ∈ (Edg‘𝐺) ↔ {(𝐵‘((#‘𝐴) − 1)), (𝐵‘0)} ∈ ran (iEdg‘𝐺)))
102100, 1013anbi23d 1393 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝐺 ∈ USGraph → ((( lastS ‘𝐵) = (𝐵‘0) ∧ ∀𝑖 ∈ (0..^((#‘𝐴) − 1)){(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(𝐵‘((#‘𝐴) − 1)), (𝐵‘0)} ∈ (Edg‘𝐺)) ↔ (( lastS ‘𝐵) = (𝐵‘0) ∧ ∀𝑖 ∈ (0..^((#‘𝐴) − 1)){(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∈ ran (iEdg‘𝐺) ∧ {(𝐵‘((#‘𝐴) − 1)), (𝐵‘0)} ∈ ran (iEdg‘𝐺))))
103102adantr 479 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐺 ∈ USGraph ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) → ((( lastS ‘𝐵) = (𝐵‘0) ∧ ∀𝑖 ∈ (0..^((#‘𝐴) − 1)){(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(𝐵‘((#‘𝐴) − 1)), (𝐵‘0)} ∈ (Edg‘𝐺)) ↔ (( lastS ‘𝐵) = (𝐵‘0) ∧ ∀𝑖 ∈ (0..^((#‘𝐴) − 1)){(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∈ ran (iEdg‘𝐺) ∧ {(𝐵‘((#‘𝐴) − 1)), (𝐵‘0)} ∈ ran (iEdg‘𝐺))))
1041033ad2ant1 1074 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝐺 ∈ USGraph ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ (𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺) ∧ 2 ≤ (#‘𝐵)) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) → ((( lastS ‘𝐵) = (𝐵‘0) ∧ ∀𝑖 ∈ (0..^((#‘𝐴) − 1)){(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(𝐵‘((#‘𝐴) − 1)), (𝐵‘0)} ∈ (Edg‘𝐺)) ↔ (( lastS ‘𝐵) = (𝐵‘0) ∧ ∀𝑖 ∈ (0..^((#‘𝐴) − 1)){(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∈ ran (iEdg‘𝐺) ∧ {(𝐵‘((#‘𝐴) − 1)), (𝐵‘0)} ∈ ran (iEdg‘𝐺))))
10597, 104mpbird 245 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝐺 ∈ USGraph ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ (𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺) ∧ 2 ≤ (#‘𝐵)) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) → (( lastS ‘𝐵) = (𝐵‘0) ∧ ∀𝑖 ∈ (0..^((#‘𝐴) − 1)){(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(𝐵‘((#‘𝐴) − 1)), (𝐵‘0)} ∈ (Edg‘𝐺)))
10657, 58, 92, 93, 105syl121anc 1322 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((((#‘𝐴) ∈ ℕ0𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → (( lastS ‘𝐵) = (𝐵‘0) ∧ ∀𝑖 ∈ (0..^((#‘𝐴) − 1)){(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(𝐵‘((#‘𝐴) − 1)), (𝐵‘0)} ∈ (Edg‘𝐺)))
1079, 10, 1, 14clwlksfclwwlk1hash 41265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑐𝐶 → (#‘𝐴) ∈ (0...(#‘𝐵)))
108 simp2 1054 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((#‘𝐴) ∈ (0...(#‘𝐵)) ∧ 𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝑖 ∈ (0..^((#‘𝐴) − 1))) → 𝐵 ∈ Word (Vtx‘𝐺))
109 simp1 1053 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((#‘𝐴) ∈ (0...(#‘𝐵)) ∧ 𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝑖 ∈ (0..^((#‘𝐴) − 1))) → (#‘𝐴) ∈ (0...(#‘𝐵)))
110 elfzelz 12164 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((#‘𝐴) ∈ (0...(#‘𝐵)) → (#‘𝐴) ∈ ℤ)
111 peano2zm 11249 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((#‘𝐴) ∈ ℤ → ((#‘𝐴) − 1) ∈ ℤ)
112 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((#‘𝐴) ∈ ℤ → (#‘𝐴) ∈ ℤ)
11365lem1d 10802 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((#‘𝐴) ∈ ℤ → ((#‘𝐴) − 1) ≤ (#‘𝐴))
114 eluz2 11521 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((#‘𝐴) ∈ (ℤ‘((#‘𝐴) − 1)) ↔ (((#‘𝐴) − 1) ∈ ℤ ∧ (#‘𝐴) ∈ ℤ ∧ ((#‘𝐴) − 1) ≤ (#‘𝐴)))
115111, 112, 113, 114syl3anbrc 1238 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((#‘𝐴) ∈ ℤ → (#‘𝐴) ∈ (ℤ‘((#‘𝐴) − 1)))
116 fzoss2 12316 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((#‘𝐴) ∈ (ℤ‘((#‘𝐴) − 1)) → (0..^((#‘𝐴) − 1)) ⊆ (0..^(#‘𝐴)))
117110, 115, 1163syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((#‘𝐴) ∈ (0...(#‘𝐵)) → (0..^((#‘𝐴) − 1)) ⊆ (0..^(#‘𝐴)))
118117sselda 3563 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((#‘𝐴) ∈ (0...(#‘𝐵)) ∧ 𝑖 ∈ (0..^((#‘𝐴) − 1))) → 𝑖 ∈ (0..^(#‘𝐴)))
1191183adant2 1072 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((#‘𝐴) ∈ (0...(#‘𝐵)) ∧ 𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝑖 ∈ (0..^((#‘𝐴) − 1))) → 𝑖 ∈ (0..^(#‘𝐴)))
120 swrd0fv 13233 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝐵 ∈ Word (Vtx‘𝐺) ∧ (#‘𝐴) ∈ (0...(#‘𝐵)) ∧ 𝑖 ∈ (0..^(#‘𝐴))) → ((𝐵 substr ⟨0, (#‘𝐴)⟩)‘𝑖) = (𝐵𝑖))
121108, 109, 119, 120syl3anc 1317 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((#‘𝐴) ∈ (0...(#‘𝐵)) ∧ 𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝑖 ∈ (0..^((#‘𝐴) − 1))) → ((𝐵 substr ⟨0, (#‘𝐴)⟩)‘𝑖) = (𝐵𝑖))
122121eqcomd 2611 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((#‘𝐴) ∈ (0...(#‘𝐵)) ∧ 𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝑖 ∈ (0..^((#‘𝐴) − 1))) → (𝐵𝑖) = ((𝐵 substr ⟨0, (#‘𝐴)⟩)‘𝑖))
123 elfzom1elp1fzo 12353 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((#‘𝐴) ∈ ℤ ∧ 𝑖 ∈ (0..^((#‘𝐴) − 1))) → (𝑖 + 1) ∈ (0..^(#‘𝐴)))
124110, 123sylan 486 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((#‘𝐴) ∈ (0...(#‘𝐵)) ∧ 𝑖 ∈ (0..^((#‘𝐴) − 1))) → (𝑖 + 1) ∈ (0..^(#‘𝐴)))
1251243adant2 1072 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((#‘𝐴) ∈ (0...(#‘𝐵)) ∧ 𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝑖 ∈ (0..^((#‘𝐴) − 1))) → (𝑖 + 1) ∈ (0..^(#‘𝐴)))
126 swrd0fv 13233 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝐵 ∈ Word (Vtx‘𝐺) ∧ (#‘𝐴) ∈ (0...(#‘𝐵)) ∧ (𝑖 + 1) ∈ (0..^(#‘𝐴))) → ((𝐵 substr ⟨0, (#‘𝐴)⟩)‘(𝑖 + 1)) = (𝐵‘(𝑖 + 1)))
127126eqcomd 2611 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝐵 ∈ Word (Vtx‘𝐺) ∧ (#‘𝐴) ∈ (0...(#‘𝐵)) ∧ (𝑖 + 1) ∈ (0..^(#‘𝐴))) → (𝐵‘(𝑖 + 1)) = ((𝐵 substr ⟨0, (#‘𝐴)⟩)‘(𝑖 + 1)))
128108, 109, 125, 127syl3anc 1317 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((#‘𝐴) ∈ (0...(#‘𝐵)) ∧ 𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝑖 ∈ (0..^((#‘𝐴) − 1))) → (𝐵‘(𝑖 + 1)) = ((𝐵 substr ⟨0, (#‘𝐴)⟩)‘(𝑖 + 1)))
129122, 128preq12d 4215 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((#‘𝐴) ∈ (0...(#‘𝐵)) ∧ 𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝑖 ∈ (0..^((#‘𝐴) − 1))) → {(𝐵𝑖), (𝐵‘(𝑖 + 1))} = {((𝐵 substr ⟨0, (#‘𝐴)⟩)‘𝑖), ((𝐵 substr ⟨0, (#‘𝐴)⟩)‘(𝑖 + 1))})
1301293exp 1255 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((#‘𝐴) ∈ (0...(#‘𝐵)) → (𝐵 ∈ Word (Vtx‘𝐺) → (𝑖 ∈ (0..^((#‘𝐴) − 1)) → {(𝐵𝑖), (𝐵‘(𝑖 + 1))} = {((𝐵 substr ⟨0, (#‘𝐴)⟩)‘𝑖), ((𝐵 substr ⟨0, (#‘𝐴)⟩)‘(𝑖 + 1))})))
131107, 15, 130sylc 62 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑐𝐶 → (𝑖 ∈ (0..^((#‘𝐴) − 1)) → {(𝐵𝑖), (𝐵‘(𝑖 + 1))} = {((𝐵 substr ⟨0, (#‘𝐴)⟩)‘𝑖), ((𝐵 substr ⟨0, (#‘𝐴)⟩)‘(𝑖 + 1))}))
132131imp 443 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑐𝐶𝑖 ∈ (0..^((#‘𝐴) − 1))) → {(𝐵𝑖), (𝐵‘(𝑖 + 1))} = {((𝐵 substr ⟨0, (#‘𝐴)⟩)‘𝑖), ((𝐵 substr ⟨0, (#‘𝐴)⟩)‘(𝑖 + 1))})
133132eleq1d 2667 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑐𝐶𝑖 ∈ (0..^((#‘𝐴) − 1))) → ({(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ {((𝐵 substr ⟨0, (#‘𝐴)⟩)‘𝑖), ((𝐵 substr ⟨0, (#‘𝐴)⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
134133ralbidva 2963 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑐𝐶 → (∀𝑖 ∈ (0..^((#‘𝐴) − 1)){(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ (0..^((#‘𝐴) − 1)){((𝐵 substr ⟨0, (#‘𝐴)⟩)‘𝑖), ((𝐵 substr ⟨0, (#‘𝐴)⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
135134ad2antlr 758 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((((#‘𝐴) ∈ ℕ0𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → (∀𝑖 ∈ (0..^((#‘𝐴) − 1)){(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ (0..^((#‘𝐴) − 1)){((𝐵 substr ⟨0, (#‘𝐴)⟩)‘𝑖), ((𝐵 substr ⟨0, (#‘𝐴)⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
1369, 10, 1, 14clwlksfclwwlk2sswd 41266 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑐𝐶 → (#‘𝐴) = (#‘(𝐵 substr ⟨0, (#‘𝐴)⟩)))
137136oveq1d 6538 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑐𝐶 → ((#‘𝐴) − 1) = ((#‘(𝐵 substr ⟨0, (#‘𝐴)⟩)) − 1))
138137ad2antlr 758 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((((#‘𝐴) ∈ ℕ0𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → ((#‘𝐴) − 1) = ((#‘(𝐵 substr ⟨0, (#‘𝐴)⟩)) − 1))
139138oveq2d 6539 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((((#‘𝐴) ∈ ℕ0𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → (0..^((#‘𝐴) − 1)) = (0..^((#‘(𝐵 substr ⟨0, (#‘𝐴)⟩)) − 1)))
140139raleqdv 3116 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((((#‘𝐴) ∈ ℕ0𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → (∀𝑖 ∈ (0..^((#‘𝐴) − 1)){((𝐵 substr ⟨0, (#‘𝐴)⟩)‘𝑖), ((𝐵 substr ⟨0, (#‘𝐴)⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ (0..^((#‘(𝐵 substr ⟨0, (#‘𝐴)⟩)) − 1)){((𝐵 substr ⟨0, (#‘𝐴)⟩)‘𝑖), ((𝐵 substr ⟨0, (#‘𝐴)⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
141135, 140bitrd 266 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((((#‘𝐴) ∈ ℕ0𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → (∀𝑖 ∈ (0..^((#‘𝐴) − 1)){(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ (0..^((#‘(𝐵 substr ⟨0, (#‘𝐴)⟩)) − 1)){((𝐵 substr ⟨0, (#‘𝐴)⟩)‘𝑖), ((𝐵 substr ⟨0, (#‘𝐴)⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
142 eleq1 2671 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑁 = (#‘𝐴) → (𝑁 ∈ ℙ ↔ (#‘𝐴) ∈ ℙ))
143142biimpd 217 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑁 = (#‘𝐴) → (𝑁 ∈ ℙ → (#‘𝐴) ∈ ℙ))
144143eqcoms 2613 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((#‘𝐴) = 𝑁 → (𝑁 ∈ ℙ → (#‘𝐴) ∈ ℙ))
145 prmnn 15168 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((#‘𝐴) ∈ ℙ → (#‘𝐴) ∈ ℕ)
146 elfz2nn0 12251 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((#‘𝐴) ∈ (0...(#‘𝐵)) ↔ ((#‘𝐴) ∈ ℕ0 ∧ (#‘𝐵) ∈ ℕ0 ∧ (#‘𝐴) ≤ (#‘𝐵)))
147 1zzd 11237 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (((#‘𝐴) ∈ ℕ0 ∧ (#‘𝐵) ∈ ℕ0) → 1 ∈ ℤ)
148 nn0z 11229 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ((#‘𝐵) ∈ ℕ0 → (#‘𝐵) ∈ ℤ)
149148adantl 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (((#‘𝐴) ∈ ℕ0 ∧ (#‘𝐵) ∈ ℕ0) → (#‘𝐵) ∈ ℤ)
150 nn0z 11229 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ((#‘𝐴) ∈ ℕ0 → (#‘𝐴) ∈ ℤ)
151150adantr 479 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (((#‘𝐴) ∈ ℕ0 ∧ (#‘𝐵) ∈ ℕ0) → (#‘𝐴) ∈ ℤ)
152147, 149, 1513jca 1234 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (((#‘𝐴) ∈ ℕ0 ∧ (#‘𝐵) ∈ ℕ0) → (1 ∈ ℤ ∧ (#‘𝐵) ∈ ℤ ∧ (#‘𝐴) ∈ ℤ))
1531523adant3 1073 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (((#‘𝐴) ∈ ℕ0 ∧ (#‘𝐵) ∈ ℕ0 ∧ (#‘𝐴) ≤ (#‘𝐵)) → (1 ∈ ℤ ∧ (#‘𝐵) ∈ ℤ ∧ (#‘𝐴) ∈ ℤ))
154153adantr 479 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((((#‘𝐴) ∈ ℕ0 ∧ (#‘𝐵) ∈ ℕ0 ∧ (#‘𝐴) ≤ (#‘𝐵)) ∧ (#‘𝐴) ∈ ℕ) → (1 ∈ ℤ ∧ (#‘𝐵) ∈ ℤ ∧ (#‘𝐴) ∈ ℤ))
155 simp3 1055 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (((#‘𝐴) ∈ ℕ0 ∧ (#‘𝐵) ∈ ℕ0 ∧ (#‘𝐴) ≤ (#‘𝐵)) → (#‘𝐴) ≤ (#‘𝐵))
156 nnge1 10889 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((#‘𝐴) ∈ ℕ → 1 ≤ (#‘𝐴))
157155, 156anim12ci 588 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((((#‘𝐴) ∈ ℕ0 ∧ (#‘𝐵) ∈ ℕ0 ∧ (#‘𝐴) ≤ (#‘𝐵)) ∧ (#‘𝐴) ∈ ℕ) → (1 ≤ (#‘𝐴) ∧ (#‘𝐴) ≤ (#‘𝐵)))
158154, 157jca 552 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((((#‘𝐴) ∈ ℕ0 ∧ (#‘𝐵) ∈ ℕ0 ∧ (#‘𝐴) ≤ (#‘𝐵)) ∧ (#‘𝐴) ∈ ℕ) → ((1 ∈ ℤ ∧ (#‘𝐵) ∈ ℤ ∧ (#‘𝐴) ∈ ℤ) ∧ (1 ≤ (#‘𝐴) ∧ (#‘𝐴) ≤ (#‘𝐵))))
159146, 158sylanb 487 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (((#‘𝐴) ∈ (0...(#‘𝐵)) ∧ (#‘𝐴) ∈ ℕ) → ((1 ∈ ℤ ∧ (#‘𝐵) ∈ ℤ ∧ (#‘𝐴) ∈ ℤ) ∧ (1 ≤ (#‘𝐴) ∧ (#‘𝐴) ≤ (#‘𝐵))))
160 elfz2 12155 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((#‘𝐴) ∈ (1...(#‘𝐵)) ↔ ((1 ∈ ℤ ∧ (#‘𝐵) ∈ ℤ ∧ (#‘𝐴) ∈ ℤ) ∧ (1 ≤ (#‘𝐴) ∧ (#‘𝐴) ≤ (#‘𝐵))))
161159, 160sylibr 222 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((#‘𝐴) ∈ (0...(#‘𝐵)) ∧ (#‘𝐴) ∈ ℕ) → (#‘𝐴) ∈ (1...(#‘𝐵)))
162 swrd0fvlsw 13237 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝐵 ∈ Word (Vtx‘𝐺) ∧ (#‘𝐴) ∈ (1...(#‘𝐵))) → ( lastS ‘(𝐵 substr ⟨0, (#‘𝐴)⟩)) = (𝐵‘((#‘𝐴) − 1)))
163162eqcomd 2611 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝐵 ∈ Word (Vtx‘𝐺) ∧ (#‘𝐴) ∈ (1...(#‘𝐵))) → (𝐵‘((#‘𝐴) − 1)) = ( lastS ‘(𝐵 substr ⟨0, (#‘𝐴)⟩)))
164 swrd0fv0 13234 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝐵 ∈ Word (Vtx‘𝐺) ∧ (#‘𝐴) ∈ (1...(#‘𝐵))) → ((𝐵 substr ⟨0, (#‘𝐴)⟩)‘0) = (𝐵‘0))
165164eqcomd 2611 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝐵 ∈ Word (Vtx‘𝐺) ∧ (#‘𝐴) ∈ (1...(#‘𝐵))) → (𝐵‘0) = ((𝐵 substr ⟨0, (#‘𝐴)⟩)‘0))
166163, 165preq12d 4215 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝐵 ∈ Word (Vtx‘𝐺) ∧ (#‘𝐴) ∈ (1...(#‘𝐵))) → {(𝐵‘((#‘𝐴) − 1)), (𝐵‘0)} = {( lastS ‘(𝐵 substr ⟨0, (#‘𝐴)⟩)), ((𝐵 substr ⟨0, (#‘𝐴)⟩)‘0)})
167166expcom 449 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((#‘𝐴) ∈ (1...(#‘𝐵)) → (𝐵 ∈ Word (Vtx‘𝐺) → {(𝐵‘((#‘𝐴) − 1)), (𝐵‘0)} = {( lastS ‘(𝐵 substr ⟨0, (#‘𝐴)⟩)), ((𝐵 substr ⟨0, (#‘𝐴)⟩)‘0)}))
168161, 167syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((#‘𝐴) ∈ (0...(#‘𝐵)) ∧ (#‘𝐴) ∈ ℕ) → (𝐵 ∈ Word (Vtx‘𝐺) → {(𝐵‘((#‘𝐴) − 1)), (𝐵‘0)} = {( lastS ‘(𝐵 substr ⟨0, (#‘𝐴)⟩)), ((𝐵 substr ⟨0, (#‘𝐴)⟩)‘0)}))
169168ex 448 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((#‘𝐴) ∈ (0...(#‘𝐵)) → ((#‘𝐴) ∈ ℕ → (𝐵 ∈ Word (Vtx‘𝐺) → {(𝐵‘((#‘𝐴) − 1)), (𝐵‘0)} = {( lastS ‘(𝐵 substr ⟨0, (#‘𝐴)⟩)), ((𝐵 substr ⟨0, (#‘𝐴)⟩)‘0)})))
170169com23 83 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((#‘𝐴) ∈ (0...(#‘𝐵)) → (𝐵 ∈ Word (Vtx‘𝐺) → ((#‘𝐴) ∈ ℕ → {(𝐵‘((#‘𝐴) − 1)), (𝐵‘0)} = {( lastS ‘(𝐵 substr ⟨0, (#‘𝐴)⟩)), ((𝐵 substr ⟨0, (#‘𝐴)⟩)‘0)})))
171107, 15, 170sylc 62 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑐𝐶 → ((#‘𝐴) ∈ ℕ → {(𝐵‘((#‘𝐴) − 1)), (𝐵‘0)} = {( lastS ‘(𝐵 substr ⟨0, (#‘𝐴)⟩)), ((𝐵 substr ⟨0, (#‘𝐴)⟩)‘0)}))
172145, 171syl5com 31 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((#‘𝐴) ∈ ℙ → (𝑐𝐶 → {(𝐵‘((#‘𝐴) − 1)), (𝐵‘0)} = {( lastS ‘(𝐵 substr ⟨0, (#‘𝐴)⟩)), ((𝐵 substr ⟨0, (#‘𝐴)⟩)‘0)}))
173144, 172syl6 34 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((#‘𝐴) = 𝑁 → (𝑁 ∈ ℙ → (𝑐𝐶 → {(𝐵‘((#‘𝐴) − 1)), (𝐵‘0)} = {( lastS ‘(𝐵 substr ⟨0, (#‘𝐴)⟩)), ((𝐵 substr ⟨0, (#‘𝐴)⟩)‘0)})))
174173com23 83 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((#‘𝐴) = 𝑁 → (𝑐𝐶 → (𝑁 ∈ ℙ → {(𝐵‘((#‘𝐴) − 1)), (𝐵‘0)} = {( lastS ‘(𝐵 substr ⟨0, (#‘𝐴)⟩)), ((𝐵 substr ⟨0, (#‘𝐴)⟩)‘0)})))
175174adantl 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((((#‘𝐴) ∈ ℕ0𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) → (𝑐𝐶 → (𝑁 ∈ ℙ → {(𝐵‘((#‘𝐴) − 1)), (𝐵‘0)} = {( lastS ‘(𝐵 substr ⟨0, (#‘𝐴)⟩)), ((𝐵 substr ⟨0, (#‘𝐴)⟩)‘0)})))
176175imp 443 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((((#‘𝐴) ∈ ℕ0𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐𝐶) → (𝑁 ∈ ℙ → {(𝐵‘((#‘𝐴) − 1)), (𝐵‘0)} = {( lastS ‘(𝐵 substr ⟨0, (#‘𝐴)⟩)), ((𝐵 substr ⟨0, (#‘𝐴)⟩)‘0)}))
177176com12 32 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑁 ∈ ℙ → (((((((#‘𝐴) ∈ ℕ0𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐𝐶) → {(𝐵‘((#‘𝐴) − 1)), (𝐵‘0)} = {( lastS ‘(𝐵 substr ⟨0, (#‘𝐴)⟩)), ((𝐵 substr ⟨0, (#‘𝐴)⟩)‘0)}))
178177adantl 480 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (((((((#‘𝐴) ∈ ℕ0𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐𝐶) → {(𝐵‘((#‘𝐴) − 1)), (𝐵‘0)} = {( lastS ‘(𝐵 substr ⟨0, (#‘𝐴)⟩)), ((𝐵 substr ⟨0, (#‘𝐴)⟩)‘0)}))
179178impcom 444 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((((#‘𝐴) ∈ ℕ0𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → {(𝐵‘((#‘𝐴) − 1)), (𝐵‘0)} = {( lastS ‘(𝐵 substr ⟨0, (#‘𝐴)⟩)), ((𝐵 substr ⟨0, (#‘𝐴)⟩)‘0)})
180179eleq1d 2667 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((((#‘𝐴) ∈ ℕ0𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → ({(𝐵‘((#‘𝐴) − 1)), (𝐵‘0)} ∈ (Edg‘𝐺) ↔ {( lastS ‘(𝐵 substr ⟨0, (#‘𝐴)⟩)), ((𝐵 substr ⟨0, (#‘𝐴)⟩)‘0)} ∈ (Edg‘𝐺)))
181141, 1803anbi23d 1393 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((((#‘𝐴) ∈ ℕ0𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → ((( lastS ‘𝐵) = (𝐵‘0) ∧ ∀𝑖 ∈ (0..^((#‘𝐴) − 1)){(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(𝐵‘((#‘𝐴) − 1)), (𝐵‘0)} ∈ (Edg‘𝐺)) ↔ (( lastS ‘𝐵) = (𝐵‘0) ∧ ∀𝑖 ∈ (0..^((#‘(𝐵 substr ⟨0, (#‘𝐴)⟩)) − 1)){((𝐵 substr ⟨0, (#‘𝐴)⟩)‘𝑖), ((𝐵 substr ⟨0, (#‘𝐴)⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘(𝐵 substr ⟨0, (#‘𝐴)⟩)), ((𝐵 substr ⟨0, (#‘𝐴)⟩)‘0)} ∈ (Edg‘𝐺))))
182106, 181mpbid 220 . . . . . . . . . . . . . . . . . . . . . 22 ((((((((#‘𝐴) ∈ ℕ0𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → (( lastS ‘𝐵) = (𝐵‘0) ∧ ∀𝑖 ∈ (0..^((#‘(𝐵 substr ⟨0, (#‘𝐴)⟩)) − 1)){((𝐵 substr ⟨0, (#‘𝐴)⟩)‘𝑖), ((𝐵 substr ⟨0, (#‘𝐴)⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘(𝐵 substr ⟨0, (#‘𝐴)⟩)), ((𝐵 substr ⟨0, (#‘𝐴)⟩)‘0)} ∈ (Edg‘𝐺)))
183 3simpc 1052 . . . . . . . . . . . . . . . . . . . . . 22 ((( lastS ‘𝐵) = (𝐵‘0) ∧ ∀𝑖 ∈ (0..^((#‘(𝐵 substr ⟨0, (#‘𝐴)⟩)) − 1)){((𝐵 substr ⟨0, (#‘𝐴)⟩)‘𝑖), ((𝐵 substr ⟨0, (#‘𝐴)⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘(𝐵 substr ⟨0, (#‘𝐴)⟩)), ((𝐵 substr ⟨0, (#‘𝐴)⟩)‘0)} ∈ (Edg‘𝐺)) → (∀𝑖 ∈ (0..^((#‘(𝐵 substr ⟨0, (#‘𝐴)⟩)) − 1)){((𝐵 substr ⟨0, (#‘𝐴)⟩)‘𝑖), ((𝐵 substr ⟨0, (#‘𝐴)⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘(𝐵 substr ⟨0, (#‘𝐴)⟩)), ((𝐵 substr ⟨0, (#‘𝐴)⟩)‘0)} ∈ (Edg‘𝐺)))
184182, 183syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((((((((#‘𝐴) ∈ ℕ0𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → (∀𝑖 ∈ (0..^((#‘(𝐵 substr ⟨0, (#‘𝐴)⟩)) − 1)){((𝐵 substr ⟨0, (#‘𝐴)⟩)‘𝑖), ((𝐵 substr ⟨0, (#‘𝐴)⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘(𝐵 substr ⟨0, (#‘𝐴)⟩)), ((𝐵 substr ⟨0, (#‘𝐴)⟩)‘0)} ∈ (Edg‘𝐺)))
185 3anass 1034 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐵 substr ⟨0, (#‘𝐴)⟩) ∈ Word (Vtx‘𝐺) ∧ (𝐵 substr ⟨0, (#‘𝐴)⟩) ≠ ∅) ∧ ∀𝑖 ∈ (0..^((#‘(𝐵 substr ⟨0, (#‘𝐴)⟩)) − 1)){((𝐵 substr ⟨0, (#‘𝐴)⟩)‘𝑖), ((𝐵 substr ⟨0, (#‘𝐴)⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘(𝐵 substr ⟨0, (#‘𝐴)⟩)), ((𝐵 substr ⟨0, (#‘𝐴)⟩)‘0)} ∈ (Edg‘𝐺)) ↔ (((𝐵 substr ⟨0, (#‘𝐴)⟩) ∈ Word (Vtx‘𝐺) ∧ (𝐵 substr ⟨0, (#‘𝐴)⟩) ≠ ∅) ∧ (∀𝑖 ∈ (0..^((#‘(𝐵 substr ⟨0, (#‘𝐴)⟩)) − 1)){((𝐵 substr ⟨0, (#‘𝐴)⟩)‘𝑖), ((𝐵 substr ⟨0, (#‘𝐴)⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘(𝐵 substr ⟨0, (#‘𝐴)⟩)), ((𝐵 substr ⟨0, (#‘𝐴)⟩)‘0)} ∈ (Edg‘𝐺))))
18654, 184, 185sylanbrc 694 . . . . . . . . . . . . . . . . . . . 20 ((((((((#‘𝐴) ∈ ℕ0𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → (((𝐵 substr ⟨0, (#‘𝐴)⟩) ∈ Word (Vtx‘𝐺) ∧ (𝐵 substr ⟨0, (#‘𝐴)⟩) ≠ ∅) ∧ ∀𝑖 ∈ (0..^((#‘(𝐵 substr ⟨0, (#‘𝐴)⟩)) − 1)){((𝐵 substr ⟨0, (#‘𝐴)⟩)‘𝑖), ((𝐵 substr ⟨0, (#‘𝐴)⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘(𝐵 substr ⟨0, (#‘𝐴)⟩)), ((𝐵 substr ⟨0, (#‘𝐴)⟩)‘0)} ∈ (Edg‘𝐺)))
187 eqid 2605 . . . . . . . . . . . . . . . . . . . . 21 (Edg‘𝐺) = (Edg‘𝐺)
1887, 187isclwwlks 41186 . . . . . . . . . . . . . . . . . . . 20 ((𝐵 substr ⟨0, (#‘𝐴)⟩) ∈ (ClWWalkS‘𝐺) ↔ (((𝐵 substr ⟨0, (#‘𝐴)⟩) ∈ Word (Vtx‘𝐺) ∧ (𝐵 substr ⟨0, (#‘𝐴)⟩) ≠ ∅) ∧ ∀𝑖 ∈ (0..^((#‘(𝐵 substr ⟨0, (#‘𝐴)⟩)) − 1)){((𝐵 substr ⟨0, (#‘𝐴)⟩)‘𝑖), ((𝐵 substr ⟨0, (#‘𝐴)⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘(𝐵 substr ⟨0, (#‘𝐴)⟩)), ((𝐵 substr ⟨0, (#‘𝐴)⟩)‘0)} ∈ (Edg‘𝐺)))
189186, 188sylibr 222 . . . . . . . . . . . . . . . . . . 19 ((((((((#‘𝐴) ∈ ℕ0𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → (𝐵 substr ⟨0, (#‘𝐴)⟩) ∈ (ClWWalkS‘𝐺))
190136eqeq1d 2607 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑐𝐶 → ((#‘𝐴) = 𝑁 ↔ (#‘(𝐵 substr ⟨0, (#‘𝐴)⟩)) = 𝑁))
191190biimpcd 237 . . . . . . . . . . . . . . . . . . . . . 22 ((#‘𝐴) = 𝑁 → (𝑐𝐶 → (#‘(𝐵 substr ⟨0, (#‘𝐴)⟩)) = 𝑁))
192191adantl 480 . . . . . . . . . . . . . . . . . . . . 21 ((((((#‘𝐴) ∈ ℕ0𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) → (𝑐𝐶 → (#‘(𝐵 substr ⟨0, (#‘𝐴)⟩)) = 𝑁))
193192imp 443 . . . . . . . . . . . . . . . . . . . 20 (((((((#‘𝐴) ∈ ℕ0𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐𝐶) → (#‘(𝐵 substr ⟨0, (#‘𝐴)⟩)) = 𝑁)
194193adantr 479 . . . . . . . . . . . . . . . . . . 19 ((((((((#‘𝐴) ∈ ℕ0𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → (#‘(𝐵 substr ⟨0, (#‘𝐴)⟩)) = 𝑁)
195189, 194jca 552 . . . . . . . . . . . . . . . . . 18 ((((((((#‘𝐴) ∈ ℕ0𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → ((𝐵 substr ⟨0, (#‘𝐴)⟩) ∈ (ClWWalkS‘𝐺) ∧ (#‘(𝐵 substr ⟨0, (#‘𝐴)⟩)) = 𝑁))
19622adantl 480 . . . . . . . . . . . . . . . . . . 19 ((((((((#‘𝐴) ∈ ℕ0𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → 𝑁 ∈ ℕ)
197 isclwwlksn 41188 . . . . . . . . . . . . . . . . . . 19 (𝑁 ∈ ℕ → ((𝐵 substr ⟨0, (#‘𝐴)⟩) ∈ (𝑁 ClWWalkSN 𝐺) ↔ ((𝐵 substr ⟨0, (#‘𝐴)⟩) ∈ (ClWWalkS‘𝐺) ∧ (#‘(𝐵 substr ⟨0, (#‘𝐴)⟩)) = 𝑁)))
198196, 197syl 17 . . . . . . . . . . . . . . . . . 18 ((((((((#‘𝐴) ∈ ℕ0𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → ((𝐵 substr ⟨0, (#‘𝐴)⟩) ∈ (𝑁 ClWWalkSN 𝐺) ↔ ((𝐵 substr ⟨0, (#‘𝐴)⟩) ∈ (ClWWalkS‘𝐺) ∧ (#‘(𝐵 substr ⟨0, (#‘𝐴)⟩)) = 𝑁)))
199195, 198mpbird 245 . . . . . . . . . . . . . . . . 17 ((((((((#‘𝐴) ∈ ℕ0𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → (𝐵 substr ⟨0, (#‘𝐴)⟩) ∈ (𝑁 ClWWalkSN 𝐺))
200199exp31 627 . . . . . . . . . . . . . . . 16 ((((((#‘𝐴) ∈ ℕ0𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) → (𝑐𝐶 → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (𝐵 substr ⟨0, (#‘𝐴)⟩) ∈ (𝑁 ClWWalkSN 𝐺))))
201200exp41 635 . . . . . . . . . . . . . . 15 (((#‘𝐴) ∈ ℕ0𝐴 ∈ Word dom (iEdg‘𝐺)) → (𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺) → ((∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴))) → ((#‘𝐴) = 𝑁 → (𝑐𝐶 → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (𝐵 substr ⟨0, (#‘𝐴)⟩) ∈ (𝑁 ClWWalkSN 𝐺)))))))
20213, 201mpancom 699 . . . . . . . . . . . . . 14 (𝐴 ∈ Word dom (iEdg‘𝐺) → (𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺) → ((∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴))) → ((#‘𝐴) = 𝑁 → (𝑐𝐶 → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (𝐵 substr ⟨0, (#‘𝐴)⟩) ∈ (𝑁 ClWWalkSN 𝐺)))))))
203202imp 443 . . . . . . . . . . . . 13 ((𝐴 ∈ Word dom (iEdg‘𝐺) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) → ((∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴))) → ((#‘𝐴) = 𝑁 → (𝑐𝐶 → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (𝐵 substr ⟨0, (#‘𝐴)⟩) ∈ (𝑁 ClWWalkSN 𝐺))))))
2042033impib 1253 . . . . . . . . . . . 12 (((𝐴 ∈ Word dom (iEdg‘𝐺) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ ∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴))) → ((#‘𝐴) = 𝑁 → (𝑐𝐶 → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (𝐵 substr ⟨0, (#‘𝐴)⟩) ∈ (𝑁 ClWWalkSN 𝐺)))))
205204com12 32 . . . . . . . . . . 11 ((#‘𝐴) = 𝑁 → (((𝐴 ∈ Word dom (iEdg‘𝐺) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ ∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴))) → (𝑐𝐶 → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (𝐵 substr ⟨0, (#‘𝐴)⟩) ∈ (𝑁 ClWWalkSN 𝐺)))))
206205com14 93 . . . . . . . . . 10 ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (((𝐴 ∈ Word dom (iEdg‘𝐺) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ ∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴))) → (𝑐𝐶 → ((#‘𝐴) = 𝑁 → (𝐵 substr ⟨0, (#‘𝐴)⟩) ∈ (𝑁 ClWWalkSN 𝐺)))))
207206adantr 479 . . . . . . . . 9 (((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) ∧ 𝑐 ∈ (ClWalkS‘𝐺)) → (((𝐴 ∈ Word dom (iEdg‘𝐺) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ ∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴))) → (𝑐𝐶 → ((#‘𝐴) = 𝑁 → (𝐵 substr ⟨0, (#‘𝐴)⟩) ∈ (𝑁 ClWWalkSN 𝐺)))))
20812, 207mpd 15 . . . . . . . 8 (((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) ∧ 𝑐 ∈ (ClWalkS‘𝐺)) → (𝑐𝐶 → ((#‘𝐴) = 𝑁 → (𝐵 substr ⟨0, (#‘𝐴)⟩) ∈ (𝑁 ClWWalkSN 𝐺))))
209208expcom 449 . . . . . . 7 (𝑐 ∈ (ClWalkS‘𝐺) → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (𝑐𝐶 → ((#‘𝐴) = 𝑁 → (𝐵 substr ⟨0, (#‘𝐴)⟩) ∈ (𝑁 ClWWalkSN 𝐺)))))
210209com24 92 . . . . . 6 (𝑐 ∈ (ClWalkS‘𝐺) → ((#‘𝐴) = 𝑁 → (𝑐𝐶 → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (𝐵 substr ⟨0, (#‘𝐴)⟩) ∈ (𝑁 ClWWalkSN 𝐺)))))
211210imp 443 . . . . 5 ((𝑐 ∈ (ClWalkS‘𝐺) ∧ (#‘𝐴) = 𝑁) → (𝑐𝐶 → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (𝐵 substr ⟨0, (#‘𝐴)⟩) ∈ (𝑁 ClWWalkSN 𝐺))))
2122, 211sylbi 205 . . . 4 (𝑐𝐶 → (𝑐𝐶 → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (𝐵 substr ⟨0, (#‘𝐴)⟩) ∈ (𝑁 ClWWalkSN 𝐺))))
213212pm2.43i 49 . . 3 (𝑐𝐶 → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (𝐵 substr ⟨0, (#‘𝐴)⟩) ∈ (𝑁 ClWWalkSN 𝐺)))
214213impcom 444 . 2 (((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) ∧ 𝑐𝐶) → (𝐵 substr ⟨0, (#‘𝐴)⟩) ∈ (𝑁 ClWWalkSN 𝐺))
215214, 14fmptd 6273 1 ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → 𝐹:𝐶⟶(𝑁 ClWWalkSN 𝐺))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wa 382  w3a 1030   = wceq 1474  wcel 1975  wne 2775  wral 2891  {crab 2895  cdif 3532  wss 3535  c0 3869  𝒫 cpw 4103  {csn 4120  {cpr 4122  cop 4126   class class class wbr 4573  cmpt 4633  dom cdm 5024  ran crn 5025  wf 5782  1-1wf1 5783  cfv 5786  (class class class)co 6523  1st c1st 7030  2nd c2nd 7031  cr 9787  0cc0 9788  1c1 9789   + caddc 9791  cle 9927  cmin 10113  cn 10863  2c2 10913  0cn0 11135  cz 11206  cuz 11515  ...cfz 12148  ..^cfzo 12285  #chash 12930  Word cword 13088   lastS clsw 13089   substr csubstr 13092  cprime 15165  Vtxcvtx 40227  iEdgciedg 40228   UPGraph cupgr 40304  Edgcedga 40349   USGraph cusgr 40377   FinUSGraph cfusgr 40533  ClWalkScclwlks 40974  ClWWalkScclwwlks 41181   ClWWalkSN cclwwlksn 41182
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-6 1873  ax-7 1920  ax-8 1977  ax-9 1984  ax-10 2004  ax-11 2019  ax-12 2031  ax-13 2228  ax-ext 2585  ax-rep 4689  ax-sep 4699  ax-nul 4708  ax-pow 4760  ax-pr 4824  ax-un 6820  ax-cnex 9844  ax-resscn 9845  ax-1cn 9846  ax-icn 9847  ax-addcl 9848  ax-addrcl 9849  ax-mulcl 9850  ax-mulrcl 9851  ax-mulcom 9852  ax-addass 9853  ax-mulass 9854  ax-distr 9855  ax-i2m1 9856  ax-1ne0 9857  ax-1rid 9858  ax-rnegex 9859  ax-rrecex 9860  ax-cnre 9861  ax-pre-lttri 9862  ax-pre-lttrn 9863  ax-pre-ltadd 9864  ax-pre-mulgt0 9865  ax-pre-sup 9866
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-ifp 1006  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1866  df-eu 2457  df-mo 2458  df-clab 2592  df-cleq 2598  df-clel 2601  df-nfc 2735  df-ne 2777  df-nel 2778  df-ral 2896  df-rex 2897  df-reu 2898  df-rmo 2899  df-rab 2900  df-v 3170  df-sbc 3398  df-csb 3495  df-dif 3538  df-un 3540  df-in 3542  df-ss 3549  df-pss 3551  df-nul 3870  df-if 4032  df-pw 4105  df-sn 4121  df-pr 4123  df-tp 4125  df-op 4127  df-uni 4363  df-int 4401  df-iun 4447  df-br 4574  df-opab 4634  df-mpt 4635  df-tr 4671  df-eprel 4935  df-id 4939  df-po 4945  df-so 4946  df-fr 4983  df-we 4985  df-xp 5030  df-rel 5031  df-cnv 5032  df-co 5033  df-dm 5034  df-rn 5035  df-res 5036  df-ima 5037  df-pred 5579  df-ord 5625  df-on 5626  df-lim 5627  df-suc 5628  df-iota 5750  df-fun 5788  df-fn 5789  df-f 5790  df-f1 5791  df-fo 5792  df-f1o 5793  df-fv 5794  df-riota 6485  df-ov 6526  df-oprab 6527  df-mpt2 6528  df-om 6931  df-1st 7032  df-2nd 7033  df-wrecs 7267  df-recs 7328  df-rdg 7366  df-1o 7420  df-2o 7421  df-oadd 7424  df-er 7602  df-map 7719  df-pm 7720  df-en 7815  df-dom 7816  df-sdom 7817  df-fin 7818  df-sup 8204  df-card 8621  df-cda 8846  df-pnf 9928  df-mnf 9929  df-xr 9930  df-ltxr 9931  df-le 9932  df-sub 10115  df-neg 10116  df-div 10530  df-nn 10864  df-2 10922  df-3 10923  df-n0 11136  df-z 11207  df-uz 11516  df-rp 11661  df-fz 12149  df-fzo 12286  df-seq 12615  df-exp 12674  df-hash 12931  df-word 13096  df-lsw 13097  df-substr 13100  df-cj 13629  df-re 13630  df-im 13631  df-sqrt 13765  df-abs 13766  df-dvds 14764  df-prm 15166  df-uhgr 40278  df-upgr 40306  df-edga 40350  df-uspgr 40378  df-usgr 40379  df-fusgr 40534  df-1wlks 40798  df-wlks 40799  df-clwlks 40975  df-clwwlks 41183  df-clwwlksn 41184
This theorem is referenced by:  clwlksfoclwwlk  41268  clwlksf1clwwlk  41274
  Copyright terms: Public domain W3C validator