gsumwrd2dccatlem - Mathbox for Thierry Arnoux

	Mathbox for Thierry Arnoux		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > gsumwrd2dccatlem		Structured version Visualization version GIF version

Theorem gsumwrd2dccatlem 33046

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

**Hypotheses**
Ref	Expression
gsumwrd2dccatlem.u	⊢ 𝑈 = ∪ 𝑤 ∈ Word 𝐴({𝑤} × (0...(♯‘𝑤)))
gsumwrd2dccatlem.f	⊢ 𝐹 = (𝑎 ∈ (Word 𝐴 × Word 𝐴) ↦ ⟨((1^st ‘𝑎) ++ (2^nd ‘𝑎)), (♯‘(1^st ‘𝑎))⟩)
gsumwrd2dccatlem.g	⊢ 𝐺 = (𝑏 ∈ 𝑈 ↦ ⟨((1^st ‘𝑏) prefix (2^nd ‘𝑏)), ((1^st ‘𝑏) substr ⟨(2^nd ‘𝑏), (♯‘(1^st ‘𝑏))⟩)⟩)
gsumwrd2dccatlem.a	⊢ (𝜑 → 𝐴 ∈ 𝑉)

**Assertion**
Ref	Expression
gsumwrd2dccatlem	⊢ (𝜑 → (𝐹:(Word 𝐴 × Word 𝐴)–1-1-onto→𝑈 ∧ ^◡𝐹 = 𝐺))

Distinct variable groups: 𝐴,𝑎,𝑏,𝑤 𝐹,𝑏 𝑈,𝑎,𝑏 𝜑,𝑎,𝑏,𝑤 Allowed substitution hints: 𝑈(𝑤) 𝐹(𝑤,𝑎) 𝐺(𝑤,𝑎,𝑏) 𝑉(𝑤,𝑎,𝑏)

