Theorem psgnunilem2 19402

Description: Lemma for psgnuni 19406. 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 14441	. . . . . . 7 ⊢ ∅ ∈ Word 𝑇
3		splcl 14654	. . . . . . 7 ⊢ ((𝑊 ∈ Word 𝑇 ∧ ∅ ∈ Word 𝑇) → (𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩) ∈ Word 𝑇)
4	1, 2, 3	sylancl 586	. . . . . 6 ⊢ (𝜑 → (𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩) ∈ Word 𝑇)
5	4	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ ((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷)) → (𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩) ∈ Word 𝑇)
6		fzossfz 13573	. . . . . . . . . . 11 ⊢ (0..^𝐿) ⊆ (0...𝐿)
7		psgnunilem2.ix	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐼 ∈ (0..^𝐿))
8	6, 7	sselid 3927	. . . . . . . . . 10 ⊢ (𝜑 → 𝐼 ∈ (0...𝐿))
9		elfznn0 13515	. . . . . . . . . 10 ⊢ (𝐼 ∈ (0...𝐿) → 𝐼 ∈ ℕ0)
10	8, 9	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝐼 ∈ ℕ0)
11		2nn0 12393	. . . . . . . . . 10 ⊢ 2 ∈ ℕ0
12		nn0addcl 12411	. . . . . . . . . 10 ⊢ ((𝐼 ∈ ℕ0 ∧ 2 ∈ ℕ0) → (𝐼 + 2) ∈ ℕ0)
13	10, 11, 12	sylancl 586	. . . . . . . . 9 ⊢ (𝜑 → (𝐼 + 2) ∈ ℕ0)
14	10	nn0red 12438	. . . . . . . . . 10 ⊢ (𝜑 → 𝐼 ∈ ℝ)
15		nn0addge1 12422	. . . . . . . . . 10 ⊢ ((𝐼 ∈ ℝ ∧ 2 ∈ ℕ0) → 𝐼 ≤ (𝐼 + 2))
16	14, 11, 15	sylancl 586	. . . . . . . . 9 ⊢ (𝜑 → 𝐼 ≤ (𝐼 + 2))
17		elfz2nn0 13513	. . . . . . . . 9 ⊢ (𝐼 ∈ (0...(𝐼 + 2)) ↔ (𝐼 ∈ ℕ0 ∧ (𝐼 + 2) ∈ ℕ0 ∧ 𝐼 ≤ (𝐼 + 2)))
18	10, 13, 16, 17	syl3anbrc 1344	. . . . . . . 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 19401	. . . . . . . . . 10 ⊢ (𝜑 → (𝐼 + 1) ∈ (0..^𝐿))
27		fzofzp1 13659	. . . . . . . . . 10 ⊢ ((𝐼 + 1) ∈ (0..^𝐿) → ((𝐼 + 1) + 1) ∈ (0...𝐿))
28	26, 27	syl 17	. . . . . . . . 9 ⊢ (𝜑 → ((𝐼 + 1) + 1) ∈ (0...𝐿))
29		df-2 12183	. . . . . . . . . . 11 ⊢ 2 = (1 + 1)
30	29	oveq2i 7352	. . . . . . . . . 10 ⊢ (𝐼 + 2) = (𝐼 + (1 + 1))
31	10	nn0cnd 12439	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐼 ∈ ℂ)
32		1cnd 11102	. . . . . . . . . . 11 ⊢ (𝜑 → 1 ∈ ℂ)
33	31, 32, 32	addassd 11129	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐼 + 1) + 1) = (𝐼 + (1 + 1)))
34	30, 33	eqtr4id 2785	. . . . . . . . 9 ⊢ (𝜑 → (𝐼 + 2) = ((𝐼 + 1) + 1))
35	23	oveq2d 7357	. . . . . . . . 9 ⊢ (𝜑 → (0...(♯‘𝑊)) = (0...𝐿))
36	28, 34, 35	3eltr4d 2846	. . . . . . . 8 ⊢ (𝜑 → (𝐼 + 2) ∈ (0...(♯‘𝑊)))
37	2	a1i 11	. . . . . . . 8 ⊢ (𝜑 → ∅ ∈ Word 𝑇)
38	1, 18, 36, 37	spllen 14656	. . . . . . 7 ⊢ (𝜑 → (♯‘(𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩)) = ((♯‘𝑊) + ((♯‘∅) − ((𝐼 + 2) − 𝐼))))
39		hash0 14269	. . . . . . . . . . 11 ⊢ (♯‘∅) = 0
40	39	oveq1i 7351	. . . . . . . . . 10 ⊢ ((♯‘∅) − ((𝐼 + 2) − 𝐼)) = (0 − ((𝐼 + 2) − 𝐼))
41		df-neg 11342	. . . . . . . . . 10 ⊢ -((𝐼 + 2) − 𝐼) = (0 − ((𝐼 + 2) − 𝐼))
42	40, 41	eqtr4i 2757	. . . . . . . . 9 ⊢ ((♯‘∅) − ((𝐼 + 2) − 𝐼)) = -((𝐼 + 2) − 𝐼)
43		2cn 12195	. . . . . . . . . . 11 ⊢ 2 ∈ ℂ
44		pncan2 11362	. . . . . . . . . . 11 ⊢ ((𝐼 ∈ ℂ ∧ 2 ∈ ℂ) → ((𝐼 + 2) − 𝐼) = 2)
45	31, 43, 44	sylancl 586	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐼 + 2) − 𝐼) = 2)
46	45	negeqd 11349	. . . . . . . . 9 ⊢ (𝜑 → -((𝐼 + 2) − 𝐼) = -2)
47	42, 46	eqtrid 2778	. . . . . . . 8 ⊢ (𝜑 → ((♯‘∅) − ((𝐼 + 2) − 𝐼)) = -2)
48	23, 47	oveq12d 7359	. . . . . . 7 ⊢ (𝜑 → ((♯‘𝑊) + ((♯‘∅) − ((𝐼 + 2) − 𝐼))) = (𝐿 + -2))
49		elfzel2 13417	. . . . . . . . . 10 ⊢ (𝐼 ∈ (0...𝐿) → 𝐿 ∈ ℤ)
50	8, 49	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝐿 ∈ ℤ)
51	50	zcnd 12573	. . . . . . . 8 ⊢ (𝜑 → 𝐿 ∈ ℂ)
52		negsub 11404	. . . . . . . 8 ⊢ ((𝐿 ∈ ℂ ∧ 2 ∈ ℂ) → (𝐿 + -2) = (𝐿 − 2))
53	51, 43, 52	sylancl 586	. . . . . . 7 ⊢ (𝜑 → (𝐿 + -2) = (𝐿 − 2))
54	38, 48, 53	3eqtrd 2770	. . . . . 6 ⊢ (𝜑 → (♯‘(𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩)) = (𝐿 − 2))
55	54	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ ((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷)) → (♯‘(𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩)) = (𝐿 − 2))
56		splid 14655	. . . . . . . . 9 ⊢ ((𝑊 ∈ Word 𝑇 ∧ (𝐼 ∈ (0...(𝐼 + 2)) ∧ (𝐼 + 2) ∈ (0...(♯‘𝑊)))) → (𝑊 splice ⟨𝐼, (𝐼 + 2), (𝑊 substr ⟨𝐼, (𝐼 + 2)⟩)⟩) = 𝑊)
57	1, 18, 36, 56	syl12anc 836	. . . . . . . 8 ⊢ (𝜑 → (𝑊 splice ⟨𝐼, (𝐼 + 2), (𝑊 substr ⟨𝐼, (𝐼 + 2)⟩)⟩) = 𝑊)
58	57	oveq2d 7357	. . . . . . 7 ⊢ (𝜑 → (𝐺 Σg (𝑊 splice ⟨𝐼, (𝐼 + 2), (𝑊 substr ⟨𝐼, (𝐼 + 2)⟩)⟩)) = (𝐺 Σg 𝑊))
59	58	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷)) → (𝐺 Σg (𝑊 splice ⟨𝐼, (𝐼 + 2), (𝑊 substr ⟨𝐼, (𝐼 + 2)⟩)⟩)) = (𝐺 Σg 𝑊))
60		eqid 2731	. . . . . . 7 ⊢ (Base‘𝐺) = (Base‘𝐺)
61	19	symggrp 19307	. . . . . . . . . 10 ⊢ (𝐷 ∈ 𝑉 → 𝐺 ∈ Grp)
62	21, 61	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝐺 ∈ Grp)
63	62	grpmndd 18854	. . . . . . . 8 ⊢ (𝜑 → 𝐺 ∈ Mnd)
64	63	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷)) → 𝐺 ∈ Mnd)
65	20, 19, 60	symgtrf 19376	. . . . . . . . . 10 ⊢ 𝑇 ⊆ (Base‘𝐺)
66		sswrd 14424	. . . . . . . . . 10 ⊢ (𝑇 ⊆ (Base‘𝐺) → Word 𝑇 ⊆ Word (Base‘𝐺))
67	65, 66	ax-mp 5	. . . . . . . . 9 ⊢ Word 𝑇 ⊆ Word (Base‘𝐺)
68	67, 1	sselid 3927	. . . . . . . 8 ⊢ (𝜑 → 𝑊 ∈ Word (Base‘𝐺))
69	68	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷)) → 𝑊 ∈ Word (Base‘𝐺))
70	18	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷)) → 𝐼 ∈ (0...(𝐼 + 2)))
71	36	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷)) → (𝐼 + 2) ∈ (0...(♯‘𝑊)))
72		swrdcl 14548	. . . . . . . . 9 ⊢ (𝑊 ∈ Word (Base‘𝐺) → (𝑊 substr ⟨𝐼, (𝐼 + 2)⟩) ∈ Word (Base‘𝐺))
73	68, 72	syl 17	. . . . . . . 8 ⊢ (𝜑 → (𝑊 substr ⟨𝐼, (𝐼 + 2)⟩) ∈ Word (Base‘𝐺))
74	73	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷)) → (𝑊 substr ⟨𝐼, (𝐼 + 2)⟩) ∈ Word (Base‘𝐺))
75		wrd0 14441	. . . . . . . 8 ⊢ ∅ ∈ Word (Base‘𝐺)
76	75	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷)) → ∅ ∈ Word (Base‘𝐺))
77	23	oveq2d 7357	. . . . . . . . . . . . 13 ⊢ (𝜑 → (0..^(♯‘𝑊)) = (0..^𝐿))
78	26, 77	eleqtrrd 2834	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐼 + 1) ∈ (0..^(♯‘𝑊)))
79		swrds2 14842	. . . . . . . . . . . 12 ⊢ ((𝑊 ∈ Word 𝑇 ∧ 𝐼 ∈ ℕ0 ∧ (𝐼 + 1) ∈ (0..^(♯‘𝑊))) → (𝑊 substr ⟨𝐼, (𝐼 + 2)⟩) = ⟨“(𝑊‘𝐼)(𝑊‘(𝐼 + 1))”⟩)
80	1, 10, 78, 79	syl3anc 1373	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑊 substr ⟨𝐼, (𝐼 + 2)⟩) = ⟨“(𝑊‘𝐼)(𝑊‘(𝐼 + 1))”⟩)
81	80	oveq2d 7357	. . . . . . . . . 10 ⊢ (𝜑 → (𝐺 Σg (𝑊 substr ⟨𝐼, (𝐼 + 2)⟩)) = (𝐺 Σg ⟨“(𝑊‘𝐼)(𝑊‘(𝐼 + 1))”⟩))
82		wrdf 14420	. . . . . . . . . . . . . . 15 ⊢ (𝑊 ∈ Word 𝑇 → 𝑊:(0..^(♯‘𝑊))⟶𝑇)
83	1, 82	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑊:(0..^(♯‘𝑊))⟶𝑇)
84	77	feq2d 6630	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑊:(0..^(♯‘𝑊))⟶𝑇 ↔ 𝑊:(0..^𝐿)⟶𝑇))
85	83, 84	mpbid 232	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑊:(0..^𝐿)⟶𝑇)
86	85, 7	ffvelcdmd 7013	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑊‘𝐼) ∈ 𝑇)
87	65, 86	sselid 3927	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑊‘𝐼) ∈ (Base‘𝐺))
88	85, 26	ffvelcdmd 7013	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑊‘(𝐼 + 1)) ∈ 𝑇)
89	65, 88	sselid 3927	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑊‘(𝐼 + 1)) ∈ (Base‘𝐺))
90		eqid 2731	. . . . . . . . . . . 12 ⊢ (+g‘𝐺) = (+g‘𝐺)
91	60, 90	gsumws2 18745	. . . . . . . . . . 11 ⊢ ((𝐺 ∈ Mnd ∧ (𝑊‘𝐼) ∈ (Base‘𝐺) ∧ (𝑊‘(𝐼 + 1)) ∈ (Base‘𝐺)) → (𝐺 Σg ⟨“(𝑊‘𝐼)(𝑊‘(𝐼 + 1))”⟩) = ((𝑊‘𝐼)(+g‘𝐺)(𝑊‘(𝐼 + 1))))
92	63, 87, 89, 91	syl3anc 1373	. . . . . . . . . 10 ⊢ (𝜑 → (𝐺 Σg ⟨“(𝑊‘𝐼)(𝑊‘(𝐼 + 1))”⟩) = ((𝑊‘𝐼)(+g‘𝐺)(𝑊‘(𝐼 + 1))))
93	19, 60, 90	symgov 19291	. . . . . . . . . . 11 ⊢ (((𝑊‘𝐼) ∈ (Base‘𝐺) ∧ (𝑊‘(𝐼 + 1)) ∈ (Base‘𝐺)) → ((𝑊‘𝐼)(+g‘𝐺)(𝑊‘(𝐼 + 1))) = ((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))))
94	87, 89, 93	syl2anc 584	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑊‘𝐼)(+g‘𝐺)(𝑊‘(𝐼 + 1))) = ((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))))
95	81, 92, 94	3eqtrd 2770	. . . . . . . . 9 ⊢ (𝜑 → (𝐺 Σg (𝑊 substr ⟨𝐼, (𝐼 + 2)⟩)) = ((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))))
96	95	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷)) → (𝐺 Σg (𝑊 substr ⟨𝐼, (𝐼 + 2)⟩)) = ((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))))
97		simpr 484	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷)) → ((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷))
98	19	symgid 19308	. . . . . . . . . . 11 ⊢ (𝐷 ∈ 𝑉 → ( I ↾ 𝐷) = (0g‘𝐺))
99	21, 98	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → ( I ↾ 𝐷) = (0g‘𝐺))
100		eqid 2731	. . . . . . . . . . 11 ⊢ (0g‘𝐺) = (0g‘𝐺)
101	100	gsum0 18587	. . . . . . . . . 10 ⊢ (𝐺 Σg ∅) = (0g‘𝐺)
102	99, 101	eqtr4di 2784	. . . . . . . . 9 ⊢ (𝜑 → ( I ↾ 𝐷) = (𝐺 Σg ∅))
103	102	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷)) → ( I ↾ 𝐷) = (𝐺 Σg ∅))
104	96, 97, 103	3eqtrd 2770	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷)) → (𝐺 Σg (𝑊 substr ⟨𝐼, (𝐼 + 2)⟩)) = (𝐺 Σg ∅))
105	60, 64, 69, 70, 71, 74, 76, 104	gsumspl 18747	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷)) → (𝐺 Σg (𝑊 splice ⟨𝐼, (𝐼 + 2), (𝑊 substr ⟨𝐼, (𝐼 + 2)⟩)⟩)) = (𝐺 Σg (𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩)))
106	22	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷)) → (𝐺 Σg 𝑊) = ( I ↾ 𝐷))
107	59, 105, 106	3eqtr3d 2774	. . . . 5 ⊢ ((𝜑 ∧ ((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷)) → (𝐺 Σg (𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩)) = ( I ↾ 𝐷))
108		fveqeq2 6826	. . . . . . 7 ⊢ (𝑥 = (𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩) → ((♯‘𝑥) = (𝐿 − 2) ↔ (♯‘(𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩)) = (𝐿 − 2)))
109		oveq2 7349	. . . . . . . 8 ⊢ (𝑥 = (𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩) → (𝐺 Σg 𝑥) = (𝐺 Σg (𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩)))
110	109	eqeq1d 2733	. . . . . . 7 ⊢ (𝑥 = (𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩) → ((𝐺 Σg 𝑥) = ( I ↾ 𝐷) ↔ (𝐺 Σg (𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩)) = ( I ↾ 𝐷)))
111	108, 110	anbi12d 632	. . . . . 6 ⊢ (𝑥 = (𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩) → (((♯‘𝑥) = (𝐿 − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)) ↔ ((♯‘(𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩)) = (𝐿 − 2) ∧ (𝐺 Σg (𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩)) = ( I ↾ 𝐷))))
112	111	rspcev 3572	. . . . 5 ⊢ (((𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩) ∈ Word 𝑇 ∧ ((♯‘(𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩)) = (𝐿 − 2) ∧ (𝐺 Σg (𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩)) = ( I ↾ 𝐷))) → ∃𝑥 ∈ Word 𝑇((♯‘𝑥) = (𝐿 − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)))
113	5, 55, 107, 112	syl12anc 836	. . . 4 ⊢ ((𝜑 ∧ ((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷)) → ∃𝑥 ∈ Word 𝑇((♯‘𝑥) = (𝐿 − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)))
114		psgnunilem2.in	. . . . 5 ⊢ (𝜑 → ¬ ∃𝑥 ∈ Word 𝑇((♯‘𝑥) = (𝐿 − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)))
115	114	adantr 480	. . . 4 ⊢ ((𝜑 ∧ ((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷)) → ¬ ∃𝑥 ∈ Word 𝑇((♯‘𝑥) = (𝐿 − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)))
116	113, 115	pm2.21dd 195	. . 3 ⊢ ((𝜑 ∧ ((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷)) → ∃𝑤 ∈ Word 𝑇(((𝐺 Σg 𝑤) = ( I ↾ 𝐷) ∧ (♯‘𝑤) = 𝐿) ∧ ((𝐼 + 1) ∈ (0..^𝐿) ∧ 𝐴 ∈ dom ((𝑤‘(𝐼 + 1)) ∖ I ) ∧ ∀𝑗 ∈ (0..^(𝐼 + 1)) ¬ 𝐴 ∈ dom ((𝑤‘𝑗) ∖ I ))))
117	116	ex 412	. 2 ⊢ (𝜑 → (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷) → ∃𝑤 ∈ Word 𝑇(((𝐺 Σg 𝑤) = ( I ↾ 𝐷) ∧ (♯‘𝑤) = 𝐿) ∧ ((𝐼 + 1) ∈ (0..^𝐿) ∧ 𝐴 ∈ dom ((𝑤‘(𝐼 + 1)) ∖ I ) ∧ ∀𝑗 ∈ (0..^(𝐼 + 1)) ¬ 𝐴 ∈ dom ((𝑤‘𝑗) ∖ I )))))
118	1	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → 𝑊 ∈ Word 𝑇)
119		simprl 770	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → 𝑟 ∈ 𝑇)
120		simprr 772	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → 𝑠 ∈ 𝑇)
121	119, 120	s2cld 14773	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → ⟨“𝑟𝑠”⟩ ∈ Word 𝑇)
122		splcl 14654	. . . . . . 7 ⊢ ((𝑊 ∈ Word 𝑇 ∧ ⟨“𝑟𝑠”⟩ ∈ Word 𝑇) → (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩) ∈ Word 𝑇)
123	118, 121, 122	syl2anc 584	. . . . . 6 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩) ∈ Word 𝑇)
124	123	adantrr 717	. . . . 5 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩) ∈ Word 𝑇)
125	63	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → 𝐺 ∈ Mnd)
126	68	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → 𝑊 ∈ Word (Base‘𝐺))
127	18	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → 𝐼 ∈ (0...(𝐼 + 2)))
128	36	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → (𝐼 + 2) ∈ (0...(♯‘𝑊)))
129	67, 121	sselid 3927	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → ⟨“𝑟𝑠”⟩ ∈ Word (Base‘𝐺))
130	129	adantrr 717	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → ⟨“𝑟𝑠”⟩ ∈ Word (Base‘𝐺))
131	73	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → (𝑊 substr ⟨𝐼, (𝐼 + 2)⟩) ∈ Word (Base‘𝐺))
132		simprr1 1222	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → ((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠))
133	95	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → (𝐺 Σg (𝑊 substr ⟨𝐼, (𝐼 + 2)⟩)) = ((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))))
134	63	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → 𝐺 ∈ Mnd)
135	65	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑇 ⊆ (Base‘𝐺))
136	135	sselda 3929	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑟 ∈ 𝑇) → 𝑟 ∈ (Base‘𝐺))
137	136	adantrr 717	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → 𝑟 ∈ (Base‘𝐺))
138	135	sselda 3929	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝑇) → 𝑠 ∈ (Base‘𝐺))
139	138	adantrl 716	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → 𝑠 ∈ (Base‘𝐺))
140	60, 90	gsumws2 18745	. . . . . . . . . . . 12 ⊢ ((𝐺 ∈ Mnd ∧ 𝑟 ∈ (Base‘𝐺) ∧ 𝑠 ∈ (Base‘𝐺)) → (𝐺 Σg ⟨“𝑟𝑠”⟩) = (𝑟(+g‘𝐺)𝑠))
141	134, 137, 139, 140	syl3anc 1373	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → (𝐺 Σg ⟨“𝑟𝑠”⟩) = (𝑟(+g‘𝐺)𝑠))
142	19, 60, 90	symgov 19291	. . . . . . . . . . . 12 ⊢ ((𝑟 ∈ (Base‘𝐺) ∧ 𝑠 ∈ (Base‘𝐺)) → (𝑟(+g‘𝐺)𝑠) = (𝑟 ∘ 𝑠))
143	137, 139, 142	syl2anc 584	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → (𝑟(+g‘𝐺)𝑠) = (𝑟 ∘ 𝑠))
144	141, 143	eqtrd 2766	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → (𝐺 Σg ⟨“𝑟𝑠”⟩) = (𝑟 ∘ 𝑠))
145	144	adantrr 717	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → (𝐺 Σg ⟨“𝑟𝑠”⟩) = (𝑟 ∘ 𝑠))
146	132, 133, 145	3eqtr4rd 2777	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → (𝐺 Σg ⟨“𝑟𝑠”⟩) = (𝐺 Σg (𝑊 substr ⟨𝐼, (𝐼 + 2)⟩)))
147	60, 125, 126, 127, 128, 130, 131, 146	gsumspl 18747	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → (𝐺 Σg (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)) = (𝐺 Σg (𝑊 splice ⟨𝐼, (𝐼 + 2), (𝑊 substr ⟨𝐼, (𝐼 + 2)⟩)⟩)))
148	58	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → (𝐺 Σg (𝑊 splice ⟨𝐼, (𝐼 + 2), (𝑊 substr ⟨𝐼, (𝐼 + 2)⟩)⟩)) = (𝐺 Σg 𝑊))
149	22	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → (𝐺 Σg 𝑊) = ( I ↾ 𝐷))
150	147, 148, 149	3eqtrd 2770	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → (𝐺 Σg (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)) = ( I ↾ 𝐷))
151	18	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → 𝐼 ∈ (0...(𝐼 + 2)))
152	36	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → (𝐼 + 2) ∈ (0...(♯‘𝑊)))
153	118, 151, 152, 121	spllen 14656	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → (♯‘(𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)) = ((♯‘𝑊) + ((♯‘⟨“𝑟𝑠”⟩) − ((𝐼 + 2) − 𝐼))))
154		s2len 14791	. . . . . . . . . . . . 13 ⊢ (♯‘⟨“𝑟𝑠”⟩) = 2
155	154	oveq1i 7351	. . . . . . . . . . . 12 ⊢ ((♯‘⟨“𝑟𝑠”⟩) − ((𝐼 + 2) − 𝐼)) = (2 − ((𝐼 + 2) − 𝐼))
156	45	oveq2d 7357	. . . . . . . . . . . . 13 ⊢ (𝜑 → (2 − ((𝐼 + 2) − 𝐼)) = (2 − 2))
157	43	subidi 11427	. . . . . . . . . . . . 13 ⊢ (2 − 2) = 0
158	156, 157	eqtrdi 2782	. . . . . . . . . . . 12 ⊢ (𝜑 → (2 − ((𝐼 + 2) − 𝐼)) = 0)
159	155, 158	eqtrid 2778	. . . . . . . . . . 11 ⊢ (𝜑 → ((♯‘⟨“𝑟𝑠”⟩) − ((𝐼 + 2) − 𝐼)) = 0)
160	159	oveq2d 7357	. . . . . . . . . 10 ⊢ (𝜑 → ((♯‘𝑊) + ((♯‘⟨“𝑟𝑠”⟩) − ((𝐼 + 2) − 𝐼))) = ((♯‘𝑊) + 0))
161	23, 51	eqeltrd 2831	. . . . . . . . . . 11 ⊢ (𝜑 → (♯‘𝑊) ∈ ℂ)
162	161	addridd 11308	. . . . . . . . . 10 ⊢ (𝜑 → ((♯‘𝑊) + 0) = (♯‘𝑊))
163	160, 162, 23	3eqtrd 2770	. . . . . . . . 9 ⊢ (𝜑 → ((♯‘𝑊) + ((♯‘⟨“𝑟𝑠”⟩) − ((𝐼 + 2) − 𝐼))) = 𝐿)
164	163	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → ((♯‘𝑊) + ((♯‘⟨“𝑟𝑠”⟩) − ((𝐼 + 2) − 𝐼))) = 𝐿)
165	153, 164	eqtrd 2766	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → (♯‘(𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)) = 𝐿)
166	165	adantrr 717	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → (♯‘(𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)) = 𝐿)
167	150, 166	jca 511	. . . . 5 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → ((𝐺 Σg (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)) = ( I ↾ 𝐷) ∧ (♯‘(𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)) = 𝐿))
168	26	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → (𝐼 + 1) ∈ (0..^𝐿))
169		simprr2 1223	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → 𝐴 ∈ dom (𝑠 ∖ I ))
170		1nn0 12392	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ ℕ0
171		2nn 12193	. . . . . . . . . . . . . . 15 ⊢ 2 ∈ ℕ
172		1lt2 12286	. . . . . . . . . . . . . . 15 ⊢ 1 < 2
173		elfzo0 13595	. . . . . . . . . . . . . . 15 ⊢ (1 ∈ (0..^2) ↔ (1 ∈ ℕ0 ∧ 2 ∈ ℕ ∧ 1 < 2))
174	170, 171, 172, 173	mpbir3an 1342	. . . . . . . . . . . . . 14 ⊢ 1 ∈ (0..^2)
175	154	oveq2i 7352	. . . . . . . . . . . . . 14 ⊢ (0..^(♯‘⟨“𝑟𝑠”⟩)) = (0..^2)
176	174, 175	eleqtrri 2830	. . . . . . . . . . . . 13 ⊢ 1 ∈ (0..^(♯‘⟨“𝑟𝑠”⟩))
177	176	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → 1 ∈ (0..^(♯‘⟨“𝑟𝑠”⟩)))
178	118, 151, 152, 121, 177	splfv2a 14658	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → ((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘(𝐼 + 1)) = (⟨“𝑟𝑠”⟩‘1))
179		s2fv1 14790	. . . . . . . . . . . 12 ⊢ (𝑠 ∈ 𝑇 → (⟨“𝑟𝑠”⟩‘1) = 𝑠)
180	179	ad2antll 729	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → (⟨“𝑟𝑠”⟩‘1) = 𝑠)
181	178, 180	eqtrd 2766	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → ((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘(𝐼 + 1)) = 𝑠)
182	181	adantrr 717	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → ((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘(𝐼 + 1)) = 𝑠)
183	182	difeq1d 4070	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘(𝐼 + 1)) ∖ I ) = (𝑠 ∖ I ))
184	183	dmeqd 5840	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘(𝐼 + 1)) ∖ I ) = dom (𝑠 ∖ I ))
185	169, 184	eleqtrrd 2834	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → 𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘(𝐼 + 1)) ∖ I ))
186		fzosplitsni 13674	. . . . . . . . . . 11 ⊢ (𝐼 ∈ (ℤ≥‘0) → (𝑗 ∈ (0..^(𝐼 + 1)) ↔ (𝑗 ∈ (0..^𝐼) ∨ 𝑗 = 𝐼)))
187		nn0uz 12769	. . . . . . . . . . 11 ⊢ ℕ0 = (ℤ≥‘0)
188	186, 187	eleq2s 2849	. . . . . . . . . 10 ⊢ (𝐼 ∈ ℕ0 → (𝑗 ∈ (0..^(𝐼 + 1)) ↔ (𝑗 ∈ (0..^𝐼) ∨ 𝑗 = 𝐼)))
189	10, 188	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (𝑗 ∈ (0..^(𝐼 + 1)) ↔ (𝑗 ∈ (0..^𝐼) ∨ 𝑗 = 𝐼)))
190	189	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → (𝑗 ∈ (0..^(𝐼 + 1)) ↔ (𝑗 ∈ (0..^𝐼) ∨ 𝑗 = 𝐼)))
191		fveq2 6817	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 𝑗 → (𝑊‘𝑘) = (𝑊‘𝑗))
192	191	difeq1d 4070	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 𝑗 → ((𝑊‘𝑘) ∖ I ) = ((𝑊‘𝑗) ∖ I ))
193	192	dmeqd 5840	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 𝑗 → dom ((𝑊‘𝑘) ∖ I ) = dom ((𝑊‘𝑗) ∖ I ))
194	193	eleq2d 2817	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 𝑗 → (𝐴 ∈ dom ((𝑊‘𝑘) ∖ I ) ↔ 𝐴 ∈ dom ((𝑊‘𝑗) ∖ I )))
195	194	notbid 318	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑗 → (¬ 𝐴 ∈ dom ((𝑊‘𝑘) ∖ I ) ↔ ¬ 𝐴 ∈ dom ((𝑊‘𝑗) ∖ I )))
196	195	rspccva 3571	. . . . . . . . . . . . . 14 ⊢ ((∀𝑘 ∈ (0..^𝐼) ¬ 𝐴 ∈ dom ((𝑊‘𝑘) ∖ I ) ∧ 𝑗 ∈ (0..^𝐼)) → ¬ 𝐴 ∈ dom ((𝑊‘𝑗) ∖ I ))
197	25, 196	sylan 580	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝐼)) → ¬ 𝐴 ∈ dom ((𝑊‘𝑗) ∖ I ))
198	197	adantlr 715	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) ∧ 𝑗 ∈ (0..^𝐼)) → ¬ 𝐴 ∈ dom ((𝑊‘𝑗) ∖ I ))
199	1	ad2antrr 726	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) ∧ 𝑗 ∈ (0..^𝐼)) → 𝑊 ∈ Word 𝑇)
200	18	ad2antrr 726	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) ∧ 𝑗 ∈ (0..^𝐼)) → 𝐼 ∈ (0...(𝐼 + 2)))
201	36	ad2antrr 726	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) ∧ 𝑗 ∈ (0..^𝐼)) → (𝐼 + 2) ∈ (0...(♯‘𝑊)))
202	121	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) ∧ 𝑗 ∈ (0..^𝐼)) → ⟨“𝑟𝑠”⟩ ∈ Word 𝑇)
203		simpr 484	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) ∧ 𝑗 ∈ (0..^𝐼)) → 𝑗 ∈ (0..^𝐼))
204	199, 200, 201, 202, 203	splfv1 14657	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) ∧ 𝑗 ∈ (0..^𝐼)) → ((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) = (𝑊‘𝑗))
205	204	difeq1d 4070	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) ∧ 𝑗 ∈ (0..^𝐼)) → (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) ∖ I ) = ((𝑊‘𝑗) ∖ I ))
206	205	dmeqd 5840	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) ∧ 𝑗 ∈ (0..^𝐼)) → dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) ∖ I ) = dom ((𝑊‘𝑗) ∖ I ))
207	198, 206	neleqtrrd 2854	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) ∧ 𝑗 ∈ (0..^𝐼)) → ¬ 𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) ∖ I ))
208	207	ex 412	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → (𝑗 ∈ (0..^𝐼) → ¬ 𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) ∖ I )))
209	208	adantrr 717	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → (𝑗 ∈ (0..^𝐼) → ¬ 𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) ∖ I )))
210		simprr3 1224	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → ¬ 𝐴 ∈ dom (𝑟 ∖ I ))
211		0nn0 12391	. . . . . . . . . . . . . . . . . . . 20 ⊢ 0 ∈ ℕ0
212		2pos 12223	. . . . . . . . . . . . . . . . . . . 20 ⊢ 0 < 2
213		elfzo0 13595	. . . . . . . . . . . . . . . . . . . 20 ⊢ (0 ∈ (0..^2) ↔ (0 ∈ ℕ0 ∧ 2 ∈ ℕ ∧ 0 < 2))
214	211, 171, 212, 213	mpbir3an 1342	. . . . . . . . . . . . . . . . . . 19 ⊢ 0 ∈ (0..^2)
215	214, 175	eleqtrri 2830	. . . . . . . . . . . . . . . . . 18 ⊢ 0 ∈ (0..^(♯‘⟨“𝑟𝑠”⟩))
216	215	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → 0 ∈ (0..^(♯‘⟨“𝑟𝑠”⟩)))
217	118, 151, 152, 121, 216	splfv2a 14658	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → ((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘(𝐼 + 0)) = (⟨“𝑟𝑠”⟩‘0))
218	31	addridd 11308	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐼 + 0) = 𝐼)
219	218	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → (𝐼 + 0) = 𝐼)
220	219	fveq2d 6821	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → ((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘(𝐼 + 0)) = ((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝐼))
221		s2fv0 14789	. . . . . . . . . . . . . . . . 17 ⊢ (𝑟 ∈ 𝑇 → (⟨“𝑟𝑠”⟩‘0) = 𝑟)
222	221	ad2antrl 728	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → (⟨“𝑟𝑠”⟩‘0) = 𝑟)
223	217, 220, 222	3eqtr3d 2774	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → ((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝐼) = 𝑟)
224	223	difeq1d 4070	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝐼) ∖ I ) = (𝑟 ∖ I ))
225	224	dmeqd 5840	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝐼) ∖ I ) = dom (𝑟 ∖ I ))
226	225	eleq2d 2817	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → (𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝐼) ∖ I ) ↔ 𝐴 ∈ dom (𝑟 ∖ I )))
227	226	adantrr 717	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → (𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝐼) ∖ I ) ↔ 𝐴 ∈ dom (𝑟 ∖ I )))
228	210, 227	mtbird 325	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → ¬ 𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝐼) ∖ I ))
229		fveq2 6817	. . . . . . . . . . . . . 14 ⊢ (𝑗 = 𝐼 → ((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) = ((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝐼))
230	229	difeq1d 4070	. . . . . . . . . . . . 13 ⊢ (𝑗 = 𝐼 → (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) ∖ I ) = (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝐼) ∖ I ))
231	230	dmeqd 5840	. . . . . . . . . . . 12 ⊢ (𝑗 = 𝐼 → dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) ∖ I ) = dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝐼) ∖ I ))
232	231	eleq2d 2817	. . . . . . . . . . 11 ⊢ (𝑗 = 𝐼 → (𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) ∖ I ) ↔ 𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝐼) ∖ I )))
233	232	notbid 318	. . . . . . . . . 10 ⊢ (𝑗 = 𝐼 → (¬ 𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) ∖ I ) ↔ ¬ 𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝐼) ∖ I )))
234	228, 233	syl5ibrcom 247	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → (𝑗 = 𝐼 → ¬ 𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) ∖ I )))
235	209, 234	jaod 859	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → ((𝑗 ∈ (0..^𝐼) ∨ 𝑗 = 𝐼) → ¬ 𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) ∖ I )))
236	190, 235	sylbid 240	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → (𝑗 ∈ (0..^(𝐼 + 1)) → ¬ 𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) ∖ I )))
237	236	ralrimiv 3123	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → ∀𝑗 ∈ (0..^(𝐼 + 1)) ¬ 𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) ∖ I ))
238	168, 185, 237	3jca 1128	. . . . 5 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → ((𝐼 + 1) ∈ (0..^𝐿) ∧ 𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘(𝐼 + 1)) ∖ I ) ∧ ∀𝑗 ∈ (0..^(𝐼 + 1)) ¬ 𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) ∖ I )))
239		oveq2 7349	. . . . . . . . 9 ⊢ (𝑤 = (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩) → (𝐺 Σg 𝑤) = (𝐺 Σg (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)))
240	239	eqeq1d 2733	. . . . . . . 8 ⊢ (𝑤 = (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩) → ((𝐺 Σg 𝑤) = ( I ↾ 𝐷) ↔ (𝐺 Σg (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)) = ( I ↾ 𝐷)))
241		fveqeq2 6826	. . . . . . . 8 ⊢ (𝑤 = (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩) → ((♯‘𝑤) = 𝐿 ↔ (♯‘(𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)) = 𝐿))
242	240, 241	anbi12d 632	. . . . . . 7 ⊢ (𝑤 = (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩) → (((𝐺 Σg 𝑤) = ( I ↾ 𝐷) ∧ (♯‘𝑤) = 𝐿) ↔ ((𝐺 Σg (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)) = ( I ↾ 𝐷) ∧ (♯‘(𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)) = 𝐿)))
243		fveq1 6816	. . . . . . . . . . 11 ⊢ (𝑤 = (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩) → (𝑤‘(𝐼 + 1)) = ((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘(𝐼 + 1)))
244	243	difeq1d 4070	. . . . . . . . . 10 ⊢ (𝑤 = (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩) → ((𝑤‘(𝐼 + 1)) ∖ I ) = (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘(𝐼 + 1)) ∖ I ))
245	244	dmeqd 5840	. . . . . . . . 9 ⊢ (𝑤 = (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩) → dom ((𝑤‘(𝐼 + 1)) ∖ I ) = dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘(𝐼 + 1)) ∖ I ))
246	245	eleq2d 2817	. . . . . . . 8 ⊢ (𝑤 = (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩) → (𝐴 ∈ dom ((𝑤‘(𝐼 + 1)) ∖ I ) ↔ 𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘(𝐼 + 1)) ∖ I )))
247		fveq1 6816	. . . . . . . . . . . . 13 ⊢ (𝑤 = (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩) → (𝑤‘𝑗) = ((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗))
248	247	difeq1d 4070	. . . . . . . . . . . 12 ⊢ (𝑤 = (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩) → ((𝑤‘𝑗) ∖ I ) = (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) ∖ I ))
249	248	dmeqd 5840	. . . . . . . . . . 11 ⊢ (𝑤 = (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩) → dom ((𝑤‘𝑗) ∖ I ) = dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) ∖ I ))
250	249	eleq2d 2817	. . . . . . . . . 10 ⊢ (𝑤 = (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩) → (𝐴 ∈ dom ((𝑤‘𝑗) ∖ I ) ↔ 𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) ∖ I )))
251	250	notbid 318	. . . . . . . . 9 ⊢ (𝑤 = (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩) → (¬ 𝐴 ∈ dom ((𝑤‘𝑗) ∖ I ) ↔ ¬ 𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) ∖ I )))
252	251	ralbidv 3155	. . . . . . . 8 ⊢ (𝑤 = (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩) → (∀𝑗 ∈ (0..^(𝐼 + 1)) ¬ 𝐴 ∈ dom ((𝑤‘𝑗) ∖ I ) ↔ ∀𝑗 ∈ (0..^(𝐼 + 1)) ¬ 𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) ∖ I )))
253	246, 252	3anbi23d 1441	. . . . . . 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 ))))
254	242, 253	anbi12d 632	. . . . . 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 )))))
255	254	rspcev 3572	. . . . 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 ))))
256	124, 167, 238, 255	syl12anc 836	. . . 4 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → ∃𝑤 ∈ Word 𝑇(((𝐺 Σg 𝑤) = ( I ↾ 𝐷) ∧ (♯‘𝑤) = 𝐿) ∧ ((𝐼 + 1) ∈ (0..^𝐿) ∧ 𝐴 ∈ dom ((𝑤‘(𝐼 + 1)) ∖ I ) ∧ ∀𝑗 ∈ (0..^(𝐼 + 1)) ¬ 𝐴 ∈ dom ((𝑤‘𝑗) ∖ I ))))
257	256	expr 456	. . 3 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → ((((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )) → ∃𝑤 ∈ Word 𝑇(((𝐺 Σg 𝑤) = ( I ↾ 𝐷) ∧ (♯‘𝑤) = 𝐿) ∧ ((𝐼 + 1) ∈ (0..^𝐿) ∧ 𝐴 ∈ dom ((𝑤‘(𝐼 + 1)) ∖ I ) ∧ ∀𝑗 ∈ (0..^(𝐼 + 1)) ¬ 𝐴 ∈ dom ((𝑤‘𝑗) ∖ I )))))
258	257	rexlimdvva 3189	. 2 ⊢ (𝜑 → (∃𝑟 ∈ 𝑇 ∃𝑠 ∈ 𝑇 (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )) → ∃𝑤 ∈ Word 𝑇(((𝐺 Σg 𝑤) = ( I ↾ 𝐷) ∧ (♯‘𝑤) = 𝐿) ∧ ((𝐼 + 1) ∈ (0..^𝐿) ∧ 𝐴 ∈ dom ((𝑤‘(𝐼 + 1)) ∖ I ) ∧ ∀𝑗 ∈ (0..^(𝐼 + 1)) ¬ 𝐴 ∈ dom ((𝑤‘𝑗) ∖ I )))))
259	20, 21, 86, 88, 24	psgnunilem1 19400	. 2 ⊢ (𝜑 → (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷) ∨ ∃𝑟 ∈ 𝑇 ∃𝑠 ∈ 𝑇 (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I ))))
260	117, 258, 259	mpjaod 860	1 ⊢ (𝜑 → ∃𝑤 ∈ Word 𝑇(((𝐺 Σg 𝑤) = ( I ↾ 𝐷) ∧ (♯‘𝑤) = 𝐿) ∧ ((𝐼 + 1) ∈ (0..^𝐿) ∧ 𝐴 ∈ dom ((𝑤‘(𝐼 + 1)) ∖ I ) ∧ ∀𝑗 ∈ (0..^(𝐼 + 1)) ¬ 𝐴 ∈ dom ((𝑤‘𝑗) ∖ I ))))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 847   ∧ w3a 1086   = wceq 1541   ∈ wcel 2111  ∀wral 3047  ∃wrex 3056   ∖ cdif 3894   ⊆ wss 3897  ∅c0 4278  ⟨cop 4577  ⟨cotp 4579   class class class wbr 5086   I cid 5505  dom cdm 5611  ran crn 5612   ↾ cres 5613   ∘ ccom 5615  ⟶wf 6472  ‘cfv 6476  (class class class)co 7341  ℂcc 10999  ℝcr 11000  0cc0 11001  1c1 11002   + caddc 11004   < clt 11141   ≤ cle 11142   − cmin 11339  -cneg 11340  ℕcn 12120  2c2 12175  ℕ₀cn0 12376  ℤcz 12463  ℤ_≥cuz 12727  ...cfz 13402  ..^cfzo 13549  ♯chash 14232  Word cword 14415   substr csubstr 14543   splice csplice 14651  ⟨“cs2 14743  Basecbs 17115  +_gcplusg 17156  0_gc0g 17338   Σ_g cgsu 17339  Mndcmnd 18637  Grpcgrp 18841  SymGrpcsymg 19276  pmTrspcpmtr 19348

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-rep 5212  ax-sep 5229  ax-nul 5239  ax-pow 5298  ax-pr 5365  ax-un 7663  ax-cnex 11057  ax-resscn 11058  ax-1cn 11059  ax-icn 11060  ax-addcl 11061  ax-addrcl 11062  ax-mulcl 11063  ax-mulrcl 11064  ax-mulcom 11065  ax-addass 11066  ax-mulass 11067  ax-distr 11068  ax-i2m1 11069  ax-1ne0 11070  ax-1rid 11071  ax-rnegex 11072  ax-rrecex 11073  ax-cnre 11074  ax-pre-lttri 11075  ax-pre-lttrn 11076  ax-pre-ltadd 11077  ax-pre-mulgt0 11078

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-xor 1513  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-nel 3033  df-ral 3048  df-rex 3057  df-rmo 3346  df-reu 3347  df-rab 3396  df-v 3438  df-sbc 3737  df-csb 3846  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-pss 3917  df-nul 4279  df-if 4471  df-pw 4547  df-sn 4572  df-pr 4574  df-tp 4576  df-op 4578  df-ot 4580  df-uni 4855  df-int 4893  df-iun 4938  df-br 5087  df-opab 5149  df-mpt 5168  df-tr 5194  df-id 5506  df-eprel 5511  df-po 5519  df-so 5520  df-fr 5564  df-we 5566  df-xp 5617  df-rel 5618  df-cnv 5619  df-co 5620  df-dm 5621  df-rn 5622  df-res 5623  df-ima 5624  df-pred 6243  df-ord 6304  df-on 6305  df-lim 6306  df-suc 6307  df-iota 6432  df-fun 6478  df-fn 6479  df-f 6480  df-f1 6481  df-fo 6482  df-f1o 6483  df-fv 6484  df-riota 7298  df-ov 7344  df-oprab 7345  df-mpo 7346  df-om 7792  df-1st 7916  df-2nd 7917  df-frecs 8206  df-wrecs 8237  df-recs 8286  df-rdg 8324  df-1o 8380  df-2o 8381  df-er 8617  df-map 8747  df-en 8865  df-dom 8866  df-sdom 8867  df-fin 8868  df-card 9827  df-pnf 11143  df-mnf 11144  df-xr 11145  df-ltxr 11146  df-le 11147  df-sub 11341  df-neg 11342  df-nn 12121  df-2 12183  df-3 12184  df-4 12185  df-5 12186  df-6 12187  df-7 12188  df-8 12189  df-9 12190  df-n0 12377  df-xnn0 12450  df-z 12464  df-uz 12728  df-fz 13403  df-fzo 13550  df-seq 13904  df-hash 14233  df-word 14416  df-lsw 14465  df-concat 14473  df-s1 14499  df-substr 14544  df-pfx 14574  df-splice 14652  df-s2 14750  df-struct 17053  df-sets 17070  df-slot 17088  df-ndx 17100  df-base 17116  df-ress 17137  df-plusg 17169  df-tset 17175  df-0g 17340  df-gsum 17341  df-mgm 18543  df-sgrp 18622  df-mnd 18638  df-submnd 18687  df-efmnd 18772  df-grp 18844  df-minusg 18845  df-subg 19031  df-symg 19277  df-pmtr 19349

This theorem is referenced by:  psgnunilem3  19403