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 33157

Description: Lemma for gsumwrd2dccat 33158. 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 4578	. . . . . . . . 9 ⊢ (𝑤 = ((1^st ‘𝑎) ++ (2^nd ‘𝑎)) → {𝑤} = {((1^st ‘𝑎) ++ (2^nd ‘𝑎))})
3		fveq2 6836	. . . . . . . . . 10 ⊢ (𝑤 = ((1^st ‘𝑎) ++ (2^nd ‘𝑎)) → (♯‘𝑤) = (♯‘((1^st ‘𝑎) ++ (2^nd ‘𝑎))))
4	3	oveq2d 7378	. . . . . . . . 9 ⊢ (𝑤 = ((1^st ‘𝑎) ++ (2^nd ‘𝑎)) → (0...(♯‘𝑤)) = (0...(♯‘((1^st ‘𝑎) ++ (2^nd ‘𝑎)))))
5	2, 4	xpeq12d 5657	. . . . . . . 8 ⊢ (𝑤 = ((1^st ‘𝑎) ++ (2^nd ‘𝑎)) → ({𝑤} × (0...(♯‘𝑤))) = ({((1^st ‘𝑎) ++ (2^nd ‘𝑎))} × (0...(♯‘((1^st ‘𝑎) ++ (2^nd ‘𝑎))))))
6	5	eleq2d 2823	. . . . . . 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 7969	. . . . . . . . 9 ⊢ (𝑎 ∈ (Word 𝐴 × Word 𝐴) → (1^st ‘𝑎) ∈ Word 𝐴)
8	7	adantl 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (1^st ‘𝑎) ∈ Word 𝐴)
9		xp2nd 7970	. . . . . . . . 9 ⊢ (𝑎 ∈ (Word 𝐴 × Word 𝐴) → (2^nd ‘𝑎) ∈ Word 𝐴)
10	9	adantl 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (2^nd ‘𝑎) ∈ Word 𝐴)
11		ccatcl 14531	. . . . . . . 8 ⊢ (((1^st ‘𝑎) ∈ Word 𝐴 ∧ (2^nd ‘𝑎) ∈ Word 𝐴) → ((1^st ‘𝑎) ++ (2^nd ‘𝑎)) ∈ Word 𝐴)
12	8, 10, 11	syl2anc 585	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → ((1^st ‘𝑎) ++ (2^nd ‘𝑎)) ∈ Word 𝐴)
13		ovex 7395	. . . . . . . . . 10 ⊢ ((1^st ‘𝑎) ++ (2^nd ‘𝑎)) ∈ V
14	13	snid 4607	. . . . . . . . 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 12531	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → 0 ∈ ℤ)
17		lencl 14490	. . . . . . . . . . 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 12544	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (♯‘((1^st ‘𝑎) ++ (2^nd ‘𝑎))) ∈ ℤ)
20		lencl 14490	. . . . . . . . . . 11 ⊢ ((1^st ‘𝑎) ∈ Word 𝐴 → (♯‘(1^st ‘𝑎)) ∈ ℕ₀)
21	8, 20	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (♯‘(1^st ‘𝑎)) ∈ ℕ₀)
22	21	nn0zd 12544	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (♯‘(1^st ‘𝑎)) ∈ ℤ)
23	21	nn0ge0d 12496	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → 0 ≤ (♯‘(1^st ‘𝑎)))
24		lencl 14490	. . . . . . . . . . . . 13 ⊢ ((2^nd ‘𝑎) ∈ Word 𝐴 → (♯‘(2^nd ‘𝑎)) ∈ ℕ₀)
25	10, 24	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (♯‘(2^nd ‘𝑎)) ∈ ℕ₀)
26	25	nn0ge0d 12496	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → 0 ≤ (♯‘(2^nd ‘𝑎)))
27	21	nn0red 12494	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (♯‘(1^st ‘𝑎)) ∈ ℝ)
28	25	nn0red 12494	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (♯‘(2^nd ‘𝑎)) ∈ ℝ)
29	27, 28	addge01d 11733	. . . . . . . . . . 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 14532	. . . . . . . . . . 11 ⊢ (((1^st ‘𝑎) ∈ Word 𝐴 ∧ (2^nd ‘𝑎) ∈ Word 𝐴) → (♯‘((1^st ‘𝑎) ++ (2^nd ‘𝑎))) = ((♯‘(1^st ‘𝑎)) + (♯‘(2^nd ‘𝑎))))
32	8, 10, 31	syl2anc 585	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (♯‘((1^st ‘𝑎) ++ (2^nd ‘𝑎))) = ((♯‘(1^st ‘𝑎)) + (♯‘(2^nd ‘𝑎))))
33	30, 32	breqtrrd 5114	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (♯‘(1^st ‘𝑎)) ≤ (♯‘((1^st ‘𝑎) ++ (2^nd ‘𝑎))))
34	16, 19, 22, 23, 33	elfzd 13464	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (♯‘(1^st ‘𝑎)) ∈ (0...(♯‘((1^st ‘𝑎) ++ (2^nd ‘𝑎)))))
35	15, 34	opelxpd 5665	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → ⟨((1^st ‘𝑎) ++ (2^nd ‘𝑎)), (♯‘(1^st ‘𝑎))⟩ ∈ ({((1^st ‘𝑎) ++ (2^nd ‘𝑎))} × (0...(♯‘((1^st ‘𝑎) ++ (2^nd ‘𝑎))))))
36	6, 12, 35	rspcedvdw 3568	. . . . . 6 ⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → ∃𝑤 ∈ Word 𝐴⟨((1^st ‘𝑎) ++ (2^nd ‘𝑎)), (♯‘(1^st ‘𝑎))⟩ ∈ ({𝑤} × (0...(♯‘𝑤))))
37	36	eliund 4941	. . . . 5 ⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → ⟨((1^st ‘𝑎) ++ (2^nd ‘𝑎)), (♯‘(1^st ‘𝑎))⟩ ∈ ∪ 𝑤 ∈ Word 𝐴({𝑤} × (0...(♯‘𝑤))))
38		gsumwrd2dccatlem.u	. . . . 5 ⊢ 𝑈 = ∪ 𝑤 ∈ Word 𝐴({𝑤} × (0...(♯‘𝑤)))
39	37, 38	eleqtrrdi 2848	. . . 4 ⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → ⟨((1^st ‘𝑎) ++ (2^nd ‘𝑎)), (♯‘(1^st ‘𝑎))⟩ ∈ 𝑈)
40		simpr 484	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑏 ∈ ({𝑢} × (0...(♯‘𝑢)))) → 𝑏 ∈ ({𝑢} × (0...(♯‘𝑢))))
41		xp1st 7969	. . . . . . . . . 10 ⊢ (𝑏 ∈ ({𝑢} × (0...(♯‘𝑢))) → (1^st ‘𝑏) ∈ {𝑢})
42		elsni 4585	. . . . . . . . . 10 ⊢ ((1^st ‘𝑏) ∈ {𝑢} → (1^st ‘𝑏) = 𝑢)
43	40, 41, 42	3syl 18	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑏 ∈ ({𝑢} × (0...(♯‘𝑢)))) → (1^st ‘𝑏) = 𝑢)
44		simplr 769	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑏 ∈ ({𝑢} × (0...(♯‘𝑢)))) → 𝑢 ∈ Word 𝐴)
45	43, 44	eqeltrd 2837	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑏 ∈ ({𝑢} × (0...(♯‘𝑢)))) → (1^st ‘𝑏) ∈ Word 𝐴)
46	45	adantllr 720	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑏 ∈ ({𝑢} × (0...(♯‘𝑢)))) → (1^st ‘𝑏) ∈ Word 𝐴)
47	38	eleq2i 2829	. . . . . . . . . . 11 ⊢ (𝑏 ∈ 𝑈 ↔ 𝑏 ∈ ∪ 𝑤 ∈ Word 𝐴({𝑤} × (0...(♯‘𝑤))))
48	47	biimpi 216	. . . . . . . . . 10 ⊢ (𝑏 ∈ 𝑈 → 𝑏 ∈ ∪ 𝑤 ∈ Word 𝐴({𝑤} × (0...(♯‘𝑤))))
49	48	adantl 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝑈) → 𝑏 ∈ ∪ 𝑤 ∈ Word 𝐴({𝑤} × (0...(♯‘𝑤))))
50		eliun 4938	. . . . . . . . 9 ⊢ (𝑏 ∈ ∪ 𝑤 ∈ Word 𝐴({𝑤} × (0...(♯‘𝑤))) ↔ ∃𝑤 ∈ Word 𝐴𝑏 ∈ ({𝑤} × (0...(♯‘𝑤))))
51	49, 50	sylib 218	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝑈) → ∃𝑤 ∈ Word 𝐴𝑏 ∈ ({𝑤} × (0...(♯‘𝑤))))
52		sneq 4578	. . . . . . . . . . 11 ⊢ (𝑢 = 𝑤 → {𝑢} = {𝑤})
53		fveq2 6836	. . . . . . . . . . . 12 ⊢ (𝑢 = 𝑤 → (♯‘𝑢) = (♯‘𝑤))
54	53	oveq2d 7378	. . . . . . . . . . 11 ⊢ (𝑢 = 𝑤 → (0...(♯‘𝑢)) = (0...(♯‘𝑤)))
55	52, 54	xpeq12d 5657	. . . . . . . . . 10 ⊢ (𝑢 = 𝑤 → ({𝑢} × (0...(♯‘𝑢))) = ({𝑤} × (0...(♯‘𝑤))))
56	55	eleq2d 2823	. . . . . . . . 9 ⊢ (𝑢 = 𝑤 → (𝑏 ∈ ({𝑢} × (0...(♯‘𝑢))) ↔ 𝑏 ∈ ({𝑤} × (0...(♯‘𝑤)))))
57	56	cbvrexvw 3217	. . . . . . . 8 ⊢ (∃𝑢 ∈ Word 𝐴𝑏 ∈ ({𝑢} × (0...(♯‘𝑢))) ↔ ∃𝑤 ∈ Word 𝐴𝑏 ∈ ({𝑤} × (0...(♯‘𝑤))))
58	51, 57	sylibr 234	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝑈) → ∃𝑢 ∈ Word 𝐴𝑏 ∈ ({𝑢} × (0...(♯‘𝑢))))
59	46, 58	r19.29a 3146	. . . . . 6 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝑈) → (1^st ‘𝑏) ∈ Word 𝐴)
60		pfxcl 14635	. . . . . 6 ⊢ ((1^st ‘𝑏) ∈ Word 𝐴 → ((1^st ‘𝑏) prefix (2^nd ‘𝑏)) ∈ Word 𝐴)
61	59, 60	syl 17	. . . . 5 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝑈) → ((1^st ‘𝑏) prefix (2^nd ‘𝑏)) ∈ Word 𝐴)
62		swrdcl 14603	. . . . . 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 5665	. . . 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 5788	. . . . . . . . . 10 ⊢ (𝑏 ∈ ∪ 𝑤 ∈ Word 𝐴({𝑤} × (0...(♯‘𝑤))) ↔ ∃𝑤∃𝑛(𝑏 = ⟨𝑤, 𝑛⟩ ∧ (𝑤 ∈ Word 𝐴 ∧ 𝑛 ∈ (0...(♯‘𝑤)))))
67	65, 66	sylib 218	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → ∃𝑤∃𝑛(𝑏 = ⟨𝑤, 𝑛⟩ ∧ (𝑤 ∈ Word 𝐴 ∧ 𝑛 ∈ (0...(♯‘𝑤)))))
68		opeq1 4817	. . . . . . . . . . . . 13 ⊢ (𝑢 = 𝑤 → ⟨𝑢, 𝑛⟩ = ⟨𝑤, 𝑛⟩)
69	68	eqeq2d 2748	. . . . . . . . . . . 12 ⊢ (𝑢 = 𝑤 → (𝑏 = ⟨𝑢, 𝑛⟩ ↔ 𝑏 = ⟨𝑤, 𝑛⟩))
70		eleq1w 2820	. . . . . . . . . . . . 13 ⊢ (𝑢 = 𝑤 → (𝑢 ∈ Word 𝐴 ↔ 𝑤 ∈ Word 𝐴))
71	54	eleq2d 2823	. . . . . . . . . . . . 13 ⊢ (𝑢 = 𝑤 → (𝑛 ∈ (0...(♯‘𝑢)) ↔ 𝑛 ∈ (0...(♯‘𝑤))))
72	70, 71	anbi12d 633	. . . . . . . . . . . 12 ⊢ (𝑢 = 𝑤 → ((𝑢 ∈ Word 𝐴 ∧ 𝑛 ∈ (0...(♯‘𝑢))) ↔ (𝑤 ∈ Word 𝐴 ∧ 𝑛 ∈ (0...(♯‘𝑤)))))
73	69, 72	anbi12d 633	. . . . . . . . . . 11 ⊢ (𝑢 = 𝑤 → ((𝑏 = ⟨𝑢, 𝑛⟩ ∧ (𝑢 ∈ Word 𝐴 ∧ 𝑛 ∈ (0...(♯‘𝑢)))) ↔ (𝑏 = ⟨𝑤, 𝑛⟩ ∧ (𝑤 ∈ Word 𝐴 ∧ 𝑛 ∈ (0...(♯‘𝑤))))))
74	73	exbidv 1923	. . . . . . . . . 10 ⊢ (𝑢 = 𝑤 → (∃𝑛(𝑏 = ⟨𝑢, 𝑛⟩ ∧ (𝑢 ∈ Word 𝐴 ∧ 𝑛 ∈ (0...(♯‘𝑢)))) ↔ ∃𝑛(𝑏 = ⟨𝑤, 𝑛⟩ ∧ (𝑤 ∈ Word 𝐴 ∧ 𝑛 ∈ (0...(♯‘𝑤))))))
75	74	cbvexvw 2039	. . . . . . . . 9 ⊢ (∃𝑢∃𝑛(𝑏 = ⟨𝑢, 𝑛⟩ ∧ (𝑢 ∈ Word 𝐴 ∧ 𝑛 ∈ (0...(♯‘𝑢)))) ↔ ∃𝑤∃𝑛(𝑏 = ⟨𝑤, 𝑛⟩ ∧ (𝑤 ∈ Word 𝐴 ∧ 𝑛 ∈ (0...(♯‘𝑤)))))
76	67, 75	sylibr 234	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → ∃𝑢∃𝑛(𝑏 = ⟨𝑢, 𝑛⟩ ∧ (𝑢 ∈ Word 𝐴 ∧ 𝑛 ∈ (0...(♯‘𝑢)))))
77		simplr 769	. . . . . . . . . . . . . . . . . 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 7380	. . . . . . . . . . . . . . . . 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 3434	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑢 ∈ V
81		vex 3434	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑛 ∈ V
82	80, 81	op1std 7947	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑏 = ⟨𝑢, 𝑛⟩ → (1^st ‘𝑏) = 𝑢)
83	82	ad5antlr 736	. . . . . . . . . . . . . . . . . . 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 784	. . . . . . . . . . . . . . . . . . 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 2837	. . . . . . . . . . . . . . . . . 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 7948	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑏 = ⟨𝑢, 𝑛⟩ → (2^nd ‘𝑏) = 𝑛)
87	86	ad5antlr 736	. . . . . . . . . . . . . . . . . . 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 776	. . . . . . . . . . . . . . . . . . . 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 2743	. . . . . . . . . . . . . . . . . . . . . 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 6840	. . . . . . . . . . . . . . . . . . . . 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 7378	. . . . . . . . . . . . . . . . . . . 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 2839	. . . . . . . . . . . . . . . . . . 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 2837	. . . . . . . . . . . . . . . . . 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 14667	. . . . . . . . . . . . . . . . . 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 585	. . . . . . . . . . . . . . . . 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 2773	. . . . . . . . . . . . . . . 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 6840	. . . . . . . . . . . . . . . . 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 14641	. . . . . . . . . . . . . . . . . 18 ⊢ (((1^st ‘𝑏) ∈ Word 𝐴 ∧ (2^nd ‘𝑏) ∈ (0...(♯‘(1^st ‘𝑏)))) → (♯‘((1^st ‘𝑏) prefix (2^nd ‘𝑏))) = (2^nd ‘𝑏))
99	85, 93, 98	syl2anc 585	. . . . . . . . . . . . . . . . 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 2773	. . . . . . . . . . . . . . . 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 769	. . . . . . . . . . . . . . . . . 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 7380	. . . . . . . . . . . . . . . . 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 735	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) ∧ 𝑏 = ⟨𝑢, 𝑛⟩) ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑛 ∈ (0...(♯‘𝑢))) ∧ (1^st ‘𝑏) = ((1^st ‘𝑎) ++ (2^nd ‘𝑎))) ∧ (2^nd ‘𝑏) = (♯‘(1^st ‘𝑎))) → (1^st ‘𝑎) ∈ Word 𝐴)
107	10	ad5antr 735	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) ∧ 𝑏 = ⟨𝑢, 𝑛⟩) ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑛 ∈ (0...(♯‘𝑢))) ∧ (1^st ‘𝑏) = ((1^st ‘𝑎) ++ (2^nd ‘𝑎))) ∧ (2^nd ‘𝑏) = (♯‘(1^st ‘𝑎))) → (2^nd ‘𝑎) ∈ Word 𝐴)
108		pfxccat1 14659	. . . . . . . . . . . . . . . . . 18 ⊢ (((1^st ‘𝑎) ∈ Word 𝐴 ∧ (2^nd ‘𝑎) ∈ Word 𝐴) → (((1^st ‘𝑎) ++ (2^nd ‘𝑎)) prefix (♯‘(1^st ‘𝑎))) = (1^st ‘𝑎))
109	106, 107, 108	syl2anc 585	. . . . . . . . . . . . . . . . 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 2773	. . . . . . . . . . . . . . . 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 6840	. . . . . . . . . . . . . . . . . . . 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 585	. . . . . . . . . . . . . . . . . . . 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 2772	. . . . . . . . . . . . . . . . . . 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 4825	. . . . . . . . . . . . . . . . . 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 7380	. . . . . . . . . . . . . . . . 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 14627	. . . . . . . . . . . . . . . . . 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 585	. . . . . . . . . . . . . . . . 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 2773	. . . . . . . . . . . . . . . 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 801	. . . . . . . . . . . . 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 716	. . . . . . . . . 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 1935	. . . . . . . . 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 1937	. . . . . . 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 7979	. . . . . . . 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 4752	. . . . . . . . . . . . 13 ⊢ (𝑤 ∈ Word 𝐴 → {𝑤} ⊆ Word 𝐴)
131	130	adantl 481	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) ∧ 𝑤 ∈ Word 𝐴) → {𝑤} ⊆ Word 𝐴)
132		fz0ssnn0 13571	. . . . . . . . . . . 12 ⊢ (0...(♯‘𝑤)) ⊆ ℕ₀
133		xpss12 5641	. . . . . . . . . . . 12 ⊢ (({𝑤} ⊆ Word 𝐴 ∧ (0...(♯‘𝑤)) ⊆ ℕ₀) → ({𝑤} × (0...(♯‘𝑤))) ⊆ (Word 𝐴 × ℕ₀))
134	131, 132, 133	sylancl 587	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) ∧ 𝑤 ∈ Word 𝐴) → ({𝑤} × (0...(♯‘𝑤))) ⊆ (Word 𝐴 × ℕ₀))
135	134	iunssd 4994	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → ∪ 𝑤 ∈ Word 𝐴({𝑤} × (0...(♯‘𝑤))) ⊆ (Word 𝐴 × ℕ₀))
136	135	adantlr 716	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → ∪ 𝑤 ∈ Word 𝐴({𝑤} × (0...(♯‘𝑤))) ⊆ (Word 𝐴 × ℕ₀))
137	136, 65	sseldd 3923	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → 𝑏 ∈ (Word 𝐴 × ℕ₀))
138		eqop 7979	. . . . . . . 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 653	. . . . 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 7615	. . 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 2790	. 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 1542 ∃wex 1781 ∈ wcel 2114 ∃wrex 3062 ⊆ wss 3890 {csn 4568 ⟨cop 4574 ∪ ciun 4934 class class class wbr 5086 ↦ cmpt 5167 × cxp 5624 ^◡ccnv 5625 –1-1-onto→wf1o 6493 ‘cfv 6494 (class class class)co 7362 1^st c1st 7935 2^nd c2nd 7936 0cc0 11033 + caddc 11036 ≤ cle 11175 ℕ₀cn0 12432 ...cfz 13456 ♯chash 14287 Word cword 14470 ++ cconcat 14527 substr csubstr 14598 prefix cpfx 14628

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-rep 5213 ax-sep 5232 ax-nul 5242 ax-pow 5304 ax-pr 5372 ax-un 7684 ax-cnex 11089 ax-resscn 11090 ax-1cn 11091 ax-icn 11092 ax-addcl 11093 ax-addrcl 11094 ax-mulcl 11095 ax-mulrcl 11096 ax-mulcom 11097 ax-addass 11098 ax-mulass 11099 ax-distr 11100 ax-i2m1 11101 ax-1ne0 11102 ax-1rid 11103 ax-rnegex 11104 ax-rrecex 11105 ax-cnre 11106 ax-pre-lttri 11107 ax-pre-lttrn 11108 ax-pre-ltadd 11109 ax-pre-mulgt0 11110

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3063 df-reu 3344 df-rab 3391 df-v 3432 df-sbc 3730 df-csb 3839 df-dif 3893 df-un 3895 df-in 3897 df-ss 3907 df-pss 3910 df-nul 4275 df-if 4468 df-pw 4544 df-sn 4569 df-pr 4571 df-op 4575 df-uni 4852 df-int 4891 df-iun 4936 df-br 5087 df-opab 5149 df-mpt 5168 df-tr 5194 df-id 5521 df-eprel 5526 df-po 5534 df-so 5535 df-fr 5579 df-we 5581 df-xp 5632 df-rel 5633 df-cnv 5634 df-co 5635 df-dm 5636 df-rn 5637 df-res 5638 df-ima 5639 df-pred 6261 df-ord 6322 df-on 6323 df-lim 6324 df-suc 6325 df-iota 6450 df-fun 6496 df-fn 6497 df-f 6498 df-f1 6499 df-fo 6500 df-f1o 6501 df-fv 6502 df-riota 7319 df-ov 7365 df-oprab 7366 df-mpo 7367 df-om 7813 df-1st 7937 df-2nd 7938 df-frecs 8226 df-wrecs 8257 df-recs 8306 df-rdg 8344 df-1o 8400 df-er 8638 df-en 8889 df-dom 8890 df-sdom 8891 df-fin 8892 df-card 9858 df-pnf 11176 df-mnf 11177 df-xr 11178 df-ltxr 11179 df-le 11180 df-sub 11374 df-neg 11375 df-nn 12170 df-n0 12433 df-z 12520 df-uz 12784 df-fz 13457 df-fzo 13604 df-hash 14288 df-word 14471 df-concat 14528 df-substr 14599 df-pfx 14629

This theorem is referenced by: gsumwrd2dccat 33158

W3C validator