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

Theorem clwwlkext2edg 29576
Description: If a word concatenated with a vertex represents a closed walk in (in a graph), there is an edge between this vertex and the last vertex of the word, and between this vertex and the first vertex of the word. (Contributed by Alexander van der Vekens, 3-Oct-2018.) (Revised by AV, 27-Apr-2021.) (Proof shortened by AV, 22-Mar-2022.)
Hypotheses
Ref Expression
clwwlkext2edg.v 𝑉 = (Vtxβ€˜πΊ)
clwwlkext2edg.e 𝐸 = (Edgβ€˜πΊ)
Assertion
Ref Expression
clwwlkext2edg (((π‘Š ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (β„€β‰₯β€˜2)) ∧ (π‘Š ++ βŸ¨β€œπ‘β€βŸ©) ∈ (𝑁 ClWWalksN 𝐺)) β†’ ({(lastSβ€˜π‘Š), 𝑍} ∈ 𝐸 ∧ {𝑍, (π‘Šβ€˜0)} ∈ 𝐸))

Proof of Theorem clwwlkext2edg
Dummy variable 𝑖 is distinct from all other variables.
StepHypRef Expression
1 clwwlknnn 29553 . . 3 ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©) ∈ (𝑁 ClWWalksN 𝐺) β†’ 𝑁 ∈ β„•)
2 clwwlkext2edg.v . . . . 5 𝑉 = (Vtxβ€˜πΊ)
3 clwwlkext2edg.e . . . . 5 𝐸 = (Edgβ€˜πΊ)
42, 3isclwwlknx 29556 . . . 4 (𝑁 ∈ β„• β†’ ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©) ∈ (𝑁 ClWWalksN 𝐺) ↔ (((π‘Š ++ βŸ¨β€œπ‘β€βŸ©) ∈ Word 𝑉 ∧ βˆ€π‘– ∈ (0..^((β™―β€˜(π‘Š ++ βŸ¨β€œπ‘β€βŸ©)) βˆ’ 1)){((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜π‘–), ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜(𝑖 + 1))} ∈ 𝐸 ∧ {(lastSβ€˜(π‘Š ++ βŸ¨β€œπ‘β€βŸ©)), ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜0)} ∈ 𝐸) ∧ (β™―β€˜(π‘Š ++ βŸ¨β€œπ‘β€βŸ©)) = 𝑁)))
5 ige2m2fzo 13699 . . . . . . . . . . . . . . 15 (𝑁 ∈ (β„€β‰₯β€˜2) β†’ (𝑁 βˆ’ 2) ∈ (0..^(𝑁 βˆ’ 1)))
653ad2ant3 1133 . . . . . . . . . . . . . 14 ((π‘Š ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (β„€β‰₯β€˜2)) β†’ (𝑁 βˆ’ 2) ∈ (0..^(𝑁 βˆ’ 1)))
76adantr 479 . . . . . . . . . . . . 13 (((π‘Š ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (β„€β‰₯β€˜2)) ∧ (β™―β€˜(π‘Š ++ βŸ¨β€œπ‘β€βŸ©)) = 𝑁) β†’ (𝑁 βˆ’ 2) ∈ (0..^(𝑁 βˆ’ 1)))
8 oveq1 7418 . . . . . . . . . . . . . . . 16 ((β™―β€˜(π‘Š ++ βŸ¨β€œπ‘β€βŸ©)) = 𝑁 β†’ ((β™―β€˜(π‘Š ++ βŸ¨β€œπ‘β€βŸ©)) βˆ’ 1) = (𝑁 βˆ’ 1))
98oveq2d 7427 . . . . . . . . . . . . . . 15 ((β™―β€˜(π‘Š ++ βŸ¨β€œπ‘β€βŸ©)) = 𝑁 β†’ (0..^((β™―β€˜(π‘Š ++ βŸ¨β€œπ‘β€βŸ©)) βˆ’ 1)) = (0..^(𝑁 βˆ’ 1)))
109eleq2d 2817 . . . . . . . . . . . . . 14 ((β™―β€˜(π‘Š ++ βŸ¨β€œπ‘β€βŸ©)) = 𝑁 β†’ ((𝑁 βˆ’ 2) ∈ (0..^((β™―β€˜(π‘Š ++ βŸ¨β€œπ‘β€βŸ©)) βˆ’ 1)) ↔ (𝑁 βˆ’ 2) ∈ (0..^(𝑁 βˆ’ 1))))
1110adantl 480 . . . . . . . . . . . . 13 (((π‘Š ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (β„€β‰₯β€˜2)) ∧ (β™―β€˜(π‘Š ++ βŸ¨β€œπ‘β€βŸ©)) = 𝑁) β†’ ((𝑁 βˆ’ 2) ∈ (0..^((β™―β€˜(π‘Š ++ βŸ¨β€œπ‘β€βŸ©)) βˆ’ 1)) ↔ (𝑁 βˆ’ 2) ∈ (0..^(𝑁 βˆ’ 1))))
127, 11mpbird 256 . . . . . . . . . . . 12 (((π‘Š ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (β„€β‰₯β€˜2)) ∧ (β™―β€˜(π‘Š ++ βŸ¨β€œπ‘β€βŸ©)) = 𝑁) β†’ (𝑁 βˆ’ 2) ∈ (0..^((β™―β€˜(π‘Š ++ βŸ¨β€œπ‘β€βŸ©)) βˆ’ 1)))
13 fveq2 6890 . . . . . . . . . . . . . . 15 (𝑖 = (𝑁 βˆ’ 2) β†’ ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜π‘–) = ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜(𝑁 βˆ’ 2)))
14 fvoveq1 7434 . . . . . . . . . . . . . . 15 (𝑖 = (𝑁 βˆ’ 2) β†’ ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜(𝑖 + 1)) = ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜((𝑁 βˆ’ 2) + 1)))
1513, 14preq12d 4744 . . . . . . . . . . . . . 14 (𝑖 = (𝑁 βˆ’ 2) β†’ {((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜π‘–), ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜(𝑖 + 1))} = {((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜(𝑁 βˆ’ 2)), ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜((𝑁 βˆ’ 2) + 1))})
1615eleq1d 2816 . . . . . . . . . . . . 13 (𝑖 = (𝑁 βˆ’ 2) β†’ ({((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜π‘–), ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜(𝑖 + 1))} ∈ 𝐸 ↔ {((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜(𝑁 βˆ’ 2)), ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜((𝑁 βˆ’ 2) + 1))} ∈ 𝐸))
1716rspcv 3607 . . . . . . . . . . . 12 ((𝑁 βˆ’ 2) ∈ (0..^((β™―β€˜(π‘Š ++ βŸ¨β€œπ‘β€βŸ©)) βˆ’ 1)) β†’ (βˆ€π‘– ∈ (0..^((β™―β€˜(π‘Š ++ βŸ¨β€œπ‘β€βŸ©)) βˆ’ 1)){((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜π‘–), ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜(𝑖 + 1))} ∈ 𝐸 β†’ {((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜(𝑁 βˆ’ 2)), ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜((𝑁 βˆ’ 2) + 1))} ∈ 𝐸))
1812, 17syl 17 . . . . . . . . . . 11 (((π‘Š ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (β„€β‰₯β€˜2)) ∧ (β™―β€˜(π‘Š ++ βŸ¨β€œπ‘β€βŸ©)) = 𝑁) β†’ (βˆ€π‘– ∈ (0..^((β™―β€˜(π‘Š ++ βŸ¨β€œπ‘β€βŸ©)) βˆ’ 1)){((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜π‘–), ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜(𝑖 + 1))} ∈ 𝐸 β†’ {((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜(𝑁 βˆ’ 2)), ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜((𝑁 βˆ’ 2) + 1))} ∈ 𝐸))
19 wrdlenccats1lenm1 14576 . . . . . . . . . . . . . . . . . . . . . 22 (π‘Š ∈ Word 𝑉 β†’ ((β™―β€˜(π‘Š ++ βŸ¨β€œπ‘β€βŸ©)) βˆ’ 1) = (β™―β€˜π‘Š))
2019eqcomd 2736 . . . . . . . . . . . . . . . . . . . . 21 (π‘Š ∈ Word 𝑉 β†’ (β™―β€˜π‘Š) = ((β™―β€˜(π‘Š ++ βŸ¨β€œπ‘β€βŸ©)) βˆ’ 1))
2120adantr 479 . . . . . . . . . . . . . . . . . . . 20 ((π‘Š ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉) β†’ (β™―β€˜π‘Š) = ((β™―β€˜(π‘Š ++ βŸ¨β€œπ‘β€βŸ©)) βˆ’ 1))
2221, 8sylan9eq 2790 . . . . . . . . . . . . . . . . . . 19 (((π‘Š ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉) ∧ (β™―β€˜(π‘Š ++ βŸ¨β€œπ‘β€βŸ©)) = 𝑁) β†’ (β™―β€˜π‘Š) = (𝑁 βˆ’ 1))
2322ex 411 . . . . . . . . . . . . . . . . . 18 ((π‘Š ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉) β†’ ((β™―β€˜(π‘Š ++ βŸ¨β€œπ‘β€βŸ©)) = 𝑁 β†’ (β™―β€˜π‘Š) = (𝑁 βˆ’ 1)))
24233adant3 1130 . . . . . . . . . . . . . . . . 17 ((π‘Š ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (β„€β‰₯β€˜2)) β†’ ((β™―β€˜(π‘Š ++ βŸ¨β€œπ‘β€βŸ©)) = 𝑁 β†’ (β™―β€˜π‘Š) = (𝑁 βˆ’ 1)))
25 eluzelcn 12838 . . . . . . . . . . . . . . . . . . . . . 22 (𝑁 ∈ (β„€β‰₯β€˜2) β†’ 𝑁 ∈ β„‚)
26 1cnd 11213 . . . . . . . . . . . . . . . . . . . . . 22 (𝑁 ∈ (β„€β‰₯β€˜2) β†’ 1 ∈ β„‚)
2725, 26, 26subsub4d 11606 . . . . . . . . . . . . . . . . . . . . 21 (𝑁 ∈ (β„€β‰₯β€˜2) β†’ ((𝑁 βˆ’ 1) βˆ’ 1) = (𝑁 βˆ’ (1 + 1)))
28 1p1e2 12341 . . . . . . . . . . . . . . . . . . . . . . 23 (1 + 1) = 2
2928a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (𝑁 ∈ (β„€β‰₯β€˜2) β†’ (1 + 1) = 2)
3029oveq2d 7427 . . . . . . . . . . . . . . . . . . . . 21 (𝑁 ∈ (β„€β‰₯β€˜2) β†’ (𝑁 βˆ’ (1 + 1)) = (𝑁 βˆ’ 2))
3127, 30eqtr2d 2771 . . . . . . . . . . . . . . . . . . . 20 (𝑁 ∈ (β„€β‰₯β€˜2) β†’ (𝑁 βˆ’ 2) = ((𝑁 βˆ’ 1) βˆ’ 1))
32313ad2ant3 1133 . . . . . . . . . . . . . . . . . . 19 ((π‘Š ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (β„€β‰₯β€˜2)) β†’ (𝑁 βˆ’ 2) = ((𝑁 βˆ’ 1) βˆ’ 1))
33 oveq1 7418 . . . . . . . . . . . . . . . . . . . 20 ((β™―β€˜π‘Š) = (𝑁 βˆ’ 1) β†’ ((β™―β€˜π‘Š) βˆ’ 1) = ((𝑁 βˆ’ 1) βˆ’ 1))
3433eqcomd 2736 . . . . . . . . . . . . . . . . . . 19 ((β™―β€˜π‘Š) = (𝑁 βˆ’ 1) β†’ ((𝑁 βˆ’ 1) βˆ’ 1) = ((β™―β€˜π‘Š) βˆ’ 1))
3532, 34sylan9eq 2790 . . . . . . . . . . . . . . . . . 18 (((π‘Š ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (β„€β‰₯β€˜2)) ∧ (β™―β€˜π‘Š) = (𝑁 βˆ’ 1)) β†’ (𝑁 βˆ’ 2) = ((β™―β€˜π‘Š) βˆ’ 1))
3635ex 411 . . . . . . . . . . . . . . . . 17 ((π‘Š ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (β„€β‰₯β€˜2)) β†’ ((β™―β€˜π‘Š) = (𝑁 βˆ’ 1) β†’ (𝑁 βˆ’ 2) = ((β™―β€˜π‘Š) βˆ’ 1)))
3724, 36syld 47 . . . . . . . . . . . . . . . 16 ((π‘Š ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (β„€β‰₯β€˜2)) β†’ ((β™―β€˜(π‘Š ++ βŸ¨β€œπ‘β€βŸ©)) = 𝑁 β†’ (𝑁 βˆ’ 2) = ((β™―β€˜π‘Š) βˆ’ 1)))
3837imp 405 . . . . . . . . . . . . . . 15 (((π‘Š ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (β„€β‰₯β€˜2)) ∧ (β™―β€˜(π‘Š ++ βŸ¨β€œπ‘β€βŸ©)) = 𝑁) β†’ (𝑁 βˆ’ 2) = ((β™―β€˜π‘Š) βˆ’ 1))
3938fveq2d 6894 . . . . . . . . . . . . . 14 (((π‘Š ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (β„€β‰₯β€˜2)) ∧ (β™―β€˜(π‘Š ++ βŸ¨β€œπ‘β€βŸ©)) = 𝑁) β†’ ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜(𝑁 βˆ’ 2)) = ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜((β™―β€˜π‘Š) βˆ’ 1)))
40 simpl1 1189 . . . . . . . . . . . . . . . . . . 19 (((π‘Š ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (β„€β‰₯β€˜2)) ∧ (β™―β€˜π‘Š) = (𝑁 βˆ’ 1)) β†’ π‘Š ∈ Word 𝑉)
41 s1cl 14556 . . . . . . . . . . . . . . . . . . . . 21 (𝑍 ∈ 𝑉 β†’ βŸ¨β€œπ‘β€βŸ© ∈ Word 𝑉)
42413ad2ant2 1132 . . . . . . . . . . . . . . . . . . . 20 ((π‘Š ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (β„€β‰₯β€˜2)) β†’ βŸ¨β€œπ‘β€βŸ© ∈ Word 𝑉)
4342adantr 479 . . . . . . . . . . . . . . . . . . 19 (((π‘Š ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (β„€β‰₯β€˜2)) ∧ (β™―β€˜π‘Š) = (𝑁 βˆ’ 1)) β†’ βŸ¨β€œπ‘β€βŸ© ∈ Word 𝑉)
44 eluz2 12832 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑁 ∈ (β„€β‰₯β€˜2) ↔ (2 ∈ β„€ ∧ 𝑁 ∈ β„€ ∧ 2 ≀ 𝑁))
45 zre 12566 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑁 ∈ β„€ β†’ 𝑁 ∈ ℝ)
46 1red 11219 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑁 ∈ ℝ ∧ 2 ≀ 𝑁) β†’ 1 ∈ ℝ)
47 2re 12290 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 2 ∈ ℝ
4847a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑁 ∈ ℝ ∧ 2 ≀ 𝑁) β†’ 2 ∈ ℝ)
49 simpl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑁 ∈ ℝ ∧ 2 ≀ 𝑁) β†’ 𝑁 ∈ ℝ)
50 1lt2 12387 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 1 < 2
5150a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑁 ∈ ℝ ∧ 2 ≀ 𝑁) β†’ 1 < 2)
52 simpr 483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑁 ∈ ℝ ∧ 2 ≀ 𝑁) β†’ 2 ≀ 𝑁)
5346, 48, 49, 51, 52ltletrd 11378 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑁 ∈ ℝ ∧ 2 ≀ 𝑁) β†’ 1 < 𝑁)
54 1red 11219 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑁 ∈ ℝ β†’ 1 ∈ ℝ)
55 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑁 ∈ ℝ β†’ 𝑁 ∈ ℝ)
5654, 55posdifd 11805 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑁 ∈ ℝ β†’ (1 < 𝑁 ↔ 0 < (𝑁 βˆ’ 1)))
5756adantr 479 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑁 ∈ ℝ ∧ 2 ≀ 𝑁) β†’ (1 < 𝑁 ↔ 0 < (𝑁 βˆ’ 1)))
5853, 57mpbid 231 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑁 ∈ ℝ ∧ 2 ≀ 𝑁) β†’ 0 < (𝑁 βˆ’ 1))
5958ex 411 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑁 ∈ ℝ β†’ (2 ≀ 𝑁 β†’ 0 < (𝑁 βˆ’ 1)))
6045, 59syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑁 ∈ β„€ β†’ (2 ≀ 𝑁 β†’ 0 < (𝑁 βˆ’ 1)))
6160a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 (2 ∈ β„€ β†’ (𝑁 ∈ β„€ β†’ (2 ≀ 𝑁 β†’ 0 < (𝑁 βˆ’ 1))))
62613imp 1109 . . . . . . . . . . . . . . . . . . . . . . . 24 ((2 ∈ β„€ ∧ 𝑁 ∈ β„€ ∧ 2 ≀ 𝑁) β†’ 0 < (𝑁 βˆ’ 1))
6344, 62sylbi 216 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑁 ∈ (β„€β‰₯β€˜2) β†’ 0 < (𝑁 βˆ’ 1))
6463ad2antlr 723 . . . . . . . . . . . . . . . . . . . . . 22 (((π‘Š ∈ Word 𝑉 ∧ 𝑁 ∈ (β„€β‰₯β€˜2)) ∧ (β™―β€˜π‘Š) = (𝑁 βˆ’ 1)) β†’ 0 < (𝑁 βˆ’ 1))
65 breq2 5151 . . . . . . . . . . . . . . . . . . . . . . 23 ((β™―β€˜π‘Š) = (𝑁 βˆ’ 1) β†’ (0 < (β™―β€˜π‘Š) ↔ 0 < (𝑁 βˆ’ 1)))
6665adantl 480 . . . . . . . . . . . . . . . . . . . . . 22 (((π‘Š ∈ Word 𝑉 ∧ 𝑁 ∈ (β„€β‰₯β€˜2)) ∧ (β™―β€˜π‘Š) = (𝑁 βˆ’ 1)) β†’ (0 < (β™―β€˜π‘Š) ↔ 0 < (𝑁 βˆ’ 1)))
6764, 66mpbird 256 . . . . . . . . . . . . . . . . . . . . 21 (((π‘Š ∈ Word 𝑉 ∧ 𝑁 ∈ (β„€β‰₯β€˜2)) ∧ (β™―β€˜π‘Š) = (𝑁 βˆ’ 1)) β†’ 0 < (β™―β€˜π‘Š))
68 hashneq0 14328 . . . . . . . . . . . . . . . . . . . . . . 23 (π‘Š ∈ Word 𝑉 β†’ (0 < (β™―β€˜π‘Š) ↔ π‘Š β‰  βˆ…))
6968adantr 479 . . . . . . . . . . . . . . . . . . . . . 22 ((π‘Š ∈ Word 𝑉 ∧ 𝑁 ∈ (β„€β‰₯β€˜2)) β†’ (0 < (β™―β€˜π‘Š) ↔ π‘Š β‰  βˆ…))
7069adantr 479 . . . . . . . . . . . . . . . . . . . . 21 (((π‘Š ∈ Word 𝑉 ∧ 𝑁 ∈ (β„€β‰₯β€˜2)) ∧ (β™―β€˜π‘Š) = (𝑁 βˆ’ 1)) β†’ (0 < (β™―β€˜π‘Š) ↔ π‘Š β‰  βˆ…))
7167, 70mpbid 231 . . . . . . . . . . . . . . . . . . . 20 (((π‘Š ∈ Word 𝑉 ∧ 𝑁 ∈ (β„€β‰₯β€˜2)) ∧ (β™―β€˜π‘Š) = (𝑁 βˆ’ 1)) β†’ π‘Š β‰  βˆ…)
72713adantl2 1165 . . . . . . . . . . . . . . . . . . 19 (((π‘Š ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (β„€β‰₯β€˜2)) ∧ (β™―β€˜π‘Š) = (𝑁 βˆ’ 1)) β†’ π‘Š β‰  βˆ…)
7340, 43, 723jca 1126 . . . . . . . . . . . . . . . . . 18 (((π‘Š ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (β„€β‰₯β€˜2)) ∧ (β™―β€˜π‘Š) = (𝑁 βˆ’ 1)) β†’ (π‘Š ∈ Word 𝑉 ∧ βŸ¨β€œπ‘β€βŸ© ∈ Word 𝑉 ∧ π‘Š β‰  βˆ…))
7473ex 411 . . . . . . . . . . . . . . . . 17 ((π‘Š ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (β„€β‰₯β€˜2)) β†’ ((β™―β€˜π‘Š) = (𝑁 βˆ’ 1) β†’ (π‘Š ∈ Word 𝑉 ∧ βŸ¨β€œπ‘β€βŸ© ∈ Word 𝑉 ∧ π‘Š β‰  βˆ…)))
7524, 74syld 47 . . . . . . . . . . . . . . . 16 ((π‘Š ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (β„€β‰₯β€˜2)) β†’ ((β™―β€˜(π‘Š ++ βŸ¨β€œπ‘β€βŸ©)) = 𝑁 β†’ (π‘Š ∈ Word 𝑉 ∧ βŸ¨β€œπ‘β€βŸ© ∈ Word 𝑉 ∧ π‘Š β‰  βˆ…)))
7675imp 405 . . . . . . . . . . . . . . 15 (((π‘Š ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (β„€β‰₯β€˜2)) ∧ (β™―β€˜(π‘Š ++ βŸ¨β€œπ‘β€βŸ©)) = 𝑁) β†’ (π‘Š ∈ Word 𝑉 ∧ βŸ¨β€œπ‘β€βŸ© ∈ Word 𝑉 ∧ π‘Š β‰  βˆ…))
77 ccatval1lsw 14538 . . . . . . . . . . . . . . 15 ((π‘Š ∈ Word 𝑉 ∧ βŸ¨β€œπ‘β€βŸ© ∈ Word 𝑉 ∧ π‘Š β‰  βˆ…) β†’ ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜((β™―β€˜π‘Š) βˆ’ 1)) = (lastSβ€˜π‘Š))
7876, 77syl 17 . . . . . . . . . . . . . 14 (((π‘Š ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (β„€β‰₯β€˜2)) ∧ (β™―β€˜(π‘Š ++ βŸ¨β€œπ‘β€βŸ©)) = 𝑁) β†’ ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜((β™―β€˜π‘Š) βˆ’ 1)) = (lastSβ€˜π‘Š))
7939, 78eqtrd 2770 . . . . . . . . . . . . 13 (((π‘Š ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (β„€β‰₯β€˜2)) ∧ (β™―β€˜(π‘Š ++ βŸ¨β€œπ‘β€βŸ©)) = 𝑁) β†’ ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜(𝑁 βˆ’ 2)) = (lastSβ€˜π‘Š))
80 2m1e1 12342 . . . . . . . . . . . . . . . . . . . . . . 23 (2 βˆ’ 1) = 1
8180a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (𝑁 ∈ (β„€β‰₯β€˜2) β†’ (2 βˆ’ 1) = 1)
8281eqcomd 2736 . . . . . . . . . . . . . . . . . . . . 21 (𝑁 ∈ (β„€β‰₯β€˜2) β†’ 1 = (2 βˆ’ 1))
8382oveq2d 7427 . . . . . . . . . . . . . . . . . . . 20 (𝑁 ∈ (β„€β‰₯β€˜2) β†’ (𝑁 βˆ’ 1) = (𝑁 βˆ’ (2 βˆ’ 1)))
84 2cnd 12294 . . . . . . . . . . . . . . . . . . . . 21 (𝑁 ∈ (β„€β‰₯β€˜2) β†’ 2 ∈ β„‚)
8525, 84, 26subsubd 11603 . . . . . . . . . . . . . . . . . . . 20 (𝑁 ∈ (β„€β‰₯β€˜2) β†’ (𝑁 βˆ’ (2 βˆ’ 1)) = ((𝑁 βˆ’ 2) + 1))
8683, 85eqtr2d 2771 . . . . . . . . . . . . . . . . . . 19 (𝑁 ∈ (β„€β‰₯β€˜2) β†’ ((𝑁 βˆ’ 2) + 1) = (𝑁 βˆ’ 1))
87863ad2ant3 1133 . . . . . . . . . . . . . . . . . 18 ((π‘Š ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (β„€β‰₯β€˜2)) β†’ ((𝑁 βˆ’ 2) + 1) = (𝑁 βˆ’ 1))
88 eqeq2 2742 . . . . . . . . . . . . . . . . . 18 ((β™―β€˜π‘Š) = (𝑁 βˆ’ 1) β†’ (((𝑁 βˆ’ 2) + 1) = (β™―β€˜π‘Š) ↔ ((𝑁 βˆ’ 2) + 1) = (𝑁 βˆ’ 1)))
8987, 88syl5ibrcom 246 . . . . . . . . . . . . . . . . 17 ((π‘Š ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (β„€β‰₯β€˜2)) β†’ ((β™―β€˜π‘Š) = (𝑁 βˆ’ 1) β†’ ((𝑁 βˆ’ 2) + 1) = (β™―β€˜π‘Š)))
9024, 89syld 47 . . . . . . . . . . . . . . . 16 ((π‘Š ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (β„€β‰₯β€˜2)) β†’ ((β™―β€˜(π‘Š ++ βŸ¨β€œπ‘β€βŸ©)) = 𝑁 β†’ ((𝑁 βˆ’ 2) + 1) = (β™―β€˜π‘Š)))
9190imp 405 . . . . . . . . . . . . . . 15 (((π‘Š ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (β„€β‰₯β€˜2)) ∧ (β™―β€˜(π‘Š ++ βŸ¨β€œπ‘β€βŸ©)) = 𝑁) β†’ ((𝑁 βˆ’ 2) + 1) = (β™―β€˜π‘Š))
9291fveq2d 6894 . . . . . . . . . . . . . 14 (((π‘Š ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (β„€β‰₯β€˜2)) ∧ (β™―β€˜(π‘Š ++ βŸ¨β€œπ‘β€βŸ©)) = 𝑁) β†’ ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜((𝑁 βˆ’ 2) + 1)) = ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜(β™―β€˜π‘Š)))
93 id 22 . . . . . . . . . . . . . . . . 17 ((π‘Š ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉) β†’ (π‘Š ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉))
94933adant3 1130 . . . . . . . . . . . . . . . 16 ((π‘Š ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (β„€β‰₯β€˜2)) β†’ (π‘Š ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉))
9594adantr 479 . . . . . . . . . . . . . . 15 (((π‘Š ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (β„€β‰₯β€˜2)) ∧ (β™―β€˜(π‘Š ++ βŸ¨β€œπ‘β€βŸ©)) = 𝑁) β†’ (π‘Š ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉))
96 ccatws1ls 14587 . . . . . . . . . . . . . . 15 ((π‘Š ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉) β†’ ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜(β™―β€˜π‘Š)) = 𝑍)
9795, 96syl 17 . . . . . . . . . . . . . 14 (((π‘Š ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (β„€β‰₯β€˜2)) ∧ (β™―β€˜(π‘Š ++ βŸ¨β€œπ‘β€βŸ©)) = 𝑁) β†’ ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜(β™―β€˜π‘Š)) = 𝑍)
9892, 97eqtrd 2770 . . . . . . . . . . . . 13 (((π‘Š ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (β„€β‰₯β€˜2)) ∧ (β™―β€˜(π‘Š ++ βŸ¨β€œπ‘β€βŸ©)) = 𝑁) β†’ ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜((𝑁 βˆ’ 2) + 1)) = 𝑍)
9979, 98preq12d 4744 . . . . . . . . . . . 12 (((π‘Š ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (β„€β‰₯β€˜2)) ∧ (β™―β€˜(π‘Š ++ βŸ¨β€œπ‘β€βŸ©)) = 𝑁) β†’ {((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜(𝑁 βˆ’ 2)), ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜((𝑁 βˆ’ 2) + 1))} = {(lastSβ€˜π‘Š), 𝑍})
10099eleq1d 2816 . . . . . . . . . . 11 (((π‘Š ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (β„€β‰₯β€˜2)) ∧ (β™―β€˜(π‘Š ++ βŸ¨β€œπ‘β€βŸ©)) = 𝑁) β†’ ({((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜(𝑁 βˆ’ 2)), ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜((𝑁 βˆ’ 2) + 1))} ∈ 𝐸 ↔ {(lastSβ€˜π‘Š), 𝑍} ∈ 𝐸))
10118, 100sylibd 238 . . . . . . . . . 10 (((π‘Š ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (β„€β‰₯β€˜2)) ∧ (β™―β€˜(π‘Š ++ βŸ¨β€œπ‘β€βŸ©)) = 𝑁) β†’ (βˆ€π‘– ∈ (0..^((β™―β€˜(π‘Š ++ βŸ¨β€œπ‘β€βŸ©)) βˆ’ 1)){((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜π‘–), ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜(𝑖 + 1))} ∈ 𝐸 β†’ {(lastSβ€˜π‘Š), 𝑍} ∈ 𝐸))
102101ex 411 . . . . . . . . 9 ((π‘Š ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (β„€β‰₯β€˜2)) β†’ ((β™―β€˜(π‘Š ++ βŸ¨β€œπ‘β€βŸ©)) = 𝑁 β†’ (βˆ€π‘– ∈ (0..^((β™―β€˜(π‘Š ++ βŸ¨β€œπ‘β€βŸ©)) βˆ’ 1)){((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜π‘–), ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜(𝑖 + 1))} ∈ 𝐸 β†’ {(lastSβ€˜π‘Š), 𝑍} ∈ 𝐸)))
103102com13 88 . . . . . . . 8 (βˆ€π‘– ∈ (0..^((β™―β€˜(π‘Š ++ βŸ¨β€œπ‘β€βŸ©)) βˆ’ 1)){((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜π‘–), ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜(𝑖 + 1))} ∈ 𝐸 β†’ ((β™―β€˜(π‘Š ++ βŸ¨β€œπ‘β€βŸ©)) = 𝑁 β†’ ((π‘Š ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (β„€β‰₯β€˜2)) β†’ {(lastSβ€˜π‘Š), 𝑍} ∈ 𝐸)))
1041033ad2ant2 1132 . . . . . . 7 (((π‘Š ++ βŸ¨β€œπ‘β€βŸ©) ∈ Word 𝑉 ∧ βˆ€π‘– ∈ (0..^((β™―β€˜(π‘Š ++ βŸ¨β€œπ‘β€βŸ©)) βˆ’ 1)){((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜π‘–), ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜(𝑖 + 1))} ∈ 𝐸 ∧ {(lastSβ€˜(π‘Š ++ βŸ¨β€œπ‘β€βŸ©)), ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜0)} ∈ 𝐸) β†’ ((β™―β€˜(π‘Š ++ βŸ¨β€œπ‘β€βŸ©)) = 𝑁 β†’ ((π‘Š ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (β„€β‰₯β€˜2)) β†’ {(lastSβ€˜π‘Š), 𝑍} ∈ 𝐸)))
105104imp31 416 . . . . . 6 (((((π‘Š ++ βŸ¨β€œπ‘β€βŸ©) ∈ Word 𝑉 ∧ βˆ€π‘– ∈ (0..^((β™―β€˜(π‘Š ++ βŸ¨β€œπ‘β€βŸ©)) βˆ’ 1)){((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜π‘–), ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜(𝑖 + 1))} ∈ 𝐸 ∧ {(lastSβ€˜(π‘Š ++ βŸ¨β€œπ‘β€βŸ©)), ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜0)} ∈ 𝐸) ∧ (β™―β€˜(π‘Š ++ βŸ¨β€œπ‘β€βŸ©)) = 𝑁) ∧ (π‘Š ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (β„€β‰₯β€˜2))) β†’ {(lastSβ€˜π‘Š), 𝑍} ∈ 𝐸)
10694adantr 479 . . . . . . . . . . . . . . 15 (((π‘Š ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (β„€β‰₯β€˜2)) ∧ (β™―β€˜π‘Š) = (𝑁 βˆ’ 1)) β†’ (π‘Š ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉))
107 lswccats1 14588 . . . . . . . . . . . . . . 15 ((π‘Š ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉) β†’ (lastSβ€˜(π‘Š ++ βŸ¨β€œπ‘β€βŸ©)) = 𝑍)
108106, 107syl 17 . . . . . . . . . . . . . 14 (((π‘Š ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (β„€β‰₯β€˜2)) ∧ (β™―β€˜π‘Š) = (𝑁 βˆ’ 1)) β†’ (lastSβ€˜(π‘Š ++ βŸ¨β€œπ‘β€βŸ©)) = 𝑍)
109633ad2ant3 1133 . . . . . . . . . . . . . . . . 17 ((π‘Š ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (β„€β‰₯β€˜2)) β†’ 0 < (𝑁 βˆ’ 1))
110109adantr 479 . . . . . . . . . . . . . . . 16 (((π‘Š ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (β„€β‰₯β€˜2)) ∧ (β™―β€˜π‘Š) = (𝑁 βˆ’ 1)) β†’ 0 < (𝑁 βˆ’ 1))
11165adantl 480 . . . . . . . . . . . . . . . 16 (((π‘Š ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (β„€β‰₯β€˜2)) ∧ (β™―β€˜π‘Š) = (𝑁 βˆ’ 1)) β†’ (0 < (β™―β€˜π‘Š) ↔ 0 < (𝑁 βˆ’ 1)))
112110, 111mpbird 256 . . . . . . . . . . . . . . 15 (((π‘Š ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (β„€β‰₯β€˜2)) ∧ (β™―β€˜π‘Š) = (𝑁 βˆ’ 1)) β†’ 0 < (β™―β€˜π‘Š))
113 ccatfv0 14537 . . . . . . . . . . . . . . 15 ((π‘Š ∈ Word 𝑉 ∧ βŸ¨β€œπ‘β€βŸ© ∈ Word 𝑉 ∧ 0 < (β™―β€˜π‘Š)) β†’ ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜0) = (π‘Šβ€˜0))
11440, 43, 112, 113syl3anc 1369 . . . . . . . . . . . . . 14 (((π‘Š ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (β„€β‰₯β€˜2)) ∧ (β™―β€˜π‘Š) = (𝑁 βˆ’ 1)) β†’ ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜0) = (π‘Šβ€˜0))
115108, 114preq12d 4744 . . . . . . . . . . . . 13 (((π‘Š ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (β„€β‰₯β€˜2)) ∧ (β™―β€˜π‘Š) = (𝑁 βˆ’ 1)) β†’ {(lastSβ€˜(π‘Š ++ βŸ¨β€œπ‘β€βŸ©)), ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜0)} = {𝑍, (π‘Šβ€˜0)})
116115ex 411 . . . . . . . . . . . 12 ((π‘Š ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (β„€β‰₯β€˜2)) β†’ ((β™―β€˜π‘Š) = (𝑁 βˆ’ 1) β†’ {(lastSβ€˜(π‘Š ++ βŸ¨β€œπ‘β€βŸ©)), ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜0)} = {𝑍, (π‘Šβ€˜0)}))
11724, 116syld 47 . . . . . . . . . . 11 ((π‘Š ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (β„€β‰₯β€˜2)) β†’ ((β™―β€˜(π‘Š ++ βŸ¨β€œπ‘β€βŸ©)) = 𝑁 β†’ {(lastSβ€˜(π‘Š ++ βŸ¨β€œπ‘β€βŸ©)), ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜0)} = {𝑍, (π‘Šβ€˜0)}))
118117impcom 406 . . . . . . . . . 10 (((β™―β€˜(π‘Š ++ βŸ¨β€œπ‘β€βŸ©)) = 𝑁 ∧ (π‘Š ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (β„€β‰₯β€˜2))) β†’ {(lastSβ€˜(π‘Š ++ βŸ¨β€œπ‘β€βŸ©)), ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜0)} = {𝑍, (π‘Šβ€˜0)})
119118eleq1d 2816 . . . . . . . . 9 (((β™―β€˜(π‘Š ++ βŸ¨β€œπ‘β€βŸ©)) = 𝑁 ∧ (π‘Š ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (β„€β‰₯β€˜2))) β†’ ({(lastSβ€˜(π‘Š ++ βŸ¨β€œπ‘β€βŸ©)), ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜0)} ∈ 𝐸 ↔ {𝑍, (π‘Šβ€˜0)} ∈ 𝐸))
120119biimpcd 248 . . . . . . . 8 ({(lastSβ€˜(π‘Š ++ βŸ¨β€œπ‘β€βŸ©)), ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜0)} ∈ 𝐸 β†’ (((β™―β€˜(π‘Š ++ βŸ¨β€œπ‘β€βŸ©)) = 𝑁 ∧ (π‘Š ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (β„€β‰₯β€˜2))) β†’ {𝑍, (π‘Šβ€˜0)} ∈ 𝐸))
1211203ad2ant3 1133 . . . . . . 7 (((π‘Š ++ βŸ¨β€œπ‘β€βŸ©) ∈ Word 𝑉 ∧ βˆ€π‘– ∈ (0..^((β™―β€˜(π‘Š ++ βŸ¨β€œπ‘β€βŸ©)) βˆ’ 1)){((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜π‘–), ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜(𝑖 + 1))} ∈ 𝐸 ∧ {(lastSβ€˜(π‘Š ++ βŸ¨β€œπ‘β€βŸ©)), ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜0)} ∈ 𝐸) β†’ (((β™―β€˜(π‘Š ++ βŸ¨β€œπ‘β€βŸ©)) = 𝑁 ∧ (π‘Š ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (β„€β‰₯β€˜2))) β†’ {𝑍, (π‘Šβ€˜0)} ∈ 𝐸))
122121impl 454 . . . . . 6 (((((π‘Š ++ βŸ¨β€œπ‘β€βŸ©) ∈ Word 𝑉 ∧ βˆ€π‘– ∈ (0..^((β™―β€˜(π‘Š ++ βŸ¨β€œπ‘β€βŸ©)) βˆ’ 1)){((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜π‘–), ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜(𝑖 + 1))} ∈ 𝐸 ∧ {(lastSβ€˜(π‘Š ++ βŸ¨β€œπ‘β€βŸ©)), ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜0)} ∈ 𝐸) ∧ (β™―β€˜(π‘Š ++ βŸ¨β€œπ‘β€βŸ©)) = 𝑁) ∧ (π‘Š ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (β„€β‰₯β€˜2))) β†’ {𝑍, (π‘Šβ€˜0)} ∈ 𝐸)
123105, 122jca 510 . . . . 5 (((((π‘Š ++ βŸ¨β€œπ‘β€βŸ©) ∈ Word 𝑉 ∧ βˆ€π‘– ∈ (0..^((β™―β€˜(π‘Š ++ βŸ¨β€œπ‘β€βŸ©)) βˆ’ 1)){((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜π‘–), ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜(𝑖 + 1))} ∈ 𝐸 ∧ {(lastSβ€˜(π‘Š ++ βŸ¨β€œπ‘β€βŸ©)), ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜0)} ∈ 𝐸) ∧ (β™―β€˜(π‘Š ++ βŸ¨β€œπ‘β€βŸ©)) = 𝑁) ∧ (π‘Š ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (β„€β‰₯β€˜2))) β†’ ({(lastSβ€˜π‘Š), 𝑍} ∈ 𝐸 ∧ {𝑍, (π‘Šβ€˜0)} ∈ 𝐸))
124123ex 411 . . . 4 ((((π‘Š ++ βŸ¨β€œπ‘β€βŸ©) ∈ Word 𝑉 ∧ βˆ€π‘– ∈ (0..^((β™―β€˜(π‘Š ++ βŸ¨β€œπ‘β€βŸ©)) βˆ’ 1)){((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜π‘–), ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜(𝑖 + 1))} ∈ 𝐸 ∧ {(lastSβ€˜(π‘Š ++ βŸ¨β€œπ‘β€βŸ©)), ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜0)} ∈ 𝐸) ∧ (β™―β€˜(π‘Š ++ βŸ¨β€œπ‘β€βŸ©)) = 𝑁) β†’ ((π‘Š ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (β„€β‰₯β€˜2)) β†’ ({(lastSβ€˜π‘Š), 𝑍} ∈ 𝐸 ∧ {𝑍, (π‘Šβ€˜0)} ∈ 𝐸)))
1254, 124syl6bi 252 . . 3 (𝑁 ∈ β„• β†’ ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©) ∈ (𝑁 ClWWalksN 𝐺) β†’ ((π‘Š ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (β„€β‰₯β€˜2)) β†’ ({(lastSβ€˜π‘Š), 𝑍} ∈ 𝐸 ∧ {𝑍, (π‘Šβ€˜0)} ∈ 𝐸))))
1261, 125mpcom 38 . 2 ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©) ∈ (𝑁 ClWWalksN 𝐺) β†’ ((π‘Š ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (β„€β‰₯β€˜2)) β†’ ({(lastSβ€˜π‘Š), 𝑍} ∈ 𝐸 ∧ {𝑍, (π‘Šβ€˜0)} ∈ 𝐸)))
127126impcom 406 1 (((π‘Š ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (β„€β‰₯β€˜2)) ∧ (π‘Š ++ βŸ¨β€œπ‘β€βŸ©) ∈ (𝑁 ClWWalksN 𝐺)) β†’ ({(lastSβ€˜π‘Š), 𝑍} ∈ 𝐸 ∧ {𝑍, (π‘Šβ€˜0)} ∈ 𝐸))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 394   ∧ w3a 1085   = wceq 1539   ∈ wcel 2104   β‰  wne 2938  βˆ€wral 3059  βˆ…c0 4321  {cpr 4629   class class class wbr 5147  β€˜cfv 6542  (class class class)co 7411  β„cr 11111  0cc0 11112  1c1 11113   + caddc 11115   < clt 11252   ≀ cle 11253   βˆ’ cmin 11448  β„•cn 12216  2c2 12271  β„€cz 12562  β„€β‰₯cuz 12826  ..^cfzo 13631  β™―chash 14294  Word cword 14468  lastSclsw 14516   ++ cconcat 14524  βŸ¨β€œcs1 14549  Vtxcvtx 28523  Edgcedg 28574   ClWWalksN cclwwlkn 29544
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7727  ax-cnex 11168  ax-resscn 11169  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-addrcl 11173  ax-mulcl 11174  ax-mulrcl 11175  ax-mulcom 11176  ax-addass 11177  ax-mulass 11178  ax-distr 11179  ax-i2m1 11180  ax-1ne0 11181  ax-1rid 11182  ax-rnegex 11183  ax-rrecex 11184  ax-cnre 11185  ax-pre-lttri 11186  ax-pre-lttrn 11187  ax-pre-ltadd 11188  ax-pre-mulgt0 11189
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-nel 3045  df-ral 3060  df-rex 3069  df-reu 3375  df-rab 3431  df-v 3474  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-int 4950  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6299  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-riota 7367  df-ov 7414  df-oprab 7415  df-mpo 7416  df-om 7858  df-1st 7977  df-2nd 7978  df-frecs 8268  df-wrecs 8299  df-recs 8373  df-rdg 8412  df-1o 8468  df-oadd 8472  df-er 8705  df-map 8824  df-en 8942  df-dom 8943  df-sdom 8944  df-fin 8945  df-card 9936  df-pnf 11254  df-mnf 11255  df-xr 11256  df-ltxr 11257  df-le 11258  df-sub 11450  df-neg 11451  df-nn 12217  df-2 12279  df-n0 12477  df-xnn0 12549  df-z 12563  df-uz 12827  df-rp 12979  df-fz 13489  df-fzo 13632  df-hash 14295  df-word 14469  df-lsw 14517  df-concat 14525  df-s1 14550  df-clwwlk 29502  df-clwwlkn 29545
This theorem is referenced by:  numclwwlk2lem1  29896
  Copyright terms: Public domain W3C validator