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 33549

Description: Lemma for gsumwrd2dccat 33550. 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 4594	. . . . . . . . 9 ⊢ (𝑤 = ((1^st ‘𝑎) ++ (2^nd ‘𝑎)) → {𝑤} = {((1^st ‘𝑎) ++ (2^nd ‘𝑎))})
3		fveq2 6881	. . . . . . . . . 10 ⊢ (𝑤 = ((1^st ‘𝑎) ++ (2^nd ‘𝑎)) → (♯‘𝑤) = (♯‘((1^st ‘𝑎) ++ (2^nd ‘𝑎))))
4	3	oveq2d 7432	. . . . . . . . 9 ⊢ (𝑤 = ((1^st ‘𝑎) ++ (2^nd ‘𝑎)) → (0...(♯‘𝑤)) = (0...(♯‘((1^st ‘𝑎) ++ (2^nd ‘𝑎)))))
5	2, 4	xpeq12d 5686	. . . . . . . 8 ⊢ (𝑤 = ((1^st ‘𝑎) ++ (2^nd ‘𝑎)) → ({𝑤} × (0...(♯‘𝑤))) = ({((1^st ‘𝑎) ++ (2^nd ‘𝑎))} × (0...(♯‘((1^st ‘𝑎) ++ (2^nd ‘𝑎))))))
6	5	eleq2d 2846	. . . . . . 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 8024	. . . . . . . . 9 ⊢ (𝑎 ∈ (Word 𝐴 × Word 𝐴) → (1^st ‘𝑎) ∈ Word 𝐴)
8	7	adantl 487	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (1^st ‘𝑎) ∈ Word 𝐴)
9		xp2nd 8025	. . . . . . . . 9 ⊢ (𝑎 ∈ (Word 𝐴 × Word 𝐴) → (2^nd ‘𝑎) ∈ Word 𝐴)
10	9	adantl 487	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (2^nd ‘𝑎) ∈ Word 𝐴)
11		ccatcl 14664	. . . . . . . 8 ⊢ (((1^st ‘𝑎) ∈ Word 𝐴 ∧ (2^nd ‘𝑎) ∈ Word 𝐴) → ((1^st ‘𝑎) ++ (2^nd ‘𝑎)) ∈ Word 𝐴)
12	8, 10, 11	syl2anc 596	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → ((1^st ‘𝑎) ++ (2^nd ‘𝑎)) ∈ Word 𝐴)
13		ovex 7449	. . . . . . . . . 10 ⊢ ((1^st ‘𝑎) ++ (2^nd ‘𝑎)) ∈ V
14	13	snid 4623	. . . . . . . . 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 12652	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → 0 ∈ ℤ)
17		lencl 14623	. . . . . . . . . . 11 ⊢ (((1^st ‘𝑎) ++ (2^nd ‘𝑎)) ∈ Word 𝐴 → (♯‘((1^st ‘𝑎) ++ (2^nd ‘𝑎))) ∈ ℕ₀)
18	12, 17	syl 18	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (♯‘((1^st ‘𝑎) ++ (2^nd ‘𝑎))) ∈ ℕ₀)
19	18	nn0zd 12665	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (♯‘((1^st ‘𝑎) ++ (2^nd ‘𝑎))) ∈ ℤ)
20		lencl 14623	. . . . . . . . . . 11 ⊢ ((1^st ‘𝑎) ∈ Word 𝐴 → (♯‘(1^st ‘𝑎)) ∈ ℕ₀)
21	8, 20	syl 18	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (♯‘(1^st ‘𝑎)) ∈ ℕ₀)
22	21	nn0zd 12665	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (♯‘(1^st ‘𝑎)) ∈ ℤ)
23	21	nn0ge0d 12617	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → 0 ≤ (♯‘(1^st ‘𝑎)))
24		lencl 14623	. . . . . . . . . . . . 13 ⊢ ((2^nd ‘𝑎) ∈ Word 𝐴 → (♯‘(2^nd ‘𝑎)) ∈ ℕ₀)
25	10, 24	syl 18	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (♯‘(2^nd ‘𝑎)) ∈ ℕ₀)
26	25	nn0ge0d 12617	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → 0 ≤ (♯‘(2^nd ‘𝑎)))
27	21	nn0red 12615	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (♯‘(1^st ‘𝑎)) ∈ ℝ)
28	25	nn0red 12615	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (♯‘(2^nd ‘𝑎)) ∈ ℝ)
29	27, 28	addge01d 11851	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (0 ≤ (♯‘(2^nd ‘𝑎)) ↔ (♯‘(1^st ‘𝑎)) ≤ ((♯‘(1^st ‘𝑎)) + (♯‘(2^nd ‘𝑎)))))
30	26, 29	mpbid 235	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (♯‘(1^st ‘𝑎)) ≤ ((♯‘(1^st ‘𝑎)) + (♯‘(2^nd ‘𝑎))))
31		ccatlen 14665	. . . . . . . . . . 11 ⊢ (((1^st ‘𝑎) ∈ Word 𝐴 ∧ (2^nd ‘𝑎) ∈ Word 𝐴) → (♯‘((1^st ‘𝑎) ++ (2^nd ‘𝑎))) = ((♯‘(1^st ‘𝑎)) + (♯‘(2^nd ‘𝑎))))
32	8, 10, 31	syl2anc 596	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (♯‘((1^st ‘𝑎) ++ (2^nd ‘𝑎))) = ((♯‘(1^st ‘𝑎)) + (♯‘(2^nd ‘𝑎))))
33	30, 32	breqtrrd 5133	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (♯‘(1^st ‘𝑎)) ≤ (♯‘((1^st ‘𝑎) ++ (2^nd ‘𝑎))))
34	16, 19, 22, 23, 33	elfzd 13594	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (♯‘(1^st ‘𝑎)) ∈ (0...(♯‘((1^st ‘𝑎) ++ (2^nd ‘𝑎)))))
35	15, 34	opelxpd 5694	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → ⟨((1^st ‘𝑎) ++ (2^nd ‘𝑎)), (♯‘(1^st ‘𝑎))⟩ ∈ ({((1^st ‘𝑎) ++ (2^nd ‘𝑎))} × (0...(♯‘((1^st ‘𝑎) ++ (2^nd ‘𝑎))))))
36	6, 12, 35	rspcedvdw 3579	. . . . . 6 ⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → ∃𝑤 ∈ Word 𝐴⟨((1^st ‘𝑎) ++ (2^nd ‘𝑎)), (♯‘(1^st ‘𝑎))⟩ ∈ ({𝑤} × (0...(♯‘𝑤))))
37	36	eliund 4958	. . . . 5 ⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → ⟨((1^st ‘𝑎) ++ (2^nd ‘𝑎)), (♯‘(1^st ‘𝑎))⟩ ∈ ∪ 𝑤 ∈ Word 𝐴({𝑤} × (0...(♯‘𝑤))))
38		gsumwrd2dccatlem.u	. . . . 5 ⊢ 𝑈 = ∪ 𝑤 ∈ Word 𝐴({𝑤} × (0...(♯‘𝑤)))
39	37, 38	eleqtrrdi 2871	. . . 4 ⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → ⟨((1^st ‘𝑎) ++ (2^nd ‘𝑎)), (♯‘(1^st ‘𝑎))⟩ ∈ 𝑈)
40		simpr 490	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑏 ∈ ({𝑢} × (0...(♯‘𝑢)))) → 𝑏 ∈ ({𝑢} × (0...(♯‘𝑢))))
41		xp1st 8024	. . . . . . . . . 10 ⊢ (𝑏 ∈ ({𝑢} × (0...(♯‘𝑢))) → (1^st ‘𝑏) ∈ {𝑢})
42		elsni 4601	. . . . . . . . . 10 ⊢ ((1^st ‘𝑏) ∈ {𝑢} → (1^st ‘𝑏) = 𝑢)
43	40, 41, 42	3syl 19	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑏 ∈ ({𝑢} × (0...(♯‘𝑢)))) → (1^st ‘𝑏) = 𝑢)
44		simplr 781	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑏 ∈ ({𝑢} × (0...(♯‘𝑢)))) → 𝑢 ∈ Word 𝐴)
45	43, 44	eqeltrd 2860	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑏 ∈ ({𝑢} × (0...(♯‘𝑢)))) → (1^st ‘𝑏) ∈ Word 𝐴)
46	45	adantllr 732	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑏 ∈ ({𝑢} × (0...(♯‘𝑢)))) → (1^st ‘𝑏) ∈ Word 𝐴)
47	38	eleq2i 2852	. . . . . . . . . 10 ⊢ (𝑏 ∈ 𝑈 ↔ 𝑏 ∈ ∪ 𝑤 ∈ Word 𝐴({𝑤} × (0...(♯‘𝑤))))
48	47	bilani 510	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝑈) → 𝑏 ∈ ∪ 𝑤 ∈ Word 𝐴({𝑤} × (0...(♯‘𝑤))))
49		eliun 4955	. . . . . . . . 9 ⊢ (𝑏 ∈ ∪ 𝑤 ∈ Word 𝐴({𝑤} × (0...(♯‘𝑤))) ↔ ∃𝑤 ∈ Word 𝐴𝑏 ∈ ({𝑤} × (0...(♯‘𝑤))))
50	48, 49	sylib 221	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝑈) → ∃𝑤 ∈ Word 𝐴𝑏 ∈ ({𝑤} × (0...(♯‘𝑤))))
51		sneq 4594	. . . . . . . . . . 11 ⊢ (𝑢 = 𝑤 → {𝑢} = {𝑤})
52		fveq2 6881	. . . . . . . . . . . 12 ⊢ (𝑢 = 𝑤 → (♯‘𝑢) = (♯‘𝑤))
53	52	oveq2d 7432	. . . . . . . . . . 11 ⊢ (𝑢 = 𝑤 → (0...(♯‘𝑢)) = (0...(♯‘𝑤)))
54	51, 53	xpeq12d 5686	. . . . . . . . . 10 ⊢ (𝑢 = 𝑤 → ({𝑢} × (0...(♯‘𝑢))) = ({𝑤} × (0...(♯‘𝑤))))
55	54	eleq2d 2846	. . . . . . . . 9 ⊢ (𝑢 = 𝑤 → (𝑏 ∈ ({𝑢} × (0...(♯‘𝑢))) ↔ 𝑏 ∈ ({𝑤} × (0...(♯‘𝑤)))))
56	55	cbvrexvw 3241	. . . . . . . 8 ⊢ (∃𝑢 ∈ Word 𝐴𝑏 ∈ ({𝑢} × (0...(♯‘𝑢))) ↔ ∃𝑤 ∈ Word 𝐴𝑏 ∈ ({𝑤} × (0...(♯‘𝑤))))
57	50, 56	sylibr 237	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝑈) → ∃𝑢 ∈ Word 𝐴𝑏 ∈ ({𝑢} × (0...(♯‘𝑢))))
58	46, 57	r19.29a 3170	. . . . . 6 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝑈) → (1^st ‘𝑏) ∈ Word 𝐴)
59		pfxcl 14772	. . . . . 6 ⊢ ((1^st ‘𝑏) ∈ Word 𝐴 → ((1^st ‘𝑏) prefix (2^nd ‘𝑏)) ∈ Word 𝐴)
60	58, 59	syl 18	. . . . 5 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝑈) → ((1^st ‘𝑏) prefix (2^nd ‘𝑏)) ∈ Word 𝐴)
61		swrdcl 14738	. . . . . 6 ⊢ ((1^st ‘𝑏) ∈ Word 𝐴 → ((1^st ‘𝑏) substr ⟨(2^nd ‘𝑏), (♯‘(1^st ‘𝑏))⟩) ∈ Word 𝐴)
62	58, 61	syl 18	. . . . 5 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝑈) → ((1^st ‘𝑏) substr ⟨(2^nd ‘𝑏), (♯‘(1^st ‘𝑏))⟩) ∈ Word 𝐴)
63	60, 62	opelxpd 5694	. . . 4 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝑈) → ⟨((1^st ‘𝑏) prefix (2^nd ‘𝑏)), ((1^st ‘𝑏) substr ⟨(2^nd ‘𝑏), (♯‘(1^st ‘𝑏))⟩)⟩ ∈ (Word 𝐴 × Word 𝐴))
64	48	adantr 486	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → 𝑏 ∈ ∪ 𝑤 ∈ Word 𝐴({𝑤} × (0...(♯‘𝑤))))
65		eliunxp 5818	. . . . . . . . . 10 ⊢ (𝑏 ∈ ∪ 𝑤 ∈ Word 𝐴({𝑤} × (0...(♯‘𝑤))) ↔ ∃𝑤∃𝑛(𝑏 = ⟨𝑤, 𝑛⟩ ∧ (𝑤 ∈ Word 𝐴 ∧ 𝑛 ∈ (0...(♯‘𝑤)))))
66	64, 65	sylib 221	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → ∃𝑤∃𝑛(𝑏 = ⟨𝑤, 𝑛⟩ ∧ (𝑤 ∈ Word 𝐴 ∧ 𝑛 ∈ (0...(♯‘𝑤)))))
67		opeq1 4833	. . . . . . . . . . . . 13 ⊢ (𝑢 = 𝑤 → ⟨𝑢, 𝑛⟩ = ⟨𝑤, 𝑛⟩)
68	67	eqeq2d 2771	. . . . . . . . . . . 12 ⊢ (𝑢 = 𝑤 → (𝑏 = ⟨𝑢, 𝑛⟩ ↔ 𝑏 = ⟨𝑤, 𝑛⟩))
69		eleq1w 2843	. . . . . . . . . . . . 13 ⊢ (𝑢 = 𝑤 → (𝑢 ∈ Word 𝐴 ↔ 𝑤 ∈ Word 𝐴))
70	53	eleq2d 2846	. . . . . . . . . . . . 13 ⊢ (𝑢 = 𝑤 → (𝑛 ∈ (0...(♯‘𝑢)) ↔ 𝑛 ∈ (0...(♯‘𝑤))))
71	69, 70	anbi12d 644	. . . . . . . . . . . 12 ⊢ (𝑢 = 𝑤 → ((𝑢 ∈ Word 𝐴 ∧ 𝑛 ∈ (0...(♯‘𝑢))) ↔ (𝑤 ∈ Word 𝐴 ∧ 𝑛 ∈ (0...(♯‘𝑤)))))
72	68, 71	anbi12d 644	. . . . . . . . . . 11 ⊢ (𝑢 = 𝑤 → ((𝑏 = ⟨𝑢, 𝑛⟩ ∧ (𝑢 ∈ Word 𝐴 ∧ 𝑛 ∈ (0...(♯‘𝑢)))) ↔ (𝑏 = ⟨𝑤, 𝑛⟩ ∧ (𝑤 ∈ Word 𝐴 ∧ 𝑛 ∈ (0...(♯‘𝑤))))))
73	72	exbidv 1954	. . . . . . . . . 10 ⊢ (𝑢 = 𝑤 → (∃𝑛(𝑏 = ⟨𝑢, 𝑛⟩ ∧ (𝑢 ∈ Word 𝐴 ∧ 𝑛 ∈ (0...(♯‘𝑢)))) ↔ ∃𝑛(𝑏 = ⟨𝑤, 𝑛⟩ ∧ (𝑤 ∈ Word 𝐴 ∧ 𝑛 ∈ (0...(♯‘𝑤))))))
74	73	cbvexvw 2070	. . . . . . . . 9 ⊢ (∃𝑢∃𝑛(𝑏 = ⟨𝑢, 𝑛⟩ ∧ (𝑢 ∈ Word 𝐴 ∧ 𝑛 ∈ (0...(♯‘𝑢)))) ↔ ∃𝑤∃𝑛(𝑏 = ⟨𝑤, 𝑛⟩ ∧ (𝑤 ∈ Word 𝐴 ∧ 𝑛 ∈ (0...(♯‘𝑤)))))
75	66, 74	sylibr 237	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → ∃𝑢∃𝑛(𝑏 = ⟨𝑢, 𝑛⟩ ∧ (𝑢 ∈ Word 𝐴 ∧ 𝑛 ∈ (0...(♯‘𝑢)))))
76		simplr 781	. . . . . . . . . . . . . . . . . 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 ‘𝑏)))
77		simpr 490	. . . . . . . . . . . . . . . . . 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 ‘𝑏))⟩))
78	76, 77	oveq12d 7434	. . . . . . . . . . . . . . . . 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 ‘𝑏))⟩)))
79		vex 3454	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑢 ∈ V
80		vex 3454	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑛 ∈ V
81	79, 80	op1std 8002	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑏 = ⟨𝑢, 𝑛⟩ → (1^st ‘𝑏) = 𝑢)
82	81	ad5antlr 748	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) ∧ 𝑏 = ⟨𝑢, 𝑛⟩) ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑛 ∈ (0...(♯‘𝑢))) ∧ (1^st ‘𝑎) = ((1^st ‘𝑏) prefix (2^nd ‘𝑏))) ∧ (2^nd ‘𝑎) = ((1^st ‘𝑏) substr ⟨(2^nd ‘𝑏), (♯‘(1^st ‘𝑏))⟩)) → (1^st ‘𝑏) = 𝑢)
83		simp-4r 796	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) ∧ 𝑏 = ⟨𝑢, 𝑛⟩) ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑛 ∈ (0...(♯‘𝑢))) ∧ (1^st ‘𝑎) = ((1^st ‘𝑏) prefix (2^nd ‘𝑏))) ∧ (2^nd ‘𝑎) = ((1^st ‘𝑏) substr ⟨(2^nd ‘𝑏), (♯‘(1^st ‘𝑏))⟩)) → 𝑢 ∈ Word 𝐴)
84	82, 83	eqeltrd 2860	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) ∧ 𝑏 = ⟨𝑢, 𝑛⟩) ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑛 ∈ (0...(♯‘𝑢))) ∧ (1^st ‘𝑎) = ((1^st ‘𝑏) prefix (2^nd ‘𝑏))) ∧ (2^nd ‘𝑎) = ((1^st ‘𝑏) substr ⟨(2^nd ‘𝑏), (♯‘(1^st ‘𝑏))⟩)) → (1^st ‘𝑏) ∈ Word 𝐴)
85	79, 80	op2ndd 8003	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑏 = ⟨𝑢, 𝑛⟩ → (2^nd ‘𝑏) = 𝑛)
86	85	ad5antlr 748	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) ∧ 𝑏 = ⟨𝑢, 𝑛⟩) ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑛 ∈ (0...(♯‘𝑢))) ∧ (1^st ‘𝑎) = ((1^st ‘𝑏) prefix (2^nd ‘𝑏))) ∧ (2^nd ‘𝑎) = ((1^st ‘𝑏) substr ⟨(2^nd ‘𝑏), (♯‘(1^st ‘𝑏))⟩)) → (2^nd ‘𝑏) = 𝑛)
87		simpllr 788	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) ∧ 𝑏 = ⟨𝑢, 𝑛⟩) ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑛 ∈ (0...(♯‘𝑢))) ∧ (1^st ‘𝑎) = ((1^st ‘𝑏) prefix (2^nd ‘𝑏))) ∧ (2^nd ‘𝑎) = ((1^st ‘𝑏) substr ⟨(2^nd ‘𝑏), (♯‘(1^st ‘𝑏))⟩)) → 𝑛 ∈ (0...(♯‘𝑢)))
88	82	eqcomd 2766	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) ∧ 𝑏 = ⟨𝑢, 𝑛⟩) ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑛 ∈ (0...(♯‘𝑢))) ∧ (1^st ‘𝑎) = ((1^st ‘𝑏) prefix (2^nd ‘𝑏))) ∧ (2^nd ‘𝑎) = ((1^st ‘𝑏) substr ⟨(2^nd ‘𝑏), (♯‘(1^st ‘𝑏))⟩)) → 𝑢 = (1^st ‘𝑏))
89	88	fveq2d 6885	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) ∧ 𝑏 = ⟨𝑢, 𝑛⟩) ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑛 ∈ (0...(♯‘𝑢))) ∧ (1^st ‘𝑎) = ((1^st ‘𝑏) prefix (2^nd ‘𝑏))) ∧ (2^nd ‘𝑎) = ((1^st ‘𝑏) substr ⟨(2^nd ‘𝑏), (♯‘(1^st ‘𝑏))⟩)) → (♯‘𝑢) = (♯‘(1^st ‘𝑏)))
90	89	oveq2d 7432	. . . . . . . . . . . . . . . . . . . 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 ‘𝑏))))
91	87, 90	eleqtrd 2862	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) ∧ 𝑏 = ⟨𝑢, 𝑛⟩) ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑛 ∈ (0...(♯‘𝑢))) ∧ (1^st ‘𝑎) = ((1^st ‘𝑏) prefix (2^nd ‘𝑏))) ∧ (2^nd ‘𝑎) = ((1^st ‘𝑏) substr ⟨(2^nd ‘𝑏), (♯‘(1^st ‘𝑏))⟩)) → 𝑛 ∈ (0...(♯‘(1^st ‘𝑏))))
92	86, 91	eqeltrd 2860	. . . . . . . . . . . . . . . . . 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 ‘𝑏))))
93		pfxcctswrd 14804	. . . . . . . . . . . . . . . . . 18 ⊢ (((1^st ‘𝑏) ∈ Word 𝐴 ∧ (2^nd ‘𝑏) ∈ (0...(♯‘(1^st ‘𝑏)))) → (((1^st ‘𝑏) prefix (2^nd ‘𝑏)) ++ ((1^st ‘𝑏) substr ⟨(2^nd ‘𝑏), (♯‘(1^st ‘𝑏))⟩)) = (1^st ‘𝑏))
94	84, 92, 93	syl2anc 596	. . . . . . . . . . . . . . . . 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 ‘𝑏))
95	78, 94	eqtr2d 2796	. . . . . . . . . . . . . . . 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 ‘𝑎)))
96	76	fveq2d 6885	. . . . . . . . . . . . . . . . 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 ‘𝑏))))
97		pfxlen 14778	. . . . . . . . . . . . . . . . . 18 ⊢ (((1^st ‘𝑏) ∈ Word 𝐴 ∧ (2^nd ‘𝑏) ∈ (0...(♯‘(1^st ‘𝑏)))) → (♯‘((1^st ‘𝑏) prefix (2^nd ‘𝑏))) = (2^nd ‘𝑏))
98	84, 92, 97	syl2anc 596	. . . . . . . . . . . . . . . . 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 ‘𝑏))
99	96, 98	eqtr2d 2796	. . . . . . . . . . . . . . . 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 ‘𝑎)))
100	95, 99	jca 521	. . . . . . . . . . . . . . 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 ‘𝑎))))
101	100	anasss 472	. . . . . . . . . . . . . 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 ‘𝑎))))
102		simplr 781	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) ∧ 𝑏 = ⟨𝑢, 𝑛⟩) ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑛 ∈ (0...(♯‘𝑢))) ∧ (1^st ‘𝑏) = ((1^st ‘𝑎) ++ (2^nd ‘𝑎))) ∧ (2^nd ‘𝑏) = (♯‘(1^st ‘𝑎))) → (1^st ‘𝑏) = ((1^st ‘𝑎) ++ (2^nd ‘𝑎)))
103		simpr 490	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) ∧ 𝑏 = ⟨𝑢, 𝑛⟩) ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑛 ∈ (0...(♯‘𝑢))) ∧ (1^st ‘𝑏) = ((1^st ‘𝑎) ++ (2^nd ‘𝑎))) ∧ (2^nd ‘𝑏) = (♯‘(1^st ‘𝑎))) → (2^nd ‘𝑏) = (♯‘(1^st ‘𝑎)))
104	102, 103	oveq12d 7434	. . . . . . . . . . . . . . . . 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 ‘𝑎))))
105	8	ad5antr 747	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) ∧ 𝑏 = ⟨𝑢, 𝑛⟩) ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑛 ∈ (0...(♯‘𝑢))) ∧ (1^st ‘𝑏) = ((1^st ‘𝑎) ++ (2^nd ‘𝑎))) ∧ (2^nd ‘𝑏) = (♯‘(1^st ‘𝑎))) → (1^st ‘𝑎) ∈ Word 𝐴)
106	10	ad5antr 747	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) ∧ 𝑏 = ⟨𝑢, 𝑛⟩) ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑛 ∈ (0...(♯‘𝑢))) ∧ (1^st ‘𝑏) = ((1^st ‘𝑎) ++ (2^nd ‘𝑎))) ∧ (2^nd ‘𝑏) = (♯‘(1^st ‘𝑎))) → (2^nd ‘𝑎) ∈ Word 𝐴)
107		pfxccat1 14796	. . . . . . . . . . . . . . . . . 18 ⊢ (((1^st ‘𝑎) ∈ Word 𝐴 ∧ (2^nd ‘𝑎) ∈ Word 𝐴) → (((1^st ‘𝑎) ++ (2^nd ‘𝑎)) prefix (♯‘(1^st ‘𝑎))) = (1^st ‘𝑎))
108	105, 106, 107	syl2anc 596	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) ∧ 𝑏 = ⟨𝑢, 𝑛⟩) ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑛 ∈ (0...(♯‘𝑢))) ∧ (1^st ‘𝑏) = ((1^st ‘𝑎) ++ (2^nd ‘𝑎))) ∧ (2^nd ‘𝑏) = (♯‘(1^st ‘𝑎))) → (((1^st ‘𝑎) ++ (2^nd ‘𝑎)) prefix (♯‘(1^st ‘𝑎))) = (1^st ‘𝑎))
109	104, 108	eqtr2d 2796	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) ∧ 𝑏 = ⟨𝑢, 𝑛⟩) ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑛 ∈ (0...(♯‘𝑢))) ∧ (1^st ‘𝑏) = ((1^st ‘𝑎) ++ (2^nd ‘𝑎))) ∧ (2^nd ‘𝑏) = (♯‘(1^st ‘𝑎))) → (1^st ‘𝑎) = ((1^st ‘𝑏) prefix (2^nd ‘𝑏)))
110	102	fveq2d 6885	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) ∧ 𝑏 = ⟨𝑢, 𝑛⟩) ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑛 ∈ (0...(♯‘𝑢))) ∧ (1^st ‘𝑏) = ((1^st ‘𝑎) ++ (2^nd ‘𝑎))) ∧ (2^nd ‘𝑏) = (♯‘(1^st ‘𝑎))) → (♯‘(1^st ‘𝑏)) = (♯‘((1^st ‘𝑎) ++ (2^nd ‘𝑎))))
111	105, 106, 31	syl2anc 596	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) ∧ 𝑏 = ⟨𝑢, 𝑛⟩) ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑛 ∈ (0...(♯‘𝑢))) ∧ (1^st ‘𝑏) = ((1^st ‘𝑎) ++ (2^nd ‘𝑎))) ∧ (2^nd ‘𝑏) = (♯‘(1^st ‘𝑎))) → (♯‘((1^st ‘𝑎) ++ (2^nd ‘𝑎))) = ((♯‘(1^st ‘𝑎)) + (♯‘(2^nd ‘𝑎))))
112	110, 111	eqtrd 2795	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) ∧ 𝑏 = ⟨𝑢, 𝑛⟩) ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑛 ∈ (0...(♯‘𝑢))) ∧ (1^st ‘𝑏) = ((1^st ‘𝑎) ++ (2^nd ‘𝑎))) ∧ (2^nd ‘𝑏) = (♯‘(1^st ‘𝑎))) → (♯‘(1^st ‘𝑏)) = ((♯‘(1^st ‘𝑎)) + (♯‘(2^nd ‘𝑎))))
113	103, 112	opeq12d 4841	. . . . . . . . . . . . . . . . . 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 ‘𝑎)))⟩)
114	102, 113	oveq12d 7434	. . . . . . . . . . . . . . . . 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 ‘𝑎)))⟩))
115		swrdccat2 14764	. . . . . . . . . . . . . . . . . 18 ⊢ (((1^st ‘𝑎) ∈ Word 𝐴 ∧ (2^nd ‘𝑎) ∈ Word 𝐴) → (((1^st ‘𝑎) ++ (2^nd ‘𝑎)) substr ⟨(♯‘(1^st ‘𝑎)), ((♯‘(1^st ‘𝑎)) + (♯‘(2^nd ‘𝑎)))⟩) = (2^nd ‘𝑎))
116	105, 106, 115	syl2anc 596	. . . . . . . . . . . . . . . . 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 ‘𝑎))
117	114, 116	eqtr2d 2796	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) ∧ 𝑏 = ⟨𝑢, 𝑛⟩) ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑛 ∈ (0...(♯‘𝑢))) ∧ (1^st ‘𝑏) = ((1^st ‘𝑎) ++ (2^nd ‘𝑎))) ∧ (2^nd ‘𝑏) = (♯‘(1^st ‘𝑎))) → (2^nd ‘𝑎) = ((1^st ‘𝑏) substr ⟨(2^nd ‘𝑏), (♯‘(1^st ‘𝑏))⟩))
118	109, 117	jca 521	. . . . . . . . . . . . . . 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 ‘𝑏))⟩)))
119	118	anasss 472	. . . . . . . . . . . . . 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 ‘𝑏))⟩)))
120	101, 119	impbida 813	. . . . . . . . . . . . 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 ‘𝑎)))))
121	120	anasss 472	. . . . . . . . . . . 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 ‘𝑎)))))
122	121	expl 463	. . . . . . . . . . 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 ‘𝑎))))))
123	122	adantlr 728	. . . . . . . . . 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 ‘𝑎))))))
124	123	exlimdv 1966	. . . . . . . . 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 ‘𝑎))))))
125	124	imp 412	. . . . . . . 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 ‘𝑎)))))
126	75, 125	exlimddv 1968	. . . . . . 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 ‘𝑎)))))
127		eqop 8034	. . . . . . . 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 ‘𝑏))⟩))))
128	127	adantl 487	. . . . . . 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 ‘𝑏))⟩))))
129		snssi 4746	. . . . . . . . . . . . 13 ⊢ (𝑤 ∈ Word 𝐴 → {𝑤} ⊆ Word 𝐴)
130	129	adantl 487	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) ∧ 𝑤 ∈ Word 𝐴) → {𝑤} ⊆ Word 𝐴)
131		fz0ssnn0 13702	. . . . . . . . . . . 12 ⊢ (0...(♯‘𝑤)) ⊆ ℕ₀
132		xpss12 5670	. . . . . . . . . . . 12 ⊢ (({𝑤} ⊆ Word 𝐴 ∧ (0...(♯‘𝑤)) ⊆ ℕ₀) → ({𝑤} × (0...(♯‘𝑤))) ⊆ (Word 𝐴 × ℕ₀))
133	130, 131, 132	sylancl 598	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) ∧ 𝑤 ∈ Word 𝐴) → ({𝑤} × (0...(♯‘𝑤))) ⊆ (Word 𝐴 × ℕ₀))
134	133	iunssd 5009	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → ∪ 𝑤 ∈ Word 𝐴({𝑤} × (0...(♯‘𝑤))) ⊆ (Word 𝐴 × ℕ₀))
135	134	adantlr 728	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → ∪ 𝑤 ∈ Word 𝐴({𝑤} × (0...(♯‘𝑤))) ⊆ (Word 𝐴 × ℕ₀))
136	135, 64	sseldd 3932	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → 𝑏 ∈ (Word 𝐴 × ℕ₀))
137		eqop 8034	. . . . . . . 8 ⊢ (𝑏 ∈ (Word 𝐴 × ℕ₀) → (𝑏 = ⟨((1^st ‘𝑎) ++ (2^nd ‘𝑎)), (♯‘(1^st ‘𝑎))⟩ ↔ ((1^st ‘𝑏) = ((1^st ‘𝑎) ++ (2^nd ‘𝑎)) ∧ (2^nd ‘𝑏) = (♯‘(1^st ‘𝑎)))))
138	136, 137	syl 18	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (𝑏 = ⟨((1^st ‘𝑎) ++ (2^nd ‘𝑎)), (♯‘(1^st ‘𝑎))⟩ ↔ ((1^st ‘𝑏) = ((1^st ‘𝑎) ++ (2^nd ‘𝑎)) ∧ (2^nd ‘𝑏) = (♯‘(1^st ‘𝑎)))))
139	126, 128, 138	3bitr4d 314	. . . . . 6 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (𝑎 = ⟨((1^st ‘𝑏) prefix (2^nd ‘𝑏)), ((1^st ‘𝑏) substr ⟨(2^nd ‘𝑏), (♯‘(1^st ‘𝑏))⟩)⟩ ↔ 𝑏 = ⟨((1^st ‘𝑎) ++ (2^nd ‘𝑎)), (♯‘(1^st ‘𝑎))⟩))
140	139	an32s 665	. . . . 5 ⊢ (((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) ∧ 𝑏 ∈ 𝑈) → (𝑎 = ⟨((1^st ‘𝑏) prefix (2^nd ‘𝑏)), ((1^st ‘𝑏) substr ⟨(2^nd ‘𝑏), (♯‘(1^st ‘𝑏))⟩)⟩ ↔ 𝑏 = ⟨((1^st ‘𝑎) ++ (2^nd ‘𝑎)), (♯‘(1^st ‘𝑎))⟩))
141	140	anasss 472	. . . 4 ⊢ ((𝜑 ∧ (𝑎 ∈ (Word 𝐴 × Word 𝐴) ∧ 𝑏 ∈ 𝑈)) → (𝑎 = ⟨((1^st ‘𝑏) prefix (2^nd ‘𝑏)), ((1^st ‘𝑏) substr ⟨(2^nd ‘𝑏), (♯‘(1^st ‘𝑏))⟩)⟩ ↔ 𝑏 = ⟨((1^st ‘𝑎) ++ (2^nd ‘𝑎)), (♯‘(1^st ‘𝑎))⟩))
142	1, 39, 63, 141	f1ocnv2d 7670	. . 3 ⊢ (𝜑 → (𝐹:(Word 𝐴 × Word 𝐴)–1-1-onto→𝑈 ∧ ^◡𝐹 = (𝑏 ∈ 𝑈 ↦ ⟨((1^st ‘𝑏) prefix (2^nd ‘𝑏)), ((1^st ‘𝑏) substr ⟨(2^nd ‘𝑏), (♯‘(1^st ‘𝑏))⟩)⟩)))
143	142	simpld 500	. 2 ⊢ (𝜑 → 𝐹:(Word 𝐴 × Word 𝐴)–1-1-onto→𝑈)
144	142	simprd 501	. . 3 ⊢ (𝜑 → ^◡𝐹 = (𝑏 ∈ 𝑈 ↦ ⟨((1^st ‘𝑏) prefix (2^nd ‘𝑏)), ((1^st ‘𝑏) substr ⟨(2^nd ‘𝑏), (♯‘(1^st ‘𝑏))⟩)⟩))
145		gsumwrd2dccatlem.g	. . 3 ⊢ 𝐺 = (𝑏 ∈ 𝑈 ↦ ⟨((1^st ‘𝑏) prefix (2^nd ‘𝑏)), ((1^st ‘𝑏) substr ⟨(2^nd ‘𝑏), (♯‘(1^st ‘𝑏))⟩)⟩)
146	144, 145	eqtr4di 2813	. 2 ⊢ (𝜑 → ^◡𝐹 = 𝐺)
147	143, 146	jca 521	1 ⊢ (𝜑 → (𝐹:(Word 𝐴 × Word 𝐴)–1-1-onto→𝑈 ∧ ^◡𝐹 = 𝐺))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 = wceq 1570 ∃wex 1812 ∈ wcel 2145 ∃wrex 3086 ⊆ wss 3899 {csn 4584 ⟨cop 4590 ∪ ciun 4951 class class class wbr 5103 ↦ cmpt 5186 × cxp 5653 ^◡ccnv 5654 –1-1-onto→wf1o 6534 ‘cfv 6535 (class class class)co 7416 1^st c1st 7990 2^nd c2nd 7991 0cc0 11149 + caddc 11152 ≤ cle 11293 ℕ₀cn0 12553 ...cfz 13586 ♯chash 14419 Word cword 14603 ++ cconcat 14660 substr csubstr 14733 prefix cpfx 14765

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2732 ax-rep 5232 ax-sep 5251 ax-nul 5263 ax-pow 5330 ax-pr 5398 ax-un 7742 ax-cnex 11205 ax-resscn 11206 ax-1cn 11207 ax-icn 11208 ax-addcl 11209 ax-addrcl 11210 ax-mulcl 11211 ax-mulrcl 11212 ax-mulcom 11213 ax-addass 11214 ax-mulass 11215 ax-distr 11216 ax-i2m1 11217 ax-1ne0 11218 ax-1rid 11219 ax-rnegex 11220 ax-rrecex 11221 ax-cnre 11222 ax-pre-lttri 11223 ax-pre-lttrn 11224 ax-pre-ltadd 11225 ax-pre-mulgt0 11226

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-nel 3062 df-ral 3077 df-rex 3087 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-op 4591 df-uni 4868 df-int 4908 df-iun 4953 df-br 5104 df-opab 5168 df-mpt 5187 df-tr 5213 df-id 5550 df-eprel 5555 df-po 5563 df-so 5564 df-fr 5608 df-we 5610 df-xp 5661 df-rel 5662 df-cnv 5663 df-co 5664 df-dm 5665 df-rn 5666 df-res 5667 df-ima 5668 df-pred 6301 df-ord 6362 df-on 6363 df-lim 6364 df-suc 6365 df-iota 6491 df-fun 6537 df-fn 6538 df-f 6539 df-f1 6540 df-fo 6541 df-f1o 6542 df-fv 6543 df-riota 7373 df-ov 7419 df-oprab 7420 df-mpo 7421 df-om 7869 df-1st 7992 df-2nd 7993 df-frecs 8285 df-wrecs 8316 df-recs 8365 df-rdg 8404 df-1o 8462 df-er 8703 df-en 8960 df-dom 8961 df-sdom 8962 df-fin 8963 df-card 9969 df-pnf 11294 df-mnf 11295 df-xr 11296 df-ltxr 11297 df-le 11298 df-sub 11492 df-neg 11493 df-nn 12283 df-n0 12554 df-z 12641 df-uz 12913 df-fz 13587 df-fzo 13735 df-hash 14420 df-word 14604 df-concat 14661 df-substr 14734 df-pfx 14766

This theorem is used by: gsumwrd2dccat 33550

W3C validator