ccatpfx

Description: Concatenating a prefix with an adjacent subword makes a longer prefix. (Contributed by AV, 7-May-2020)

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

Proof

Step	Hyp	Ref	Expression
1		pfxcl	$⊢ S \in Word A \to S prefix Y \in Word A$
2		swrdcl	$⊢ S \in Word A \to S substr ⟨Y, Z⟩ \in Word A$
3		ccatcl	$⊢ (S prefix Y \in Word A \land S substr ⟨Y, Z⟩ \in Word A) \to (S prefix Y) ++ (S substr ⟨Y, Z⟩) \in Word A$
4	1 2 3	syl2anc	$⊢ S \in Word A \to (S prefix Y) ++ (S substr ⟨Y, Z⟩) \in Word A$
5		wrdfn	$⊢ (S prefix Y) ++ (S substr ⟨Y, Z⟩) \in Word A \to ((S prefix Y) ++ (S substr ⟨Y, Z⟩)) Fn (0 ..^\|(S prefix Y) ++ (S substr ⟨Y, Z⟩)\|)$
6	4 5	syl	$⊢ S \in Word A \to ((S prefix Y) ++ (S substr ⟨Y, Z⟩)) Fn (0 ..^\|(S prefix Y) ++ (S substr ⟨Y, Z⟩)\|)$
7	6	adantr	$⊢ (S \in Word A \land (Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \to ((S prefix Y) ++ (S substr ⟨Y, Z⟩)) Fn (0 ..^\|(S prefix Y) ++ (S substr ⟨Y, Z⟩)\|)$
8		ccatlen	$⊢ (S prefix Y \in Word A \land S substr ⟨Y, Z⟩ \in Word A) \to \|(S prefix Y) ++ (S substr ⟨Y, Z⟩)\| = \|S prefix Y\| + \|S substr ⟨Y, Z⟩\|$
9	1 2 8	syl2anc	$⊢ S \in Word A \to \|(S prefix Y) ++ (S substr ⟨Y, Z⟩)\| = \|S prefix Y\| + \|S substr ⟨Y, Z⟩\|$
10	9	adantr	$⊢ (S \in Word A \land (Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \to \|(S prefix Y) ++ (S substr ⟨Y, Z⟩)\| = \|S prefix Y\| + \|S substr ⟨Y, Z⟩\|$
11		fzass4	$⊢ (Y \in (0 \dots \|S\|) \land Z \in (Y \dots \|S\|)) \leftrightarrow (Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))$
12	11	biimpri	$⊢ (Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|)) \to (Y \in (0 \dots \|S\|) \land Z \in (Y \dots \|S\|))$
13	12	simpld	$⊢ (Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|)) \to Y \in (0 \dots \|S\|)$
14		pfxlen	$⊢ (S \in Word A \land Y \in (0 \dots \|S\|)) \to \|S prefix Y\| = Y$
15	13 14	sylan2	$⊢ (S \in Word A \land (Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \to \|S prefix Y\| = Y$
16		swrdlen	$⊢ (S \in Word A \land Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|)) \to \|S substr ⟨Y, Z⟩\| = Z - Y$
17	16	3expb	$⊢ (S \in Word A \land (Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \to \|S substr ⟨Y, Z⟩\| = Z - Y$
18	15 17	oveq12d	$⊢ (S \in Word A \land (Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \to \|S prefix Y\| + \|S substr ⟨Y, Z⟩\| = Y + Z - Y$
19		elfzelz	$⊢ Y \in (0 \dots Z) \to Y \in ℤ$
20	19	zcnd	$⊢ Y \in (0 \dots Z) \to Y \in ℂ$
21		elfzelz	$⊢ Z \in (0 \dots \|S\|) \to Z \in ℤ$
22	21	zcnd	$⊢ Z \in (0 \dots \|S\|) \to Z \in ℂ$
23		pncan3	$⊢ (Y \in ℂ \land Z \in ℂ) \to Y + Z - Y = Z$
24	20 22 23	syl2an	$⊢ (Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|)) \to Y + Z - Y = Z$
25	24	adantl	$⊢ (S \in Word A \land (Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \to Y + Z - Y = Z$
26	10 18 25	3eqtrd	$⊢ (S \in Word A \land (Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \to \|(S prefix Y) ++ (S substr ⟨Y, Z⟩)\| = Z$
27	26	oveq2d	$⊢ (S \in Word A \land (Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \to (0 ..^\|(S prefix Y) ++ (S substr ⟨Y, Z⟩)\|) = (0 ..^Z)$
28	27	fneq2d	$⊢ (S \in Word A \land (Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \to (((S prefix Y) ++ (S substr ⟨Y, Z⟩)) Fn (0 ..^\|(S prefix Y) ++ (S substr ⟨Y, Z⟩)\|) \leftrightarrow ((S prefix Y) ++ (S substr ⟨Y, Z⟩)) Fn (0 ..^Z))$
29	7 28	mpbid	$⊢ (S \in Word A \land (Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \to ((S prefix Y) ++ (S substr ⟨Y, Z⟩)) Fn (0 ..^Z)$
30		pfxfn	$⊢ (S \in Word A \land Z \in (0 \dots \|S\|)) \to (S prefix Z) Fn (0 ..^Z)$
31	30	adantrl	$⊢ (S \in Word A \land (Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \to (S prefix Z) Fn (0 ..^Z)$
32		id	$⊢ x \in (0 ..^Z) \to x \in (0 ..^Z)$
33	19	ad2antrl	$⊢ (S \in Word A \land (Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \to Y \in ℤ$
34		fzospliti	$⊢ (x \in (0 ..^Z) \land Y \in ℤ) \to (x \in (0 ..^Y) \lor x \in (Y ..^Z))$
35	32 33 34	syl2anr	$⊢ ((S \in Word A \land (Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \land x \in (0 ..^Z)) \to (x \in (0 ..^Y) \lor x \in (Y ..^Z))$
36	1	ad2antrr	$⊢ ((S \in Word A \land (Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \land x \in (0 ..^Y)) \to S prefix Y \in Word A$
37	2	ad2antrr	$⊢ ((S \in Word A \land (Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \land x \in (0 ..^Y)) \to S substr ⟨Y, Z⟩ \in Word A$
38	15	oveq2d	$⊢ (S \in Word A \land (Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \to (0 ..^\|S prefix Y\|) = (0 ..^Y)$
39	38	eleq2d	$⊢ (S \in Word A \land (Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \to (x \in (0 ..^\|S prefix Y\|) \leftrightarrow x \in (0 ..^Y))$
40	39	biimpar	$⊢ ((S \in Word A \land (Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \land x \in (0 ..^Y)) \to x \in (0 ..^\|S prefix Y\|)$
41		ccatval1	$⊢ (S prefix Y \in Word A \land S substr ⟨Y, Z⟩ \in Word A \land x \in (0 ..^\|S prefix Y\|)) \to ((S prefix Y) ++ (S substr ⟨Y, Z⟩)) (x) = (S prefix Y) (x)$
42	36 37 40 41	syl3anc	$⊢ ((S \in Word A \land (Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \land x \in (0 ..^Y)) \to ((S prefix Y) ++ (S substr ⟨Y, Z⟩)) (x) = (S prefix Y) (x)$
43		simpl	$⊢ (S \in Word A \land (Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \to S \in Word A$
44	13	adantl	$⊢ (S \in Word A \land (Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \to Y \in (0 \dots \|S\|)$
45		id	$⊢ x \in (0 ..^Y) \to x \in (0 ..^Y)$
46		pfxfv	$⊢ (S \in Word A \land Y \in (0 \dots \|S\|) \land x \in (0 ..^Y)) \to (S prefix Y) (x) = S (x)$
47	43 44 45 46	syl2an3an	$⊢ ((S \in Word A \land (Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \land x \in (0 ..^Y)) \to (S prefix Y) (x) = S (x)$
48	42 47	eqtrd	$⊢ ((S \in Word A \land (Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \land x \in (0 ..^Y)) \to ((S prefix Y) ++ (S substr ⟨Y, Z⟩)) (x) = S (x)$
49	1	ad2antrr	$⊢ ((S \in Word A \land (Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \land x \in (Y ..^Z)) \to S prefix Y \in Word A$
50	2	ad2antrr	$⊢ ((S \in Word A \land (Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \land x \in (Y ..^Z)) \to S substr ⟨Y, Z⟩ \in Word A$
51	18 25	eqtrd	$⊢ (S \in Word A \land (Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \to \|S prefix Y\| + \|S substr ⟨Y, Z⟩\| = Z$
52	15 51	oveq12d	$⊢ (S \in Word A \land (Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \to (\|S prefix Y\| ..^\|S prefix Y\| + \|S substr ⟨Y, Z⟩\|) = (Y ..^Z)$
53	52	eleq2d	$⊢ (S \in Word A \land (Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \to (x \in (\|S prefix Y\| ..^\|S prefix Y\| + \|S substr ⟨Y, Z⟩\|) \leftrightarrow x \in (Y ..^Z))$
54	53	biimpar	$⊢ ((S \in Word A \land (Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \land x \in (Y ..^Z)) \to x \in (\|S prefix Y\| ..^\|S prefix Y\| + \|S substr ⟨Y, Z⟩\|)$
55		ccatval2	$⊢ (S prefix Y \in Word A \land S substr ⟨Y, Z⟩ \in Word A \land x \in (\|S prefix Y\| ..^\|S prefix Y\| + \|S substr ⟨Y, Z⟩\|)) \to ((S prefix Y) ++ (S substr ⟨Y, Z⟩)) (x) = (S substr ⟨Y, Z⟩) (x - \|S prefix Y\|)$
56	49 50 54 55	syl3anc	$⊢ ((S \in Word A \land (Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \land x \in (Y ..^Z)) \to ((S prefix Y) ++ (S substr ⟨Y, Z⟩)) (x) = (S substr ⟨Y, Z⟩) (x - \|S prefix Y\|)$
57		id	$⊢ (S \in Word A \land Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|)) \to (S \in Word A \land Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))$
58	57	3expb	$⊢ (S \in Word A \land (Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \to (S \in Word A \land Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))$
59	15	oveq2d	$⊢ (S \in Word A \land (Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \to x - \|S prefix Y\| = x - Y$
60	59	adantr	$⊢ ((S \in Word A \land (Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \land x \in (Y ..^Z)) \to x - \|S prefix Y\| = x - Y$
61		id	$⊢ x \in (Y ..^Z) \to x \in (Y ..^Z)$
62		fzosubel	$⊢ (x \in (Y ..^Z) \land Y \in ℤ) \to x - Y \in (Y - Y ..^Z - Y)$
63	61 33 62	syl2anr	$⊢ ((S \in Word A \land (Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \land x \in (Y ..^Z)) \to x - Y \in (Y - Y ..^Z - Y)$
64	20	subidd	$⊢ Y \in (0 \dots Z) \to Y - Y = 0$
65	64	oveq1d	$⊢ Y \in (0 \dots Z) \to (Y - Y ..^Z - Y) = (0 ..^Z - Y)$
66	65	eleq2d	$⊢ Y \in (0 \dots Z) \to (x - Y \in (Y - Y ..^Z - Y) \leftrightarrow x - Y \in (0 ..^Z - Y))$
67	66	ad2antrl	$⊢ (S \in Word A \land (Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \to (x - Y \in (Y - Y ..^Z - Y) \leftrightarrow x - Y \in (0 ..^Z - Y))$
68	67	adantr	$⊢ ((S \in Word A \land (Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \land x \in (Y ..^Z)) \to (x - Y \in (Y - Y ..^Z - Y) \leftrightarrow x - Y \in (0 ..^Z - Y))$
69	63 68	mpbid	$⊢ ((S \in Word A \land (Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \land x \in (Y ..^Z)) \to x - Y \in (0 ..^Z - Y)$
70	60 69	eqeltrd	$⊢ ((S \in Word A \land (Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \land x \in (Y ..^Z)) \to x - \|S prefix Y\| \in (0 ..^Z - Y)$
71		swrdfv	$⊢ ((S \in Word A \land Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|)) \land x - \|S prefix Y\| \in (0 ..^Z - Y)) \to (S substr ⟨Y, Z⟩) (x - \|S prefix Y\|) = S (x - \|S prefix Y\| + Y)$
72	58 70 71	syl2an2r	$⊢ ((S \in Word A \land (Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \land x \in (Y ..^Z)) \to (S substr ⟨Y, Z⟩) (x - \|S prefix Y\|) = S (x - \|S prefix Y\| + Y)$
73	59	oveq1d	$⊢ (S \in Word A \land (Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \to x - \|S prefix Y\| + Y = x - Y + Y$
74	73	adantr	$⊢ ((S \in Word A \land (Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \land x \in (Y ..^Z)) \to x - \|S prefix Y\| + Y = x - Y + Y$
75		elfzoelz	$⊢ x \in (Y ..^Z) \to x \in ℤ$
76	75	zcnd	$⊢ x \in (Y ..^Z) \to x \in ℂ$
77	20	ad2antrl	$⊢ (S \in Word A \land (Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \to Y \in ℂ$
78		npcan	$⊢ (x \in ℂ \land Y \in ℂ) \to x - Y + Y = x$
79	76 77 78	syl2anr	$⊢ ((S \in Word A \land (Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \land x \in (Y ..^Z)) \to x - Y + Y = x$
80	74 79	eqtrd	$⊢ ((S \in Word A \land (Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \land x \in (Y ..^Z)) \to x - \|S prefix Y\| + Y = x$
81	80	fveq2d	$⊢ ((S \in Word A \land (Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \land x \in (Y ..^Z)) \to S (x - \|S prefix Y\| + Y) = S (x)$
82	56 72 81	3eqtrd	$⊢ ((S \in Word A \land (Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \land x \in (Y ..^Z)) \to ((S prefix Y) ++ (S substr ⟨Y, Z⟩)) (x) = S (x)$
83	48 82	jaodan	$⊢ ((S \in Word A \land (Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \land (x \in (0 ..^Y) \lor x \in (Y ..^Z))) \to ((S prefix Y) ++ (S substr ⟨Y, Z⟩)) (x) = S (x)$
84	35 83	syldan	$⊢ ((S \in Word A \land (Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \land x \in (0 ..^Z)) \to ((S prefix Y) ++ (S substr ⟨Y, Z⟩)) (x) = S (x)$
85		pfxfv	$⊢ (S \in Word A \land Z \in (0 \dots \|S\|) \land x \in (0 ..^Z)) \to (S prefix Z) (x) = S (x)$
86	85	3expa	$⊢ ((S \in Word A \land Z \in (0 \dots \|S\|)) \land x \in (0 ..^Z)) \to (S prefix Z) (x) = S (x)$
87	86	adantlrl	$⊢ ((S \in Word A \land (Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \land x \in (0 ..^Z)) \to (S prefix Z) (x) = S (x)$
88	84 87	eqtr4d	$⊢ ((S \in Word A \land (Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \land x \in (0 ..^Z)) \to ((S prefix Y) ++ (S substr ⟨Y, Z⟩)) (x) = (S prefix Z) (x)$
89	29 31 88	eqfnfvd	$⊢ (S \in Word A \land (Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|))) \to (S prefix Y) ++ (S substr ⟨Y, Z⟩) = S prefix Z$
90	89	3impb	$⊢ (S \in Word A \land Y \in (0 \dots Z) \land Z \in (0 \dots \|S\|)) \to (S prefix Y) ++ (S substr ⟨Y, Z⟩) = S prefix Z$

Metamath Proof Explorer

Theorem ccatpfx

Proof