gsumwrd2dccatlem

Description: Lemma for gsumwrd2dccat . Expose a bijection F between (ordered) pairs of words and words with a length of a subword. (Contributed by Thierry Arnoux, 5-Oct-2025)

	Ref	Expression
Hypotheses	gsumwrd2dccatlem.u	$⊢ U = ⋃_{w \in Word A} (\{w\} \times (0 \dots \|w\|))$
	gsumwrd2dccatlem.f	$⊢ F = (a \in (Word A \times Word A) ⟼ ⟨1^{st} (a) ++ 2^{nd} (a), \|1^{st} (a)\|⟩)$
	gsumwrd2dccatlem.g	$⊢ G = (b \in U ⟼ ⟨1^{st} (b) prefix 2^{nd} (b), 1^{st} (b) substr ⟨2^{nd} (b), \|1^{st} (b)\|⟩⟩)$
	gsumwrd2dccatlem.a	$⊢ φ \to A \in V$
Assertion	gsumwrd2dccatlem	$⊢ φ \to (F : Word A \times Word A \underset{1-1 onto}{⟶} U \land F^{-1} = G)$

Proof

Step	Hyp	Ref	Expression
1		gsumwrd2dccatlem.u	$⊢ U = ⋃_{w \in Word A} (\{w\} \times (0 \dots \|w\|))$
2		gsumwrd2dccatlem.f	$⊢ F = (a \in (Word A \times Word A) ⟼ ⟨1^{st} (a) ++ 2^{nd} (a), \|1^{st} (a)\|⟩)$
3		gsumwrd2dccatlem.g	$⊢ G = (b \in U ⟼ ⟨1^{st} (b) prefix 2^{nd} (b), 1^{st} (b) substr ⟨2^{nd} (b), \|1^{st} (b)\|⟩⟩)$
4		gsumwrd2dccatlem.a	$⊢ φ \to A \in V$
5		sneq	$⊢ w = 1^{st} (a) ++ 2^{nd} (a) \to \{w\} = \{1^{st} (a) ++ 2^{nd} (a)\}$
6		fveq2	$⊢ w = 1^{st} (a) ++ 2^{nd} (a) \to \|w\| = \|1^{st} (a) ++ 2^{nd} (a)\|$
7	6	oveq2d	$⊢ w = 1^{st} (a) ++ 2^{nd} (a) \to (0 \dots \|w\|) = (0 \dots \|1^{st} (a) ++ 2^{nd} (a)\|)$
8	5 7	xpeq12d	$⊢ w = 1^{st} (a) ++ 2^{nd} (a) \to \{w\} \times (0 \dots \|w\|) = \{1^{st} (a) ++ 2^{nd} (a)\} \times (0 \dots \|1^{st} (a) ++ 2^{nd} (a)\|)$
9	8	eleq2d	$⊢ w = 1^{st} (a) ++ 2^{nd} (a) \to (⟨1^{st} (a) ++ 2^{nd} (a), \|1^{st} (a)\|⟩ \in (\{w\} \times (0 \dots \|w\|)) \leftrightarrow ⟨1^{st} (a) ++ 2^{nd} (a), \|1^{st} (a)\|⟩ \in (\{1^{st} (a) ++ 2^{nd} (a)\} \times (0 \dots \|1^{st} (a) ++ 2^{nd} (a)\|)))$
10		xp1st	$⊢ a \in (Word A \times Word A) \to 1^{st} (a) \in Word A$
11	10	adantl	$⊢ (φ \land a \in (Word A \times Word A)) \to 1^{st} (a) \in Word A$
12		xp2nd	$⊢ a \in (Word A \times Word A) \to 2^{nd} (a) \in Word A$
13	12	adantl	$⊢ (φ \land a \in (Word A \times Word A)) \to 2^{nd} (a) \in Word A$
14		ccatcl	$⊢ (1^{st} (a) \in Word A \land 2^{nd} (a) \in Word A) \to 1^{st} (a) ++ 2^{nd} (a) \in Word A$
15	11 13 14	syl2anc	$⊢ (φ \land a \in (Word A \times Word A)) \to 1^{st} (a) ++ 2^{nd} (a) \in Word A$
16		ovex	$⊢ 1^{st} (a) ++ 2^{nd} (a) \in V$
17	16	snid	$⊢ 1^{st} (a) ++ 2^{nd} (a) \in \{1^{st} (a) ++ 2^{nd} (a)\}$
18	17	a1i	$⊢ (φ \land a \in (Word A \times Word A)) \to 1^{st} (a) ++ 2^{nd} (a) \in \{1^{st} (a) ++ 2^{nd} (a)\}$
19		0zd	$⊢ (φ \land a \in (Word A \times Word A)) \to 0 \in ℤ$
20		lencl	$⊢ 1^{st} (a) ++ 2^{nd} (a) \in Word A \to \|1^{st} (a) ++ 2^{nd} (a)\| \in ℕ_{0}$
21	15 20	syl	$⊢ (φ \land a \in (Word A \times Word A)) \to \|1^{st} (a) ++ 2^{nd} (a)\| \in ℕ_{0}$
22	21	nn0zd	$⊢ (φ \land a \in (Word A \times Word A)) \to \|1^{st} (a) ++ 2^{nd} (a)\| \in ℤ$
23		lencl	$⊢ 1^{st} (a) \in Word A \to \|1^{st} (a)\| \in ℕ_{0}$
24	11 23	syl	$⊢ (φ \land a \in (Word A \times Word A)) \to \|1^{st} (a)\| \in ℕ_{0}$
25	24	nn0zd	$⊢ (φ \land a \in (Word A \times Word A)) \to \|1^{st} (a)\| \in ℤ$
26	24	nn0ge0d	$⊢ (φ \land a \in (Word A \times Word A)) \to 0 \leq \|1^{st} (a)\|$
27		lencl	$⊢ 2^{nd} (a) \in Word A \to \|2^{nd} (a)\| \in ℕ_{0}$
28	13 27	syl	$⊢ (φ \land a \in (Word A \times Word A)) \to \|2^{nd} (a)\| \in ℕ_{0}$
29	28	nn0ge0d	$⊢ (φ \land a \in (Word A \times Word A)) \to 0 \leq \|2^{nd} (a)\|$
30	24	nn0red	$⊢ (φ \land a \in (Word A \times Word A)) \to \|1^{st} (a)\| \in ℝ$
31	28	nn0red	$⊢ (φ \land a \in (Word A \times Word A)) \to \|2^{nd} (a)\| \in ℝ$
32	30 31	addge01d	$⊢ (φ \land a \in (Word A \times Word A)) \to (0 \leq \|2^{nd} (a)\| \leftrightarrow \|1^{st} (a)\| \leq \|1^{st} (a)\| + \|2^{nd} (a)\|)$
33	29 32	mpbid	$⊢ (φ \land a \in (Word A \times Word A)) \to \|1^{st} (a)\| \leq \|1^{st} (a)\| + \|2^{nd} (a)\|$
34		ccatlen	$⊢ (1^{st} (a) \in Word A \land 2^{nd} (a) \in Word A) \to \|1^{st} (a) ++ 2^{nd} (a)\| = \|1^{st} (a)\| + \|2^{nd} (a)\|$
35	11 13 34	syl2anc	$⊢ (φ \land a \in (Word A \times Word A)) \to \|1^{st} (a) ++ 2^{nd} (a)\| = \|1^{st} (a)\| + \|2^{nd} (a)\|$
36	33 35	breqtrrd	$⊢ (φ \land a \in (Word A \times Word A)) \to \|1^{st} (a)\| \leq \|1^{st} (a) ++ 2^{nd} (a)\|$
37	19 22 25 26 36	elfzd	$⊢ (φ \land a \in (Word A \times Word A)) \to \|1^{st} (a)\| \in (0 \dots \|1^{st} (a) ++ 2^{nd} (a)\|)$
38	18 37	opelxpd	$⊢ (φ \land a \in (Word A \times Word A)) \to ⟨1^{st} (a) ++ 2^{nd} (a), \|1^{st} (a)\|⟩ \in (\{1^{st} (a) ++ 2^{nd} (a)\} \times (0 \dots \|1^{st} (a) ++ 2^{nd} (a)\|))$
39	9 15 38	rspcedvdw	$⊢ (φ \land a \in (Word A \times Word A)) \to \exists w \in Word A ⟨1^{st} (a) ++ 2^{nd} (a), \|1^{st} (a)\|⟩ \in (\{w\} \times (0 \dots \|w\|))$
40	39	eliund	$⊢ (φ \land a \in (Word A \times Word A)) \to ⟨1^{st} (a) ++ 2^{nd} (a), \|1^{st} (a)\|⟩ \in ⋃_{w \in Word A} (\{w\} \times (0 \dots \|w\|))$
41	40 1	eleqtrrdi	$⊢ (φ \land a \in (Word A \times Word A)) \to ⟨1^{st} (a) ++ 2^{nd} (a), \|1^{st} (a)\|⟩ \in U$
42		simpr	$⊢ ((φ \land u \in Word A) \land b \in (\{u\} \times (0 \dots \|u\|))) \to b \in (\{u\} \times (0 \dots \|u\|))$
43		xp1st	$⊢ b \in (\{u\} \times (0 \dots \|u\|)) \to 1^{st} (b) \in \{u\}$
44		elsni	$⊢ 1^{st} (b) \in \{u\} \to 1^{st} (b) = u$
45	42 43 44	3syl	$⊢ ((φ \land u \in Word A) \land b \in (\{u\} \times (0 \dots \|u\|))) \to 1^{st} (b) = u$
46		simplr	$⊢ ((φ \land u \in Word A) \land b \in (\{u\} \times (0 \dots \|u\|))) \to u \in Word A$
47	45 46	eqeltrd	$⊢ ((φ \land u \in Word A) \land b \in (\{u\} \times (0 \dots \|u\|))) \to 1^{st} (b) \in Word A$
48	47	adantllr	$⊢ (((φ \land b \in U) \land u \in Word A) \land b \in (\{u\} \times (0 \dots \|u\|))) \to 1^{st} (b) \in Word A$
49	1	eleq2i	$⊢ b \in U \leftrightarrow b \in ⋃_{w \in Word A} (\{w\} \times (0 \dots \|w\|))$
50	49	bilani	$⊢ (φ \land b \in U) \to b \in ⋃_{w \in Word A} (\{w\} \times (0 \dots \|w\|))$
51		eliun	$⊢ b \in ⋃_{w \in Word A} (\{w\} \times (0 \dots \|w\|)) \leftrightarrow \exists w \in Word A b \in (\{w\} \times (0 \dots \|w\|))$
52	50 51	sylib	$⊢ (φ \land b \in U) \to \exists w \in Word A b \in (\{w\} \times (0 \dots \|w\|))$
53		sneq	$⊢ u = w \to \{u\} = \{w\}$
54		fveq2	$⊢ u = w \to \|u\| = \|w\|$
55	54	oveq2d	$⊢ u = w \to (0 \dots \|u\|) = (0 \dots \|w\|)$
56	53 55	xpeq12d	$⊢ u = w \to \{u\} \times (0 \dots \|u\|) = \{w\} \times (0 \dots \|w\|)$
57	56	eleq2d	$⊢ u = w \to (b \in (\{u\} \times (0 \dots \|u\|)) \leftrightarrow b \in (\{w\} \times (0 \dots \|w\|)))$
58	57	cbvrexvw	$⊢ \exists u \in Word A b \in (\{u\} \times (0 \dots \|u\|)) \leftrightarrow \exists w \in Word A b \in (\{w\} \times (0 \dots \|w\|))$
59	52 58	sylibr	$⊢ (φ \land b \in U) \to \exists u \in Word A b \in (\{u\} \times (0 \dots \|u\|))$
60	48 59	r19.29a	$⊢ (φ \land b \in U) \to 1^{st} (b) \in Word A$
61		pfxcl	$⊢ 1^{st} (b) \in Word A \to 1^{st} (b) prefix 2^{nd} (b) \in Word A$
62	60 61	syl	$⊢ (φ \land b \in U) \to 1^{st} (b) prefix 2^{nd} (b) \in Word A$
63		swrdcl	$⊢ 1^{st} (b) \in Word A \to 1^{st} (b) substr ⟨2^{nd} (b), \|1^{st} (b)\|⟩ \in Word A$
64	60 63	syl	$⊢ (φ \land b \in U) \to 1^{st} (b) substr ⟨2^{nd} (b), \|1^{st} (b)\|⟩ \in Word A$
65	62 64	opelxpd	$⊢ (φ \land b \in U) \to ⟨1^{st} (b) prefix 2^{nd} (b), 1^{st} (b) substr ⟨2^{nd} (b), \|1^{st} (b)\|⟩⟩ \in (Word A \times Word A)$
66	50	adantr	$⊢ ((φ \land b \in U) \land a \in (Word A \times Word A)) \to b \in ⋃_{w \in Word A} (\{w\} \times (0 \dots \|w\|))$
67		eliunxp	$⊢ b \in ⋃_{w \in Word A} (\{w\} \times (0 \dots \|w\|)) \leftrightarrow \exists w \exists n (b = ⟨w, n⟩ \land (w \in Word A \land n \in (0 \dots \|w\|)))$
68	66 67	sylib	$⊢ ((φ \land b \in U) \land a \in (Word A \times Word A)) \to \exists w \exists n (b = ⟨w, n⟩ \land (w \in Word A \land n \in (0 \dots \|w\|)))$
69		opeq1	$⊢ u = w \to ⟨u, n⟩ = ⟨w, n⟩$
70	69	eqeq2d	$⊢ u = w \to (b = ⟨u, n⟩ \leftrightarrow b = ⟨w, n⟩)$
71		eleq1w	$⊢ u = w \to (u \in Word A \leftrightarrow w \in Word A)$
72	55	eleq2d	$⊢ u = w \to (n \in (0 \dots \|u\|) \leftrightarrow n \in (0 \dots \|w\|))$
73	71 72	anbi12d	$⊢ u = w \to ((u \in Word A \land n \in (0 \dots \|u\|)) \leftrightarrow (w \in Word A \land n \in (0 \dots \|w\|)))$
74	70 73	anbi12d	$⊢ u = w \to ((b = ⟨u, n⟩ \land (u \in Word A \land n \in (0 \dots \|u\|))) \leftrightarrow (b = ⟨w, n⟩ \land (w \in Word A \land n \in (0 \dots \|w\|))))$
75	74	exbidv	$⊢ u = w \to (\exists n (b = ⟨u, n⟩ \land (u \in Word A \land n \in (0 \dots \|u\|))) \leftrightarrow \exists n (b = ⟨w, n⟩ \land (w \in Word A \land n \in (0 \dots \|w\|))))$
76	75	cbvexvw	$⊢ \exists u \exists n (b = ⟨u, n⟩ \land (u \in Word A \land n \in (0 \dots \|u\|))) \leftrightarrow \exists w \exists n (b = ⟨w, n⟩ \land (w \in Word A \land n \in (0 \dots \|w\|)))$
77	68 76	sylibr	$⊢ ((φ \land b \in U) \land a \in (Word A \times Word A)) \to \exists u \exists n (b = ⟨u, n⟩ \land (u \in Word A \land n \in (0 \dots \|u\|)))$
78		simplr	$⊢ ((((((φ \land a \in (Word A \times Word A)) \land b = ⟨u, n⟩) \land u \in Word A) \land n \in (0 \dots \|u\|)) \land 1^{st} (a) = 1^{st} (b) prefix 2^{nd} (b)) \land 2^{nd} (a) = 1^{st} (b) substr ⟨2^{nd} (b), \|1^{st} (b)\|⟩) \to 1^{st} (a) = 1^{st} (b) prefix 2^{nd} (b)$
79		simpr	$⊢ ((((((φ \land a \in (Word A \times Word A)) \land b = ⟨u, n⟩) \land u \in Word A) \land n \in (0 \dots \|u\|)) \land 1^{st} (a) = 1^{st} (b) prefix 2^{nd} (b)) \land 2^{nd} (a) = 1^{st} (b) substr ⟨2^{nd} (b), \|1^{st} (b)\|⟩) \to 2^{nd} (a) = 1^{st} (b) substr ⟨2^{nd} (b), \|1^{st} (b)\|⟩$
80	78 79	oveq12d	$⊢ ((((((φ \land a \in (Word A \times Word A)) \land b = ⟨u, n⟩) \land u \in Word A) \land n \in (0 \dots \|u\|)) \land 1^{st} (a) = 1^{st} (b) prefix 2^{nd} (b)) \land 2^{nd} (a) = 1^{st} (b) substr ⟨2^{nd} (b), \|1^{st} (b)\|⟩) \to 1^{st} (a) ++ 2^{nd} (a) = (1^{st} (b) prefix 2^{nd} (b)) ++ (1^{st} (b) substr ⟨2^{nd} (b), \|1^{st} (b)\|⟩)$
81		vex	$⊢ u \in V$
82		vex	$⊢ n \in V$
83	81 82	op1std	$⊢ b = ⟨u, n⟩ \to 1^{st} (b) = u$
84	83	ad5antlr	$⊢ ((((((φ \land a \in (Word A \times Word A)) \land b = ⟨u, n⟩) \land u \in Word A) \land n \in (0 \dots \|u\|)) \land 1^{st} (a) = 1^{st} (b) prefix 2^{nd} (b)) \land 2^{nd} (a) = 1^{st} (b) substr ⟨2^{nd} (b), \|1^{st} (b)\|⟩) \to 1^{st} (b) = u$
85		simp-4r	$⊢ ((((((φ \land a \in (Word A \times Word A)) \land b = ⟨u, n⟩) \land u \in Word A) \land n \in (0 \dots \|u\|)) \land 1^{st} (a) = 1^{st} (b) prefix 2^{nd} (b)) \land 2^{nd} (a) = 1^{st} (b) substr ⟨2^{nd} (b), \|1^{st} (b)\|⟩) \to u \in Word A$
86	84 85	eqeltrd	$⊢ ((((((φ \land a \in (Word A \times Word A)) \land b = ⟨u, n⟩) \land u \in Word A) \land n \in (0 \dots \|u\|)) \land 1^{st} (a) = 1^{st} (b) prefix 2^{nd} (b)) \land 2^{nd} (a) = 1^{st} (b) substr ⟨2^{nd} (b), \|1^{st} (b)\|⟩) \to 1^{st} (b) \in Word A$
87	81 82	op2ndd	$⊢ b = ⟨u, n⟩ \to 2^{nd} (b) = n$
88	87	ad5antlr	$⊢ ((((((φ \land a \in (Word A \times Word A)) \land b = ⟨u, n⟩) \land u \in Word A) \land n \in (0 \dots \|u\|)) \land 1^{st} (a) = 1^{st} (b) prefix 2^{nd} (b)) \land 2^{nd} (a) = 1^{st} (b) substr ⟨2^{nd} (b), \|1^{st} (b)\|⟩) \to 2^{nd} (b) = n$
89		simpllr	$⊢ ((((((φ \land a \in (Word A \times Word A)) \land b = ⟨u, n⟩) \land u \in Word A) \land n \in (0 \dots \|u\|)) \land 1^{st} (a) = 1^{st} (b) prefix 2^{nd} (b)) \land 2^{nd} (a) = 1^{st} (b) substr ⟨2^{nd} (b), \|1^{st} (b)\|⟩) \to n \in (0 \dots \|u\|)$
90	84	eqcomd	$⊢ ((((((φ \land a \in (Word A \times Word A)) \land b = ⟨u, n⟩) \land u \in Word A) \land n \in (0 \dots \|u\|)) \land 1^{st} (a) = 1^{st} (b) prefix 2^{nd} (b)) \land 2^{nd} (a) = 1^{st} (b) substr ⟨2^{nd} (b), \|1^{st} (b)\|⟩) \to u = 1^{st} (b)$
91	90	fveq2d	$⊢ ((((((φ \land a \in (Word A \times Word A)) \land b = ⟨u, n⟩) \land u \in Word A) \land n \in (0 \dots \|u\|)) \land 1^{st} (a) = 1^{st} (b) prefix 2^{nd} (b)) \land 2^{nd} (a) = 1^{st} (b) substr ⟨2^{nd} (b), \|1^{st} (b)\|⟩) \to \|u\| = \|1^{st} (b)\|$
92	91	oveq2d	$⊢ ((((((φ \land a \in (Word A \times Word A)) \land b = ⟨u, n⟩) \land u \in Word A) \land n \in (0 \dots \|u\|)) \land 1^{st} (a) = 1^{st} (b) prefix 2^{nd} (b)) \land 2^{nd} (a) = 1^{st} (b) substr ⟨2^{nd} (b), \|1^{st} (b)\|⟩) \to (0 \dots \|u\|) = (0 \dots \|1^{st} (b)\|)$
93	89 92	eleqtrd	$⊢ ((((((φ \land a \in (Word A \times Word A)) \land b = ⟨u, n⟩) \land u \in Word A) \land n \in (0 \dots \|u\|)) \land 1^{st} (a) = 1^{st} (b) prefix 2^{nd} (b)) \land 2^{nd} (a) = 1^{st} (b) substr ⟨2^{nd} (b), \|1^{st} (b)\|⟩) \to n \in (0 \dots \|1^{st} (b)\|)$
94	88 93	eqeltrd	$⊢ ((((((φ \land a \in (Word A \times Word A)) \land b = ⟨u, n⟩) \land u \in Word A) \land n \in (0 \dots \|u\|)) \land 1^{st} (a) = 1^{st} (b) prefix 2^{nd} (b)) \land 2^{nd} (a) = 1^{st} (b) substr ⟨2^{nd} (b), \|1^{st} (b)\|⟩) \to 2^{nd} (b) \in (0 \dots \|1^{st} (b)\|)$
95		pfxcctswrd	$⊢ (1^{st} (b) \in Word A \land 2^{nd} (b) \in (0 \dots \|1^{st} (b)\|)) \to (1^{st} (b) prefix 2^{nd} (b)) ++ (1^{st} (b) substr ⟨2^{nd} (b), \|1^{st} (b)\|⟩) = 1^{st} (b)$
96	86 94 95	syl2anc	$⊢ ((((((φ \land a \in (Word A \times Word A)) \land b = ⟨u, n⟩) \land u \in Word A) \land n \in (0 \dots \|u\|)) \land 1^{st} (a) = 1^{st} (b) prefix 2^{nd} (b)) \land 2^{nd} (a) = 1^{st} (b) substr ⟨2^{nd} (b), \|1^{st} (b)\|⟩) \to (1^{st} (b) prefix 2^{nd} (b)) ++ (1^{st} (b) substr ⟨2^{nd} (b), \|1^{st} (b)\|⟩) = 1^{st} (b)$
97	80 96	eqtr2d	$⊢ ((((((φ \land a \in (Word A \times Word A)) \land b = ⟨u, n⟩) \land u \in Word A) \land n \in (0 \dots \|u\|)) \land 1^{st} (a) = 1^{st} (b) prefix 2^{nd} (b)) \land 2^{nd} (a) = 1^{st} (b) substr ⟨2^{nd} (b), \|1^{st} (b)\|⟩) \to 1^{st} (b) = 1^{st} (a) ++ 2^{nd} (a)$
98	78	fveq2d	$⊢ ((((((φ \land a \in (Word A \times Word A)) \land b = ⟨u, n⟩) \land u \in Word A) \land n \in (0 \dots \|u\|)) \land 1^{st} (a) = 1^{st} (b) prefix 2^{nd} (b)) \land 2^{nd} (a) = 1^{st} (b) substr ⟨2^{nd} (b), \|1^{st} (b)\|⟩) \to \|1^{st} (a)\| = \|1^{st} (b) prefix 2^{nd} (b)\|$
99		pfxlen	$⊢ (1^{st} (b) \in Word A \land 2^{nd} (b) \in (0 \dots \|1^{st} (b)\|)) \to \|1^{st} (b) prefix 2^{nd} (b)\| = 2^{nd} (b)$
100	86 94 99	syl2anc	$⊢ ((((((φ \land a \in (Word A \times Word A)) \land b = ⟨u, n⟩) \land u \in Word A) \land n \in (0 \dots \|u\|)) \land 1^{st} (a) = 1^{st} (b) prefix 2^{nd} (b)) \land 2^{nd} (a) = 1^{st} (b) substr ⟨2^{nd} (b), \|1^{st} (b)\|⟩) \to \|1^{st} (b) prefix 2^{nd} (b)\| = 2^{nd} (b)$
101	98 100	eqtr2d	$⊢ ((((((φ \land a \in (Word A \times Word A)) \land b = ⟨u, n⟩) \land u \in Word A) \land n \in (0 \dots \|u\|)) \land 1^{st} (a) = 1^{st} (b) prefix 2^{nd} (b)) \land 2^{nd} (a) = 1^{st} (b) substr ⟨2^{nd} (b), \|1^{st} (b)\|⟩) \to 2^{nd} (b) = \|1^{st} (a)\|$
102	97 101	jca	$⊢ ((((((φ \land a \in (Word A \times Word A)) \land b = ⟨u, n⟩) \land u \in Word A) \land n \in (0 \dots \|u\|)) \land 1^{st} (a) = 1^{st} (b) prefix 2^{nd} (b)) \land 2^{nd} (a) = 1^{st} (b) substr ⟨2^{nd} (b), \|1^{st} (b)\|⟩) \to (1^{st} (b) = 1^{st} (a) ++ 2^{nd} (a) \land 2^{nd} (b) = \|1^{st} (a)\|)$
103	102	anasss	$⊢ (((((φ \land a \in (Word A \times Word A)) \land b = ⟨u, n⟩) \land u \in Word A) \land n \in (0 \dots \|u\|)) \land (1^{st} (a) = 1^{st} (b) prefix 2^{nd} (b) \land 2^{nd} (a) = 1^{st} (b) substr ⟨2^{nd} (b), \|1^{st} (b)\|⟩)) \to (1^{st} (b) = 1^{st} (a) ++ 2^{nd} (a) \land 2^{nd} (b) = \|1^{st} (a)\|)$
104		simplr	$⊢ ((((((φ \land a \in (Word A \times Word A)) \land b = ⟨u, n⟩) \land u \in Word A) \land n \in (0 \dots \|u\|)) \land 1^{st} (b) = 1^{st} (a) ++ 2^{nd} (a)) \land 2^{nd} (b) = \|1^{st} (a)\|) \to 1^{st} (b) = 1^{st} (a) ++ 2^{nd} (a)$
105		simpr	$⊢ ((((((φ \land a \in (Word A \times Word A)) \land b = ⟨u, n⟩) \land u \in Word A) \land n \in (0 \dots \|u\|)) \land 1^{st} (b) = 1^{st} (a) ++ 2^{nd} (a)) \land 2^{nd} (b) = \|1^{st} (a)\|) \to 2^{nd} (b) = \|1^{st} (a)\|$
106	104 105	oveq12d	$⊢ ((((((φ \land a \in (Word A \times Word A)) \land b = ⟨u, n⟩) \land u \in Word A) \land n \in (0 \dots \|u\|)) \land 1^{st} (b) = 1^{st} (a) ++ 2^{nd} (a)) \land 2^{nd} (b) = \|1^{st} (a)\|) \to 1^{st} (b) prefix 2^{nd} (b) = (1^{st} (a) ++ 2^{nd} (a)) prefix \|1^{st} (a)\|$
107	11	ad5antr	$⊢ ((((((φ \land a \in (Word A \times Word A)) \land b = ⟨u, n⟩) \land u \in Word A) \land n \in (0 \dots \|u\|)) \land 1^{st} (b) = 1^{st} (a) ++ 2^{nd} (a)) \land 2^{nd} (b) = \|1^{st} (a)\|) \to 1^{st} (a) \in Word A$
108	13	ad5antr	$⊢ ((((((φ \land a \in (Word A \times Word A)) \land b = ⟨u, n⟩) \land u \in Word A) \land n \in (0 \dots \|u\|)) \land 1^{st} (b) = 1^{st} (a) ++ 2^{nd} (a)) \land 2^{nd} (b) = \|1^{st} (a)\|) \to 2^{nd} (a) \in Word A$
109		pfxccat1	$⊢ (1^{st} (a) \in Word A \land 2^{nd} (a) \in Word A) \to (1^{st} (a) ++ 2^{nd} (a)) prefix \|1^{st} (a)\| = 1^{st} (a)$
110	107 108 109	syl2anc	$⊢ ((((((φ \land a \in (Word A \times Word A)) \land b = ⟨u, n⟩) \land u \in Word A) \land n \in (0 \dots \|u\|)) \land 1^{st} (b) = 1^{st} (a) ++ 2^{nd} (a)) \land 2^{nd} (b) = \|1^{st} (a)\|) \to (1^{st} (a) ++ 2^{nd} (a)) prefix \|1^{st} (a)\| = 1^{st} (a)$
111	106 110	eqtr2d	$⊢ ((((((φ \land a \in (Word A \times Word A)) \land b = ⟨u, n⟩) \land u \in Word A) \land n \in (0 \dots \|u\|)) \land 1^{st} (b) = 1^{st} (a) ++ 2^{nd} (a)) \land 2^{nd} (b) = \|1^{st} (a)\|) \to 1^{st} (a) = 1^{st} (b) prefix 2^{nd} (b)$
112	104	fveq2d	$⊢ ((((((φ \land a \in (Word A \times Word A)) \land b = ⟨u, n⟩) \land u \in Word A) \land n \in (0 \dots \|u\|)) \land 1^{st} (b) = 1^{st} (a) ++ 2^{nd} (a)) \land 2^{nd} (b) = \|1^{st} (a)\|) \to \|1^{st} (b)\| = \|1^{st} (a) ++ 2^{nd} (a)\|$
113	107 108 34	syl2anc	$⊢ ((((((φ \land a \in (Word A \times Word A)) \land b = ⟨u, n⟩) \land u \in Word A) \land n \in (0 \dots \|u\|)) \land 1^{st} (b) = 1^{st} (a) ++ 2^{nd} (a)) \land 2^{nd} (b) = \|1^{st} (a)\|) \to \|1^{st} (a) ++ 2^{nd} (a)\| = \|1^{st} (a)\| + \|2^{nd} (a)\|$
114	112 113	eqtrd	$⊢ ((((((φ \land a \in (Word A \times Word A)) \land b = ⟨u, n⟩) \land u \in Word A) \land n \in (0 \dots \|u\|)) \land 1^{st} (b) = 1^{st} (a) ++ 2^{nd} (a)) \land 2^{nd} (b) = \|1^{st} (a)\|) \to \|1^{st} (b)\| = \|1^{st} (a)\| + \|2^{nd} (a)\|$
115	105 114	opeq12d	$⊢ ((((((φ \land a \in (Word A \times Word A)) \land b = ⟨u, n⟩) \land u \in Word A) \land n \in (0 \dots \|u\|)) \land 1^{st} (b) = 1^{st} (a) ++ 2^{nd} (a)) \land 2^{nd} (b) = \|1^{st} (a)\|) \to ⟨2^{nd} (b), \|1^{st} (b)\|⟩ = ⟨\|1^{st} (a)\|, \|1^{st} (a)\| + \|2^{nd} (a)\|⟩$
116	104 115	oveq12d	$⊢ ((((((φ \land a \in (Word A \times Word A)) \land b = ⟨u, n⟩) \land u \in Word A) \land n \in (0 \dots \|u\|)) \land 1^{st} (b) = 1^{st} (a) ++ 2^{nd} (a)) \land 2^{nd} (b) = \|1^{st} (a)\|) \to 1^{st} (b) substr ⟨2^{nd} (b), \|1^{st} (b)\|⟩ = (1^{st} (a) ++ 2^{nd} (a)) substr ⟨\|1^{st} (a)\|, \|1^{st} (a)\| + \|2^{nd} (a)\|⟩$
117		swrdccat2	$⊢ (1^{st} (a) \in Word A \land 2^{nd} (a) \in Word A) \to (1^{st} (a) ++ 2^{nd} (a)) substr ⟨\|1^{st} (a)\|, \|1^{st} (a)\| + \|2^{nd} (a)\|⟩ = 2^{nd} (a)$
118	107 108 117	syl2anc	$⊢ ((((((φ \land a \in (Word A \times Word A)) \land b = ⟨u, n⟩) \land u \in Word A) \land n \in (0 \dots \|u\|)) \land 1^{st} (b) = 1^{st} (a) ++ 2^{nd} (a)) \land 2^{nd} (b) = \|1^{st} (a)\|) \to (1^{st} (a) ++ 2^{nd} (a)) substr ⟨\|1^{st} (a)\|, \|1^{st} (a)\| + \|2^{nd} (a)\|⟩ = 2^{nd} (a)$
119	116 118	eqtr2d	$⊢ ((((((φ \land a \in (Word A \times Word A)) \land b = ⟨u, n⟩) \land u \in Word A) \land n \in (0 \dots \|u\|)) \land 1^{st} (b) = 1^{st} (a) ++ 2^{nd} (a)) \land 2^{nd} (b) = \|1^{st} (a)\|) \to 2^{nd} (a) = 1^{st} (b) substr ⟨2^{nd} (b), \|1^{st} (b)\|⟩$
120	111 119	jca	$⊢ ((((((φ \land a \in (Word A \times Word A)) \land b = ⟨u, n⟩) \land u \in Word A) \land n \in (0 \dots \|u\|)) \land 1^{st} (b) = 1^{st} (a) ++ 2^{nd} (a)) \land 2^{nd} (b) = \|1^{st} (a)\|) \to (1^{st} (a) = 1^{st} (b) prefix 2^{nd} (b) \land 2^{nd} (a) = 1^{st} (b) substr ⟨2^{nd} (b), \|1^{st} (b)\|⟩)$
121	120	anasss	$⊢ (((((φ \land a \in (Word A \times Word A)) \land b = ⟨u, n⟩) \land u \in Word A) \land n \in (0 \dots \|u\|)) \land (1^{st} (b) = 1^{st} (a) ++ 2^{nd} (a) \land 2^{nd} (b) = \|1^{st} (a)\|)) \to (1^{st} (a) = 1^{st} (b) prefix 2^{nd} (b) \land 2^{nd} (a) = 1^{st} (b) substr ⟨2^{nd} (b), \|1^{st} (b)\|⟩)$
122	103 121	impbida	$⊢ ((((φ \land a \in (Word A \times Word A)) \land b = ⟨u, n⟩) \land u \in Word A) \land n \in (0 \dots \|u\|)) \to ((1^{st} (a) = 1^{st} (b) prefix 2^{nd} (b) \land 2^{nd} (a) = 1^{st} (b) substr ⟨2^{nd} (b), \|1^{st} (b)\|⟩) \leftrightarrow (1^{st} (b) = 1^{st} (a) ++ 2^{nd} (a) \land 2^{nd} (b) = \|1^{st} (a)\|))$
123	122	anasss	$⊢ (((φ \land a \in (Word A \times Word A)) \land b = ⟨u, n⟩) \land (u \in Word A \land n \in (0 \dots \|u\|))) \to ((1^{st} (a) = 1^{st} (b) prefix 2^{nd} (b) \land 2^{nd} (a) = 1^{st} (b) substr ⟨2^{nd} (b), \|1^{st} (b)\|⟩) \leftrightarrow (1^{st} (b) = 1^{st} (a) ++ 2^{nd} (a) \land 2^{nd} (b) = \|1^{st} (a)\|))$
124	123	expl	$⊢ (φ \land a \in (Word A \times Word A)) \to ((b = ⟨u, n⟩ \land (u \in Word A \land n \in (0 \dots \|u\|))) \to ((1^{st} (a) = 1^{st} (b) prefix 2^{nd} (b) \land 2^{nd} (a) = 1^{st} (b) substr ⟨2^{nd} (b), \|1^{st} (b)\|⟩) \leftrightarrow (1^{st} (b) = 1^{st} (a) ++ 2^{nd} (a) \land 2^{nd} (b) = \|1^{st} (a)\|)))$
125	124	adantlr	$⊢ ((φ \land b \in U) \land a \in (Word A \times Word A)) \to ((b = ⟨u, n⟩ \land (u \in Word A \land n \in (0 \dots \|u\|))) \to ((1^{st} (a) = 1^{st} (b) prefix 2^{nd} (b) \land 2^{nd} (a) = 1^{st} (b) substr ⟨2^{nd} (b), \|1^{st} (b)\|⟩) \leftrightarrow (1^{st} (b) = 1^{st} (a) ++ 2^{nd} (a) \land 2^{nd} (b) = \|1^{st} (a)\|)))$
126	125	exlimdv	$⊢ ((φ \land b \in U) \land a \in (Word A \times Word A)) \to (\exists n (b = ⟨u, n⟩ \land (u \in Word A \land n \in (0 \dots \|u\|))) \to ((1^{st} (a) = 1^{st} (b) prefix 2^{nd} (b) \land 2^{nd} (a) = 1^{st} (b) substr ⟨2^{nd} (b), \|1^{st} (b)\|⟩) \leftrightarrow (1^{st} (b) = 1^{st} (a) ++ 2^{nd} (a) \land 2^{nd} (b) = \|1^{st} (a)\|)))$
127	126	imp	$⊢ (((φ \land b \in U) \land a \in (Word A \times Word A)) \land \exists n (b = ⟨u, n⟩ \land (u \in Word A \land n \in (0 \dots \|u\|)))) \to ((1^{st} (a) = 1^{st} (b) prefix 2^{nd} (b) \land 2^{nd} (a) = 1^{st} (b) substr ⟨2^{nd} (b), \|1^{st} (b)\|⟩) \leftrightarrow (1^{st} (b) = 1^{st} (a) ++ 2^{nd} (a) \land 2^{nd} (b) = \|1^{st} (a)\|))$
128	77 127	exlimddv	$⊢ ((φ \land b \in U) \land a \in (Word A \times Word A)) \to ((1^{st} (a) = 1^{st} (b) prefix 2^{nd} (b) \land 2^{nd} (a) = 1^{st} (b) substr ⟨2^{nd} (b), \|1^{st} (b)\|⟩) \leftrightarrow (1^{st} (b) = 1^{st} (a) ++ 2^{nd} (a) \land 2^{nd} (b) = \|1^{st} (a)\|))$
129		eqop	$⊢ a \in (Word A \times Word A) \to (a = ⟨1^{st} (b) prefix 2^{nd} (b), 1^{st} (b) substr ⟨2^{nd} (b), \|1^{st} (b)\|⟩⟩ \leftrightarrow (1^{st} (a) = 1^{st} (b) prefix 2^{nd} (b) \land 2^{nd} (a) = 1^{st} (b) substr ⟨2^{nd} (b), \|1^{st} (b)\|⟩))$
130	129	adantl	$⊢ ((φ \land b \in U) \land a \in (Word A \times Word A)) \to (a = ⟨1^{st} (b) prefix 2^{nd} (b), 1^{st} (b) substr ⟨2^{nd} (b), \|1^{st} (b)\|⟩⟩ \leftrightarrow (1^{st} (a) = 1^{st} (b) prefix 2^{nd} (b) \land 2^{nd} (a) = 1^{st} (b) substr ⟨2^{nd} (b), \|1^{st} (b)\|⟩))$
131		snssi	$⊢ w \in Word A \to \{w\} \subseteq Word A$
132	131	adantl	$⊢ ((φ \land a \in (Word A \times Word A)) \land w \in Word A) \to \{w\} \subseteq Word A$
133		fz0ssnn0	$⊢ (0 \dots \|w\|) \subseteq ℕ_{0}$
134		xpss12	$⊢ (\{w\} \subseteq Word A \land (0 \dots \|w\|) \subseteq ℕ_{0}) \to \{w\} \times (0 \dots \|w\|) \subseteq Word A \times ℕ_{0}$
135	132 133 134	sylancl	$⊢ ((φ \land a \in (Word A \times Word A)) \land w \in Word A) \to \{w\} \times (0 \dots \|w\|) \subseteq Word A \times ℕ_{0}$
136	135	iunssd	$⊢ (φ \land a \in (Word A \times Word A)) \to ⋃_{w \in Word A} (\{w\} \times (0 \dots \|w\|)) \subseteq Word A \times ℕ_{0}$
137	136	adantlr	$⊢ ((φ \land b \in U) \land a \in (Word A \times Word A)) \to ⋃_{w \in Word A} (\{w\} \times (0 \dots \|w\|)) \subseteq Word A \times ℕ_{0}$
138	137 66	sseldd	$⊢ ((φ \land b \in U) \land a \in (Word A \times Word A)) \to b \in (Word A \times ℕ_{0})$
139		eqop	$⊢ b \in (Word A \times ℕ_{0}) \to (b = ⟨1^{st} (a) ++ 2^{nd} (a), \|1^{st} (a)\|⟩ \leftrightarrow (1^{st} (b) = 1^{st} (a) ++ 2^{nd} (a) \land 2^{nd} (b) = \|1^{st} (a)\|))$
140	138 139	syl	$⊢ ((φ \land b \in U) \land a \in (Word A \times Word A)) \to (b = ⟨1^{st} (a) ++ 2^{nd} (a), \|1^{st} (a)\|⟩ \leftrightarrow (1^{st} (b) = 1^{st} (a) ++ 2^{nd} (a) \land 2^{nd} (b) = \|1^{st} (a)\|))$
141	128 130 140	3bitr4d	$⊢ ((φ \land b \in U) \land a \in (Word A \times Word A)) \to (a = ⟨1^{st} (b) prefix 2^{nd} (b), 1^{st} (b) substr ⟨2^{nd} (b), \|1^{st} (b)\|⟩⟩ \leftrightarrow b = ⟨1^{st} (a) ++ 2^{nd} (a), \|1^{st} (a)\|⟩)$
142	141	an32s	$⊢ ((φ \land a \in (Word A \times Word A)) \land b \in U) \to (a = ⟨1^{st} (b) prefix 2^{nd} (b), 1^{st} (b) substr ⟨2^{nd} (b), \|1^{st} (b)\|⟩⟩ \leftrightarrow b = ⟨1^{st} (a) ++ 2^{nd} (a), \|1^{st} (a)\|⟩)$
143	142	anasss	$⊢ (φ \land (a \in (Word A \times Word A) \land b \in U)) \to (a = ⟨1^{st} (b) prefix 2^{nd} (b), 1^{st} (b) substr ⟨2^{nd} (b), \|1^{st} (b)\|⟩⟩ \leftrightarrow b = ⟨1^{st} (a) ++ 2^{nd} (a), \|1^{st} (a)\|⟩)$
144	2 41 65 143	f1ocnv2d	$⊢ φ \to (F : Word A \times Word A \underset{1-1 onto}{⟶} U \land F^{-1} = (b \in U ⟼ ⟨1^{st} (b) prefix 2^{nd} (b), 1^{st} (b) substr ⟨2^{nd} (b), \|1^{st} (b)\|⟩⟩))$
145	144	simpld	$⊢ φ \to F : Word A \times Word A \underset{1-1 onto}{⟶} U$
146	144	simprd	$⊢ φ \to F^{-1} = (b \in U ⟼ ⟨1^{st} (b) prefix 2^{nd} (b), 1^{st} (b) substr ⟨2^{nd} (b), \|1^{st} (b)\|⟩⟩)$
147	146 3	eqtr4di	$⊢ φ \to F^{-1} = G$
148	145 147	jca	$⊢ φ \to (F : Word A \times Word A \underset{1-1 onto}{⟶} U \land F^{-1} = G)$

Metamath Proof Explorer

Theorem gsumwrd2dccatlem

Proof