Theorem ccatswrd 13870

Description: Joining two adjacent subwords makes a longer subword. (Contributed by Stefan O'Rear, 20-Aug-2015.)

Assertion

Ref	Expression
ccatswrd	⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) → ((𝑆 substr ⟨𝑋, 𝑌⟩) ++ (𝑆 substr ⟨𝑌, 𝑍⟩)) = (𝑆 substr ⟨𝑋, 𝑍⟩))

Proof of Theorem ccatswrd

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		swrdcl 13847	. . . . . 6 ⊢ (𝑆 ∈ Word 𝐴 → (𝑆 substr ⟨𝑋, 𝑌⟩) ∈ Word 𝐴)
2	1	adantr 481	. . . . 5 ⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) → (𝑆 substr ⟨𝑋, 𝑌⟩) ∈ Word 𝐴)
3		swrdcl 13847	. . . . . 6 ⊢ (𝑆 ∈ Word 𝐴 → (𝑆 substr ⟨𝑌, 𝑍⟩) ∈ Word 𝐴)
4	3	adantr 481	. . . . 5 ⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) → (𝑆 substr ⟨𝑌, 𝑍⟩) ∈ Word 𝐴)
5		ccatcl 13776	. . . . 5 ⊢ (((𝑆 substr ⟨𝑋, 𝑌⟩) ∈ Word 𝐴 ∧ (𝑆 substr ⟨𝑌, 𝑍⟩) ∈ Word 𝐴) → ((𝑆 substr ⟨𝑋, 𝑌⟩) ++ (𝑆 substr ⟨𝑌, 𝑍⟩)) ∈ Word 𝐴)
6	2, 4, 5	syl2anc 584	. . . 4 ⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) → ((𝑆 substr ⟨𝑋, 𝑌⟩) ++ (𝑆 substr ⟨𝑌, 𝑍⟩)) ∈ Word 𝐴)
7		wrdf 13716	. . . 4 ⊢ (((𝑆 substr ⟨𝑋, 𝑌⟩) ++ (𝑆 substr ⟨𝑌, 𝑍⟩)) ∈ Word 𝐴 → ((𝑆 substr ⟨𝑋, 𝑌⟩) ++ (𝑆 substr ⟨𝑌, 𝑍⟩)):(0..^(♯‘((𝑆 substr ⟨𝑋, 𝑌⟩) ++ (𝑆 substr ⟨𝑌, 𝑍⟩))))⟶𝐴)
8		ffn 6389	. . . 4 ⊢ (((𝑆 substr ⟨𝑋, 𝑌⟩) ++ (𝑆 substr ⟨𝑌, 𝑍⟩)):(0..^(♯‘((𝑆 substr ⟨𝑋, 𝑌⟩) ++ (𝑆 substr ⟨𝑌, 𝑍⟩))))⟶𝐴 → ((𝑆 substr ⟨𝑋, 𝑌⟩) ++ (𝑆 substr ⟨𝑌, 𝑍⟩)) Fn (0..^(♯‘((𝑆 substr ⟨𝑋, 𝑌⟩) ++ (𝑆 substr ⟨𝑌, 𝑍⟩)))))
9	6, 7, 8	3syl 18	. . 3 ⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) → ((𝑆 substr ⟨𝑋, 𝑌⟩) ++ (𝑆 substr ⟨𝑌, 𝑍⟩)) Fn (0..^(♯‘((𝑆 substr ⟨𝑋, 𝑌⟩) ++ (𝑆 substr ⟨𝑌, 𝑍⟩)))))
10		ccatlen 13777	. . . . . . 7 ⊢ (((𝑆 substr ⟨𝑋, 𝑌⟩) ∈ Word 𝐴 ∧ (𝑆 substr ⟨𝑌, 𝑍⟩) ∈ Word 𝐴) → (♯‘((𝑆 substr ⟨𝑋, 𝑌⟩) ++ (𝑆 substr ⟨𝑌, 𝑍⟩))) = ((♯‘(𝑆 substr ⟨𝑋, 𝑌⟩)) + (♯‘(𝑆 substr ⟨𝑌, 𝑍⟩))))
11	2, 4, 10	syl2anc 584	. . . . . 6 ⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) → (♯‘((𝑆 substr ⟨𝑋, 𝑌⟩) ++ (𝑆 substr ⟨𝑌, 𝑍⟩))) = ((♯‘(𝑆 substr ⟨𝑋, 𝑌⟩)) + (♯‘(𝑆 substr ⟨𝑌, 𝑍⟩))))
12		simpl 483	. . . . . . . . 9 ⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) → 𝑆 ∈ Word 𝐴)
13		simpr1 1187	. . . . . . . . 9 ⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) → 𝑋 ∈ (0...𝑌))
14		simpr2 1188	. . . . . . . . . 10 ⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) → 𝑌 ∈ (0...𝑍))
15		simpr3 1189	. . . . . . . . . 10 ⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) → 𝑍 ∈ (0...(♯‘𝑆)))
16		fzass4 12799	. . . . . . . . . . . 12 ⊢ ((𝑌 ∈ (0...(♯‘𝑆)) ∧ 𝑍 ∈ (𝑌...(♯‘𝑆))) ↔ (𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆))))
17	16	biimpri 229	. . . . . . . . . . 11 ⊢ ((𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆))) → (𝑌 ∈ (0...(♯‘𝑆)) ∧ 𝑍 ∈ (𝑌...(♯‘𝑆))))
18	17	simpld 495	. . . . . . . . . 10 ⊢ ((𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆))) → 𝑌 ∈ (0...(♯‘𝑆)))
19	14, 15, 18	syl2anc 584	. . . . . . . . 9 ⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) → 𝑌 ∈ (0...(♯‘𝑆)))
20		swrdlen 13849	. . . . . . . . 9 ⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...(♯‘𝑆))) → (♯‘(𝑆 substr ⟨𝑋, 𝑌⟩)) = (𝑌 − 𝑋))
21	12, 13, 19, 20	syl3anc 1364	. . . . . . . 8 ⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) → (♯‘(𝑆 substr ⟨𝑋, 𝑌⟩)) = (𝑌 − 𝑋))
22		swrdlen 13849	. . . . . . . . 9 ⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆))) → (♯‘(𝑆 substr ⟨𝑌, 𝑍⟩)) = (𝑍 − 𝑌))
23	12, 14, 15, 22	syl3anc 1364	. . . . . . . 8 ⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) → (♯‘(𝑆 substr ⟨𝑌, 𝑍⟩)) = (𝑍 − 𝑌))
24	21, 23	oveq12d 7041	. . . . . . 7 ⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) → ((♯‘(𝑆 substr ⟨𝑋, 𝑌⟩)) + (♯‘(𝑆 substr ⟨𝑌, 𝑍⟩))) = ((𝑌 − 𝑋) + (𝑍 − 𝑌)))
25		elfzelz 12762	. . . . . . . . . 10 ⊢ (𝑌 ∈ (0...𝑍) → 𝑌 ∈ ℤ)
26	14, 25	syl 17	. . . . . . . . 9 ⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) → 𝑌 ∈ ℤ)
27	26	zcnd 11942	. . . . . . . 8 ⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) → 𝑌 ∈ ℂ)
28		elfzelz 12762	. . . . . . . . . 10 ⊢ (𝑋 ∈ (0...𝑌) → 𝑋 ∈ ℤ)
29	13, 28	syl 17	. . . . . . . . 9 ⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) → 𝑋 ∈ ℤ)
30	29	zcnd 11942	. . . . . . . 8 ⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) → 𝑋 ∈ ℂ)
31		elfzelz 12762	. . . . . . . . . 10 ⊢ (𝑍 ∈ (0...(♯‘𝑆)) → 𝑍 ∈ ℤ)
32	15, 31	syl 17	. . . . . . . . 9 ⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) → 𝑍 ∈ ℤ)
33	32	zcnd 11942	. . . . . . . 8 ⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) → 𝑍 ∈ ℂ)
34	27, 30, 33	npncan3d 10887	. . . . . . 7 ⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) → ((𝑌 − 𝑋) + (𝑍 − 𝑌)) = (𝑍 − 𝑋))
35	24, 34	eqtrd 2833	. . . . . 6 ⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) → ((♯‘(𝑆 substr ⟨𝑋, 𝑌⟩)) + (♯‘(𝑆 substr ⟨𝑌, 𝑍⟩))) = (𝑍 − 𝑋))
36	11, 35	eqtrd 2833	. . . . 5 ⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) → (♯‘((𝑆 substr ⟨𝑋, 𝑌⟩) ++ (𝑆 substr ⟨𝑌, 𝑍⟩))) = (𝑍 − 𝑋))
37	36	oveq2d 7039	. . . 4 ⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) → (0..^(♯‘((𝑆 substr ⟨𝑋, 𝑌⟩) ++ (𝑆 substr ⟨𝑌, 𝑍⟩)))) = (0..^(𝑍 − 𝑋)))
38	37	fneq2d 6324	. . 3 ⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) → (((𝑆 substr ⟨𝑋, 𝑌⟩) ++ (𝑆 substr ⟨𝑌, 𝑍⟩)) Fn (0..^(♯‘((𝑆 substr ⟨𝑋, 𝑌⟩) ++ (𝑆 substr ⟨𝑌, 𝑍⟩)))) ↔ ((𝑆 substr ⟨𝑋, 𝑌⟩) ++ (𝑆 substr ⟨𝑌, 𝑍⟩)) Fn (0..^(𝑍 − 𝑋))))
39	9, 38	mpbid 233	. 2 ⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) → ((𝑆 substr ⟨𝑋, 𝑌⟩) ++ (𝑆 substr ⟨𝑌, 𝑍⟩)) Fn (0..^(𝑍 − 𝑋)))
40		swrdcl 13847	. . . . 5 ⊢ (𝑆 ∈ Word 𝐴 → (𝑆 substr ⟨𝑋, 𝑍⟩) ∈ Word 𝐴)
41	40	adantr 481	. . . 4 ⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) → (𝑆 substr ⟨𝑋, 𝑍⟩) ∈ Word 𝐴)
42		wrdf 13716	. . . 4 ⊢ ((𝑆 substr ⟨𝑋, 𝑍⟩) ∈ Word 𝐴 → (𝑆 substr ⟨𝑋, 𝑍⟩):(0..^(♯‘(𝑆 substr ⟨𝑋, 𝑍⟩)))⟶𝐴)
43		ffn 6389	. . . 4 ⊢ ((𝑆 substr ⟨𝑋, 𝑍⟩):(0..^(♯‘(𝑆 substr ⟨𝑋, 𝑍⟩)))⟶𝐴 → (𝑆 substr ⟨𝑋, 𝑍⟩) Fn (0..^(♯‘(𝑆 substr ⟨𝑋, 𝑍⟩))))
44	41, 42, 43	3syl 18	. . 3 ⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) → (𝑆 substr ⟨𝑋, 𝑍⟩) Fn (0..^(♯‘(𝑆 substr ⟨𝑋, 𝑍⟩))))
45		fzass4 12799	. . . . . . . . 9 ⊢ ((𝑋 ∈ (0...𝑍) ∧ 𝑌 ∈ (𝑋...𝑍)) ↔ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍)))
46	45	biimpri 229	. . . . . . . 8 ⊢ ((𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍)) → (𝑋 ∈ (0...𝑍) ∧ 𝑌 ∈ (𝑋...𝑍)))
47	46	simpld 495	. . . . . . 7 ⊢ ((𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍)) → 𝑋 ∈ (0...𝑍))
48	13, 14, 47	syl2anc 584	. . . . . 6 ⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) → 𝑋 ∈ (0...𝑍))
49		swrdlen 13849	. . . . . 6 ⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑋 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆))) → (♯‘(𝑆 substr ⟨𝑋, 𝑍⟩)) = (𝑍 − 𝑋))
50	12, 48, 15, 49	syl3anc 1364	. . . . 5 ⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) → (♯‘(𝑆 substr ⟨𝑋, 𝑍⟩)) = (𝑍 − 𝑋))
51	50	oveq2d 7039	. . . 4 ⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) → (0..^(♯‘(𝑆 substr ⟨𝑋, 𝑍⟩))) = (0..^(𝑍 − 𝑋)))
52	51	fneq2d 6324	. . 3 ⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) → ((𝑆 substr ⟨𝑋, 𝑍⟩) Fn (0..^(♯‘(𝑆 substr ⟨𝑋, 𝑍⟩))) ↔ (𝑆 substr ⟨𝑋, 𝑍⟩) Fn (0..^(𝑍 − 𝑋))))
53	44, 52	mpbid 233	. 2 ⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) → (𝑆 substr ⟨𝑋, 𝑍⟩) Fn (0..^(𝑍 − 𝑋)))
54		simpr 485	. . . . 5 ⊢ (((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) ∧ 𝑥 ∈ (0..^(𝑍 − 𝑋))) → 𝑥 ∈ (0..^(𝑍 − 𝑋)))
55	26, 29	zsubcld 11946	. . . . . 6 ⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) → (𝑌 − 𝑋) ∈ ℤ)
56	55	adantr 481	. . . . 5 ⊢ (((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) ∧ 𝑥 ∈ (0..^(𝑍 − 𝑋))) → (𝑌 − 𝑋) ∈ ℤ)
57		fzospliti 12923	. . . . 5 ⊢ ((𝑥 ∈ (0..^(𝑍 − 𝑋)) ∧ (𝑌 − 𝑋) ∈ ℤ) → (𝑥 ∈ (0..^(𝑌 − 𝑋)) ∨ 𝑥 ∈ ((𝑌 − 𝑋)..^(𝑍 − 𝑋))))
58	54, 56, 57	syl2anc 584	. . . 4 ⊢ (((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) ∧ 𝑥 ∈ (0..^(𝑍 − 𝑋))) → (𝑥 ∈ (0..^(𝑌 − 𝑋)) ∨ 𝑥 ∈ ((𝑌 − 𝑋)..^(𝑍 − 𝑋))))
59	2	adantr 481	. . . . . . 7 ⊢ (((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) ∧ 𝑥 ∈ (0..^(𝑌 − 𝑋))) → (𝑆 substr ⟨𝑋, 𝑌⟩) ∈ Word 𝐴)
60	4	adantr 481	. . . . . . 7 ⊢ (((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) ∧ 𝑥 ∈ (0..^(𝑌 − 𝑋))) → (𝑆 substr ⟨𝑌, 𝑍⟩) ∈ Word 𝐴)
61	21	oveq2d 7039	. . . . . . . . 9 ⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) → (0..^(♯‘(𝑆 substr ⟨𝑋, 𝑌⟩))) = (0..^(𝑌 − 𝑋)))
62	61	eleq2d 2870	. . . . . . . 8 ⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) → (𝑥 ∈ (0..^(♯‘(𝑆 substr ⟨𝑋, 𝑌⟩))) ↔ 𝑥 ∈ (0..^(𝑌 − 𝑋))))
63	62	biimpar 478	. . . . . . 7 ⊢ (((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) ∧ 𝑥 ∈ (0..^(𝑌 − 𝑋))) → 𝑥 ∈ (0..^(♯‘(𝑆 substr ⟨𝑋, 𝑌⟩))))
64		ccatval1 13779	. . . . . . 7 ⊢ (((𝑆 substr ⟨𝑋, 𝑌⟩) ∈ Word 𝐴 ∧ (𝑆 substr ⟨𝑌, 𝑍⟩) ∈ Word 𝐴 ∧ 𝑥 ∈ (0..^(♯‘(𝑆 substr ⟨𝑋, 𝑌⟩)))) → (((𝑆 substr ⟨𝑋, 𝑌⟩) ++ (𝑆 substr ⟨𝑌, 𝑍⟩))‘𝑥) = ((𝑆 substr ⟨𝑋, 𝑌⟩)‘𝑥))
65	59, 60, 63, 64	syl3anc 1364	. . . . . 6 ⊢ (((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) ∧ 𝑥 ∈ (0..^(𝑌 − 𝑋))) → (((𝑆 substr ⟨𝑋, 𝑌⟩) ++ (𝑆 substr ⟨𝑌, 𝑍⟩))‘𝑥) = ((𝑆 substr ⟨𝑋, 𝑌⟩)‘𝑥))
66		simpll 763	. . . . . . 7 ⊢ (((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) ∧ 𝑥 ∈ (0..^(𝑌 − 𝑋))) → 𝑆 ∈ Word 𝐴)
67		simplr1 1208	. . . . . . 7 ⊢ (((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) ∧ 𝑥 ∈ (0..^(𝑌 − 𝑋))) → 𝑋 ∈ (0...𝑌))
68	19	adantr 481	. . . . . . 7 ⊢ (((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) ∧ 𝑥 ∈ (0..^(𝑌 − 𝑋))) → 𝑌 ∈ (0...(♯‘𝑆)))
69		simpr 485	. . . . . . 7 ⊢ (((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) ∧ 𝑥 ∈ (0..^(𝑌 − 𝑋))) → 𝑥 ∈ (0..^(𝑌 − 𝑋)))
70		swrdfv 13850	. . . . . . 7 ⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...(♯‘𝑆))) ∧ 𝑥 ∈ (0..^(𝑌 − 𝑋))) → ((𝑆 substr ⟨𝑋, 𝑌⟩)‘𝑥) = (𝑆‘(𝑥 + 𝑋)))
71	66, 67, 68, 69, 70	syl31anc 1366	. . . . . 6 ⊢ (((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) ∧ 𝑥 ∈ (0..^(𝑌 − 𝑋))) → ((𝑆 substr ⟨𝑋, 𝑌⟩)‘𝑥) = (𝑆‘(𝑥 + 𝑋)))
72	65, 71	eqtrd 2833	. . . . 5 ⊢ (((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) ∧ 𝑥 ∈ (0..^(𝑌 − 𝑋))) → (((𝑆 substr ⟨𝑋, 𝑌⟩) ++ (𝑆 substr ⟨𝑌, 𝑍⟩))‘𝑥) = (𝑆‘(𝑥 + 𝑋)))
73	2	adantr 481	. . . . . . 7 ⊢ (((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) ∧ 𝑥 ∈ ((𝑌 − 𝑋)..^(𝑍 − 𝑋))) → (𝑆 substr ⟨𝑋, 𝑌⟩) ∈ Word 𝐴)
74	4	adantr 481	. . . . . . 7 ⊢ (((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) ∧ 𝑥 ∈ ((𝑌 − 𝑋)..^(𝑍 − 𝑋))) → (𝑆 substr ⟨𝑌, 𝑍⟩) ∈ Word 𝐴)
75	21, 35	oveq12d 7041	. . . . . . . . 9 ⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) → ((♯‘(𝑆 substr ⟨𝑋, 𝑌⟩))..^((♯‘(𝑆 substr ⟨𝑋, 𝑌⟩)) + (♯‘(𝑆 substr ⟨𝑌, 𝑍⟩)))) = ((𝑌 − 𝑋)..^(𝑍 − 𝑋)))
76	75	eleq2d 2870	. . . . . . . 8 ⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) → (𝑥 ∈ ((♯‘(𝑆 substr ⟨𝑋, 𝑌⟩))..^((♯‘(𝑆 substr ⟨𝑋, 𝑌⟩)) + (♯‘(𝑆 substr ⟨𝑌, 𝑍⟩)))) ↔ 𝑥 ∈ ((𝑌 − 𝑋)..^(𝑍 − 𝑋))))
77	76	biimpar 478	. . . . . . 7 ⊢ (((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) ∧ 𝑥 ∈ ((𝑌 − 𝑋)..^(𝑍 − 𝑋))) → 𝑥 ∈ ((♯‘(𝑆 substr ⟨𝑋, 𝑌⟩))..^((♯‘(𝑆 substr ⟨𝑋, 𝑌⟩)) + (♯‘(𝑆 substr ⟨𝑌, 𝑍⟩)))))
78		ccatval2 13780	. . . . . . 7 ⊢ (((𝑆 substr ⟨𝑋, 𝑌⟩) ∈ Word 𝐴 ∧ (𝑆 substr ⟨𝑌, 𝑍⟩) ∈ Word 𝐴 ∧ 𝑥 ∈ ((♯‘(𝑆 substr ⟨𝑋, 𝑌⟩))..^((♯‘(𝑆 substr ⟨𝑋, 𝑌⟩)) + (♯‘(𝑆 substr ⟨𝑌, 𝑍⟩))))) → (((𝑆 substr ⟨𝑋, 𝑌⟩) ++ (𝑆 substr ⟨𝑌, 𝑍⟩))‘𝑥) = ((𝑆 substr ⟨𝑌, 𝑍⟩)‘(𝑥 − (♯‘(𝑆 substr ⟨𝑋, 𝑌⟩)))))
79	73, 74, 77, 78	syl3anc 1364	. . . . . 6 ⊢ (((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) ∧ 𝑥 ∈ ((𝑌 − 𝑋)..^(𝑍 − 𝑋))) → (((𝑆 substr ⟨𝑋, 𝑌⟩) ++ (𝑆 substr ⟨𝑌, 𝑍⟩))‘𝑥) = ((𝑆 substr ⟨𝑌, 𝑍⟩)‘(𝑥 − (♯‘(𝑆 substr ⟨𝑋, 𝑌⟩)))))
80		simpll 763	. . . . . . 7 ⊢ (((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) ∧ 𝑥 ∈ ((𝑌 − 𝑋)..^(𝑍 − 𝑋))) → 𝑆 ∈ Word 𝐴)
81		simplr2 1209	. . . . . . 7 ⊢ (((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) ∧ 𝑥 ∈ ((𝑌 − 𝑋)..^(𝑍 − 𝑋))) → 𝑌 ∈ (0...𝑍))
82		simplr3 1210	. . . . . . 7 ⊢ (((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) ∧ 𝑥 ∈ ((𝑌 − 𝑋)..^(𝑍 − 𝑋))) → 𝑍 ∈ (0...(♯‘𝑆)))
83	21	oveq2d 7039	. . . . . . . . 9 ⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) → (𝑥 − (♯‘(𝑆 substr ⟨𝑋, 𝑌⟩))) = (𝑥 − (𝑌 − 𝑋)))
84	83	adantr 481	. . . . . . . 8 ⊢ (((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) ∧ 𝑥 ∈ ((𝑌 − 𝑋)..^(𝑍 − 𝑋))) → (𝑥 − (♯‘(𝑆 substr ⟨𝑋, 𝑌⟩))) = (𝑥 − (𝑌 − 𝑋)))
85	34	oveq2d 7039	. . . . . . . . . . 11 ⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) → ((𝑌 − 𝑋)..^((𝑌 − 𝑋) + (𝑍 − 𝑌))) = ((𝑌 − 𝑋)..^(𝑍 − 𝑋)))
86	85	eleq2d 2870	. . . . . . . . . 10 ⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) → (𝑥 ∈ ((𝑌 − 𝑋)..^((𝑌 − 𝑋) + (𝑍 − 𝑌))) ↔ 𝑥 ∈ ((𝑌 − 𝑋)..^(𝑍 − 𝑋))))
87	86	biimpar 478	. . . . . . . . 9 ⊢ (((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) ∧ 𝑥 ∈ ((𝑌 − 𝑋)..^(𝑍 − 𝑋))) → 𝑥 ∈ ((𝑌 − 𝑋)..^((𝑌 − 𝑋) + (𝑍 − 𝑌))))
88	32, 26	zsubcld 11946	. . . . . . . . . 10 ⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) → (𝑍 − 𝑌) ∈ ℤ)
89	88	adantr 481	. . . . . . . . 9 ⊢ (((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) ∧ 𝑥 ∈ ((𝑌 − 𝑋)..^(𝑍 − 𝑋))) → (𝑍 − 𝑌) ∈ ℤ)
90		fzosubel3 12952	. . . . . . . . 9 ⊢ ((𝑥 ∈ ((𝑌 − 𝑋)..^((𝑌 − 𝑋) + (𝑍 − 𝑌))) ∧ (𝑍 − 𝑌) ∈ ℤ) → (𝑥 − (𝑌 − 𝑋)) ∈ (0..^(𝑍 − 𝑌)))
91	87, 89, 90	syl2anc 584	. . . . . . . 8 ⊢ (((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) ∧ 𝑥 ∈ ((𝑌 − 𝑋)..^(𝑍 − 𝑋))) → (𝑥 − (𝑌 − 𝑋)) ∈ (0..^(𝑍 − 𝑌)))
92	84, 91	eqeltrd 2885	. . . . . . 7 ⊢ (((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) ∧ 𝑥 ∈ ((𝑌 − 𝑋)..^(𝑍 − 𝑋))) → (𝑥 − (♯‘(𝑆 substr ⟨𝑋, 𝑌⟩))) ∈ (0..^(𝑍 − 𝑌)))
93		swrdfv 13850	. . . . . . 7 ⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆))) ∧ (𝑥 − (♯‘(𝑆 substr ⟨𝑋, 𝑌⟩))) ∈ (0..^(𝑍 − 𝑌))) → ((𝑆 substr ⟨𝑌, 𝑍⟩)‘(𝑥 − (♯‘(𝑆 substr ⟨𝑋, 𝑌⟩)))) = (𝑆‘((𝑥 − (♯‘(𝑆 substr ⟨𝑋, 𝑌⟩))) + 𝑌)))
94	80, 81, 82, 92, 93	syl31anc 1366	. . . . . 6 ⊢ (((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) ∧ 𝑥 ∈ ((𝑌 − 𝑋)..^(𝑍 − 𝑋))) → ((𝑆 substr ⟨𝑌, 𝑍⟩)‘(𝑥 − (♯‘(𝑆 substr ⟨𝑋, 𝑌⟩)))) = (𝑆‘((𝑥 − (♯‘(𝑆 substr ⟨𝑋, 𝑌⟩))) + 𝑌)))
95	83	oveq1d 7038	. . . . . . . . 9 ⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) → ((𝑥 − (♯‘(𝑆 substr ⟨𝑋, 𝑌⟩))) + 𝑌) = ((𝑥 − (𝑌 − 𝑋)) + 𝑌))
96	95	adantr 481	. . . . . . . 8 ⊢ (((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) ∧ 𝑥 ∈ ((𝑌 − 𝑋)..^(𝑍 − 𝑋))) → ((𝑥 − (♯‘(𝑆 substr ⟨𝑋, 𝑌⟩))) + 𝑌) = ((𝑥 − (𝑌 − 𝑋)) + 𝑌))
97		elfzoelz 12892	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ((𝑌 − 𝑋)..^(𝑍 − 𝑋)) → 𝑥 ∈ ℤ)
98	97	zcnd 11942	. . . . . . . . . 10 ⊢ (𝑥 ∈ ((𝑌 − 𝑋)..^(𝑍 − 𝑋)) → 𝑥 ∈ ℂ)
99	98	adantl 482	. . . . . . . . 9 ⊢ (((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) ∧ 𝑥 ∈ ((𝑌 − 𝑋)..^(𝑍 − 𝑋))) → 𝑥 ∈ ℂ)
100	27, 30	subcld 10851	. . . . . . . . . 10 ⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) → (𝑌 − 𝑋) ∈ ℂ)
101	100	adantr 481	. . . . . . . . 9 ⊢ (((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) ∧ 𝑥 ∈ ((𝑌 − 𝑋)..^(𝑍 − 𝑋))) → (𝑌 − 𝑋) ∈ ℂ)
102	27	adantr 481	. . . . . . . . 9 ⊢ (((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) ∧ 𝑥 ∈ ((𝑌 − 𝑋)..^(𝑍 − 𝑋))) → 𝑌 ∈ ℂ)
103	99, 101, 102	subadd23d 10873	. . . . . . . 8 ⊢ (((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) ∧ 𝑥 ∈ ((𝑌 − 𝑋)..^(𝑍 − 𝑋))) → ((𝑥 − (𝑌 − 𝑋)) + 𝑌) = (𝑥 + (𝑌 − (𝑌 − 𝑋))))
104	27, 30	nncand 10856	. . . . . . . . . 10 ⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) → (𝑌 − (𝑌 − 𝑋)) = 𝑋)
105	104	oveq2d 7039	. . . . . . . . 9 ⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) → (𝑥 + (𝑌 − (𝑌 − 𝑋))) = (𝑥 + 𝑋))
106	105	adantr 481	. . . . . . . 8 ⊢ (((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) ∧ 𝑥 ∈ ((𝑌 − 𝑋)..^(𝑍 − 𝑋))) → (𝑥 + (𝑌 − (𝑌 − 𝑋))) = (𝑥 + 𝑋))
107	96, 103, 106	3eqtrd 2837	. . . . . . 7 ⊢ (((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) ∧ 𝑥 ∈ ((𝑌 − 𝑋)..^(𝑍 − 𝑋))) → ((𝑥 − (♯‘(𝑆 substr ⟨𝑋, 𝑌⟩))) + 𝑌) = (𝑥 + 𝑋))
108	107	fveq2d 6549	. . . . . 6 ⊢ (((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) ∧ 𝑥 ∈ ((𝑌 − 𝑋)..^(𝑍 − 𝑋))) → (𝑆‘((𝑥 − (♯‘(𝑆 substr ⟨𝑋, 𝑌⟩))) + 𝑌)) = (𝑆‘(𝑥 + 𝑋)))
109	79, 94, 108	3eqtrd 2837	. . . . 5 ⊢ (((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) ∧ 𝑥 ∈ ((𝑌 − 𝑋)..^(𝑍 − 𝑋))) → (((𝑆 substr ⟨𝑋, 𝑌⟩) ++ (𝑆 substr ⟨𝑌, 𝑍⟩))‘𝑥) = (𝑆‘(𝑥 + 𝑋)))
110	72, 109	jaodan 952	. . . 4 ⊢ (((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) ∧ (𝑥 ∈ (0..^(𝑌 − 𝑋)) ∨ 𝑥 ∈ ((𝑌 − 𝑋)..^(𝑍 − 𝑋)))) → (((𝑆 substr ⟨𝑋, 𝑌⟩) ++ (𝑆 substr ⟨𝑌, 𝑍⟩))‘𝑥) = (𝑆‘(𝑥 + 𝑋)))
111	58, 110	syldan 591	. . 3 ⊢ (((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) ∧ 𝑥 ∈ (0..^(𝑍 − 𝑋))) → (((𝑆 substr ⟨𝑋, 𝑌⟩) ++ (𝑆 substr ⟨𝑌, 𝑍⟩))‘𝑥) = (𝑆‘(𝑥 + 𝑋)))
112		simpll 763	. . . 4 ⊢ (((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) ∧ 𝑥 ∈ (0..^(𝑍 − 𝑋))) → 𝑆 ∈ Word 𝐴)
113	48	adantr 481	. . . 4 ⊢ (((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) ∧ 𝑥 ∈ (0..^(𝑍 − 𝑋))) → 𝑋 ∈ (0...𝑍))
114		simplr3 1210	. . . 4 ⊢ (((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) ∧ 𝑥 ∈ (0..^(𝑍 − 𝑋))) → 𝑍 ∈ (0...(♯‘𝑆)))
115		swrdfv 13850	. . . 4 ⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑋 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆))) ∧ 𝑥 ∈ (0..^(𝑍 − 𝑋))) → ((𝑆 substr ⟨𝑋, 𝑍⟩)‘𝑥) = (𝑆‘(𝑥 + 𝑋)))
116	112, 113, 114, 54, 115	syl31anc 1366	. . 3 ⊢ (((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) ∧ 𝑥 ∈ (0..^(𝑍 − 𝑋))) → ((𝑆 substr ⟨𝑋, 𝑍⟩)‘𝑥) = (𝑆‘(𝑥 + 𝑋)))
117	111, 116	eqtr4d 2836	. 2 ⊢ (((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) ∧ 𝑥 ∈ (0..^(𝑍 − 𝑋))) → (((𝑆 substr ⟨𝑋, 𝑌⟩) ++ (𝑆 substr ⟨𝑌, 𝑍⟩))‘𝑥) = ((𝑆 substr ⟨𝑋, 𝑍⟩)‘𝑥))
118	39, 53, 117	eqfnfvd 6677	1 ⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) → ((𝑆 substr ⟨𝑋, 𝑌⟩) ++ (𝑆 substr ⟨𝑌, 𝑍⟩)) = (𝑆 substr ⟨𝑋, 𝑍⟩))

