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

Theorem swrdswrd 14744
Description: A subword of a subword is a subword. (Contributed by Alexander van der Vekens, 4-Apr-2018.)
Assertion
Ref Expression
swrdswrd ((𝑊 ∈ Word 𝑉𝑁 ∈ (0...(♯‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) → ((𝐾 ∈ (0...(𝑁𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁𝑀))) → ((𝑊 substr ⟨𝑀, 𝑁⟩) substr ⟨𝐾, 𝐿⟩) = (𝑊 substr ⟨(𝑀 + 𝐾), (𝑀 + 𝐿)⟩)))

Proof of Theorem swrdswrd
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 swrdcl 14684 . . . . . 6 (𝑊 ∈ Word 𝑉 → (𝑊 substr ⟨𝑀, 𝑁⟩) ∈ Word 𝑉)
213ad2ant1 1133 . . . . 5 ((𝑊 ∈ Word 𝑉𝑁 ∈ (0...(♯‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) → (𝑊 substr ⟨𝑀, 𝑁⟩) ∈ Word 𝑉)
32adantr 480 . . . 4 (((𝑊 ∈ Word 𝑉𝑁 ∈ (0...(♯‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ∧ (𝐾 ∈ (0...(𝑁𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁𝑀)))) → (𝑊 substr ⟨𝑀, 𝑁⟩) ∈ Word 𝑉)
4 elfz0ubfz0 13673 . . . . 5 ((𝐾 ∈ (0...(𝑁𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁𝑀))) → 𝐾 ∈ (0...𝐿))
54adantl 481 . . . 4 (((𝑊 ∈ Word 𝑉𝑁 ∈ (0...(♯‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ∧ (𝐾 ∈ (0...(𝑁𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁𝑀)))) → 𝐾 ∈ (0...𝐿))
6 elfzuz 13561 . . . . . . . . 9 (𝐾 ∈ (0...(𝑁𝑀)) → 𝐾 ∈ (ℤ‘0))
76adantl 481 . . . . . . . 8 (((𝑊 ∈ Word 𝑉𝑁 ∈ (0...(♯‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ∧ 𝐾 ∈ (0...(𝑁𝑀))) → 𝐾 ∈ (ℤ‘0))
8 fzss1 13604 . . . . . . . 8 (𝐾 ∈ (ℤ‘0) → (𝐾...(𝑁𝑀)) ⊆ (0...(𝑁𝑀)))
97, 8syl 17 . . . . . . 7 (((𝑊 ∈ Word 𝑉𝑁 ∈ (0...(♯‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ∧ 𝐾 ∈ (0...(𝑁𝑀))) → (𝐾...(𝑁𝑀)) ⊆ (0...(𝑁𝑀)))
109sseld 3981 . . . . . 6 (((𝑊 ∈ Word 𝑉𝑁 ∈ (0...(♯‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ∧ 𝐾 ∈ (0...(𝑁𝑀))) → (𝐿 ∈ (𝐾...(𝑁𝑀)) → 𝐿 ∈ (0...(𝑁𝑀))))
1110impr 454 . . . . 5 (((𝑊 ∈ Word 𝑉𝑁 ∈ (0...(♯‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ∧ (𝐾 ∈ (0...(𝑁𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁𝑀)))) → 𝐿 ∈ (0...(𝑁𝑀)))
12 3ancomb 1098 . . . . . . . . 9 ((𝑊 ∈ Word 𝑉𝑁 ∈ (0...(♯‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ↔ (𝑊 ∈ Word 𝑉𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))))
1312biimpi 216 . . . . . . . 8 ((𝑊 ∈ Word 𝑉𝑁 ∈ (0...(♯‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) → (𝑊 ∈ Word 𝑉𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))))
1413adantr 480 . . . . . . 7 (((𝑊 ∈ Word 𝑉𝑁 ∈ (0...(♯‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ∧ (𝐾 ∈ (0...(𝑁𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁𝑀)))) → (𝑊 ∈ Word 𝑉𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))))
15 swrdlen 14686 . . . . . . 7 ((𝑊 ∈ Word 𝑉𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) → (♯‘(𝑊 substr ⟨𝑀, 𝑁⟩)) = (𝑁𝑀))
1614, 15syl 17 . . . . . 6 (((𝑊 ∈ Word 𝑉𝑁 ∈ (0...(♯‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ∧ (𝐾 ∈ (0...(𝑁𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁𝑀)))) → (♯‘(𝑊 substr ⟨𝑀, 𝑁⟩)) = (𝑁𝑀))
1716oveq2d 7448 . . . . 5 (((𝑊 ∈ Word 𝑉𝑁 ∈ (0...(♯‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ∧ (𝐾 ∈ (0...(𝑁𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁𝑀)))) → (0...(♯‘(𝑊 substr ⟨𝑀, 𝑁⟩))) = (0...(𝑁𝑀)))
1811, 17eleqtrrd 2843 . . . 4 (((𝑊 ∈ Word 𝑉𝑁 ∈ (0...(♯‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ∧ (𝐾 ∈ (0...(𝑁𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁𝑀)))) → 𝐿 ∈ (0...(♯‘(𝑊 substr ⟨𝑀, 𝑁⟩))))
19 swrdval2 14685 . . . 4 (((𝑊 substr ⟨𝑀, 𝑁⟩) ∈ Word 𝑉𝐾 ∈ (0...𝐿) ∧ 𝐿 ∈ (0...(♯‘(𝑊 substr ⟨𝑀, 𝑁⟩)))) → ((𝑊 substr ⟨𝑀, 𝑁⟩) substr ⟨𝐾, 𝐿⟩) = (𝑥 ∈ (0..^(𝐿𝐾)) ↦ ((𝑊 substr ⟨𝑀, 𝑁⟩)‘(𝑥 + 𝐾))))
203, 5, 18, 19syl3anc 1372 . . 3 (((𝑊 ∈ Word 𝑉𝑁 ∈ (0...(♯‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ∧ (𝐾 ∈ (0...(𝑁𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁𝑀)))) → ((𝑊 substr ⟨𝑀, 𝑁⟩) substr ⟨𝐾, 𝐿⟩) = (𝑥 ∈ (0..^(𝐿𝐾)) ↦ ((𝑊 substr ⟨𝑀, 𝑁⟩)‘(𝑥 + 𝐾))))
21 fvex 6918 . . . . . 6 ((𝑊 substr ⟨𝑀, 𝑁⟩)‘(𝑥 + 𝐾)) ∈ V
22 eqid 2736 . . . . . 6 (𝑥 ∈ (0..^(𝐿𝐾)) ↦ ((𝑊 substr ⟨𝑀, 𝑁⟩)‘(𝑥 + 𝐾))) = (𝑥 ∈ (0..^(𝐿𝐾)) ↦ ((𝑊 substr ⟨𝑀, 𝑁⟩)‘(𝑥 + 𝐾)))
2321, 22fnmpti 6710 . . . . 5 (𝑥 ∈ (0..^(𝐿𝐾)) ↦ ((𝑊 substr ⟨𝑀, 𝑁⟩)‘(𝑥 + 𝐾))) Fn (0..^(𝐿𝐾))
2423a1i 11 . . . 4 (((𝑊 ∈ Word 𝑉𝑁 ∈ (0...(♯‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ∧ (𝐾 ∈ (0...(𝑁𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁𝑀)))) → (𝑥 ∈ (0..^(𝐿𝐾)) ↦ ((𝑊 substr ⟨𝑀, 𝑁⟩)‘(𝑥 + 𝐾))) Fn (0..^(𝐿𝐾)))
25 swrdswrdlem 14743 . . . . . 6 (((𝑊 ∈ Word 𝑉𝑁 ∈ (0...(♯‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ∧ (𝐾 ∈ (0...(𝑁𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁𝑀)))) → (𝑊 ∈ Word 𝑉 ∧ (𝑀 + 𝐾) ∈ (0...(𝑀 + 𝐿)) ∧ (𝑀 + 𝐿) ∈ (0...(♯‘𝑊))))
26 swrdvalfn 14690 . . . . . 6 ((𝑊 ∈ Word 𝑉 ∧ (𝑀 + 𝐾) ∈ (0...(𝑀 + 𝐿)) ∧ (𝑀 + 𝐿) ∈ (0...(♯‘𝑊))) → (𝑊 substr ⟨(𝑀 + 𝐾), (𝑀 + 𝐿)⟩) Fn (0..^((𝑀 + 𝐿) − (𝑀 + 𝐾))))
2725, 26syl 17 . . . . 5 (((𝑊 ∈ Word 𝑉𝑁 ∈ (0...(♯‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ∧ (𝐾 ∈ (0...(𝑁𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁𝑀)))) → (𝑊 substr ⟨(𝑀 + 𝐾), (𝑀 + 𝐿)⟩) Fn (0..^((𝑀 + 𝐿) − (𝑀 + 𝐾))))
28 elfzelz 13565 . . . . . . . . . 10 (𝑀 ∈ (0...𝑁) → 𝑀 ∈ ℤ)
29 elfzelz 13565 . . . . . . . . . . 11 (𝐿 ∈ (𝐾...(𝑁𝑀)) → 𝐿 ∈ ℤ)
30 elfzelz 13565 . . . . . . . . . . 11 (𝐾 ∈ (0...(𝑁𝑀)) → 𝐾 ∈ ℤ)
31 zcn 12620 . . . . . . . . . . . . . 14 (𝑀 ∈ ℤ → 𝑀 ∈ ℂ)
3231adantr 480 . . . . . . . . . . . . 13 ((𝑀 ∈ ℤ ∧ (𝐿 ∈ ℤ ∧ 𝐾 ∈ ℤ)) → 𝑀 ∈ ℂ)
33 zcn 12620 . . . . . . . . . . . . . 14 (𝐿 ∈ ℤ → 𝐿 ∈ ℂ)
3433ad2antrl 728 . . . . . . . . . . . . 13 ((𝑀 ∈ ℤ ∧ (𝐿 ∈ ℤ ∧ 𝐾 ∈ ℤ)) → 𝐿 ∈ ℂ)
35 zcn 12620 . . . . . . . . . . . . . 14 (𝐾 ∈ ℤ → 𝐾 ∈ ℂ)
3635ad2antll 729 . . . . . . . . . . . . 13 ((𝑀 ∈ ℤ ∧ (𝐿 ∈ ℤ ∧ 𝐾 ∈ ℤ)) → 𝐾 ∈ ℂ)
37 pnpcan 11549 . . . . . . . . . . . . . 14 ((𝑀 ∈ ℂ ∧ 𝐿 ∈ ℂ ∧ 𝐾 ∈ ℂ) → ((𝑀 + 𝐿) − (𝑀 + 𝐾)) = (𝐿𝐾))
3837eqcomd 2742 . . . . . . . . . . . . 13 ((𝑀 ∈ ℂ ∧ 𝐿 ∈ ℂ ∧ 𝐾 ∈ ℂ) → (𝐿𝐾) = ((𝑀 + 𝐿) − (𝑀 + 𝐾)))
3932, 34, 36, 38syl3anc 1372 . . . . . . . . . . . 12 ((𝑀 ∈ ℤ ∧ (𝐿 ∈ ℤ ∧ 𝐾 ∈ ℤ)) → (𝐿𝐾) = ((𝑀 + 𝐿) − (𝑀 + 𝐾)))
4039expcom 413 . . . . . . . . . . 11 ((𝐿 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑀 ∈ ℤ → (𝐿𝐾) = ((𝑀 + 𝐿) − (𝑀 + 𝐾))))
4129, 30, 40syl2anr 597 . . . . . . . . . 10 ((𝐾 ∈ (0...(𝑁𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁𝑀))) → (𝑀 ∈ ℤ → (𝐿𝐾) = ((𝑀 + 𝐿) − (𝑀 + 𝐾))))
4228, 41syl5com 31 . . . . . . . . 9 (𝑀 ∈ (0...𝑁) → ((𝐾 ∈ (0...(𝑁𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁𝑀))) → (𝐿𝐾) = ((𝑀 + 𝐿) − (𝑀 + 𝐾))))
43423ad2ant3 1135 . . . . . . . 8 ((𝑊 ∈ Word 𝑉𝑁 ∈ (0...(♯‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) → ((𝐾 ∈ (0...(𝑁𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁𝑀))) → (𝐿𝐾) = ((𝑀 + 𝐿) − (𝑀 + 𝐾))))
4443imp 406 . . . . . . 7 (((𝑊 ∈ Word 𝑉𝑁 ∈ (0...(♯‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ∧ (𝐾 ∈ (0...(𝑁𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁𝑀)))) → (𝐿𝐾) = ((𝑀 + 𝐿) − (𝑀 + 𝐾)))
4544oveq2d 7448 . . . . . 6 (((𝑊 ∈ Word 𝑉𝑁 ∈ (0...(♯‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ∧ (𝐾 ∈ (0...(𝑁𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁𝑀)))) → (0..^(𝐿𝐾)) = (0..^((𝑀 + 𝐿) − (𝑀 + 𝐾))))
4645fneq2d 6661 . . . . 5 (((𝑊 ∈ Word 𝑉𝑁 ∈ (0...(♯‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ∧ (𝐾 ∈ (0...(𝑁𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁𝑀)))) → ((𝑊 substr ⟨(𝑀 + 𝐾), (𝑀 + 𝐿)⟩) Fn (0..^(𝐿𝐾)) ↔ (𝑊 substr ⟨(𝑀 + 𝐾), (𝑀 + 𝐿)⟩) Fn (0..^((𝑀 + 𝐿) − (𝑀 + 𝐾)))))
4727, 46mpbird 257 . . . 4 (((𝑊 ∈ Word 𝑉𝑁 ∈ (0...(♯‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ∧ (𝐾 ∈ (0...(𝑁𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁𝑀)))) → (𝑊 substr ⟨(𝑀 + 𝐾), (𝑀 + 𝐿)⟩) Fn (0..^(𝐿𝐾)))
48 simpr 484 . . . . . . 7 ((((𝑊 ∈ Word 𝑉𝑁 ∈ (0...(♯‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ∧ (𝐾 ∈ (0...(𝑁𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁𝑀)))) ∧ 𝑦 ∈ (0..^(𝐿𝐾))) → 𝑦 ∈ (0..^(𝐿𝐾)))
49 fvex 6918 . . . . . . 7 (𝑊‘((𝑦 + 𝐾) + 𝑀)) ∈ V
50 oveq1 7439 . . . . . . . . 9 (𝑥 = 𝑦 → (𝑥 + 𝐾) = (𝑦 + 𝐾))
5150fvoveq1d 7454 . . . . . . . 8 (𝑥 = 𝑦 → (𝑊‘((𝑥 + 𝐾) + 𝑀)) = (𝑊‘((𝑦 + 𝐾) + 𝑀)))
52 eqid 2736 . . . . . . . 8 (𝑥 ∈ (0..^(𝐿𝐾)) ↦ (𝑊‘((𝑥 + 𝐾) + 𝑀))) = (𝑥 ∈ (0..^(𝐿𝐾)) ↦ (𝑊‘((𝑥 + 𝐾) + 𝑀)))
5351, 52fvmptg 7013 . . . . . . 7 ((𝑦 ∈ (0..^(𝐿𝐾)) ∧ (𝑊‘((𝑦 + 𝐾) + 𝑀)) ∈ V) → ((𝑥 ∈ (0..^(𝐿𝐾)) ↦ (𝑊‘((𝑥 + 𝐾) + 𝑀)))‘𝑦) = (𝑊‘((𝑦 + 𝐾) + 𝑀)))
5448, 49, 53sylancl 586 . . . . . 6 ((((𝑊 ∈ Word 𝑉𝑁 ∈ (0...(♯‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ∧ (𝐾 ∈ (0...(𝑁𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁𝑀)))) ∧ 𝑦 ∈ (0..^(𝐿𝐾))) → ((𝑥 ∈ (0..^(𝐿𝐾)) ↦ (𝑊‘((𝑥 + 𝐾) + 𝑀)))‘𝑦) = (𝑊‘((𝑦 + 𝐾) + 𝑀)))
55 zcn 12620 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ ℤ → 𝑦 ∈ ℂ)
5655, 31, 353anim123i 1151 . . . . . . . . . . . . . . . . 17 ((𝑦 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑦 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ 𝐾 ∈ ℂ))
57563expa 1118 . . . . . . . . . . . . . . . 16 (((𝑦 ∈ ℤ ∧ 𝑀 ∈ ℤ) ∧ 𝐾 ∈ ℤ) → (𝑦 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ 𝐾 ∈ ℂ))
58 add32r 11482 . . . . . . . . . . . . . . . . 17 ((𝑦 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ 𝐾 ∈ ℂ) → (𝑦 + (𝑀 + 𝐾)) = ((𝑦 + 𝐾) + 𝑀))
5958eqcomd 2742 . . . . . . . . . . . . . . . 16 ((𝑦 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ 𝐾 ∈ ℂ) → ((𝑦 + 𝐾) + 𝑀) = (𝑦 + (𝑀 + 𝐾)))
6057, 59syl 17 . . . . . . . . . . . . . . 15 (((𝑦 ∈ ℤ ∧ 𝑀 ∈ ℤ) ∧ 𝐾 ∈ ℤ) → ((𝑦 + 𝐾) + 𝑀) = (𝑦 + (𝑀 + 𝐾)))
6160exp31 419 . . . . . . . . . . . . . 14 (𝑦 ∈ ℤ → (𝑀 ∈ ℤ → (𝐾 ∈ ℤ → ((𝑦 + 𝐾) + 𝑀) = (𝑦 + (𝑀 + 𝐾)))))
6261com13 88 . . . . . . . . . . . . 13 (𝐾 ∈ ℤ → (𝑀 ∈ ℤ → (𝑦 ∈ ℤ → ((𝑦 + 𝐾) + 𝑀) = (𝑦 + (𝑀 + 𝐾)))))
6330, 62syl 17 . . . . . . . . . . . 12 (𝐾 ∈ (0...(𝑁𝑀)) → (𝑀 ∈ ℤ → (𝑦 ∈ ℤ → ((𝑦 + 𝐾) + 𝑀) = (𝑦 + (𝑀 + 𝐾)))))
6463adantr 480 . . . . . . . . . . 11 ((𝐾 ∈ (0...(𝑁𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁𝑀))) → (𝑀 ∈ ℤ → (𝑦 ∈ ℤ → ((𝑦 + 𝐾) + 𝑀) = (𝑦 + (𝑀 + 𝐾)))))
6528, 64syl5com 31 . . . . . . . . . 10 (𝑀 ∈ (0...𝑁) → ((𝐾 ∈ (0...(𝑁𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁𝑀))) → (𝑦 ∈ ℤ → ((𝑦 + 𝐾) + 𝑀) = (𝑦 + (𝑀 + 𝐾)))))
66653ad2ant3 1135 . . . . . . . . 9 ((𝑊 ∈ Word 𝑉𝑁 ∈ (0...(♯‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) → ((𝐾 ∈ (0...(𝑁𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁𝑀))) → (𝑦 ∈ ℤ → ((𝑦 + 𝐾) + 𝑀) = (𝑦 + (𝑀 + 𝐾)))))
6766imp 406 . . . . . . . 8 (((𝑊 ∈ Word 𝑉𝑁 ∈ (0...(♯‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ∧ (𝐾 ∈ (0...(𝑁𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁𝑀)))) → (𝑦 ∈ ℤ → ((𝑦 + 𝐾) + 𝑀) = (𝑦 + (𝑀 + 𝐾))))
68 elfzoelz 13700 . . . . . . . 8 (𝑦 ∈ (0..^(𝐿𝐾)) → 𝑦 ∈ ℤ)
6967, 68impel 505 . . . . . . 7 ((((𝑊 ∈ Word 𝑉𝑁 ∈ (0...(♯‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ∧ (𝐾 ∈ (0...(𝑁𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁𝑀)))) ∧ 𝑦 ∈ (0..^(𝐿𝐾))) → ((𝑦 + 𝐾) + 𝑀) = (𝑦 + (𝑀 + 𝐾)))
7069fveq2d 6909 . . . . . 6 ((((𝑊 ∈ Word 𝑉𝑁 ∈ (0...(♯‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ∧ (𝐾 ∈ (0...(𝑁𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁𝑀)))) ∧ 𝑦 ∈ (0..^(𝐿𝐾))) → (𝑊‘((𝑦 + 𝐾) + 𝑀)) = (𝑊‘(𝑦 + (𝑀 + 𝐾))))
7154, 70eqtrd 2776 . . . . 5 ((((𝑊 ∈ Word 𝑉𝑁 ∈ (0...(♯‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ∧ (𝐾 ∈ (0...(𝑁𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁𝑀)))) ∧ 𝑦 ∈ (0..^(𝐿𝐾))) → ((𝑥 ∈ (0..^(𝐿𝐾)) ↦ (𝑊‘((𝑥 + 𝐾) + 𝑀)))‘𝑦) = (𝑊‘(𝑦 + (𝑀 + 𝐾))))
7213ad3antrrr 730 . . . . . . . 8 (((((𝑊 ∈ Word 𝑉𝑁 ∈ (0...(♯‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ∧ (𝐾 ∈ (0...(𝑁𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁𝑀)))) ∧ 𝑦 ∈ (0..^(𝐿𝐾))) ∧ 𝑥 ∈ (0..^(𝐿𝐾))) → (𝑊 ∈ Word 𝑉𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))))
73 elfz2nn0 13659 . . . . . . . . . . . . 13 (𝐾 ∈ (0...(𝑁𝑀)) ↔ (𝐾 ∈ ℕ0 ∧ (𝑁𝑀) ∈ ℕ0𝐾 ≤ (𝑁𝑀)))
74 elfz2 13555 . . . . . . . . . . . . . . . 16 (𝐿 ∈ (𝐾...(𝑁𝑀)) ↔ ((𝐾 ∈ ℤ ∧ (𝑁𝑀) ∈ ℤ ∧ 𝐿 ∈ ℤ) ∧ (𝐾𝐿𝐿 ≤ (𝑁𝑀))))
75 elfzo0 13741 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ (0..^(𝐿𝐾)) ↔ (𝑥 ∈ ℕ0 ∧ (𝐿𝐾) ∈ ℕ ∧ 𝑥 < (𝐿𝐾)))
76 nn0re 12537 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑥 ∈ ℕ0𝑥 ∈ ℝ)
7776ad2antrl 728 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝐾 ∈ ℕ0 ∧ (𝑥 ∈ ℕ0𝐿 ∈ ℤ)) → 𝑥 ∈ ℝ)
78 nn0re 12537 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝐾 ∈ ℕ0𝐾 ∈ ℝ)
7978adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝐾 ∈ ℕ0 ∧ (𝑥 ∈ ℕ0𝐿 ∈ ℤ)) → 𝐾 ∈ ℝ)
80 zre 12619 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝐿 ∈ ℤ → 𝐿 ∈ ℝ)
8180ad2antll 729 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝐾 ∈ ℕ0 ∧ (𝑥 ∈ ℕ0𝐿 ∈ ℤ)) → 𝐿 ∈ ℝ)
82 ltaddsub 11738 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑥 ∈ ℝ ∧ 𝐾 ∈ ℝ ∧ 𝐿 ∈ ℝ) → ((𝑥 + 𝐾) < 𝐿𝑥 < (𝐿𝐾)))
8382bicomd 223 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑥 ∈ ℝ ∧ 𝐾 ∈ ℝ ∧ 𝐿 ∈ ℝ) → (𝑥 < (𝐿𝐾) ↔ (𝑥 + 𝐾) < 𝐿))
8477, 79, 81, 83syl3anc 1372 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝐾 ∈ ℕ0 ∧ (𝑥 ∈ ℕ0𝐿 ∈ ℤ)) → (𝑥 < (𝐿𝐾) ↔ (𝑥 + 𝐾) < 𝐿))
85 nn0addcl 12563 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑥 ∈ ℕ0𝐾 ∈ ℕ0) → (𝑥 + 𝐾) ∈ ℕ0)
8685ex 412 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑥 ∈ ℕ0 → (𝐾 ∈ ℕ0 → (𝑥 + 𝐾) ∈ ℕ0))
8786adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑥 ∈ ℕ0𝐿 ∈ ℤ) → (𝐾 ∈ ℕ0 → (𝑥 + 𝐾) ∈ ℕ0))
8887impcom 407 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝐾 ∈ ℕ0 ∧ (𝑥 ∈ ℕ0𝐿 ∈ ℤ)) → (𝑥 + 𝐾) ∈ ℕ0)
8988ad3antrrr 730 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((𝐾 ∈ ℕ0 ∧ (𝑥 ∈ ℕ0𝐿 ∈ ℤ)) ∧ (𝑥 + 𝐾) < 𝐿) ∧ (𝑁𝑀) ∈ ℕ0) ∧ 𝐿 ≤ (𝑁𝑀)) → (𝑥 + 𝐾) ∈ ℕ0)
90 elnn0z 12628 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑥 + 𝐾) ∈ ℕ0 ↔ ((𝑥 + 𝐾) ∈ ℤ ∧ 0 ≤ (𝑥 + 𝐾)))
91 0red 11265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (((𝑥 + 𝐾) ∈ ℤ ∧ 𝐿 ∈ ℤ) → 0 ∈ ℝ)
92 zre 12619 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ((𝑥 + 𝐾) ∈ ℤ → (𝑥 + 𝐾) ∈ ℝ)
9392adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (((𝑥 + 𝐾) ∈ ℤ ∧ 𝐿 ∈ ℤ) → (𝑥 + 𝐾) ∈ ℝ)
9480adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (((𝑥 + 𝐾) ∈ ℤ ∧ 𝐿 ∈ ℤ) → 𝐿 ∈ ℝ)
95 lelttr 11352 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((0 ∈ ℝ ∧ (𝑥 + 𝐾) ∈ ℝ ∧ 𝐿 ∈ ℝ) → ((0 ≤ (𝑥 + 𝐾) ∧ (𝑥 + 𝐾) < 𝐿) → 0 < 𝐿))
9691, 93, 94, 95syl3anc 1372 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (((𝑥 + 𝐾) ∈ ℤ ∧ 𝐿 ∈ ℤ) → ((0 ≤ (𝑥 + 𝐾) ∧ (𝑥 + 𝐾) < 𝐿) → 0 < 𝐿))
97 0red 11265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ((𝐿 ∈ ℤ ∧ (𝑁𝑀) ∈ ℕ0) → 0 ∈ ℝ)
9880adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ((𝐿 ∈ ℤ ∧ (𝑁𝑀) ∈ ℕ0) → 𝐿 ∈ ℝ)
99 nn0re 12537 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ((𝑁𝑀) ∈ ℕ0 → (𝑁𝑀) ∈ ℝ)
10099adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ((𝐿 ∈ ℤ ∧ (𝑁𝑀) ∈ ℕ0) → (𝑁𝑀) ∈ ℝ)
101 ltletr 11354 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ((0 ∈ ℝ ∧ 𝐿 ∈ ℝ ∧ (𝑁𝑀) ∈ ℝ) → ((0 < 𝐿𝐿 ≤ (𝑁𝑀)) → 0 < (𝑁𝑀)))
10297, 98, 100, 101syl3anc 1372 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ((𝐿 ∈ ℤ ∧ (𝑁𝑀) ∈ ℕ0) → ((0 < 𝐿𝐿 ≤ (𝑁𝑀)) → 0 < (𝑁𝑀)))
103 elnnnn0b 12572 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ((𝑁𝑀) ∈ ℕ ↔ ((𝑁𝑀) ∈ ℕ0 ∧ 0 < (𝑁𝑀)))
104103simplbi2 500 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ((𝑁𝑀) ∈ ℕ0 → (0 < (𝑁𝑀) → (𝑁𝑀) ∈ ℕ))
105104adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ((𝐿 ∈ ℤ ∧ (𝑁𝑀) ∈ ℕ0) → (0 < (𝑁𝑀) → (𝑁𝑀) ∈ ℕ))
106102, 105syld 47 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ((𝐿 ∈ ℤ ∧ (𝑁𝑀) ∈ ℕ0) → ((0 < 𝐿𝐿 ≤ (𝑁𝑀)) → (𝑁𝑀) ∈ ℕ))
107106exp4b 430 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (𝐿 ∈ ℤ → ((𝑁𝑀) ∈ ℕ0 → (0 < 𝐿 → (𝐿 ≤ (𝑁𝑀) → (𝑁𝑀) ∈ ℕ))))
108107com23 86 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (𝐿 ∈ ℤ → (0 < 𝐿 → ((𝑁𝑀) ∈ ℕ0 → (𝐿 ≤ (𝑁𝑀) → (𝑁𝑀) ∈ ℕ))))
109108adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (((𝑥 + 𝐾) ∈ ℤ ∧ 𝐿 ∈ ℤ) → (0 < 𝐿 → ((𝑁𝑀) ∈ ℕ0 → (𝐿 ≤ (𝑁𝑀) → (𝑁𝑀) ∈ ℕ))))
11096, 109syld 47 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (((𝑥 + 𝐾) ∈ ℤ ∧ 𝐿 ∈ ℤ) → ((0 ≤ (𝑥 + 𝐾) ∧ (𝑥 + 𝐾) < 𝐿) → ((𝑁𝑀) ∈ ℕ0 → (𝐿 ≤ (𝑁𝑀) → (𝑁𝑀) ∈ ℕ))))
111110expd 415 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (((𝑥 + 𝐾) ∈ ℤ ∧ 𝐿 ∈ ℤ) → (0 ≤ (𝑥 + 𝐾) → ((𝑥 + 𝐾) < 𝐿 → ((𝑁𝑀) ∈ ℕ0 → (𝐿 ≤ (𝑁𝑀) → (𝑁𝑀) ∈ ℕ)))))
112111a1d 25 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (((𝑥 + 𝐾) ∈ ℤ ∧ 𝐿 ∈ ℤ) → ((𝑥 ∈ ℕ0𝐾 ∈ ℕ0) → (0 ≤ (𝑥 + 𝐾) → ((𝑥 + 𝐾) < 𝐿 → ((𝑁𝑀) ∈ ℕ0 → (𝐿 ≤ (𝑁𝑀) → (𝑁𝑀) ∈ ℕ))))))
113112ex 412 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝑥 + 𝐾) ∈ ℤ → (𝐿 ∈ ℤ → ((𝑥 ∈ ℕ0𝐾 ∈ ℕ0) → (0 ≤ (𝑥 + 𝐾) → ((𝑥 + 𝐾) < 𝐿 → ((𝑁𝑀) ∈ ℕ0 → (𝐿 ≤ (𝑁𝑀) → (𝑁𝑀) ∈ ℕ)))))))
114113com24 95 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑥 + 𝐾) ∈ ℤ → (0 ≤ (𝑥 + 𝐾) → ((𝑥 ∈ ℕ0𝐾 ∈ ℕ0) → (𝐿 ∈ ℤ → ((𝑥 + 𝐾) < 𝐿 → ((𝑁𝑀) ∈ ℕ0 → (𝐿 ≤ (𝑁𝑀) → (𝑁𝑀) ∈ ℕ)))))))
115114imp 406 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((𝑥 + 𝐾) ∈ ℤ ∧ 0 ≤ (𝑥 + 𝐾)) → ((𝑥 ∈ ℕ0𝐾 ∈ ℕ0) → (𝐿 ∈ ℤ → ((𝑥 + 𝐾) < 𝐿 → ((𝑁𝑀) ∈ ℕ0 → (𝐿 ≤ (𝑁𝑀) → (𝑁𝑀) ∈ ℕ))))))
11690, 115sylbi 217 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑥 + 𝐾) ∈ ℕ0 → ((𝑥 ∈ ℕ0𝐾 ∈ ℕ0) → (𝐿 ∈ ℤ → ((𝑥 + 𝐾) < 𝐿 → ((𝑁𝑀) ∈ ℕ0 → (𝐿 ≤ (𝑁𝑀) → (𝑁𝑀) ∈ ℕ))))))
11785, 116mpcom 38 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑥 ∈ ℕ0𝐾 ∈ ℕ0) → (𝐿 ∈ ℤ → ((𝑥 + 𝐾) < 𝐿 → ((𝑁𝑀) ∈ ℕ0 → (𝐿 ≤ (𝑁𝑀) → (𝑁𝑀) ∈ ℕ)))))
118117impancom 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑥 ∈ ℕ0𝐿 ∈ ℤ) → (𝐾 ∈ ℕ0 → ((𝑥 + 𝐾) < 𝐿 → ((𝑁𝑀) ∈ ℕ0 → (𝐿 ≤ (𝑁𝑀) → (𝑁𝑀) ∈ ℕ)))))
119118impcom 407 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝐾 ∈ ℕ0 ∧ (𝑥 ∈ ℕ0𝐿 ∈ ℤ)) → ((𝑥 + 𝐾) < 𝐿 → ((𝑁𝑀) ∈ ℕ0 → (𝐿 ≤ (𝑁𝑀) → (𝑁𝑀) ∈ ℕ))))
120119imp41 425 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((𝐾 ∈ ℕ0 ∧ (𝑥 ∈ ℕ0𝐿 ∈ ℤ)) ∧ (𝑥 + 𝐾) < 𝐿) ∧ (𝑁𝑀) ∈ ℕ0) ∧ 𝐿 ≤ (𝑁𝑀)) → (𝑁𝑀) ∈ ℕ)
121 nn0readdcl 12595 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝑥 ∈ ℕ0𝐾 ∈ ℕ0) → (𝑥 + 𝐾) ∈ ℝ)
122121ex 412 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑥 ∈ ℕ0 → (𝐾 ∈ ℕ0 → (𝑥 + 𝐾) ∈ ℝ))
123122adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑥 ∈ ℕ0𝐿 ∈ ℤ) → (𝐾 ∈ ℕ0 → (𝑥 + 𝐾) ∈ ℝ))
124123impcom 407 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝐾 ∈ ℕ0 ∧ (𝑥 ∈ ℕ0𝐿 ∈ ℤ)) → (𝑥 + 𝐾) ∈ ℝ)
125 ltletr 11354 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((𝑥 + 𝐾) ∈ ℝ ∧ 𝐿 ∈ ℝ ∧ (𝑁𝑀) ∈ ℝ) → (((𝑥 + 𝐾) < 𝐿𝐿 ≤ (𝑁𝑀)) → (𝑥 + 𝐾) < (𝑁𝑀)))
126124, 81, 99, 125syl2an3an 1423 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝐾 ∈ ℕ0 ∧ (𝑥 ∈ ℕ0𝐿 ∈ ℤ)) ∧ (𝑁𝑀) ∈ ℕ0) → (((𝑥 + 𝐾) < 𝐿𝐿 ≤ (𝑁𝑀)) → (𝑥 + 𝐾) < (𝑁𝑀)))
127126exp4b 430 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝐾 ∈ ℕ0 ∧ (𝑥 ∈ ℕ0𝐿 ∈ ℤ)) → ((𝑁𝑀) ∈ ℕ0 → ((𝑥 + 𝐾) < 𝐿 → (𝐿 ≤ (𝑁𝑀) → (𝑥 + 𝐾) < (𝑁𝑀)))))
128127com23 86 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝐾 ∈ ℕ0 ∧ (𝑥 ∈ ℕ0𝐿 ∈ ℤ)) → ((𝑥 + 𝐾) < 𝐿 → ((𝑁𝑀) ∈ ℕ0 → (𝐿 ≤ (𝑁𝑀) → (𝑥 + 𝐾) < (𝑁𝑀)))))
129128imp41 425 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((𝐾 ∈ ℕ0 ∧ (𝑥 ∈ ℕ0𝐿 ∈ ℤ)) ∧ (𝑥 + 𝐾) < 𝐿) ∧ (𝑁𝑀) ∈ ℕ0) ∧ 𝐿 ≤ (𝑁𝑀)) → (𝑥 + 𝐾) < (𝑁𝑀))
130 elfzo0 13741 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑥 + 𝐾) ∈ (0..^(𝑁𝑀)) ↔ ((𝑥 + 𝐾) ∈ ℕ0 ∧ (𝑁𝑀) ∈ ℕ ∧ (𝑥 + 𝐾) < (𝑁𝑀)))
13189, 120, 129, 130syl3anbrc 1343 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((𝐾 ∈ ℕ0 ∧ (𝑥 ∈ ℕ0𝐿 ∈ ℤ)) ∧ (𝑥 + 𝐾) < 𝐿) ∧ (𝑁𝑀) ∈ ℕ0) ∧ 𝐿 ≤ (𝑁𝑀)) → (𝑥 + 𝐾) ∈ (0..^(𝑁𝑀)))
132131exp41 434 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝐾 ∈ ℕ0 ∧ (𝑥 ∈ ℕ0𝐿 ∈ ℤ)) → ((𝑥 + 𝐾) < 𝐿 → ((𝑁𝑀) ∈ ℕ0 → (𝐿 ≤ (𝑁𝑀) → (𝑥 + 𝐾) ∈ (0..^(𝑁𝑀))))))
13384, 132sylbid 240 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝐾 ∈ ℕ0 ∧ (𝑥 ∈ ℕ0𝐿 ∈ ℤ)) → (𝑥 < (𝐿𝐾) → ((𝑁𝑀) ∈ ℕ0 → (𝐿 ≤ (𝑁𝑀) → (𝑥 + 𝐾) ∈ (0..^(𝑁𝑀))))))
134133ex 412 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝐾 ∈ ℕ0 → ((𝑥 ∈ ℕ0𝐿 ∈ ℤ) → (𝑥 < (𝐿𝐾) → ((𝑁𝑀) ∈ ℕ0 → (𝐿 ≤ (𝑁𝑀) → (𝑥 + 𝐾) ∈ (0..^(𝑁𝑀)))))))
135134com24 95 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝐾 ∈ ℕ0 → ((𝑁𝑀) ∈ ℕ0 → (𝑥 < (𝐿𝐾) → ((𝑥 ∈ ℕ0𝐿 ∈ ℤ) → (𝐿 ≤ (𝑁𝑀) → (𝑥 + 𝐾) ∈ (0..^(𝑁𝑀)))))))
136135imp 406 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐾 ∈ ℕ0 ∧ (𝑁𝑀) ∈ ℕ0) → (𝑥 < (𝐿𝐾) → ((𝑥 ∈ ℕ0𝐿 ∈ ℤ) → (𝐿 ≤ (𝑁𝑀) → (𝑥 + 𝐾) ∈ (0..^(𝑁𝑀))))))
137136com13 88 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑥 ∈ ℕ0𝐿 ∈ ℤ) → (𝑥 < (𝐿𝐾) → ((𝐾 ∈ ℕ0 ∧ (𝑁𝑀) ∈ ℕ0) → (𝐿 ≤ (𝑁𝑀) → (𝑥 + 𝐾) ∈ (0..^(𝑁𝑀))))))
138137impancom 451 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑥 ∈ ℕ0𝑥 < (𝐿𝐾)) → (𝐿 ∈ ℤ → ((𝐾 ∈ ℕ0 ∧ (𝑁𝑀) ∈ ℕ0) → (𝐿 ≤ (𝑁𝑀) → (𝑥 + 𝐾) ∈ (0..^(𝑁𝑀))))))
1391383adant2 1131 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑥 ∈ ℕ0 ∧ (𝐿𝐾) ∈ ℕ ∧ 𝑥 < (𝐿𝐾)) → (𝐿 ∈ ℤ → ((𝐾 ∈ ℕ0 ∧ (𝑁𝑀) ∈ ℕ0) → (𝐿 ≤ (𝑁𝑀) → (𝑥 + 𝐾) ∈ (0..^(𝑁𝑀))))))
14075, 139sylbi 217 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ (0..^(𝐿𝐾)) → (𝐿 ∈ ℤ → ((𝐾 ∈ ℕ0 ∧ (𝑁𝑀) ∈ ℕ0) → (𝐿 ≤ (𝑁𝑀) → (𝑥 + 𝐾) ∈ (0..^(𝑁𝑀))))))
141140com14 96 . . . . . . . . . . . . . . . . . . . 20 (𝐿 ≤ (𝑁𝑀) → (𝐿 ∈ ℤ → ((𝐾 ∈ ℕ0 ∧ (𝑁𝑀) ∈ ℕ0) → (𝑥 ∈ (0..^(𝐿𝐾)) → (𝑥 + 𝐾) ∈ (0..^(𝑁𝑀))))))
142141adantl 481 . . . . . . . . . . . . . . . . . . 19 ((𝐾𝐿𝐿 ≤ (𝑁𝑀)) → (𝐿 ∈ ℤ → ((𝐾 ∈ ℕ0 ∧ (𝑁𝑀) ∈ ℕ0) → (𝑥 ∈ (0..^(𝐿𝐾)) → (𝑥 + 𝐾) ∈ (0..^(𝑁𝑀))))))
143142com12 32 . . . . . . . . . . . . . . . . . 18 (𝐿 ∈ ℤ → ((𝐾𝐿𝐿 ≤ (𝑁𝑀)) → ((𝐾 ∈ ℕ0 ∧ (𝑁𝑀) ∈ ℕ0) → (𝑥 ∈ (0..^(𝐿𝐾)) → (𝑥 + 𝐾) ∈ (0..^(𝑁𝑀))))))
1441433ad2ant3 1135 . . . . . . . . . . . . . . . . 17 ((𝐾 ∈ ℤ ∧ (𝑁𝑀) ∈ ℤ ∧ 𝐿 ∈ ℤ) → ((𝐾𝐿𝐿 ≤ (𝑁𝑀)) → ((𝐾 ∈ ℕ0 ∧ (𝑁𝑀) ∈ ℕ0) → (𝑥 ∈ (0..^(𝐿𝐾)) → (𝑥 + 𝐾) ∈ (0..^(𝑁𝑀))))))
145144imp 406 . . . . . . . . . . . . . . . 16 (((𝐾 ∈ ℤ ∧ (𝑁𝑀) ∈ ℤ ∧ 𝐿 ∈ ℤ) ∧ (𝐾𝐿𝐿 ≤ (𝑁𝑀))) → ((𝐾 ∈ ℕ0 ∧ (𝑁𝑀) ∈ ℕ0) → (𝑥 ∈ (0..^(𝐿𝐾)) → (𝑥 + 𝐾) ∈ (0..^(𝑁𝑀)))))
14674, 145sylbi 217 . . . . . . . . . . . . . . 15 (𝐿 ∈ (𝐾...(𝑁𝑀)) → ((𝐾 ∈ ℕ0 ∧ (𝑁𝑀) ∈ ℕ0) → (𝑥 ∈ (0..^(𝐿𝐾)) → (𝑥 + 𝐾) ∈ (0..^(𝑁𝑀)))))
147146com12 32 . . . . . . . . . . . . . 14 ((𝐾 ∈ ℕ0 ∧ (𝑁𝑀) ∈ ℕ0) → (𝐿 ∈ (𝐾...(𝑁𝑀)) → (𝑥 ∈ (0..^(𝐿𝐾)) → (𝑥 + 𝐾) ∈ (0..^(𝑁𝑀)))))
1481473adant3 1132 . . . . . . . . . . . . 13 ((𝐾 ∈ ℕ0 ∧ (𝑁𝑀) ∈ ℕ0𝐾 ≤ (𝑁𝑀)) → (𝐿 ∈ (𝐾...(𝑁𝑀)) → (𝑥 ∈ (0..^(𝐿𝐾)) → (𝑥 + 𝐾) ∈ (0..^(𝑁𝑀)))))
14973, 148sylbi 217 . . . . . . . . . . . 12 (𝐾 ∈ (0...(𝑁𝑀)) → (𝐿 ∈ (𝐾...(𝑁𝑀)) → (𝑥 ∈ (0..^(𝐿𝐾)) → (𝑥 + 𝐾) ∈ (0..^(𝑁𝑀)))))
150149imp 406 . . . . . . . . . . 11 ((𝐾 ∈ (0...(𝑁𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁𝑀))) → (𝑥 ∈ (0..^(𝐿𝐾)) → (𝑥 + 𝐾) ∈ (0..^(𝑁𝑀))))
151150adantl 481 . . . . . . . . . 10 (((𝑊 ∈ Word 𝑉𝑁 ∈ (0...(♯‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ∧ (𝐾 ∈ (0...(𝑁𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁𝑀)))) → (𝑥 ∈ (0..^(𝐿𝐾)) → (𝑥 + 𝐾) ∈ (0..^(𝑁𝑀))))
152151adantr 480 . . . . . . . . 9 ((((𝑊 ∈ Word 𝑉𝑁 ∈ (0...(♯‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ∧ (𝐾 ∈ (0...(𝑁𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁𝑀)))) ∧ 𝑦 ∈ (0..^(𝐿𝐾))) → (𝑥 ∈ (0..^(𝐿𝐾)) → (𝑥 + 𝐾) ∈ (0..^(𝑁𝑀))))
153152imp 406 . . . . . . . 8 (((((𝑊 ∈ Word 𝑉𝑁 ∈ (0...(♯‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ∧ (𝐾 ∈ (0...(𝑁𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁𝑀)))) ∧ 𝑦 ∈ (0..^(𝐿𝐾))) ∧ 𝑥 ∈ (0..^(𝐿𝐾))) → (𝑥 + 𝐾) ∈ (0..^(𝑁𝑀)))
154 swrdfv 14687 . . . . . . . 8 (((𝑊 ∈ Word 𝑉𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ (𝑥 + 𝐾) ∈ (0..^(𝑁𝑀))) → ((𝑊 substr ⟨𝑀, 𝑁⟩)‘(𝑥 + 𝐾)) = (𝑊‘((𝑥 + 𝐾) + 𝑀)))
15572, 153, 154syl2anc 584 . . . . . . 7 (((((𝑊 ∈ Word 𝑉𝑁 ∈ (0...(♯‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ∧ (𝐾 ∈ (0...(𝑁𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁𝑀)))) ∧ 𝑦 ∈ (0..^(𝐿𝐾))) ∧ 𝑥 ∈ (0..^(𝐿𝐾))) → ((𝑊 substr ⟨𝑀, 𝑁⟩)‘(𝑥 + 𝐾)) = (𝑊‘((𝑥 + 𝐾) + 𝑀)))
156155mpteq2dva 5241 . . . . . 6 ((((𝑊 ∈ Word 𝑉𝑁 ∈ (0...(♯‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ∧ (𝐾 ∈ (0...(𝑁𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁𝑀)))) ∧ 𝑦 ∈ (0..^(𝐿𝐾))) → (𝑥 ∈ (0..^(𝐿𝐾)) ↦ ((𝑊 substr ⟨𝑀, 𝑁⟩)‘(𝑥 + 𝐾))) = (𝑥 ∈ (0..^(𝐿𝐾)) ↦ (𝑊‘((𝑥 + 𝐾) + 𝑀))))
157156fveq1d 6907 . . . . 5 ((((𝑊 ∈ Word 𝑉𝑁 ∈ (0...(♯‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ∧ (𝐾 ∈ (0...(𝑁𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁𝑀)))) ∧ 𝑦 ∈ (0..^(𝐿𝐾))) → ((𝑥 ∈ (0..^(𝐿𝐾)) ↦ ((𝑊 substr ⟨𝑀, 𝑁⟩)‘(𝑥 + 𝐾)))‘𝑦) = ((𝑥 ∈ (0..^(𝐿𝐾)) ↦ (𝑊‘((𝑥 + 𝐾) + 𝑀)))‘𝑦))
15825adantr 480 . . . . . 6 ((((𝑊 ∈ Word 𝑉𝑁 ∈ (0...(♯‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ∧ (𝐾 ∈ (0...(𝑁𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁𝑀)))) ∧ 𝑦 ∈ (0..^(𝐿𝐾))) → (𝑊 ∈ Word 𝑉 ∧ (𝑀 + 𝐾) ∈ (0...(𝑀 + 𝐿)) ∧ (𝑀 + 𝐿) ∈ (0...(♯‘𝑊))))
15931, 33, 353anim123i 1151 . . . . . . . . . . . . . . . . . 18 ((𝑀 ∈ ℤ ∧ 𝐿 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑀 ∈ ℂ ∧ 𝐿 ∈ ℂ ∧ 𝐾 ∈ ℂ))
1601593expa 1118 . . . . . . . . . . . . . . . . 17 (((𝑀 ∈ ℤ ∧ 𝐿 ∈ ℤ) ∧ 𝐾 ∈ ℤ) → (𝑀 ∈ ℂ ∧ 𝐿 ∈ ℂ ∧ 𝐾 ∈ ℂ))
161160, 38syl 17 . . . . . . . . . . . . . . . 16 (((𝑀 ∈ ℤ ∧ 𝐿 ∈ ℤ) ∧ 𝐾 ∈ ℤ) → (𝐿𝐾) = ((𝑀 + 𝐿) − (𝑀 + 𝐾)))
162161exp31 419 . . . . . . . . . . . . . . 15 (𝑀 ∈ ℤ → (𝐿 ∈ ℤ → (𝐾 ∈ ℤ → (𝐿𝐾) = ((𝑀 + 𝐿) − (𝑀 + 𝐾)))))
163162com3l 89 . . . . . . . . . . . . . 14 (𝐿 ∈ ℤ → (𝐾 ∈ ℤ → (𝑀 ∈ ℤ → (𝐿𝐾) = ((𝑀 + 𝐿) − (𝑀 + 𝐾)))))
16429, 163syl 17 . . . . . . . . . . . . 13 (𝐿 ∈ (𝐾...(𝑁𝑀)) → (𝐾 ∈ ℤ → (𝑀 ∈ ℤ → (𝐿𝐾) = ((𝑀 + 𝐿) − (𝑀 + 𝐾)))))
16530, 164mpan9 506 . . . . . . . . . . . 12 ((𝐾 ∈ (0...(𝑁𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁𝑀))) → (𝑀 ∈ ℤ → (𝐿𝐾) = ((𝑀 + 𝐿) − (𝑀 + 𝐾))))
16628, 165syl5com 31 . . . . . . . . . . 11 (𝑀 ∈ (0...𝑁) → ((𝐾 ∈ (0...(𝑁𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁𝑀))) → (𝐿𝐾) = ((𝑀 + 𝐿) − (𝑀 + 𝐾))))
1671663ad2ant3 1135 . . . . . . . . . 10 ((𝑊 ∈ Word 𝑉𝑁 ∈ (0...(♯‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) → ((𝐾 ∈ (0...(𝑁𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁𝑀))) → (𝐿𝐾) = ((𝑀 + 𝐿) − (𝑀 + 𝐾))))
168167imp 406 . . . . . . . . 9 (((𝑊 ∈ Word 𝑉𝑁 ∈ (0...(♯‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ∧ (𝐾 ∈ (0...(𝑁𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁𝑀)))) → (𝐿𝐾) = ((𝑀 + 𝐿) − (𝑀 + 𝐾)))
169168oveq2d 7448 . . . . . . . 8 (((𝑊 ∈ Word 𝑉𝑁 ∈ (0...(♯‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ∧ (𝐾 ∈ (0...(𝑁𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁𝑀)))) → (0..^(𝐿𝐾)) = (0..^((𝑀 + 𝐿) − (𝑀 + 𝐾))))
170169eleq2d 2826 . . . . . . 7 (((𝑊 ∈ Word 𝑉𝑁 ∈ (0...(♯‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ∧ (𝐾 ∈ (0...(𝑁𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁𝑀)))) → (𝑦 ∈ (0..^(𝐿𝐾)) ↔ 𝑦 ∈ (0..^((𝑀 + 𝐿) − (𝑀 + 𝐾)))))
171170biimpa 476 . . . . . 6 ((((𝑊 ∈ Word 𝑉𝑁 ∈ (0...(♯‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ∧ (𝐾 ∈ (0...(𝑁𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁𝑀)))) ∧ 𝑦 ∈ (0..^(𝐿𝐾))) → 𝑦 ∈ (0..^((𝑀 + 𝐿) − (𝑀 + 𝐾))))
172 swrdfv 14687 . . . . . 6 (((𝑊 ∈ Word 𝑉 ∧ (𝑀 + 𝐾) ∈ (0...(𝑀 + 𝐿)) ∧ (𝑀 + 𝐿) ∈ (0...(♯‘𝑊))) ∧ 𝑦 ∈ (0..^((𝑀 + 𝐿) − (𝑀 + 𝐾)))) → ((𝑊 substr ⟨(𝑀 + 𝐾), (𝑀 + 𝐿)⟩)‘𝑦) = (𝑊‘(𝑦 + (𝑀 + 𝐾))))
173158, 171, 172syl2anc 584 . . . . 5 ((((𝑊 ∈ Word 𝑉𝑁 ∈ (0...(♯‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ∧ (𝐾 ∈ (0...(𝑁𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁𝑀)))) ∧ 𝑦 ∈ (0..^(𝐿𝐾))) → ((𝑊 substr ⟨(𝑀 + 𝐾), (𝑀 + 𝐿)⟩)‘𝑦) = (𝑊‘(𝑦 + (𝑀 + 𝐾))))
17471, 157, 1733eqtr4d 2786 . . . 4 ((((𝑊 ∈ Word 𝑉𝑁 ∈ (0...(♯‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ∧ (𝐾 ∈ (0...(𝑁𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁𝑀)))) ∧ 𝑦 ∈ (0..^(𝐿𝐾))) → ((𝑥 ∈ (0..^(𝐿𝐾)) ↦ ((𝑊 substr ⟨𝑀, 𝑁⟩)‘(𝑥 + 𝐾)))‘𝑦) = ((𝑊 substr ⟨(𝑀 + 𝐾), (𝑀 + 𝐿)⟩)‘𝑦))
17524, 47, 174eqfnfvd 7053 . . 3 (((𝑊 ∈ Word 𝑉𝑁 ∈ (0...(♯‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ∧ (𝐾 ∈ (0...(𝑁𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁𝑀)))) → (𝑥 ∈ (0..^(𝐿𝐾)) ↦ ((𝑊 substr ⟨𝑀, 𝑁⟩)‘(𝑥 + 𝐾))) = (𝑊 substr ⟨(𝑀 + 𝐾), (𝑀 + 𝐿)⟩))
17620, 175eqtrd 2776 . 2 (((𝑊 ∈ Word 𝑉𝑁 ∈ (0...(♯‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ∧ (𝐾 ∈ (0...(𝑁𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁𝑀)))) → ((𝑊 substr ⟨𝑀, 𝑁⟩) substr ⟨𝐾, 𝐿⟩) = (𝑊 substr ⟨(𝑀 + 𝐾), (𝑀 + 𝐿)⟩))
177176ex 412 1 ((𝑊 ∈ Word 𝑉𝑁 ∈ (0...(♯‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) → ((𝐾 ∈ (0...(𝑁𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁𝑀))) → ((𝑊 substr ⟨𝑀, 𝑁⟩) substr ⟨𝐾, 𝐿⟩) = (𝑊 substr ⟨(𝑀 + 𝐾), (𝑀 + 𝐿)⟩)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  w3a 1086   = wceq 1539  wcel 2107  Vcvv 3479  wss 3950  cop 4631   class class class wbr 5142  cmpt 5224   Fn wfn 6555  cfv 6560  (class class class)co 7432  cc 11154  cr 11155  0cc0 11156   + caddc 11159   < clt 11296  cle 11297  cmin 11493  cn 12267  0cn0 12528  cz 12615  cuz 12879  ...cfz 13548  ..^cfzo 13695  chash 14370  Word cword 14553   substr csubstr 14679
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2707  ax-rep 5278  ax-sep 5295  ax-nul 5305  ax-pow 5364  ax-pr 5431  ax-un 7756  ax-cnex 11212  ax-resscn 11213  ax-1cn 11214  ax-icn 11215  ax-addcl 11216  ax-addrcl 11217  ax-mulcl 11218  ax-mulrcl 11219  ax-mulcom 11220  ax-addass 11221  ax-mulass 11222  ax-distr 11223  ax-i2m1 11224  ax-1ne0 11225  ax-1rid 11226  ax-rnegex 11227  ax-rrecex 11228  ax-cnre 11229  ax-pre-lttri 11230  ax-pre-lttrn 11231  ax-pre-ltadd 11232  ax-pre-mulgt0 11233
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2728  df-clel 2815  df-nfc 2891  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-reu 3380  df-rab 3436  df-v 3481  df-sbc 3788  df-csb 3899  df-dif 3953  df-un 3955  df-in 3957  df-ss 3967  df-pss 3970  df-nul 4333  df-if 4525  df-pw 4601  df-sn 4626  df-pr 4628  df-op 4632  df-uni 4907  df-int 4946  df-iun 4992  df-br 5143  df-opab 5205  df-mpt 5225  df-tr 5259  df-id 5577  df-eprel 5583  df-po 5591  df-so 5592  df-fr 5636  df-we 5638  df-xp 5690  df-rel 5691  df-cnv 5692  df-co 5693  df-dm 5694  df-rn 5695  df-res 5696  df-ima 5697  df-pred 6320  df-ord 6386  df-on 6387  df-lim 6388  df-suc 6389  df-iota 6513  df-fun 6562  df-fn 6563  df-f 6564  df-f1 6565  df-fo 6566  df-f1o 6567  df-fv 6568  df-riota 7389  df-ov 7435  df-oprab 7436  df-mpo 7437  df-om 7889  df-1st 8015  df-2nd 8016  df-frecs 8307  df-wrecs 8338  df-recs 8412  df-rdg 8451  df-1o 8507  df-er 8746  df-en 8987  df-dom 8988  df-sdom 8989  df-fin 8990  df-card 9980  df-pnf 11298  df-mnf 11299  df-xr 11300  df-ltxr 11301  df-le 11302  df-sub 11495  df-neg 11496  df-nn 12268  df-n0 12529  df-z 12616  df-uz 12880  df-fz 13549  df-fzo 13696  df-hash 14371  df-word 14554  df-substr 14680
This theorem is referenced by:  pfxswrd  14745  swrdpfx  14746
  Copyright terms: Public domain W3C validator