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 33013

Description: Lemma for gsumwrd2dccat 33014. 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 4602	. . . . . . . . 9 ⊢ (𝑤 = ((1^st ‘𝑎) ++ (2^nd ‘𝑎)) → {𝑤} = {((1^st ‘𝑎) ++ (2^nd ‘𝑎))})
3		fveq2 6861	. . . . . . . . . 10 ⊢ (𝑤 = ((1^st ‘𝑎) ++ (2^nd ‘𝑎)) → (♯‘𝑤) = (♯‘((1^st ‘𝑎) ++ (2^nd ‘𝑎))))
4	3	oveq2d 7406	. . . . . . . . 9 ⊢ (𝑤 = ((1^st ‘𝑎) ++ (2^nd ‘𝑎)) → (0...(♯‘𝑤)) = (0...(♯‘((1^st ‘𝑎) ++ (2^nd ‘𝑎)))))
5	2, 4	xpeq12d 5672	. . . . . . . 8 ⊢ (𝑤 = ((1^st ‘𝑎) ++ (2^nd ‘𝑎)) → ({𝑤} × (0...(♯‘𝑤))) = ({((1^st ‘𝑎) ++ (2^nd ‘𝑎))} × (0...(♯‘((1^st ‘𝑎) ++ (2^nd ‘𝑎))))))
6	5	eleq2d 2815	. . . . . . 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 8003	. . . . . . . . 9 ⊢ (𝑎 ∈ (Word 𝐴 × Word 𝐴) → (1^st ‘𝑎) ∈ Word 𝐴)
8	7	adantl 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (1^st ‘𝑎) ∈ Word 𝐴)
9		xp2nd 8004	. . . . . . . . 9 ⊢ (𝑎 ∈ (Word 𝐴 × Word 𝐴) → (2^nd ‘𝑎) ∈ Word 𝐴)
10	9	adantl 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (2^nd ‘𝑎) ∈ Word 𝐴)
11		ccatcl 14546	. . . . . . . 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 7423	. . . . . . . . . 10 ⊢ ((1^st ‘𝑎) ++ (2^nd ‘𝑎)) ∈ V
14	13	snid 4629	. . . . . . . . 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 12548	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → 0 ∈ ℤ)
17		lencl 14505	. . . . . . . . . . 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 12562	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (♯‘((1^st ‘𝑎) ++ (2^nd ‘𝑎))) ∈ ℤ)
20		lencl 14505	. . . . . . . . . . 11 ⊢ ((1^st ‘𝑎) ∈ Word 𝐴 → (♯‘(1^st ‘𝑎)) ∈ ℕ₀)
21	8, 20	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (♯‘(1^st ‘𝑎)) ∈ ℕ₀)
22	21	nn0zd 12562	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (♯‘(1^st ‘𝑎)) ∈ ℤ)
23	21	nn0ge0d 12513	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → 0 ≤ (♯‘(1^st ‘𝑎)))
24		lencl 14505	. . . . . . . . . . . . 13 ⊢ ((2^nd ‘𝑎) ∈ Word 𝐴 → (♯‘(2^nd ‘𝑎)) ∈ ℕ₀)
25	10, 24	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (♯‘(2^nd ‘𝑎)) ∈ ℕ₀)
26	25	nn0ge0d 12513	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → 0 ≤ (♯‘(2^nd ‘𝑎)))
27	21	nn0red 12511	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (♯‘(1^st ‘𝑎)) ∈ ℝ)
28	25	nn0red 12511	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (♯‘(2^nd ‘𝑎)) ∈ ℝ)
29	27, 28	addge01d 11773	. . . . . . . . . . 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 14547	. . . . . . . . . . 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 5138	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (♯‘(1^st ‘𝑎)) ≤ (♯‘((1^st ‘𝑎) ++ (2^nd ‘𝑎))))
34	16, 19, 22, 23, 33	elfzd 13483	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (♯‘(1^st ‘𝑎)) ∈ (0...(♯‘((1^st ‘𝑎) ++ (2^nd ‘𝑎)))))
35	15, 34	opelxpd 5680	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → ⟨((1^st ‘𝑎) ++ (2^nd ‘𝑎)), (♯‘(1^st ‘𝑎))⟩ ∈ ({((1^st ‘𝑎) ++ (2^nd ‘𝑎))} × (0...(♯‘((1^st ‘𝑎) ++ (2^nd ‘𝑎))))))
36	6, 12, 35	rspcedvdw 3594	. . . . . 6 ⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → ∃𝑤 ∈ Word 𝐴⟨((1^st ‘𝑎) ++ (2^nd ‘𝑎)), (♯‘(1^st ‘𝑎))⟩ ∈ ({𝑤} × (0...(♯‘𝑤))))
37	36	eliund 4965	. . . . 5 ⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → ⟨((1^st ‘𝑎) ++ (2^nd ‘𝑎)), (♯‘(1^st ‘𝑎))⟩ ∈ ∪ 𝑤 ∈ Word 𝐴({𝑤} × (0...(♯‘𝑤))))
38		gsumwrd2dccatlem.u	. . . . 5 ⊢ 𝑈 = ∪ 𝑤 ∈ Word 𝐴({𝑤} × (0...(♯‘𝑤)))
39	37, 38	eleqtrrdi 2840	. . . 4 ⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → ⟨((1^st ‘𝑎) ++ (2^nd ‘𝑎)), (♯‘(1^st ‘𝑎))⟩ ∈ 𝑈)
40		simpr 484	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑏 ∈ ({𝑢} × (0...(♯‘𝑢)))) → 𝑏 ∈ ({𝑢} × (0...(♯‘𝑢))))
41		xp1st 8003	. . . . . . . . . 10 ⊢ (𝑏 ∈ ({𝑢} × (0...(♯‘𝑢))) → (1^st ‘𝑏) ∈ {𝑢})
42		elsni 4609	. . . . . . . . . 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 2829	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑏 ∈ ({𝑢} × (0...(♯‘𝑢)))) → (1^st ‘𝑏) ∈ Word 𝐴)
46	45	adantllr 719	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑏 ∈ ({𝑢} × (0...(♯‘𝑢)))) → (1^st ‘𝑏) ∈ Word 𝐴)
47	38	eleq2i 2821	. . . . . . . . . . 11 ⊢ (𝑏 ∈ 𝑈 ↔ 𝑏 ∈ ∪ 𝑤 ∈ Word 𝐴({𝑤} × (0...(♯‘𝑤))))
48	47	biimpi 216	. . . . . . . . . 10 ⊢ (𝑏 ∈ 𝑈 → 𝑏 ∈ ∪ 𝑤 ∈ Word 𝐴({𝑤} × (0...(♯‘𝑤))))
49	48	adantl 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝑈) → 𝑏 ∈ ∪ 𝑤 ∈ Word 𝐴({𝑤} × (0...(♯‘𝑤))))
50		eliun 4962	. . . . . . . . 9 ⊢ (𝑏 ∈ ∪ 𝑤 ∈ Word 𝐴({𝑤} × (0...(♯‘𝑤))) ↔ ∃𝑤 ∈ Word 𝐴𝑏 ∈ ({𝑤} × (0...(♯‘𝑤))))
51	49, 50	sylib 218	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝑈) → ∃𝑤 ∈ Word 𝐴𝑏 ∈ ({𝑤} × (0...(♯‘𝑤))))
52		sneq 4602	. . . . . . . . . . 11 ⊢ (𝑢 = 𝑤 → {𝑢} = {𝑤})
53		fveq2 6861	. . . . . . . . . . . 12 ⊢ (𝑢 = 𝑤 → (♯‘𝑢) = (♯‘𝑤))
54	53	oveq2d 7406	. . . . . . . . . . 11 ⊢ (𝑢 = 𝑤 → (0...(♯‘𝑢)) = (0...(♯‘𝑤)))
55	52, 54	xpeq12d 5672	. . . . . . . . . 10 ⊢ (𝑢 = 𝑤 → ({𝑢} × (0...(♯‘𝑢))) = ({𝑤} × (0...(♯‘𝑤))))
56	55	eleq2d 2815	. . . . . . . . 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 3142	. . . . . 6 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝑈) → (1^st ‘𝑏) ∈ Word 𝐴)
60		pfxcl 14649	. . . . . 6 ⊢ ((1^st ‘𝑏) ∈ Word 𝐴 → ((1^st ‘𝑏) prefix (2^nd ‘𝑏)) ∈ Word 𝐴)
61	59, 60	syl 17	. . . . 5 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝑈) → ((1^st ‘𝑏) prefix (2^nd ‘𝑏)) ∈ Word 𝐴)
62		swrdcl 14617	. . . . . 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 5680	. . . 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 5804	. . . . . . . . . 10 ⊢ (𝑏 ∈ ∪ 𝑤 ∈ Word 𝐴({𝑤} × (0...(♯‘𝑤))) ↔ ∃𝑤∃𝑛(𝑏 = ⟨𝑤, 𝑛⟩ ∧ (𝑤 ∈ Word 𝐴 ∧ 𝑛 ∈ (0...(♯‘𝑤)))))
67	65, 66	sylib 218	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → ∃𝑤∃𝑛(𝑏 = ⟨𝑤, 𝑛⟩ ∧ (𝑤 ∈ Word 𝐴 ∧ 𝑛 ∈ (0...(♯‘𝑤)))))
68		opeq1 4840	. . . . . . . . . . . . 13 ⊢ (𝑢 = 𝑤 → ⟨𝑢, 𝑛⟩ = ⟨𝑤, 𝑛⟩)
69	68	eqeq2d 2741	. . . . . . . . . . . 12 ⊢ (𝑢 = 𝑤 → (𝑏 = ⟨𝑢, 𝑛⟩ ↔ 𝑏 = ⟨𝑤, 𝑛⟩))
70		eleq1w 2812	. . . . . . . . . . . . 13 ⊢ (𝑢 = 𝑤 → (𝑢 ∈ Word 𝐴 ↔ 𝑤 ∈ Word 𝐴))
71	54	eleq2d 2815	. . . . . . . . . . . . 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 7408	. . . . . . . . . . . . . . . . 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 3454	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑢 ∈ V
81		vex 3454	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑛 ∈ V
82	80, 81	op1std 7981	. . . . . . . . . . . . . . . . . . . 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 2829	. . . . . . . . . . . . . . . . . 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 7982	. . . . . . . . . . . . . . . . . . . 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 2736	. . . . . . . . . . . . . . . . . . . . . 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 6865	. . . . . . . . . . . . . . . . . . . . 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 7406	. . . . . . . . . . . . . . . . . . . 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 2831	. . . . . . . . . . . . . . . . . . 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 2829	. . . . . . . . . . . . . . . . . 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 14682	. . . . . . . . . . . . . . . . . 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 2766	. . . . . . . . . . . . . . . 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 6865	. . . . . . . . . . . . . . . . 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 14655	. . . . . . . . . . . . . . . . . 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 2766	. . . . . . . . . . . . . . . 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 7408	. . . . . . . . . . . . . . . . 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 14674	. . . . . . . . . . . . . . . . . 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 2766	. . . . . . . . . . . . . . . 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 6865	. . . . . . . . . . . . . . . . . . . 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 2765	. . . . . . . . . . . . . . . . . . 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 4848	. . . . . . . . . . . . . . . . . 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 7408	. . . . . . . . . . . . . . . . 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 14641	. . . . . . . . . . . . . . . . . 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 2766	. . . . . . . . . . . . . . . 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 8013	. . . . . . . 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 4775	. . . . . . . . . . . . 13 ⊢ (𝑤 ∈ Word 𝐴 → {𝑤} ⊆ Word 𝐴)
131	130	adantl 481	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) ∧ 𝑤 ∈ Word 𝐴) → {𝑤} ⊆ Word 𝐴)
132		fz0ssnn0 13590	. . . . . . . . . . . 12 ⊢ (0...(♯‘𝑤)) ⊆ ℕ₀
133		xpss12 5656	. . . . . . . . . . . 12 ⊢ (({𝑤} ⊆ Word 𝐴 ∧ (0...(♯‘𝑤)) ⊆ ℕ₀) → ({𝑤} × (0...(♯‘𝑤))) ⊆ (Word 𝐴 × ℕ₀))
134	131, 132, 133	sylancl 586	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) ∧ 𝑤 ∈ Word 𝐴) → ({𝑤} × (0...(♯‘𝑤))) ⊆ (Word 𝐴 × ℕ₀))
135	134	iunssd 5017	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → ∪ 𝑤 ∈ Word 𝐴({𝑤} × (0...(♯‘𝑤))) ⊆ (Word 𝐴 × ℕ₀))
136	135	adantlr 715	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → ∪ 𝑤 ∈ Word 𝐴({𝑤} × (0...(♯‘𝑤))) ⊆ (Word 𝐴 × ℕ₀))
137	136, 65	sseldd 3950	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → 𝑏 ∈ (Word 𝐴 × ℕ₀))
138		eqop 8013	. . . . . . . 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 7645	. . 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 2783	. 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 3054 ⊆ wss 3917 {csn 4592 ⟨cop 4598 ∪ ciun 4958 class class class wbr 5110 ↦ cmpt 5191 × cxp 5639 ^◡ccnv 5640 –1-1-onto→wf1o 6513 ‘cfv 6514 (class class class)co 7390 1^st c1st 7969 2^nd c2nd 7970 0cc0 11075 + caddc 11078 ≤ cle 11216 ℕ₀cn0 12449 ...cfz 13475 ♯chash 14302 Word cword 14485 ++ cconcat 14542 substr csubstr 14612 prefix cpfx 14642

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 2702 ax-rep 5237 ax-sep 5254 ax-nul 5264 ax-pow 5323 ax-pr 5390 ax-un 7714 ax-cnex 11131 ax-resscn 11132 ax-1cn 11133 ax-icn 11134 ax-addcl 11135 ax-addrcl 11136 ax-mulcl 11137 ax-mulrcl 11138 ax-mulcom 11139 ax-addass 11140 ax-mulass 11141 ax-distr 11142 ax-i2m1 11143 ax-1ne0 11144 ax-1rid 11145 ax-rnegex 11146 ax-rrecex 11147 ax-cnre 11148 ax-pre-lttri 11149 ax-pre-lttrn 11150 ax-pre-ltadd 11151 ax-pre-mulgt0 11152

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 2534 df-eu 2563 df-clab 2709 df-cleq 2722 df-clel 2804 df-nfc 2879 df-ne 2927 df-nel 3031 df-ral 3046 df-rex 3055 df-reu 3357 df-rab 3409 df-v 3452 df-sbc 3757 df-csb 3866 df-dif 3920 df-un 3922 df-in 3924 df-ss 3934 df-pss 3937 df-nul 4300 df-if 4492 df-pw 4568 df-sn 4593 df-pr 4595 df-op 4599 df-uni 4875 df-int 4914 df-iun 4960 df-br 5111 df-opab 5173 df-mpt 5192 df-tr 5218 df-id 5536 df-eprel 5541 df-po 5549 df-so 5550 df-fr 5594 df-we 5596 df-xp 5647 df-rel 5648 df-cnv 5649 df-co 5650 df-dm 5651 df-rn 5652 df-res 5653 df-ima 5654 df-pred 6277 df-ord 6338 df-on 6339 df-lim 6340 df-suc 6341 df-iota 6467 df-fun 6516 df-fn 6517 df-f 6518 df-f1 6519 df-fo 6520 df-f1o 6521 df-fv 6522 df-riota 7347 df-ov 7393 df-oprab 7394 df-mpo 7395 df-om 7846 df-1st 7971 df-2nd 7972 df-frecs 8263 df-wrecs 8294 df-recs 8343 df-rdg 8381 df-1o 8437 df-er 8674 df-en 8922 df-dom 8923 df-sdom 8924 df-fin 8925 df-card 9899 df-pnf 11217 df-mnf 11218 df-xr 11219 df-ltxr 11220 df-le 11221 df-sub 11414 df-neg 11415 df-nn 12194 df-n0 12450 df-z 12537 df-uz 12801 df-fz 13476 df-fzo 13623 df-hash 14303 df-word 14486 df-concat 14543 df-substr 14613 df-pfx 14643

This theorem is referenced by: gsumwrd2dccat 33014

W3C validator