Theorem psgnunilem2 18615

Description: Lemma for psgnuni 18619. 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 13882	. . . . . . 7 ⊢ ∅ ∈ Word 𝑇
3		splcl 14105	. . . . . . 7 ⊢ ((𝑊 ∈ Word 𝑇 ∧ ∅ ∈ Word 𝑇) → (𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩) ∈ Word 𝑇)
4	1, 2, 3	sylancl 589	. . . . . 6 ⊢ (𝜑 → (𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩) ∈ Word 𝑇)
5	4	adantr 484	. . . . 5 ⊢ ((𝜑 ∧ ((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷)) → (𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩) ∈ Word 𝑇)
6		fzossfz 13051	. . . . . . . . . . 11 ⊢ (0..^𝐿) ⊆ (0...𝐿)
7		psgnunilem2.ix	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐼 ∈ (0..^𝐿))
8	6, 7	sseldi 3913	. . . . . . . . . 10 ⊢ (𝜑 → 𝐼 ∈ (0...𝐿))
9		elfznn0 12995	. . . . . . . . . 10 ⊢ (𝐼 ∈ (0...𝐿) → 𝐼 ∈ ℕ0)
10	8, 9	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝐼 ∈ ℕ0)
11		2nn0 11902	. . . . . . . . . 10 ⊢ 2 ∈ ℕ0
12		nn0addcl 11920	. . . . . . . . . 10 ⊢ ((𝐼 ∈ ℕ0 ∧ 2 ∈ ℕ0) → (𝐼 + 2) ∈ ℕ0)
13	10, 11, 12	sylancl 589	. . . . . . . . 9 ⊢ (𝜑 → (𝐼 + 2) ∈ ℕ0)
14	10	nn0red 11944	. . . . . . . . . 10 ⊢ (𝜑 → 𝐼 ∈ ℝ)
15		nn0addge1 11931	. . . . . . . . . 10 ⊢ ((𝐼 ∈ ℝ ∧ 2 ∈ ℕ0) → 𝐼 ≤ (𝐼 + 2))
16	14, 11, 15	sylancl 589	. . . . . . . . 9 ⊢ (𝜑 → 𝐼 ≤ (𝐼 + 2))
17		elfz2nn0 12993	. . . . . . . . 9 ⊢ (𝐼 ∈ (0...(𝐼 + 2)) ↔ (𝐼 ∈ ℕ0 ∧ (𝐼 + 2) ∈ ℕ0 ∧ 𝐼 ≤ (𝐼 + 2)))
18	10, 13, 16, 17	syl3anbrc 1340	. . . . . . . 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 18614	. . . . . . . . . 10 ⊢ (𝜑 → (𝐼 + 1) ∈ (0..^𝐿))
27		fzofzp1 13129	. . . . . . . . . 10 ⊢ ((𝐼 + 1) ∈ (0..^𝐿) → ((𝐼 + 1) + 1) ∈ (0...𝐿))
28	26, 27	syl 17	. . . . . . . . 9 ⊢ (𝜑 → ((𝐼 + 1) + 1) ∈ (0...𝐿))
29		df-2 11688	. . . . . . . . . . 11 ⊢ 2 = (1 + 1)
30	29	oveq2i 7146	. . . . . . . . . 10 ⊢ (𝐼 + 2) = (𝐼 + (1 + 1))
31	10	nn0cnd 11945	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐼 ∈ ℂ)
32		1cnd 10625	. . . . . . . . . . 11 ⊢ (𝜑 → 1 ∈ ℂ)
33	31, 32, 32	addassd 10652	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐼 + 1) + 1) = (𝐼 + (1 + 1)))
34	30, 33	eqtr4id 2852	. . . . . . . . 9 ⊢ (𝜑 → (𝐼 + 2) = ((𝐼 + 1) + 1))
35	23	oveq2d 7151	. . . . . . . . 9 ⊢ (𝜑 → (0...(♯‘𝑊)) = (0...𝐿))
36	28, 34, 35	3eltr4d 2905	. . . . . . . 8 ⊢ (𝜑 → (𝐼 + 2) ∈ (0...(♯‘𝑊)))
37	2	a1i 11	. . . . . . . 8 ⊢ (𝜑 → ∅ ∈ Word 𝑇)
38	1, 18, 36, 37	spllen 14107	. . . . . . 7 ⊢ (𝜑 → (♯‘(𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩)) = ((♯‘𝑊) + ((♯‘∅) − ((𝐼 + 2) − 𝐼))))
39		hash0 13724	. . . . . . . . . . 11 ⊢ (♯‘∅) = 0
40	39	oveq1i 7145	. . . . . . . . . 10 ⊢ ((♯‘∅) − ((𝐼 + 2) − 𝐼)) = (0 − ((𝐼 + 2) − 𝐼))
41		df-neg 10862	. . . . . . . . . 10 ⊢ -((𝐼 + 2) − 𝐼) = (0 − ((𝐼 + 2) − 𝐼))
42	40, 41	eqtr4i 2824	. . . . . . . . 9 ⊢ ((♯‘∅) − ((𝐼 + 2) − 𝐼)) = -((𝐼 + 2) − 𝐼)
43		2cn 11700	. . . . . . . . . . 11 ⊢ 2 ∈ ℂ
44		pncan2 10882	. . . . . . . . . . 11 ⊢ ((𝐼 ∈ ℂ ∧ 2 ∈ ℂ) → ((𝐼 + 2) − 𝐼) = 2)
45	31, 43, 44	sylancl 589	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐼 + 2) − 𝐼) = 2)
46	45	negeqd 10869	. . . . . . . . 9 ⊢ (𝜑 → -((𝐼 + 2) − 𝐼) = -2)
47	42, 46	syl5eq 2845	. . . . . . . 8 ⊢ (𝜑 → ((♯‘∅) − ((𝐼 + 2) − 𝐼)) = -2)
48	23, 47	oveq12d 7153	. . . . . . 7 ⊢ (𝜑 → ((♯‘𝑊) + ((♯‘∅) − ((𝐼 + 2) − 𝐼))) = (𝐿 + -2))
49		elfzel2 12900	. . . . . . . . . 10 ⊢ (𝐼 ∈ (0...𝐿) → 𝐿 ∈ ℤ)
50	8, 49	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝐿 ∈ ℤ)
51	50	zcnd 12076	. . . . . . . 8 ⊢ (𝜑 → 𝐿 ∈ ℂ)
52		negsub 10923	. . . . . . . 8 ⊢ ((𝐿 ∈ ℂ ∧ 2 ∈ ℂ) → (𝐿 + -2) = (𝐿 − 2))
53	51, 43, 52	sylancl 589	. . . . . . 7 ⊢ (𝜑 → (𝐿 + -2) = (𝐿 − 2))
54	38, 48, 53	3eqtrd 2837	. . . . . 6 ⊢ (𝜑 → (♯‘(𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩)) = (𝐿 − 2))
55	54	adantr 484	. . . . 5 ⊢ ((𝜑 ∧ ((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷)) → (♯‘(𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩)) = (𝐿 − 2))
56		splid 14106	. . . . . . . . 9 ⊢ ((𝑊 ∈ Word 𝑇 ∧ (𝐼 ∈ (0...(𝐼 + 2)) ∧ (𝐼 + 2) ∈ (0...(♯‘𝑊)))) → (𝑊 splice ⟨𝐼, (𝐼 + 2), (𝑊 substr ⟨𝐼, (𝐼 + 2)⟩)⟩) = 𝑊)
57	1, 18, 36, 56	syl12anc 835	. . . . . . . 8 ⊢ (𝜑 → (𝑊 splice ⟨𝐼, (𝐼 + 2), (𝑊 substr ⟨𝐼, (𝐼 + 2)⟩)⟩) = 𝑊)
58	57	oveq2d 7151	. . . . . . 7 ⊢ (𝜑 → (𝐺 Σg (𝑊 splice ⟨𝐼, (𝐼 + 2), (𝑊 substr ⟨𝐼, (𝐼 + 2)⟩)⟩)) = (𝐺 Σg 𝑊))
59	58	adantr 484	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷)) → (𝐺 Σg (𝑊 splice ⟨𝐼, (𝐼 + 2), (𝑊 substr ⟨𝐼, (𝐼 + 2)⟩)⟩)) = (𝐺 Σg 𝑊))
60		eqid 2798	. . . . . . 7 ⊢ (Base‘𝐺) = (Base‘𝐺)
61	19	symggrp 18520	. . . . . . . . . 10 ⊢ (𝐷 ∈ 𝑉 → 𝐺 ∈ Grp)
62	21, 61	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝐺 ∈ Grp)
63		grpmnd 18102	. . . . . . . . 9 ⊢ (𝐺 ∈ Grp → 𝐺 ∈ Mnd)
64	62, 63	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝐺 ∈ Mnd)
65	64	adantr 484	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷)) → 𝐺 ∈ Mnd)
66	20, 19, 60	symgtrf 18589	. . . . . . . . . 10 ⊢ 𝑇 ⊆ (Base‘𝐺)
67		sswrd 13865	. . . . . . . . . 10 ⊢ (𝑇 ⊆ (Base‘𝐺) → Word 𝑇 ⊆ Word (Base‘𝐺))
68	66, 67	ax-mp 5	. . . . . . . . 9 ⊢ Word 𝑇 ⊆ Word (Base‘𝐺)
69	68, 1	sseldi 3913	. . . . . . . 8 ⊢ (𝜑 → 𝑊 ∈ Word (Base‘𝐺))
70	69	adantr 484	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷)) → 𝑊 ∈ Word (Base‘𝐺))
71	18	adantr 484	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷)) → 𝐼 ∈ (0...(𝐼 + 2)))
72	36	adantr 484	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷)) → (𝐼 + 2) ∈ (0...(♯‘𝑊)))
73		swrdcl 13998	. . . . . . . . 9 ⊢ (𝑊 ∈ Word (Base‘𝐺) → (𝑊 substr ⟨𝐼, (𝐼 + 2)⟩) ∈ Word (Base‘𝐺))
74	69, 73	syl 17	. . . . . . . 8 ⊢ (𝜑 → (𝑊 substr ⟨𝐼, (𝐼 + 2)⟩) ∈ Word (Base‘𝐺))
75	74	adantr 484	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷)) → (𝑊 substr ⟨𝐼, (𝐼 + 2)⟩) ∈ Word (Base‘𝐺))
76		wrd0 13882	. . . . . . . 8 ⊢ ∅ ∈ Word (Base‘𝐺)
77	76	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷)) → ∅ ∈ Word (Base‘𝐺))
78	23	oveq2d 7151	. . . . . . . . . . . . 13 ⊢ (𝜑 → (0..^(♯‘𝑊)) = (0..^𝐿))
79	26, 78	eleqtrrd 2893	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐼 + 1) ∈ (0..^(♯‘𝑊)))
80		swrds2 14293	. . . . . . . . . . . 12 ⊢ ((𝑊 ∈ Word 𝑇 ∧ 𝐼 ∈ ℕ0 ∧ (𝐼 + 1) ∈ (0..^(♯‘𝑊))) → (𝑊 substr ⟨𝐼, (𝐼 + 2)⟩) = ⟨“(𝑊‘𝐼)(𝑊‘(𝐼 + 1))”⟩)
81	1, 10, 79, 80	syl3anc 1368	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑊 substr ⟨𝐼, (𝐼 + 2)⟩) = ⟨“(𝑊‘𝐼)(𝑊‘(𝐼 + 1))”⟩)
82	81	oveq2d 7151	. . . . . . . . . 10 ⊢ (𝜑 → (𝐺 Σg (𝑊 substr ⟨𝐼, (𝐼 + 2)⟩)) = (𝐺 Σg ⟨“(𝑊‘𝐼)(𝑊‘(𝐼 + 1))”⟩))
83		wrdf 13862	. . . . . . . . . . . . . . 15 ⊢ (𝑊 ∈ Word 𝑇 → 𝑊:(0..^(♯‘𝑊))⟶𝑇)
84	1, 83	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑊:(0..^(♯‘𝑊))⟶𝑇)
85	78	feq2d 6473	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑊:(0..^(♯‘𝑊))⟶𝑇 ↔ 𝑊:(0..^𝐿)⟶𝑇))
86	84, 85	mpbid 235	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑊:(0..^𝐿)⟶𝑇)
87	86, 7	ffvelrnd 6829	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑊‘𝐼) ∈ 𝑇)
88	66, 87	sseldi 3913	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑊‘𝐼) ∈ (Base‘𝐺))
89	86, 26	ffvelrnd 6829	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑊‘(𝐼 + 1)) ∈ 𝑇)
90	66, 89	sseldi 3913	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑊‘(𝐼 + 1)) ∈ (Base‘𝐺))
91		eqid 2798	. . . . . . . . . . . 12 ⊢ (+g‘𝐺) = (+g‘𝐺)
92	60, 91	gsumws2 17999	. . . . . . . . . . 11 ⊢ ((𝐺 ∈ Mnd ∧ (𝑊‘𝐼) ∈ (Base‘𝐺) ∧ (𝑊‘(𝐼 + 1)) ∈ (Base‘𝐺)) → (𝐺 Σg ⟨“(𝑊‘𝐼)(𝑊‘(𝐼 + 1))”⟩) = ((𝑊‘𝐼)(+g‘𝐺)(𝑊‘(𝐼 + 1))))
93	64, 88, 90, 92	syl3anc 1368	. . . . . . . . . 10 ⊢ (𝜑 → (𝐺 Σg ⟨“(𝑊‘𝐼)(𝑊‘(𝐼 + 1))”⟩) = ((𝑊‘𝐼)(+g‘𝐺)(𝑊‘(𝐼 + 1))))
94	19, 60, 91	symgov 18504	. . . . . . . . . . 11 ⊢ (((𝑊‘𝐼) ∈ (Base‘𝐺) ∧ (𝑊‘(𝐼 + 1)) ∈ (Base‘𝐺)) → ((𝑊‘𝐼)(+g‘𝐺)(𝑊‘(𝐼 + 1))) = ((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))))
95	88, 90, 94	syl2anc 587	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑊‘𝐼)(+g‘𝐺)(𝑊‘(𝐼 + 1))) = ((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))))
96	82, 93, 95	3eqtrd 2837	. . . . . . . . 9 ⊢ (𝜑 → (𝐺 Σg (𝑊 substr ⟨𝐼, (𝐼 + 2)⟩)) = ((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))))
97	96	adantr 484	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷)) → (𝐺 Σg (𝑊 substr ⟨𝐼, (𝐼 + 2)⟩)) = ((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))))
98		simpr 488	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷)) → ((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷))
99	19	symgid 18521	. . . . . . . . . . 11 ⊢ (𝐷 ∈ 𝑉 → ( I ↾ 𝐷) = (0g‘𝐺))
100	21, 99	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → ( I ↾ 𝐷) = (0g‘𝐺))
101		eqid 2798	. . . . . . . . . . 11 ⊢ (0g‘𝐺) = (0g‘𝐺)
102	101	gsum0 17886	. . . . . . . . . 10 ⊢ (𝐺 Σg ∅) = (0g‘𝐺)
103	100, 102	eqtr4di 2851	. . . . . . . . 9 ⊢ (𝜑 → ( I ↾ 𝐷) = (𝐺 Σg ∅))
104	103	adantr 484	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷)) → ( I ↾ 𝐷) = (𝐺 Σg ∅))
105	97, 98, 104	3eqtrd 2837	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷)) → (𝐺 Σg (𝑊 substr ⟨𝐼, (𝐼 + 2)⟩)) = (𝐺 Σg ∅))
106	60, 65, 70, 71, 72, 75, 77, 105	gsumspl 18001	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷)) → (𝐺 Σg (𝑊 splice ⟨𝐼, (𝐼 + 2), (𝑊 substr ⟨𝐼, (𝐼 + 2)⟩)⟩)) = (𝐺 Σg (𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩)))
107	22	adantr 484	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷)) → (𝐺 Σg 𝑊) = ( I ↾ 𝐷))
108	59, 106, 107	3eqtr3d 2841	. . . . 5 ⊢ ((𝜑 ∧ ((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷)) → (𝐺 Σg (𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩)) = ( I ↾ 𝐷))
109		fveqeq2 6654	. . . . . . 7 ⊢ (𝑥 = (𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩) → ((♯‘𝑥) = (𝐿 − 2) ↔ (♯‘(𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩)) = (𝐿 − 2)))
110		oveq2 7143	. . . . . . . 8 ⊢ (𝑥 = (𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩) → (𝐺 Σg 𝑥) = (𝐺 Σg (𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩)))
111	110	eqeq1d 2800	. . . . . . 7 ⊢ (𝑥 = (𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩) → ((𝐺 Σg 𝑥) = ( I ↾ 𝐷) ↔ (𝐺 Σg (𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩)) = ( I ↾ 𝐷)))
112	109, 111	anbi12d 633	. . . . . 6 ⊢ (𝑥 = (𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩) → (((♯‘𝑥) = (𝐿 − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)) ↔ ((♯‘(𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩)) = (𝐿 − 2) ∧ (𝐺 Σg (𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩)) = ( I ↾ 𝐷))))
113	112	rspcev 3571	. . . . 5 ⊢ (((𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩) ∈ Word 𝑇 ∧ ((♯‘(𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩)) = (𝐿 − 2) ∧ (𝐺 Σg (𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩)) = ( I ↾ 𝐷))) → ∃𝑥 ∈ Word 𝑇((♯‘𝑥) = (𝐿 − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)))
114	5, 55, 108, 113	syl12anc 835	. . . 4 ⊢ ((𝜑 ∧ ((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷)) → ∃𝑥 ∈ Word 𝑇((♯‘𝑥) = (𝐿 − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)))
115		psgnunilem2.in	. . . . 5 ⊢ (𝜑 → ¬ ∃𝑥 ∈ Word 𝑇((♯‘𝑥) = (𝐿 − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)))
116	115	adantr 484	. . . 4 ⊢ ((𝜑 ∧ ((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷)) → ¬ ∃𝑥 ∈ Word 𝑇((♯‘𝑥) = (𝐿 − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)))
117	114, 116	pm2.21dd 198	. . 3 ⊢ ((𝜑 ∧ ((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷)) → ∃𝑤 ∈ Word 𝑇(((𝐺 Σg 𝑤) = ( I ↾ 𝐷) ∧ (♯‘𝑤) = 𝐿) ∧ ((𝐼 + 1) ∈ (0..^𝐿) ∧ 𝐴 ∈ dom ((𝑤‘(𝐼 + 1)) ∖ I ) ∧ ∀𝑗 ∈ (0..^(𝐼 + 1)) ¬ 𝐴 ∈ dom ((𝑤‘𝑗) ∖ I ))))
118	117	ex 416	. 2 ⊢ (𝜑 → (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷) → ∃𝑤 ∈ Word 𝑇(((𝐺 Σg 𝑤) = ( I ↾ 𝐷) ∧ (♯‘𝑤) = 𝐿) ∧ ((𝐼 + 1) ∈ (0..^𝐿) ∧ 𝐴 ∈ dom ((𝑤‘(𝐼 + 1)) ∖ I ) ∧ ∀𝑗 ∈ (0..^(𝐼 + 1)) ¬ 𝐴 ∈ dom ((𝑤‘𝑗) ∖ I )))))
119	1	adantr 484	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → 𝑊 ∈ Word 𝑇)
120		simprl 770	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → 𝑟 ∈ 𝑇)
121		simprr 772	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → 𝑠 ∈ 𝑇)
122	120, 121	s2cld 14224	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → ⟨“𝑟𝑠”⟩ ∈ Word 𝑇)
123		splcl 14105	. . . . . . 7 ⊢ ((𝑊 ∈ Word 𝑇 ∧ ⟨“𝑟𝑠”⟩ ∈ Word 𝑇) → (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩) ∈ Word 𝑇)
124	119, 122, 123	syl2anc 587	. . . . . 6 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩) ∈ Word 𝑇)
125	124	adantrr 716	. . . . 5 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩) ∈ Word 𝑇)
126	64	adantr 484	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → 𝐺 ∈ Mnd)
127	69	adantr 484	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → 𝑊 ∈ Word (Base‘𝐺))
128	18	adantr 484	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → 𝐼 ∈ (0...(𝐼 + 2)))
129	36	adantr 484	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → (𝐼 + 2) ∈ (0...(♯‘𝑊)))
130	68, 122	sseldi 3913	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → ⟨“𝑟𝑠”⟩ ∈ Word (Base‘𝐺))
131	130	adantrr 716	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → ⟨“𝑟𝑠”⟩ ∈ Word (Base‘𝐺))
132	74	adantr 484	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → (𝑊 substr ⟨𝐼, (𝐼 + 2)⟩) ∈ Word (Base‘𝐺))
133		simprr1 1218	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → ((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠))
134	96	adantr 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → (𝐺 Σg (𝑊 substr ⟨𝐼, (𝐼 + 2)⟩)) = ((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))))
135	64	adantr 484	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → 𝐺 ∈ Mnd)
136	66	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑇 ⊆ (Base‘𝐺))
137	136	sselda 3915	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑟 ∈ 𝑇) → 𝑟 ∈ (Base‘𝐺))
138	137	adantrr 716	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → 𝑟 ∈ (Base‘𝐺))
139	136	sselda 3915	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝑇) → 𝑠 ∈ (Base‘𝐺))
140	139	adantrl 715	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → 𝑠 ∈ (Base‘𝐺))
141	60, 91	gsumws2 17999	. . . . . . . . . . . 12 ⊢ ((𝐺 ∈ Mnd ∧ 𝑟 ∈ (Base‘𝐺) ∧ 𝑠 ∈ (Base‘𝐺)) → (𝐺 Σg ⟨“𝑟𝑠”⟩) = (𝑟(+g‘𝐺)𝑠))
142	135, 138, 140, 141	syl3anc 1368	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → (𝐺 Σg ⟨“𝑟𝑠”⟩) = (𝑟(+g‘𝐺)𝑠))
143	19, 60, 91	symgov 18504	. . . . . . . . . . . 12 ⊢ ((𝑟 ∈ (Base‘𝐺) ∧ 𝑠 ∈ (Base‘𝐺)) → (𝑟(+g‘𝐺)𝑠) = (𝑟 ∘ 𝑠))
144	138, 140, 143	syl2anc 587	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → (𝑟(+g‘𝐺)𝑠) = (𝑟 ∘ 𝑠))
145	142, 144	eqtrd 2833	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → (𝐺 Σg ⟨“𝑟𝑠”⟩) = (𝑟 ∘ 𝑠))
146	145	adantrr 716	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → (𝐺 Σg ⟨“𝑟𝑠”⟩) = (𝑟 ∘ 𝑠))
147	133, 134, 146	3eqtr4rd 2844	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → (𝐺 Σg ⟨“𝑟𝑠”⟩) = (𝐺 Σg (𝑊 substr ⟨𝐼, (𝐼 + 2)⟩)))
148	60, 126, 127, 128, 129, 131, 132, 147	gsumspl 18001	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → (𝐺 Σg (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)) = (𝐺 Σg (𝑊 splice ⟨𝐼, (𝐼 + 2), (𝑊 substr ⟨𝐼, (𝐼 + 2)⟩)⟩)))
149	58	adantr 484	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → (𝐺 Σg (𝑊 splice ⟨𝐼, (𝐼 + 2), (𝑊 substr ⟨𝐼, (𝐼 + 2)⟩)⟩)) = (𝐺 Σg 𝑊))
150	22	adantr 484	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → (𝐺 Σg 𝑊) = ( I ↾ 𝐷))
151	148, 149, 150	3eqtrd 2837	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → (𝐺 Σg (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)) = ( I ↾ 𝐷))
152	18	adantr 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → 𝐼 ∈ (0...(𝐼 + 2)))
153	36	adantr 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → (𝐼 + 2) ∈ (0...(♯‘𝑊)))
154	119, 152, 153, 122	spllen 14107	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → (♯‘(𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)) = ((♯‘𝑊) + ((♯‘⟨“𝑟𝑠”⟩) − ((𝐼 + 2) − 𝐼))))
155		s2len 14242	. . . . . . . . . . . . 13 ⊢ (♯‘⟨“𝑟𝑠”⟩) = 2
156	155	oveq1i 7145	. . . . . . . . . . . 12 ⊢ ((♯‘⟨“𝑟𝑠”⟩) − ((𝐼 + 2) − 𝐼)) = (2 − ((𝐼 + 2) − 𝐼))
157	45	oveq2d 7151	. . . . . . . . . . . . 13 ⊢ (𝜑 → (2 − ((𝐼 + 2) − 𝐼)) = (2 − 2))
158	43	subidi 10946	. . . . . . . . . . . . 13 ⊢ (2 − 2) = 0
159	157, 158	eqtrdi 2849	. . . . . . . . . . . 12 ⊢ (𝜑 → (2 − ((𝐼 + 2) − 𝐼)) = 0)
160	156, 159	syl5eq 2845	. . . . . . . . . . 11 ⊢ (𝜑 → ((♯‘⟨“𝑟𝑠”⟩) − ((𝐼 + 2) − 𝐼)) = 0)
161	160	oveq2d 7151	. . . . . . . . . 10 ⊢ (𝜑 → ((♯‘𝑊) + ((♯‘⟨“𝑟𝑠”⟩) − ((𝐼 + 2) − 𝐼))) = ((♯‘𝑊) + 0))
162	23, 51	eqeltrd 2890	. . . . . . . . . . 11 ⊢ (𝜑 → (♯‘𝑊) ∈ ℂ)
163	162	addid1d 10829	. . . . . . . . . 10 ⊢ (𝜑 → ((♯‘𝑊) + 0) = (♯‘𝑊))
164	161, 163, 23	3eqtrd 2837	. . . . . . . . 9 ⊢ (𝜑 → ((♯‘𝑊) + ((♯‘⟨“𝑟𝑠”⟩) − ((𝐼 + 2) − 𝐼))) = 𝐿)
165	164	adantr 484	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → ((♯‘𝑊) + ((♯‘⟨“𝑟𝑠”⟩) − ((𝐼 + 2) − 𝐼))) = 𝐿)
166	154, 165	eqtrd 2833	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → (♯‘(𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)) = 𝐿)
167	166	adantrr 716	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → (♯‘(𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)) = 𝐿)
168	151, 167	jca 515	. . . . 5 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → ((𝐺 Σg (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)) = ( I ↾ 𝐷) ∧ (♯‘(𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)) = 𝐿))
169	26	adantr 484	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → (𝐼 + 1) ∈ (0..^𝐿))
170		simprr2 1219	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → 𝐴 ∈ dom (𝑠 ∖ I ))
171		1nn0 11901	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ ℕ0
172		2nn 11698	. . . . . . . . . . . . . . 15 ⊢ 2 ∈ ℕ
173		1lt2 11796	. . . . . . . . . . . . . . 15 ⊢ 1 < 2
174		elfzo0 13073	. . . . . . . . . . . . . . 15 ⊢ (1 ∈ (0..^2) ↔ (1 ∈ ℕ0 ∧ 2 ∈ ℕ ∧ 1 < 2))
175	171, 172, 173, 174	mpbir3an 1338	. . . . . . . . . . . . . 14 ⊢ 1 ∈ (0..^2)
176	155	oveq2i 7146	. . . . . . . . . . . . . 14 ⊢ (0..^(♯‘⟨“𝑟𝑠”⟩)) = (0..^2)
177	175, 176	eleqtrri 2889	. . . . . . . . . . . . 13 ⊢ 1 ∈ (0..^(♯‘⟨“𝑟𝑠”⟩))
178	177	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → 1 ∈ (0..^(♯‘⟨“𝑟𝑠”⟩)))
179	119, 152, 153, 122, 178	splfv2a 14109	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → ((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘(𝐼 + 1)) = (⟨“𝑟𝑠”⟩‘1))
180		s2fv1 14241	. . . . . . . . . . . 12 ⊢ (𝑠 ∈ 𝑇 → (⟨“𝑟𝑠”⟩‘1) = 𝑠)
181	180	ad2antll 728	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → (⟨“𝑟𝑠”⟩‘1) = 𝑠)
182	179, 181	eqtrd 2833	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → ((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘(𝐼 + 1)) = 𝑠)
183	182	adantrr 716	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → ((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘(𝐼 + 1)) = 𝑠)
184	183	difeq1d 4049	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘(𝐼 + 1)) ∖ I ) = (𝑠 ∖ I ))
185	184	dmeqd 5738	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘(𝐼 + 1)) ∖ I ) = dom (𝑠 ∖ I ))
186	170, 185	eleqtrrd 2893	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → 𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘(𝐼 + 1)) ∖ I ))
187		fzosplitsni 13143	. . . . . . . . . . 11 ⊢ (𝐼 ∈ (ℤ≥‘0) → (𝑗 ∈ (0..^(𝐼 + 1)) ↔ (𝑗 ∈ (0..^𝐼) ∨ 𝑗 = 𝐼)))
188		nn0uz 12268	. . . . . . . . . . 11 ⊢ ℕ0 = (ℤ≥‘0)
189	187, 188	eleq2s 2908	. . . . . . . . . 10 ⊢ (𝐼 ∈ ℕ0 → (𝑗 ∈ (0..^(𝐼 + 1)) ↔ (𝑗 ∈ (0..^𝐼) ∨ 𝑗 = 𝐼)))
190	10, 189	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (𝑗 ∈ (0..^(𝐼 + 1)) ↔ (𝑗 ∈ (0..^𝐼) ∨ 𝑗 = 𝐼)))
191	190	adantr 484	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → (𝑗 ∈ (0..^(𝐼 + 1)) ↔ (𝑗 ∈ (0..^𝐼) ∨ 𝑗 = 𝐼)))
192		fveq2 6645	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 𝑗 → (𝑊‘𝑘) = (𝑊‘𝑗))
193	192	difeq1d 4049	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 𝑗 → ((𝑊‘𝑘) ∖ I ) = ((𝑊‘𝑗) ∖ I ))
194	193	dmeqd 5738	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 𝑗 → dom ((𝑊‘𝑘) ∖ I ) = dom ((𝑊‘𝑗) ∖ I ))
195	194	eleq2d 2875	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 𝑗 → (𝐴 ∈ dom ((𝑊‘𝑘) ∖ I ) ↔ 𝐴 ∈ dom ((𝑊‘𝑗) ∖ I )))
196	195	notbid 321	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑗 → (¬ 𝐴 ∈ dom ((𝑊‘𝑘) ∖ I ) ↔ ¬ 𝐴 ∈ dom ((𝑊‘𝑗) ∖ I )))
197	196	rspccva 3570	. . . . . . . . . . . . . 14 ⊢ ((∀𝑘 ∈ (0..^𝐼) ¬ 𝐴 ∈ dom ((𝑊‘𝑘) ∖ I ) ∧ 𝑗 ∈ (0..^𝐼)) → ¬ 𝐴 ∈ dom ((𝑊‘𝑗) ∖ I ))
198	25, 197	sylan 583	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝐼)) → ¬ 𝐴 ∈ dom ((𝑊‘𝑗) ∖ I ))
199	198	adantlr 714	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) ∧ 𝑗 ∈ (0..^𝐼)) → ¬ 𝐴 ∈ dom ((𝑊‘𝑗) ∖ I ))
200	1	ad2antrr 725	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) ∧ 𝑗 ∈ (0..^𝐼)) → 𝑊 ∈ Word 𝑇)
201	18	ad2antrr 725	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) ∧ 𝑗 ∈ (0..^𝐼)) → 𝐼 ∈ (0...(𝐼 + 2)))
202	36	ad2antrr 725	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) ∧ 𝑗 ∈ (0..^𝐼)) → (𝐼 + 2) ∈ (0...(♯‘𝑊)))
203	122	adantr 484	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) ∧ 𝑗 ∈ (0..^𝐼)) → ⟨“𝑟𝑠”⟩ ∈ Word 𝑇)
204		simpr 488	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) ∧ 𝑗 ∈ (0..^𝐼)) → 𝑗 ∈ (0..^𝐼))
205	200, 201, 202, 203, 204	splfv1 14108	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) ∧ 𝑗 ∈ (0..^𝐼)) → ((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) = (𝑊‘𝑗))
206	205	difeq1d 4049	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) ∧ 𝑗 ∈ (0..^𝐼)) → (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) ∖ I ) = ((𝑊‘𝑗) ∖ I ))
207	206	dmeqd 5738	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) ∧ 𝑗 ∈ (0..^𝐼)) → dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) ∖ I ) = dom ((𝑊‘𝑗) ∖ I ))
208	199, 207	neleqtrrd 2912	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) ∧ 𝑗 ∈ (0..^𝐼)) → ¬ 𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) ∖ I ))
209	208	ex 416	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → (𝑗 ∈ (0..^𝐼) → ¬ 𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) ∖ I )))
210	209	adantrr 716	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → (𝑗 ∈ (0..^𝐼) → ¬ 𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) ∖ I )))
211		simprr3 1220	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → ¬ 𝐴 ∈ dom (𝑟 ∖ I ))
212		0nn0 11900	. . . . . . . . . . . . . . . . . . . 20 ⊢ 0 ∈ ℕ0
213		2pos 11728	. . . . . . . . . . . . . . . . . . . 20 ⊢ 0 < 2
214		elfzo0 13073	. . . . . . . . . . . . . . . . . . . 20 ⊢ (0 ∈ (0..^2) ↔ (0 ∈ ℕ0 ∧ 2 ∈ ℕ ∧ 0 < 2))
215	212, 172, 213, 214	mpbir3an 1338	. . . . . . . . . . . . . . . . . . 19 ⊢ 0 ∈ (0..^2)
216	215, 176	eleqtrri 2889	. . . . . . . . . . . . . . . . . 18 ⊢ 0 ∈ (0..^(♯‘⟨“𝑟𝑠”⟩))
217	216	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → 0 ∈ (0..^(♯‘⟨“𝑟𝑠”⟩)))
218	119, 152, 153, 122, 217	splfv2a 14109	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → ((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘(𝐼 + 0)) = (⟨“𝑟𝑠”⟩‘0))
219	31	addid1d 10829	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐼 + 0) = 𝐼)
220	219	adantr 484	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → (𝐼 + 0) = 𝐼)
221	220	fveq2d 6649	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → ((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘(𝐼 + 0)) = ((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝐼))
222		s2fv0 14240	. . . . . . . . . . . . . . . . 17 ⊢ (𝑟 ∈ 𝑇 → (⟨“𝑟𝑠”⟩‘0) = 𝑟)
223	222	ad2antrl 727	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → (⟨“𝑟𝑠”⟩‘0) = 𝑟)
224	218, 221, 223	3eqtr3d 2841	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → ((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝐼) = 𝑟)
225	224	difeq1d 4049	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝐼) ∖ I ) = (𝑟 ∖ I ))
226	225	dmeqd 5738	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝐼) ∖ I ) = dom (𝑟 ∖ I ))
227	226	eleq2d 2875	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → (𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝐼) ∖ I ) ↔ 𝐴 ∈ dom (𝑟 ∖ I )))
228	227	adantrr 716	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → (𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝐼) ∖ I ) ↔ 𝐴 ∈ dom (𝑟 ∖ I )))
229	211, 228	mtbird 328	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → ¬ 𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝐼) ∖ I ))
230		fveq2 6645	. . . . . . . . . . . . . 14 ⊢ (𝑗 = 𝐼 → ((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) = ((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝐼))
231	230	difeq1d 4049	. . . . . . . . . . . . 13 ⊢ (𝑗 = 𝐼 → (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) ∖ I ) = (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝐼) ∖ I ))
232	231	dmeqd 5738	. . . . . . . . . . . 12 ⊢ (𝑗 = 𝐼 → dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) ∖ I ) = dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝐼) ∖ I ))
233	232	eleq2d 2875	. . . . . . . . . . 11 ⊢ (𝑗 = 𝐼 → (𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) ∖ I ) ↔ 𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝐼) ∖ I )))
234	233	notbid 321	. . . . . . . . . 10 ⊢ (𝑗 = 𝐼 → (¬ 𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) ∖ I ) ↔ ¬ 𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝐼) ∖ I )))
235	229, 234	syl5ibrcom 250	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → (𝑗 = 𝐼 → ¬ 𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) ∖ I )))
236	210, 235	jaod 856	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → ((𝑗 ∈ (0..^𝐼) ∨ 𝑗 = 𝐼) → ¬ 𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) ∖ I )))
237	191, 236	sylbid 243	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → (𝑗 ∈ (0..^(𝐼 + 1)) → ¬ 𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) ∖ I )))
238	237	ralrimiv 3148	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → ∀𝑗 ∈ (0..^(𝐼 + 1)) ¬ 𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) ∖ I ))
239	169, 186, 238	3jca 1125	. . . . 5 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → ((𝐼 + 1) ∈ (0..^𝐿) ∧ 𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘(𝐼 + 1)) ∖ I ) ∧ ∀𝑗 ∈ (0..^(𝐼 + 1)) ¬ 𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) ∖ I )))
240		oveq2 7143	. . . . . . . . 9 ⊢ (𝑤 = (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩) → (𝐺 Σg 𝑤) = (𝐺 Σg (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)))
241	240	eqeq1d 2800	. . . . . . . 8 ⊢ (𝑤 = (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩) → ((𝐺 Σg 𝑤) = ( I ↾ 𝐷) ↔ (𝐺 Σg (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)) = ( I ↾ 𝐷)))
242		fveqeq2 6654	. . . . . . . 8 ⊢ (𝑤 = (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩) → ((♯‘𝑤) = 𝐿 ↔ (♯‘(𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)) = 𝐿))
243	241, 242	anbi12d 633	. . . . . . 7 ⊢ (𝑤 = (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩) → (((𝐺 Σg 𝑤) = ( I ↾ 𝐷) ∧ (♯‘𝑤) = 𝐿) ↔ ((𝐺 Σg (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)) = ( I ↾ 𝐷) ∧ (♯‘(𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)) = 𝐿)))
244		fveq1 6644	. . . . . . . . . . 11 ⊢ (𝑤 = (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩) → (𝑤‘(𝐼 + 1)) = ((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘(𝐼 + 1)))
245	244	difeq1d 4049	. . . . . . . . . 10 ⊢ (𝑤 = (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩) → ((𝑤‘(𝐼 + 1)) ∖ I ) = (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘(𝐼 + 1)) ∖ I ))
246	245	dmeqd 5738	. . . . . . . . 9 ⊢ (𝑤 = (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩) → dom ((𝑤‘(𝐼 + 1)) ∖ I ) = dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘(𝐼 + 1)) ∖ I ))
247	246	eleq2d 2875	. . . . . . . 8 ⊢ (𝑤 = (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩) → (𝐴 ∈ dom ((𝑤‘(𝐼 + 1)) ∖ I ) ↔ 𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘(𝐼 + 1)) ∖ I )))
248		fveq1 6644	. . . . . . . . . . . . 13 ⊢ (𝑤 = (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩) → (𝑤‘𝑗) = ((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗))
249	248	difeq1d 4049	. . . . . . . . . . . 12 ⊢ (𝑤 = (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩) → ((𝑤‘𝑗) ∖ I ) = (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) ∖ I ))
250	249	dmeqd 5738	. . . . . . . . . . 11 ⊢ (𝑤 = (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩) → dom ((𝑤‘𝑗) ∖ I ) = dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) ∖ I ))
251	250	eleq2d 2875	. . . . . . . . . 10 ⊢ (𝑤 = (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩) → (𝐴 ∈ dom ((𝑤‘𝑗) ∖ I ) ↔ 𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) ∖ I )))
252	251	notbid 321	. . . . . . . . 9 ⊢ (𝑤 = (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩) → (¬ 𝐴 ∈ dom ((𝑤‘𝑗) ∖ I ) ↔ ¬ 𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) ∖ I )))
253	252	ralbidv 3162	. . . . . . . 8 ⊢ (𝑤 = (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩) → (∀𝑗 ∈ (0..^(𝐼 + 1)) ¬ 𝐴 ∈ dom ((𝑤‘𝑗) ∖ I ) ↔ ∀𝑗 ∈ (0..^(𝐼 + 1)) ¬ 𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) ∖ I )))
254	247, 253	3anbi23d 1436	. . . . . . 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 ))))
255	243, 254	anbi12d 633	. . . . . 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 )))))
256	255	rspcev 3571	. . . . 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 ))))
257	125, 168, 239, 256	syl12anc 835	. . . 4 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → ∃𝑤 ∈ Word 𝑇(((𝐺 Σg 𝑤) = ( I ↾ 𝐷) ∧ (♯‘𝑤) = 𝐿) ∧ ((𝐼 + 1) ∈ (0..^𝐿) ∧ 𝐴 ∈ dom ((𝑤‘(𝐼 + 1)) ∖ I ) ∧ ∀𝑗 ∈ (0..^(𝐼 + 1)) ¬ 𝐴 ∈ dom ((𝑤‘𝑗) ∖ I ))))
258	257	expr 460	. . 3 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → ((((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )) → ∃𝑤 ∈ Word 𝑇(((𝐺 Σg 𝑤) = ( I ↾ 𝐷) ∧ (♯‘𝑤) = 𝐿) ∧ ((𝐼 + 1) ∈ (0..^𝐿) ∧ 𝐴 ∈ dom ((𝑤‘(𝐼 + 1)) ∖ I ) ∧ ∀𝑗 ∈ (0..^(𝐼 + 1)) ¬ 𝐴 ∈ dom ((𝑤‘𝑗) ∖ I )))))
259	258	rexlimdvva 3253	. 2 ⊢ (𝜑 → (∃𝑟 ∈ 𝑇 ∃𝑠 ∈ 𝑇 (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )) → ∃𝑤 ∈ Word 𝑇(((𝐺 Σg 𝑤) = ( I ↾ 𝐷) ∧ (♯‘𝑤) = 𝐿) ∧ ((𝐼 + 1) ∈ (0..^𝐿) ∧ 𝐴 ∈ dom ((𝑤‘(𝐼 + 1)) ∖ I ) ∧ ∀𝑗 ∈ (0..^(𝐼 + 1)) ¬ 𝐴 ∈ dom ((𝑤‘𝑗) ∖ I )))))
260	20, 21, 87, 89, 24	psgnunilem1 18613	. 2 ⊢ (𝜑 → (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷) ∨ ∃𝑟 ∈ 𝑇 ∃𝑠 ∈ 𝑇 (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I ))))
261	118, 259, 260	mpjaod 857	1 ⊢ (𝜑 → ∃𝑤 ∈ Word 𝑇(((𝐺 Σg 𝑤) = ( I ↾ 𝐷) ∧ (♯‘𝑤) = 𝐿) ∧ ((𝐼 + 1) ∈ (0..^𝐿) ∧ 𝐴 ∈ dom ((𝑤‘(𝐼 + 1)) ∖ I ) ∧ ∀𝑗 ∈ (0..^(𝐼 + 1)) ¬ 𝐴 ∈ dom ((𝑤‘𝑗) ∖ I ))))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   ∨ wo 844   ∧ w3a 1084   = wceq 1538   ∈ wcel 2111  ∀wral 3106  ∃wrex 3107   ∖ cdif 3878   ⊆ wss 3881  ∅c0 4243  ⟨cop 4531  ⟨cotp 4533   class class class wbr 5030   I cid 5424  dom cdm 5519  ran crn 5520   ↾ cres 5521   ∘ ccom 5523  ⟶wf 6320  ‘cfv 6324  (class class class)co 7135  ℂcc 10524  ℝcr 10525  0cc0 10526  1c1 10527   + caddc 10529   < clt 10664   ≤ cle 10665   − cmin 10859  -cneg 10860  ℕcn 11625  2c2 11680  ℕ₀cn0 11885  ℤcz 11969  ℤ_≥cuz 12231  ...cfz 12885  ..^cfzo 13028  ♯chash 13686  Word cword 13857   substr csubstr 13993   splice csplice 14102  ⟨“cs2 14194  Basecbs 16475  +_gcplusg 16557  0_gc0g 16705   Σ_g cgsu 16706  Mndcmnd 17903  Grpcgrp 18095  SymGrpcsymg 18487  pmTrspcpmtr 18561

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-rep 5154  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295  ax-un 7441  ax-cnex 10582  ax-resscn 10583  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-addrcl 10587  ax-mulcl 10588  ax-mulrcl 10589  ax-mulcom 10590  ax-addass 10591  ax-mulass 10592  ax-distr 10593  ax-i2m1 10594  ax-1ne0 10595  ax-1rid 10596  ax-rnegex 10597  ax-rrecex 10598  ax-cnre 10599  ax-pre-lttri 10600  ax-pre-lttrn 10601  ax-pre-ltadd 10602  ax-pre-mulgt0 10603

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-xor 1503  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-nel 3092  df-ral 3111  df-rex 3112  df-reu 3113  df-rmo 3114  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-pss 3900  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-ot 4534  df-uni 4801  df-int 4839  df-iun 4883  df-br 5031  df-opab 5093  df-mpt 5111  df-tr 5137  df-id 5425  df-eprel 5430  df-po 5438  df-so 5439  df-fr 5478  df-we 5480  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-pred 6116  df-ord 6162  df-on 6163  df-lim 6164  df-suc 6165  df-iota 6283  df-fun 6326  df-fn 6327  df-f 6328  df-f1 6329  df-fo 6330  df-f1o 6331  df-fv 6332  df-riota 7093  df-ov 7138  df-oprab 7139  df-mpo 7140  df-om 7561  df-1st 7671  df-2nd 7672  df-wrecs 7930  df-recs 7991  df-rdg 8029  df-1o 8085  df-2o 8086  df-oadd 8089  df-er 8272  df-map 8391  df-en 8493  df-dom 8494  df-sdom 8495  df-fin 8496  df-card 9352  df-pnf 10666  df-mnf 10667  df-xr 10668  df-ltxr 10669  df-le 10670  df-sub 10861  df-neg 10862  df-nn 11626  df-2 11688  df-3 11689  df-4 11690  df-5 11691  df-6 11692  df-7 11693  df-8 11694  df-9 11695  df-n0 11886  df-xnn0 11956  df-z 11970  df-uz 12232  df-fz 12886  df-fzo 13029  df-seq 13365  df-hash 13687  df-word 13858  df-lsw 13906  df-concat 13914  df-s1 13941  df-substr 13994  df-pfx 14024  df-splice 14103  df-s2 14201  df-struct 16477  df-ndx 16478  df-slot 16479  df-base 16481  df-sets 16482  df-ress 16483  df-plusg 16570  df-tset 16576  df-0g 16707  df-gsum 16708  df-mgm 17844  df-sgrp 17893  df-mnd 17904  df-submnd 17949  df-efmnd 18026  df-grp 18098  df-minusg 18099  df-subg 18268  df-symg 18488  df-pmtr 18562

This theorem is referenced by:  psgnunilem3  18616