Theorem psgnunilem2 17738

Description: Lemma for psgnuni 17742. Induction step for moving a transposition as far to the right as possible. (Contributed by Stefan O'Rear, 24-Aug-2015.) (Revised by Mario Carneiro, 28-Feb-2016.)

Hypotheses

Ref	Expression
psgnunilem2.g	⊢ 𝐺 = (SymGrp‘𝐷)
psgnunilem2.t	⊢ 𝑇 = ran (pmTrsp‘𝐷)
psgnunilem2.d	⊢ (𝜑 → 𝐷 ∈ 𝑉)
psgnunilem2.w	⊢ (𝜑 → 𝑊 ∈ Word 𝑇)
psgnunilem2.id	⊢ (𝜑 → (𝐺 Σg 𝑊) = ( I ↾ 𝐷))
psgnunilem2.l	⊢ (𝜑 → (#‘𝑊) = 𝐿)
psgnunilem2.ix	⊢ (𝜑 → 𝐼 ∈ (0..^𝐿))
psgnunilem2.a	⊢ (𝜑 → 𝐴 ∈ dom ((𝑊‘𝐼) ∖ I ))
psgnunilem2.al	⊢ (𝜑 → ∀𝑘 ∈ (0..^𝐼) ¬ 𝐴 ∈ dom ((𝑊‘𝑘) ∖ I ))
psgnunilem2.in	⊢ (𝜑 → ¬ ∃𝑥 ∈ Word 𝑇((#‘𝑥) = (𝐿 − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)))

Assertion

Ref	Expression
psgnunilem2	⊢ (𝜑 → ∃𝑤 ∈ Word 𝑇(((𝐺 Σg 𝑤) = ( I ↾ 𝐷) ∧ (#‘𝑤) = 𝐿) ∧ ((𝐼 + 1) ∈ (0..^𝐿) ∧ 𝐴 ∈ dom ((𝑤‘(𝐼 + 1)) ∖ I ) ∧ ∀𝑗 ∈ (0..^(𝐼 + 1)) ¬ 𝐴 ∈ dom ((𝑤‘𝑗) ∖ I ))))

Distinct variable groups:   𝑗,𝑘,𝑤,𝐴   𝑥,𝑗,𝐷,𝑤   𝜑,𝑗   𝑗,𝐺   𝑥,𝑘,𝐺,𝑤   𝑗,𝐼,𝑘,𝑤,𝑥   𝑇,𝑗,𝑤,𝑥   𝑗,𝑊,𝑘,𝑤,𝑥   𝑤,𝐿,𝑥

Allowed substitution hints:   𝜑(𝑥,𝑤,𝑘)   𝐴(𝑥)   𝐷(𝑘)   𝑇(𝑘)   𝐿(𝑗,𝑘)   𝑉(𝑥,𝑤,𝑗,𝑘)

Proof of Theorem psgnunilem2

Dummy variables 𝑟 𝑠 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		psgnunilem2.w	. . . . . . 7 ⊢ (𝜑 → 𝑊 ∈ Word 𝑇)
2		wrd0 13185	. . . . . . 7 ⊢ ∅ ∈ Word 𝑇
3		splcl 13354	. . . . . . 7 ⊢ ((𝑊 ∈ Word 𝑇 ∧ ∅ ∈ Word 𝑇) → (𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩) ∈ Word 𝑇)
4	1, 2, 3	sylancl 693	. . . . . 6 ⊢ (𝜑 → (𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩) ∈ Word 𝑇)
5	4	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ ((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷)) → (𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩) ∈ Word 𝑇)
6		fzossfz 12357	. . . . . . . . . . 11 ⊢ (0..^𝐿) ⊆ (0...𝐿)
7		psgnunilem2.ix	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐼 ∈ (0..^𝐿))
8	6, 7	sseldi 3566	. . . . . . . . . 10 ⊢ (𝜑 → 𝐼 ∈ (0...𝐿))
9		elfznn0 12302	. . . . . . . . . 10 ⊢ (𝐼 ∈ (0...𝐿) → 𝐼 ∈ ℕ0)
10	8, 9	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝐼 ∈ ℕ0)
11		2nn0 11186	. . . . . . . . . 10 ⊢ 2 ∈ ℕ0
12		nn0addcl 11205	. . . . . . . . . 10 ⊢ ((𝐼 ∈ ℕ0 ∧ 2 ∈ ℕ0) → (𝐼 + 2) ∈ ℕ0)
13	10, 11, 12	sylancl 693	. . . . . . . . 9 ⊢ (𝜑 → (𝐼 + 2) ∈ ℕ0)
14	10	nn0red 11229	. . . . . . . . . 10 ⊢ (𝜑 → 𝐼 ∈ ℝ)
15		nn0addge1 11216	. . . . . . . . . 10 ⊢ ((𝐼 ∈ ℝ ∧ 2 ∈ ℕ0) → 𝐼 ≤ (𝐼 + 2))
16	14, 11, 15	sylancl 693	. . . . . . . . 9 ⊢ (𝜑 → 𝐼 ≤ (𝐼 + 2))
17		elfz2nn0 12300	. . . . . . . . 9 ⊢ (𝐼 ∈ (0...(𝐼 + 2)) ↔ (𝐼 ∈ ℕ0 ∧ (𝐼 + 2) ∈ ℕ0 ∧ 𝐼 ≤ (𝐼 + 2)))
18	10, 13, 16, 17	syl3anbrc 1239	. . . . . . . 8 ⊢ (𝜑 → 𝐼 ∈ (0...(𝐼 + 2)))
19		psgnunilem2.g	. . . . . . . . . . 11 ⊢ 𝐺 = (SymGrp‘𝐷)
20		psgnunilem2.t	. . . . . . . . . . 11 ⊢ 𝑇 = ran (pmTrsp‘𝐷)
21		psgnunilem2.d	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐷 ∈ 𝑉)
22		psgnunilem2.id	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐺 Σg 𝑊) = ( I ↾ 𝐷))
23		psgnunilem2.l	. . . . . . . . . . 11 ⊢ (𝜑 → (#‘𝑊) = 𝐿)
24		psgnunilem2.a	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 ∈ dom ((𝑊‘𝐼) ∖ I ))
25		psgnunilem2.al	. . . . . . . . . . 11 ⊢ (𝜑 → ∀𝑘 ∈ (0..^𝐼) ¬ 𝐴 ∈ dom ((𝑊‘𝑘) ∖ I ))
26	19, 20, 21, 1, 22, 23, 7, 24, 25	psgnunilem5 17737	. . . . . . . . . 10 ⊢ (𝜑 → (𝐼 + 1) ∈ (0..^𝐿))
27		fzofzp1 12431	. . . . . . . . . 10 ⊢ ((𝐼 + 1) ∈ (0..^𝐿) → ((𝐼 + 1) + 1) ∈ (0...𝐿))
28	26, 27	syl 17	. . . . . . . . 9 ⊢ (𝜑 → ((𝐼 + 1) + 1) ∈ (0...𝐿))
29	10	nn0cnd 11230	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐼 ∈ ℂ)
30		1cnd 9935	. . . . . . . . . . 11 ⊢ (𝜑 → 1 ∈ ℂ)
31	29, 30, 30	addassd 9941	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐼 + 1) + 1) = (𝐼 + (1 + 1)))
32		df-2 10956	. . . . . . . . . . 11 ⊢ 2 = (1 + 1)
33	32	oveq2i 6560	. . . . . . . . . 10 ⊢ (𝐼 + 2) = (𝐼 + (1 + 1))
34	31, 33	syl6reqr 2663	. . . . . . . . 9 ⊢ (𝜑 → (𝐼 + 2) = ((𝐼 + 1) + 1))
35	23	oveq2d 6565	. . . . . . . . 9 ⊢ (𝜑 → (0...(#‘𝑊)) = (0...𝐿))
36	28, 34, 35	3eltr4d 2703	. . . . . . . 8 ⊢ (𝜑 → (𝐼 + 2) ∈ (0...(#‘𝑊)))
37	2	a1i 11	. . . . . . . 8 ⊢ (𝜑 → ∅ ∈ Word 𝑇)
38	1, 18, 36, 37	spllen 13356	. . . . . . 7 ⊢ (𝜑 → (#‘(𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩)) = ((#‘𝑊) + ((#‘∅) − ((𝐼 + 2) − 𝐼))))
39		hash0 13019	. . . . . . . . . . 11 ⊢ (#‘∅) = 0
40	39	oveq1i 6559	. . . . . . . . . 10 ⊢ ((#‘∅) − ((𝐼 + 2) − 𝐼)) = (0 − ((𝐼 + 2) − 𝐼))
41		df-neg 10148	. . . . . . . . . 10 ⊢ -((𝐼 + 2) − 𝐼) = (0 − ((𝐼 + 2) − 𝐼))
42	40, 41	eqtr4i 2635	. . . . . . . . 9 ⊢ ((#‘∅) − ((𝐼 + 2) − 𝐼)) = -((𝐼 + 2) − 𝐼)
43		2cn 10968	. . . . . . . . . . 11 ⊢ 2 ∈ ℂ
44		pncan2 10167	. . . . . . . . . . 11 ⊢ ((𝐼 ∈ ℂ ∧ 2 ∈ ℂ) → ((𝐼 + 2) − 𝐼) = 2)
45	29, 43, 44	sylancl 693	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐼 + 2) − 𝐼) = 2)
46	45	negeqd 10154	. . . . . . . . 9 ⊢ (𝜑 → -((𝐼 + 2) − 𝐼) = -2)
47	42, 46	syl5eq 2656	. . . . . . . 8 ⊢ (𝜑 → ((#‘∅) − ((𝐼 + 2) − 𝐼)) = -2)
48	23, 47	oveq12d 6567	. . . . . . 7 ⊢ (𝜑 → ((#‘𝑊) + ((#‘∅) − ((𝐼 + 2) − 𝐼))) = (𝐿 + -2))
49		elfzel2 12211	. . . . . . . . . 10 ⊢ (𝐼 ∈ (0...𝐿) → 𝐿 ∈ ℤ)
50	8, 49	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝐿 ∈ ℤ)
51	50	zcnd 11359	. . . . . . . 8 ⊢ (𝜑 → 𝐿 ∈ ℂ)
52		negsub 10208	. . . . . . . 8 ⊢ ((𝐿 ∈ ℂ ∧ 2 ∈ ℂ) → (𝐿 + -2) = (𝐿 − 2))
53	51, 43, 52	sylancl 693	. . . . . . 7 ⊢ (𝜑 → (𝐿 + -2) = (𝐿 − 2))
54	38, 48, 53	3eqtrd 2648	. . . . . 6 ⊢ (𝜑 → (#‘(𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩)) = (𝐿 − 2))
55	54	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ ((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷)) → (#‘(𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩)) = (𝐿 − 2))
56		splid 13355	. . . . . . . . 9 ⊢ ((𝑊 ∈ Word 𝑇 ∧ (𝐼 ∈ (0...(𝐼 + 2)) ∧ (𝐼 + 2) ∈ (0...(#‘𝑊)))) → (𝑊 splice ⟨𝐼, (𝐼 + 2), (𝑊 substr ⟨𝐼, (𝐼 + 2)⟩)⟩) = 𝑊)
57	1, 18, 36, 56	syl12anc 1316	. . . . . . . 8 ⊢ (𝜑 → (𝑊 splice ⟨𝐼, (𝐼 + 2), (𝑊 substr ⟨𝐼, (𝐼 + 2)⟩)⟩) = 𝑊)
58	57	oveq2d 6565	. . . . . . 7 ⊢ (𝜑 → (𝐺 Σg (𝑊 splice ⟨𝐼, (𝐼 + 2), (𝑊 substr ⟨𝐼, (𝐼 + 2)⟩)⟩)) = (𝐺 Σg 𝑊))
59	58	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷)) → (𝐺 Σg (𝑊 splice ⟨𝐼, (𝐼 + 2), (𝑊 substr ⟨𝐼, (𝐼 + 2)⟩)⟩)) = (𝐺 Σg 𝑊))
60		eqid 2610	. . . . . . 7 ⊢ (Base‘𝐺) = (Base‘𝐺)
61	19	symggrp 17643	. . . . . . . . . 10 ⊢ (𝐷 ∈ 𝑉 → 𝐺 ∈ Grp)
62	21, 61	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝐺 ∈ Grp)
63		grpmnd 17252	. . . . . . . . 9 ⊢ (𝐺 ∈ Grp → 𝐺 ∈ Mnd)
64	62, 63	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝐺 ∈ Mnd)
65	64	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷)) → 𝐺 ∈ Mnd)
66	20, 19, 60	symgtrf 17712	. . . . . . . . . 10 ⊢ 𝑇 ⊆ (Base‘𝐺)
67		sswrd 13168	. . . . . . . . . 10 ⊢ (𝑇 ⊆ (Base‘𝐺) → Word 𝑇 ⊆ Word (Base‘𝐺))
68	66, 67	ax-mp 5	. . . . . . . . 9 ⊢ Word 𝑇 ⊆ Word (Base‘𝐺)
69	68, 1	sseldi 3566	. . . . . . . 8 ⊢ (𝜑 → 𝑊 ∈ Word (Base‘𝐺))
70	69	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷)) → 𝑊 ∈ Word (Base‘𝐺))
71	18	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷)) → 𝐼 ∈ (0...(𝐼 + 2)))
72	36	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷)) → (𝐼 + 2) ∈ (0...(#‘𝑊)))
73		swrdcl 13271	. . . . . . . . 9 ⊢ (𝑊 ∈ Word (Base‘𝐺) → (𝑊 substr ⟨𝐼, (𝐼 + 2)⟩) ∈ Word (Base‘𝐺))
74	69, 73	syl 17	. . . . . . . 8 ⊢ (𝜑 → (𝑊 substr ⟨𝐼, (𝐼 + 2)⟩) ∈ Word (Base‘𝐺))
75	74	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷)) → (𝑊 substr ⟨𝐼, (𝐼 + 2)⟩) ∈ Word (Base‘𝐺))
76		wrd0 13185	. . . . . . . 8 ⊢ ∅ ∈ Word (Base‘𝐺)
77	76	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷)) → ∅ ∈ Word (Base‘𝐺))
78	23	oveq2d 6565	. . . . . . . . . . . . 13 ⊢ (𝜑 → (0..^(#‘𝑊)) = (0..^𝐿))
79	26, 78	eleqtrrd 2691	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐼 + 1) ∈ (0..^(#‘𝑊)))
80		swrds2 13533	. . . . . . . . . . . 12 ⊢ ((𝑊 ∈ Word 𝑇 ∧ 𝐼 ∈ ℕ0 ∧ (𝐼 + 1) ∈ (0..^(#‘𝑊))) → (𝑊 substr ⟨𝐼, (𝐼 + 2)⟩) = ⟨“(𝑊‘𝐼)(𝑊‘(𝐼 + 1))”⟩)
81	1, 10, 79, 80	syl3anc 1318	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑊 substr ⟨𝐼, (𝐼 + 2)⟩) = ⟨“(𝑊‘𝐼)(𝑊‘(𝐼 + 1))”⟩)
82	81	oveq2d 6565	. . . . . . . . . 10 ⊢ (𝜑 → (𝐺 Σg (𝑊 substr ⟨𝐼, (𝐼 + 2)⟩)) = (𝐺 Σg ⟨“(𝑊‘𝐼)(𝑊‘(𝐼 + 1))”⟩))
83		wrdf 13165	. . . . . . . . . . . . . . 15 ⊢ (𝑊 ∈ Word 𝑇 → 𝑊:(0..^(#‘𝑊))⟶𝑇)
84	1, 83	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑊:(0..^(#‘𝑊))⟶𝑇)
85	78	feq2d 5944	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑊:(0..^(#‘𝑊))⟶𝑇 ↔ 𝑊:(0..^𝐿)⟶𝑇))
86	84, 85	mpbid 221	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑊:(0..^𝐿)⟶𝑇)
87	86, 7	ffvelrnd 6268	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑊‘𝐼) ∈ 𝑇)
88	66, 87	sseldi 3566	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑊‘𝐼) ∈ (Base‘𝐺))
89	86, 26	ffvelrnd 6268	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑊‘(𝐼 + 1)) ∈ 𝑇)
90	66, 89	sseldi 3566	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑊‘(𝐼 + 1)) ∈ (Base‘𝐺))
91		eqid 2610	. . . . . . . . . . . 12 ⊢ (+g‘𝐺) = (+g‘𝐺)
92	60, 91	gsumws2 17202	. . . . . . . . . . 11 ⊢ ((𝐺 ∈ Mnd ∧ (𝑊‘𝐼) ∈ (Base‘𝐺) ∧ (𝑊‘(𝐼 + 1)) ∈ (Base‘𝐺)) → (𝐺 Σg ⟨“(𝑊‘𝐼)(𝑊‘(𝐼 + 1))”⟩) = ((𝑊‘𝐼)(+g‘𝐺)(𝑊‘(𝐼 + 1))))
93	64, 88, 90, 92	syl3anc 1318	. . . . . . . . . 10 ⊢ (𝜑 → (𝐺 Σg ⟨“(𝑊‘𝐼)(𝑊‘(𝐼 + 1))”⟩) = ((𝑊‘𝐼)(+g‘𝐺)(𝑊‘(𝐼 + 1))))
94	19, 60, 91	symgov 17633	. . . . . . . . . . 11 ⊢ (((𝑊‘𝐼) ∈ (Base‘𝐺) ∧ (𝑊‘(𝐼 + 1)) ∈ (Base‘𝐺)) → ((𝑊‘𝐼)(+g‘𝐺)(𝑊‘(𝐼 + 1))) = ((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))))
95	88, 90, 94	syl2anc 691	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑊‘𝐼)(+g‘𝐺)(𝑊‘(𝐼 + 1))) = ((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))))
96	82, 93, 95	3eqtrd 2648	. . . . . . . . 9 ⊢ (𝜑 → (𝐺 Σg (𝑊 substr ⟨𝐼, (𝐼 + 2)⟩)) = ((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))))
97	96	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷)) → (𝐺 Σg (𝑊 substr ⟨𝐼, (𝐼 + 2)⟩)) = ((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))))
98		simpr 476	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷)) → ((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷))
99	19	symgid 17644	. . . . . . . . . . 11 ⊢ (𝐷 ∈ 𝑉 → ( I ↾ 𝐷) = (0g‘𝐺))
100	21, 99	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → ( I ↾ 𝐷) = (0g‘𝐺))
101		eqid 2610	. . . . . . . . . . 11 ⊢ (0g‘𝐺) = (0g‘𝐺)
102	101	gsum0 17101	. . . . . . . . . 10 ⊢ (𝐺 Σg ∅) = (0g‘𝐺)
103	100, 102	syl6eqr 2662	. . . . . . . . 9 ⊢ (𝜑 → ( I ↾ 𝐷) = (𝐺 Σg ∅))
104	103	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷)) → ( I ↾ 𝐷) = (𝐺 Σg ∅))
105	97, 98, 104	3eqtrd 2648	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷)) → (𝐺 Σg (𝑊 substr ⟨𝐼, (𝐼 + 2)⟩)) = (𝐺 Σg ∅))
106	60, 65, 70, 71, 72, 75, 77, 105	gsumspl 17204	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷)) → (𝐺 Σg (𝑊 splice ⟨𝐼, (𝐼 + 2), (𝑊 substr ⟨𝐼, (𝐼 + 2)⟩)⟩)) = (𝐺 Σg (𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩)))
107	22	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷)) → (𝐺 Σg 𝑊) = ( I ↾ 𝐷))
108	59, 106, 107	3eqtr3d 2652	. . . . 5 ⊢ ((𝜑 ∧ ((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷)) → (𝐺 Σg (𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩)) = ( I ↾ 𝐷))
109		fveq2 6103	. . . . . . . 8 ⊢ (𝑥 = (𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩) → (#‘𝑥) = (#‘(𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩)))
110	109	eqeq1d 2612	. . . . . . 7 ⊢ (𝑥 = (𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩) → ((#‘𝑥) = (𝐿 − 2) ↔ (#‘(𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩)) = (𝐿 − 2)))
111		oveq2 6557	. . . . . . . 8 ⊢ (𝑥 = (𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩) → (𝐺 Σg 𝑥) = (𝐺 Σg (𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩)))
112	111	eqeq1d 2612	. . . . . . 7 ⊢ (𝑥 = (𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩) → ((𝐺 Σg 𝑥) = ( I ↾ 𝐷) ↔ (𝐺 Σg (𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩)) = ( I ↾ 𝐷)))
113	110, 112	anbi12d 743	. . . . . 6 ⊢ (𝑥 = (𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩) → (((#‘𝑥) = (𝐿 − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)) ↔ ((#‘(𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩)) = (𝐿 − 2) ∧ (𝐺 Σg (𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩)) = ( I ↾ 𝐷))))
114	113	rspcev 3282	. . . . 5 ⊢ (((𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩) ∈ Word 𝑇 ∧ ((#‘(𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩)) = (𝐿 − 2) ∧ (𝐺 Σg (𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩)) = ( I ↾ 𝐷))) → ∃𝑥 ∈ Word 𝑇((#‘𝑥) = (𝐿 − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)))
115	5, 55, 108, 114	syl12anc 1316	. . . 4 ⊢ ((𝜑 ∧ ((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷)) → ∃𝑥 ∈ Word 𝑇((#‘𝑥) = (𝐿 − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)))
116		psgnunilem2.in	. . . . 5 ⊢ (𝜑 → ¬ ∃𝑥 ∈ Word 𝑇((#‘𝑥) = (𝐿 − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)))
117	116	adantr 480	. . . 4 ⊢ ((𝜑 ∧ ((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷)) → ¬ ∃𝑥 ∈ Word 𝑇((#‘𝑥) = (𝐿 − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)))
118	115, 117	pm2.21dd 185	. . 3 ⊢ ((𝜑 ∧ ((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷)) → ∃𝑤 ∈ Word 𝑇(((𝐺 Σg 𝑤) = ( I ↾ 𝐷) ∧ (#‘𝑤) = 𝐿) ∧ ((𝐼 + 1) ∈ (0..^𝐿) ∧ 𝐴 ∈ dom ((𝑤‘(𝐼 + 1)) ∖ I ) ∧ ∀𝑗 ∈ (0..^(𝐼 + 1)) ¬ 𝐴 ∈ dom ((𝑤‘𝑗) ∖ I ))))
119	118	ex 449	. 2 ⊢ (𝜑 → (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷) → ∃𝑤 ∈ Word 𝑇(((𝐺 Σg 𝑤) = ( I ↾ 𝐷) ∧ (#‘𝑤) = 𝐿) ∧ ((𝐼 + 1) ∈ (0..^𝐿) ∧ 𝐴 ∈ dom ((𝑤‘(𝐼 + 1)) ∖ I ) ∧ ∀𝑗 ∈ (0..^(𝐼 + 1)) ¬ 𝐴 ∈ dom ((𝑤‘𝑗) ∖ I )))))
120	1	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → 𝑊 ∈ Word 𝑇)
121		simprl 790	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → 𝑟 ∈ 𝑇)
122		simprr 792	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → 𝑠 ∈ 𝑇)
123	121, 122	s2cld 13466	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → ⟨“𝑟𝑠”⟩ ∈ Word 𝑇)
124		splcl 13354	. . . . . . 7 ⊢ ((𝑊 ∈ Word 𝑇 ∧ ⟨“𝑟𝑠”⟩ ∈ Word 𝑇) → (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩) ∈ Word 𝑇)
125	120, 123, 124	syl2anc 691	. . . . . 6 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩) ∈ Word 𝑇)
126	125	adantrr 749	. . . . 5 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩) ∈ Word 𝑇)
127	64	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → 𝐺 ∈ Mnd)
128	69	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → 𝑊 ∈ Word (Base‘𝐺))
129	18	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → 𝐼 ∈ (0...(𝐼 + 2)))
130	36	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → (𝐼 + 2) ∈ (0...(#‘𝑊)))
131	68, 123	sseldi 3566	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → ⟨“𝑟𝑠”⟩ ∈ Word (Base‘𝐺))
132	131	adantrr 749	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → ⟨“𝑟𝑠”⟩ ∈ Word (Base‘𝐺))
133	74	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → (𝑊 substr ⟨𝐼, (𝐼 + 2)⟩) ∈ Word (Base‘𝐺))
134		simprr1 1102	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → ((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠))
135	96	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → (𝐺 Σg (𝑊 substr ⟨𝐼, (𝐼 + 2)⟩)) = ((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))))
136	64	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → 𝐺 ∈ Mnd)
137	66	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑇 ⊆ (Base‘𝐺))
138	137	sselda 3568	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑟 ∈ 𝑇) → 𝑟 ∈ (Base‘𝐺))
139	138	adantrr 749	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → 𝑟 ∈ (Base‘𝐺))
140	137	sselda 3568	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝑇) → 𝑠 ∈ (Base‘𝐺))
141	140	adantrl 748	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → 𝑠 ∈ (Base‘𝐺))
142	60, 91	gsumws2 17202	. . . . . . . . . . . 12 ⊢ ((𝐺 ∈ Mnd ∧ 𝑟 ∈ (Base‘𝐺) ∧ 𝑠 ∈ (Base‘𝐺)) → (𝐺 Σg ⟨“𝑟𝑠”⟩) = (𝑟(+g‘𝐺)𝑠))
143	136, 139, 141, 142	syl3anc 1318	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → (𝐺 Σg ⟨“𝑟𝑠”⟩) = (𝑟(+g‘𝐺)𝑠))
144	19, 60, 91	symgov 17633	. . . . . . . . . . . 12 ⊢ ((𝑟 ∈ (Base‘𝐺) ∧ 𝑠 ∈ (Base‘𝐺)) → (𝑟(+g‘𝐺)𝑠) = (𝑟 ∘ 𝑠))
145	139, 141, 144	syl2anc 691	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → (𝑟(+g‘𝐺)𝑠) = (𝑟 ∘ 𝑠))
146	143, 145	eqtrd 2644	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → (𝐺 Σg ⟨“𝑟𝑠”⟩) = (𝑟 ∘ 𝑠))
147	146	adantrr 749	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → (𝐺 Σg ⟨“𝑟𝑠”⟩) = (𝑟 ∘ 𝑠))
148	134, 135, 147	3eqtr4rd 2655	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → (𝐺 Σg ⟨“𝑟𝑠”⟩) = (𝐺 Σg (𝑊 substr ⟨𝐼, (𝐼 + 2)⟩)))
149	60, 127, 128, 129, 130, 132, 133, 148	gsumspl 17204	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → (𝐺 Σg (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)) = (𝐺 Σg (𝑊 splice ⟨𝐼, (𝐼 + 2), (𝑊 substr ⟨𝐼, (𝐼 + 2)⟩)⟩)))
150	58	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → (𝐺 Σg (𝑊 splice ⟨𝐼, (𝐼 + 2), (𝑊 substr ⟨𝐼, (𝐼 + 2)⟩)⟩)) = (𝐺 Σg 𝑊))
151	22	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → (𝐺 Σg 𝑊) = ( I ↾ 𝐷))
152	149, 150, 151	3eqtrd 2648	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → (𝐺 Σg (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)) = ( I ↾ 𝐷))
153	18	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → 𝐼 ∈ (0...(𝐼 + 2)))
154	36	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → (𝐼 + 2) ∈ (0...(#‘𝑊)))
155	120, 153, 154, 123	spllen 13356	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → (#‘(𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)) = ((#‘𝑊) + ((#‘⟨“𝑟𝑠”⟩) − ((𝐼 + 2) − 𝐼))))
156		s2len 13484	. . . . . . . . . . . . 13 ⊢ (#‘⟨“𝑟𝑠”⟩) = 2
157	156	oveq1i 6559	. . . . . . . . . . . 12 ⊢ ((#‘⟨“𝑟𝑠”⟩) − ((𝐼 + 2) − 𝐼)) = (2 − ((𝐼 + 2) − 𝐼))
158	45	oveq2d 6565	. . . . . . . . . . . . 13 ⊢ (𝜑 → (2 − ((𝐼 + 2) − 𝐼)) = (2 − 2))
159	43	subidi 10231	. . . . . . . . . . . . 13 ⊢ (2 − 2) = 0
160	158, 159	syl6eq 2660	. . . . . . . . . . . 12 ⊢ (𝜑 → (2 − ((𝐼 + 2) − 𝐼)) = 0)
161	157, 160	syl5eq 2656	. . . . . . . . . . 11 ⊢ (𝜑 → ((#‘⟨“𝑟𝑠”⟩) − ((𝐼 + 2) − 𝐼)) = 0)
162	161	oveq2d 6565	. . . . . . . . . 10 ⊢ (𝜑 → ((#‘𝑊) + ((#‘⟨“𝑟𝑠”⟩) − ((𝐼 + 2) − 𝐼))) = ((#‘𝑊) + 0))
163	23, 51	eqeltrd 2688	. . . . . . . . . . 11 ⊢ (𝜑 → (#‘𝑊) ∈ ℂ)
164	163	addid1d 10115	. . . . . . . . . 10 ⊢ (𝜑 → ((#‘𝑊) + 0) = (#‘𝑊))
165	162, 164, 23	3eqtrd 2648	. . . . . . . . 9 ⊢ (𝜑 → ((#‘𝑊) + ((#‘⟨“𝑟𝑠”⟩) − ((𝐼 + 2) − 𝐼))) = 𝐿)
166	165	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → ((#‘𝑊) + ((#‘⟨“𝑟𝑠”⟩) − ((𝐼 + 2) − 𝐼))) = 𝐿)
167	155, 166	eqtrd 2644	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → (#‘(𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)) = 𝐿)
168	167	adantrr 749	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → (#‘(𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)) = 𝐿)
169	152, 168	jca 553	. . . . 5 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → ((𝐺 Σg (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)) = ( I ↾ 𝐷) ∧ (#‘(𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)) = 𝐿))
170	26	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → (𝐼 + 1) ∈ (0..^𝐿))
171		simprr2 1103	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → 𝐴 ∈ dom (𝑠 ∖ I ))
172		1nn0 11185	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ ℕ0
173		2nn 11062	. . . . . . . . . . . . . . 15 ⊢ 2 ∈ ℕ
174		1lt2 11071	. . . . . . . . . . . . . . 15 ⊢ 1 < 2
175		elfzo0 12376	. . . . . . . . . . . . . . 15 ⊢ (1 ∈ (0..^2) ↔ (1 ∈ ℕ0 ∧ 2 ∈ ℕ ∧ 1 < 2))
176	172, 173, 174, 175	mpbir3an 1237	. . . . . . . . . . . . . 14 ⊢ 1 ∈ (0..^2)
177	156	oveq2i 6560	. . . . . . . . . . . . . 14 ⊢ (0..^(#‘⟨“𝑟𝑠”⟩)) = (0..^2)
178	176, 177	eleqtrri 2687	. . . . . . . . . . . . 13 ⊢ 1 ∈ (0..^(#‘⟨“𝑟𝑠”⟩))
179	178	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → 1 ∈ (0..^(#‘⟨“𝑟𝑠”⟩)))
180	120, 153, 154, 123, 179	splfv2a 13358	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → ((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘(𝐼 + 1)) = (⟨“𝑟𝑠”⟩‘1))
181		s2fv1 13483	. . . . . . . . . . . 12 ⊢ (𝑠 ∈ 𝑇 → (⟨“𝑟𝑠”⟩‘1) = 𝑠)
182	181	ad2antll 761	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → (⟨“𝑟𝑠”⟩‘1) = 𝑠)
183	180, 182	eqtrd 2644	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → ((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘(𝐼 + 1)) = 𝑠)
184	183	adantrr 749	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → ((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘(𝐼 + 1)) = 𝑠)
185	184	difeq1d 3689	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘(𝐼 + 1)) ∖ I ) = (𝑠 ∖ I ))
186	185	dmeqd 5248	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘(𝐼 + 1)) ∖ I ) = dom (𝑠 ∖ I ))
187	171, 186	eleqtrrd 2691	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → 𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘(𝐼 + 1)) ∖ I ))
188		fzosplitsni 12444	. . . . . . . . . . 11 ⊢ (𝐼 ∈ (ℤ≥‘0) → (𝑗 ∈ (0..^(𝐼 + 1)) ↔ (𝑗 ∈ (0..^𝐼) ∨ 𝑗 = 𝐼)))
189		nn0uz 11598	. . . . . . . . . . 11 ⊢ ℕ0 = (ℤ≥‘0)
190	188, 189	eleq2s 2706	. . . . . . . . . 10 ⊢ (𝐼 ∈ ℕ0 → (𝑗 ∈ (0..^(𝐼 + 1)) ↔ (𝑗 ∈ (0..^𝐼) ∨ 𝑗 = 𝐼)))
191	10, 190	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (𝑗 ∈ (0..^(𝐼 + 1)) ↔ (𝑗 ∈ (0..^𝐼) ∨ 𝑗 = 𝐼)))
192	191	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → (𝑗 ∈ (0..^(𝐼 + 1)) ↔ (𝑗 ∈ (0..^𝐼) ∨ 𝑗 = 𝐼)))
193		fveq2 6103	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 𝑗 → (𝑊‘𝑘) = (𝑊‘𝑗))
194	193	difeq1d 3689	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 𝑗 → ((𝑊‘𝑘) ∖ I ) = ((𝑊‘𝑗) ∖ I ))
195	194	dmeqd 5248	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 𝑗 → dom ((𝑊‘𝑘) ∖ I ) = dom ((𝑊‘𝑗) ∖ I ))
196	195	eleq2d 2673	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 𝑗 → (𝐴 ∈ dom ((𝑊‘𝑘) ∖ I ) ↔ 𝐴 ∈ dom ((𝑊‘𝑗) ∖ I )))
197	196	notbid 307	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑗 → (¬ 𝐴 ∈ dom ((𝑊‘𝑘) ∖ I ) ↔ ¬ 𝐴 ∈ dom ((𝑊‘𝑗) ∖ I )))
198	197	rspccva 3281	. . . . . . . . . . . . . 14 ⊢ ((∀𝑘 ∈ (0..^𝐼) ¬ 𝐴 ∈ dom ((𝑊‘𝑘) ∖ I ) ∧ 𝑗 ∈ (0..^𝐼)) → ¬ 𝐴 ∈ dom ((𝑊‘𝑗) ∖ I ))
199	25, 198	sylan 487	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝐼)) → ¬ 𝐴 ∈ dom ((𝑊‘𝑗) ∖ I ))
200	199	adantlr 747	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) ∧ 𝑗 ∈ (0..^𝐼)) → ¬ 𝐴 ∈ dom ((𝑊‘𝑗) ∖ I ))
201	1	ad2antrr 758	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) ∧ 𝑗 ∈ (0..^𝐼)) → 𝑊 ∈ Word 𝑇)
202	18	ad2antrr 758	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) ∧ 𝑗 ∈ (0..^𝐼)) → 𝐼 ∈ (0...(𝐼 + 2)))
203	36	ad2antrr 758	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) ∧ 𝑗 ∈ (0..^𝐼)) → (𝐼 + 2) ∈ (0...(#‘𝑊)))
204	123	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) ∧ 𝑗 ∈ (0..^𝐼)) → ⟨“𝑟𝑠”⟩ ∈ Word 𝑇)
205		simpr 476	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) ∧ 𝑗 ∈ (0..^𝐼)) → 𝑗 ∈ (0..^𝐼))
206	201, 202, 203, 204, 205	splfv1 13357	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) ∧ 𝑗 ∈ (0..^𝐼)) → ((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) = (𝑊‘𝑗))
207	206	difeq1d 3689	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) ∧ 𝑗 ∈ (0..^𝐼)) → (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) ∖ I ) = ((𝑊‘𝑗) ∖ I ))
208	207	dmeqd 5248	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) ∧ 𝑗 ∈ (0..^𝐼)) → dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) ∖ I ) = dom ((𝑊‘𝑗) ∖ I ))
209	200, 208	neleqtrrd 2710	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) ∧ 𝑗 ∈ (0..^𝐼)) → ¬ 𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) ∖ I ))
210	209	ex 449	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → (𝑗 ∈ (0..^𝐼) → ¬ 𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) ∖ I )))
211	210	adantrr 749	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → (𝑗 ∈ (0..^𝐼) → ¬ 𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) ∖ I )))
212		simprr3 1104	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → ¬ 𝐴 ∈ dom (𝑟 ∖ I ))
213		0nn0 11184	. . . . . . . . . . . . . . . . . . . 20 ⊢ 0 ∈ ℕ0
214		2pos 10989	. . . . . . . . . . . . . . . . . . . 20 ⊢ 0 < 2
215		elfzo0 12376	. . . . . . . . . . . . . . . . . . . 20 ⊢ (0 ∈ (0..^2) ↔ (0 ∈ ℕ0 ∧ 2 ∈ ℕ ∧ 0 < 2))
216	213, 173, 214, 215	mpbir3an 1237	. . . . . . . . . . . . . . . . . . 19 ⊢ 0 ∈ (0..^2)
217	216, 177	eleqtrri 2687	. . . . . . . . . . . . . . . . . 18 ⊢ 0 ∈ (0..^(#‘⟨“𝑟𝑠”⟩))
218	217	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → 0 ∈ (0..^(#‘⟨“𝑟𝑠”⟩)))
219	120, 153, 154, 123, 218	splfv2a 13358	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → ((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘(𝐼 + 0)) = (⟨“𝑟𝑠”⟩‘0))
220	29	addid1d 10115	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐼 + 0) = 𝐼)
221	220	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → (𝐼 + 0) = 𝐼)
222	221	fveq2d 6107	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → ((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘(𝐼 + 0)) = ((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝐼))
223		s2fv0 13482	. . . . . . . . . . . . . . . . 17 ⊢ (𝑟 ∈ 𝑇 → (⟨“𝑟𝑠”⟩‘0) = 𝑟)
224	223	ad2antrl 760	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → (⟨“𝑟𝑠”⟩‘0) = 𝑟)
225	219, 222, 224	3eqtr3d 2652	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → ((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝐼) = 𝑟)
226	225	difeq1d 3689	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝐼) ∖ I ) = (𝑟 ∖ I ))
227	226	dmeqd 5248	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝐼) ∖ I ) = dom (𝑟 ∖ I ))
228	227	eleq2d 2673	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → (𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝐼) ∖ I ) ↔ 𝐴 ∈ dom (𝑟 ∖ I )))
229	228	adantrr 749	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → (𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝐼) ∖ I ) ↔ 𝐴 ∈ dom (𝑟 ∖ I )))
230	212, 229	mtbird 314	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → ¬ 𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝐼) ∖ I ))
231		fveq2 6103	. . . . . . . . . . . . . 14 ⊢ (𝑗 = 𝐼 → ((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) = ((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝐼))
232	231	difeq1d 3689	. . . . . . . . . . . . 13 ⊢ (𝑗 = 𝐼 → (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) ∖ I ) = (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝐼) ∖ I ))
233	232	dmeqd 5248	. . . . . . . . . . . 12 ⊢ (𝑗 = 𝐼 → dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) ∖ I ) = dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝐼) ∖ I ))
234	233	eleq2d 2673	. . . . . . . . . . 11 ⊢ (𝑗 = 𝐼 → (𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) ∖ I ) ↔ 𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝐼) ∖ I )))
235	234	notbid 307	. . . . . . . . . 10 ⊢ (𝑗 = 𝐼 → (¬ 𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) ∖ I ) ↔ ¬ 𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝐼) ∖ I )))
236	230, 235	syl5ibrcom 236	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → (𝑗 = 𝐼 → ¬ 𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) ∖ I )))
237	211, 236	jaod 394	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → ((𝑗 ∈ (0..^𝐼) ∨ 𝑗 = 𝐼) → ¬ 𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) ∖ I )))
238	192, 237	sylbid 229	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → (𝑗 ∈ (0..^(𝐼 + 1)) → ¬ 𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) ∖ I )))
239	238	ralrimiv 2948	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → ∀𝑗 ∈ (0..^(𝐼 + 1)) ¬ 𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) ∖ I ))
240	170, 187, 239	3jca 1235	. . . . 5 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → ((𝐼 + 1) ∈ (0..^𝐿) ∧ 𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘(𝐼 + 1)) ∖ I ) ∧ ∀𝑗 ∈ (0..^(𝐼 + 1)) ¬ 𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) ∖ I )))
241		oveq2 6557	. . . . . . . . 9 ⊢ (𝑤 = (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩) → (𝐺 Σg 𝑤) = (𝐺 Σg (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)))
242	241	eqeq1d 2612	. . . . . . . 8 ⊢ (𝑤 = (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩) → ((𝐺 Σg 𝑤) = ( I ↾ 𝐷) ↔ (𝐺 Σg (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)) = ( I ↾ 𝐷)))
243		fveq2 6103	. . . . . . . . 9 ⊢ (𝑤 = (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩) → (#‘𝑤) = (#‘(𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)))
244	243	eqeq1d 2612	. . . . . . . 8 ⊢ (𝑤 = (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩) → ((#‘𝑤) = 𝐿 ↔ (#‘(𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)) = 𝐿))
245	242, 244	anbi12d 743	. . . . . . 7 ⊢ (𝑤 = (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩) → (((𝐺 Σg 𝑤) = ( I ↾ 𝐷) ∧ (#‘𝑤) = 𝐿) ↔ ((𝐺 Σg (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)) = ( I ↾ 𝐷) ∧ (#‘(𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)) = 𝐿)))
246		fveq1 6102	. . . . . . . . . . 11 ⊢ (𝑤 = (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩) → (𝑤‘(𝐼 + 1)) = ((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘(𝐼 + 1)))
247	246	difeq1d 3689	. . . . . . . . . 10 ⊢ (𝑤 = (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩) → ((𝑤‘(𝐼 + 1)) ∖ I ) = (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘(𝐼 + 1)) ∖ I ))
248	247	dmeqd 5248	. . . . . . . . 9 ⊢ (𝑤 = (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩) → dom ((𝑤‘(𝐼 + 1)) ∖ I ) = dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘(𝐼 + 1)) ∖ I ))
249	248	eleq2d 2673	. . . . . . . 8 ⊢ (𝑤 = (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩) → (𝐴 ∈ dom ((𝑤‘(𝐼 + 1)) ∖ I ) ↔ 𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘(𝐼 + 1)) ∖ I )))
250		fveq1 6102	. . . . . . . . . . . . 13 ⊢ (𝑤 = (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩) → (𝑤‘𝑗) = ((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗))
251	250	difeq1d 3689	. . . . . . . . . . . 12 ⊢ (𝑤 = (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩) → ((𝑤‘𝑗) ∖ I ) = (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) ∖ I ))
252	251	dmeqd 5248	. . . . . . . . . . 11 ⊢ (𝑤 = (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩) → dom ((𝑤‘𝑗) ∖ I ) = dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) ∖ I ))
253	252	eleq2d 2673	. . . . . . . . . 10 ⊢ (𝑤 = (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩) → (𝐴 ∈ dom ((𝑤‘𝑗) ∖ I ) ↔ 𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) ∖ I )))
254	253	notbid 307	. . . . . . . . 9 ⊢ (𝑤 = (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩) → (¬ 𝐴 ∈ dom ((𝑤‘𝑗) ∖ I ) ↔ ¬ 𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) ∖ I )))
255	254	ralbidv 2969	. . . . . . . 8 ⊢ (𝑤 = (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩) → (∀𝑗 ∈ (0..^(𝐼 + 1)) ¬ 𝐴 ∈ dom ((𝑤‘𝑗) ∖ I ) ↔ ∀𝑗 ∈ (0..^(𝐼 + 1)) ¬ 𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) ∖ I )))
256	249, 255	3anbi23d 1394	. . . . . . 7 ⊢ (𝑤 = (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩) → (((𝐼 + 1) ∈ (0..^𝐿) ∧ 𝐴 ∈ dom ((𝑤‘(𝐼 + 1)) ∖ I ) ∧ ∀𝑗 ∈ (0..^(𝐼 + 1)) ¬ 𝐴 ∈ dom ((𝑤‘𝑗) ∖ I )) ↔ ((𝐼 + 1) ∈ (0..^𝐿) ∧ 𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘(𝐼 + 1)) ∖ I ) ∧ ∀𝑗 ∈ (0..^(𝐼 + 1)) ¬ 𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) ∖ I ))))
257	245, 256	anbi12d 743	. . . . . 6 ⊢ (𝑤 = (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩) → ((((𝐺 Σg 𝑤) = ( I ↾ 𝐷) ∧ (#‘𝑤) = 𝐿) ∧ ((𝐼 + 1) ∈ (0..^𝐿) ∧ 𝐴 ∈ dom ((𝑤‘(𝐼 + 1)) ∖ I ) ∧ ∀𝑗 ∈ (0..^(𝐼 + 1)) ¬ 𝐴 ∈ dom ((𝑤‘𝑗) ∖ I ))) ↔ (((𝐺 Σg (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)) = ( I ↾ 𝐷) ∧ (#‘(𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)) = 𝐿) ∧ ((𝐼 + 1) ∈ (0..^𝐿) ∧ 𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘(𝐼 + 1)) ∖ I ) ∧ ∀𝑗 ∈ (0..^(𝐼 + 1)) ¬ 𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) ∖ I )))))
258	257	rspcev 3282	. . . . 5 ⊢ (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩) ∈ Word 𝑇 ∧ (((𝐺 Σg (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)) = ( I ↾ 𝐷) ∧ (#‘(𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)) = 𝐿) ∧ ((𝐼 + 1) ∈ (0..^𝐿) ∧ 𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘(𝐼 + 1)) ∖ I ) ∧ ∀𝑗 ∈ (0..^(𝐼 + 1)) ¬ 𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) ∖ I )))) → ∃𝑤 ∈ Word 𝑇(((𝐺 Σg 𝑤) = ( I ↾ 𝐷) ∧ (#‘𝑤) = 𝐿) ∧ ((𝐼 + 1) ∈ (0..^𝐿) ∧ 𝐴 ∈ dom ((𝑤‘(𝐼 + 1)) ∖ I ) ∧ ∀𝑗 ∈ (0..^(𝐼 + 1)) ¬ 𝐴 ∈ dom ((𝑤‘𝑗) ∖ I ))))
259	126, 169, 240, 258	syl12anc 1316	. . . 4 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → ∃𝑤 ∈ Word 𝑇(((𝐺 Σg 𝑤) = ( I ↾ 𝐷) ∧ (#‘𝑤) = 𝐿) ∧ ((𝐼 + 1) ∈ (0..^𝐿) ∧ 𝐴 ∈ dom ((𝑤‘(𝐼 + 1)) ∖ I ) ∧ ∀𝑗 ∈ (0..^(𝐼 + 1)) ¬ 𝐴 ∈ dom ((𝑤‘𝑗) ∖ I ))))
260	259	expr 641	. . 3 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → ((((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )) → ∃𝑤 ∈ Word 𝑇(((𝐺 Σg 𝑤) = ( I ↾ 𝐷) ∧ (#‘𝑤) = 𝐿) ∧ ((𝐼 + 1) ∈ (0..^𝐿) ∧ 𝐴 ∈ dom ((𝑤‘(𝐼 + 1)) ∖ I ) ∧ ∀𝑗 ∈ (0..^(𝐼 + 1)) ¬ 𝐴 ∈ dom ((𝑤‘𝑗) ∖ I )))))
261	260	rexlimdvva 3020	. 2 ⊢ (𝜑 → (∃𝑟 ∈ 𝑇 ∃𝑠 ∈ 𝑇 (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )) → ∃𝑤 ∈ Word 𝑇(((𝐺 Σg 𝑤) = ( I ↾ 𝐷) ∧ (#‘𝑤) = 𝐿) ∧ ((𝐼 + 1) ∈ (0..^𝐿) ∧ 𝐴 ∈ dom ((𝑤‘(𝐼 + 1)) ∖ I ) ∧ ∀𝑗 ∈ (0..^(𝐼 + 1)) ¬ 𝐴 ∈ dom ((𝑤‘𝑗) ∖ I )))))
262	20, 21, 87, 89, 24	psgnunilem1 17736	. 2 ⊢ (𝜑 → (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷) ∨ ∃𝑟 ∈ 𝑇 ∃𝑠 ∈ 𝑇 (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I ))))
263	119, 261, 262	mpjaod 395	1 ⊢ (𝜑 → ∃𝑤 ∈ Word 𝑇(((𝐺 Σg 𝑤) = ( I ↾ 𝐷) ∧ (#‘𝑤) = 𝐿) ∧ ((𝐼 + 1) ∈ (0..^𝐿) ∧ 𝐴 ∈ dom ((𝑤‘(𝐼 + 1)) ∖ I ) ∧ ∀𝑗 ∈ (0..^(𝐼 + 1)) ¬ 𝐴 ∈ dom ((𝑤‘𝑗) ∖ I ))))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∨ wo 382   ∧ wa 383   ∧ w3a 1031   = wceq 1475   ∈ wcel 1977  ∀wral 2896  ∃wrex 2897   ∖ cdif 3537   ⊆ wss 3540  ∅c0 3874  ⟨cop 4131  ⟨cotp 4133   class class class wbr 4583   I cid 4948  dom cdm 5038  ran crn 5039   ↾ cres 5040   ∘ ccom 5042  ⟶wf 5800  ‘cfv 5804  (class class class)co 6549  ℂcc 9813  ℝcr 9814  0cc0 9815  1c1 9816   + caddc 9818   < clt 9953   ≤ cle 9954   − cmin 10145  -cneg 10146  ℕcn 10897  2c2 10947  ℕ₀cn0 11169  ℤcz 11254  ℤ_≥cuz 11563  ...cfz 12197  ..^cfzo 12334  #chash 12979  Word cword 13146   substr csubstr 13150   splice csplice 13151  ⟨“cs2 13437  Basecbs 15695  +_gcplusg 15768  0_gc0g 15923   Σ_g cgsu 15924  Mndcmnd 17117  Grpcgrp 17245  SymGrpcsymg 17620  pmTrspcpmtr 17684

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-xor 1457  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-ot 4134  df-uni 4373  df-int 4411  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-1st 7059  df-2nd 7060  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-2o 7448  df-oadd 7451  df-er 7629  df-map 7746  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845  df-card 8648  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-nn 10898  df-2 10956  df-3 10957  df-4 10958  df-5 10959  df-6 10960  df-7 10961  df-8 10962  df-9 10963  df-n0 11170  df-z 11255  df-uz 11564  df-fz 12198  df-fzo 12335  df-seq 12664  df-hash 12980  df-word 13154  df-lsw 13155  df-concat 13156  df-s1 13157  df-substr 13158  df-splice 13159  df-s2 13444  df-struct 15697  df-ndx 15698  df-slot 15699  df-base 15700  df-sets 15701  df-ress 15702  df-plusg 15781  df-tset 15787  df-0g 15925  df-gsum 15926  df-mgm 17065  df-sgrp 17107  df-mnd 17118  df-submnd 17159  df-grp 17248  df-minusg 17249  df-subg 17414  df-symg 17621  df-pmtr 17685

This theorem is referenced by:  psgnunilem3  17739