pfxccat1

Description: Recover the left half of a concatenated word. (Contributed by Mario Carneiro, 27-Sep-2015) (Revised by AV, 6-May-2020)

		Ref	Expression
	Assertion	pfxccat1	$⊢ (S \in Word B \land T \in Word B) \to (S ++ T) prefix \|S\| = S$

Proof

Step	Hyp	Ref	Expression
1		ccatcl	$⊢ (S \in Word B \land T \in Word B) \to S ++ T \in Word B$
2		lencl	$⊢ S \in Word B \to \|S\| \in ℕ_{0}$
3		lencl	$⊢ T \in Word B \to \|T\| \in ℕ_{0}$
4	2 3	anim12i	$⊢ (S \in Word B \land T \in Word B) \to (\|S\| \in ℕ_{0} \land \|T\| \in ℕ_{0})$
5		nn0fz0	$⊢ \|S\| \in ℕ_{0} \leftrightarrow \|S\| \in (0 \dots \|S\|)$
6	2 5	sylib	$⊢ S \in Word B \to \|S\| \in (0 \dots \|S\|)$
7	6	adantr	$⊢ (S \in Word B \land T \in Word B) \to \|S\| \in (0 \dots \|S\|)$
8		elfz0add	$⊢ (\|S\| \in ℕ_{0} \land \|T\| \in ℕ_{0}) \to (\|S\| \in (0 \dots \|S\|) \to \|S\| \in (0 \dots \|S\| + \|T\|))$
9	4 7 8	sylc	$⊢ (S \in Word B \land T \in Word B) \to \|S\| \in (0 \dots \|S\| + \|T\|)$
10		ccatlen	$⊢ (S \in Word B \land T \in Word B) \to \|S ++ T\| = \|S\| + \|T\|$
11	10	oveq2d	$⊢ (S \in Word B \land T \in Word B) \to (0 \dots \|S ++ T\|) = (0 \dots \|S\| + \|T\|)$
12	9 11	eleqtrrd	$⊢ (S \in Word B \land T \in Word B) \to \|S\| \in (0 \dots \|S ++ T\|)$
13		pfxres	$⊢ (S ++ T \in Word B \land \|S\| \in (0 \dots \|S ++ T\|)) \to (S ++ T) prefix \|S\| = {(S ++ T) ↾}_{(0 ..^\|S\|)}$
14	1 12 13	syl2anc	$⊢ (S \in Word B \land T \in Word B) \to (S ++ T) prefix \|S\| = {(S ++ T) ↾}_{(0 ..^\|S\|)}$
15		ccatvalfn	$⊢ (S \in Word B \land T \in Word B) \to (S ++ T) Fn (0 ..^\|S\| + \|T\|)$
16	2	nn0zd	$⊢ S \in Word B \to \|S\| \in ℤ$
17	16	uzidd	$⊢ S \in Word B \to \|S\| \in ℤ_{\geq \|S\|}$
18		uzaddcl	$⊢ (\|S\| \in ℤ_{\geq \|S\|} \land \|T\| \in ℕ_{0}) \to \|S\| + \|T\| \in ℤ_{\geq \|S\|}$
19	17 3 18	syl2an	$⊢ (S \in Word B \land T \in Word B) \to \|S\| + \|T\| \in ℤ_{\geq \|S\|}$
20		fzoss2	$⊢ \|S\| + \|T\| \in ℤ_{\geq \|S\|} \to (0 ..^\|S\|) \subseteq (0 ..^\|S\| + \|T\|)$
21	19 20	syl	$⊢ (S \in Word B \land T \in Word B) \to (0 ..^\|S\|) \subseteq (0 ..^\|S\| + \|T\|)$
22	15 21	fnssresd	$⊢ (S \in Word B \land T \in Word B) \to ({(S ++ T) ↾}_{(0 ..^\|S\|)}) Fn (0 ..^\|S\|)$
23		wrdfn	$⊢ S \in Word B \to S Fn (0 ..^\|S\|)$
24	23	adantr	$⊢ (S \in Word B \land T \in Word B) \to S Fn (0 ..^\|S\|)$
25		fvres	$⊢ k \in (0 ..^\|S\|) \to ({(S ++ T) ↾}_{(0 ..^\|S\|)}) (k) = (S ++ T) (k)$
26	25	adantl	$⊢ ((S \in Word B \land T \in Word B) \land k \in (0 ..^\|S\|)) \to ({(S ++ T) ↾}_{(0 ..^\|S\|)}) (k) = (S ++ T) (k)$
27		ccatval1	$⊢ (S \in Word B \land T \in Word B \land k \in (0 ..^\|S\|)) \to (S ++ T) (k) = S (k)$
28	27	3expa	$⊢ ((S \in Word B \land T \in Word B) \land k \in (0 ..^\|S\|)) \to (S ++ T) (k) = S (k)$
29	26 28	eqtrd	$⊢ ((S \in Word B \land T \in Word B) \land k \in (0 ..^\|S\|)) \to ({(S ++ T) ↾}_{(0 ..^\|S\|)}) (k) = S (k)$
30	22 24 29	eqfnfvd	$⊢ (S \in Word B \land T \in Word B) \to {(S ++ T) ↾}_{(0 ..^\|S\|)} = S$
31	14 30	eqtrd	$⊢ (S \in Word B \land T \in Word B) \to (S ++ T) prefix \|S\| = S$

Metamath Proof Explorer

Theorem pfxccat1

Proof