MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  clwlksfclwwlkOLD Structured version   Visualization version   GIF version

Theorem clwlksfclwwlkOLD 27357
Description: Obsolete version of clwlkclwwlkf 27263 as of 23-May-2022. (Contributed by Alexander van der Vekens, 25-Jun-2018.) (Revised by AV, 2-May-2021.) (Proof modification is discouraged.) (New usage is discouraged.)
Hypotheses
Ref Expression
clwlksfclwwlkOLD.1 𝐴 = (1st𝑐)
clwlksfclwwlkOLD.2 𝐵 = (2nd𝑐)
clwlksfclwwlkOLD.c 𝐶 = {𝑐 ∈ (ClWalks‘𝐺) ∣ (♯‘𝐴) = 𝑁}
clwlksfclwwlkOLD.f 𝐹 = (𝑐𝐶 ↦ (𝐵 substr ⟨0, (♯‘𝐴)⟩))
Assertion
Ref Expression
clwlksfclwwlkOLD ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → 𝐹:𝐶⟶(𝑁 ClWWalksN 𝐺))
Distinct variable groups:   𝐺,𝑐   𝑁,𝑐   𝐶,𝑐
Allowed substitution hints:   𝐴(𝑐)   𝐵(𝑐)   𝐹(𝑐)

