numclwwlk1lem2foalem

Description: Lemma for numclwwlk1lem2foa . (Contributed by AV, 29-May-2021) (Revised by AV, 1-Nov-2022)

		Ref	Expression
	Assertion	numclwwlk1lem2foalem	$⊢ ((W \in Word V \land \|W\| = N - 2) \land (X \in V \land Y \in V) \land N \in ℤ_{\geq 3}) \to (((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩) prefix (N - 2) = W \land ((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩) (N - 1) = Y \land ((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩) (N - 2) = X)$

Proof

Step	Hyp	Ref	Expression
1		simpl	$⊢ (W \in Word V \land \|W\| = N - 2) \to W \in Word V$
2		s1cl	$⊢ X \in V \to ⟨“ X ”⟩ \in Word V$
3		s1cl	$⊢ Y \in V \to ⟨“ Y ”⟩ \in Word V$
4	1 2 3	3anim123i	$⊢ ((W \in Word V \land \|W\| = N - 2) \land X \in V \land Y \in V) \to (W \in Word V \land ⟨“ X ”⟩ \in Word V \land ⟨“ Y ”⟩ \in Word V)$
5	4	3expb	$⊢ ((W \in Word V \land \|W\| = N - 2) \land (X \in V \land Y \in V)) \to (W \in Word V \land ⟨“ X ”⟩ \in Word V \land ⟨“ Y ”⟩ \in Word V)$
6		ccatass	$⊢ (W \in Word V \land ⟨“ X ”⟩ \in Word V \land ⟨“ Y ”⟩ \in Word V) \to (W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩ = W ++ (⟨“ X ”⟩ ++ ⟨“ Y ”⟩)$
7	5 6	syl	$⊢ ((W \in Word V \land \|W\| = N - 2) \land (X \in V \land Y \in V)) \to (W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩ = W ++ (⟨“ X ”⟩ ++ ⟨“ Y ”⟩)$
8	7	oveq1d	$⊢ ((W \in Word V \land \|W\| = N - 2) \land (X \in V \land Y \in V)) \to ((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩) prefix (N - 2) = (W ++ (⟨“ X ”⟩ ++ ⟨“ Y ”⟩)) prefix (N - 2)$
9	1	adantr	$⊢ ((W \in Word V \land \|W\| = N - 2) \land (X \in V \land Y \in V)) \to W \in Word V$
10		ccat2s1cl	$⊢ (X \in V \land Y \in V) \to ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ \in Word V$
11	10	adantl	$⊢ ((W \in Word V \land \|W\| = N - 2) \land (X \in V \land Y \in V)) \to ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ \in Word V$
12		simpr	$⊢ (W \in Word V \land \|W\| = N - 2) \to \|W\| = N - 2$
13	12	eqcomd	$⊢ (W \in Word V \land \|W\| = N - 2) \to N - 2 = \|W\|$
14	13	adantr	$⊢ ((W \in Word V \land \|W\| = N - 2) \land (X \in V \land Y \in V)) \to N - 2 = \|W\|$
15		pfxccatid	$⊢ (W \in Word V \land ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ \in Word V \land N - 2 = \|W\|) \to (W ++ (⟨“ X ”⟩ ++ ⟨“ Y ”⟩)) prefix (N - 2) = W$
16	9 11 14 15	syl3anc	$⊢ ((W \in Word V \land \|W\| = N - 2) \land (X \in V \land Y \in V)) \to (W ++ (⟨“ X ”⟩ ++ ⟨“ Y ”⟩)) prefix (N - 2) = W$
17	8 16	eqtrd	$⊢ ((W \in Word V \land \|W\| = N - 2) \land (X \in V \land Y \in V)) \to ((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩) prefix (N - 2) = W$
18	17	3adant3	$⊢ ((W \in Word V \land \|W\| = N - 2) \land (X \in V \land Y \in V) \land N \in ℤ_{\geq 3}) \to ((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩) prefix (N - 2) = W$
19		1e2m1	$⊢ 1 = 2 - 1$
20	19	oveq2i	$⊢ N - 1 = N - (2 - 1)$
21		eluzelcn	$⊢ N \in ℤ_{\geq 3} \to N \in ℂ$
22		2cnd	$⊢ N \in ℤ_{\geq 3} \to 2 \in ℂ$
23		1cnd	$⊢ N \in ℤ_{\geq 3} \to 1 \in ℂ$
24	21 22 23	subsubd	$⊢ N \in ℤ_{\geq 3} \to N - (2 - 1) = N - 2 + 1$
25	20 24	syl5eq	$⊢ N \in ℤ_{\geq 3} \to N - 1 = N - 2 + 1$
26	25	3ad2ant3	$⊢ ((W \in Word V \land \|W\| = N - 2) \land (X \in V \land Y \in V) \land N \in ℤ_{\geq 3}) \to N - 1 = N - 2 + 1$
27	26	fveq2d	$⊢ ((W \in Word V \land \|W\| = N - 2) \land (X \in V \land Y \in V) \land N \in ℤ_{\geq 3}) \to ((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩) (N - 1) = ((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩) (N - 2 + 1)$
28		ccatw2s1p2	$⊢ ((W \in Word V \land \|W\| = N - 2) \land (X \in V \land Y \in V)) \to ((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩) (N - 2 + 1) = Y$
29	28	3adant3	$⊢ ((W \in Word V \land \|W\| = N - 2) \land (X \in V \land Y \in V) \land N \in ℤ_{\geq 3}) \to ((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩) (N - 2 + 1) = Y$
30	27 29	eqtrd	$⊢ ((W \in Word V \land \|W\| = N - 2) \land (X \in V \land Y \in V) \land N \in ℤ_{\geq 3}) \to ((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩) (N - 1) = Y$
31		simpl	$⊢ (X \in V \land Y \in V) \to X \in V$
32		ccatw2s1p1	$⊢ (W \in Word V \land \|W\| = N - 2 \land X \in V) \to ((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩) (N - 2) = X$
33	1 12 31 32	syl2an3an	$⊢ ((W \in Word V \land \|W\| = N - 2) \land (X \in V \land Y \in V)) \to ((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩) (N - 2) = X$
34	33	3adant3	$⊢ ((W \in Word V \land \|W\| = N - 2) \land (X \in V \land Y \in V) \land N \in ℤ_{\geq 3}) \to ((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩) (N - 2) = X$
35	18 30 34	3jca	$⊢ ((W \in Word V \land \|W\| = N - 2) \land (X \in V \land Y \in V) \land N \in ℤ_{\geq 3}) \to (((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩) prefix (N - 2) = W \land ((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩) (N - 1) = Y \land ((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩) (N - 2) = X)$

Metamath Proof Explorer

Theorem numclwwlk1lem2foalem

Proof