Proof of Theorem gsumwrd2dccatlem Dummy variables 𝑛 𝑢 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		gsumwrd2dccatlem.f	. . . 4 ⊢ 𝐹 = (𝑎 ∈ (Word 𝐴 × Word 𝐴) ↦ ⟨((1^st ‘𝑎) ++ (2^nd ‘𝑎)), (♯‘(1^st ‘𝑎))⟩)
2		sneq 4583	. . . . . . . . 9 ⊢ (𝑤 = ((1^st ‘𝑎) ++ (2^nd ‘𝑎)) → {𝑤} = {((1^st ‘𝑎) ++ (2^nd ‘𝑎))})
3		fveq2 6822	. . . . . . . . . 10 ⊢ (𝑤 = ((1^st ‘𝑎) ++ (2^nd ‘𝑎)) → (♯‘𝑤) = (♯‘((1^st ‘𝑎) ++ (2^nd ‘𝑎))))
4	3	oveq2d 7362	. . . . . . . . 9 ⊢ (𝑤 = ((1^st ‘𝑎) ++ (2^nd ‘𝑎)) → (0...(♯‘𝑤)) = (0...(♯‘((1^st ‘𝑎) ++ (2^nd ‘𝑎)))))
5	2, 4	xpeq12d 5645	. . . . . . . 8 ⊢ (𝑤 = ((1^st ‘𝑎) ++ (2^nd ‘𝑎)) → ({𝑤} × (0...(♯‘𝑤))) = ({((1^st ‘𝑎) ++ (2^nd ‘𝑎))} × (0...(♯‘((1^st ‘𝑎) ++ (2^nd ‘𝑎))))))
6	5	eleq2d 2817	. . . . . . 7 ⊢ (𝑤 = ((1^st ‘𝑎) ++ (2^nd ‘𝑎)) → (⟨((1^st ‘𝑎) ++ (2^nd ‘𝑎)), (♯‘(1^st ‘𝑎))⟩ ∈ ({𝑤} × (0...(♯‘𝑤))) ↔ ⟨((1^st ‘𝑎) ++ (2^nd ‘𝑎)), (♯‘(1^st ‘𝑎))⟩ ∈ ({((1^st ‘𝑎) ++ (2^nd ‘𝑎))} × (0...(♯‘((1^st ‘𝑎) ++ (2^nd ‘𝑎)))))))
7		xp1st 7953	. . . . . . . . 9 ⊢ (𝑎 ∈ (Word 𝐴 × Word 𝐴) → (1^st ‘𝑎) ∈ Word 𝐴)
8	7	adantl 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (1^st ‘𝑎) ∈ Word 𝐴)
9		xp2nd 7954	. . . . . . . . 9 ⊢ (𝑎 ∈ (Word 𝐴 × Word 𝐴) → (2^nd ‘𝑎) ∈ Word 𝐴)
10	9	adantl 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (2^nd ‘𝑎) ∈ Word 𝐴)
11		ccatcl 14481	. . . . . . . 8 ⊢ (((1^st ‘𝑎) ∈ Word 𝐴 ∧ (2^nd ‘𝑎) ∈ Word 𝐴) → ((1^st ‘𝑎) ++ (2^nd ‘𝑎)) ∈ Word 𝐴)
12	8, 10, 11	syl2anc 584	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → ((1^st ‘𝑎) ++ (2^nd ‘𝑎)) ∈ Word 𝐴)
13		ovex 7379	. . . . . . . . . 10 ⊢ ((1^st ‘𝑎) ++ (2^nd ‘𝑎)) ∈ V
14	13	snid 4612	. . . . . . . . 9 ⊢ ((1^st ‘𝑎) ++ (2^nd ‘𝑎)) ∈ {((1^st ‘𝑎) ++ (2^nd ‘𝑎))}
15	14	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → ((1^st ‘𝑎) ++ (2^nd ‘𝑎)) ∈ {((1^st ‘𝑎) ++ (2^nd ‘𝑎))})
16		0zd 12480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → 0 ∈ ℤ)
17		lencl 14440	. . . . . . . . . . 11 ⊢ (((1^st ‘𝑎) ++ (2^nd ‘𝑎)) ∈ Word 𝐴 → (♯‘((1^st ‘𝑎) ++ (2^nd ‘𝑎))) ∈ ℕ₀)
18	12, 17	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (♯‘((1^st ‘𝑎) ++ (2^nd ‘𝑎))) ∈ ℕ₀)
19	18	nn0zd 12494	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (♯‘((1^st ‘𝑎) ++ (2^nd ‘𝑎))) ∈ ℤ)
20		lencl 14440	. . . . . . . . . . 11 ⊢ ((1^st ‘𝑎) ∈ Word 𝐴 → (♯‘(1^st ‘𝑎)) ∈ ℕ₀)
21	8, 20	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (♯‘(1^st ‘𝑎)) ∈ ℕ₀)
22	21	nn0zd 12494	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (♯‘(1^st ‘𝑎)) ∈ ℤ)
23	21	nn0ge0d 12445	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → 0 ≤ (♯‘(1^st ‘𝑎)))
24		lencl 14440	. . . . . . . . . . . . 13 ⊢ ((2^nd ‘𝑎) ∈ Word 𝐴 → (♯‘(2^nd ‘𝑎)) ∈ ℕ₀)
25	10, 24	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (♯‘(2^nd ‘𝑎)) ∈ ℕ₀)
26	25	nn0ge0d 12445	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → 0 ≤ (♯‘(2^nd ‘𝑎)))
27	21	nn0red 12443	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (♯‘(1^st ‘𝑎)) ∈ ℝ)
28	25	nn0red 12443	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (♯‘(2^nd ‘𝑎)) ∈ ℝ)
29	27, 28	addge01d 11705	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (0 ≤ (♯‘(2^nd ‘𝑎)) ↔ (♯‘(1^st ‘𝑎)) ≤ ((♯‘(1^st ‘𝑎)) + (♯‘(2^nd ‘𝑎)))))
30	26, 29	mpbid 232	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (♯‘(1^st ‘𝑎)) ≤ ((♯‘(1^st ‘𝑎)) + (♯‘(2^nd ‘𝑎))))
31		ccatlen 14482	. . . . . . . . . . 11 ⊢ (((1^st ‘𝑎) ∈ Word 𝐴 ∧ (2^nd ‘𝑎) ∈ Word 𝐴) → (♯‘((1^st ‘𝑎) ++ (2^nd ‘𝑎))) = ((♯‘(1^st ‘𝑎)) + (♯‘(2^nd ‘𝑎))))
32	8, 10, 31	syl2anc 584	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (♯‘((1^st ‘𝑎) ++ (2^nd ‘𝑎))) = ((♯‘(1^st ‘𝑎)) + (♯‘(2^nd ‘𝑎))))
33	30, 32	breqtrrd 5117	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (♯‘(1^st ‘𝑎)) ≤ (♯‘((1^st ‘𝑎) ++ (2^nd ‘𝑎))))
34	16, 19, 22, 23, 33	elfzd 13415	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (♯‘(1^st ‘𝑎)) ∈ (0...(♯‘((1^st ‘𝑎) ++ (2^nd ‘𝑎)))))
35	15, 34	opelxpd 5653	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → ⟨((1^st ‘𝑎) ++ (2^nd ‘𝑎)), (♯‘(1^st ‘𝑎))⟩ ∈ ({((1^st ‘𝑎) ++ (2^nd ‘𝑎))} × (0...(♯‘((1^st ‘𝑎) ++ (2^nd ‘𝑎))))))
36	6, 12, 35	rspcedvdw 3575	. . . . . 6 ⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → ∃𝑤 ∈ Word 𝐴⟨((1^st ‘𝑎) ++ (2^nd ‘𝑎)), (♯‘(1^st ‘𝑎))⟩ ∈ ({𝑤} × (0...(♯‘𝑤))))
37	36	eliund 4946	. . . . 5 ⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → ⟨((1^st ‘𝑎) ++ (2^nd ‘𝑎)), (♯‘(1^st ‘𝑎))⟩ ∈ ∪ 𝑤 ∈ Word 𝐴({𝑤} × (0...(♯‘𝑤))))
38		gsumwrd2dccatlem.u	. . . . 5 ⊢ 𝑈 = ∪ 𝑤 ∈ Word 𝐴({𝑤} × (0...(♯‘𝑤)))
39	37, 38	eleqtrrdi 2842	. . . 4 ⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → ⟨((1^st ‘𝑎) ++ (2^nd ‘𝑎)), (♯‘(1^st ‘𝑎))⟩ ∈ 𝑈)
40		simpr 484	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑏 ∈ ({𝑢} × (0...(♯‘𝑢)))) → 𝑏 ∈ ({𝑢} × (0...(♯‘𝑢))))
41		xp1st 7953	. . . . . . . . . 10 ⊢ (𝑏 ∈ ({𝑢} × (0...(♯‘𝑢))) → (1^st ‘𝑏) ∈ {𝑢})
42		elsni 4590	. . . . . . . . . 10 ⊢ ((1^st ‘𝑏) ∈ {𝑢} → (1^st ‘𝑏) = 𝑢)
43	40, 41, 42	3syl 18	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑏 ∈ ({𝑢} × (0...(♯‘𝑢)))) → (1^st ‘𝑏) = 𝑢)
44		simplr 768	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑏 ∈ ({𝑢} × (0...(♯‘𝑢)))) → 𝑢 ∈ Word 𝐴)
45	43, 44	eqeltrd 2831	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑏 ∈ ({𝑢} × (0...(♯‘𝑢)))) → (1^st ‘𝑏) ∈ Word 𝐴)
46	45	adantllr 719	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑏 ∈ ({𝑢} × (0...(♯‘𝑢)))) → (1^st ‘𝑏) ∈ Word 𝐴)
47	38	eleq2i 2823	. . . . . . . . . . 11 ⊢ (𝑏 ∈ 𝑈 ↔ 𝑏 ∈ ∪ 𝑤 ∈ Word 𝐴({𝑤} × (0...(♯‘𝑤))))
48	47	biimpi 216	. . . . . . . . . 10 ⊢ (𝑏 ∈ 𝑈 → 𝑏 ∈ ∪ 𝑤 ∈ Word 𝐴({𝑤} × (0...(♯‘𝑤))))
49	48	adantl 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝑈) → 𝑏 ∈ ∪ 𝑤 ∈ Word 𝐴({𝑤} × (0...(♯‘𝑤))))
50		eliun 4943	. . . . . . . . 9 ⊢ (𝑏 ∈ ∪ 𝑤 ∈ Word 𝐴({𝑤} × (0...(♯‘𝑤))) ↔ ∃𝑤 ∈ Word 𝐴𝑏 ∈ ({𝑤} × (0...(♯‘𝑤))))
51	49, 50	sylib 218	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝑈) → ∃𝑤 ∈ Word 𝐴𝑏 ∈ ({𝑤} × (0...(♯‘𝑤))))
52		sneq 4583	. . . . . . . . . . 11 ⊢ (𝑢 = 𝑤 → {𝑢} = {𝑤})
53		fveq2 6822	. . . . . . . . . . . 12 ⊢ (𝑢 = 𝑤 → (♯‘𝑢) = (♯‘𝑤))
54	53	oveq2d 7362	. . . . . . . . . . 11 ⊢ (𝑢 = 𝑤 → (0...(♯‘𝑢)) = (0...(♯‘𝑤)))
55	52, 54	xpeq12d 5645	. . . . . . . . . 10 ⊢ (𝑢 = 𝑤 → ({𝑢} × (0...(♯‘𝑢))) = ({𝑤} × (0...(♯‘𝑤))))
56	55	eleq2d 2817	. . . . . . . . 9 ⊢ (𝑢 = 𝑤 → (𝑏 ∈ ({𝑢} × (0...(♯‘𝑢))) ↔ 𝑏 ∈ ({𝑤} × (0...(♯‘𝑤)))))
57	56	cbvrexvw 3211	. . . . . . . 8 ⊢ (∃𝑢 ∈ Word 𝐴𝑏 ∈ ({𝑢} × (0...(♯‘𝑢))) ↔ ∃𝑤 ∈ Word 𝐴𝑏 ∈ ({𝑤} × (0...(♯‘𝑤))))
58	51, 57	sylibr 234	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝑈) → ∃𝑢 ∈ Word 𝐴𝑏 ∈ ({𝑢} × (0...(♯‘𝑢))))
59	46, 58	r19.29a 3140	. . . . . 6 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝑈) → (1^st ‘𝑏) ∈ Word 𝐴)
60		pfxcl 14585	. . . . . 6 ⊢ ((1^st ‘𝑏) ∈ Word 𝐴 → ((1^st ‘𝑏) prefix (2^nd ‘𝑏)) ∈ Word 𝐴)
61	59, 60	syl 17	. . . . 5 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝑈) → ((1^st ‘𝑏) prefix (2^nd ‘𝑏)) ∈ Word 𝐴)
62		swrdcl 14553	. . . . . 6 ⊢ ((1^st ‘𝑏) ∈ Word 𝐴 → ((1^st ‘𝑏) substr ⟨(2^nd ‘𝑏), (♯‘(1^st ‘𝑏))⟩) ∈ Word 𝐴)
63	59, 62	syl 17	. . . . 5 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝑈) → ((1^st ‘𝑏) substr ⟨(2^nd ‘𝑏), (♯‘(1^st ‘𝑏))⟩) ∈ Word 𝐴)
64	61, 63	opelxpd 5653	. . . 4 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝑈) → ⟨((1^st ‘𝑏) prefix (2^nd ‘𝑏)), ((1^st ‘𝑏) substr ⟨(2^nd ‘𝑏), (♯‘(1^st ‘𝑏))⟩)⟩ ∈ (Word 𝐴 × Word 𝐴))
65	49	adantr 480	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → 𝑏 ∈ ∪ 𝑤 ∈ Word 𝐴({𝑤} × (0...(♯‘𝑤))))
66		eliunxp 5776	. . . . . . . . . 10 ⊢ (𝑏 ∈ ∪ 𝑤 ∈ Word 𝐴({𝑤} × (0...(♯‘𝑤))) ↔ ∃𝑤∃𝑛(𝑏 = ⟨𝑤, 𝑛⟩ ∧ (𝑤 ∈ Word 𝐴 ∧ 𝑛 ∈ (0...(♯‘𝑤)))))
67	65, 66	sylib 218	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → ∃𝑤∃𝑛(𝑏 = ⟨𝑤, 𝑛⟩ ∧ (𝑤 ∈ Word 𝐴 ∧ 𝑛 ∈ (0...(♯‘𝑤)))))
68		opeq1 4822	. . . . . . . . . . . . 13 ⊢ (𝑢 = 𝑤 → ⟨𝑢, 𝑛⟩ = ⟨𝑤, 𝑛⟩)
69	68	eqeq2d 2742	. . . . . . . . . . . 12 ⊢ (𝑢 = 𝑤 → (𝑏 = ⟨𝑢, 𝑛⟩ ↔ 𝑏 = ⟨𝑤, 𝑛⟩))
70		eleq1w 2814	. . . . . . . . . . . . 13 ⊢ (𝑢 = 𝑤 → (𝑢 ∈ Word 𝐴 ↔ 𝑤 ∈ Word 𝐴))
71	54	eleq2d 2817	. . . . . . . . . . . . 13 ⊢ (𝑢 = 𝑤 → (𝑛 ∈ (0...(♯‘𝑢)) ↔ 𝑛 ∈ (0...(♯‘𝑤))))
72	70, 71	anbi12d 632	. . . . . . . . . . . 12 ⊢ (𝑢 = 𝑤 → ((𝑢 ∈ Word 𝐴 ∧ 𝑛 ∈ (0...(♯‘𝑢))) ↔ (𝑤 ∈ Word 𝐴 ∧ 𝑛 ∈ (0...(♯‘𝑤)))))
73	69, 72	anbi12d 632	. . . . . . . . . . 11 ⊢ (𝑢 = 𝑤 → ((𝑏 = ⟨𝑢, 𝑛⟩ ∧ (𝑢 ∈ Word 𝐴 ∧ 𝑛 ∈ (0...(♯‘𝑢)))) ↔ (𝑏 = ⟨𝑤, 𝑛⟩ ∧ (𝑤 ∈ Word 𝐴 ∧ 𝑛 ∈ (0...(♯‘𝑤))))))
74	73	exbidv 1922	. . . . . . . . . 10 ⊢ (𝑢 = 𝑤 → (∃𝑛(𝑏 = ⟨𝑢, 𝑛⟩ ∧ (𝑢 ∈ Word 𝐴 ∧ 𝑛 ∈ (0...(♯‘𝑢)))) ↔ ∃𝑛(𝑏 = ⟨𝑤, 𝑛⟩ ∧ (𝑤 ∈ Word 𝐴 ∧ 𝑛 ∈ (0...(♯‘𝑤))))))
75	74	cbvexvw 2038	. . . . . . . . 9 ⊢ (∃𝑢∃𝑛(𝑏 = ⟨𝑢, 𝑛⟩ ∧ (𝑢 ∈ Word 𝐴 ∧ 𝑛 ∈ (0...(♯‘𝑢)))) ↔ ∃𝑤∃𝑛(𝑏 = ⟨𝑤, 𝑛⟩ ∧ (𝑤 ∈ Word 𝐴 ∧ 𝑛 ∈ (0...(♯‘𝑤)))))
76	67, 75	sylibr 234	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → ∃𝑢∃𝑛(𝑏 = ⟨𝑢, 𝑛⟩ ∧ (𝑢 ∈ Word 𝐴 ∧ 𝑛 ∈ (0...(♯‘𝑢)))))
77		simplr 768	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) ∧ 𝑏 = ⟨𝑢, 𝑛⟩) ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑛 ∈ (0...(♯‘𝑢))) ∧ (1^st ‘𝑎) = ((1^st ‘𝑏) prefix (2^nd ‘𝑏))) ∧ (2^nd ‘𝑎) = ((1^st ‘𝑏) substr ⟨(2^nd ‘𝑏), (♯‘(1^st ‘𝑏))⟩)) → (1^st ‘𝑎) = ((1^st ‘𝑏) prefix (2^nd ‘𝑏)))
78		simpr 484	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) ∧ 𝑏 = ⟨𝑢, 𝑛⟩) ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑛 ∈ (0...(♯‘𝑢))) ∧ (1^st ‘𝑎) = ((1^st ‘𝑏) prefix (2^nd ‘𝑏))) ∧ (2^nd ‘𝑎) = ((1^st ‘𝑏) substr ⟨(2^nd ‘𝑏), (♯‘(1^st ‘𝑏))⟩)) → (2^nd ‘𝑎) = ((1^st ‘𝑏) substr ⟨(2^nd ‘𝑏), (♯‘(1^st ‘𝑏))⟩))
79	77, 78	oveq12d 7364	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) ∧ 𝑏 = ⟨𝑢, 𝑛⟩) ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑛 ∈ (0...(♯‘𝑢))) ∧ (1^st ‘𝑎) = ((1^st ‘𝑏) prefix (2^nd ‘𝑏))) ∧ (2^nd ‘𝑎) = ((1^st ‘𝑏) substr ⟨(2^nd ‘𝑏), (♯‘(1^st ‘𝑏))⟩)) → ((1^st ‘𝑎) ++ (2^nd ‘𝑎)) = (((1^st ‘𝑏) prefix (2^nd ‘𝑏)) ++ ((1^st ‘𝑏) substr ⟨(2^nd ‘𝑏), (♯‘(1^st ‘𝑏))⟩)))
80		vex 3440	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑢 ∈ V
81		vex 3440	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑛 ∈ V
82	80, 81	op1std 7931	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑏 = ⟨𝑢, 𝑛⟩ → (1^st ‘𝑏) = 𝑢)
83	82	ad5antlr 735	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) ∧ 𝑏 = ⟨𝑢, 𝑛⟩) ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑛 ∈ (0...(♯‘𝑢))) ∧ (1^st ‘𝑎) = ((1^st ‘𝑏) prefix (2^nd ‘𝑏))) ∧ (2^nd ‘𝑎) = ((1^st ‘𝑏) substr ⟨(2^nd ‘𝑏), (♯‘(1^st ‘𝑏))⟩)) → (1^st ‘𝑏) = 𝑢)
84		simp-4r 783	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) ∧ 𝑏 = ⟨𝑢, 𝑛⟩) ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑛 ∈ (0...(♯‘𝑢))) ∧ (1^st ‘𝑎) = ((1^st ‘𝑏) prefix (2^nd ‘𝑏))) ∧ (2^nd ‘𝑎) = ((1^st ‘𝑏) substr ⟨(2^nd ‘𝑏), (♯‘(1^st ‘𝑏))⟩)) → 𝑢 ∈ Word 𝐴)
85	83, 84	eqeltrd 2831	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) ∧ 𝑏 = ⟨𝑢, 𝑛⟩) ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑛 ∈ (0...(♯‘𝑢))) ∧ (1^st ‘𝑎) = ((1^st ‘𝑏) prefix (2^nd ‘𝑏))) ∧ (2^nd ‘𝑎) = ((1^st ‘𝑏) substr ⟨(2^nd ‘𝑏), (♯‘(1^st ‘𝑏))⟩)) → (1^st ‘𝑏) ∈ Word 𝐴)
86	80, 81	op2ndd 7932	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑏 = ⟨𝑢, 𝑛⟩ → (2^nd ‘𝑏) = 𝑛)
87	86	ad5antlr 735	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) ∧ 𝑏 = ⟨𝑢, 𝑛⟩) ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑛 ∈ (0...(♯‘𝑢))) ∧ (1^st ‘𝑎) = ((1^st ‘𝑏) prefix (2^nd ‘𝑏))) ∧ (2^nd ‘𝑎) = ((1^st ‘𝑏) substr ⟨(2^nd ‘𝑏), (♯‘(1^st ‘𝑏))⟩)) → (2^nd ‘𝑏) = 𝑛)
88		simpllr 775	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) ∧ 𝑏 = ⟨𝑢, 𝑛⟩) ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑛 ∈ (0...(♯‘𝑢))) ∧ (1^st ‘𝑎) = ((1^st ‘𝑏) prefix (2^nd ‘𝑏))) ∧ (2^nd ‘𝑎) = ((1^st ‘𝑏) substr ⟨(2^nd ‘𝑏), (♯‘(1^st ‘𝑏))⟩)) → 𝑛 ∈ (0...(♯‘𝑢)))
89	83	eqcomd 2737	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) ∧ 𝑏 = ⟨𝑢, 𝑛⟩) ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑛 ∈ (0...(♯‘𝑢))) ∧ (1^st ‘𝑎) = ((1^st ‘𝑏) prefix (2^nd ‘𝑏))) ∧ (2^nd ‘𝑎) = ((1^st ‘𝑏) substr ⟨(2^nd ‘𝑏), (♯‘(1^st ‘𝑏))⟩)) → 𝑢 = (1^st ‘𝑏))
90	89	fveq2d 6826	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) ∧ 𝑏 = ⟨𝑢, 𝑛⟩) ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑛 ∈ (0...(♯‘𝑢))) ∧ (1^st ‘𝑎) = ((1^st ‘𝑏) prefix (2^nd ‘𝑏))) ∧ (2^nd ‘𝑎) = ((1^st ‘𝑏) substr ⟨(2^nd ‘𝑏), (♯‘(1^st ‘𝑏))⟩)) → (♯‘𝑢) = (♯‘(1^st ‘𝑏)))
91	90	oveq2d 7362	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) ∧ 𝑏 = ⟨𝑢, 𝑛⟩) ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑛 ∈ (0...(♯‘𝑢))) ∧ (1^st ‘𝑎) = ((1^st ‘𝑏) prefix (2^nd ‘𝑏))) ∧ (2^nd ‘𝑎) = ((1^st ‘𝑏) substr ⟨(2^nd ‘𝑏), (♯‘(1^st ‘𝑏))⟩)) → (0...(♯‘𝑢)) = (0...(♯‘(1^st ‘𝑏))))
92	88, 91	eleqtrd 2833	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) ∧ 𝑏 = ⟨𝑢, 𝑛⟩) ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑛 ∈ (0...(♯‘𝑢))) ∧ (1^st ‘𝑎) = ((1^st ‘𝑏) prefix (2^nd ‘𝑏))) ∧ (2^nd ‘𝑎) = ((1^st ‘𝑏) substr ⟨(2^nd ‘𝑏), (♯‘(1^st ‘𝑏))⟩)) → 𝑛 ∈ (0...(♯‘(1^st ‘𝑏))))
93	87, 92	eqeltrd 2831	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) ∧ 𝑏 = ⟨𝑢, 𝑛⟩) ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑛 ∈ (0...(♯‘𝑢))) ∧ (1^st ‘𝑎) = ((1^st ‘𝑏) prefix (2^nd ‘𝑏))) ∧ (2^nd ‘𝑎) = ((1^st ‘𝑏) substr ⟨(2^nd ‘𝑏), (♯‘(1^st ‘𝑏))⟩)) → (2^nd ‘𝑏) ∈ (0...(♯‘(1^st ‘𝑏))))
94		pfxcctswrd 14617	. . . . . . . . . . . . . . . . . 18 ⊢ (((1^st ‘𝑏) ∈ Word 𝐴 ∧ (2^nd ‘𝑏) ∈ (0...(♯‘(1^st ‘𝑏)))) → (((1^st ‘𝑏) prefix (2^nd ‘𝑏)) ++ ((1^st ‘𝑏) substr ⟨(2^nd ‘𝑏), (♯‘(1^st ‘𝑏))⟩)) = (1^st ‘𝑏))
95	85, 93, 94	syl2anc 584	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) ∧ 𝑏 = ⟨𝑢, 𝑛⟩) ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑛 ∈ (0...(♯‘𝑢))) ∧ (1^st ‘𝑎) = ((1^st ‘𝑏) prefix (2^nd ‘𝑏))) ∧ (2^nd ‘𝑎) = ((1^st ‘𝑏) substr ⟨(2^nd ‘𝑏), (♯‘(1^st ‘𝑏))⟩)) → (((1^st ‘𝑏) prefix (2^nd ‘𝑏)) ++ ((1^st ‘𝑏) substr ⟨(2^nd ‘𝑏), (♯‘(1^st ‘𝑏))⟩)) = (1^st ‘𝑏))
96	79, 95	eqtr2d 2767	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) ∧ 𝑏 = ⟨𝑢, 𝑛⟩) ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑛 ∈ (0...(♯‘𝑢))) ∧ (1^st ‘𝑎) = ((1^st ‘𝑏) prefix (2^nd ‘𝑏))) ∧ (2^nd ‘𝑎) = ((1^st ‘𝑏) substr ⟨(2^nd ‘𝑏), (♯‘(1^st ‘𝑏))⟩)) → (1^st ‘𝑏) = ((1^st ‘𝑎) ++ (2^nd ‘𝑎)))
97	77	fveq2d 6826	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) ∧ 𝑏 = ⟨𝑢, 𝑛⟩) ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑛 ∈ (0...(♯‘𝑢))) ∧ (1^st ‘𝑎) = ((1^st ‘𝑏) prefix (2^nd ‘𝑏))) ∧ (2^nd ‘𝑎) = ((1^st ‘𝑏) substr ⟨(2^nd ‘𝑏), (♯‘(1^st ‘𝑏))⟩)) → (♯‘(1^st ‘𝑎)) = (♯‘((1^st ‘𝑏) prefix (2^nd ‘𝑏))))
98		pfxlen 14591	. . . . . . . . . . . . . . . . . 18 ⊢ (((1^st ‘𝑏) ∈ Word 𝐴 ∧ (2^nd ‘𝑏) ∈ (0...(♯‘(1^st ‘𝑏)))) → (♯‘((1^st ‘𝑏) prefix (2^nd ‘𝑏))) = (2^nd ‘𝑏))
99	85, 93, 98	syl2anc 584	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) ∧ 𝑏 = ⟨𝑢, 𝑛⟩) ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑛 ∈ (0...(♯‘𝑢))) ∧ (1^st ‘𝑎) = ((1^st ‘𝑏) prefix (2^nd ‘𝑏))) ∧ (2^nd ‘𝑎) = ((1^st ‘𝑏) substr ⟨(2^nd ‘𝑏), (♯‘(1^st ‘𝑏))⟩)) → (♯‘((1^st ‘𝑏) prefix (2^nd ‘𝑏))) = (2^nd ‘𝑏))
100	97, 99	eqtr2d 2767	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) ∧ 𝑏 = ⟨𝑢, 𝑛⟩) ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑛 ∈ (0...(♯‘𝑢))) ∧ (1^st ‘𝑎) = ((1^st ‘𝑏) prefix (2^nd ‘𝑏))) ∧ (2^nd ‘𝑎) = ((1^st ‘𝑏) substr ⟨(2^nd ‘𝑏), (♯‘(1^st ‘𝑏))⟩)) → (2^nd ‘𝑏) = (♯‘(1^st ‘𝑎)))
101	96, 100	jca 511	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) ∧ 𝑏 = ⟨𝑢, 𝑛⟩) ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑛 ∈ (0...(♯‘𝑢))) ∧ (1^st ‘𝑎) = ((1^st ‘𝑏) prefix (2^nd ‘𝑏))) ∧ (2^nd ‘𝑎) = ((1^st ‘𝑏) substr ⟨(2^nd ‘𝑏), (♯‘(1^st ‘𝑏))⟩)) → ((1^st ‘𝑏) = ((1^st ‘𝑎) ++ (2^nd ‘𝑎)) ∧ (2^nd ‘𝑏) = (♯‘(1^st ‘𝑎))))
102	101	anasss 466	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) ∧ 𝑏 = ⟨𝑢, 𝑛⟩) ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑛 ∈ (0...(♯‘𝑢))) ∧ ((1^st ‘𝑎) = ((1^st ‘𝑏) prefix (2^nd ‘𝑏)) ∧ (2^nd ‘𝑎) = ((1^st ‘𝑏) substr ⟨(2^nd ‘𝑏), (♯‘(1^st ‘𝑏))⟩))) → ((1^st ‘𝑏) = ((1^st ‘𝑎) ++ (2^nd ‘𝑎)) ∧ (2^nd ‘𝑏) = (♯‘(1^st ‘𝑎))))
103		simplr 768	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) ∧ 𝑏 = ⟨𝑢, 𝑛⟩) ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑛 ∈ (0...(♯‘𝑢))) ∧ (1^st ‘𝑏) = ((1^st ‘𝑎) ++ (2^nd ‘𝑎))) ∧ (2^nd ‘𝑏) = (♯‘(1^st ‘𝑎))) → (1^st ‘𝑏) = ((1^st ‘𝑎) ++ (2^nd ‘𝑎)))
104		simpr 484	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) ∧ 𝑏 = ⟨𝑢, 𝑛⟩) ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑛 ∈ (0...(♯‘𝑢))) ∧ (1^st ‘𝑏) = ((1^st ‘𝑎) ++ (2^nd ‘𝑎))) ∧ (2^nd ‘𝑏) = (♯‘(1^st ‘𝑎))) → (2^nd ‘𝑏) = (♯‘(1^st ‘𝑎)))
105	103, 104	oveq12d 7364	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) ∧ 𝑏 = ⟨𝑢, 𝑛⟩) ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑛 ∈ (0...(♯‘𝑢))) ∧ (1^st ‘𝑏) = ((1^st ‘𝑎) ++ (2^nd ‘𝑎))) ∧ (2^nd ‘𝑏) = (♯‘(1^st ‘𝑎))) → ((1^st ‘𝑏) prefix (2^nd ‘𝑏)) = (((1^st ‘𝑎) ++ (2^nd ‘𝑎)) prefix (♯‘(1^st ‘𝑎))))
106	8	ad5antr 734	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) ∧ 𝑏 = ⟨𝑢, 𝑛⟩) ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑛 ∈ (0...(♯‘𝑢))) ∧ (1^st ‘𝑏) = ((1^st ‘𝑎) ++ (2^nd ‘𝑎))) ∧ (2^nd ‘𝑏) = (♯‘(1^st ‘𝑎))) → (1^st ‘𝑎) ∈ Word 𝐴)
107	10	ad5antr 734	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) ∧ 𝑏 = ⟨𝑢, 𝑛⟩) ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑛 ∈ (0...(♯‘𝑢))) ∧ (1^st ‘𝑏) = ((1^st ‘𝑎) ++ (2^nd ‘𝑎))) ∧ (2^nd ‘𝑏) = (♯‘(1^st ‘𝑎))) → (2^nd ‘𝑎) ∈ Word 𝐴)
108		pfxccat1 14609	. . . . . . . . . . . . . . . . . 18 ⊢ (((1^st ‘𝑎) ∈ Word 𝐴 ∧ (2^nd ‘𝑎) ∈ Word 𝐴) → (((1^st ‘𝑎) ++ (2^nd ‘𝑎)) prefix (♯‘(1^st ‘𝑎))) = (1^st ‘𝑎))
109	106, 107, 108	syl2anc 584	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) ∧ 𝑏 = ⟨𝑢, 𝑛⟩) ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑛 ∈ (0...(♯‘𝑢))) ∧ (1^st ‘𝑏) = ((1^st ‘𝑎) ++ (2^nd ‘𝑎))) ∧ (2^nd ‘𝑏) = (♯‘(1^st ‘𝑎))) → (((1^st ‘𝑎) ++ (2^nd ‘𝑎)) prefix (♯‘(1^st ‘𝑎))) = (1^st ‘𝑎))
110	105, 109	eqtr2d 2767	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) ∧ 𝑏 = ⟨𝑢, 𝑛⟩) ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑛 ∈ (0...(♯‘𝑢))) ∧ (1^st ‘𝑏) = ((1^st ‘𝑎) ++ (2^nd ‘𝑎))) ∧ (2^nd ‘𝑏) = (♯‘(1^st ‘𝑎))) → (1^st ‘𝑎) = ((1^st ‘𝑏) prefix (2^nd ‘𝑏)))
111	103	fveq2d 6826	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) ∧ 𝑏 = ⟨𝑢, 𝑛⟩) ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑛 ∈ (0...(♯‘𝑢))) ∧ (1^st ‘𝑏) = ((1^st ‘𝑎) ++ (2^nd ‘𝑎))) ∧ (2^nd ‘𝑏) = (♯‘(1^st ‘𝑎))) → (♯‘(1^st ‘𝑏)) = (♯‘((1^st ‘𝑎) ++ (2^nd ‘𝑎))))
112	106, 107, 31	syl2anc 584	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) ∧ 𝑏 = ⟨𝑢, 𝑛⟩) ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑛 ∈ (0...(♯‘𝑢))) ∧ (1^st ‘𝑏) = ((1^st ‘𝑎) ++ (2^nd ‘𝑎))) ∧ (2^nd ‘𝑏) = (♯‘(1^st ‘𝑎))) → (♯‘((1^st ‘𝑎) ++ (2^nd ‘𝑎))) = ((♯‘(1^st ‘𝑎)) + (♯‘(2^nd ‘𝑎))))
113	111, 112	eqtrd 2766	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) ∧ 𝑏 = ⟨𝑢, 𝑛⟩) ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑛 ∈ (0...(♯‘𝑢))) ∧ (1^st ‘𝑏) = ((1^st ‘𝑎) ++ (2^nd ‘𝑎))) ∧ (2^nd ‘𝑏) = (♯‘(1^st ‘𝑎))) → (♯‘(1^st ‘𝑏)) = ((♯‘(1^st ‘𝑎)) + (♯‘(2^nd ‘𝑎))))
114	104, 113	opeq12d 4830	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) ∧ 𝑏 = ⟨𝑢, 𝑛⟩) ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑛 ∈ (0...(♯‘𝑢))) ∧ (1^st ‘𝑏) = ((1^st ‘𝑎) ++ (2^nd ‘𝑎))) ∧ (2^nd ‘𝑏) = (♯‘(1^st ‘𝑎))) → ⟨(2^nd ‘𝑏), (♯‘(1^st ‘𝑏))⟩ = ⟨(♯‘(1^st ‘𝑎)), ((♯‘(1^st ‘𝑎)) + (♯‘(2^nd ‘𝑎)))⟩)
115	103, 114	oveq12d 7364	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) ∧ 𝑏 = ⟨𝑢, 𝑛⟩) ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑛 ∈ (0...(♯‘𝑢))) ∧ (1^st ‘𝑏) = ((1^st ‘𝑎) ++ (2^nd ‘𝑎))) ∧ (2^nd ‘𝑏) = (♯‘(1^st ‘𝑎))) → ((1^st ‘𝑏) substr ⟨(2^nd ‘𝑏), (♯‘(1^st ‘𝑏))⟩) = (((1^st ‘𝑎) ++ (2^nd ‘𝑎)) substr ⟨(♯‘(1^st ‘𝑎)), ((♯‘(1^st ‘𝑎)) + (♯‘(2^nd ‘𝑎)))⟩))
116		swrdccat2 14577	. . . . . . . . . . . . . . . . . 18 ⊢ (((1^st ‘𝑎) ∈ Word 𝐴 ∧ (2^nd ‘𝑎) ∈ Word 𝐴) → (((1^st ‘𝑎) ++ (2^nd ‘𝑎)) substr ⟨(♯‘(1^st ‘𝑎)), ((♯‘(1^st ‘𝑎)) + (♯‘(2^nd ‘𝑎)))⟩) = (2^nd ‘𝑎))
117	106, 107, 116	syl2anc 584	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) ∧ 𝑏 = ⟨𝑢, 𝑛⟩) ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑛 ∈ (0...(♯‘𝑢))) ∧ (1^st ‘𝑏) = ((1^st ‘𝑎) ++ (2^nd ‘𝑎))) ∧ (2^nd ‘𝑏) = (♯‘(1^st ‘𝑎))) → (((1^st ‘𝑎) ++ (2^nd ‘𝑎)) substr ⟨(♯‘(1^st ‘𝑎)), ((♯‘(1^st ‘𝑎)) + (♯‘(2^nd ‘𝑎)))⟩) = (2^nd ‘𝑎))
118	115, 117	eqtr2d 2767	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) ∧ 𝑏 = ⟨𝑢, 𝑛⟩) ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑛 ∈ (0...(♯‘𝑢))) ∧ (1^st ‘𝑏) = ((1^st ‘𝑎) ++ (2^nd ‘𝑎))) ∧ (2^nd ‘𝑏) = (♯‘(1^st ‘𝑎))) → (2^nd ‘𝑎) = ((1^st ‘𝑏) substr ⟨(2^nd ‘𝑏), (♯‘(1^st ‘𝑏))⟩))
119	110, 118	jca 511	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) ∧ 𝑏 = ⟨𝑢, 𝑛⟩) ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑛 ∈ (0...(♯‘𝑢))) ∧ (1^st ‘𝑏) = ((1^st ‘𝑎) ++ (2^nd ‘𝑎))) ∧ (2^nd ‘𝑏) = (♯‘(1^st ‘𝑎))) → ((1^st ‘𝑎) = ((1^st ‘𝑏) prefix (2^nd ‘𝑏)) ∧ (2^nd ‘𝑎) = ((1^st ‘𝑏) substr ⟨(2^nd ‘𝑏), (♯‘(1^st ‘𝑏))⟩)))
120	119	anasss 466	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) ∧ 𝑏 = ⟨𝑢, 𝑛⟩) ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑛 ∈ (0...(♯‘𝑢))) ∧ ((1^st ‘𝑏) = ((1^st ‘𝑎) ++ (2^nd ‘𝑎)) ∧ (2^nd ‘𝑏) = (♯‘(1^st ‘𝑎)))) → ((1^st ‘𝑎) = ((1^st ‘𝑏) prefix (2^nd ‘𝑏)) ∧ (2^nd ‘𝑎) = ((1^st ‘𝑏) substr ⟨(2^nd ‘𝑏), (♯‘(1^st ‘𝑏))⟩)))
121	102, 120	impbida 800	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) ∧ 𝑏 = ⟨𝑢, 𝑛⟩) ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑛 ∈ (0...(♯‘𝑢))) → (((1^st ‘𝑎) = ((1^st ‘𝑏) prefix (2^nd ‘𝑏)) ∧ (2^nd ‘𝑎) = ((1^st ‘𝑏) substr ⟨(2^nd ‘𝑏), (♯‘(1^st ‘𝑏))⟩)) ↔ ((1^st ‘𝑏) = ((1^st ‘𝑎) ++ (2^nd ‘𝑎)) ∧ (2^nd ‘𝑏) = (♯‘(1^st ‘𝑎)))))
122	121	anasss 466	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) ∧ 𝑏 = ⟨𝑢, 𝑛⟩) ∧ (𝑢 ∈ Word 𝐴 ∧ 𝑛 ∈ (0...(♯‘𝑢)))) → (((1^st ‘𝑎) = ((1^st ‘𝑏) prefix (2^nd ‘𝑏)) ∧ (2^nd ‘𝑎) = ((1^st ‘𝑏) substr ⟨(2^nd ‘𝑏), (♯‘(1^st ‘𝑏))⟩)) ↔ ((1^st ‘𝑏) = ((1^st ‘𝑎) ++ (2^nd ‘𝑎)) ∧ (2^nd ‘𝑏) = (♯‘(1^st ‘𝑎)))))
123	122	expl 457	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → ((𝑏 = ⟨𝑢, 𝑛⟩ ∧ (𝑢 ∈ Word 𝐴 ∧ 𝑛 ∈ (0...(♯‘𝑢)))) → (((1^st ‘𝑎) = ((1^st ‘𝑏) prefix (2^nd ‘𝑏)) ∧ (2^nd ‘𝑎) = ((1^st ‘𝑏) substr ⟨(2^nd ‘𝑏), (♯‘(1^st ‘𝑏))⟩)) ↔ ((1^st ‘𝑏) = ((1^st ‘𝑎) ++ (2^nd ‘𝑎)) ∧ (2^nd ‘𝑏) = (♯‘(1^st ‘𝑎))))))
124	123	adantlr 715	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → ((𝑏 = ⟨𝑢, 𝑛⟩ ∧ (𝑢 ∈ Word 𝐴 ∧ 𝑛 ∈ (0...(♯‘𝑢)))) → (((1^st ‘𝑎) = ((1^st ‘𝑏) prefix (2^nd ‘𝑏)) ∧ (2^nd ‘𝑎) = ((1^st ‘𝑏) substr ⟨(2^nd ‘𝑏), (♯‘(1^st ‘𝑏))⟩)) ↔ ((1^st ‘𝑏) = ((1^st ‘𝑎) ++ (2^nd ‘𝑎)) ∧ (2^nd ‘𝑏) = (♯‘(1^st ‘𝑎))))))
125	124	exlimdv 1934	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (∃𝑛(𝑏 = ⟨𝑢, 𝑛⟩ ∧ (𝑢 ∈ Word 𝐴 ∧ 𝑛 ∈ (0...(♯‘𝑢)))) → (((1^st ‘𝑎) = ((1^st ‘𝑏) prefix (2^nd ‘𝑏)) ∧ (2^nd ‘𝑎) = ((1^st ‘𝑏) substr ⟨(2^nd ‘𝑏), (♯‘(1^st ‘𝑏))⟩)) ↔ ((1^st ‘𝑏) = ((1^st ‘𝑎) ++ (2^nd ‘𝑎)) ∧ (2^nd ‘𝑏) = (♯‘(1^st ‘𝑎))))))
126	125	imp 406	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) ∧ ∃𝑛(𝑏 = ⟨𝑢, 𝑛⟩ ∧ (𝑢 ∈ Word 𝐴 ∧ 𝑛 ∈ (0...(♯‘𝑢))))) → (((1^st ‘𝑎) = ((1^st ‘𝑏) prefix (2^nd ‘𝑏)) ∧ (2^nd ‘𝑎) = ((1^st ‘𝑏) substr ⟨(2^nd ‘𝑏), (♯‘(1^st ‘𝑏))⟩)) ↔ ((1^st ‘𝑏) = ((1^st ‘𝑎) ++ (2^nd ‘𝑎)) ∧ (2^nd ‘𝑏) = (♯‘(1^st ‘𝑎)))))
127	76, 126	exlimddv 1936	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (((1^st ‘𝑎) = ((1^st ‘𝑏) prefix (2^nd ‘𝑏)) ∧ (2^nd ‘𝑎) = ((1^st ‘𝑏) substr ⟨(2^nd ‘𝑏), (♯‘(1^st ‘𝑏))⟩)) ↔ ((1^st ‘𝑏) = ((1^st ‘𝑎) ++ (2^nd ‘𝑎)) ∧ (2^nd ‘𝑏) = (♯‘(1^st ‘𝑎)))))
128		eqop 7963	. . . . . . . 8 ⊢ (𝑎 ∈ (Word 𝐴 × Word 𝐴) → (𝑎 = ⟨((1^st ‘𝑏) prefix (2^nd ‘𝑏)), ((1^st ‘𝑏) substr ⟨(2^nd ‘𝑏), (♯‘(1^st ‘𝑏))⟩)⟩ ↔ ((1^st ‘𝑎) = ((1^st ‘𝑏) prefix (2^nd ‘𝑏)) ∧ (2^nd ‘𝑎) = ((1^st ‘𝑏) substr ⟨(2^nd ‘𝑏), (♯‘(1^st ‘𝑏))⟩))))
129	128	adantl 481	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (𝑎 = ⟨((1^st ‘𝑏) prefix (2^nd ‘𝑏)), ((1^st ‘𝑏) substr ⟨(2^nd ‘𝑏), (♯‘(1^st ‘𝑏))⟩)⟩ ↔ ((1^st ‘𝑎) = ((1^st ‘𝑏) prefix (2^nd ‘𝑏)) ∧ (2^nd ‘𝑎) = ((1^st ‘𝑏) substr ⟨(2^nd ‘𝑏), (♯‘(1^st ‘𝑏))⟩))))
130		snssi 4757	. . . . . . . . . . . . 13 ⊢ (𝑤 ∈ Word 𝐴 → {𝑤} ⊆ Word 𝐴)
131	130	adantl 481	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) ∧ 𝑤 ∈ Word 𝐴) → {𝑤} ⊆ Word 𝐴)
132		fz0ssnn0 13522	. . . . . . . . . . . 12 ⊢ (0...(♯‘𝑤)) ⊆ ℕ₀
133		xpss12 5629	. . . . . . . . . . . 12 ⊢ (({𝑤} ⊆ Word 𝐴 ∧ (0...(♯‘𝑤)) ⊆ ℕ₀) → ({𝑤} × (0...(♯‘𝑤))) ⊆ (Word 𝐴 × ℕ₀))
134	131, 132, 133	sylancl 586	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) ∧ 𝑤 ∈ Word 𝐴) → ({𝑤} × (0...(♯‘𝑤))) ⊆ (Word 𝐴 × ℕ₀))
135	134	iunssd 4997	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → ∪ 𝑤 ∈ Word 𝐴({𝑤} × (0...(♯‘𝑤))) ⊆ (Word 𝐴 × ℕ₀))
136	135	adantlr 715	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → ∪ 𝑤 ∈ Word 𝐴({𝑤} × (0...(♯‘𝑤))) ⊆ (Word 𝐴 × ℕ₀))
137	136, 65	sseldd 3930	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → 𝑏 ∈ (Word 𝐴 × ℕ₀))
138		eqop 7963	. . . . . . . 8 ⊢ (𝑏 ∈ (Word 𝐴 × ℕ₀) → (𝑏 = ⟨((1^st ‘𝑎) ++ (2^nd ‘𝑎)), (♯‘(1^st ‘𝑎))⟩ ↔ ((1^st ‘𝑏) = ((1^st ‘𝑎) ++ (2^nd ‘𝑎)) ∧ (2^nd ‘𝑏) = (♯‘(1^st ‘𝑎)))))
139	137, 138	syl 17	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (𝑏 = ⟨((1^st ‘𝑎) ++ (2^nd ‘𝑎)), (♯‘(1^st ‘𝑎))⟩ ↔ ((1^st ‘𝑏) = ((1^st ‘𝑎) ++ (2^nd ‘𝑎)) ∧ (2^nd ‘𝑏) = (♯‘(1^st ‘𝑎)))))
140	127, 129, 139	3bitr4d 311	. . . . . 6 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (𝑎 = ⟨((1^st ‘𝑏) prefix (2^nd ‘𝑏)), ((1^st ‘𝑏) substr ⟨(2^nd ‘𝑏), (♯‘(1^st ‘𝑏))⟩)⟩ ↔ 𝑏 = ⟨((1^st ‘𝑎) ++ (2^nd ‘𝑎)), (♯‘(1^st ‘𝑎))⟩))
141	140	an32s 652	. . . . 5 ⊢ (((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) ∧ 𝑏 ∈ 𝑈) → (𝑎 = ⟨((1^st ‘𝑏) prefix (2^nd ‘𝑏)), ((1^st ‘𝑏) substr ⟨(2^nd ‘𝑏), (♯‘(1^st ‘𝑏))⟩)⟩ ↔ 𝑏 = ⟨((1^st ‘𝑎) ++ (2^nd ‘𝑎)), (♯‘(1^st ‘𝑎))⟩))
142	141	anasss 466	. . . 4 ⊢ ((𝜑 ∧ (𝑎 ∈ (Word 𝐴 × Word 𝐴) ∧ 𝑏 ∈ 𝑈)) → (𝑎 = ⟨((1^st ‘𝑏) prefix (2^nd ‘𝑏)), ((1^st ‘𝑏) substr ⟨(2^nd ‘𝑏), (♯‘(1^st ‘𝑏))⟩)⟩ ↔ 𝑏 = ⟨((1^st ‘𝑎) ++ (2^nd ‘𝑎)), (♯‘(1^st ‘𝑎))⟩))
143	1, 39, 64, 142	f1ocnv2d 7599	. . 3 ⊢ (𝜑 → (𝐹:(Word 𝐴 × Word 𝐴)–1-1-onto→𝑈 ∧ ^◡𝐹 = (𝑏 ∈ 𝑈 ↦ ⟨((1^st ‘𝑏) prefix (2^nd ‘𝑏)), ((1^st ‘𝑏) substr ⟨(2^nd ‘𝑏), (♯‘(1^st ‘𝑏))⟩)⟩)))
144	143	simpld 494	. 2 ⊢ (𝜑 → 𝐹:(Word 𝐴 × Word 𝐴)–1-1-onto→𝑈)
145	143	simprd 495	. . 3 ⊢ (𝜑 → ^◡𝐹 = (𝑏 ∈ 𝑈 ↦ ⟨((1^st ‘𝑏) prefix (2^nd ‘𝑏)), ((1^st ‘𝑏) substr ⟨(2^nd ‘𝑏), (♯‘(1^st ‘𝑏))⟩)⟩))
146		gsumwrd2dccatlem.g	. . 3 ⊢ 𝐺 = (𝑏 ∈ 𝑈 ↦ ⟨((1^st ‘𝑏) prefix (2^nd ‘𝑏)), ((1^st ‘𝑏) substr ⟨(2^nd ‘𝑏), (♯‘(1^st ‘𝑏))⟩)⟩)
147	145, 146	eqtr4di 2784	. 2 ⊢ (𝜑 → ^◡𝐹 = 𝐺)
148	144, 147	jca 511	1 ⊢ (𝜑 → (𝐹:(Word 𝐴 × Word 𝐴)–1-1-onto→𝑈 ∧ ^◡𝐹 = 𝐺))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1541 ∃wex 1780 ∈ wcel 2111 ∃wrex 3056 ⊆ wss 3897 {csn 4573 ⟨cop 4579 ∪ ciun 4939 class class class wbr 5089 ↦ cmpt 5170 × cxp 5612 ^◡ccnv 5613 –1-1-onto→wf1o 6480 ‘cfv 6481 (class class class)co 7346 1^st c1st 7919 2^nd c2nd 7920 0cc0 11006 + caddc 11009 ≤ cle 11147 ℕ₀cn0 12381 ...cfz 13407 ♯chash 14237 Word cword 14420 ++ cconcat 14477 substr csubstr 14548 prefix cpfx 14578

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2113 ax-9 2121 ax-10 2144 ax-11 2160 ax-12 2180 ax-ext 2703 ax-rep 5215 ax-sep 5232 ax-nul 5242 ax-pow 5301 ax-pr 5368 ax-un 7668 ax-cnex 11062 ax-resscn 11063 ax-1cn 11064 ax-icn 11065 ax-addcl 11066 ax-addrcl 11067 ax-mulcl 11068 ax-mulrcl 11069 ax-mulcom 11070 ax-addass 11071 ax-mulass 11072 ax-distr 11073 ax-i2m1 11074 ax-1ne0 11075 ax-1rid 11076 ax-rnegex 11077 ax-rrecex 11078 ax-cnre 11079 ax-pre-lttri 11080 ax-pre-lttrn 11081 ax-pre-ltadd 11082 ax-pre-mulgt0 11083

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2535 df-eu 2564 df-clab 2710 df-cleq 2723 df-clel 2806 df-nfc 2881 df-ne 2929 df-nel 3033 df-ral 3048 df-rex 3057 df-reu 3347 df-rab 3396 df-v 3438 df-sbc 3737 df-csb 3846 df-dif 3900 df-un 3902 df-in 3904 df-ss 3914 df-pss 3917 df-nul 4281 df-if 4473 df-pw 4549 df-sn 4574 df-pr 4576 df-op 4580 df-uni 4857 df-int 4896 df-iun 4941 df-br 5090 df-opab 5152 df-mpt 5171 df-tr 5197 df-id 5509 df-eprel 5514 df-po 5522 df-so 5523 df-fr 5567 df-we 5569 df-xp 5620 df-rel 5621 df-cnv 5622 df-co 5623 df-dm 5624 df-rn 5625 df-res 5626 df-ima 5627 df-pred 6248 df-ord 6309 df-on 6310 df-lim 6311 df-suc 6312 df-iota 6437 df-fun 6483 df-fn 6484 df-f 6485 df-f1 6486 df-fo 6487 df-f1o 6488 df-fv 6489 df-riota 7303 df-ov 7349 df-oprab 7350 df-mpo 7351 df-om 7797 df-1st 7921 df-2nd 7922 df-frecs 8211 df-wrecs 8242 df-recs 8291 df-rdg 8329 df-1o 8385 df-er 8622 df-en 8870 df-dom 8871 df-sdom 8872 df-fin 8873 df-card 9832 df-pnf 11148 df-mnf 11149 df-xr 11150 df-ltxr 11151 df-le 11152 df-sub 11346 df-neg 11347 df-nn 12126 df-n0 12382 df-z 12469 df-uz 12733 df-fz 13408 df-fzo 13555 df-hash 14238 df-word 14421 df-concat 14478 df-substr 14549 df-pfx 14579

This theorem is referenced by: gsumwrd2dccat 33047

W3C validator