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	biimpi	$⊢ b \in U \to b \in ⋃_{w \in Word A} (\{w\} \times (0 \dots \|w\|))$
51	50	adantl	$⊢ (φ \land b \in U) \to b \in ⋃_{w \in Word A} (\{w\} \times (0 \dots \|w\|))$
52		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\|))$
53	51 52	sylib	$⊢ (φ \land b \in U) \to \exists w \in Word A b \in (\{w\} \times (0 \dots \|w\|))$
54		sneq	$⊢ u = w \to \{u\} = \{w\}$
55		fveq2	$⊢ u = w \to \|u\| = \|w\|$
56	55	oveq2d	$⊢ u = w \to (0 \dots \|u\|) = (0 \dots \|w\|)$
57	54 56	xpeq12d	$⊢ u = w \to \{u\} \times (0 \dots \|u\|) = \{w\} \times (0 \dots \|w\|)$
58	57	eleq2d	$⊢ u = w \to (b \in (\{u\} \times (0 \dots \|u\|)) \leftrightarrow b \in (\{w\} \times (0 \dots \|w\|)))$
59	58	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\|))$
60	53 59	sylibr	$⊢ (φ \land b \in U) \to \exists u \in Word A b \in (\{u\} \times (0 \dots \|u\|))$
61	48 60	r19.29a	$⊢ (φ \land b \in U) \to 1^{st} (b) \in Word A$
62		pfxcl	$⊢ 1^{st} (b) \in Word A \to 1^{st} (b) prefix 2^{nd} (b) \in Word A$
63	61 62	syl	$⊢ (φ \land b \in U) \to 1^{st} (b) prefix 2^{nd} (b) \in Word A$
64		swrdcl	$⊢ 1^{st} (b) \in Word A \to 1^{st} (b) substr ⟨2^{nd} (b), \|1^{st} (b)\|⟩ \in Word A$
65	61 64	syl	$⊢ (φ \land b \in U) \to 1^{st} (b) substr ⟨2^{nd} (b), \|1^{st} (b)\|⟩ \in Word A$
66	63 65	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)$
67	51	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\|))$
68		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\|)))$
69	67 68	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\|)))$
70		opeq1	$⊢ u = w \to ⟨u, n⟩ = ⟨w, n⟩$
71	70	eqeq2d	$⊢ u = w \to (b = ⟨u, n⟩ \leftrightarrow b = ⟨w, n⟩)$
72		eleq1w	$⊢ u = w \to (u \in Word A \leftrightarrow w \in Word A)$
73	56	eleq2d	$⊢ u = w \to (n \in (0 \dots \|u\|) \leftrightarrow n \in (0 \dots \|w\|))$
74	72 73	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\|)))$
75	71 74	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\|))))$
76	75	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\|))))$
77	76	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\|)))$
78	69 77	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\|)))$
79		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)$
80		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)\|⟩$
81	79 80	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)\|⟩)$
82		vex	$⊢ u \in V$
83		vex	$⊢ n \in V$
84	82 83	op1std	$⊢ b = ⟨u, n⟩ \to 1^{st} (b) = u$
85	84	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$
86		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$
87	85 86	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$
88	82 83	op2ndd	$⊢ b = ⟨u, n⟩ \to 2^{nd} (b) = n$
89	88	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$
90		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\|)$
91	85	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)$
92	91	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)\|$
93	92	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)\|)$
94	90 93	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)\|)$
95	89 94	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)\|)$
96		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)$
97	87 95 96	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)$
98	81 97	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)$
99	79	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)\|$
100		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)$
101	87 95 100	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)$
102	99 101	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)\|$
103	98 102	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)\|)$
104	103	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)\|)$
105		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)$
106		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)\|$
107	105 106	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)\|$
108	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$
109	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$
110		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)$
111	108 109 110	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)$
112	107 111	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)$
113	105	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)\|$
114	108 109 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)\|$
115	113 114	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)\|$
116	106 115	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)\|⟩$
117	105 116	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)\|⟩$
118		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)$
119	108 109 118	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)$
120	117 119	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)\|⟩$
121	112 120	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)\|⟩)$
122	121	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)\|⟩)$
123	104 122	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)\|))$
124	123	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)\|))$
125	124	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)\|)))$
126	125	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)\|)))$
127	126	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)\|)))$
128	127	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)\|))$
129	78 128	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)\|))$
130		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)\|⟩))$
131	130	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)\|⟩))$
132		snssi	$⊢ w \in Word A \to \{w\} \subseteq Word A$
133	132	adantl	$⊢ ((φ \land a \in (Word A \times Word A)) \land w \in Word A) \to \{w\} \subseteq Word A$
134		fz0ssnn0	$⊢ (0 \dots \|w\|) \subseteq ℕ_{0}$
135		xpss12	$⊢ (\{w\} \subseteq Word A \land (0 \dots \|w\|) \subseteq ℕ_{0}) \to \{w\} \times (0 \dots \|w\|) \subseteq Word A \times ℕ_{0}$
136	133 134 135	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}$
137	136	iunssd	$⊢ (φ \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	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}$
139	138 67	sseldd	$⊢ ((φ \land b \in U) \land a \in (Word A \times Word A)) \to b \in (Word A \times ℕ_{0})$
140		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)\|))$
141	139 140	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)\|))$
142	129 131 141	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)\|⟩)$
143	142	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)\|⟩)$
144	143	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)\|⟩)$
145	2 41 66 144	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)\|⟩⟩))$
146	145	simpld	$⊢ φ \to F : Word A \times Word A \underset{1-1 onto}{⟶} U$
147	145	simprd	$⊢ φ \to F^{-1} = (b \in U ⟼ ⟨1^{st} (b) prefix 2^{nd} (b), 1^{st} (b) substr ⟨2^{nd} (b), \|1^{st} (b)\|⟩⟩)$
148	147 3	eqtr4di	$⊢ φ \to F^{-1} = G$
149	146 148	jca	$⊢ φ \to (F : Word A \times Word A \underset{1-1 onto}{⟶} U \land F^{-1} = G)$

Metamath Proof Explorer

Theorem gsumwrd2dccatlem

Proof