Proof of Theorem clwlksfclwwlkOLD
Dummy variables 𝑖 𝑥 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 clwlksfclwwlkOLD.c . . . . . 6 𝐶 = {𝑐 ∈ (ClWalks‘𝐺) ∣ (♯‘𝐴) = 𝑁}
21rabeq2i 3346 . . . . 5 (𝑐𝐶 ↔ (𝑐 ∈ (ClWalks‘𝐺) ∧ (♯‘𝐴) = 𝑁))
3 fusgrusgr 26509 . . . . . . . . . . . 12 (𝐺 ∈ FinUSGraph → 𝐺 ∈ USGraph)
4 usgrupgr 26371 . . . . . . . . . . . 12 (𝐺 ∈ USGraph → 𝐺 ∈ UPGraph)
53, 4syl 17 . . . . . . . . . . 11 (𝐺 ∈ FinUSGraph → 𝐺 ∈ UPGraph)
65adantr 472 . . . . . . . . . 10 ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → 𝐺 ∈ UPGraph)
7 eqid 2765 . . . . . . . . . . 11 (Vtx‘𝐺) = (Vtx‘𝐺)
8 eqid 2765 . . . . . . . . . . 11 (iEdg‘𝐺) = (iEdg‘𝐺)
9 clwlksfclwwlkOLD.1 . . . . . . . . . . 11 𝐴 = (1st𝑐)
10 clwlksfclwwlkOLD.2 . . . . . . . . . . 11 𝐵 = (2nd𝑐)
117, 8, 9, 10upgrclwlkcompim 26989 . . . . . . . . . 10 ((𝐺 ∈ UPGraph ∧ 𝑐 ∈ (ClWalks‘𝐺)) → ((𝐴 ∈ Word dom (iEdg‘𝐺) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ ∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴))))
126, 11sylan 575 . . . . . . . . 9 (((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) ∧ 𝑐 ∈ (ClWalks‘𝐺)) → ((𝐴 ∈ Word dom (iEdg‘𝐺) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ ∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴))))
13 lencl 13512 . . . . . . . . . . . . . . 15 (𝐴 ∈ Word dom (iEdg‘𝐺) → (♯‘𝐴) ∈ ℕ0)
14 clwlksfclwwlkOLD.f . . . . . . . . . . . . . . . . . . . . . . . 24 𝐹 = (𝑐𝐶 ↦ (𝐵 substr ⟨0, (♯‘𝐴)⟩))
159, 10, 1, 14clwlksfclwwlk2wrdOLD 27353 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑐𝐶𝐵 ∈ Word (Vtx‘𝐺))
1615ad2antlr 718 . . . . . . . . . . . . . . . . . . . . . 22 ((((((((♯‘𝐴) ∈ ℕ0𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → 𝐵 ∈ Word (Vtx‘𝐺))
17 swrdcl 13629 . . . . . . . . . . . . . . . . . . . . . 22 (𝐵 ∈ Word (Vtx‘𝐺) → (𝐵 substr ⟨0, (♯‘𝐴)⟩) ∈ Word (Vtx‘𝐺))
1816, 17syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((((((((♯‘𝐴) ∈ ℕ0𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → (𝐵 substr ⟨0, (♯‘𝐴)⟩) ∈ Word (Vtx‘𝐺))
19 ffz0iswrd 13520 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺) → 𝐵 ∈ Word (Vtx‘𝐺))
20193ad2ant1 1163 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺) ∧ (♯‘𝐴) = 𝑁 ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → 𝐵 ∈ Word (Vtx‘𝐺))
21 prmnn 15684 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑁 ∈ ℙ → 𝑁 ∈ ℕ)
2221adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → 𝑁 ∈ ℕ)
23223ad2ant3 1165 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺) ∧ (♯‘𝐴) = 𝑁 ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → 𝑁 ∈ ℕ)
24 oveq2 6854 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((♯‘𝐴) = 𝑁 → (0...(♯‘𝐴)) = (0...𝑁))
2524feq2d 6211 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((♯‘𝐴) = 𝑁 → (𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺) ↔ 𝐵:(0...𝑁)⟶(Vtx‘𝐺)))
2622nnnn0d 11603 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → 𝑁 ∈ ℕ0)
27 ffz0hash 13439 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑁 ∈ ℕ0𝐵:(0...𝑁)⟶(Vtx‘𝐺)) → (♯‘𝐵) = (𝑁 + 1))
2826, 27sylan 575 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) ∧ 𝐵:(0...𝑁)⟶(Vtx‘𝐺)) → (♯‘𝐵) = (𝑁 + 1))
2928ex 401 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (𝐵:(0...𝑁)⟶(Vtx‘𝐺) → (♯‘𝐵) = (𝑁 + 1)))
3021nnred 11296 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑁 ∈ ℙ → 𝑁 ∈ ℝ)
3130adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑁 ∈ ℙ ∧ (♯‘𝐵) = (𝑁 + 1)) → 𝑁 ∈ ℝ)
3231lep1d 11214 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑁 ∈ ℙ ∧ (♯‘𝐵) = (𝑁 + 1)) → 𝑁 ≤ (𝑁 + 1))
33 breq2 4815 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((♯‘𝐵) = (𝑁 + 1) → (𝑁 ≤ (♯‘𝐵) ↔ 𝑁 ≤ (𝑁 + 1)))
3433adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑁 ∈ ℙ ∧ (♯‘𝐵) = (𝑁 + 1)) → (𝑁 ≤ (♯‘𝐵) ↔ 𝑁 ≤ (𝑁 + 1)))
3532, 34mpbird 248 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑁 ∈ ℙ ∧ (♯‘𝐵) = (𝑁 + 1)) → 𝑁 ≤ (♯‘𝐵))
3635ex 401 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑁 ∈ ℙ → ((♯‘𝐵) = (𝑁 + 1) → 𝑁 ≤ (♯‘𝐵)))
3736adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → ((♯‘𝐵) = (𝑁 + 1) → 𝑁 ≤ (♯‘𝐵)))
3829, 37syldc 48 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝐵:(0...𝑁)⟶(Vtx‘𝐺) → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → 𝑁 ≤ (♯‘𝐵)))
3925, 38syl6bi 244 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((♯‘𝐴) = 𝑁 → (𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺) → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → 𝑁 ≤ (♯‘𝐵))))
40393imp21 1141 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺) ∧ (♯‘𝐴) = 𝑁 ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → 𝑁 ≤ (♯‘𝐵))
41 swrdn0OLD 13641 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ ℕ ∧ 𝑁 ≤ (♯‘𝐵)) → (𝐵 substr ⟨0, 𝑁⟩) ≠ ∅)
4220, 23, 40, 41syl3anc 1490 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺) ∧ (♯‘𝐴) = 𝑁 ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → (𝐵 substr ⟨0, 𝑁⟩) ≠ ∅)
43 opeq2 4562 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((♯‘𝐴) = 𝑁 → ⟨0, (♯‘𝐴)⟩ = ⟨0, 𝑁⟩)
4443oveq2d 6862 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((♯‘𝐴) = 𝑁 → (𝐵 substr ⟨0, (♯‘𝐴)⟩) = (𝐵 substr ⟨0, 𝑁⟩))
4544neeq1d 2996 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((♯‘𝐴) = 𝑁 → ((𝐵 substr ⟨0, (♯‘𝐴)⟩) ≠ ∅ ↔ (𝐵 substr ⟨0, 𝑁⟩) ≠ ∅))
46453ad2ant2 1164 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺) ∧ (♯‘𝐴) = 𝑁 ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → ((𝐵 substr ⟨0, (♯‘𝐴)⟩) ≠ ∅ ↔ (𝐵 substr ⟨0, 𝑁⟩) ≠ ∅))
4742, 46mpbird 248 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺) ∧ (♯‘𝐴) = 𝑁 ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → (𝐵 substr ⟨0, (♯‘𝐴)⟩) ≠ ∅)
48473exp 1148 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺) → ((♯‘𝐴) = 𝑁 → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (𝐵 substr ⟨0, (♯‘𝐴)⟩) ≠ ∅)))
4948ad2antlr 718 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((♯‘𝐴) ∈ ℕ0𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) → ((♯‘𝐴) = 𝑁 → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (𝐵 substr ⟨0, (♯‘𝐴)⟩) ≠ ∅)))
5049imp 395 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((♯‘𝐴) ∈ ℕ0𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (𝐵 substr ⟨0, (♯‘𝐴)⟩) ≠ ∅))
5150adantr 472 . . . . . . . . . . . . . . . . . . . . . 22 (((((((♯‘𝐴) ∈ ℕ0𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐𝐶) → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (𝐵 substr ⟨0, (♯‘𝐴)⟩) ≠ ∅))
5251imp 395 . . . . . . . . . . . . . . . . . . . . 21 ((((((((♯‘𝐴) ∈ ℕ0𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → (𝐵 substr ⟨0, (♯‘𝐴)⟩) ≠ ∅)
5318, 52jca 507 . . . . . . . . . . . . . . . . . . . 20 ((((((((♯‘𝐴) ∈ ℕ0𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → ((𝐵 substr ⟨0, (♯‘𝐴)⟩) ∈ Word (Vtx‘𝐺) ∧ (𝐵 substr ⟨0, (♯‘𝐴)⟩) ≠ ∅))
54 simp-5r 807 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((((♯‘𝐴) ∈ ℕ0𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐𝐶) → 𝐴 ∈ Word dom (iEdg‘𝐺))
553adantr 472 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → 𝐺 ∈ USGraph)
5654, 55anim12ci 607 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((((♯‘𝐴) ∈ ℕ0𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → (𝐺 ∈ USGraph ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)))
57 simp-5r 807 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((((♯‘𝐴) ∈ ℕ0𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺))
58 prmuz2 15704 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑁 ∈ ℙ → 𝑁 ∈ (ℤ‘2))
59 ffz0hash 13439 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((♯‘𝐴) ∈ ℕ0𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) → (♯‘𝐵) = ((♯‘𝐴) + 1))
6059adantlr 706 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((♯‘𝐴) ∈ ℕ0𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) → (♯‘𝐵) = ((♯‘𝐴) + 1))
61 eluz2 11899 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((♯‘𝐴) ∈ (ℤ‘2) ↔ (2 ∈ ℤ ∧ (♯‘𝐴) ∈ ℤ ∧ 2 ≤ (♯‘𝐴)))
62 2re 11351 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 2 ∈ ℝ
6362a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((♯‘𝐴) ∈ ℤ → 2 ∈ ℝ)
64 zre 11633 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((♯‘𝐴) ∈ ℤ → (♯‘𝐴) ∈ ℝ)
65 peano2re 10468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((♯‘𝐴) ∈ ℝ → ((♯‘𝐴) + 1) ∈ ℝ)
6664, 65syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((♯‘𝐴) ∈ ℤ → ((♯‘𝐴) + 1) ∈ ℝ)
6763, 64, 663jca 1158 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((♯‘𝐴) ∈ ℤ → (2 ∈ ℝ ∧ (♯‘𝐴) ∈ ℝ ∧ ((♯‘𝐴) + 1) ∈ ℝ))
6867adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((♯‘𝐴) ∈ ℤ ∧ 2 ≤ (♯‘𝐴)) → (2 ∈ ℝ ∧ (♯‘𝐴) ∈ ℝ ∧ ((♯‘𝐴) + 1) ∈ ℝ))
69 simpr 477 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((♯‘𝐴) ∈ ℤ ∧ 2 ≤ (♯‘𝐴)) → 2 ≤ (♯‘𝐴))
7064lep1d 11214 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((♯‘𝐴) ∈ ℤ → (♯‘𝐴) ≤ ((♯‘𝐴) + 1))
7170adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((♯‘𝐴) ∈ ℤ ∧ 2 ≤ (♯‘𝐴)) → (♯‘𝐴) ≤ ((♯‘𝐴) + 1))
72 letr 10390 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((2 ∈ ℝ ∧ (♯‘𝐴) ∈ ℝ ∧ ((♯‘𝐴) + 1) ∈ ℝ) → ((2 ≤ (♯‘𝐴) ∧ (♯‘𝐴) ≤ ((♯‘𝐴) + 1)) → 2 ≤ ((♯‘𝐴) + 1)))
7372imp 395 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((2 ∈ ℝ ∧ (♯‘𝐴) ∈ ℝ ∧ ((♯‘𝐴) + 1) ∈ ℝ) ∧ (2 ≤ (♯‘𝐴) ∧ (♯‘𝐴) ≤ ((♯‘𝐴) + 1))) → 2 ≤ ((♯‘𝐴) + 1))
7468, 69, 71, 73syl12anc 865 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((♯‘𝐴) ∈ ℤ ∧ 2 ≤ (♯‘𝐴)) → 2 ≤ ((♯‘𝐴) + 1))
75743adant1 1160 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((2 ∈ ℤ ∧ (♯‘𝐴) ∈ ℤ ∧ 2 ≤ (♯‘𝐴)) → 2 ≤ ((♯‘𝐴) + 1))
7661, 75sylbi 208 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((♯‘𝐴) ∈ (ℤ‘2) → 2 ≤ ((♯‘𝐴) + 1))
7776a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((♯‘𝐵) = ((♯‘𝐴) + 1) ∧ (♯‘𝐴) = 𝑁) → ((♯‘𝐴) ∈ (ℤ‘2) → 2 ≤ ((♯‘𝐴) + 1)))
78 eleq1 2832 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑁 = (♯‘𝐴) → (𝑁 ∈ (ℤ‘2) ↔ (♯‘𝐴) ∈ (ℤ‘2)))
7978eqcoms 2773 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((♯‘𝐴) = 𝑁 → (𝑁 ∈ (ℤ‘2) ↔ (♯‘𝐴) ∈ (ℤ‘2)))
8079adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((♯‘𝐵) = ((♯‘𝐴) + 1) ∧ (♯‘𝐴) = 𝑁) → (𝑁 ∈ (ℤ‘2) ↔ (♯‘𝐴) ∈ (ℤ‘2)))
81 breq2 4815 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((♯‘𝐵) = ((♯‘𝐴) + 1) → (2 ≤ (♯‘𝐵) ↔ 2 ≤ ((♯‘𝐴) + 1)))
8281adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((♯‘𝐵) = ((♯‘𝐴) + 1) ∧ (♯‘𝐴) = 𝑁) → (2 ≤ (♯‘𝐵) ↔ 2 ≤ ((♯‘𝐴) + 1)))
8377, 80, 823imtr4d 285 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((♯‘𝐵) = ((♯‘𝐴) + 1) ∧ (♯‘𝐴) = 𝑁) → (𝑁 ∈ (ℤ‘2) → 2 ≤ (♯‘𝐵)))
8483ex 401 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((♯‘𝐵) = ((♯‘𝐴) + 1) → ((♯‘𝐴) = 𝑁 → (𝑁 ∈ (ℤ‘2) → 2 ≤ (♯‘𝐵))))
8560, 84syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((♯‘𝐴) ∈ ℕ0𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) → ((♯‘𝐴) = 𝑁 → (𝑁 ∈ (ℤ‘2) → 2 ≤ (♯‘𝐵))))
8685adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((♯‘𝐴) ∈ ℕ0𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) → ((♯‘𝐴) = 𝑁 → (𝑁 ∈ (ℤ‘2) → 2 ≤ (♯‘𝐵))))
8786imp 395 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((♯‘𝐴) ∈ ℕ0𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) → (𝑁 ∈ (ℤ‘2) → 2 ≤ (♯‘𝐵)))
8887adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((((♯‘𝐴) ∈ ℕ0𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐𝐶) → (𝑁 ∈ (ℤ‘2) → 2 ≤ (♯‘𝐵)))
8958, 88syl5com 31 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑁 ∈ ℙ → (((((((♯‘𝐴) ∈ ℕ0𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐𝐶) → 2 ≤ (♯‘𝐵)))
9089adantl 473 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (((((((♯‘𝐴) ∈ ℕ0𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐𝐶) → 2 ≤ (♯‘𝐵)))
9190impcom 396 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((((♯‘𝐴) ∈ ℕ0𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → 2 ≤ (♯‘𝐵))
92 simp-4r 803 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((((♯‘𝐴) ∈ ℕ0𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴))))
937, 8usgrf 26344 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝐺 ∈ USGraph → (iEdg‘𝐺):dom (iEdg‘𝐺)–1-1→{𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣ (♯‘𝑥) = 2})
9493anim1i 608 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐺 ∈ USGraph ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) → ((iEdg‘𝐺):dom (iEdg‘𝐺)–1-1→{𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣ (♯‘𝑥) = 2} ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)))
95 clwlkclwwlklem2 27247 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((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‘𝐺)))
9694, 95syl3an1 1202 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝐺 ∈ USGraph ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ (𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺) ∧ 2 ≤ (♯‘𝐵)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) → ((lastS‘𝐵) = (𝐵‘0) ∧ ∀𝑖 ∈ (0..^((♯‘𝐴) − 1)){(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∈ ran (iEdg‘𝐺) ∧ {(𝐵‘((♯‘𝐴) − 1)), (𝐵‘0)} ∈ ran (iEdg‘𝐺)))
97 biid 252 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((lastS‘𝐵) = (𝐵‘0) ↔ (lastS‘𝐵) = (𝐵‘0))
98 edgval 26234 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (Edg‘𝐺) = ran (iEdg‘𝐺)
9998eleq2i 2836 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ({(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∈ ran (iEdg‘𝐺))
10099ralbii 3127 . . . . . . . . . . . . . . . . . . . . . . . . 25 (∀𝑖 ∈ (0..^((♯‘𝐴) − 1)){(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ (0..^((♯‘𝐴) − 1)){(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∈ ran (iEdg‘𝐺))
10198eleq2i 2836 . . . . . . . . . . . . . . . . . . . . . . . . 25 ({(𝐵‘((♯‘𝐴) − 1)), (𝐵‘0)} ∈ (Edg‘𝐺) ↔ {(𝐵‘((♯‘𝐴) − 1)), (𝐵‘0)} ∈ ran (iEdg‘𝐺))
10297, 100, 1013anbi123i 1194 . . . . . . . . . . . . . . . . . . . . . . . 24 (((lastS‘𝐵) = (𝐵‘0) ∧ ∀𝑖 ∈ (0..^((♯‘𝐴) − 1)){(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(𝐵‘((♯‘𝐴) − 1)), (𝐵‘0)} ∈ (Edg‘𝐺)) ↔ ((lastS‘𝐵) = (𝐵‘0) ∧ ∀𝑖 ∈ (0..^((♯‘𝐴) − 1)){(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∈ ran (iEdg‘𝐺) ∧ {(𝐵‘((♯‘𝐴) − 1)), (𝐵‘0)} ∈ ran (iEdg‘𝐺)))
10396, 102sylibr 225 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐺 ∈ USGraph ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ (𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺) ∧ 2 ≤ (♯‘𝐵)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) → ((lastS‘𝐵) = (𝐵‘0) ∧ ∀𝑖 ∈ (0..^((♯‘𝐴) − 1)){(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(𝐵‘((♯‘𝐴) − 1)), (𝐵‘0)} ∈ (Edg‘𝐺)))
10456, 57, 91, 92, 103syl121anc 1494 . . . . . . . . . . . . . . . . . . . . . 22 ((((((((♯‘𝐴) ∈ ℕ0𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → ((lastS‘𝐵) = (𝐵‘0) ∧ ∀𝑖 ∈ (0..^((♯‘𝐴) − 1)){(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(𝐵‘((♯‘𝐴) − 1)), (𝐵‘0)} ∈ (Edg‘𝐺)))
1059, 10, 1, 14clwlksfclwwlk1hashOLD 27355 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑐𝐶 → (♯‘𝐴) ∈ (0...(♯‘𝐵)))
106 simp2 1167 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((♯‘𝐴) ∈ (0...(♯‘𝐵)) ∧ 𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝑖 ∈ (0..^((♯‘𝐴) − 1))) → 𝐵 ∈ Word (Vtx‘𝐺))
107 simp1 1166 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((♯‘𝐴) ∈ (0...(♯‘𝐵)) ∧ 𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝑖 ∈ (0..^((♯‘𝐴) − 1))) → (♯‘𝐴) ∈ (0...(♯‘𝐵)))
108 elfzelz 12556 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((♯‘𝐴) ∈ (0...(♯‘𝐵)) → (♯‘𝐴) ∈ ℤ)
109 peano2zm 11673 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((♯‘𝐴) ∈ ℤ → ((♯‘𝐴) − 1) ∈ ℤ)
110 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((♯‘𝐴) ∈ ℤ → (♯‘𝐴) ∈ ℤ)
11164lem1d 11216 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((♯‘𝐴) ∈ ℤ → ((♯‘𝐴) − 1) ≤ (♯‘𝐴))
112 eluz2 11899 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((♯‘𝐴) ∈ (ℤ‘((♯‘𝐴) − 1)) ↔ (((♯‘𝐴) − 1) ∈ ℤ ∧ (♯‘𝐴) ∈ ℤ ∧ ((♯‘𝐴) − 1) ≤ (♯‘𝐴)))
113109, 110, 111, 112syl3anbrc 1443 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((♯‘𝐴) ∈ ℤ → (♯‘𝐴) ∈ (ℤ‘((♯‘𝐴) − 1)))
114 fzoss2 12711 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((♯‘𝐴) ∈ (ℤ‘((♯‘𝐴) − 1)) → (0..^((♯‘𝐴) − 1)) ⊆ (0..^(♯‘𝐴)))
115108, 113, 1143syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((♯‘𝐴) ∈ (0...(♯‘𝐵)) → (0..^((♯‘𝐴) − 1)) ⊆ (0..^(♯‘𝐴)))
116115sselda 3763 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((♯‘𝐴) ∈ (0...(♯‘𝐵)) ∧ 𝑖 ∈ (0..^((♯‘𝐴) − 1))) → 𝑖 ∈ (0..^(♯‘𝐴)))
1171163adant2 1161 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((♯‘𝐴) ∈ (0...(♯‘𝐵)) ∧ 𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝑖 ∈ (0..^((♯‘𝐴) − 1))) → 𝑖 ∈ (0..^(♯‘𝐴)))
118 swrd0fvOLD 13652 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝐵 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝐴) ∈ (0...(♯‘𝐵)) ∧ 𝑖 ∈ (0..^(♯‘𝐴))) → ((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘𝑖) = (𝐵𝑖))
119106, 107, 117, 118syl3anc 1490 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((♯‘𝐴) ∈ (0...(♯‘𝐵)) ∧ 𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝑖 ∈ (0..^((♯‘𝐴) − 1))) → ((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘𝑖) = (𝐵𝑖))
120119eqcomd 2771 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((♯‘𝐴) ∈ (0...(♯‘𝐵)) ∧ 𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝑖 ∈ (0..^((♯‘𝐴) − 1))) → (𝐵𝑖) = ((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘𝑖))
121 elfzom1elp1fzo 12750 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((♯‘𝐴) ∈ ℤ ∧ 𝑖 ∈ (0..^((♯‘𝐴) − 1))) → (𝑖 + 1) ∈ (0..^(♯‘𝐴)))
122108, 121sylan 575 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((♯‘𝐴) ∈ (0...(♯‘𝐵)) ∧ 𝑖 ∈ (0..^((♯‘𝐴) − 1))) → (𝑖 + 1) ∈ (0..^(♯‘𝐴)))
1231223adant2 1161 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((♯‘𝐴) ∈ (0...(♯‘𝐵)) ∧ 𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝑖 ∈ (0..^((♯‘𝐴) − 1))) → (𝑖 + 1) ∈ (0..^(♯‘𝐴)))
124 swrd0fvOLD 13652 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝐵 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝐴) ∈ (0...(♯‘𝐵)) ∧ (𝑖 + 1) ∈ (0..^(♯‘𝐴))) → ((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘(𝑖 + 1)) = (𝐵‘(𝑖 + 1)))
125124eqcomd 2771 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝐵 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝐴) ∈ (0...(♯‘𝐵)) ∧ (𝑖 + 1) ∈ (0..^(♯‘𝐴))) → (𝐵‘(𝑖 + 1)) = ((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘(𝑖 + 1)))
126106, 107, 123, 125syl3anc 1490 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((♯‘𝐴) ∈ (0...(♯‘𝐵)) ∧ 𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝑖 ∈ (0..^((♯‘𝐴) − 1))) → (𝐵‘(𝑖 + 1)) = ((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘(𝑖 + 1)))
127120, 126preq12d 4433 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((♯‘𝐴) ∈ (0...(♯‘𝐵)) ∧ 𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝑖 ∈ (0..^((♯‘𝐴) − 1))) → {(𝐵𝑖), (𝐵‘(𝑖 + 1))} = {((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘𝑖), ((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘(𝑖 + 1))})
1281273exp 1148 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((♯‘𝐴) ∈ (0...(♯‘𝐵)) → (𝐵 ∈ Word (Vtx‘𝐺) → (𝑖 ∈ (0..^((♯‘𝐴) − 1)) → {(𝐵𝑖), (𝐵‘(𝑖 + 1))} = {((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘𝑖), ((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘(𝑖 + 1))})))
129105, 15, 128sylc 65 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑐𝐶 → (𝑖 ∈ (0..^((♯‘𝐴) − 1)) → {(𝐵𝑖), (𝐵‘(𝑖 + 1))} = {((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘𝑖), ((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘(𝑖 + 1))}))
130129imp 395 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑐𝐶𝑖 ∈ (0..^((♯‘𝐴) − 1))) → {(𝐵𝑖), (𝐵‘(𝑖 + 1))} = {((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘𝑖), ((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘(𝑖 + 1))})
131130eleq1d 2829 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑐𝐶𝑖 ∈ (0..^((♯‘𝐴) − 1))) → ({(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ {((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘𝑖), ((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
132131ralbidva 3132 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑐𝐶 → (∀𝑖 ∈ (0..^((♯‘𝐴) − 1)){(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ (0..^((♯‘𝐴) − 1)){((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘𝑖), ((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
133132ad2antlr 718 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((((♯‘𝐴) ∈ ℕ0𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → (∀𝑖 ∈ (0..^((♯‘𝐴) − 1)){(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ (0..^((♯‘𝐴) − 1)){((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘𝑖), ((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
1349, 10, 1, 14clwlksfclwwlk2sswdOLD 27356 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑐𝐶 → (♯‘𝐴) = (♯‘(𝐵 substr ⟨0, (♯‘𝐴)⟩)))
135134oveq1d 6861 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑐𝐶 → ((♯‘𝐴) − 1) = ((♯‘(𝐵 substr ⟨0, (♯‘𝐴)⟩)) − 1))
136135ad2antlr 718 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((((♯‘𝐴) ∈ ℕ0𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → ((♯‘𝐴) − 1) = ((♯‘(𝐵 substr ⟨0, (♯‘𝐴)⟩)) − 1))
137136oveq2d 6862 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((((♯‘𝐴) ∈ ℕ0𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → (0..^((♯‘𝐴) − 1)) = (0..^((♯‘(𝐵 substr ⟨0, (♯‘𝐴)⟩)) − 1)))
138137raleqdv 3292 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((((♯‘𝐴) ∈ ℕ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‘𝐺)))
139133, 138bitrd 270 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((((♯‘𝐴) ∈ ℕ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‘𝐺)))
140 eleq1 2832 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑁 = (♯‘𝐴) → (𝑁 ∈ ℙ ↔ (♯‘𝐴) ∈ ℙ))
141140biimpd 220 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑁 = (♯‘𝐴) → (𝑁 ∈ ℙ → (♯‘𝐴) ∈ ℙ))
142141eqcoms 2773 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((♯‘𝐴) = 𝑁 → (𝑁 ∈ ℙ → (♯‘𝐴) ∈ ℙ))
143 prmnn 15684 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((♯‘𝐴) ∈ ℙ → (♯‘𝐴) ∈ ℕ)
144 elfz2nn0 12645 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((♯‘𝐴) ∈ (0...(♯‘𝐵)) ↔ ((♯‘𝐴) ∈ ℕ0 ∧ (♯‘𝐵) ∈ ℕ0 ∧ (♯‘𝐴) ≤ (♯‘𝐵)))
145 1zzd 11661 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (((♯‘𝐴) ∈ ℕ0 ∧ (♯‘𝐵) ∈ ℕ0) → 1 ∈ ℤ)
146 nn0z 11653 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((♯‘𝐵) ∈ ℕ0 → (♯‘𝐵) ∈ ℤ)
147146adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (((♯‘𝐴) ∈ ℕ0 ∧ (♯‘𝐵) ∈ ℕ0) → (♯‘𝐵) ∈ ℤ)
148 nn0z 11653 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((♯‘𝐴) ∈ ℕ0 → (♯‘𝐴) ∈ ℤ)
149148adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (((♯‘𝐴) ∈ ℕ0 ∧ (♯‘𝐵) ∈ ℕ0) → (♯‘𝐴) ∈ ℤ)
150145, 147, 1493jca 1158 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (((♯‘𝐴) ∈ ℕ0 ∧ (♯‘𝐵) ∈ ℕ0) → (1 ∈ ℤ ∧ (♯‘𝐵) ∈ ℤ ∧ (♯‘𝐴) ∈ ℤ))
1511503adant3 1162 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (((♯‘𝐴) ∈ ℕ0 ∧ (♯‘𝐵) ∈ ℕ0 ∧ (♯‘𝐴) ≤ (♯‘𝐵)) → (1 ∈ ℤ ∧ (♯‘𝐵) ∈ ℤ ∧ (♯‘𝐴) ∈ ℤ))
152151adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((((♯‘𝐴) ∈ ℕ0 ∧ (♯‘𝐵) ∈ ℕ0 ∧ (♯‘𝐴) ≤ (♯‘𝐵)) ∧ (♯‘𝐴) ∈ ℕ) → (1 ∈ ℤ ∧ (♯‘𝐵) ∈ ℤ ∧ (♯‘𝐴) ∈ ℤ))
153 simp3 1168 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (((♯‘𝐴) ∈ ℕ0 ∧ (♯‘𝐵) ∈ ℕ0 ∧ (♯‘𝐴) ≤ (♯‘𝐵)) → (♯‘𝐴) ≤ (♯‘𝐵))
154 nnge1 11308 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((♯‘𝐴) ∈ ℕ → 1 ≤ (♯‘𝐴))
155153, 154anim12ci 607 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((((♯‘𝐴) ∈ ℕ0 ∧ (♯‘𝐵) ∈ ℕ0 ∧ (♯‘𝐴) ≤ (♯‘𝐵)) ∧ (♯‘𝐴) ∈ ℕ) → (1 ≤ (♯‘𝐴) ∧ (♯‘𝐴) ≤ (♯‘𝐵)))
156152, 155jca 507 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((((♯‘𝐴) ∈ ℕ0 ∧ (♯‘𝐵) ∈ ℕ0 ∧ (♯‘𝐴) ≤ (♯‘𝐵)) ∧ (♯‘𝐴) ∈ ℕ) → ((1 ∈ ℤ ∧ (♯‘𝐵) ∈ ℤ ∧ (♯‘𝐴) ∈ ℤ) ∧ (1 ≤ (♯‘𝐴) ∧ (♯‘𝐴) ≤ (♯‘𝐵))))
157144, 156sylanb 576 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((♯‘𝐴) ∈ (0...(♯‘𝐵)) ∧ (♯‘𝐴) ∈ ℕ) → ((1 ∈ ℤ ∧ (♯‘𝐵) ∈ ℤ ∧ (♯‘𝐴) ∈ ℤ) ∧ (1 ≤ (♯‘𝐴) ∧ (♯‘𝐴) ≤ (♯‘𝐵))))
158 elfz2 12547 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((♯‘𝐴) ∈ (1...(♯‘𝐵)) ↔ ((1 ∈ ℤ ∧ (♯‘𝐵) ∈ ℤ ∧ (♯‘𝐴) ∈ ℤ) ∧ (1 ≤ (♯‘𝐴) ∧ (♯‘𝐴) ≤ (♯‘𝐵))))
159157, 158sylibr 225 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((♯‘𝐴) ∈ (0...(♯‘𝐵)) ∧ (♯‘𝐴) ∈ ℕ) → (♯‘𝐴) ∈ (1...(♯‘𝐵)))
160 swrd0fvlswOLD 13656 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝐵 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝐴) ∈ (1...(♯‘𝐵))) → (lastS‘(𝐵 substr ⟨0, (♯‘𝐴)⟩)) = (𝐵‘((♯‘𝐴) − 1)))
161160eqcomd 2771 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝐵 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝐴) ∈ (1...(♯‘𝐵))) → (𝐵‘((♯‘𝐴) − 1)) = (lastS‘(𝐵 substr ⟨0, (♯‘𝐴)⟩)))
162 swrd0fv0OLD 13653 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝐵 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝐴) ∈ (1...(♯‘𝐵))) → ((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘0) = (𝐵‘0))
163162eqcomd 2771 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝐵 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝐴) ∈ (1...(♯‘𝐵))) → (𝐵‘0) = ((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘0))
164161, 163preq12d 4433 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝐵 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝐴) ∈ (1...(♯‘𝐵))) → {(𝐵‘((♯‘𝐴) − 1)), (𝐵‘0)} = {(lastS‘(𝐵 substr ⟨0, (♯‘𝐴)⟩)), ((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘0)})
165164expcom 402 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((♯‘𝐴) ∈ (1...(♯‘𝐵)) → (𝐵 ∈ Word (Vtx‘𝐺) → {(𝐵‘((♯‘𝐴) − 1)), (𝐵‘0)} = {(lastS‘(𝐵 substr ⟨0, (♯‘𝐴)⟩)), ((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘0)}))
166159, 165syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((♯‘𝐴) ∈ (0...(♯‘𝐵)) ∧ (♯‘𝐴) ∈ ℕ) → (𝐵 ∈ Word (Vtx‘𝐺) → {(𝐵‘((♯‘𝐴) − 1)), (𝐵‘0)} = {(lastS‘(𝐵 substr ⟨0, (♯‘𝐴)⟩)), ((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘0)}))
167166ex 401 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((♯‘𝐴) ∈ (0...(♯‘𝐵)) → ((♯‘𝐴) ∈ ℕ → (𝐵 ∈ Word (Vtx‘𝐺) → {(𝐵‘((♯‘𝐴) − 1)), (𝐵‘0)} = {(lastS‘(𝐵 substr ⟨0, (♯‘𝐴)⟩)), ((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘0)})))
168167com23 86 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((♯‘𝐴) ∈ (0...(♯‘𝐵)) → (𝐵 ∈ Word (Vtx‘𝐺) → ((♯‘𝐴) ∈ ℕ → {(𝐵‘((♯‘𝐴) − 1)), (𝐵‘0)} = {(lastS‘(𝐵 substr ⟨0, (♯‘𝐴)⟩)), ((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘0)})))
169105, 15, 168sylc 65 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑐𝐶 → ((♯‘𝐴) ∈ ℕ → {(𝐵‘((♯‘𝐴) − 1)), (𝐵‘0)} = {(lastS‘(𝐵 substr ⟨0, (♯‘𝐴)⟩)), ((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘0)}))
170143, 169syl5com 31 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((♯‘𝐴) ∈ ℙ → (𝑐𝐶 → {(𝐵‘((♯‘𝐴) − 1)), (𝐵‘0)} = {(lastS‘(𝐵 substr ⟨0, (♯‘𝐴)⟩)), ((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘0)}))
171142, 170syl6 35 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((♯‘𝐴) = 𝑁 → (𝑁 ∈ ℙ → (𝑐𝐶 → {(𝐵‘((♯‘𝐴) − 1)), (𝐵‘0)} = {(lastS‘(𝐵 substr ⟨0, (♯‘𝐴)⟩)), ((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘0)})))
172171com23 86 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((♯‘𝐴) = 𝑁 → (𝑐𝐶 → (𝑁 ∈ ℙ → {(𝐵‘((♯‘𝐴) − 1)), (𝐵‘0)} = {(lastS‘(𝐵 substr ⟨0, (♯‘𝐴)⟩)), ((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘0)})))
173172adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((♯‘𝐴) ∈ ℕ0𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) → (𝑐𝐶 → (𝑁 ∈ ℙ → {(𝐵‘((♯‘𝐴) − 1)), (𝐵‘0)} = {(lastS‘(𝐵 substr ⟨0, (♯‘𝐴)⟩)), ((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘0)})))
174173imp 395 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((((♯‘𝐴) ∈ ℕ0𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐𝐶) → (𝑁 ∈ ℙ → {(𝐵‘((♯‘𝐴) − 1)), (𝐵‘0)} = {(lastS‘(𝐵 substr ⟨0, (♯‘𝐴)⟩)), ((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘0)}))
175174com12 32 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑁 ∈ ℙ → (((((((♯‘𝐴) ∈ ℕ0𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐𝐶) → {(𝐵‘((♯‘𝐴) − 1)), (𝐵‘0)} = {(lastS‘(𝐵 substr ⟨0, (♯‘𝐴)⟩)), ((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘0)}))
176175adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (((((((♯‘𝐴) ∈ ℕ0𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐𝐶) → {(𝐵‘((♯‘𝐴) − 1)), (𝐵‘0)} = {(lastS‘(𝐵 substr ⟨0, (♯‘𝐴)⟩)), ((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘0)}))
177176impcom 396 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((((♯‘𝐴) ∈ ℕ0𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → {(𝐵‘((♯‘𝐴) − 1)), (𝐵‘0)} = {(lastS‘(𝐵 substr ⟨0, (♯‘𝐴)⟩)), ((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘0)})
178177eleq1d 2829 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((((♯‘𝐴) ∈ ℕ0𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → ({(𝐵‘((♯‘𝐴) − 1)), (𝐵‘0)} ∈ (Edg‘𝐺) ↔ {(lastS‘(𝐵 substr ⟨0, (♯‘𝐴)⟩)), ((𝐵 substr ⟨0, (♯‘𝐴)⟩)‘0)} ∈ (Edg‘𝐺)))
179139, 1783anbi23d 1563 . . . . . . . . . . . . . . . . . . . . . 22 ((((((((♯‘𝐴) ∈ ℕ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‘𝐺))))
180104, 179mpbid 223 . . . . . . . . . . . . . . . . . . . . 21 ((((((((♯‘𝐴) ∈ ℕ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‘𝐺)))
181 3simpc 1182 . . . . . . . . . . . . . . . . . . . . 21 (((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‘𝐺)))
182180, 181syl 17 . . . . . . . . . . . . . . . . . . . 20 ((((((((♯‘𝐴) ∈ ℕ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‘𝐺)))
183 3anass 1116 . . . . . . . . . . . . . . . . . . . 20 ((((𝐵 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‘𝐺))))
18453, 182, 183sylanbrc 578 . . . . . . . . . . . . . . . . . . 19 ((((((((♯‘𝐴) ∈ ℕ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‘𝐺)))
185 eqid 2765 . . . . . . . . . . . . . . . . . . . 20 (Edg‘𝐺) = (Edg‘𝐺)
1867, 185isclwwlk 27231 . . . . . . . . . . . . . . . . . . 19 ((𝐵 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‘𝐺)))
187184, 186sylibr 225 . . . . . . . . . . . . . . . . . 18 ((((((((♯‘𝐴) ∈ ℕ0𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → (𝐵 substr ⟨0, (♯‘𝐴)⟩) ∈ (ClWWalks‘𝐺))
188134eqeq1d 2767 . . . . . . . . . . . . . . . . . . . . . 22 (𝑐𝐶 → ((♯‘𝐴) = 𝑁 ↔ (♯‘(𝐵 substr ⟨0, (♯‘𝐴)⟩)) = 𝑁))
189188biimpcd 240 . . . . . . . . . . . . . . . . . . . . 21 ((♯‘𝐴) = 𝑁 → (𝑐𝐶 → (♯‘(𝐵 substr ⟨0, (♯‘𝐴)⟩)) = 𝑁))
190189adantl 473 . . . . . . . . . . . . . . . . . . . 20 ((((((♯‘𝐴) ∈ ℕ0𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) → (𝑐𝐶 → (♯‘(𝐵 substr ⟨0, (♯‘𝐴)⟩)) = 𝑁))
191190imp 395 . . . . . . . . . . . . . . . . . . 19 (((((((♯‘𝐴) ∈ ℕ0𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐𝐶) → (♯‘(𝐵 substr ⟨0, (♯‘𝐴)⟩)) = 𝑁)
192191adantr 472 . . . . . . . . . . . . . . . . . 18 ((((((((♯‘𝐴) ∈ ℕ0𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → (♯‘(𝐵 substr ⟨0, (♯‘𝐴)⟩)) = 𝑁)
193 isclwwlkn 27286 . . . . . . . . . . . . . . . . . 18 ((𝐵 substr ⟨0, (♯‘𝐴)⟩) ∈ (𝑁 ClWWalksN 𝐺) ↔ ((𝐵 substr ⟨0, (♯‘𝐴)⟩) ∈ (ClWWalks‘𝐺) ∧ (♯‘(𝐵 substr ⟨0, (♯‘𝐴)⟩)) = 𝑁))
194187, 192, 193sylanbrc 578 . . . . . . . . . . . . . . . . 17 ((((((((♯‘𝐴) ∈ ℕ0𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → (𝐵 substr ⟨0, (♯‘𝐴)⟩) ∈ (𝑁 ClWWalksN 𝐺))
195194exp31 410 . . . . . . . . . . . . . . . 16 ((((((♯‘𝐴) ∈ ℕ0𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) → (𝑐𝐶 → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (𝐵 substr ⟨0, (♯‘𝐴)⟩) ∈ (𝑁 ClWWalksN 𝐺))))
196195exp41 425 . . . . . . . . . . . . . . 15 (((♯‘𝐴) ∈ ℕ0𝐴 ∈ Word dom (iEdg‘𝐺)) → (𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺) → ((∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴))) → ((♯‘𝐴) = 𝑁 → (𝑐𝐶 → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (𝐵 substr ⟨0, (♯‘𝐴)⟩) ∈ (𝑁 ClWWalksN 𝐺)))))))
19713, 196mpancom 679 . . . . . . . . . . . . . 14 (𝐴 ∈ Word dom (iEdg‘𝐺) → (𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺) → ((∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴))) → ((♯‘𝐴) = 𝑁 → (𝑐𝐶 → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (𝐵 substr ⟨0, (♯‘𝐴)⟩) ∈ (𝑁 ClWWalksN 𝐺)))))))
198197imp 395 . . . . . . . . . . . . 13 ((𝐴 ∈ Word dom (iEdg‘𝐺) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) → ((∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴))) → ((♯‘𝐴) = 𝑁 → (𝑐𝐶 → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (𝐵 substr ⟨0, (♯‘𝐴)⟩) ∈ (𝑁 ClWWalksN 𝐺))))))
1991983impib 1144 . . . . . . . . . . . 12 (((𝐴 ∈ Word dom (iEdg‘𝐺) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ ∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴))) → ((♯‘𝐴) = 𝑁 → (𝑐𝐶 → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (𝐵 substr ⟨0, (♯‘𝐴)⟩) ∈ (𝑁 ClWWalksN 𝐺)))))
200199com12 32 . . . . . . . . . . 11 ((♯‘𝐴) = 𝑁 → (((𝐴 ∈ Word dom (iEdg‘𝐺) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ ∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴))) → (𝑐𝐶 → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (𝐵 substr ⟨0, (♯‘𝐴)⟩) ∈ (𝑁 ClWWalksN 𝐺)))))
201200com14 96 . . . . . . . . . 10 ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (((𝐴 ∈ Word dom (iEdg‘𝐺) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ ∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴))) → (𝑐𝐶 → ((♯‘𝐴) = 𝑁 → (𝐵 substr ⟨0, (♯‘𝐴)⟩) ∈ (𝑁 ClWWalksN 𝐺)))))
202201adantr 472 . . . . . . . . 9 (((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) ∧ 𝑐 ∈ (ClWalks‘𝐺)) → (((𝐴 ∈ Word dom (iEdg‘𝐺) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ ∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴𝑖)) = {(𝐵𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴))) → (𝑐𝐶 → ((♯‘𝐴) = 𝑁 → (𝐵 substr ⟨0, (♯‘𝐴)⟩) ∈ (𝑁 ClWWalksN 𝐺)))))
20312, 202mpd 15 . . . . . . . 8 (((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) ∧ 𝑐 ∈ (ClWalks‘𝐺)) → (𝑐𝐶 → ((♯‘𝐴) = 𝑁 → (𝐵 substr ⟨0, (♯‘𝐴)⟩) ∈ (𝑁 ClWWalksN 𝐺))))
204203expcom 402 . . . . . . 7 (𝑐 ∈ (ClWalks‘𝐺) → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (𝑐𝐶 → ((♯‘𝐴) = 𝑁 → (𝐵 substr ⟨0, (♯‘𝐴)⟩) ∈ (𝑁 ClWWalksN 𝐺)))))
205204com24 95 . . . . . 6 (𝑐 ∈ (ClWalks‘𝐺) → ((♯‘𝐴) = 𝑁 → (𝑐𝐶 → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (𝐵 substr ⟨0, (♯‘𝐴)⟩) ∈ (𝑁 ClWWalksN 𝐺)))))
206205imp 395 . . . . 5 ((𝑐 ∈ (ClWalks‘𝐺) ∧ (♯‘𝐴) = 𝑁) → (𝑐𝐶 → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (𝐵 substr ⟨0, (♯‘𝐴)⟩) ∈ (𝑁 ClWWalksN 𝐺))))
2072, 206sylbi 208 . . . 4 (𝑐𝐶 → (𝑐𝐶 → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (𝐵 substr ⟨0, (♯‘𝐴)⟩) ∈ (𝑁 ClWWalksN 𝐺))))
208207pm2.43i 52 . . 3 (𝑐𝐶 → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (𝐵 substr ⟨0, (♯‘𝐴)⟩) ∈ (𝑁 ClWWalksN 𝐺)))
209208impcom 396 . 2 (((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) ∧ 𝑐𝐶) → (𝐵 substr ⟨0, (♯‘𝐴)⟩) ∈ (𝑁 ClWWalksN 𝐺))
210209, 14fmptd 6578 1 ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → 𝐹:𝐶⟶(𝑁 ClWWalksN 𝐺))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384  w3a 1107   = wceq 1652  wcel 2155  wne 2937  wral 3055  {crab 3059  cdif 3731  wss 3734  c0 4081  𝒫 cpw 4317  {csn 4336  {cpr 4338  cop 4342   class class class wbr 4811  cmpt 4890  dom cdm 5279  ran crn 5280  wf 6066  1-1wf1 6067  cfv 6070  (class class class)co 6846  1st c1st 7368  2nd c2nd 7369  cr 10192  0cc0 10193  1c1 10194   + caddc 10196  cle 10333  cmin 10525  cn 11279  2c2 11332  0cn0 11543  cz 11629  cuz 11893  ...cfz 12540  ..^cfzo 12680  chash 13328  Word cword 13493  lastSclsw 13541   substr csubstr 13624  cprime 15681  Vtxcvtx 26181  iEdgciedg 26182  Edgcedg 26232  UPGraphcupgr 26268  USGraphcusgr 26338  FinUSGraphcfusgr 26503  ClWalkscclwlks 26978  ClWWalkscclwwlk 27228   ClWWalksN cclwwlkn 27280
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-rep 4932  ax-sep 4943  ax-nul 4951  ax-pow 5003  ax-pr 5064  ax-un 7151  ax-cnex 10249  ax-resscn 10250  ax-1cn 10251  ax-icn 10252  ax-addcl 10253  ax-addrcl 10254  ax-mulcl 10255  ax-mulrcl 10256  ax-mulcom 10257  ax-addass 10258  ax-mulass 10259  ax-distr 10260  ax-i2m1 10261  ax-1ne0 10262  ax-1rid 10263  ax-rnegex 10264  ax-rrecex 10265  ax-cnre 10266  ax-pre-lttri 10267  ax-pre-lttrn 10268  ax-pre-ltadd 10269  ax-pre-mulgt0 10270  ax-pre-sup 10271
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-ifp 1086  df-3or 1108  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-nel 3041  df-ral 3060  df-rex 3061  df-reu 3062  df-rmo 3063  df-rab 3064  df-v 3352  df-sbc 3599  df-csb 3694  df-dif 3737  df-un 3739  df-in 3741  df-ss 3748  df-pss 3750  df-nul 4082  df-if 4246  df-pw 4319  df-sn 4337  df-pr 4339  df-tp 4341  df-op 4343  df-uni 4597  df-int 4636  df-iun 4680  df-br 4812  df-opab 4874  df-mpt 4891  df-tr 4914  df-id 5187  df-eprel 5192  df-po 5200  df-so 5201  df-fr 5238  df-we 5240  df-xp 5285  df-rel 5286  df-cnv 5287  df-co 5288  df-dm 5289  df-rn 5290  df-res 5291  df-ima 5292  df-pred 5867  df-ord 5913  df-on 5914  df-lim 5915  df-suc 5916  df-iota 6033  df-fun 6072  df-fn 6073  df-f 6074  df-f1 6075  df-fo 6076  df-f1o 6077  df-fv 6078  df-riota 6807  df-ov 6849  df-oprab 6850  df-mpt2 6851  df-om 7268  df-1st 7370  df-2nd 7371  df-wrecs 7614  df-recs 7676  df-rdg 7714  df-1o 7768  df-2o 7769  df-oadd 7772  df-er 7951  df-map 8066  df-pm 8067  df-en 8165  df-dom 8166  df-sdom 8167  df-fin 8168  df-sup 8559  df-card 9020  df-cda 9247  df-pnf 10334  df-mnf 10335  df-xr 10336  df-ltxr 10337  df-le 10338  df-sub 10527  df-neg 10528  df-div 10944  df-nn 11280  df-2 11340  df-3 11341  df-n0 11544  df-xnn0 11616  df-z 11630  df-uz 11894  df-rp 12036  df-fz 12541  df-fzo 12681  df-seq 13016  df-exp 13075  df-hash 13329  df-word 13494  df-lsw 13542  df-substr 13625  df-cj 14140  df-re 14141  df-im 14142  df-sqrt 14276  df-abs 14277  df-dvds 15282  df-prm 15682  df-edg 26233  df-uhgr 26246  df-upgr 26270  df-uspgr 26339  df-usgr 26340  df-fusgr 26504  df-wlks 26802  df-clwlks 26979  df-clwwlk 27229  df-clwwlkn 27282
This theorem is referenced by:  clwlksfoclwwlkOLD  27358  clwlksf1clwwlkOLD  27364
  Copyright terms: Public domain W3C validator