ccatswrd

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

		Ref	Expression
	Assertion	ccatswrd	$⊢ (S \in Word A \land (X \in (0 \dots Y) \land Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \to (S substr ⟨X, Y⟩) ++ (S substr ⟨Y, Z⟩) = S substr ⟨X, Z⟩$

Proof

Step	Hyp	Ref	Expression
1		swrdcl	$⊢ S \in Word A \to S substr ⟨X, Y⟩ \in Word A$
2	1	adantr	$⊢ (S \in Word A \land (X \in (0 \dots Y) \land Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \to S substr ⟨X, Y⟩ \in Word A$
3		swrdcl	$⊢ S \in Word A \to S substr ⟨Y, Z⟩ \in Word A$
4	3	adantr	$⊢ (S \in Word A \land (X \in (0 \dots Y) \land Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \to S substr ⟨Y, Z⟩ \in Word A$
5		ccatcl	$⊢ (S substr ⟨X, Y⟩ \in Word A \land S substr ⟨Y, Z⟩ \in Word A) \to (S substr ⟨X, Y⟩) ++ (S substr ⟨Y, Z⟩) \in Word A$
6	2 4 5	syl2anc	$⊢ (S \in Word A \land (X \in (0 \dots Y) \land Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \to (S substr ⟨X, Y⟩) ++ (S substr ⟨Y, Z⟩) \in Word A$
7		wrdfn	$⊢ (S substr ⟨X, Y⟩) ++ (S substr ⟨Y, Z⟩) \in Word A \to ((S substr ⟨X, Y⟩) ++ (S substr ⟨Y, Z⟩)) Fn (0 ..^\|(S substr ⟨X, Y⟩) ++ (S substr ⟨Y, Z⟩)\|)$
8	6 7	syl	$⊢ (S \in Word A \land (X \in (0 \dots Y) \land Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \to ((S substr ⟨X, Y⟩) ++ (S substr ⟨Y, Z⟩)) Fn (0 ..^\|(S substr ⟨X, Y⟩) ++ (S substr ⟨Y, Z⟩)\|)$
9		ccatlen	$⊢ (S substr ⟨X, Y⟩ \in Word A \land S substr ⟨Y, Z⟩ \in Word A) \to \|(S substr ⟨X, Y⟩) ++ (S substr ⟨Y, Z⟩)\| = \|S substr ⟨X, Y⟩\| + \|S substr ⟨Y, Z⟩\|$
10	2 4 9	syl2anc	$⊢ (S \in Word A \land (X \in (0 \dots Y) \land Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \to \|(S substr ⟨X, Y⟩) ++ (S substr ⟨Y, Z⟩)\| = \|S substr ⟨X, Y⟩\| + \|S substr ⟨Y, Z⟩\|$
11		simpl	$⊢ (S \in Word A \land (X \in (0 \dots Y) \land Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \to S \in Word A$
12		simpr1	$⊢ (S \in Word A \land (X \in (0 \dots Y) \land Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \to X \in (0 \dots Y)$
13		simpr2	$⊢ (S \in Word A \land (X \in (0 \dots Y) \land Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \to Y \in (0 \dots Z)$
14		simpr3	$⊢ (S \in Word A \land (X \in (0 \dots Y) \land Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \to Z \in (0 \dots \|S\|)$
15		fzass4	$⊢ (Y \in (0 \dots \|S\|) \land Z \in (Y \dots \|S\|)) \leftrightarrow (Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))$
16	15	biimpri	$⊢ (Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|)) \to (Y \in (0 \dots \|S\|) \land Z \in (Y \dots \|S\|))$
17	16	simpld	$⊢ (Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|)) \to Y \in (0 \dots \|S\|)$
18	13 14 17	syl2anc	$⊢ (S \in Word A \land (X \in (0 \dots Y) \land Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \to Y \in (0 \dots \|S\|)$
19		swrdlen	$⊢ (S \in Word A \land X \in (0 \dots Y) \land Y \in (0 \dots \|S\|)) \to \|S substr ⟨X, Y⟩\| = Y - X$
20	11 12 18 19	syl3anc	$⊢ (S \in Word A \land (X \in (0 \dots Y) \land Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \to \|S substr ⟨X, Y⟩\| = Y - X$
21		swrdlen	$⊢ (S \in Word A \land Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|)) \to \|S substr ⟨Y, Z⟩\| = Z - Y$
22	21	3adant3r1	$⊢ (S \in Word A \land (X \in (0 \dots Y) \land Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \to \|S substr ⟨Y, Z⟩\| = Z - Y$
23	20 22	oveq12d	$⊢ (S \in Word A \land (X \in (0 \dots Y) \land Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \to \|S substr ⟨X, Y⟩\| + \|S substr ⟨Y, Z⟩\| = (Y - X) + Z - Y$
24		elfzelz	$⊢ Y \in (0 \dots Z) \to Y \in ℤ$
25	13 24	syl	$⊢ (S \in Word A \land (X \in (0 \dots Y) \land Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \to Y \in ℤ$
26	25	zcnd	$⊢ (S \in Word A \land (X \in (0 \dots Y) \land Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \to Y \in ℂ$
27		elfzelz	$⊢ X \in (0 \dots Y) \to X \in ℤ$
28	12 27	syl	$⊢ (S \in Word A \land (X \in (0 \dots Y) \land Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \to X \in ℤ$
29	28	zcnd	$⊢ (S \in Word A \land (X \in (0 \dots Y) \land Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \to X \in ℂ$
30		elfzelz	$⊢ Z \in (0 \dots \|S\|) \to Z \in ℤ$
31	14 30	syl	$⊢ (S \in Word A \land (X \in (0 \dots Y) \land Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \to Z \in ℤ$
32	31	zcnd	$⊢ (S \in Word A \land (X \in (0 \dots Y) \land Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \to Z \in ℂ$
33	26 29 32	npncan3d	$⊢ (S \in Word A \land (X \in (0 \dots Y) \land Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \to (Y - X) + Z - Y = Z - X$
34	10 23 33	3eqtrd	$⊢ (S \in Word A \land (X \in (0 \dots Y) \land Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \to \|(S substr ⟨X, Y⟩) ++ (S substr ⟨Y, Z⟩)\| = Z - X$
35	34	oveq2d	$⊢ (S \in Word A \land (X \in (0 \dots Y) \land Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \to (0 ..^\|(S substr ⟨X, Y⟩) ++ (S substr ⟨Y, Z⟩)\|) = (0 ..^Z - X)$
36	35	fneq2d	$⊢ (S \in Word A \land (X \in (0 \dots Y) \land Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \to (((S substr ⟨X, Y⟩) ++ (S substr ⟨Y, Z⟩)) Fn (0 ..^\|(S substr ⟨X, Y⟩) ++ (S substr ⟨Y, Z⟩)\|) \leftrightarrow ((S substr ⟨X, Y⟩) ++ (S substr ⟨Y, Z⟩)) Fn (0 ..^Z - X))$
37	8 36	mpbid	$⊢ (S \in Word A \land (X \in (0 \dots Y) \land Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \to ((S substr ⟨X, Y⟩) ++ (S substr ⟨Y, Z⟩)) Fn (0 ..^Z - X)$
38		swrdcl	$⊢ S \in Word A \to S substr ⟨X, Z⟩ \in Word A$
39	38	adantr	$⊢ (S \in Word A \land (X \in (0 \dots Y) \land Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \to S substr ⟨X, Z⟩ \in Word A$
40		wrdfn	$⊢ S substr ⟨X, Z⟩ \in Word A \to (S substr ⟨X, Z⟩) Fn (0 ..^\|S substr ⟨X, Z⟩\|)$
41	39 40	syl	$⊢ (S \in Word A \land (X \in (0 \dots Y) \land Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \to (S substr ⟨X, Z⟩) Fn (0 ..^\|S substr ⟨X, Z⟩\|)$
42		fzass4	$⊢ (X \in (0 \dots Z) \land Y \in (X \dots Z)) \leftrightarrow (X \in (0 \dots Y) \land Y \in (0 \dots Z))$
43	42	biimpri	$⊢ (X \in (0 \dots Y) \land Y \in (0 \dots Z)) \to (X \in (0 \dots Z) \land Y \in (X \dots Z))$
44	43	simpld	$⊢ (X \in (0 \dots Y) \land Y \in (0 \dots Z)) \to X \in (0 \dots Z)$
45	12 13 44	syl2anc	$⊢ (S \in Word A \land (X \in (0 \dots Y) \land Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \to X \in (0 \dots Z)$
46		swrdlen	$⊢ (S \in Word A \land X \in (0 \dots Z) \land Z \in (0 \dots \|S\|)) \to \|S substr ⟨X, Z⟩\| = Z - X$
47	11 45 14 46	syl3anc	$⊢ (S \in Word A \land (X \in (0 \dots Y) \land Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \to \|S substr ⟨X, Z⟩\| = Z - X$
48	47	oveq2d	$⊢ (S \in Word A \land (X \in (0 \dots Y) \land Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \to (0 ..^\|S substr ⟨X, Z⟩\|) = (0 ..^Z - X)$
49	48	fneq2d	$⊢ (S \in Word A \land (X \in (0 \dots Y) \land Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \to ((S substr ⟨X, Z⟩) Fn (0 ..^\|S substr ⟨X, Z⟩\|) \leftrightarrow (S substr ⟨X, Z⟩) Fn (0 ..^Z - X))$
50	41 49	mpbid	$⊢ (S \in Word A \land (X \in (0 \dots Y) \land Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \to (S substr ⟨X, Z⟩) Fn (0 ..^Z - X)$
51	25 28	zsubcld	$⊢ (S \in Word A \land (X \in (0 \dots Y) \land Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \to Y - X \in ℤ$
52	51	anim1ci	$⊢ ((S \in Word A \land (X \in (0 \dots Y) \land Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \land x \in (0 ..^Z - X)) \to (x \in (0 ..^Z - X) \land Y - X \in ℤ)$
53		fzospliti	$⊢ (x \in (0 ..^Z - X) \land Y - X \in ℤ) \to (x \in (0 ..^Y - X) \lor x \in (Y - X ..^Z - X))$
54	52 53	syl	$⊢ ((S \in Word A \land (X \in (0 \dots Y) \land Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \land x \in (0 ..^Z - X)) \to (x \in (0 ..^Y - X) \lor x \in (Y - X ..^Z - X))$
55	1	ad2antrr	$⊢ ((S \in Word A \land (X \in (0 \dots Y) \land Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \land x \in (0 ..^Y - X)) \to S substr ⟨X, Y⟩ \in Word A$
56	3	ad2antrr	$⊢ ((S \in Word A \land (X \in (0 \dots Y) \land Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \land x \in (0 ..^Y - X)) \to S substr ⟨Y, Z⟩ \in Word A$
57	20	oveq2d	$⊢ (S \in Word A \land (X \in (0 \dots Y) \land Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \to (0 ..^\|S substr ⟨X, Y⟩\|) = (0 ..^Y - X)$
58	57	eleq2d	$⊢ (S \in Word A \land (X \in (0 \dots Y) \land Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \to (x \in (0 ..^\|S substr ⟨X, Y⟩\|) \leftrightarrow x \in (0 ..^Y - X))$
59	58	biimpar	$⊢ ((S \in Word A \land (X \in (0 \dots Y) \land Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \land x \in (0 ..^Y - X)) \to x \in (0 ..^\|S substr ⟨X, Y⟩\|)$
60		ccatval1	$⊢ (S substr ⟨X, Y⟩ \in Word A \land S substr ⟨Y, Z⟩ \in Word A \land x \in (0 ..^\|S substr ⟨X, Y⟩\|)) \to ((S substr ⟨X, Y⟩) ++ (S substr ⟨Y, Z⟩)) (x) = (S substr ⟨X, Y⟩) (x)$
61	55 56 59 60	syl3anc	$⊢ ((S \in Word A \land (X \in (0 \dots Y) \land Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \land x \in (0 ..^Y - X)) \to ((S substr ⟨X, Y⟩) ++ (S substr ⟨Y, Z⟩)) (x) = (S substr ⟨X, Y⟩) (x)$
62		simpll	$⊢ ((S \in Word A \land (X \in (0 \dots Y) \land Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \land x \in (0 ..^Y - X)) \to S \in Word A$
63		simplr1	$⊢ ((S \in Word A \land (X \in (0 \dots Y) \land Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \land x \in (0 ..^Y - X)) \to X \in (0 \dots Y)$
64	18	adantr	$⊢ ((S \in Word A \land (X \in (0 \dots Y) \land Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \land x \in (0 ..^Y - X)) \to Y \in (0 \dots \|S\|)$
65		simpr	$⊢ ((S \in Word A \land (X \in (0 \dots Y) \land Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \land x \in (0 ..^Y - X)) \to x \in (0 ..^Y - X)$
66		swrdfv	$⊢ ((S \in Word A \land X \in (0 \dots Y) \land Y \in (0 \dots \|S\|)) \land x \in (0 ..^Y - X)) \to (S substr ⟨X, Y⟩) (x) = S (x + X)$
67	62 63 64 65 66	syl31anc	$⊢ ((S \in Word A \land (X \in (0 \dots Y) \land Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \land x \in (0 ..^Y - X)) \to (S substr ⟨X, Y⟩) (x) = S (x + X)$
68	61 67	eqtrd	$⊢ ((S \in Word A \land (X \in (0 \dots Y) \land Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \land x \in (0 ..^Y - X)) \to ((S substr ⟨X, Y⟩) ++ (S substr ⟨Y, Z⟩)) (x) = S (x + X)$
69	1	ad2antrr	$⊢ ((S \in Word A \land (X \in (0 \dots Y) \land Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \land x \in (Y - X ..^Z - X)) \to S substr ⟨X, Y⟩ \in Word A$
70	3	ad2antrr	$⊢ ((S \in Word A \land (X \in (0 \dots Y) \land Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \land x \in (Y - X ..^Z - X)) \to S substr ⟨Y, Z⟩ \in Word A$
71	23 33	eqtrd	$⊢ (S \in Word A \land (X \in (0 \dots Y) \land Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \to \|S substr ⟨X, Y⟩\| + \|S substr ⟨Y, Z⟩\| = Z - X$
72	20 71	oveq12d	$⊢ (S \in Word A \land (X \in (0 \dots Y) \land Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \to (\|S substr ⟨X, Y⟩\| ..^\|S substr ⟨X, Y⟩\| + \|S substr ⟨Y, Z⟩\|) = (Y - X ..^Z - X)$
73	72	eleq2d	$⊢ (S \in Word A \land (X \in (0 \dots Y) \land Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \to (x \in (\|S substr ⟨X, Y⟩\| ..^\|S substr ⟨X, Y⟩\| + \|S substr ⟨Y, Z⟩\|) \leftrightarrow x \in (Y - X ..^Z - X))$
74	73	biimpar	$⊢ ((S \in Word A \land (X \in (0 \dots Y) \land Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \land x \in (Y - X ..^Z - X)) \to x \in (\|S substr ⟨X, Y⟩\| ..^\|S substr ⟨X, Y⟩\| + \|S substr ⟨Y, Z⟩\|)$
75		ccatval2	$⊢ (S substr ⟨X, Y⟩ \in Word A \land S substr ⟨Y, Z⟩ \in Word A \land x \in (\|S substr ⟨X, Y⟩\| ..^\|S substr ⟨X, Y⟩\| + \|S substr ⟨Y, Z⟩\|)) \to ((S substr ⟨X, Y⟩) ++ (S substr ⟨Y, Z⟩)) (x) = (S substr ⟨Y, Z⟩) (x - \|S substr ⟨X, Y⟩\|)$
76	69 70 74 75	syl3anc	$⊢ ((S \in Word A \land (X \in (0 \dots Y) \land Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \land x \in (Y - X ..^Z - X)) \to ((S substr ⟨X, Y⟩) ++ (S substr ⟨Y, Z⟩)) (x) = (S substr ⟨Y, Z⟩) (x - \|S substr ⟨X, Y⟩\|)$
77		simpll	$⊢ ((S \in Word A \land (X \in (0 \dots Y) \land Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \land x \in (Y - X ..^Z - X)) \to S \in Word A$
78		simplr2	$⊢ ((S \in Word A \land (X \in (0 \dots Y) \land Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \land x \in (Y - X ..^Z - X)) \to Y \in (0 \dots Z)$
79		simplr3	$⊢ ((S \in Word A \land (X \in (0 \dots Y) \land Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \land x \in (Y - X ..^Z - X)) \to Z \in (0 \dots \|S\|)$
80	20	oveq2d	$⊢ (S \in Word A \land (X \in (0 \dots Y) \land Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \to x - \|S substr ⟨X, Y⟩\| = x - (Y - X)$
81	80	adantr	$⊢ ((S \in Word A \land (X \in (0 \dots Y) \land Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \land x \in (Y - X ..^Z - X)) \to x - \|S substr ⟨X, Y⟩\| = x - (Y - X)$
82	33	oveq2d	$⊢ (S \in Word A \land (X \in (0 \dots Y) \land Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \to (Y - X ..^(Y - X) + Z - Y) = (Y - X ..^Z - X)$
83	82	eleq2d	$⊢ (S \in Word A \land (X \in (0 \dots Y) \land Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \to (x \in (Y - X ..^(Y - X) + Z - Y) \leftrightarrow x \in (Y - X ..^Z - X))$
84	83	biimpar	$⊢ ((S \in Word A \land (X \in (0 \dots Y) \land Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \land x \in (Y - X ..^Z - X)) \to x \in (Y - X ..^(Y - X) + Z - Y)$
85	31 25	zsubcld	$⊢ (S \in Word A \land (X \in (0 \dots Y) \land Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \to Z - Y \in ℤ$
86	85	adantr	$⊢ ((S \in Word A \land (X \in (0 \dots Y) \land Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \land x \in (Y - X ..^Z - X)) \to Z - Y \in ℤ$
87		fzosubel3	$⊢ (x \in (Y - X ..^(Y - X) + Z - Y) \land Z - Y \in ℤ) \to x - (Y - X) \in (0 ..^Z - Y)$
88	84 86 87	syl2anc	$⊢ ((S \in Word A \land (X \in (0 \dots Y) \land Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \land x \in (Y - X ..^Z - X)) \to x - (Y - X) \in (0 ..^Z - Y)$
89	81 88	eqeltrd	$⊢ ((S \in Word A \land (X \in (0 \dots Y) \land Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \land x \in (Y - X ..^Z - X)) \to x - \|S substr ⟨X, Y⟩\| \in (0 ..^Z - Y)$
90		swrdfv	$⊢ ((S \in Word A \land Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|)) \land x - \|S substr ⟨X, Y⟩\| \in (0 ..^Z - Y)) \to (S substr ⟨Y, Z⟩) (x - \|S substr ⟨X, Y⟩\|) = S (x - \|S substr ⟨X, Y⟩\| + Y)$
91	77 78 79 89 90	syl31anc	$⊢ ((S \in Word A \land (X \in (0 \dots Y) \land Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \land x \in (Y - X ..^Z - X)) \to (S substr ⟨Y, Z⟩) (x - \|S substr ⟨X, Y⟩\|) = S (x - \|S substr ⟨X, Y⟩\| + Y)$
92	80	oveq1d	$⊢ (S \in Word A \land (X \in (0 \dots Y) \land Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \to x - \|S substr ⟨X, Y⟩\| + Y = x - (Y - X) + Y$
93	92	adantr	$⊢ ((S \in Word A \land (X \in (0 \dots Y) \land Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \land x \in (Y - X ..^Z - X)) \to x - \|S substr ⟨X, Y⟩\| + Y = x - (Y - X) + Y$
94		elfzoelz	$⊢ x \in (Y - X ..^Z - X) \to x \in ℤ$
95	94	zcnd	$⊢ x \in (Y - X ..^Z - X) \to x \in ℂ$
96	95	adantl	$⊢ ((S \in Word A \land (X \in (0 \dots Y) \land Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \land x \in (Y - X ..^Z - X)) \to x \in ℂ$
97	26 29	subcld	$⊢ (S \in Word A \land (X \in (0 \dots Y) \land Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \to Y - X \in ℂ$
98	97	adantr	$⊢ ((S \in Word A \land (X \in (0 \dots Y) \land Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \land x \in (Y - X ..^Z - X)) \to Y - X \in ℂ$
99	26	adantr	$⊢ ((S \in Word A \land (X \in (0 \dots Y) \land Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \land x \in (Y - X ..^Z - X)) \to Y \in ℂ$
100	96 98 99	subadd23d	$⊢ ((S \in Word A \land (X \in (0 \dots Y) \land Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \land x \in (Y - X ..^Z - X)) \to x - (Y - X) + Y = x + Y - (Y - X)$
101	26 29	nncand	$⊢ (S \in Word A \land (X \in (0 \dots Y) \land Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \to Y - (Y - X) = X$
102	101	oveq2d	$⊢ (S \in Word A \land (X \in (0 \dots Y) \land Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \to x + Y - (Y - X) = x + X$
103	102	adantr	$⊢ ((S \in Word A \land (X \in (0 \dots Y) \land Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \land x \in (Y - X ..^Z - X)) \to x + Y - (Y - X) = x + X$
104	93 100 103	3eqtrd	$⊢ ((S \in Word A \land (X \in (0 \dots Y) \land Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \land x \in (Y - X ..^Z - X)) \to x - \|S substr ⟨X, Y⟩\| + Y = x + X$
105	104	fveq2d	$⊢ ((S \in Word A \land (X \in (0 \dots Y) \land Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \land x \in (Y - X ..^Z - X)) \to S (x - \|S substr ⟨X, Y⟩\| + Y) = S (x + X)$
106	76 91 105	3eqtrd	$⊢ ((S \in Word A \land (X \in (0 \dots Y) \land Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \land x \in (Y - X ..^Z - X)) \to ((S substr ⟨X, Y⟩) ++ (S substr ⟨Y, Z⟩)) (x) = S (x + X)$
107	68 106	jaodan	$⊢ ((S \in Word A \land (X \in (0 \dots Y) \land Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \land (x \in (0 ..^Y - X) \lor x \in (Y - X ..^Z - X))) \to ((S substr ⟨X, Y⟩) ++ (S substr ⟨Y, Z⟩)) (x) = S (x + X)$
108	54 107	syldan	$⊢ ((S \in Word A \land (X \in (0 \dots Y) \land Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \land x \in (0 ..^Z - X)) \to ((S substr ⟨X, Y⟩) ++ (S substr ⟨Y, Z⟩)) (x) = S (x + X)$
109		simpll	$⊢ ((S \in Word A \land (X \in (0 \dots Y) \land Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \land x \in (0 ..^Z - X)) \to S \in Word A$
110	45	adantr	$⊢ ((S \in Word A \land (X \in (0 \dots Y) \land Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \land x \in (0 ..^Z - X)) \to X \in (0 \dots Z)$
111		simplr3	$⊢ ((S \in Word A \land (X \in (0 \dots Y) \land Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \land x \in (0 ..^Z - X)) \to Z \in (0 \dots \|S\|)$
112		simpr	$⊢ ((S \in Word A \land (X \in (0 \dots Y) \land Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \land x \in (0 ..^Z - X)) \to x \in (0 ..^Z - X)$
113		swrdfv	$⊢ ((S \in Word A \land X \in (0 \dots Z) \land Z \in (0 \dots \|S\|)) \land x \in (0 ..^Z - X)) \to (S substr ⟨X, Z⟩) (x) = S (x + X)$
114	109 110 111 112 113	syl31anc	$⊢ ((S \in Word A \land (X \in (0 \dots Y) \land Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \land x \in (0 ..^Z - X)) \to (S substr ⟨X, Z⟩) (x) = S (x + X)$
115	108 114	eqtr4d	$⊢ ((S \in Word A \land (X \in (0 \dots Y) \land Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \land x \in (0 ..^Z - X)) \to ((S substr ⟨X, Y⟩) ++ (S substr ⟨Y, Z⟩)) (x) = (S substr ⟨X, Z⟩) (x)$
116	37 50 115	eqfnfvd	$⊢ (S \in Word A \land (X \in (0 \dots Y) \land Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \to (S substr ⟨X, Y⟩) ++ (S substr ⟨Y, Z⟩) = S substr ⟨X, Z⟩$

Metamath Proof Explorer

Theorem ccatswrd

Proof