splval2

Description: Value of a splice, assuming the input word S has already been decomposed into its pieces. (Contributed by Mario Carneiro, 1-Oct-2015) (Proof shortened by AV, 15-Oct-2022)

	Ref	Expression
Hypotheses	splval2.a	$⊢ φ \to A \in Word X$
	splval2.b	$⊢ φ \to B \in Word X$
	splval2.c	$⊢ φ \to C \in Word X$
	splval2.r	$⊢ φ \to R \in Word X$
	splval2.s	$⊢ φ \to S = (A ++ B) ++ C$
	splval2.f	$⊢ φ \to F = \|A\|$
	splval2.t	$⊢ φ \to T = F + \|B\|$
Assertion	splval2	$⊢ φ \to S splice ⟨F, T, R⟩ = (A ++ R) ++ C$

Proof

Step	Hyp	Ref	Expression
1		splval2.a	$⊢ φ \to A \in Word X$
2		splval2.b	$⊢ φ \to B \in Word X$
3		splval2.c	$⊢ φ \to C \in Word X$
4		splval2.r	$⊢ φ \to R \in Word X$
5		splval2.s	$⊢ φ \to S = (A ++ B) ++ C$
6		splval2.f	$⊢ φ \to F = \|A\|$
7		splval2.t	$⊢ φ \to T = F + \|B\|$
8		ccatcl	$⊢ (A \in Word X \land B \in Word X) \to A ++ B \in Word X$
9	1 2 8	syl2anc	$⊢ φ \to A ++ B \in Word X$
10		ccatcl	$⊢ (A ++ B \in Word X \land C \in Word X) \to (A ++ B) ++ C \in Word X$
11	9 3 10	syl2anc	$⊢ φ \to (A ++ B) ++ C \in Word X$
12	5 11	eqeltrd	$⊢ φ \to S \in Word X$
13		lencl	$⊢ A \in Word X \to \|A\| \in ℕ_{0}$
14	1 13	syl	$⊢ φ \to \|A\| \in ℕ_{0}$
15	6 14	eqeltrd	$⊢ φ \to F \in ℕ_{0}$
16		lencl	$⊢ B \in Word X \to \|B\| \in ℕ_{0}$
17	2 16	syl	$⊢ φ \to \|B\| \in ℕ_{0}$
18	15 17	nn0addcld	$⊢ φ \to F + \|B\| \in ℕ_{0}$
19	7 18	eqeltrd	$⊢ φ \to T \in ℕ_{0}$
20		splval	$⊢ (S \in Word X \land (F \in ℕ_{0} \land T \in ℕ_{0} \land R \in Word X)) \to S splice ⟨F, T, R⟩ = ((S prefix F) ++ R) ++ (S substr ⟨T, \|S\|⟩)$
21	12 15 19 4 20	syl13anc	$⊢ φ \to S splice ⟨F, T, R⟩ = ((S prefix F) ++ R) ++ (S substr ⟨T, \|S\|⟩)$
22		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
23	15 22	eleqtrdi	$⊢ φ \to F \in ℤ_{\geq 0}$
24	15	nn0zd	$⊢ φ \to F \in ℤ$
25	24	uzidd	$⊢ φ \to F \in ℤ_{\geq F}$
26		uzaddcl	$⊢ (F \in ℤ_{\geq F} \land \|B\| \in ℕ_{0}) \to F + \|B\| \in ℤ_{\geq F}$
27	25 17 26	syl2anc	$⊢ φ \to F + \|B\| \in ℤ_{\geq F}$
28	7 27	eqeltrd	$⊢ φ \to T \in ℤ_{\geq F}$
29		elfzuzb	$⊢ F \in (0 \dots T) \leftrightarrow (F \in ℤ_{\geq 0} \land T \in ℤ_{\geq F})$
30	23 28 29	sylanbrc	$⊢ φ \to F \in (0 \dots T)$
31	19 22	eleqtrdi	$⊢ φ \to T \in ℤ_{\geq 0}$
32		ccatlen	$⊢ (A ++ B \in Word X \land C \in Word X) \to \|(A ++ B) ++ C\| = \|A ++ B\| + \|C\|$
33	9 3 32	syl2anc	$⊢ φ \to \|(A ++ B) ++ C\| = \|A ++ B\| + \|C\|$
34	5	fveq2d	$⊢ φ \to \|S\| = \|(A ++ B) ++ C\|$
35	6	oveq1d	$⊢ φ \to F + \|B\| = \|A\| + \|B\|$
36		ccatlen	$⊢ (A \in Word X \land B \in Word X) \to \|A ++ B\| = \|A\| + \|B\|$
37	1 2 36	syl2anc	$⊢ φ \to \|A ++ B\| = \|A\| + \|B\|$
38	35 7 37	3eqtr4d	$⊢ φ \to T = \|A ++ B\|$
39	38	oveq1d	$⊢ φ \to T + \|C\| = \|A ++ B\| + \|C\|$
40	33 34 39	3eqtr4d	$⊢ φ \to \|S\| = T + \|C\|$
41	19	nn0zd	$⊢ φ \to T \in ℤ$
42	41	uzidd	$⊢ φ \to T \in ℤ_{\geq T}$
43		lencl	$⊢ C \in Word X \to \|C\| \in ℕ_{0}$
44	3 43	syl	$⊢ φ \to \|C\| \in ℕ_{0}$
45		uzaddcl	$⊢ (T \in ℤ_{\geq T} \land \|C\| \in ℕ_{0}) \to T + \|C\| \in ℤ_{\geq T}$
46	42 44 45	syl2anc	$⊢ φ \to T + \|C\| \in ℤ_{\geq T}$
47	40 46	eqeltrd	$⊢ φ \to \|S\| \in ℤ_{\geq T}$
48		elfzuzb	$⊢ T \in (0 \dots \|S\|) \leftrightarrow (T \in ℤ_{\geq 0} \land \|S\| \in ℤ_{\geq T})$
49	31 47 48	sylanbrc	$⊢ φ \to T \in (0 \dots \|S\|)$
50		ccatpfx	$⊢ (S \in Word X \land F \in (0 \dots T) \land T \in (0 \dots \|S\|)) \to (S prefix F) ++ (S substr ⟨F, T⟩) = S prefix T$
51	12 30 49 50	syl3anc	$⊢ φ \to (S prefix F) ++ (S substr ⟨F, T⟩) = S prefix T$
52		lencl	$⊢ S \in Word X \to \|S\| \in ℕ_{0}$
53	12 52	syl	$⊢ φ \to \|S\| \in ℕ_{0}$
54	53 22	eleqtrdi	$⊢ φ \to \|S\| \in ℤ_{\geq 0}$
55		eluzfz2	$⊢ \|S\| \in ℤ_{\geq 0} \to \|S\| \in (0 \dots \|S\|)$
56	54 55	syl	$⊢ φ \to \|S\| \in (0 \dots \|S\|)$
57		ccatpfx	$⊢ (S \in Word X \land T \in (0 \dots \|S\|) \land \|S\| \in (0 \dots \|S\|)) \to (S prefix T) ++ (S substr ⟨T, \|S\|⟩) = S prefix \|S\|$
58	12 49 56 57	syl3anc	$⊢ φ \to (S prefix T) ++ (S substr ⟨T, \|S\|⟩) = S prefix \|S\|$
59		pfxid	$⊢ S \in Word X \to S prefix \|S\| = S$
60	12 59	syl	$⊢ φ \to S prefix \|S\| = S$
61	58 60 5	3eqtrd	$⊢ φ \to (S prefix T) ++ (S substr ⟨T, \|S\|⟩) = (A ++ B) ++ C$
62		pfxcl	$⊢ S \in Word X \to S prefix T \in Word X$
63	12 62	syl	$⊢ φ \to S prefix T \in Word X$
64		swrdcl	$⊢ S \in Word X \to S substr ⟨T, \|S\|⟩ \in Word X$
65	12 64	syl	$⊢ φ \to S substr ⟨T, \|S\|⟩ \in Word X$
66		pfxlen	$⊢ (S \in Word X \land T \in (0 \dots \|S\|)) \to \|S prefix T\| = T$
67	12 49 66	syl2anc	$⊢ φ \to \|S prefix T\| = T$
68	67 38	eqtrd	$⊢ φ \to \|S prefix T\| = \|A ++ B\|$
69		ccatopth	$⊢ ((S prefix T \in Word X \land S substr ⟨T, \|S\|⟩ \in Word X) \land (A ++ B \in Word X \land C \in Word X) \land \|S prefix T\| = \|A ++ B\|) \to ((S prefix T) ++ (S substr ⟨T, \|S\|⟩) = (A ++ B) ++ C \leftrightarrow (S prefix T = A ++ B \land S substr ⟨T, \|S\|⟩ = C))$
70	63 65 9 3 68 69	syl221anc	$⊢ φ \to ((S prefix T) ++ (S substr ⟨T, \|S\|⟩) = (A ++ B) ++ C \leftrightarrow (S prefix T = A ++ B \land S substr ⟨T, \|S\|⟩ = C))$
71	61 70	mpbid	$⊢ φ \to (S prefix T = A ++ B \land S substr ⟨T, \|S\|⟩ = C)$
72	71	simpld	$⊢ φ \to S prefix T = A ++ B$
73	51 72	eqtrd	$⊢ φ \to (S prefix F) ++ (S substr ⟨F, T⟩) = A ++ B$
74		pfxcl	$⊢ S \in Word X \to S prefix F \in Word X$
75	12 74	syl	$⊢ φ \to S prefix F \in Word X$
76		swrdcl	$⊢ S \in Word X \to S substr ⟨F, T⟩ \in Word X$
77	12 76	syl	$⊢ φ \to S substr ⟨F, T⟩ \in Word X$
78		uztrn	$⊢ (\|S\| \in ℤ_{\geq T} \land T \in ℤ_{\geq F}) \to \|S\| \in ℤ_{\geq F}$
79	47 28 78	syl2anc	$⊢ φ \to \|S\| \in ℤ_{\geq F}$
80		elfzuzb	$⊢ F \in (0 \dots \|S\|) \leftrightarrow (F \in ℤ_{\geq 0} \land \|S\| \in ℤ_{\geq F})$
81	23 79 80	sylanbrc	$⊢ φ \to F \in (0 \dots \|S\|)$
82		pfxlen	$⊢ (S \in Word X \land F \in (0 \dots \|S\|)) \to \|S prefix F\| = F$
83	12 81 82	syl2anc	$⊢ φ \to \|S prefix F\| = F$
84	83 6	eqtrd	$⊢ φ \to \|S prefix F\| = \|A\|$
85		ccatopth	$⊢ ((S prefix F \in Word X \land S substr ⟨F, T⟩ \in Word X) \land (A \in Word X \land B \in Word X) \land \|S prefix F\| = \|A\|) \to ((S prefix F) ++ (S substr ⟨F, T⟩) = A ++ B \leftrightarrow (S prefix F = A \land S substr ⟨F, T⟩ = B))$
86	75 77 1 2 84 85	syl221anc	$⊢ φ \to ((S prefix F) ++ (S substr ⟨F, T⟩) = A ++ B \leftrightarrow (S prefix F = A \land S substr ⟨F, T⟩ = B))$
87	73 86	mpbid	$⊢ φ \to (S prefix F = A \land S substr ⟨F, T⟩ = B)$
88	87	simpld	$⊢ φ \to S prefix F = A$
89	88	oveq1d	$⊢ φ \to (S prefix F) ++ R = A ++ R$
90	71	simprd	$⊢ φ \to S substr ⟨T, \|S\|⟩ = C$
91	89 90	oveq12d	$⊢ φ \to ((S prefix F) ++ R) ++ (S substr ⟨T, \|S\|⟩) = (A ++ R) ++ C$
92	21 91	eqtrd	$⊢ φ \to S splice ⟨F, T, R⟩ = (A ++ R) ++ C$

Metamath Proof Explorer

Theorem splval2

Proof