Theorem psgnunilem2 19513

Description: Lemma for psgnuni 19517. 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 14577	. . . . . . 7 ⊢ ∅ ∈ Word 𝑇
3		splcl 14790	. . . . . . 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 13718	. . . . . . . . . . 11 ⊢ (0..^𝐿) ⊆ (0...𝐿)
7		psgnunilem2.ix	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐼 ∈ (0..^𝐿))
8	6, 7	sselid 3981	. . . . . . . . . 10 ⊢ (𝜑 → 𝐼 ∈ (0...𝐿))
9		elfznn0 13660	. . . . . . . . . 10 ⊢ (𝐼 ∈ (0...𝐿) → 𝐼 ∈ ℕ0)
10	8, 9	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝐼 ∈ ℕ0)
11		2nn0 12543	. . . . . . . . . 10 ⊢ 2 ∈ ℕ0
12		nn0addcl 12561	. . . . . . . . . 10 ⊢ ((𝐼 ∈ ℕ0 ∧ 2 ∈ ℕ0) → (𝐼 + 2) ∈ ℕ0)
13	10, 11, 12	sylancl 586	. . . . . . . . 9 ⊢ (𝜑 → (𝐼 + 2) ∈ ℕ0)
14	10	nn0red 12588	. . . . . . . . . 10 ⊢ (𝜑 → 𝐼 ∈ ℝ)
15		nn0addge1 12572	. . . . . . . . . 10 ⊢ ((𝐼 ∈ ℝ ∧ 2 ∈ ℕ0) → 𝐼 ≤ (𝐼 + 2))
16	14, 11, 15	sylancl 586	. . . . . . . . 9 ⊢ (𝜑 → 𝐼 ≤ (𝐼 + 2))
17		elfz2nn0 13658	. . . . . . . . 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 19512	. . . . . . . . . 10 ⊢ (𝜑 → (𝐼 + 1) ∈ (0..^𝐿))
27		fzofzp1 13803	. . . . . . . . . 10 ⊢ ((𝐼 + 1) ∈ (0..^𝐿) → ((𝐼 + 1) + 1) ∈ (0...𝐿))
28	26, 27	syl 17	. . . . . . . . 9 ⊢ (𝜑 → ((𝐼 + 1) + 1) ∈ (0...𝐿))
29		df-2 12329	. . . . . . . . . . 11 ⊢ 2 = (1 + 1)
30	29	oveq2i 7442	. . . . . . . . . 10 ⊢ (𝐼 + 2) = (𝐼 + (1 + 1))
31	10	nn0cnd 12589	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐼 ∈ ℂ)
32		1cnd 11256	. . . . . . . . . . 11 ⊢ (𝜑 → 1 ∈ ℂ)
33	31, 32, 32	addassd 11283	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐼 + 1) + 1) = (𝐼 + (1 + 1)))
34	30, 33	eqtr4id 2796	. . . . . . . . 9 ⊢ (𝜑 → (𝐼 + 2) = ((𝐼 + 1) + 1))
35	23	oveq2d 7447	. . . . . . . . 9 ⊢ (𝜑 → (0...(♯‘𝑊)) = (0...𝐿))
36	28, 34, 35	3eltr4d 2856	. . . . . . . 8 ⊢ (𝜑 → (𝐼 + 2) ∈ (0...(♯‘𝑊)))
37	2	a1i 11	. . . . . . . 8 ⊢ (𝜑 → ∅ ∈ Word 𝑇)
38	1, 18, 36, 37	spllen 14792	. . . . . . 7 ⊢ (𝜑 → (♯‘(𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩)) = ((♯‘𝑊) + ((♯‘∅) − ((𝐼 + 2) − 𝐼))))
39		hash0 14406	. . . . . . . . . . 11 ⊢ (♯‘∅) = 0
40	39	oveq1i 7441	. . . . . . . . . 10 ⊢ ((♯‘∅) − ((𝐼 + 2) − 𝐼)) = (0 − ((𝐼 + 2) − 𝐼))
41		df-neg 11495	. . . . . . . . . 10 ⊢ -((𝐼 + 2) − 𝐼) = (0 − ((𝐼 + 2) − 𝐼))
42	40, 41	eqtr4i 2768	. . . . . . . . 9 ⊢ ((♯‘∅) − ((𝐼 + 2) − 𝐼)) = -((𝐼 + 2) − 𝐼)
43		2cn 12341	. . . . . . . . . . 11 ⊢ 2 ∈ ℂ
44		pncan2 11515	. . . . . . . . . . 11 ⊢ ((𝐼 ∈ ℂ ∧ 2 ∈ ℂ) → ((𝐼 + 2) − 𝐼) = 2)
45	31, 43, 44	sylancl 586	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐼 + 2) − 𝐼) = 2)
46	45	negeqd 11502	. . . . . . . . 9 ⊢ (𝜑 → -((𝐼 + 2) − 𝐼) = -2)
47	42, 46	eqtrid 2789	. . . . . . . 8 ⊢ (𝜑 → ((♯‘∅) − ((𝐼 + 2) − 𝐼)) = -2)
48	23, 47	oveq12d 7449	. . . . . . 7 ⊢ (𝜑 → ((♯‘𝑊) + ((♯‘∅) − ((𝐼 + 2) − 𝐼))) = (𝐿 + -2))
49		elfzel2 13562	. . . . . . . . . 10 ⊢ (𝐼 ∈ (0...𝐿) → 𝐿 ∈ ℤ)
50	8, 49	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝐿 ∈ ℤ)
51	50	zcnd 12723	. . . . . . . 8 ⊢ (𝜑 → 𝐿 ∈ ℂ)
52		negsub 11557	. . . . . . . 8 ⊢ ((𝐿 ∈ ℂ ∧ 2 ∈ ℂ) → (𝐿 + -2) = (𝐿 − 2))
53	51, 43, 52	sylancl 586	. . . . . . 7 ⊢ (𝜑 → (𝐿 + -2) = (𝐿 − 2))
54	38, 48, 53	3eqtrd 2781	. . . . . 6 ⊢ (𝜑 → (♯‘(𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩)) = (𝐿 − 2))
55	54	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ ((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷)) → (♯‘(𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩)) = (𝐿 − 2))
56		splid 14791	. . . . . . . . 9 ⊢ ((𝑊 ∈ Word 𝑇 ∧ (𝐼 ∈ (0...(𝐼 + 2)) ∧ (𝐼 + 2) ∈ (0...(♯‘𝑊)))) → (𝑊 splice ⟨𝐼, (𝐼 + 2), (𝑊 substr ⟨𝐼, (𝐼 + 2)⟩)⟩) = 𝑊)
57	1, 18, 36, 56	syl12anc 837	. . . . . . . 8 ⊢ (𝜑 → (𝑊 splice ⟨𝐼, (𝐼 + 2), (𝑊 substr ⟨𝐼, (𝐼 + 2)⟩)⟩) = 𝑊)
58	57	oveq2d 7447	. . . . . . 7 ⊢ (𝜑 → (𝐺 Σg (𝑊 splice ⟨𝐼, (𝐼 + 2), (𝑊 substr ⟨𝐼, (𝐼 + 2)⟩)⟩)) = (𝐺 Σg 𝑊))
59	58	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷)) → (𝐺 Σg (𝑊 splice ⟨𝐼, (𝐼 + 2), (𝑊 substr ⟨𝐼, (𝐼 + 2)⟩)⟩)) = (𝐺 Σg 𝑊))
60		eqid 2737	. . . . . . 7 ⊢ (Base‘𝐺) = (Base‘𝐺)
61	19	symggrp 19418	. . . . . . . . . 10 ⊢ (𝐷 ∈ 𝑉 → 𝐺 ∈ Grp)
62	21, 61	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝐺 ∈ Grp)
63	62	grpmndd 18964	. . . . . . . 8 ⊢ (𝜑 → 𝐺 ∈ Mnd)
64	63	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷)) → 𝐺 ∈ Mnd)
65	20, 19, 60	symgtrf 19487	. . . . . . . . . 10 ⊢ 𝑇 ⊆ (Base‘𝐺)
66		sswrd 14560	. . . . . . . . . 10 ⊢ (𝑇 ⊆ (Base‘𝐺) → Word 𝑇 ⊆ Word (Base‘𝐺))
67	65, 66	ax-mp 5	. . . . . . . . 9 ⊢ Word 𝑇 ⊆ Word (Base‘𝐺)
68	67, 1	sselid 3981	. . . . . . . 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 14683	. . . . . . . . 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 14577	. . . . . . . 8 ⊢ ∅ ∈ Word (Base‘𝐺)
76	75	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷)) → ∅ ∈ Word (Base‘𝐺))
77	23	oveq2d 7447	. . . . . . . . . . . . 13 ⊢ (𝜑 → (0..^(♯‘𝑊)) = (0..^𝐿))
78	26, 77	eleqtrrd 2844	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐼 + 1) ∈ (0..^(♯‘𝑊)))
79		swrds2 14979	. . . . . . . . . . . 12 ⊢ ((𝑊 ∈ Word 𝑇 ∧ 𝐼 ∈ ℕ0 ∧ (𝐼 + 1) ∈ (0..^(♯‘𝑊))) → (𝑊 substr ⟨𝐼, (𝐼 + 2)⟩) = ⟨“(𝑊‘𝐼)(𝑊‘(𝐼 + 1))”⟩)
80	1, 10, 78, 79	syl3anc 1373	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑊 substr ⟨𝐼, (𝐼 + 2)⟩) = ⟨“(𝑊‘𝐼)(𝑊‘(𝐼 + 1))”⟩)
81	80	oveq2d 7447	. . . . . . . . . 10 ⊢ (𝜑 → (𝐺 Σg (𝑊 substr ⟨𝐼, (𝐼 + 2)⟩)) = (𝐺 Σg ⟨“(𝑊‘𝐼)(𝑊‘(𝐼 + 1))”⟩))
82		wrdf 14557	. . . . . . . . . . . . . . 15 ⊢ (𝑊 ∈ Word 𝑇 → 𝑊:(0..^(♯‘𝑊))⟶𝑇)
83	1, 82	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑊:(0..^(♯‘𝑊))⟶𝑇)
84	77	feq2d 6722	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑊:(0..^(♯‘𝑊))⟶𝑇 ↔ 𝑊:(0..^𝐿)⟶𝑇))
85	83, 84	mpbid 232	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑊:(0..^𝐿)⟶𝑇)
86	85, 7	ffvelcdmd 7105	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑊‘𝐼) ∈ 𝑇)
87	65, 86	sselid 3981	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑊‘𝐼) ∈ (Base‘𝐺))
88	85, 26	ffvelcdmd 7105	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑊‘(𝐼 + 1)) ∈ 𝑇)
89	65, 88	sselid 3981	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑊‘(𝐼 + 1)) ∈ (Base‘𝐺))
90		eqid 2737	. . . . . . . . . . . 12 ⊢ (+g‘𝐺) = (+g‘𝐺)
91	60, 90	gsumws2 18855	. . . . . . . . . . 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 19401	. . . . . . . . . . 11 ⊢ (((𝑊‘𝐼) ∈ (Base‘𝐺) ∧ (𝑊‘(𝐼 + 1)) ∈ (Base‘𝐺)) → ((𝑊‘𝐼)(+g‘𝐺)(𝑊‘(𝐼 + 1))) = ((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))))
94	87, 89, 93	syl2anc 584	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑊‘𝐼)(+g‘𝐺)(𝑊‘(𝐼 + 1))) = ((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))))
95	81, 92, 94	3eqtrd 2781	. . . . . . . . 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 19419	. . . . . . . . . . 11 ⊢ (𝐷 ∈ 𝑉 → ( I ↾ 𝐷) = (0g‘𝐺))
99	21, 98	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → ( I ↾ 𝐷) = (0g‘𝐺))
100		eqid 2737	. . . . . . . . . . 11 ⊢ (0g‘𝐺) = (0g‘𝐺)
101	100	gsum0 18697	. . . . . . . . . 10 ⊢ (𝐺 Σg ∅) = (0g‘𝐺)
102	99, 101	eqtr4di 2795	. . . . . . . . 9 ⊢ (𝜑 → ( I ↾ 𝐷) = (𝐺 Σg ∅))
103	102	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷)) → ( I ↾ 𝐷) = (𝐺 Σg ∅))
104	96, 97, 103	3eqtrd 2781	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷)) → (𝐺 Σg (𝑊 substr ⟨𝐼, (𝐼 + 2)⟩)) = (𝐺 Σg ∅))
105	60, 64, 69, 70, 71, 74, 76, 104	gsumspl 18857	. . . . . 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 2785	. . . . 5 ⊢ ((𝜑 ∧ ((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷)) → (𝐺 Σg (𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩)) = ( I ↾ 𝐷))
108		fveqeq2 6915	. . . . . . 7 ⊢ (𝑥 = (𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩) → ((♯‘𝑥) = (𝐿 − 2) ↔ (♯‘(𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩)) = (𝐿 − 2)))
109		oveq2 7439	. . . . . . . 8 ⊢ (𝑥 = (𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩) → (𝐺 Σg 𝑥) = (𝐺 Σg (𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩)))
110	109	eqeq1d 2739	. . . . . . 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 3622	. . . . 5 ⊢ (((𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩) ∈ Word 𝑇 ∧ ((♯‘(𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩)) = (𝐿 − 2) ∧ (𝐺 Σg (𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩)) = ( I ↾ 𝐷))) → ∃𝑥 ∈ Word 𝑇((♯‘𝑥) = (𝐿 − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)))
113	5, 55, 107, 112	syl12anc 837	. . . 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 771	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → 𝑟 ∈ 𝑇)
120		simprr 773	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → 𝑠 ∈ 𝑇)
121	119, 120	s2cld 14910	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → ⟨“𝑟𝑠”⟩ ∈ Word 𝑇)
122		splcl 14790	. . . . . . 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 3981	. . . . . . . . 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 3983	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑟 ∈ 𝑇) → 𝑟 ∈ (Base‘𝐺))
137	136	adantrr 717	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → 𝑟 ∈ (Base‘𝐺))
138	135	sselda 3983	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝑇) → 𝑠 ∈ (Base‘𝐺))
139	138	adantrl 716	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → 𝑠 ∈ (Base‘𝐺))
140	60, 90	gsumws2 18855	. . . . . . . . . . . 12 ⊢ ((𝐺 ∈ Mnd ∧ 𝑟 ∈ (Base‘𝐺) ∧ 𝑠 ∈ (Base‘𝐺)) → (𝐺 Σg ⟨“𝑟𝑠”⟩) = (𝑟(+g‘𝐺)𝑠))
141	134, 137, 139, 140	syl3anc 1373	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → (𝐺 Σg ⟨“𝑟𝑠”⟩) = (𝑟(+g‘𝐺)𝑠))
142	19, 60, 90	symgov 19401	. . . . . . . . . . . 12 ⊢ ((𝑟 ∈ (Base‘𝐺) ∧ 𝑠 ∈ (Base‘𝐺)) → (𝑟(+g‘𝐺)𝑠) = (𝑟 ∘ 𝑠))
143	137, 139, 142	syl2anc 584	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → (𝑟(+g‘𝐺)𝑠) = (𝑟 ∘ 𝑠))
144	141, 143	eqtrd 2777	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → (𝐺 Σg ⟨“𝑟𝑠”⟩) = (𝑟 ∘ 𝑠))
145	144	adantrr 717	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → (𝐺 Σg ⟨“𝑟𝑠”⟩) = (𝑟 ∘ 𝑠))
146	132, 133, 145	3eqtr4rd 2788	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → (𝐺 Σg ⟨“𝑟𝑠”⟩) = (𝐺 Σg (𝑊 substr ⟨𝐼, (𝐼 + 2)⟩)))
147	60, 125, 126, 127, 128, 130, 131, 146	gsumspl 18857	. . . . . . 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 2781	. . . . . 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 14792	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → (♯‘(𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)) = ((♯‘𝑊) + ((♯‘⟨“𝑟𝑠”⟩) − ((𝐼 + 2) − 𝐼))))
154		s2len 14928	. . . . . . . . . . . . 13 ⊢ (♯‘⟨“𝑟𝑠”⟩) = 2
155	154	oveq1i 7441	. . . . . . . . . . . 12 ⊢ ((♯‘⟨“𝑟𝑠”⟩) − ((𝐼 + 2) − 𝐼)) = (2 − ((𝐼 + 2) − 𝐼))
156	45	oveq2d 7447	. . . . . . . . . . . . 13 ⊢ (𝜑 → (2 − ((𝐼 + 2) − 𝐼)) = (2 − 2))
157	43	subidi 11580	. . . . . . . . . . . . 13 ⊢ (2 − 2) = 0
158	156, 157	eqtrdi 2793	. . . . . . . . . . . 12 ⊢ (𝜑 → (2 − ((𝐼 + 2) − 𝐼)) = 0)
159	155, 158	eqtrid 2789	. . . . . . . . . . 11 ⊢ (𝜑 → ((♯‘⟨“𝑟𝑠”⟩) − ((𝐼 + 2) − 𝐼)) = 0)
160	159	oveq2d 7447	. . . . . . . . . 10 ⊢ (𝜑 → ((♯‘𝑊) + ((♯‘⟨“𝑟𝑠”⟩) − ((𝐼 + 2) − 𝐼))) = ((♯‘𝑊) + 0))
161	23, 51	eqeltrd 2841	. . . . . . . . . . 11 ⊢ (𝜑 → (♯‘𝑊) ∈ ℂ)
162	161	addridd 11461	. . . . . . . . . 10 ⊢ (𝜑 → ((♯‘𝑊) + 0) = (♯‘𝑊))
163	160, 162, 23	3eqtrd 2781	. . . . . . . . 9 ⊢ (𝜑 → ((♯‘𝑊) + ((♯‘⟨“𝑟𝑠”⟩) − ((𝐼 + 2) − 𝐼))) = 𝐿)
164	163	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → ((♯‘𝑊) + ((♯‘⟨“𝑟𝑠”⟩) − ((𝐼 + 2) − 𝐼))) = 𝐿)
165	153, 164	eqtrd 2777	. . . . . . 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 12542	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ ℕ0
171		2nn 12339	. . . . . . . . . . . . . . 15 ⊢ 2 ∈ ℕ
172		1lt2 12437	. . . . . . . . . . . . . . 15 ⊢ 1 < 2
173		elfzo0 13740	. . . . . . . . . . . . . . 15 ⊢ (1 ∈ (0..^2) ↔ (1 ∈ ℕ0 ∧ 2 ∈ ℕ ∧ 1 < 2))
174	170, 171, 172, 173	mpbir3an 1342	. . . . . . . . . . . . . 14 ⊢ 1 ∈ (0..^2)
175	154	oveq2i 7442	. . . . . . . . . . . . . 14 ⊢ (0..^(♯‘⟨“𝑟𝑠”⟩)) = (0..^2)
176	174, 175	eleqtrri 2840	. . . . . . . . . . . . 13 ⊢ 1 ∈ (0..^(♯‘⟨“𝑟𝑠”⟩))
177	176	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → 1 ∈ (0..^(♯‘⟨“𝑟𝑠”⟩)))
178	118, 151, 152, 121, 177	splfv2a 14794	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → ((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘(𝐼 + 1)) = (⟨“𝑟𝑠”⟩‘1))
179		s2fv1 14927	. . . . . . . . . . . 12 ⊢ (𝑠 ∈ 𝑇 → (⟨“𝑟𝑠”⟩‘1) = 𝑠)
180	179	ad2antll 729	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → (⟨“𝑟𝑠”⟩‘1) = 𝑠)
181	178, 180	eqtrd 2777	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → ((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘(𝐼 + 1)) = 𝑠)
182	181	adantrr 717	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → ((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘(𝐼 + 1)) = 𝑠)
183	182	difeq1d 4125	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘(𝐼 + 1)) ∖ I ) = (𝑠 ∖ I ))
184	183	dmeqd 5916	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘(𝐼 + 1)) ∖ I ) = dom (𝑠 ∖ I ))
185	169, 184	eleqtrrd 2844	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → 𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘(𝐼 + 1)) ∖ I ))
186		fzosplitsni 13817	. . . . . . . . . . 11 ⊢ (𝐼 ∈ (ℤ≥‘0) → (𝑗 ∈ (0..^(𝐼 + 1)) ↔ (𝑗 ∈ (0..^𝐼) ∨ 𝑗 = 𝐼)))
187		nn0uz 12920	. . . . . . . . . . 11 ⊢ ℕ0 = (ℤ≥‘0)
188	186, 187	eleq2s 2859	. . . . . . . . . 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 6906	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 𝑗 → (𝑊‘𝑘) = (𝑊‘𝑗))
192	191	difeq1d 4125	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 𝑗 → ((𝑊‘𝑘) ∖ I ) = ((𝑊‘𝑗) ∖ I ))
193	192	dmeqd 5916	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 𝑗 → dom ((𝑊‘𝑘) ∖ I ) = dom ((𝑊‘𝑗) ∖ I ))
194	193	eleq2d 2827	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 𝑗 → (𝐴 ∈ dom ((𝑊‘𝑘) ∖ I ) ↔ 𝐴 ∈ dom ((𝑊‘𝑗) ∖ I )))
195	194	notbid 318	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑗 → (¬ 𝐴 ∈ dom ((𝑊‘𝑘) ∖ I ) ↔ ¬ 𝐴 ∈ dom ((𝑊‘𝑗) ∖ I )))
196	195	rspccva 3621	. . . . . . . . . . . . . 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 14793	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) ∧ 𝑗 ∈ (0..^𝐼)) → ((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) = (𝑊‘𝑗))
205	204	difeq1d 4125	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) ∧ 𝑗 ∈ (0..^𝐼)) → (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) ∖ I ) = ((𝑊‘𝑗) ∖ I ))
206	205	dmeqd 5916	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) ∧ 𝑗 ∈ (0..^𝐼)) → dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) ∖ I ) = dom ((𝑊‘𝑗) ∖ I ))
207	198, 206	neleqtrrd 2864	. . . . . . . . . . 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 12541	. . . . . . . . . . . . . . . . . . . 20 ⊢ 0 ∈ ℕ0
212		2pos 12369	. . . . . . . . . . . . . . . . . . . 20 ⊢ 0 < 2
213		elfzo0 13740	. . . . . . . . . . . . . . . . . . . 20 ⊢ (0 ∈ (0..^2) ↔ (0 ∈ ℕ0 ∧ 2 ∈ ℕ ∧ 0 < 2))
214	211, 171, 212, 213	mpbir3an 1342	. . . . . . . . . . . . . . . . . . 19 ⊢ 0 ∈ (0..^2)
215	214, 175	eleqtrri 2840	. . . . . . . . . . . . . . . . . 18 ⊢ 0 ∈ (0..^(♯‘⟨“𝑟𝑠”⟩))
216	215	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → 0 ∈ (0..^(♯‘⟨“𝑟𝑠”⟩)))
217	118, 151, 152, 121, 216	splfv2a 14794	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → ((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘(𝐼 + 0)) = (⟨“𝑟𝑠”⟩‘0))
218	31	addridd 11461	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐼 + 0) = 𝐼)
219	218	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → (𝐼 + 0) = 𝐼)
220	219	fveq2d 6910	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → ((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘(𝐼 + 0)) = ((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝐼))
221		s2fv0 14926	. . . . . . . . . . . . . . . . 17 ⊢ (𝑟 ∈ 𝑇 → (⟨“𝑟𝑠”⟩‘0) = 𝑟)
222	221	ad2antrl 728	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → (⟨“𝑟𝑠”⟩‘0) = 𝑟)
223	217, 220, 222	3eqtr3d 2785	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → ((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝐼) = 𝑟)
224	223	difeq1d 4125	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝐼) ∖ I ) = (𝑟 ∖ I ))
225	224	dmeqd 5916	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝐼) ∖ I ) = dom (𝑟 ∖ I ))
226	225	eleq2d 2827	. . . . . . . . . . . 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 6906	. . . . . . . . . . . . . 14 ⊢ (𝑗 = 𝐼 → ((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) = ((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝐼))
230	229	difeq1d 4125	. . . . . . . . . . . . 13 ⊢ (𝑗 = 𝐼 → (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) ∖ I ) = (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝐼) ∖ I ))
231	230	dmeqd 5916	. . . . . . . . . . . 12 ⊢ (𝑗 = 𝐼 → dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) ∖ I ) = dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝐼) ∖ I ))
232	231	eleq2d 2827	. . . . . . . . . . 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 860	. . . . . . . 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 3145	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → ∀𝑗 ∈ (0..^(𝐼 + 1)) ¬ 𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) ∖ I ))
238	168, 185, 237	3jca 1129	. . . . 5 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → ((𝐼 + 1) ∈ (0..^𝐿) ∧ 𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘(𝐼 + 1)) ∖ I ) ∧ ∀𝑗 ∈ (0..^(𝐼 + 1)) ¬ 𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) ∖ I )))
239		oveq2 7439	. . . . . . . . 9 ⊢ (𝑤 = (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩) → (𝐺 Σg 𝑤) = (𝐺 Σg (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)))
240	239	eqeq1d 2739	. . . . . . . 8 ⊢ (𝑤 = (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩) → ((𝐺 Σg 𝑤) = ( I ↾ 𝐷) ↔ (𝐺 Σg (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)) = ( I ↾ 𝐷)))
241		fveqeq2 6915	. . . . . . . 8 ⊢ (𝑤 = (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩) → ((♯‘𝑤) = 𝐿 ↔ (♯‘(𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)) = 𝐿))
242	240, 241	anbi12d 632	. . . . . . 7 ⊢ (𝑤 = (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩) → (((𝐺 Σg 𝑤) = ( I ↾ 𝐷) ∧ (♯‘𝑤) = 𝐿) ↔ ((𝐺 Σg (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)) = ( I ↾ 𝐷) ∧ (♯‘(𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)) = 𝐿)))
243		fveq1 6905	. . . . . . . . . . 11 ⊢ (𝑤 = (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩) → (𝑤‘(𝐼 + 1)) = ((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘(𝐼 + 1)))
244	243	difeq1d 4125	. . . . . . . . . 10 ⊢ (𝑤 = (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩) → ((𝑤‘(𝐼 + 1)) ∖ I ) = (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘(𝐼 + 1)) ∖ I ))
245	244	dmeqd 5916	. . . . . . . . 9 ⊢ (𝑤 = (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩) → dom ((𝑤‘(𝐼 + 1)) ∖ I ) = dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘(𝐼 + 1)) ∖ I ))
246	245	eleq2d 2827	. . . . . . . 8 ⊢ (𝑤 = (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩) → (𝐴 ∈ dom ((𝑤‘(𝐼 + 1)) ∖ I ) ↔ 𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘(𝐼 + 1)) ∖ I )))
247		fveq1 6905	. . . . . . . . . . . . 13 ⊢ (𝑤 = (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩) → (𝑤‘𝑗) = ((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗))
248	247	difeq1d 4125	. . . . . . . . . . . 12 ⊢ (𝑤 = (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩) → ((𝑤‘𝑗) ∖ I ) = (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) ∖ I ))
249	248	dmeqd 5916	. . . . . . . . . . 11 ⊢ (𝑤 = (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩) → dom ((𝑤‘𝑗) ∖ I ) = dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) ∖ I ))
250	249	eleq2d 2827	. . . . . . . . . 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 3178	. . . . . . . 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 3622	. . . . 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 837	. . . 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 3213	. 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 19511	. 2 ⊢ (𝜑 → (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷) ∨ ∃𝑟 ∈ 𝑇 ∃𝑠 ∈ 𝑇 (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I ))))
260	117, 258, 259	mpjaod 861	1 ⊢ (𝜑 → ∃𝑤 ∈ Word 𝑇(((𝐺 Σg 𝑤) = ( I ↾ 𝐷) ∧ (♯‘𝑤) = 𝐿) ∧ ((𝐼 + 1) ∈ (0..^𝐿) ∧ 𝐴 ∈ dom ((𝑤‘(𝐼 + 1)) ∖ I ) ∧ ∀𝑗 ∈ (0..^(𝐼 + 1)) ¬ 𝐴 ∈ dom ((𝑤‘𝑗) ∖ I ))))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 848   ∧ w3a 1087   = wceq 1540   ∈ wcel 2108  ∀wral 3061  ∃wrex 3070   ∖ cdif 3948   ⊆ wss 3951  ∅c0 4333  ⟨cop 4632  ⟨cotp 4634   class class class wbr 5143   I cid 5577  dom cdm 5685  ran crn 5686   ↾ cres 5687   ∘ ccom 5689  ⟶wf 6557  ‘cfv 6561  (class class class)co 7431  ℂcc 11153  ℝcr 11154  0cc0 11155  1c1 11156   + caddc 11158   < clt 11295   ≤ cle 11296   − cmin 11492  -cneg 11493  ℕcn 12266  2c2 12321  ℕ₀cn0 12526  ℤcz 12613  ℤ_≥cuz 12878  ...cfz 13547  ..^cfzo 13694  ♯chash 14369  Word cword 14552   substr csubstr 14678   splice csplice 14787  ⟨“cs2 14880  Basecbs 17247  +_gcplusg 17297  0_gc0g 17484   Σ_g cgsu 17485  Mndcmnd 18747  Grpcgrp 18951  SymGrpcsymg 19386  pmTrspcpmtr 19459

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-cnex 11211  ax-resscn 11212  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-addrcl 11216  ax-mulcl 11217  ax-mulrcl 11218  ax-mulcom 11219  ax-addass 11220  ax-mulass 11221  ax-distr 11222  ax-i2m1 11223  ax-1ne0 11224  ax-1rid 11225  ax-rnegex 11226  ax-rrecex 11227  ax-cnre 11228  ax-pre-lttri 11229  ax-pre-lttrn 11230  ax-pre-ltadd 11231  ax-pre-mulgt0 11232

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-xor 1512  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3380  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-tp 4631  df-op 4633  df-ot 4635  df-uni 4908  df-int 4947  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-om 7888  df-1st 8014  df-2nd 8015  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-1o 8506  df-2o 8507  df-er 8745  df-map 8868  df-en 8986  df-dom 8987  df-sdom 8988  df-fin 8989  df-card 9979  df-pnf 11297  df-mnf 11298  df-xr 11299  df-ltxr 11300  df-le 11301  df-sub 11494  df-neg 11495  df-nn 12267  df-2 12329  df-3 12330  df-4 12331  df-5 12332  df-6 12333  df-7 12334  df-8 12335  df-9 12336  df-n0 12527  df-xnn0 12600  df-z 12614  df-uz 12879  df-fz 13548  df-fzo 13695  df-seq 14043  df-hash 14370  df-word 14553  df-lsw 14601  df-concat 14609  df-s1 14634  df-substr 14679  df-pfx 14709  df-splice 14788  df-s2 14887  df-struct 17184  df-sets 17201  df-slot 17219  df-ndx 17231  df-base 17248  df-ress 17275  df-plusg 17310  df-tset 17316  df-0g 17486  df-gsum 17487  df-mgm 18653  df-sgrp 18732  df-mnd 18748  df-submnd 18797  df-efmnd 18882  df-grp 18954  df-minusg 18955  df-subg 19141  df-symg 19387  df-pmtr 19460

This theorem is referenced by:  psgnunilem3  19514