Syntax hints:   → wi 4   ∧ wa 396   ∨ wo 842   ∧ w3a 1080   = wceq 1525   ∈ wcel 2083  ⟨cop 4484   Fn wfn 6227  ⟶wf 6228  ‘cfv 6232  (class class class)co 7023  ℂcc 10388  0cc0 10390   + caddc 10393   − cmin 10723  ℤcz 11835  ...cfz 12746  ..^cfzo 12887  ♯chash 13544  Word cword 13711   ++ cconcat 13772   substr csubstr 13842

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892  ax-6 1951  ax-7 1996  ax-8 2085  ax-9 2093  ax-10 2114  ax-11 2128  ax-12 2143  ax-13 2346  ax-ext 2771  ax-rep 5088  ax-sep 5101  ax-nul 5108  ax-pow 5164  ax-pr 5228  ax-un 7326  ax-cnex 10446  ax-resscn 10447  ax-1cn 10448  ax-icn 10449  ax-addcl 10450  ax-addrcl 10451  ax-mulcl 10452  ax-mulrcl 10453  ax-mulcom 10454  ax-addass 10455  ax-mulass 10456  ax-distr 10457  ax-i2m1 10458  ax-1ne0 10459  ax-1rid 10460  ax-rnegex 10461  ax-rrecex 10462  ax-cnre 10463  ax-pre-lttri 10464  ax-pre-lttrn 10465  ax-pre-ltadd 10466  ax-pre-mulgt0 10467

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3or 1081  df-3an 1082  df-tru 1528  df-ex 1766  df-nf 1770  df-sb 2045  df-mo 2578  df-eu 2614  df-clab 2778  df-cleq 2790  df-clel 2865  df-nfc 2937  df-ne 2987  df-nel 3093  df-ral 3112  df-rex 3113  df-reu 3114  df-rab 3116  df-v 3442  df-sbc 3712  df-csb 3818  df-dif 3868  df-un 3870  df-in 3872  df-ss 3880  df-pss 3882  df-nul 4218  df-if 4388  df-pw 4461  df-sn 4479  df-pr 4481  df-tp 4483  df-op 4485  df-uni 4752  df-int 4789  df-iun 4833  df-br 4969  df-opab 5031  df-mpt 5048  df-tr 5071  df-id 5355  df-eprel 5360  df-po 5369  df-so 5370  df-fr 5409  df-we 5411  df-xp 5456  df-rel 5457  df-cnv 5458  df-co 5459  df-dm 5460  df-rn 5461  df-res 5462  df-ima 5463  df-pred 6030  df-ord 6076  df-on 6077  df-lim 6078  df-suc 6079  df-iota 6196  df-fun 6234  df-fn 6235  df-f 6236  df-f1 6237  df-fo 6238  df-f1o 6239  df-fv 6240  df-riota 6984  df-ov 7026  df-oprab 7027  df-mpo 7028  df-om 7444  df-1st 7552  df-2nd 7553  df-wrecs 7805  df-recs 7867  df-rdg 7905  df-1o 7960  df-oadd 7964  df-er 8146  df-en 8365  df-dom 8366  df-sdom 8367  df-fin 8368  df-card 9221  df-pnf 10530  df-mnf 10531  df-xr 10532  df-ltxr 10533  df-le 10534  df-sub 10725  df-neg 10726  df-nn 11493  df-n0 11752  df-z 11836  df-uz 12098  df-fz 12747  df-fzo 12888  df-hash 13545  df-word 13712  df-concat 13773  df-substr 13843

This theorem is referenced by:  swrds2  14142  efgredleme  18600