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	13	elfzelzd	$⊢ (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 ℤ$
25	24	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 ℂ$
26	12	elfzelzd	$⊢ (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 ℤ$
27	26	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 ℂ$
28	14	elfzelzd	$⊢ (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 ℤ$
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 Z \in ℂ$
30	25 27 29	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$
31	10 23 30	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$
32	31	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)$
33	32	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))$
34	8 33	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)$
35		swrdcl	$⊢ S \in Word A \to S substr ⟨X, Z⟩ \in Word A$
36	35	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$
37		wrdfn	$⊢ S substr ⟨X, Z⟩ \in Word A \to (S substr ⟨X, Z⟩) Fn (0 ..^\|S substr ⟨X, Z⟩\|)$
38	36 37	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⟩\|)$
39		fzass4	$⊢ (X \in (0 \dots Z) \land Y \in (X \dots Z)) \leftrightarrow (X \in (0 \dots Y) \land Y \in (0 \dots Z))$
40	39	biimpri	$⊢ (X \in (0 \dots Y) \land Y \in (0 \dots Z)) \to (X \in (0 \dots Z) \land Y \in (X \dots Z))$
41	40	simpld	$⊢ (X \in (0 \dots Y) \land Y \in (0 \dots Z)) \to X \in (0 \dots Z)$
42	12 13 41	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)$
43		swrdlen	$⊢ (S \in Word A \land X \in (0 \dots Z) \land Z \in (0 \dots \|S\|)) \to \|S substr ⟨X, Z⟩\| = Z - X$
44	11 42 14 43	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$
45	44	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)$
46	45	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))$
47	38 46	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)$
48	24 26	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 ℤ$
49	48	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 ℤ)$
50		fzospliti	$⊢ (x \in (0 ..^Z - X) \land Y - X \in ℤ) \to (x \in (0 ..^Y - X) \lor x \in (Y - X ..^Z - X))$
51	49 50	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))$
52	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$
53	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$
54	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)$
55	54	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))$
56	55	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⟩\|)$
57		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)$
58	52 53 56 57	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)$
59		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$
60		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)$
61	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\|)$
62		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)$
63		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)$
64	59 60 61 62 63	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)$
65	58 64	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)$
66	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$
67	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$
68	23 30	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$
69	20 68	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)$
70	69	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))$
71	70	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⟩\|)$
72		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⟩\|)$
73	66 67 71 72	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⟩\|)$
74		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$
75		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)$
76		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\|)$
77	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)$
78	77	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)$
79	30	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)$
80	79	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))$
81	80	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)$
82	28 24	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 ℤ$
83	82	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 ℤ$
84		fzosubel3	$⊢ (x \in (Y - X ..^(Y - X) + Z - Y) \land Z - Y \in ℤ) \to x - (Y - X) \in (0 ..^Z - Y)$
85	81 83 84	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)$
86	78 85	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)$
87		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)$
88	74 75 76 86 87	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)$
89	77	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$
90	89	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$
91		elfzoelz	$⊢ x \in (Y - X ..^Z - X) \to x \in ℤ$
92	91	zcnd	$⊢ x \in (Y - X ..^Z - X) \to x \in ℂ$
93	92	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 ℂ$
94	25 27	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 ℂ$
95	94	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 ℂ$
96	25	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 ℂ$
97	93 95 96	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)$
98	25 27	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$
99	98	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$
100	99	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$
101	90 97 100	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$
102	101	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)$
103	73 88 102	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)$
104	65 103	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)$
105	51 104	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)$
106		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$
107	42	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)$
108		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\|)$
109		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)$
110		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)$
111	106 107 108 109 110	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)$
112	105 111	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)$
113	34 47 112	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