Theorem psgnunilem2 19564

Description: Lemma for psgnuni 19568. 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 14575	. . . . . . 7 ⊢ ∅ ∈ Word 𝑇
3		splcl 14788	. . . . . . 7 ⊢ ((𝑊 ∈ Word 𝑇 ∧ ∅ ∈ Word 𝑇) → (𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩) ∈ Word 𝑇)
4	1, 2, 3	sylancl 597	. . . . . 6 ⊢ (𝜑 → (𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩) ∈ Word 𝑇)
5	4	adantr 485	. . . . 5 ⊢ ((𝜑 ∧ ((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷)) → (𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩) ∈ Word 𝑇)
6		fzossfz 13706	. . . . . . . . . . 11 ⊢ (0..^𝐿) ⊆ (0...𝐿)
7		psgnunilem2.ix	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐼 ∈ (0..^𝐿))
8	6, 7	sselid 3943	. . . . . . . . . 10 ⊢ (𝜑 → 𝐼 ∈ (0...𝐿))
9		elfznn0 13647	. . . . . . . . . 10 ⊢ (𝐼 ∈ (0...𝐿) → 𝐼 ∈ ℕ0)
10	8, 9	syl 18	. . . . . . . . 9 ⊢ (𝜑 → 𝐼 ∈ ℕ0)
11		2nn0 12520	. . . . . . . . . 10 ⊢ 2 ∈ ℕ0
12		nn0addcl 12538	. . . . . . . . . 10 ⊢ ((𝐼 ∈ ℕ0 ∧ 2 ∈ ℕ0) → (𝐼 + 2) ∈ ℕ0)
13	10, 11, 12	sylancl 597	. . . . . . . . 9 ⊢ (𝜑 → (𝐼 + 2) ∈ ℕ0)
14	10	nn0red 12565	. . . . . . . . . 10 ⊢ (𝜑 → 𝐼 ∈ ℝ)
15		nn0addge1 12549	. . . . . . . . . 10 ⊢ ((𝐼 ∈ ℝ ∧ 2 ∈ ℕ0) → 𝐼 ≤ (𝐼 + 2))
16	14, 11, 15	sylancl 597	. . . . . . . . 9 ⊢ (𝜑 → 𝐼 ≤ (𝐼 + 2))
17		elfz2nn0 13645	. . . . . . . . 9 ⊢ (𝐼 ∈ (0...(𝐼 + 2)) ↔ (𝐼 ∈ ℕ0 ∧ (𝐼 + 2) ∈ ℕ0 ∧ 𝐼 ≤ (𝐼 + 2)))
18	10, 13, 16, 17	syl3anbrc 1360	. . . . . . . 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 19563	. . . . . . . . . 10 ⊢ (𝜑 → (𝐼 + 1) ∈ (0..^𝐿))
27		fzofzp1 13792	. . . . . . . . . 10 ⊢ ((𝐼 + 1) ∈ (0..^𝐿) → ((𝐼 + 1) + 1) ∈ (0...𝐿))
28	26, 27	syl 18	. . . . . . . . 9 ⊢ (𝜑 → ((𝐼 + 1) + 1) ∈ (0...𝐿))
29		df-2 12302	. . . . . . . . . . 11 ⊢ 2 = (1 + 1)
30	29	oveq2i 7422	. . . . . . . . . 10 ⊢ (𝐼 + 2) = (𝐼 + (1 + 1))
31	10	nn0cnd 12566	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐼 ∈ ℂ)
32		1cnd 11201	. . . . . . . . . . 11 ⊢ (𝜑 → 1 ∈ ℂ)
33	31, 32, 32	addassd 11230	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐼 + 1) + 1) = (𝐼 + (1 + 1)))
34	30, 33	eqtr4id 2823	. . . . . . . . 9 ⊢ (𝜑 → (𝐼 + 2) = ((𝐼 + 1) + 1))
35	23	oveq2d 7427	. . . . . . . . 9 ⊢ (𝜑 → (0...(♯‘𝑊)) = (0...𝐿))
36	28, 34, 35	3eltr4d 2884	. . . . . . . 8 ⊢ (𝜑 → (𝐼 + 2) ∈ (0...(♯‘𝑊)))
37	2	a1i 11	. . . . . . . 8 ⊢ (𝜑 → ∅ ∈ Word 𝑇)
38	1, 18, 36, 37	spllen 14790	. . . . . . 7 ⊢ (𝜑 → (♯‘(𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩)) = ((♯‘𝑊) + ((♯‘∅) − ((𝐼 + 2) − 𝐼))))
39		hash0 14402	. . . . . . . . . . 11 ⊢ (♯‘∅) = 0
40	39	oveq1i 7421	. . . . . . . . . 10 ⊢ ((♯‘∅) − ((𝐼 + 2) − 𝐼)) = (0 − ((𝐼 + 2) − 𝐼))
41		df-neg 11443	. . . . . . . . . 10 ⊢ -((𝐼 + 2) − 𝐼) = (0 − ((𝐼 + 2) − 𝐼))
42	40, 41	eqtr4i 2795	. . . . . . . . 9 ⊢ ((♯‘∅) − ((𝐼 + 2) − 𝐼)) = -((𝐼 + 2) − 𝐼)
43		2cn 12315	. . . . . . . . . . 11 ⊢ 2 ∈ ℂ
44		pncan2 11463	. . . . . . . . . . 11 ⊢ ((𝐼 ∈ ℂ ∧ 2 ∈ ℂ) → ((𝐼 + 2) − 𝐼) = 2)
45	31, 43, 44	sylancl 597	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐼 + 2) − 𝐼) = 2)
46	45	negeqd 11450	. . . . . . . . 9 ⊢ (𝜑 → -((𝐼 + 2) − 𝐼) = -2)
47	42, 46	eqtrid 2816	. . . . . . . 8 ⊢ (𝜑 → ((♯‘∅) − ((𝐼 + 2) − 𝐼)) = -2)
48	23, 47	oveq12d 7429	. . . . . . 7 ⊢ (𝜑 → ((♯‘𝑊) + ((♯‘∅) − ((𝐼 + 2) − 𝐼))) = (𝐿 + -2))
49		elfzel2 13549	. . . . . . . . . 10 ⊢ (𝐼 ∈ (0...𝐿) → 𝐿 ∈ ℤ)
50	8, 49	syl 18	. . . . . . . . 9 ⊢ (𝜑 → 𝐿 ∈ ℤ)
51	50	zcnd 12700	. . . . . . . 8 ⊢ (𝜑 → 𝐿 ∈ ℂ)
52		negsub 11505	. . . . . . . 8 ⊢ ((𝐿 ∈ ℂ ∧ 2 ∈ ℂ) → (𝐿 + -2) = (𝐿 − 2))
53	51, 43, 52	sylancl 597	. . . . . . 7 ⊢ (𝜑 → (𝐿 + -2) = (𝐿 − 2))
54	38, 48, 53	3eqtrd 2808	. . . . . 6 ⊢ (𝜑 → (♯‘(𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩)) = (𝐿 − 2))
55	54	adantr 485	. . . . 5 ⊢ ((𝜑 ∧ ((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷)) → (♯‘(𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩)) = (𝐿 − 2))
56		splid 14789	. . . . . . . . 9 ⊢ ((𝑊 ∈ Word 𝑇 ∧ (𝐼 ∈ (0...(𝐼 + 2)) ∧ (𝐼 + 2) ∈ (0...(♯‘𝑊)))) → (𝑊 splice ⟨𝐼, (𝐼 + 2), (𝑊 substr ⟨𝐼, (𝐼 + 2)⟩)⟩) = 𝑊)
57	1, 18, 36, 56	syl12anc 849	. . . . . . . 8 ⊢ (𝜑 → (𝑊 splice ⟨𝐼, (𝐼 + 2), (𝑊 substr ⟨𝐼, (𝐼 + 2)⟩)⟩) = 𝑊)
58	57	oveq2d 7427	. . . . . . 7 ⊢ (𝜑 → (𝐺 Σg (𝑊 splice ⟨𝐼, (𝐼 + 2), (𝑊 substr ⟨𝐼, (𝐼 + 2)⟩)⟩)) = (𝐺 Σg 𝑊))
59	58	adantr 485	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷)) → (𝐺 Σg (𝑊 splice ⟨𝐼, (𝐼 + 2), (𝑊 substr ⟨𝐼, (𝐼 + 2)⟩)⟩)) = (𝐺 Σg 𝑊))
60		eqid 2769	. . . . . . 7 ⊢ (Base‘𝐺) = (Base‘𝐺)
61	19	symggrp 19469	. . . . . . . . . 10 ⊢ (𝐷 ∈ 𝑉 → 𝐺 ∈ Grp)
62	21, 61	syl 18	. . . . . . . . 9 ⊢ (𝜑 → 𝐺 ∈ Grp)
63	62	grpmndd 19012	. . . . . . . 8 ⊢ (𝜑 → 𝐺 ∈ Mnd)
64	63	adantr 485	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷)) → 𝐺 ∈ Mnd)
65	20, 19, 60	symgtrf 19538	. . . . . . . . . 10 ⊢ 𝑇 ⊆ (Base‘𝐺)
66		sswrd 14558	. . . . . . . . . 10 ⊢ (𝑇 ⊆ (Base‘𝐺) → Word 𝑇 ⊆ Word (Base‘𝐺))
67	65, 66	ax-mp 5	. . . . . . . . 9 ⊢ Word 𝑇 ⊆ Word (Base‘𝐺)
68	67, 1	sselid 3943	. . . . . . . 8 ⊢ (𝜑 → 𝑊 ∈ Word (Base‘𝐺))
69	68	adantr 485	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷)) → 𝑊 ∈ Word (Base‘𝐺))
70	18	adantr 485	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷)) → 𝐼 ∈ (0...(𝐼 + 2)))
71	36	adantr 485	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷)) → (𝐼 + 2) ∈ (0...(♯‘𝑊)))
72		swrdcl 14682	. . . . . . . . 9 ⊢ (𝑊 ∈ Word (Base‘𝐺) → (𝑊 substr ⟨𝐼, (𝐼 + 2)⟩) ∈ Word (Base‘𝐺))
73	68, 72	syl 18	. . . . . . . 8 ⊢ (𝜑 → (𝑊 substr ⟨𝐼, (𝐼 + 2)⟩) ∈ Word (Base‘𝐺))
74	73	adantr 485	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷)) → (𝑊 substr ⟨𝐼, (𝐼 + 2)⟩) ∈ Word (Base‘𝐺))
75		wrd0 14575	. . . . . . . 8 ⊢ ∅ ∈ Word (Base‘𝐺)
76	75	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷)) → ∅ ∈ Word (Base‘𝐺))
77	23	oveq2d 7427	. . . . . . . . . . . . 13 ⊢ (𝜑 → (0..^(♯‘𝑊)) = (0..^𝐿))
78	26, 77	eleqtrrd 2872	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐼 + 1) ∈ (0..^(♯‘𝑊)))
79		swrds2 14976	. . . . . . . . . . . 12 ⊢ ((𝑊 ∈ Word 𝑇 ∧ 𝐼 ∈ ℕ0 ∧ (𝐼 + 1) ∈ (0..^(♯‘𝑊))) → (𝑊 substr ⟨𝐼, (𝐼 + 2)⟩) = ⟨“(𝑊‘𝐼)(𝑊‘(𝐼 + 1))”⟩)
80	1, 10, 78, 79	syl3anc 1396	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑊 substr ⟨𝐼, (𝐼 + 2)⟩) = ⟨“(𝑊‘𝐼)(𝑊‘(𝐼 + 1))”⟩)
81	80	oveq2d 7427	. . . . . . . . . 10 ⊢ (𝜑 → (𝐺 Σg (𝑊 substr ⟨𝐼, (𝐼 + 2)⟩)) = (𝐺 Σg ⟨“(𝑊‘𝐼)(𝑊‘(𝐼 + 1))”⟩))
82		wrdf 14554	. . . . . . . . . . . . . . 15 ⊢ (𝑊 ∈ Word 𝑇 → 𝑊:(0..^(♯‘𝑊))⟶𝑇)
83	1, 82	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑊:(0..^(♯‘𝑊))⟶𝑇)
84	77	feq2d 6690	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑊:(0..^(♯‘𝑊))⟶𝑇 ↔ 𝑊:(0..^𝐿)⟶𝑇))
85	83, 84	mpbid 235	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑊:(0..^𝐿)⟶𝑇)
86	85, 7	ffvelcdmd 7081	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑊‘𝐼) ∈ 𝑇)
87	65, 86	sselid 3943	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑊‘𝐼) ∈ (Base‘𝐺))
88	85, 26	ffvelcdmd 7081	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑊‘(𝐼 + 1)) ∈ 𝑇)
89	65, 88	sselid 3943	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑊‘(𝐼 + 1)) ∈ (Base‘𝐺))
90		eqid 2769	. . . . . . . . . . . 12 ⊢ (+g‘𝐺) = (+g‘𝐺)
91	60, 90	gsumws2 18900	. . . . . . . . . . 11 ⊢ ((𝐺 ∈ Mnd ∧ (𝑊‘𝐼) ∈ (Base‘𝐺) ∧ (𝑊‘(𝐼 + 1)) ∈ (Base‘𝐺)) → (𝐺 Σg ⟨“(𝑊‘𝐼)(𝑊‘(𝐼 + 1))”⟩) = ((𝑊‘𝐼)(+g‘𝐺)(𝑊‘(𝐼 + 1))))
92	63, 87, 89, 91	syl3anc 1396	. . . . . . . . . 10 ⊢ (𝜑 → (𝐺 Σg ⟨“(𝑊‘𝐼)(𝑊‘(𝐼 + 1))”⟩) = ((𝑊‘𝐼)(+g‘𝐺)(𝑊‘(𝐼 + 1))))
93	19, 60, 90	symgov 19453	. . . . . . . . . . 11 ⊢ (((𝑊‘𝐼) ∈ (Base‘𝐺) ∧ (𝑊‘(𝐼 + 1)) ∈ (Base‘𝐺)) → ((𝑊‘𝐼)(+g‘𝐺)(𝑊‘(𝐼 + 1))) = ((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))))
94	87, 89, 93	syl2anc 595	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑊‘𝐼)(+g‘𝐺)(𝑊‘(𝐼 + 1))) = ((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))))
95	81, 92, 94	3eqtrd 2808	. . . . . . . . 9 ⊢ (𝜑 → (𝐺 Σg (𝑊 substr ⟨𝐼, (𝐼 + 2)⟩)) = ((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))))
96	95	adantr 485	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷)) → (𝐺 Σg (𝑊 substr ⟨𝐼, (𝐼 + 2)⟩)) = ((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))))
97		simpr 489	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷)) → ((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷))
98	19	symgid 19470	. . . . . . . . . . 11 ⊢ (𝐷 ∈ 𝑉 → ( I ↾ 𝐷) = (0g‘𝐺))
99	21, 98	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → ( I ↾ 𝐷) = (0g‘𝐺))
100		eqid 2769	. . . . . . . . . . 11 ⊢ (0g‘𝐺) = (0g‘𝐺)
101	100	gsum0 18741	. . . . . . . . . 10 ⊢ (𝐺 Σg ∅) = (0g‘𝐺)
102	99, 101	eqtr4di 2822	. . . . . . . . 9 ⊢ (𝜑 → ( I ↾ 𝐷) = (𝐺 Σg ∅))
103	102	adantr 485	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷)) → ( I ↾ 𝐷) = (𝐺 Σg ∅))
104	96, 97, 103	3eqtrd 2808	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷)) → (𝐺 Σg (𝑊 substr ⟨𝐼, (𝐼 + 2)⟩)) = (𝐺 Σg ∅))
105	60, 64, 69, 70, 71, 74, 76, 104	gsumspl 18902	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷)) → (𝐺 Σg (𝑊 splice ⟨𝐼, (𝐼 + 2), (𝑊 substr ⟨𝐼, (𝐼 + 2)⟩)⟩)) = (𝐺 Σg (𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩)))
106	22	adantr 485	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷)) → (𝐺 Σg 𝑊) = ( I ↾ 𝐷))
107	59, 105, 106	3eqtr3d 2812	. . . . 5 ⊢ ((𝜑 ∧ ((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷)) → (𝐺 Σg (𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩)) = ( I ↾ 𝐷))
108		fveqeq2 6891	. . . . . . 7 ⊢ (𝑥 = (𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩) → ((♯‘𝑥) = (𝐿 − 2) ↔ (♯‘(𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩)) = (𝐿 − 2)))
109		oveq2 7419	. . . . . . . 8 ⊢ (𝑥 = (𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩) → (𝐺 Σg 𝑥) = (𝐺 Σg (𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩)))
110	109	eqeq1d 2771	. . . . . . 7 ⊢ (𝑥 = (𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩) → ((𝐺 Σg 𝑥) = ( I ↾ 𝐷) ↔ (𝐺 Σg (𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩)) = ( I ↾ 𝐷)))
111	108, 110	anbi12d 643	. . . . . 6 ⊢ (𝑥 = (𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩) → (((♯‘𝑥) = (𝐿 − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)) ↔ ((♯‘(𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩)) = (𝐿 − 2) ∧ (𝐺 Σg (𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩)) = ( I ↾ 𝐷))))
112	111	rspcev 3590	. . . . 5 ⊢ (((𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩) ∈ Word 𝑇 ∧ ((♯‘(𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩)) = (𝐿 − 2) ∧ (𝐺 Σg (𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩)) = ( I ↾ 𝐷))) → ∃𝑥 ∈ Word 𝑇((♯‘𝑥) = (𝐿 − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)))
113	5, 55, 107, 112	syl12anc 849	. . . 4 ⊢ ((𝜑 ∧ ((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷)) → ∃𝑥 ∈ Word 𝑇((♯‘𝑥) = (𝐿 − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)))
114		psgnunilem2.in	. . . . 5 ⊢ (𝜑 → ¬ ∃𝑥 ∈ Word 𝑇((♯‘𝑥) = (𝐿 − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)))
115	114	adantr 485	. . . 4 ⊢ ((𝜑 ∧ ((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷)) → ¬ ∃𝑥 ∈ Word 𝑇((♯‘𝑥) = (𝐿 − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)))
116	113, 115	pm2.21dd 198	. . 3 ⊢ ((𝜑 ∧ ((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷)) → ∃𝑤 ∈ Word 𝑇(((𝐺 Σg 𝑤) = ( I ↾ 𝐷) ∧ (♯‘𝑤) = 𝐿) ∧ ((𝐼 + 1) ∈ (0..^𝐿) ∧ 𝐴 ∈ dom ((𝑤‘(𝐼 + 1)) ∖ I ) ∧ ∀𝑗 ∈ (0..^(𝐼 + 1)) ¬ 𝐴 ∈ dom ((𝑤‘𝑗) ∖ I ))))
117	116	ex 417	. 2 ⊢ (𝜑 → (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷) → ∃𝑤 ∈ Word 𝑇(((𝐺 Σg 𝑤) = ( I ↾ 𝐷) ∧ (♯‘𝑤) = 𝐿) ∧ ((𝐼 + 1) ∈ (0..^𝐿) ∧ 𝐴 ∈ dom ((𝑤‘(𝐼 + 1)) ∖ I ) ∧ ∀𝑗 ∈ (0..^(𝐼 + 1)) ¬ 𝐴 ∈ dom ((𝑤‘𝑗) ∖ I )))))
118	1	adantr 485	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → 𝑊 ∈ Word 𝑇)
119		simprl 782	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → 𝑟 ∈ 𝑇)
120		simprr 784	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → 𝑠 ∈ 𝑇)
121	119, 120	s2cld 14907	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → ⟨“𝑟𝑠”⟩ ∈ Word 𝑇)
122		splcl 14788	. . . . . . 7 ⊢ ((𝑊 ∈ Word 𝑇 ∧ ⟨“𝑟𝑠”⟩ ∈ Word 𝑇) → (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩) ∈ Word 𝑇)
123	118, 121, 122	syl2anc 595	. . . . . 6 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩) ∈ Word 𝑇)
124	123	adantrr 729	. . . . 5 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩) ∈ Word 𝑇)
125	63	adantr 485	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → 𝐺 ∈ Mnd)
126	68	adantr 485	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → 𝑊 ∈ Word (Base‘𝐺))
127	18	adantr 485	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → 𝐼 ∈ (0...(𝐼 + 2)))
128	36	adantr 485	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → (𝐼 + 2) ∈ (0...(♯‘𝑊)))
129	67, 121	sselid 3943	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → ⟨“𝑟𝑠”⟩ ∈ Word (Base‘𝐺))
130	129	adantrr 729	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → ⟨“𝑟𝑠”⟩ ∈ Word (Base‘𝐺))
131	73	adantr 485	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → (𝑊 substr ⟨𝐼, (𝐼 + 2)⟩) ∈ Word (Base‘𝐺))
132		simprr1 1238	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → ((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠))
133	95	adantr 485	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → (𝐺 Σg (𝑊 substr ⟨𝐼, (𝐼 + 2)⟩)) = ((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))))
134	63	adantr 485	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → 𝐺 ∈ Mnd)
135	65	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑇 ⊆ (Base‘𝐺))
136	135	sselda 3945	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑟 ∈ 𝑇) → 𝑟 ∈ (Base‘𝐺))
137	136	adantrr 729	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → 𝑟 ∈ (Base‘𝐺))
138	135	sselda 3945	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝑇) → 𝑠 ∈ (Base‘𝐺))
139	138	adantrl 728	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → 𝑠 ∈ (Base‘𝐺))
140	60, 90	gsumws2 18900	. . . . . . . . . . . 12 ⊢ ((𝐺 ∈ Mnd ∧ 𝑟 ∈ (Base‘𝐺) ∧ 𝑠 ∈ (Base‘𝐺)) → (𝐺 Σg ⟨“𝑟𝑠”⟩) = (𝑟(+g‘𝐺)𝑠))
141	134, 137, 139, 140	syl3anc 1396	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → (𝐺 Σg ⟨“𝑟𝑠”⟩) = (𝑟(+g‘𝐺)𝑠))
142	19, 60, 90	symgov 19453	. . . . . . . . . . . 12 ⊢ ((𝑟 ∈ (Base‘𝐺) ∧ 𝑠 ∈ (Base‘𝐺)) → (𝑟(+g‘𝐺)𝑠) = (𝑟 ∘ 𝑠))
143	137, 139, 142	syl2anc 595	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → (𝑟(+g‘𝐺)𝑠) = (𝑟 ∘ 𝑠))
144	141, 143	eqtrd 2804	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → (𝐺 Σg ⟨“𝑟𝑠”⟩) = (𝑟 ∘ 𝑠))
145	144	adantrr 729	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → (𝐺 Σg ⟨“𝑟𝑠”⟩) = (𝑟 ∘ 𝑠))
146	132, 133, 145	3eqtr4rd 2815	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → (𝐺 Σg ⟨“𝑟𝑠”⟩) = (𝐺 Σg (𝑊 substr ⟨𝐼, (𝐼 + 2)⟩)))
147	60, 125, 126, 127, 128, 130, 131, 146	gsumspl 18902	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → (𝐺 Σg (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)) = (𝐺 Σg (𝑊 splice ⟨𝐼, (𝐼 + 2), (𝑊 substr ⟨𝐼, (𝐼 + 2)⟩)⟩)))
148	58	adantr 485	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → (𝐺 Σg (𝑊 splice ⟨𝐼, (𝐼 + 2), (𝑊 substr ⟨𝐼, (𝐼 + 2)⟩)⟩)) = (𝐺 Σg 𝑊))
149	22	adantr 485	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → (𝐺 Σg 𝑊) = ( I ↾ 𝐷))
150	147, 148, 149	3eqtrd 2808	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → (𝐺 Σg (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)) = ( I ↾ 𝐷))
151	18	adantr 485	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → 𝐼 ∈ (0...(𝐼 + 2)))
152	36	adantr 485	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → (𝐼 + 2) ∈ (0...(♯‘𝑊)))
153	118, 151, 152, 121	spllen 14790	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → (♯‘(𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)) = ((♯‘𝑊) + ((♯‘⟨“𝑟𝑠”⟩) − ((𝐼 + 2) − 𝐼))))
154		s2len 14925	. . . . . . . . . . . . 13 ⊢ (♯‘⟨“𝑟𝑠”⟩) = 2
155	154	oveq1i 7421	. . . . . . . . . . . 12 ⊢ ((♯‘⟨“𝑟𝑠”⟩) − ((𝐼 + 2) − 𝐼)) = (2 − ((𝐼 + 2) − 𝐼))
156	45	oveq2d 7427	. . . . . . . . . . . . 13 ⊢ (𝜑 → (2 − ((𝐼 + 2) − 𝐼)) = (2 − 2))
157	43	subidi 11528	. . . . . . . . . . . . 13 ⊢ (2 − 2) = 0
158	156, 157	eqtrdi 2820	. . . . . . . . . . . 12 ⊢ (𝜑 → (2 − ((𝐼 + 2) − 𝐼)) = 0)
159	155, 158	eqtrid 2816	. . . . . . . . . . 11 ⊢ (𝜑 → ((♯‘⟨“𝑟𝑠”⟩) − ((𝐼 + 2) − 𝐼)) = 0)
160	159	oveq2d 7427	. . . . . . . . . 10 ⊢ (𝜑 → ((♯‘𝑊) + ((♯‘⟨“𝑟𝑠”⟩) − ((𝐼 + 2) − 𝐼))) = ((♯‘𝑊) + 0))
161	23, 51	eqeltrd 2869	. . . . . . . . . . 11 ⊢ (𝜑 → (♯‘𝑊) ∈ ℂ)
162	161	addridd 11409	. . . . . . . . . 10 ⊢ (𝜑 → ((♯‘𝑊) + 0) = (♯‘𝑊))
163	160, 162, 23	3eqtrd 2808	. . . . . . . . 9 ⊢ (𝜑 → ((♯‘𝑊) + ((♯‘⟨“𝑟𝑠”⟩) − ((𝐼 + 2) − 𝐼))) = 𝐿)
164	163	adantr 485	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → ((♯‘𝑊) + ((♯‘⟨“𝑟𝑠”⟩) − ((𝐼 + 2) − 𝐼))) = 𝐿)
165	153, 164	eqtrd 2804	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → (♯‘(𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)) = 𝐿)
166	165	adantrr 729	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → (♯‘(𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)) = 𝐿)
167	150, 166	jca 520	. . . . 5 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → ((𝐺 Σg (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)) = ( I ↾ 𝐷) ∧ (♯‘(𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)) = 𝐿))
168	26	adantr 485	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → (𝐼 + 1) ∈ (0..^𝐿))
169		simprr2 1239	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → 𝐴 ∈ dom (𝑠 ∖ I ))
170		1nn0 12519	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ ℕ0
171		2nn 12313	. . . . . . . . . . . . . . 15 ⊢ 2 ∈ ℕ
172		1lt2 12412	. . . . . . . . . . . . . . 15 ⊢ 1 < 2
173		elfzo0 13728	. . . . . . . . . . . . . . 15 ⊢ (1 ∈ (0..^2) ↔ (1 ∈ ℕ0 ∧ 2 ∈ ℕ ∧ 1 < 2))
174	170, 171, 172, 173	mpbir3an 1358	. . . . . . . . . . . . . 14 ⊢ 1 ∈ (0..^2)
175	154	oveq2i 7422	. . . . . . . . . . . . . 14 ⊢ (0..^(♯‘⟨“𝑟𝑠”⟩)) = (0..^2)
176	174, 175	eleqtrri 2868	. . . . . . . . . . . . 13 ⊢ 1 ∈ (0..^(♯‘⟨“𝑟𝑠”⟩))
177	176	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → 1 ∈ (0..^(♯‘⟨“𝑟𝑠”⟩)))
178	118, 151, 152, 121, 177	splfv2a 14792	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → ((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘(𝐼 + 1)) = (⟨“𝑟𝑠”⟩‘1))
179		s2fv1 14924	. . . . . . . . . . . 12 ⊢ (𝑠 ∈ 𝑇 → (⟨“𝑟𝑠”⟩‘1) = 𝑠)
180	179	ad2antll 741	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → (⟨“𝑟𝑠”⟩‘1) = 𝑠)
181	178, 180	eqtrd 2804	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → ((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘(𝐼 + 1)) = 𝑠)
182	181	adantrr 729	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → ((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘(𝐼 + 1)) = 𝑠)
183	182	difeq1d 4088	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘(𝐼 + 1)) ∖ I ) = (𝑠 ∖ I ))
184	183	dmeqd 5896	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘(𝐼 + 1)) ∖ I ) = dom (𝑠 ∖ I ))
185	169, 184	eleqtrrd 2872	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → 𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘(𝐼 + 1)) ∖ I ))
186		fzosplitsni 13807	. . . . . . . . . . 11 ⊢ (𝐼 ∈ (ℤ≥‘0) → (𝑗 ∈ (0..^(𝐼 + 1)) ↔ (𝑗 ∈ (0..^𝐼) ∨ 𝑗 = 𝐼)))
187		nn0uz 12899	. . . . . . . . . . 11 ⊢ ℕ0 = (ℤ≥‘0)
188	186, 187	eleq2s 2887	. . . . . . . . . 10 ⊢ (𝐼 ∈ ℕ0 → (𝑗 ∈ (0..^(𝐼 + 1)) ↔ (𝑗 ∈ (0..^𝐼) ∨ 𝑗 = 𝐼)))
189	10, 188	syl 18	. . . . . . . . 9 ⊢ (𝜑 → (𝑗 ∈ (0..^(𝐼 + 1)) ↔ (𝑗 ∈ (0..^𝐼) ∨ 𝑗 = 𝐼)))
190	189	adantr 485	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → (𝑗 ∈ (0..^(𝐼 + 1)) ↔ (𝑗 ∈ (0..^𝐼) ∨ 𝑗 = 𝐼)))
191		fveq2 6882	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 𝑗 → (𝑊‘𝑘) = (𝑊‘𝑗))
192	191	difeq1d 4088	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 𝑗 → ((𝑊‘𝑘) ∖ I ) = ((𝑊‘𝑗) ∖ I ))
193	192	dmeqd 5896	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 𝑗 → dom ((𝑊‘𝑘) ∖ I ) = dom ((𝑊‘𝑗) ∖ I ))
194	193	eleq2d 2855	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 𝑗 → (𝐴 ∈ dom ((𝑊‘𝑘) ∖ I ) ↔ 𝐴 ∈ dom ((𝑊‘𝑗) ∖ I )))
195	194	notbid 321	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑗 → (¬ 𝐴 ∈ dom ((𝑊‘𝑘) ∖ I ) ↔ ¬ 𝐴 ∈ dom ((𝑊‘𝑗) ∖ I )))
196	195	rspccva 3589	. . . . . . . . . . . . . 14 ⊢ ((∀𝑘 ∈ (0..^𝐼) ¬ 𝐴 ∈ dom ((𝑊‘𝑘) ∖ I ) ∧ 𝑗 ∈ (0..^𝐼)) → ¬ 𝐴 ∈ dom ((𝑊‘𝑗) ∖ I ))
197	25, 196	sylan 591	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝐼)) → ¬ 𝐴 ∈ dom ((𝑊‘𝑗) ∖ I ))
198	197	adantlr 727	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) ∧ 𝑗 ∈ (0..^𝐼)) → ¬ 𝐴 ∈ dom ((𝑊‘𝑗) ∖ I ))
199	1	ad2antrr 738	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) ∧ 𝑗 ∈ (0..^𝐼)) → 𝑊 ∈ Word 𝑇)
200	18	ad2antrr 738	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) ∧ 𝑗 ∈ (0..^𝐼)) → 𝐼 ∈ (0...(𝐼 + 2)))
201	36	ad2antrr 738	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) ∧ 𝑗 ∈ (0..^𝐼)) → (𝐼 + 2) ∈ (0...(♯‘𝑊)))
202	121	adantr 485	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) ∧ 𝑗 ∈ (0..^𝐼)) → ⟨“𝑟𝑠”⟩ ∈ Word 𝑇)
203		simpr 489	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) ∧ 𝑗 ∈ (0..^𝐼)) → 𝑗 ∈ (0..^𝐼))
204	199, 200, 201, 202, 203	splfv1 14791	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) ∧ 𝑗 ∈ (0..^𝐼)) → ((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) = (𝑊‘𝑗))
205	204	difeq1d 4088	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) ∧ 𝑗 ∈ (0..^𝐼)) → (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) ∖ I ) = ((𝑊‘𝑗) ∖ I ))
206	205	dmeqd 5896	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) ∧ 𝑗 ∈ (0..^𝐼)) → dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) ∖ I ) = dom ((𝑊‘𝑗) ∖ I ))
207	198, 206	neleqtrrd 2892	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) ∧ 𝑗 ∈ (0..^𝐼)) → ¬ 𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) ∖ I ))
208	207	ex 417	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → (𝑗 ∈ (0..^𝐼) → ¬ 𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) ∖ I )))
209	208	adantrr 729	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → (𝑗 ∈ (0..^𝐼) → ¬ 𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) ∖ I )))
210		simprr3 1240	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → ¬ 𝐴 ∈ dom (𝑟 ∖ I ))
211		0nn0 12518	. . . . . . . . . . . . . . . . . . . 20 ⊢ 0 ∈ ℕ0
212		2pos 12344	. . . . . . . . . . . . . . . . . . . 20 ⊢ 0 < 2
213		elfzo0 13728	. . . . . . . . . . . . . . . . . . . 20 ⊢ (0 ∈ (0..^2) ↔ (0 ∈ ℕ0 ∧ 2 ∈ ℕ ∧ 0 < 2))
214	211, 171, 212, 213	mpbir3an 1358	. . . . . . . . . . . . . . . . . . 19 ⊢ 0 ∈ (0..^2)
215	214, 175	eleqtrri 2868	. . . . . . . . . . . . . . . . . 18 ⊢ 0 ∈ (0..^(♯‘⟨“𝑟𝑠”⟩))
216	215	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → 0 ∈ (0..^(♯‘⟨“𝑟𝑠”⟩)))
217	118, 151, 152, 121, 216	splfv2a 14792	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → ((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘(𝐼 + 0)) = (⟨“𝑟𝑠”⟩‘0))
218	31	addridd 11409	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐼 + 0) = 𝐼)
219	218	adantr 485	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → (𝐼 + 0) = 𝐼)
220	219	fveq2d 6886	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → ((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘(𝐼 + 0)) = ((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝐼))
221		s2fv0 14923	. . . . . . . . . . . . . . . . 17 ⊢ (𝑟 ∈ 𝑇 → (⟨“𝑟𝑠”⟩‘0) = 𝑟)
222	221	ad2antrl 740	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → (⟨“𝑟𝑠”⟩‘0) = 𝑟)
223	217, 220, 222	3eqtr3d 2812	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → ((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝐼) = 𝑟)
224	223	difeq1d 4088	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝐼) ∖ I ) = (𝑟 ∖ I ))
225	224	dmeqd 5896	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝐼) ∖ I ) = dom (𝑟 ∖ I ))
226	225	eleq2d 2855	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → (𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝐼) ∖ I ) ↔ 𝐴 ∈ dom (𝑟 ∖ I )))
227	226	adantrr 729	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → (𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝐼) ∖ I ) ↔ 𝐴 ∈ dom (𝑟 ∖ I )))
228	210, 227	mtbird 328	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → ¬ 𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝐼) ∖ I ))
229		fveq2 6882	. . . . . . . . . . . . . 14 ⊢ (𝑗 = 𝐼 → ((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) = ((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝐼))
230	229	difeq1d 4088	. . . . . . . . . . . . 13 ⊢ (𝑗 = 𝐼 → (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) ∖ I ) = (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝐼) ∖ I ))
231	230	dmeqd 5896	. . . . . . . . . . . 12 ⊢ (𝑗 = 𝐼 → dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) ∖ I ) = dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝐼) ∖ I ))
232	231	eleq2d 2855	. . . . . . . . . . 11 ⊢ (𝑗 = 𝐼 → (𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) ∖ I ) ↔ 𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝐼) ∖ I )))
233	232	notbid 321	. . . . . . . . . 10 ⊢ (𝑗 = 𝐼 → (¬ 𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) ∖ I ) ↔ ¬ 𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝐼) ∖ I )))
234	228, 233	syl5ibrcom 250	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → (𝑗 = 𝐼 → ¬ 𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) ∖ I )))
235	209, 234	jaod 872	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → ((𝑗 ∈ (0..^𝐼) ∨ 𝑗 = 𝐼) → ¬ 𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) ∖ I )))
236	190, 235	sylbid 243	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → (𝑗 ∈ (0..^(𝐼 + 1)) → ¬ 𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) ∖ I )))
237	236	ralrimiv 3162	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → ∀𝑗 ∈ (0..^(𝐼 + 1)) ¬ 𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) ∖ I ))
238	168, 185, 237	3jca 1144	. . . . 5 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → ((𝐼 + 1) ∈ (0..^𝐿) ∧ 𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘(𝐼 + 1)) ∖ I ) ∧ ∀𝑗 ∈ (0..^(𝐼 + 1)) ¬ 𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) ∖ I )))
239		oveq2 7419	. . . . . . . . 9 ⊢ (𝑤 = (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩) → (𝐺 Σg 𝑤) = (𝐺 Σg (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)))
240	239	eqeq1d 2771	. . . . . . . 8 ⊢ (𝑤 = (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩) → ((𝐺 Σg 𝑤) = ( I ↾ 𝐷) ↔ (𝐺 Σg (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)) = ( I ↾ 𝐷)))
241		fveqeq2 6891	. . . . . . . 8 ⊢ (𝑤 = (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩) → ((♯‘𝑤) = 𝐿 ↔ (♯‘(𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)) = 𝐿))
242	240, 241	anbi12d 643	. . . . . . 7 ⊢ (𝑤 = (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩) → (((𝐺 Σg 𝑤) = ( I ↾ 𝐷) ∧ (♯‘𝑤) = 𝐿) ↔ ((𝐺 Σg (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)) = ( I ↾ 𝐷) ∧ (♯‘(𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)) = 𝐿)))
243		fveq1 6881	. . . . . . . . . . 11 ⊢ (𝑤 = (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩) → (𝑤‘(𝐼 + 1)) = ((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘(𝐼 + 1)))
244	243	difeq1d 4088	. . . . . . . . . 10 ⊢ (𝑤 = (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩) → ((𝑤‘(𝐼 + 1)) ∖ I ) = (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘(𝐼 + 1)) ∖ I ))
245	244	dmeqd 5896	. . . . . . . . 9 ⊢ (𝑤 = (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩) → dom ((𝑤‘(𝐼 + 1)) ∖ I ) = dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘(𝐼 + 1)) ∖ I ))
246	245	eleq2d 2855	. . . . . . . 8 ⊢ (𝑤 = (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩) → (𝐴 ∈ dom ((𝑤‘(𝐼 + 1)) ∖ I ) ↔ 𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘(𝐼 + 1)) ∖ I )))
247		fveq1 6881	. . . . . . . . . . . . 13 ⊢ (𝑤 = (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩) → (𝑤‘𝑗) = ((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗))
248	247	difeq1d 4088	. . . . . . . . . . . 12 ⊢ (𝑤 = (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩) → ((𝑤‘𝑗) ∖ I ) = (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) ∖ I ))
249	248	dmeqd 5896	. . . . . . . . . . 11 ⊢ (𝑤 = (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩) → dom ((𝑤‘𝑗) ∖ I ) = dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) ∖ I ))
250	249	eleq2d 2855	. . . . . . . . . 10 ⊢ (𝑤 = (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩) → (𝐴 ∈ dom ((𝑤‘𝑗) ∖ I ) ↔ 𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) ∖ I )))
251	250	notbid 321	. . . . . . . . 9 ⊢ (𝑤 = (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩) → (¬ 𝐴 ∈ dom ((𝑤‘𝑗) ∖ I ) ↔ ¬ 𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) ∖ I )))
252	251	ralbidv 3194	. . . . . . . 8 ⊢ (𝑤 = (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩) → (∀𝑗 ∈ (0..^(𝐼 + 1)) ¬ 𝐴 ∈ dom ((𝑤‘𝑗) ∖ I ) ↔ ∀𝑗 ∈ (0..^(𝐼 + 1)) ¬ 𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) ∖ I )))
253	246, 252	3anbi23d 1465	. . . . . . 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 643	. . . . . 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 3590	. . . . 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 849	. . . 4 ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇) ∧ (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → ∃𝑤 ∈ Word 𝑇(((𝐺 Σg 𝑤) = ( I ↾ 𝐷) ∧ (♯‘𝑤) = 𝐿) ∧ ((𝐼 + 1) ∈ (0..^𝐿) ∧ 𝐴 ∈ dom ((𝑤‘(𝐼 + 1)) ∖ I ) ∧ ∀𝑗 ∈ (0..^(𝐼 + 1)) ¬ 𝐴 ∈ dom ((𝑤‘𝑗) ∖ I ))))
257	256	expr 461	. . 3 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑠 ∈ 𝑇)) → ((((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )) → ∃𝑤 ∈ Word 𝑇(((𝐺 Σg 𝑤) = ( I ↾ 𝐷) ∧ (♯‘𝑤) = 𝐿) ∧ ((𝐼 + 1) ∈ (0..^𝐿) ∧ 𝐴 ∈ dom ((𝑤‘(𝐼 + 1)) ∖ I ) ∧ ∀𝑗 ∈ (0..^(𝐼 + 1)) ¬ 𝐴 ∈ dom ((𝑤‘𝑗) ∖ I )))))
258	257	rexlimdvva 3228	. 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 19562	. 2 ⊢ (𝜑 → (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷) ∨ ∃𝑟 ∈ 𝑇 ∃𝑠 ∈ 𝑇 (((𝑊‘𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I ))))
260	117, 258, 259	mpjaod 873	1 ⊢ (𝜑 → ∃𝑤 ∈ Word 𝑇(((𝐺 Σg 𝑤) = ( I ↾ 𝐷) ∧ (♯‘𝑤) = 𝐿) ∧ ((𝐼 + 1) ∈ (0..^𝐿) ∧ 𝐴 ∈ dom ((𝑤‘(𝐼 + 1)) ∖ I ) ∧ ∀𝑗 ∈ (0..^(𝐼 + 1)) ¬ 𝐴 ∈ dom ((𝑤‘𝑗) ∖ I ))))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 400   ∨ wo 860   ∧ w3a 1101   = wceq 1567   ∈ wcel 2149  ∀wral 3085  ∃wrex 3095   ∖ cdif 3910   ⊆ wss 3913  ∅c0 4294  ⟨cop 4600  ⟨cotp 4602   class class class wbr 5113   I cid 5556  dom cdm 5662  ran crn 5663   ↾ cres 5664   ∘ ccom 5666  ⟶wf 6533  ‘cfv 6537  (class class class)co 7411  ℂcc 11097  ℝcr 11098  0cc0 11099  1c1 11100   + caddc 11102   < clt 11242   ≤ cle 11243   − cmin 11440  -cneg 11441  ℕcn 12232  2c2 12294  ℕ₀cn0 12503  ℤcz 12590  ℤ_≥cuz 12861  ...cfz 13534  ..^cfzo 13681  ♯chash 14365  Word cword 14549   substr csubstr 14677   splice csplice 14785  ⟨“cs2 14877  Basecbs 17268  +_gcplusg 17309  0_gc0g 17491   Σ_g cgsu 17492  Mndcmnd 18791  Grpcgrp 18999  SymGrpcsymg 19438  pmTrspcpmtr 19510

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-rep 5242  ax-sep 5261  ax-nul 5271  ax-pow 5337  ax-pr 5405  ax-un 7733  ax-cnex 11155  ax-resscn 11156  ax-1cn 11157  ax-icn 11158  ax-addcl 11159  ax-addrcl 11160  ax-mulcl 11161  ax-mulrcl 11162  ax-mulcom 11163  ax-addass 11164  ax-mulass 11165  ax-distr 11166  ax-i2m1 11167  ax-1ne0 11168  ax-1rid 11169  ax-rnegex 11170  ax-rrecex 11171  ax-cnre 11172  ax-pre-lttri 11173  ax-pre-lttrn 11174  ax-pre-ltadd 11175  ax-pre-mulgt0 11176

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-xor 1539  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-nel 3071  df-ral 3086  df-rex 3096  df-rmo 3376  df-reu 3377  df-rab 3424  df-v 3465  df-sbc 3754  df-csb 3862  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-pss 3933  df-nul 4295  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-tp 4599  df-op 4601  df-ot 4603  df-uni 4877  df-int 4917  df-iun 4962  df-br 5114  df-opab 5178  df-mpt 5197  df-tr 5223  df-id 5557  df-eprel 5562  df-po 5570  df-so 5571  df-fr 5615  df-we 5617  df-xp 5668  df-rel 5669  df-cnv 5670  df-co 5671  df-dm 5672  df-rn 5673  df-res 5674  df-ima 5675  df-pred 6303  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-riota 7368  df-ov 7414  df-oprab 7415  df-mpo 7416  df-om 7862  df-1st 7985  df-2nd 7986  df-frecs 8277  df-wrecs 8308  df-recs 8357  df-rdg 8396  df-1o 8452  df-2o 8453  df-er 8693  df-map 8825  df-en 8943  df-dom 8944  df-sdom 8945  df-fin 8946  df-card 9924  df-pnf 11244  df-mnf 11245  df-xr 11246  df-ltxr 11247  df-le 11248  df-sub 11442  df-neg 11443  df-nn 12233  df-2 12302  df-3 12303  df-4 12304  df-5 12305  df-6 12306  df-7 12307  df-8 12308  df-9 12309  df-n0 12504  df-xnn0 12577  df-z 12591  df-uz 12862  df-fz 13535  df-fzo 13682  df-seq 14037  df-hash 14366  df-word 14550  df-lsw 14599  df-concat 14607  df-s1 14633  df-substr 14678  df-pfx 14708  df-splice 14786  df-s2 14884  df-struct 17206  df-sets 17223  df-slot 17241  df-ndx 17253  df-base 17269  df-ress 17290  df-plusg 17322  df-tset 17328  df-0g 17493  df-gsum 17494  df-mgm 18697  df-sgrp 18776  df-mnd 18792  df-submnd 18841  df-efmnd 18927  df-grp 19002  df-minusg 19003  df-subg 19188  df-symg 19439  df-pmtr 19511

This theorem is referenced by:  psgnunilem3  19565