pfxeq

Description: The prefixes of two words are equal iff they have the same length and the same symbols at each position. (Contributed by Alexander van der Vekens, 7-Aug-2018) (Revised by AV, 4-May-2020)

		Ref	Expression
	Assertion	pfxeq	$⊢ ((W \in Word V \land U \in Word V) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land (M \leq \|W\| \land N \leq \|U\|)) \to (W prefix M = U prefix N \leftrightarrow (M = N \land \forall i \in (0 ..^M) W (i) = U (i)))$

Proof

Step	Hyp	Ref	Expression
1		pfxcl	$⊢ W \in Word V \to W prefix M \in Word V$
2		pfxcl	$⊢ U \in Word V \to U prefix N \in Word V$
3		eqwrd	$⊢ (W prefix M \in Word V \land U prefix N \in Word V) \to (W prefix M = U prefix N \leftrightarrow (\|W prefix M\| = \|U prefix N\| \land \forall i \in (0 ..^\|W prefix M\|) (W prefix M) (i) = (U prefix N) (i)))$
4	1 2 3	syl2an	$⊢ (W \in Word V \land U \in Word V) \to (W prefix M = U prefix N \leftrightarrow (\|W prefix M\| = \|U prefix N\| \land \forall i \in (0 ..^\|W prefix M\|) (W prefix M) (i) = (U prefix N) (i)))$
5	4	3ad2ant2	$⊢ ((M \in ℕ_{0} \land N \in ℕ_{0}) \land (W \in Word V \land U \in Word V) \land (M \leq \|W\| \land N \leq \|U\|)) \to (W prefix M = U prefix N \leftrightarrow (\|W prefix M\| = \|U prefix N\| \land \forall i \in (0 ..^\|W prefix M\|) (W prefix M) (i) = (U prefix N) (i)))$
6		simp2l	$⊢ ((M \in ℕ_{0} \land N \in ℕ_{0}) \land (W \in Word V \land U \in Word V) \land (M \leq \|W\| \land N \leq \|U\|)) \to W \in Word V$
7		simpl	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to M \in ℕ_{0}$
8		lencl	$⊢ W \in Word V \to \|W\| \in ℕ_{0}$
9	8	adantr	$⊢ (W \in Word V \land U \in Word V) \to \|W\| \in ℕ_{0}$
10		simpl	$⊢ (M \leq \|W\| \land N \leq \|U\|) \to M \leq \|W\|$
11	7 9 10	3anim123i	$⊢ ((M \in ℕ_{0} \land N \in ℕ_{0}) \land (W \in Word V \land U \in Word V) \land (M \leq \|W\| \land N \leq \|U\|)) \to (M \in ℕ_{0} \land \|W\| \in ℕ_{0} \land M \leq \|W\|)$
12		elfz2nn0	$⊢ M \in (0 \dots \|W\|) \leftrightarrow (M \in ℕ_{0} \land \|W\| \in ℕ_{0} \land M \leq \|W\|)$
13	11 12	sylibr	$⊢ ((M \in ℕ_{0} \land N \in ℕ_{0}) \land (W \in Word V \land U \in Word V) \land (M \leq \|W\| \land N \leq \|U\|)) \to M \in (0 \dots \|W\|)$
14		pfxlen	$⊢ (W \in Word V \land M \in (0 \dots \|W\|)) \to \|W prefix M\| = M$
15	6 13 14	syl2anc	$⊢ ((M \in ℕ_{0} \land N \in ℕ_{0}) \land (W \in Word V \land U \in Word V) \land (M \leq \|W\| \land N \leq \|U\|)) \to \|W prefix M\| = M$
16		simp2r	$⊢ ((M \in ℕ_{0} \land N \in ℕ_{0}) \land (W \in Word V \land U \in Word V) \land (M \leq \|W\| \land N \leq \|U\|)) \to U \in Word V$
17		simpr	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to N \in ℕ_{0}$
18		lencl	$⊢ U \in Word V \to \|U\| \in ℕ_{0}$
19	18	adantl	$⊢ (W \in Word V \land U \in Word V) \to \|U\| \in ℕ_{0}$
20		simpr	$⊢ (M \leq \|W\| \land N \leq \|U\|) \to N \leq \|U\|$
21	17 19 20	3anim123i	$⊢ ((M \in ℕ_{0} \land N \in ℕ_{0}) \land (W \in Word V \land U \in Word V) \land (M \leq \|W\| \land N \leq \|U\|)) \to (N \in ℕ_{0} \land \|U\| \in ℕ_{0} \land N \leq \|U\|)$
22		elfz2nn0	$⊢ N \in (0 \dots \|U\|) \leftrightarrow (N \in ℕ_{0} \land \|U\| \in ℕ_{0} \land N \leq \|U\|)$
23	21 22	sylibr	$⊢ ((M \in ℕ_{0} \land N \in ℕ_{0}) \land (W \in Word V \land U \in Word V) \land (M \leq \|W\| \land N \leq \|U\|)) \to N \in (0 \dots \|U\|)$
24		pfxlen	$⊢ (U \in Word V \land N \in (0 \dots \|U\|)) \to \|U prefix N\| = N$
25	16 23 24	syl2anc	$⊢ ((M \in ℕ_{0} \land N \in ℕ_{0}) \land (W \in Word V \land U \in Word V) \land (M \leq \|W\| \land N \leq \|U\|)) \to \|U prefix N\| = N$
26	15 25	eqeq12d	$⊢ ((M \in ℕ_{0} \land N \in ℕ_{0}) \land (W \in Word V \land U \in Word V) \land (M \leq \|W\| \land N \leq \|U\|)) \to (\|W prefix M\| = \|U prefix N\| \leftrightarrow M = N)$
27	26	anbi1d	$⊢ ((M \in ℕ_{0} \land N \in ℕ_{0}) \land (W \in Word V \land U \in Word V) \land (M \leq \|W\| \land N \leq \|U\|)) \to ((\|W prefix M\| = \|U prefix N\| \land \forall i \in (0 ..^\|W prefix M\|) (W prefix M) (i) = (U prefix N) (i)) \leftrightarrow (M = N \land \forall i \in (0 ..^\|W prefix M\|) (W prefix M) (i) = (U prefix N) (i)))$
28	15	adantr	$⊢ (((M \in ℕ_{0} \land N \in ℕ_{0}) \land (W \in Word V \land U \in Word V) \land (M \leq \|W\| \land N \leq \|U\|)) \land M = N) \to \|W prefix M\| = M$
29	28	oveq2d	$⊢ (((M \in ℕ_{0} \land N \in ℕ_{0}) \land (W \in Word V \land U \in Word V) \land (M \leq \|W\| \land N \leq \|U\|)) \land M = N) \to (0 ..^\|W prefix M\|) = (0 ..^M)$
30	29	raleqdv	$⊢ (((M \in ℕ_{0} \land N \in ℕ_{0}) \land (W \in Word V \land U \in Word V) \land (M \leq \|W\| \land N \leq \|U\|)) \land M = N) \to (\forall i \in (0 ..^\|W prefix M\|) (W prefix M) (i) = (U prefix N) (i) \leftrightarrow \forall i \in (0 ..^M) (W prefix M) (i) = (U prefix N) (i))$
31	6	ad2antrr	$⊢ ((((M \in ℕ_{0} \land N \in ℕ_{0}) \land (W \in Word V \land U \in Word V) \land (M \leq \|W\| \land N \leq \|U\|)) \land M = N) \land i \in (0 ..^M)) \to W \in Word V$
32	13	ad2antrr	$⊢ ((((M \in ℕ_{0} \land N \in ℕ_{0}) \land (W \in Word V \land U \in Word V) \land (M \leq \|W\| \land N \leq \|U\|)) \land M = N) \land i \in (0 ..^M)) \to M \in (0 \dots \|W\|)$
33		simpr	$⊢ ((((M \in ℕ_{0} \land N \in ℕ_{0}) \land (W \in Word V \land U \in Word V) \land (M \leq \|W\| \land N \leq \|U\|)) \land M = N) \land i \in (0 ..^M)) \to i \in (0 ..^M)$
34		pfxfv	$⊢ (W \in Word V \land M \in (0 \dots \|W\|) \land i \in (0 ..^M)) \to (W prefix M) (i) = W (i)$
35	31 32 33 34	syl3anc	$⊢ ((((M \in ℕ_{0} \land N \in ℕ_{0}) \land (W \in Word V \land U \in Word V) \land (M \leq \|W\| \land N \leq \|U\|)) \land M = N) \land i \in (0 ..^M)) \to (W prefix M) (i) = W (i)$
36	16	ad2antrr	$⊢ ((((M \in ℕ_{0} \land N \in ℕ_{0}) \land (W \in Word V \land U \in Word V) \land (M \leq \|W\| \land N \leq \|U\|)) \land M = N) \land i \in (0 ..^M)) \to U \in Word V$
37	23	ad2antrr	$⊢ ((((M \in ℕ_{0} \land N \in ℕ_{0}) \land (W \in Word V \land U \in Word V) \land (M \leq \|W\| \land N \leq \|U\|)) \land M = N) \land i \in (0 ..^M)) \to N \in (0 \dots \|U\|)$
38		oveq2	$⊢ M = N \to (0 ..^M) = (0 ..^N)$
39	38	eleq2d	$⊢ M = N \to (i \in (0 ..^M) \leftrightarrow i \in (0 ..^N))$
40	39	adantl	$⊢ (((M \in ℕ_{0} \land N \in ℕ_{0}) \land (W \in Word V \land U \in Word V) \land (M \leq \|W\| \land N \leq \|U\|)) \land M = N) \to (i \in (0 ..^M) \leftrightarrow i \in (0 ..^N))$
41	40	biimpa	$⊢ ((((M \in ℕ_{0} \land N \in ℕ_{0}) \land (W \in Word V \land U \in Word V) \land (M \leq \|W\| \land N \leq \|U\|)) \land M = N) \land i \in (0 ..^M)) \to i \in (0 ..^N)$
42		pfxfv	$⊢ (U \in Word V \land N \in (0 \dots \|U\|) \land i \in (0 ..^N)) \to (U prefix N) (i) = U (i)$
43	36 37 41 42	syl3anc	$⊢ ((((M \in ℕ_{0} \land N \in ℕ_{0}) \land (W \in Word V \land U \in Word V) \land (M \leq \|W\| \land N \leq \|U\|)) \land M = N) \land i \in (0 ..^M)) \to (U prefix N) (i) = U (i)$
44	35 43	eqeq12d	$⊢ ((((M \in ℕ_{0} \land N \in ℕ_{0}) \land (W \in Word V \land U \in Word V) \land (M \leq \|W\| \land N \leq \|U\|)) \land M = N) \land i \in (0 ..^M)) \to ((W prefix M) (i) = (U prefix N) (i) \leftrightarrow W (i) = U (i))$
45	44	ralbidva	$⊢ (((M \in ℕ_{0} \land N \in ℕ_{0}) \land (W \in Word V \land U \in Word V) \land (M \leq \|W\| \land N \leq \|U\|)) \land M = N) \to (\forall i \in (0 ..^M) (W prefix M) (i) = (U prefix N) (i) \leftrightarrow \forall i \in (0 ..^M) W (i) = U (i))$
46	30 45	bitrd	$⊢ (((M \in ℕ_{0} \land N \in ℕ_{0}) \land (W \in Word V \land U \in Word V) \land (M \leq \|W\| \land N \leq \|U\|)) \land M = N) \to (\forall i \in (0 ..^\|W prefix M\|) (W prefix M) (i) = (U prefix N) (i) \leftrightarrow \forall i \in (0 ..^M) W (i) = U (i))$
47	46	pm5.32da	$⊢ ((M \in ℕ_{0} \land N \in ℕ_{0}) \land (W \in Word V \land U \in Word V) \land (M \leq \|W\| \land N \leq \|U\|)) \to ((M = N \land \forall i \in (0 ..^\|W prefix M\|) (W prefix M) (i) = (U prefix N) (i)) \leftrightarrow (M = N \land \forall i \in (0 ..^M) W (i) = U (i)))$
48	5 27 47	3bitrd	$⊢ ((M \in ℕ_{0} \land N \in ℕ_{0}) \land (W \in Word V \land U \in Word V) \land (M \leq \|W\| \land N \leq \|U\|)) \to (W prefix M = U prefix N \leftrightarrow (M = N \land \forall i \in (0 ..^M) W (i) = U (i)))$
49	48	3com12	$⊢ ((W \in Word V \land U \in Word V) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land (M \leq \|W\| \land N \leq \|U\|)) \to (W prefix M = U prefix N \leftrightarrow (M = N \land \forall i \in (0 ..^M) W (i) = U (i)))$

Metamath Proof Explorer

Theorem pfxeq

Proof