Theorem swrdrn3 31809

Description: Express the range of a subword. Stronger version of swrdrn2 31808. (Contributed by Thierry Arnoux, 13-Dec-2023.)

Assertion

Ref	Expression
swrdrn3	⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) → ran (𝑊 substr ⟨𝑀, 𝑁⟩) = (𝑊 “ (𝑀..^𝑁)))

Proof of Theorem swrdrn3

Dummy variables 𝑖 𝑗 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		simpr 485	. . . . . 6 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ 𝑖 ∈ (0..^(𝑁 − 𝑀))) → 𝑖 ∈ (0..^(𝑁 − 𝑀)))
2		simpl3 1193	. . . . . . 7 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ 𝑖 ∈ (0..^(𝑁 − 𝑀))) → 𝑁 ∈ (0...(♯‘𝑊)))
3	2	elfzelzd 13442	. . . . . 6 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ 𝑖 ∈ (0..^(𝑁 − 𝑀))) → 𝑁 ∈ ℤ)
4		simpl2 1192	. . . . . . 7 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ 𝑖 ∈ (0..^(𝑁 − 𝑀))) → 𝑀 ∈ (0...𝑁))
5	4	elfzelzd 13442	. . . . . 6 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ 𝑖 ∈ (0..^(𝑁 − 𝑀))) → 𝑀 ∈ ℤ)
6		fzoaddel2 13628	. . . . . 6 ⊢ ((𝑖 ∈ (0..^(𝑁 − 𝑀)) ∧ 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑖 + 𝑀) ∈ (𝑀..^𝑁))
7	1, 3, 5, 6	syl3anc 1371	. . . . 5 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ 𝑖 ∈ (0..^(𝑁 − 𝑀))) → (𝑖 + 𝑀) ∈ (𝑀..^𝑁))
8		simpr 485	. . . . . . . 8 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ 𝑗 ∈ (𝑀..^𝑁)) → 𝑗 ∈ (𝑀..^𝑁))
9		simpl2 1192	. . . . . . . . . . . 12 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ 𝑗 ∈ (𝑀..^𝑁)) → 𝑀 ∈ (0...𝑁))
10	9	elfzelzd 13442	. . . . . . . . . . 11 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ 𝑗 ∈ (𝑀..^𝑁)) → 𝑀 ∈ ℤ)
11	10	zcnd 12608	. . . . . . . . . 10 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ 𝑗 ∈ (𝑀..^𝑁)) → 𝑀 ∈ ℂ)
12		simpl3 1193	. . . . . . . . . . . 12 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ 𝑗 ∈ (𝑀..^𝑁)) → 𝑁 ∈ (0...(♯‘𝑊)))
13	12	elfzelzd 13442	. . . . . . . . . . 11 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ 𝑗 ∈ (𝑀..^𝑁)) → 𝑁 ∈ ℤ)
14	13	zcnd 12608	. . . . . . . . . 10 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ 𝑗 ∈ (𝑀..^𝑁)) → 𝑁 ∈ ℂ)
15	11, 14	pncan3d 11515	. . . . . . . . 9 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ 𝑗 ∈ (𝑀..^𝑁)) → (𝑀 + (𝑁 − 𝑀)) = 𝑁)
16	15	oveq2d 7373	. . . . . . . 8 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ 𝑗 ∈ (𝑀..^𝑁)) → (𝑀..^(𝑀 + (𝑁 − 𝑀))) = (𝑀..^𝑁))
17	8, 16	eleqtrrd 2841	. . . . . . 7 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ 𝑗 ∈ (𝑀..^𝑁)) → 𝑗 ∈ (𝑀..^(𝑀 + (𝑁 − 𝑀))))
18	13, 10	zsubcld 12612	. . . . . . 7 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ 𝑗 ∈ (𝑀..^𝑁)) → (𝑁 − 𝑀) ∈ ℤ)
19		fzosubel3 13633	. . . . . . 7 ⊢ ((𝑗 ∈ (𝑀..^(𝑀 + (𝑁 − 𝑀))) ∧ (𝑁 − 𝑀) ∈ ℤ) → (𝑗 − 𝑀) ∈ (0..^(𝑁 − 𝑀)))
20	17, 18, 19	syl2anc 584	. . . . . 6 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ 𝑗 ∈ (𝑀..^𝑁)) → (𝑗 − 𝑀) ∈ (0..^(𝑁 − 𝑀)))
21		simpr 485	. . . . . . . 8 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ 𝑗 ∈ (𝑀..^𝑁)) ∧ 𝑖 = (𝑗 − 𝑀)) → 𝑖 = (𝑗 − 𝑀))
22	21	oveq1d 7372	. . . . . . 7 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ 𝑗 ∈ (𝑀..^𝑁)) ∧ 𝑖 = (𝑗 − 𝑀)) → (𝑖 + 𝑀) = ((𝑗 − 𝑀) + 𝑀))
23	22	eqeq2d 2747	. . . . . 6 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ 𝑗 ∈ (𝑀..^𝑁)) ∧ 𝑖 = (𝑗 − 𝑀)) → (𝑗 = (𝑖 + 𝑀) ↔ 𝑗 = ((𝑗 − 𝑀) + 𝑀)))
24		fzossz 13592	. . . . . . . . . 10 ⊢ (𝑀..^𝑁) ⊆ ℤ
25	24, 8	sselid 3942	. . . . . . . . 9 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ 𝑗 ∈ (𝑀..^𝑁)) → 𝑗 ∈ ℤ)
26	25	zcnd 12608	. . . . . . . 8 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ 𝑗 ∈ (𝑀..^𝑁)) → 𝑗 ∈ ℂ)
27	26, 11	npcand 11516	. . . . . . 7 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ 𝑗 ∈ (𝑀..^𝑁)) → ((𝑗 − 𝑀) + 𝑀) = 𝑗)
28	27	eqcomd 2742	. . . . . 6 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ 𝑗 ∈ (𝑀..^𝑁)) → 𝑗 = ((𝑗 − 𝑀) + 𝑀))
29	20, 23, 28	rspcedvd 3583	. . . . 5 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ 𝑗 ∈ (𝑀..^𝑁)) → ∃𝑖 ∈ (0..^(𝑁 − 𝑀))𝑗 = (𝑖 + 𝑀))
30		eqcom 2743	. . . . . 6 ⊢ (𝑦 = (𝑊‘𝑗) ↔ (𝑊‘𝑗) = 𝑦)
31		simpr 485	. . . . . . . 8 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ 𝑗 = (𝑖 + 𝑀)) → 𝑗 = (𝑖 + 𝑀))
32	31	fveq2d 6846	. . . . . . 7 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ 𝑗 = (𝑖 + 𝑀)) → (𝑊‘𝑗) = (𝑊‘(𝑖 + 𝑀)))
33	32	eqeq2d 2747	. . . . . 6 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ 𝑗 = (𝑖 + 𝑀)) → (𝑦 = (𝑊‘𝑗) ↔ 𝑦 = (𝑊‘(𝑖 + 𝑀))))
34	30, 33	bitr3id 284	. . . . 5 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ 𝑗 = (𝑖 + 𝑀)) → ((𝑊‘𝑗) = 𝑦 ↔ 𝑦 = (𝑊‘(𝑖 + 𝑀))))
35	7, 29, 34	rexxfrd 5364	. . . 4 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) → (∃𝑗 ∈ (𝑀..^𝑁)(𝑊‘𝑗) = 𝑦 ↔ ∃𝑖 ∈ (0..^(𝑁 − 𝑀))𝑦 = (𝑊‘(𝑖 + 𝑀))))
36		eqid 2736	. . . . 5 ⊢ (𝑖 ∈ (0..^(𝑁 − 𝑀)) ↦ (𝑊‘(𝑖 + 𝑀))) = (𝑖 ∈ (0..^(𝑁 − 𝑀)) ↦ (𝑊‘(𝑖 + 𝑀)))
37		fvex 6855	. . . . 5 ⊢ (𝑊‘(𝑖 + 𝑀)) ∈ V
38	36, 37	elrnmpti 5915	. . . 4 ⊢ (𝑦 ∈ ran (𝑖 ∈ (0..^(𝑁 − 𝑀)) ↦ (𝑊‘(𝑖 + 𝑀))) ↔ ∃𝑖 ∈ (0..^(𝑁 − 𝑀))𝑦 = (𝑊‘(𝑖 + 𝑀)))
39	35, 38	bitr4di 288	. . 3 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) → (∃𝑗 ∈ (𝑀..^𝑁)(𝑊‘𝑗) = 𝑦 ↔ 𝑦 ∈ ran (𝑖 ∈ (0..^(𝑁 − 𝑀)) ↦ (𝑊‘(𝑖 + 𝑀)))))
40		wrdf 14407	. . . . . 6 ⊢ (𝑊 ∈ Word 𝑉 → 𝑊:(0..^(♯‘𝑊))⟶𝑉)
41	40	3ad2ant1 1133	. . . . 5 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) → 𝑊:(0..^(♯‘𝑊))⟶𝑉)
42	41	ffnd 6669	. . . 4 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) → 𝑊 Fn (0..^(♯‘𝑊)))
43		elfzuz 13437	. . . . . . 7 ⊢ (𝑀 ∈ (0...𝑁) → 𝑀 ∈ (ℤ≥‘0))
44	43	3ad2ant2 1134	. . . . . 6 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) → 𝑀 ∈ (ℤ≥‘0))
45		fzoss1 13599	. . . . . 6 ⊢ (𝑀 ∈ (ℤ≥‘0) → (𝑀..^𝑁) ⊆ (0..^𝑁))
46	44, 45	syl 17	. . . . 5 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) → (𝑀..^𝑁) ⊆ (0..^𝑁))
47		elfzuz3 13438	. . . . . . 7 ⊢ (𝑁 ∈ (0...(♯‘𝑊)) → (♯‘𝑊) ∈ (ℤ≥‘𝑁))
48	47	3ad2ant3 1135	. . . . . 6 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) → (♯‘𝑊) ∈ (ℤ≥‘𝑁))
49		fzoss2 13600	. . . . . 6 ⊢ ((♯‘𝑊) ∈ (ℤ≥‘𝑁) → (0..^𝑁) ⊆ (0..^(♯‘𝑊)))
50	48, 49	syl 17	. . . . 5 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) → (0..^𝑁) ⊆ (0..^(♯‘𝑊)))
51	46, 50	sstrd 3954	. . . 4 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) → (𝑀..^𝑁) ⊆ (0..^(♯‘𝑊)))
52	42, 51	fvelimabd 6915	. . 3 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) → (𝑦 ∈ (𝑊 “ (𝑀..^𝑁)) ↔ ∃𝑗 ∈ (𝑀..^𝑁)(𝑊‘𝑗) = 𝑦))
53		swrdval2 14534	. . . . 5 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) → (𝑊 substr ⟨𝑀, 𝑁⟩) = (𝑖 ∈ (0..^(𝑁 − 𝑀)) ↦ (𝑊‘(𝑖 + 𝑀))))
54	53	rneqd 5893	. . . 4 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) → ran (𝑊 substr ⟨𝑀, 𝑁⟩) = ran (𝑖 ∈ (0..^(𝑁 − 𝑀)) ↦ (𝑊‘(𝑖 + 𝑀))))
55	54	eleq2d 2823	. . 3 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) → (𝑦 ∈ ran (𝑊 substr ⟨𝑀, 𝑁⟩) ↔ 𝑦 ∈ ran (𝑖 ∈ (0..^(𝑁 − 𝑀)) ↦ (𝑊‘(𝑖 + 𝑀)))))
56	39, 52, 55	3bitr4rd 311	. 2 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) → (𝑦 ∈ ran (𝑊 substr ⟨𝑀, 𝑁⟩) ↔ 𝑦 ∈ (𝑊 “ (𝑀..^𝑁))))
57	56	eqrdv 2734	1 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) → ran (𝑊 substr ⟨𝑀, 𝑁⟩) = (𝑊 “ (𝑀..^𝑁)))

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1087   = wceq 1541   ∈ wcel 2106  ∃wrex 3073   ⊆ wss 3910  ⟨cop 4592   ↦ cmpt 5188  ran crn 5634   “ cima 5636  ⟶wf 6492  ‘cfv 6496  (class class class)co 7357  0cc0 11051   + caddc 11054   − cmin 11385  ℤcz 12499  ℤ_≥cuz 12763  ...cfz 13424  ..^cfzo 13567  ♯chash 14230  Word cword 14402   substr csubstr 14528

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672  ax-cnex 11107  ax-resscn 11108  ax-1cn 11109  ax-icn 11110  ax-addcl 11111  ax-addrcl 11112  ax-mulcl 11113  ax-mulrcl 11114  ax-mulcom 11115  ax-addass 11116  ax-mulass 11117  ax-distr 11118  ax-i2m1 11119  ax-1ne0 11120  ax-1rid 11121  ax-rnegex 11122  ax-rrecex 11123  ax-cnre 11124  ax-pre-lttri 11125  ax-pre-lttrn 11126  ax-pre-ltadd 11127  ax-pre-mulgt0 11128

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3065  df-rex 3074  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-int 4908  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-riota 7313  df-ov 7360  df-oprab 7361  df-mpo 7362  df-om 7803  df-1st 7921  df-2nd 7922  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-rdg 8356  df-1o 8412  df-er 8648  df-en 8884  df-dom 8885  df-sdom 8886  df-fin 8887  df-card 9875  df-pnf 11191  df-mnf 11192  df-xr 11193  df-ltxr 11194  df-le 11195  df-sub 11387  df-neg 11388  df-nn 12154  df-n0 12414  df-z 12500  df-uz 12764  df-fz 13425  df-fzo 13568  df-hash 14231  df-word 14403  df-substr 14529

This theorem is referenced by:  swrdrndisj  31811  cycpmco2rn  31974