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 33020

Description: Lemma for gsumwrd2dccat 33021. 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 4587	. . . . . . . . 9 ⊢ (𝑤 = ((1^st ‘𝑎) ++ (2^nd ‘𝑎)) → {𝑤} = {((1^st ‘𝑎) ++ (2^nd ‘𝑎))})
3		fveq2 6822	. . . . . . . . . 10 ⊢ (𝑤 = ((1^st ‘𝑎) ++ (2^nd ‘𝑎)) → (♯‘𝑤) = (♯‘((1^st ‘𝑎) ++ (2^nd ‘𝑎))))
4	3	oveq2d 7365	. . . . . . . . 9 ⊢ (𝑤 = ((1^st ‘𝑎) ++ (2^nd ‘𝑎)) → (0...(♯‘𝑤)) = (0...(♯‘((1^st ‘𝑎) ++ (2^nd ‘𝑎)))))
5	2, 4	xpeq12d 5650	. . . . . . . 8 ⊢ (𝑤 = ((1^st ‘𝑎) ++ (2^nd ‘𝑎)) → ({𝑤} × (0...(♯‘𝑤))) = ({((1^st ‘𝑎) ++ (2^nd ‘𝑎))} × (0...(♯‘((1^st ‘𝑎) ++ (2^nd ‘𝑎))))))
6	5	eleq2d 2814	. . . . . . 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 7956	. . . . . . . . 9 ⊢ (𝑎 ∈ (Word 𝐴 × Word 𝐴) → (1^st ‘𝑎) ∈ Word 𝐴)
8	7	adantl 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (1^st ‘𝑎) ∈ Word 𝐴)
9		xp2nd 7957	. . . . . . . . 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 7382	. . . . . . . . . 10 ⊢ ((1^st ‘𝑎) ++ (2^nd ‘𝑎)) ∈ V
14	13	snid 4614	. . . . . . . . 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 12483	. . . . . . . . 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 12497	. . . . . . . . 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 12497	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (♯‘(1^st ‘𝑎)) ∈ ℤ)
23	21	nn0ge0d 12448	. . . . . . . . 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 12448	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → 0 ≤ (♯‘(2^nd ‘𝑎)))
27	21	nn0red 12446	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (♯‘(1^st ‘𝑎)) ∈ ℝ)
28	25	nn0red 12446	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (♯‘(2^nd ‘𝑎)) ∈ ℝ)
29	27, 28	addge01d 11708	. . . . . . . . . . 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 5120	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (♯‘(1^st ‘𝑎)) ≤ (♯‘((1^st ‘𝑎) ++ (2^nd ‘𝑎))))
34	16, 19, 22, 23, 33	elfzd 13418	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (♯‘(1^st ‘𝑎)) ∈ (0...(♯‘((1^st ‘𝑎) ++ (2^nd ‘𝑎)))))
35	15, 34	opelxpd 5658	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → ⟨((1^st ‘𝑎) ++ (2^nd ‘𝑎)), (♯‘(1^st ‘𝑎))⟩ ∈ ({((1^st ‘𝑎) ++ (2^nd ‘𝑎))} × (0...(♯‘((1^st ‘𝑎) ++ (2^nd ‘𝑎))))))
36	6, 12, 35	rspcedvdw 3580	. . . . . 6 ⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → ∃𝑤 ∈ Word 𝐴⟨((1^st ‘𝑎) ++ (2^nd ‘𝑎)), (♯‘(1^st ‘𝑎))⟩ ∈ ({𝑤} × (0...(♯‘𝑤))))
37	36	eliund 4948	. . . . 5 ⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → ⟨((1^st ‘𝑎) ++ (2^nd ‘𝑎)), (♯‘(1^st ‘𝑎))⟩ ∈ ∪ 𝑤 ∈ Word 𝐴({𝑤} × (0...(♯‘𝑤))))
38		gsumwrd2dccatlem.u	. . . . 5 ⊢ 𝑈 = ∪ 𝑤 ∈ Word 𝐴({𝑤} × (0...(♯‘𝑤)))
39	37, 38	eleqtrrdi 2839	. . . 4 ⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → ⟨((1^st ‘𝑎) ++ (2^nd ‘𝑎)), (♯‘(1^st ‘𝑎))⟩ ∈ 𝑈)
40		simpr 484	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑏 ∈ ({𝑢} × (0...(♯‘𝑢)))) → 𝑏 ∈ ({𝑢} × (0...(♯‘𝑢))))
41		xp1st 7956	. . . . . . . . . 10 ⊢ (𝑏 ∈ ({𝑢} × (0...(♯‘𝑢))) → (1^st ‘𝑏) ∈ {𝑢})
42		elsni 4594	. . . . . . . . . 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 2828	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑏 ∈ ({𝑢} × (0...(♯‘𝑢)))) → (1^st ‘𝑏) ∈ Word 𝐴)
46	45	adantllr 719	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑏 ∈ ({𝑢} × (0...(♯‘𝑢)))) → (1^st ‘𝑏) ∈ Word 𝐴)
47	38	eleq2i 2820	. . . . . . . . . . 11 ⊢ (𝑏 ∈ 𝑈 ↔ 𝑏 ∈ ∪ 𝑤 ∈ Word 𝐴({𝑤} × (0...(♯‘𝑤))))
48	47	biimpi 216	. . . . . . . . . 10 ⊢ (𝑏 ∈ 𝑈 → 𝑏 ∈ ∪ 𝑤 ∈ Word 𝐴({𝑤} × (0...(♯‘𝑤))))
49	48	adantl 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝑈) → 𝑏 ∈ ∪ 𝑤 ∈ Word 𝐴({𝑤} × (0...(♯‘𝑤))))
50		eliun 4945	. . . . . . . . 9 ⊢ (𝑏 ∈ ∪ 𝑤 ∈ Word 𝐴({𝑤} × (0...(♯‘𝑤))) ↔ ∃𝑤 ∈ Word 𝐴𝑏 ∈ ({𝑤} × (0...(♯‘𝑤))))
51	49, 50	sylib 218	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝑈) → ∃𝑤 ∈ Word 𝐴𝑏 ∈ ({𝑤} × (0...(♯‘𝑤))))
52		sneq 4587	. . . . . . . . . . 11 ⊢ (𝑢 = 𝑤 → {𝑢} = {𝑤})
53		fveq2 6822	. . . . . . . . . . . 12 ⊢ (𝑢 = 𝑤 → (♯‘𝑢) = (♯‘𝑤))
54	53	oveq2d 7365	. . . . . . . . . . 11 ⊢ (𝑢 = 𝑤 → (0...(♯‘𝑢)) = (0...(♯‘𝑤)))
55	52, 54	xpeq12d 5650	. . . . . . . . . 10 ⊢ (𝑢 = 𝑤 → ({𝑢} × (0...(♯‘𝑢))) = ({𝑤} × (0...(♯‘𝑤))))
56	55	eleq2d 2814	. . . . . . . . 9 ⊢ (𝑢 = 𝑤 → (𝑏 ∈ ({𝑢} × (0...(♯‘𝑢))) ↔ 𝑏 ∈ ({𝑤} × (0...(♯‘𝑤)))))
57	56	cbvrexvw 3208	. . . . . . . 8 ⊢ (∃𝑢 ∈ Word 𝐴𝑏 ∈ ({𝑢} × (0...(♯‘𝑢))) ↔ ∃𝑤 ∈ Word 𝐴𝑏 ∈ ({𝑤} × (0...(♯‘𝑤))))
58	51, 57	sylibr 234	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝑈) → ∃𝑢 ∈ Word 𝐴𝑏 ∈ ({𝑢} × (0...(♯‘𝑢))))
59	46, 58	r19.29a 3137	. . . . . 6 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝑈) → (1^st ‘𝑏) ∈ Word 𝐴)
60		pfxcl 14584	. . . . . 6 ⊢ ((1^st ‘𝑏) ∈ Word 𝐴 → ((1^st ‘𝑏) prefix (2^nd ‘𝑏)) ∈ Word 𝐴)
61	59, 60	syl 17	. . . . 5 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝑈) → ((1^st ‘𝑏) prefix (2^nd ‘𝑏)) ∈ Word 𝐴)
62		swrdcl 14552	. . . . . 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 5658	. . . 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 5780	. . . . . . . . . 10 ⊢ (𝑏 ∈ ∪ 𝑤 ∈ Word 𝐴({𝑤} × (0...(♯‘𝑤))) ↔ ∃𝑤∃𝑛(𝑏 = ⟨𝑤, 𝑛⟩ ∧ (𝑤 ∈ Word 𝐴 ∧ 𝑛 ∈ (0...(♯‘𝑤)))))
67	65, 66	sylib 218	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → ∃𝑤∃𝑛(𝑏 = ⟨𝑤, 𝑛⟩ ∧ (𝑤 ∈ Word 𝐴 ∧ 𝑛 ∈ (0...(♯‘𝑤)))))
68		opeq1 4824	. . . . . . . . . . . . 13 ⊢ (𝑢 = 𝑤 → ⟨𝑢, 𝑛⟩ = ⟨𝑤, 𝑛⟩)
69	68	eqeq2d 2740	. . . . . . . . . . . 12 ⊢ (𝑢 = 𝑤 → (𝑏 = ⟨𝑢, 𝑛⟩ ↔ 𝑏 = ⟨𝑤, 𝑛⟩))
70		eleq1w 2811	. . . . . . . . . . . . 13 ⊢ (𝑢 = 𝑤 → (𝑢 ∈ Word 𝐴 ↔ 𝑤 ∈ Word 𝐴))
71	54	eleq2d 2814	. . . . . . . . . . . . 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 1921	. . . . . . . . . 10 ⊢ (𝑢 = 𝑤 → (∃𝑛(𝑏 = ⟨𝑢, 𝑛⟩ ∧ (𝑢 ∈ Word 𝐴 ∧ 𝑛 ∈ (0...(♯‘𝑢)))) ↔ ∃𝑛(𝑏 = ⟨𝑤, 𝑛⟩ ∧ (𝑤 ∈ Word 𝐴 ∧ 𝑛 ∈ (0...(♯‘𝑤))))))
75	74	cbvexvw 2037	. . . . . . . . 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 7367	. . . . . . . . . . . . . . . . 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 7934	. . . . . . . . . . . . . . . . . . . 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 2828	. . . . . . . . . . . . . . . . . 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 7935	. . . . . . . . . . . . . . . . . . . 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 2735	. . . . . . . . . . . . . . . . . . . . . 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 7365	. . . . . . . . . . . . . . . . . . . 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 2830	. . . . . . . . . . . . . . . . . . 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 2828	. . . . . . . . . . . . . . . . . 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 14616	. . . . . . . . . . . . . . . . . 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 2765	. . . . . . . . . . . . . . . 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 14590	. . . . . . . . . . . . . . . . . 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 2765	. . . . . . . . . . . . . . . 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 7367	. . . . . . . . . . . . . . . . 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 14608	. . . . . . . . . . . . . . . . . 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 2765	. . . . . . . . . . . . . . . 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 2764	. . . . . . . . . . . . . . . . . . 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 4832	. . . . . . . . . . . . . . . . . 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 7367	. . . . . . . . . . . . . . . . 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 14576	. . . . . . . . . . . . . . . . . 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 2765	. . . . . . . . . . . . . . . 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 1933	. . . . . . . . 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 1935	. . . . . . 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 7966	. . . . . . . 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 4759	. . . . . . . . . . . . 13 ⊢ (𝑤 ∈ Word 𝐴 → {𝑤} ⊆ Word 𝐴)
131	130	adantl 481	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) ∧ 𝑤 ∈ Word 𝐴) → {𝑤} ⊆ Word 𝐴)
132		fz0ssnn0 13525	. . . . . . . . . . . 12 ⊢ (0...(♯‘𝑤)) ⊆ ℕ₀
133		xpss12 5634	. . . . . . . . . . . 12 ⊢ (({𝑤} ⊆ Word 𝐴 ∧ (0...(♯‘𝑤)) ⊆ ℕ₀) → ({𝑤} × (0...(♯‘𝑤))) ⊆ (Word 𝐴 × ℕ₀))
134	131, 132, 133	sylancl 586	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) ∧ 𝑤 ∈ Word 𝐴) → ({𝑤} × (0...(♯‘𝑤))) ⊆ (Word 𝐴 × ℕ₀))
135	134	iunssd 4999	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → ∪ 𝑤 ∈ Word 𝐴({𝑤} × (0...(♯‘𝑤))) ⊆ (Word 𝐴 × ℕ₀))
136	135	adantlr 715	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → ∪ 𝑤 ∈ Word 𝐴({𝑤} × (0...(♯‘𝑤))) ⊆ (Word 𝐴 × ℕ₀))
137	136, 65	sseldd 3936	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → 𝑏 ∈ (Word 𝐴 × ℕ₀))
138		eqop 7966	. . . . . . . 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 7602	. . 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 2782	. 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 1540 ∃wex 1779 ∈ wcel 2109 ∃wrex 3053 ⊆ wss 3903 {csn 4577 ⟨cop 4583 ∪ ciun 4941 class class class wbr 5092 ↦ cmpt 5173 × cxp 5617 ^◡ccnv 5618 –1-1-onto→wf1o 6481 ‘cfv 6482 (class class class)co 7349 1^st c1st 7922 2^nd c2nd 7923 0cc0 11009 + caddc 11012 ≤ cle 11150 ℕ₀cn0 12384 ...cfz 13410 ♯chash 14237 Word cword 14420 ++ cconcat 14477 substr csubstr 14547 prefix cpfx 14577

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-rep 5218 ax-sep 5235 ax-nul 5245 ax-pow 5304 ax-pr 5371 ax-un 7671 ax-cnex 11065 ax-resscn 11066 ax-1cn 11067 ax-icn 11068 ax-addcl 11069 ax-addrcl 11070 ax-mulcl 11071 ax-mulrcl 11072 ax-mulcom 11073 ax-addass 11074 ax-mulass 11075 ax-distr 11076 ax-i2m1 11077 ax-1ne0 11078 ax-1rid 11079 ax-rnegex 11080 ax-rrecex 11081 ax-cnre 11082 ax-pre-lttri 11083 ax-pre-lttrn 11084 ax-pre-ltadd 11085 ax-pre-mulgt0 11086

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-nel 3030 df-ral 3045 df-rex 3054 df-reu 3344 df-rab 3395 df-v 3438 df-sbc 3743 df-csb 3852 df-dif 3906 df-un 3908 df-in 3910 df-ss 3920 df-pss 3923 df-nul 4285 df-if 4477 df-pw 4553 df-sn 4578 df-pr 4580 df-op 4584 df-uni 4859 df-int 4897 df-iun 4943 df-br 5093 df-opab 5155 df-mpt 5174 df-tr 5200 df-id 5514 df-eprel 5519 df-po 5527 df-so 5528 df-fr 5572 df-we 5574 df-xp 5625 df-rel 5626 df-cnv 5627 df-co 5628 df-dm 5629 df-rn 5630 df-res 5631 df-ima 5632 df-pred 6249 df-ord 6310 df-on 6311 df-lim 6312 df-suc 6313 df-iota 6438 df-fun 6484 df-fn 6485 df-f 6486 df-f1 6487 df-fo 6488 df-f1o 6489 df-fv 6490 df-riota 7306 df-ov 7352 df-oprab 7353 df-mpo 7354 df-om 7800 df-1st 7924 df-2nd 7925 df-frecs 8214 df-wrecs 8245 df-recs 8294 df-rdg 8332 df-1o 8388 df-er 8625 df-en 8873 df-dom 8874 df-sdom 8875 df-fin 8876 df-card 9835 df-pnf 11151 df-mnf 11152 df-xr 11153 df-ltxr 11154 df-le 11155 df-sub 11349 df-neg 11350 df-nn 12129 df-n0 12385 df-z 12472 df-uz 12736 df-fz 13411 df-fzo 13558 df-hash 14238 df-word 14421 df-concat 14478 df-substr 14548 df-pfx 14578

This theorem is referenced by: gsumwrd2dccat 33021

W3C validator