swrdccat2

Description: Recover the right half of a concatenated word. (Contributed by Mario Carneiro, 27-Sep-2015)

		Ref	Expression
	Assertion	swrdccat2	$⊢ (S \in Word B \land T \in Word B) \to (S ++ T) substr ⟨\|S\|, \|S\| + \|T\|⟩ = T$

Proof

Step	Hyp	Ref	Expression
1		ccatcl	$⊢ (S \in Word B \land T \in Word B) \to S ++ T \in Word B$
2		swrdcl	$⊢ S ++ T \in Word B \to (S ++ T) substr ⟨\|S\|, \|S\| + \|T\|⟩ \in Word B$
3		wrdfn	$⊢ (S ++ T) substr ⟨\|S\|, \|S\| + \|T\|⟩ \in Word B \to ((S ++ T) substr ⟨\|S\|, \|S\| + \|T\|⟩) Fn (0 ..^\|(S ++ T) substr ⟨\|S\|, \|S\| + \|T\|⟩\|)$
4	1 2 3	3syl	$⊢ (S \in Word B \land T \in Word B) \to ((S ++ T) substr ⟨\|S\|, \|S\| + \|T\|⟩) Fn (0 ..^\|(S ++ T) substr ⟨\|S\|, \|S\| + \|T\|⟩\|)$
5		lencl	$⊢ S \in Word B \to \|S\| \in ℕ_{0}$
6		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
7	5 6	eleqtrdi	$⊢ S \in Word B \to \|S\| \in ℤ_{\geq 0}$
8	7	adantr	$⊢ (S \in Word B \land T \in Word B) \to \|S\| \in ℤ_{\geq 0}$
9	5	nn0zd	$⊢ S \in Word B \to \|S\| \in ℤ$
10	9	uzidd	$⊢ S \in Word B \to \|S\| \in ℤ_{\geq \|S\|}$
11		lencl	$⊢ T \in Word B \to \|T\| \in ℕ_{0}$
12		uzaddcl	$⊢ (\|S\| \in ℤ_{\geq \|S\|} \land \|T\| \in ℕ_{0}) \to \|S\| + \|T\| \in ℤ_{\geq \|S\|}$
13	10 11 12	syl2an	$⊢ (S \in Word B \land T \in Word B) \to \|S\| + \|T\| \in ℤ_{\geq \|S\|}$
14		elfzuzb	$⊢ \|S\| \in (0 \dots \|S\| + \|T\|) \leftrightarrow (\|S\| \in ℤ_{\geq 0} \land \|S\| + \|T\| \in ℤ_{\geq \|S\|})$
15	8 13 14	sylanbrc	$⊢ (S \in Word B \land T \in Word B) \to \|S\| \in (0 \dots \|S\| + \|T\|)$
16		nn0addcl	$⊢ (\|S\| \in ℕ_{0} \land \|T\| \in ℕ_{0}) \to \|S\| + \|T\| \in ℕ_{0}$
17	5 11 16	syl2an	$⊢ (S \in Word B \land T \in Word B) \to \|S\| + \|T\| \in ℕ_{0}$
18	17 6	eleqtrdi	$⊢ (S \in Word B \land T \in Word B) \to \|S\| + \|T\| \in ℤ_{\geq 0}$
19	17	nn0zd	$⊢ (S \in Word B \land T \in Word B) \to \|S\| + \|T\| \in ℤ$
20	19	uzidd	$⊢ (S \in Word B \land T \in Word B) \to \|S\| + \|T\| \in ℤ_{\geq (\|S\| + \|T\|)}$
21		elfzuzb	$⊢ \|S\| + \|T\| \in (0 \dots \|S\| + \|T\|) \leftrightarrow (\|S\| + \|T\| \in ℤ_{\geq 0} \land \|S\| + \|T\| \in ℤ_{\geq (\|S\| + \|T\|)})$
22	18 20 21	sylanbrc	$⊢ (S \in Word B \land T \in Word B) \to \|S\| + \|T\| \in (0 \dots \|S\| + \|T\|)$
23		ccatlen	$⊢ (S \in Word B \land T \in Word B) \to \|S ++ T\| = \|S\| + \|T\|$
24	23	oveq2d	$⊢ (S \in Word B \land T \in Word B) \to (0 \dots \|S ++ T\|) = (0 \dots \|S\| + \|T\|)$
25	22 24	eleqtrrd	$⊢ (S \in Word B \land T \in Word B) \to \|S\| + \|T\| \in (0 \dots \|S ++ T\|)$
26		swrdlen	$⊢ (S ++ T \in Word B \land \|S\| \in (0 \dots \|S\| + \|T\|) \land \|S\| + \|T\| \in (0 \dots \|S ++ T\|)) \to \|(S ++ T) substr ⟨\|S\|, \|S\| + \|T\|⟩\| = \|S\| + \|T\| - \|S\|$
27	1 15 25 26	syl3anc	$⊢ (S \in Word B \land T \in Word B) \to \|(S ++ T) substr ⟨\|S\|, \|S\| + \|T\|⟩\| = \|S\| + \|T\| - \|S\|$
28	5	nn0cnd	$⊢ S \in Word B \to \|S\| \in ℂ$
29	11	nn0cnd	$⊢ T \in Word B \to \|T\| \in ℂ$
30		pncan2	$⊢ (\|S\| \in ℂ \land \|T\| \in ℂ) \to \|S\| + \|T\| - \|S\| = \|T\|$
31	28 29 30	syl2an	$⊢ (S \in Word B \land T \in Word B) \to \|S\| + \|T\| - \|S\| = \|T\|$
32	27 31	eqtrd	$⊢ (S \in Word B \land T \in Word B) \to \|(S ++ T) substr ⟨\|S\|, \|S\| + \|T\|⟩\| = \|T\|$
33	32	oveq2d	$⊢ (S \in Word B \land T \in Word B) \to (0 ..^\|(S ++ T) substr ⟨\|S\|, \|S\| + \|T\|⟩\|) = (0 ..^\|T\|)$
34	33	fneq2d	$⊢ (S \in Word B \land T \in Word B) \to (((S ++ T) substr ⟨\|S\|, \|S\| + \|T\|⟩) Fn (0 ..^\|(S ++ T) substr ⟨\|S\|, \|S\| + \|T\|⟩\|) \leftrightarrow ((S ++ T) substr ⟨\|S\|, \|S\| + \|T\|⟩) Fn (0 ..^\|T\|))$
35	4 34	mpbid	$⊢ (S \in Word B \land T \in Word B) \to ((S ++ T) substr ⟨\|S\|, \|S\| + \|T\|⟩) Fn (0 ..^\|T\|)$
36		wrdfn	$⊢ T \in Word B \to T Fn (0 ..^\|T\|)$
37	36	adantl	$⊢ (S \in Word B \land T \in Word B) \to T Fn (0 ..^\|T\|)$
38	1 15 25	3jca	$⊢ (S \in Word B \land T \in Word B) \to (S ++ T \in Word B \land \|S\| \in (0 \dots \|S\| + \|T\|) \land \|S\| + \|T\| \in (0 \dots \|S ++ T\|))$
39	31	oveq2d	$⊢ (S \in Word B \land T \in Word B) \to (0 ..^\|S\| + \|T\| - \|S\|) = (0 ..^\|T\|)$
40	39	eleq2d	$⊢ (S \in Word B \land T \in Word B) \to (k \in (0 ..^\|S\| + \|T\| - \|S\|) \leftrightarrow k \in (0 ..^\|T\|))$
41	40	biimpar	$⊢ ((S \in Word B \land T \in Word B) \land k \in (0 ..^\|T\|)) \to k \in (0 ..^\|S\| + \|T\| - \|S\|)$
42		swrdfv	$⊢ ((S ++ T \in Word B \land \|S\| \in (0 \dots \|S\| + \|T\|) \land \|S\| + \|T\| \in (0 \dots \|S ++ T\|)) \land k \in (0 ..^\|S\| + \|T\| - \|S\|)) \to ((S ++ T) substr ⟨\|S\|, \|S\| + \|T\|⟩) (k) = (S ++ T) (k + \|S\|)$
43	38 41 42	syl2an2r	$⊢ ((S \in Word B \land T \in Word B) \land k \in (0 ..^\|T\|)) \to ((S ++ T) substr ⟨\|S\|, \|S\| + \|T\|⟩) (k) = (S ++ T) (k + \|S\|)$
44		ccatval3	$⊢ (S \in Word B \land T \in Word B \land k \in (0 ..^\|T\|)) \to (S ++ T) (k + \|S\|) = T (k)$
45	44	3expa	$⊢ ((S \in Word B \land T \in Word B) \land k \in (0 ..^\|T\|)) \to (S ++ T) (k + \|S\|) = T (k)$
46	43 45	eqtrd	$⊢ ((S \in Word B \land T \in Word B) \land k \in (0 ..^\|T\|)) \to ((S ++ T) substr ⟨\|S\|, \|S\| + \|T\|⟩) (k) = T (k)$
47	35 37 46	eqfnfvd	$⊢ (S \in Word B \land T \in Word B) \to (S ++ T) substr ⟨\|S\|, \|S\| + \|T\|⟩ = T$

Metamath Proof Explorer

Theorem swrdccat2

Proof