MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  psgnunilem2 Structured version   Visualization version   GIF version

Theorem psgnunilem2 17961
Description: Lemma for psgnuni 17965. 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.
StepHypRef Expression
1 psgnunilem2.w . . . . . . 7 (𝜑𝑊 ∈ Word 𝑇)
2 wrd0 13362 . . . . . . 7 ∅ ∈ Word 𝑇
3 splcl 13549 . . . . . . 7 ((𝑊 ∈ Word 𝑇 ∧ ∅ ∈ Word 𝑇) → (𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩) ∈ Word 𝑇)
41, 2, 3sylancl 695 . . . . . 6 (𝜑 → (𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩) ∈ Word 𝑇)
54adantr 480 . . . . 5 ((𝜑 ∧ ((𝑊𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷)) → (𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩) ∈ Word 𝑇)
6 fzossfz 12527 . . . . . . . . . . 11 (0..^𝐿) ⊆ (0...𝐿)
7 psgnunilem2.ix . . . . . . . . . . 11 (𝜑𝐼 ∈ (0..^𝐿))
86, 7sseldi 3634 . . . . . . . . . 10 (𝜑𝐼 ∈ (0...𝐿))
9 elfznn0 12471 . . . . . . . . . 10 (𝐼 ∈ (0...𝐿) → 𝐼 ∈ ℕ0)
108, 9syl 17 . . . . . . . . 9 (𝜑𝐼 ∈ ℕ0)
11 2nn0 11347 . . . . . . . . . 10 2 ∈ ℕ0
12 nn0addcl 11366 . . . . . . . . . 10 ((𝐼 ∈ ℕ0 ∧ 2 ∈ ℕ0) → (𝐼 + 2) ∈ ℕ0)
1310, 11, 12sylancl 695 . . . . . . . . 9 (𝜑 → (𝐼 + 2) ∈ ℕ0)
1410nn0red 11390 . . . . . . . . . 10 (𝜑𝐼 ∈ ℝ)
15 nn0addge1 11377 . . . . . . . . . 10 ((𝐼 ∈ ℝ ∧ 2 ∈ ℕ0) → 𝐼 ≤ (𝐼 + 2))
1614, 11, 15sylancl 695 . . . . . . . . 9 (𝜑𝐼 ≤ (𝐼 + 2))
17 elfz2nn0 12469 . . . . . . . . 9 (𝐼 ∈ (0...(𝐼 + 2)) ↔ (𝐼 ∈ ℕ0 ∧ (𝐼 + 2) ∈ ℕ0𝐼 ≤ (𝐼 + 2)))
1810, 13, 16, 17syl3anbrc 1265 . . . . . . . 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 ))
2619, 20, 21, 1, 22, 23, 7, 24, 25psgnunilem5 17960 . . . . . . . . . 10 (𝜑 → (𝐼 + 1) ∈ (0..^𝐿))
27 fzofzp1 12605 . . . . . . . . . 10 ((𝐼 + 1) ∈ (0..^𝐿) → ((𝐼 + 1) + 1) ∈ (0...𝐿))
2826, 27syl 17 . . . . . . . . 9 (𝜑 → ((𝐼 + 1) + 1) ∈ (0...𝐿))
2910nn0cnd 11391 . . . . . . . . . . 11 (𝜑𝐼 ∈ ℂ)
30 1cnd 10094 . . . . . . . . . . 11 (𝜑 → 1 ∈ ℂ)
3129, 30, 30addassd 10100 . . . . . . . . . 10 (𝜑 → ((𝐼 + 1) + 1) = (𝐼 + (1 + 1)))
32 df-2 11117 . . . . . . . . . . 11 2 = (1 + 1)
3332oveq2i 6701 . . . . . . . . . 10 (𝐼 + 2) = (𝐼 + (1 + 1))
3431, 33syl6reqr 2704 . . . . . . . . 9 (𝜑 → (𝐼 + 2) = ((𝐼 + 1) + 1))
3523oveq2d 6706 . . . . . . . . 9 (𝜑 → (0...(#‘𝑊)) = (0...𝐿))
3628, 34, 353eltr4d 2745 . . . . . . . 8 (𝜑 → (𝐼 + 2) ∈ (0...(#‘𝑊)))
372a1i 11 . . . . . . . 8 (𝜑 → ∅ ∈ Word 𝑇)
381, 18, 36, 37spllen 13551 . . . . . . 7 (𝜑 → (#‘(𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩)) = ((#‘𝑊) + ((#‘∅) − ((𝐼 + 2) − 𝐼))))
39 hash0 13196 . . . . . . . . . . 11 (#‘∅) = 0
4039oveq1i 6700 . . . . . . . . . 10 ((#‘∅) − ((𝐼 + 2) − 𝐼)) = (0 − ((𝐼 + 2) − 𝐼))
41 df-neg 10307 . . . . . . . . . 10 -((𝐼 + 2) − 𝐼) = (0 − ((𝐼 + 2) − 𝐼))
4240, 41eqtr4i 2676 . . . . . . . . 9 ((#‘∅) − ((𝐼 + 2) − 𝐼)) = -((𝐼 + 2) − 𝐼)
43 2cn 11129 . . . . . . . . . . 11 2 ∈ ℂ
44 pncan2 10326 . . . . . . . . . . 11 ((𝐼 ∈ ℂ ∧ 2 ∈ ℂ) → ((𝐼 + 2) − 𝐼) = 2)
4529, 43, 44sylancl 695 . . . . . . . . . 10 (𝜑 → ((𝐼 + 2) − 𝐼) = 2)
4645negeqd 10313 . . . . . . . . 9 (𝜑 → -((𝐼 + 2) − 𝐼) = -2)
4742, 46syl5eq 2697 . . . . . . . 8 (𝜑 → ((#‘∅) − ((𝐼 + 2) − 𝐼)) = -2)
4823, 47oveq12d 6708 . . . . . . 7 (𝜑 → ((#‘𝑊) + ((#‘∅) − ((𝐼 + 2) − 𝐼))) = (𝐿 + -2))
49 elfzel2 12378 . . . . . . . . . 10 (𝐼 ∈ (0...𝐿) → 𝐿 ∈ ℤ)
508, 49syl 17 . . . . . . . . 9 (𝜑𝐿 ∈ ℤ)
5150zcnd 11521 . . . . . . . 8 (𝜑𝐿 ∈ ℂ)
52 negsub 10367 . . . . . . . 8 ((𝐿 ∈ ℂ ∧ 2 ∈ ℂ) → (𝐿 + -2) = (𝐿 − 2))
5351, 43, 52sylancl 695 . . . . . . 7 (𝜑 → (𝐿 + -2) = (𝐿 − 2))
5438, 48, 533eqtrd 2689 . . . . . 6 (𝜑 → (#‘(𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩)) = (𝐿 − 2))
5554adantr 480 . . . . 5 ((𝜑 ∧ ((𝑊𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷)) → (#‘(𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩)) = (𝐿 − 2))
56 splid 13550 . . . . . . . . 9 ((𝑊 ∈ Word 𝑇 ∧ (𝐼 ∈ (0...(𝐼 + 2)) ∧ (𝐼 + 2) ∈ (0...(#‘𝑊)))) → (𝑊 splice ⟨𝐼, (𝐼 + 2), (𝑊 substr ⟨𝐼, (𝐼 + 2)⟩)⟩) = 𝑊)
571, 18, 36, 56syl12anc 1364 . . . . . . . 8 (𝜑 → (𝑊 splice ⟨𝐼, (𝐼 + 2), (𝑊 substr ⟨𝐼, (𝐼 + 2)⟩)⟩) = 𝑊)
5857oveq2d 6706 . . . . . . 7 (𝜑 → (𝐺 Σg (𝑊 splice ⟨𝐼, (𝐼 + 2), (𝑊 substr ⟨𝐼, (𝐼 + 2)⟩)⟩)) = (𝐺 Σg 𝑊))
5958adantr 480 . . . . . 6 ((𝜑 ∧ ((𝑊𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷)) → (𝐺 Σg (𝑊 splice ⟨𝐼, (𝐼 + 2), (𝑊 substr ⟨𝐼, (𝐼 + 2)⟩)⟩)) = (𝐺 Σg 𝑊))
60 eqid 2651 . . . . . . 7 (Base‘𝐺) = (Base‘𝐺)
6119symggrp 17866 . . . . . . . . . 10 (𝐷𝑉𝐺 ∈ Grp)
6221, 61syl 17 . . . . . . . . 9 (𝜑𝐺 ∈ Grp)
63 grpmnd 17476 . . . . . . . . 9 (𝐺 ∈ Grp → 𝐺 ∈ Mnd)
6462, 63syl 17 . . . . . . . 8 (𝜑𝐺 ∈ Mnd)
6564adantr 480 . . . . . . 7 ((𝜑 ∧ ((𝑊𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷)) → 𝐺 ∈ Mnd)
6620, 19, 60symgtrf 17935 . . . . . . . . . 10 𝑇 ⊆ (Base‘𝐺)
67 sswrd 13345 . . . . . . . . . 10 (𝑇 ⊆ (Base‘𝐺) → Word 𝑇 ⊆ Word (Base‘𝐺))
6866, 67ax-mp 5 . . . . . . . . 9 Word 𝑇 ⊆ Word (Base‘𝐺)
6968, 1sseldi 3634 . . . . . . . 8 (𝜑𝑊 ∈ Word (Base‘𝐺))
7069adantr 480 . . . . . . 7 ((𝜑 ∧ ((𝑊𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷)) → 𝑊 ∈ Word (Base‘𝐺))
7118adantr 480 . . . . . . 7 ((𝜑 ∧ ((𝑊𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷)) → 𝐼 ∈ (0...(𝐼 + 2)))
7236adantr 480 . . . . . . 7 ((𝜑 ∧ ((𝑊𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷)) → (𝐼 + 2) ∈ (0...(#‘𝑊)))
73 swrdcl 13464 . . . . . . . . 9 (𝑊 ∈ Word (Base‘𝐺) → (𝑊 substr ⟨𝐼, (𝐼 + 2)⟩) ∈ Word (Base‘𝐺))
7469, 73syl 17 . . . . . . . 8 (𝜑 → (𝑊 substr ⟨𝐼, (𝐼 + 2)⟩) ∈ Word (Base‘𝐺))
7574adantr 480 . . . . . . 7 ((𝜑 ∧ ((𝑊𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷)) → (𝑊 substr ⟨𝐼, (𝐼 + 2)⟩) ∈ Word (Base‘𝐺))
76 wrd0 13362 . . . . . . . 8 ∅ ∈ Word (Base‘𝐺)
7776a1i 11 . . . . . . 7 ((𝜑 ∧ ((𝑊𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷)) → ∅ ∈ Word (Base‘𝐺))
7823oveq2d 6706 . . . . . . . . . . . . 13 (𝜑 → (0..^(#‘𝑊)) = (0..^𝐿))
7926, 78eleqtrrd 2733 . . . . . . . . . . . 12 (𝜑 → (𝐼 + 1) ∈ (0..^(#‘𝑊)))
80 swrds2 13731 . . . . . . . . . . . 12 ((𝑊 ∈ Word 𝑇𝐼 ∈ ℕ0 ∧ (𝐼 + 1) ∈ (0..^(#‘𝑊))) → (𝑊 substr ⟨𝐼, (𝐼 + 2)⟩) = ⟨“(𝑊𝐼)(𝑊‘(𝐼 + 1))”⟩)
811, 10, 79, 80syl3anc 1366 . . . . . . . . . . 11 (𝜑 → (𝑊 substr ⟨𝐼, (𝐼 + 2)⟩) = ⟨“(𝑊𝐼)(𝑊‘(𝐼 + 1))”⟩)
8281oveq2d 6706 . . . . . . . . . 10 (𝜑 → (𝐺 Σg (𝑊 substr ⟨𝐼, (𝐼 + 2)⟩)) = (𝐺 Σg ⟨“(𝑊𝐼)(𝑊‘(𝐼 + 1))”⟩))
83 wrdf 13342 . . . . . . . . . . . . . . 15 (𝑊 ∈ Word 𝑇𝑊:(0..^(#‘𝑊))⟶𝑇)
841, 83syl 17 . . . . . . . . . . . . . 14 (𝜑𝑊:(0..^(#‘𝑊))⟶𝑇)
8578feq2d 6069 . . . . . . . . . . . . . 14 (𝜑 → (𝑊:(0..^(#‘𝑊))⟶𝑇𝑊:(0..^𝐿)⟶𝑇))
8684, 85mpbid 222 . . . . . . . . . . . . 13 (𝜑𝑊:(0..^𝐿)⟶𝑇)
8786, 7ffvelrnd 6400 . . . . . . . . . . . 12 (𝜑 → (𝑊𝐼) ∈ 𝑇)
8866, 87sseldi 3634 . . . . . . . . . . 11 (𝜑 → (𝑊𝐼) ∈ (Base‘𝐺))
8986, 26ffvelrnd 6400 . . . . . . . . . . . 12 (𝜑 → (𝑊‘(𝐼 + 1)) ∈ 𝑇)
9066, 89sseldi 3634 . . . . . . . . . . 11 (𝜑 → (𝑊‘(𝐼 + 1)) ∈ (Base‘𝐺))
91 eqid 2651 . . . . . . . . . . . 12 (+g𝐺) = (+g𝐺)
9260, 91gsumws2 17426 . . . . . . . . . . 11 ((𝐺 ∈ Mnd ∧ (𝑊𝐼) ∈ (Base‘𝐺) ∧ (𝑊‘(𝐼 + 1)) ∈ (Base‘𝐺)) → (𝐺 Σg ⟨“(𝑊𝐼)(𝑊‘(𝐼 + 1))”⟩) = ((𝑊𝐼)(+g𝐺)(𝑊‘(𝐼 + 1))))
9364, 88, 90, 92syl3anc 1366 . . . . . . . . . 10 (𝜑 → (𝐺 Σg ⟨“(𝑊𝐼)(𝑊‘(𝐼 + 1))”⟩) = ((𝑊𝐼)(+g𝐺)(𝑊‘(𝐼 + 1))))
9419, 60, 91symgov 17856 . . . . . . . . . . 11 (((𝑊𝐼) ∈ (Base‘𝐺) ∧ (𝑊‘(𝐼 + 1)) ∈ (Base‘𝐺)) → ((𝑊𝐼)(+g𝐺)(𝑊‘(𝐼 + 1))) = ((𝑊𝐼) ∘ (𝑊‘(𝐼 + 1))))
9588, 90, 94syl2anc 694 . . . . . . . . . 10 (𝜑 → ((𝑊𝐼)(+g𝐺)(𝑊‘(𝐼 + 1))) = ((𝑊𝐼) ∘ (𝑊‘(𝐼 + 1))))
9682, 93, 953eqtrd 2689 . . . . . . . . 9 (𝜑 → (𝐺 Σg (𝑊 substr ⟨𝐼, (𝐼 + 2)⟩)) = ((𝑊𝐼) ∘ (𝑊‘(𝐼 + 1))))
9796adantr 480 . . . . . . . 8 ((𝜑 ∧ ((𝑊𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷)) → (𝐺 Σg (𝑊 substr ⟨𝐼, (𝐼 + 2)⟩)) = ((𝑊𝐼) ∘ (𝑊‘(𝐼 + 1))))
98 simpr 476 . . . . . . . 8 ((𝜑 ∧ ((𝑊𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷)) → ((𝑊𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷))
9919symgid 17867 . . . . . . . . . . 11 (𝐷𝑉 → ( I ↾ 𝐷) = (0g𝐺))
10021, 99syl 17 . . . . . . . . . 10 (𝜑 → ( I ↾ 𝐷) = (0g𝐺))
101 eqid 2651 . . . . . . . . . . 11 (0g𝐺) = (0g𝐺)
102101gsum0 17325 . . . . . . . . . 10 (𝐺 Σg ∅) = (0g𝐺)
103100, 102syl6eqr 2703 . . . . . . . . 9 (𝜑 → ( I ↾ 𝐷) = (𝐺 Σg ∅))
104103adantr 480 . . . . . . . 8 ((𝜑 ∧ ((𝑊𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷)) → ( I ↾ 𝐷) = (𝐺 Σg ∅))
10597, 98, 1043eqtrd 2689 . . . . . . 7 ((𝜑 ∧ ((𝑊𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷)) → (𝐺 Σg (𝑊 substr ⟨𝐼, (𝐼 + 2)⟩)) = (𝐺 Σg ∅))
10660, 65, 70, 71, 72, 75, 77, 105gsumspl 17428 . . . . . 6 ((𝜑 ∧ ((𝑊𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷)) → (𝐺 Σg (𝑊 splice ⟨𝐼, (𝐼 + 2), (𝑊 substr ⟨𝐼, (𝐼 + 2)⟩)⟩)) = (𝐺 Σg (𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩)))
10722adantr 480 . . . . . 6 ((𝜑 ∧ ((𝑊𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷)) → (𝐺 Σg 𝑊) = ( I ↾ 𝐷))
10859, 106, 1073eqtr3d 2693 . . . . 5 ((𝜑 ∧ ((𝑊𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷)) → (𝐺 Σg (𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩)) = ( I ↾ 𝐷))
109 fveq2 6229 . . . . . . . 8 (𝑥 = (𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩) → (#‘𝑥) = (#‘(𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩)))
110109eqeq1d 2653 . . . . . . 7 (𝑥 = (𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩) → ((#‘𝑥) = (𝐿 − 2) ↔ (#‘(𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩)) = (𝐿 − 2)))
111 oveq2 6698 . . . . . . . 8 (𝑥 = (𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩) → (𝐺 Σg 𝑥) = (𝐺 Σg (𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩)))
112111eqeq1d 2653 . . . . . . 7 (𝑥 = (𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩) → ((𝐺 Σg 𝑥) = ( I ↾ 𝐷) ↔ (𝐺 Σg (𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩)) = ( I ↾ 𝐷)))
113110, 112anbi12d 747 . . . . . 6 (𝑥 = (𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩) → (((#‘𝑥) = (𝐿 − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)) ↔ ((#‘(𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩)) = (𝐿 − 2) ∧ (𝐺 Σg (𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩)) = ( I ↾ 𝐷))))
114113rspcev 3340 . . . . 5 (((𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩) ∈ Word 𝑇 ∧ ((#‘(𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩)) = (𝐿 − 2) ∧ (𝐺 Σg (𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩)) = ( I ↾ 𝐷))) → ∃𝑥 ∈ Word 𝑇((#‘𝑥) = (𝐿 − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)))
1155, 55, 108, 114syl12anc 1364 . . . 4 ((𝜑 ∧ ((𝑊𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷)) → ∃𝑥 ∈ Word 𝑇((#‘𝑥) = (𝐿 − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)))
116 psgnunilem2.in . . . . 5 (𝜑 → ¬ ∃𝑥 ∈ Word 𝑇((#‘𝑥) = (𝐿 − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)))
117116adantr 480 . . . 4 ((𝜑 ∧ ((𝑊𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷)) → ¬ ∃𝑥 ∈ Word 𝑇((#‘𝑥) = (𝐿 − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)))
118115, 117pm2.21dd 186 . . 3 ((𝜑 ∧ ((𝑊𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷)) → ∃𝑤 ∈ Word 𝑇(((𝐺 Σg 𝑤) = ( I ↾ 𝐷) ∧ (#‘𝑤) = 𝐿) ∧ ((𝐼 + 1) ∈ (0..^𝐿) ∧ 𝐴 ∈ dom ((𝑤‘(𝐼 + 1)) ∖ I ) ∧ ∀𝑗 ∈ (0..^(𝐼 + 1)) ¬ 𝐴 ∈ dom ((𝑤𝑗) ∖ I ))))
119118ex 449 . 2 (𝜑 → (((𝑊𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷) → ∃𝑤 ∈ Word 𝑇(((𝐺 Σg 𝑤) = ( I ↾ 𝐷) ∧ (#‘𝑤) = 𝐿) ∧ ((𝐼 + 1) ∈ (0..^𝐿) ∧ 𝐴 ∈ dom ((𝑤‘(𝐼 + 1)) ∖ I ) ∧ ∀𝑗 ∈ (0..^(𝐼 + 1)) ¬ 𝐴 ∈ dom ((𝑤𝑗) ∖ I )))))
1201adantr 480 . . . . . . 7 ((𝜑 ∧ (𝑟𝑇𝑠𝑇)) → 𝑊 ∈ Word 𝑇)
121 simprl 809 . . . . . . . 8 ((𝜑 ∧ (𝑟𝑇𝑠𝑇)) → 𝑟𝑇)
122 simprr 811 . . . . . . . 8 ((𝜑 ∧ (𝑟𝑇𝑠𝑇)) → 𝑠𝑇)
123121, 122s2cld 13662 . . . . . . 7 ((𝜑 ∧ (𝑟𝑇𝑠𝑇)) → ⟨“𝑟𝑠”⟩ ∈ Word 𝑇)
124 splcl 13549 . . . . . . 7 ((𝑊 ∈ Word 𝑇 ∧ ⟨“𝑟𝑠”⟩ ∈ Word 𝑇) → (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩) ∈ Word 𝑇)
125120, 123, 124syl2anc 694 . . . . . 6 ((𝜑 ∧ (𝑟𝑇𝑠𝑇)) → (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩) ∈ Word 𝑇)
126125adantrr 753 . . . . 5 ((𝜑 ∧ ((𝑟𝑇𝑠𝑇) ∧ (((𝑊𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩) ∈ Word 𝑇)
12764adantr 480 . . . . . . . 8 ((𝜑 ∧ ((𝑟𝑇𝑠𝑇) ∧ (((𝑊𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → 𝐺 ∈ Mnd)
12869adantr 480 . . . . . . . 8 ((𝜑 ∧ ((𝑟𝑇𝑠𝑇) ∧ (((𝑊𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → 𝑊 ∈ Word (Base‘𝐺))
12918adantr 480 . . . . . . . 8 ((𝜑 ∧ ((𝑟𝑇𝑠𝑇) ∧ (((𝑊𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → 𝐼 ∈ (0...(𝐼 + 2)))
13036adantr 480 . . . . . . . 8 ((𝜑 ∧ ((𝑟𝑇𝑠𝑇) ∧ (((𝑊𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → (𝐼 + 2) ∈ (0...(#‘𝑊)))
13168, 123sseldi 3634 . . . . . . . . 9 ((𝜑 ∧ (𝑟𝑇𝑠𝑇)) → ⟨“𝑟𝑠”⟩ ∈ Word (Base‘𝐺))
132131adantrr 753 . . . . . . . 8 ((𝜑 ∧ ((𝑟𝑇𝑠𝑇) ∧ (((𝑊𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → ⟨“𝑟𝑠”⟩ ∈ Word (Base‘𝐺))
13374adantr 480 . . . . . . . 8 ((𝜑 ∧ ((𝑟𝑇𝑠𝑇) ∧ (((𝑊𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → (𝑊 substr ⟨𝐼, (𝐼 + 2)⟩) ∈ Word (Base‘𝐺))
134 simprr1 1129 . . . . . . . . 9 ((𝜑 ∧ ((𝑟𝑇𝑠𝑇) ∧ (((𝑊𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → ((𝑊𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟𝑠))
13596adantr 480 . . . . . . . . 9 ((𝜑 ∧ ((𝑟𝑇𝑠𝑇) ∧ (((𝑊𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → (𝐺 Σg (𝑊 substr ⟨𝐼, (𝐼 + 2)⟩)) = ((𝑊𝐼) ∘ (𝑊‘(𝐼 + 1))))
13664adantr 480 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑟𝑇𝑠𝑇)) → 𝐺 ∈ Mnd)
13766a1i 11 . . . . . . . . . . . . . 14 (𝜑𝑇 ⊆ (Base‘𝐺))
138137sselda 3636 . . . . . . . . . . . . 13 ((𝜑𝑟𝑇) → 𝑟 ∈ (Base‘𝐺))
139138adantrr 753 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑟𝑇𝑠𝑇)) → 𝑟 ∈ (Base‘𝐺))
140137sselda 3636 . . . . . . . . . . . . 13 ((𝜑𝑠𝑇) → 𝑠 ∈ (Base‘𝐺))
141140adantrl 752 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑟𝑇𝑠𝑇)) → 𝑠 ∈ (Base‘𝐺))
14260, 91gsumws2 17426 . . . . . . . . . . . 12 ((𝐺 ∈ Mnd ∧ 𝑟 ∈ (Base‘𝐺) ∧ 𝑠 ∈ (Base‘𝐺)) → (𝐺 Σg ⟨“𝑟𝑠”⟩) = (𝑟(+g𝐺)𝑠))
143136, 139, 141, 142syl3anc 1366 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟𝑇𝑠𝑇)) → (𝐺 Σg ⟨“𝑟𝑠”⟩) = (𝑟(+g𝐺)𝑠))
14419, 60, 91symgov 17856 . . . . . . . . . . . 12 ((𝑟 ∈ (Base‘𝐺) ∧ 𝑠 ∈ (Base‘𝐺)) → (𝑟(+g𝐺)𝑠) = (𝑟𝑠))
145139, 141, 144syl2anc 694 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟𝑇𝑠𝑇)) → (𝑟(+g𝐺)𝑠) = (𝑟𝑠))
146143, 145eqtrd 2685 . . . . . . . . . 10 ((𝜑 ∧ (𝑟𝑇𝑠𝑇)) → (𝐺 Σg ⟨“𝑟𝑠”⟩) = (𝑟𝑠))
147146adantrr 753 . . . . . . . . 9 ((𝜑 ∧ ((𝑟𝑇𝑠𝑇) ∧ (((𝑊𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → (𝐺 Σg ⟨“𝑟𝑠”⟩) = (𝑟𝑠))
148134, 135, 1473eqtr4rd 2696 . . . . . . . 8 ((𝜑 ∧ ((𝑟𝑇𝑠𝑇) ∧ (((𝑊𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → (𝐺 Σg ⟨“𝑟𝑠”⟩) = (𝐺 Σg (𝑊 substr ⟨𝐼, (𝐼 + 2)⟩)))
14960, 127, 128, 129, 130, 132, 133, 148gsumspl 17428 . . . . . . 7 ((𝜑 ∧ ((𝑟𝑇𝑠𝑇) ∧ (((𝑊𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → (𝐺 Σg (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)) = (𝐺 Σg (𝑊 splice ⟨𝐼, (𝐼 + 2), (𝑊 substr ⟨𝐼, (𝐼 + 2)⟩)⟩)))
15058adantr 480 . . . . . . 7 ((𝜑 ∧ ((𝑟𝑇𝑠𝑇) ∧ (((𝑊𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → (𝐺 Σg (𝑊 splice ⟨𝐼, (𝐼 + 2), (𝑊 substr ⟨𝐼, (𝐼 + 2)⟩)⟩)) = (𝐺 Σg 𝑊))
15122adantr 480 . . . . . . 7 ((𝜑 ∧ ((𝑟𝑇𝑠𝑇) ∧ (((𝑊𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → (𝐺 Σg 𝑊) = ( I ↾ 𝐷))
152149, 150, 1513eqtrd 2689 . . . . . 6 ((𝜑 ∧ ((𝑟𝑇𝑠𝑇) ∧ (((𝑊𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → (𝐺 Σg (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)) = ( I ↾ 𝐷))
15318adantr 480 . . . . . . . . 9 ((𝜑 ∧ (𝑟𝑇𝑠𝑇)) → 𝐼 ∈ (0...(𝐼 + 2)))
15436adantr 480 . . . . . . . . 9 ((𝜑 ∧ (𝑟𝑇𝑠𝑇)) → (𝐼 + 2) ∈ (0...(#‘𝑊)))
155120, 153, 154, 123spllen 13551 . . . . . . . 8 ((𝜑 ∧ (𝑟𝑇𝑠𝑇)) → (#‘(𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)) = ((#‘𝑊) + ((#‘⟨“𝑟𝑠”⟩) − ((𝐼 + 2) − 𝐼))))
156 s2len 13680 . . . . . . . . . . . . 13 (#‘⟨“𝑟𝑠”⟩) = 2
157156oveq1i 6700 . . . . . . . . . . . 12 ((#‘⟨“𝑟𝑠”⟩) − ((𝐼 + 2) − 𝐼)) = (2 − ((𝐼 + 2) − 𝐼))
15845oveq2d 6706 . . . . . . . . . . . . 13 (𝜑 → (2 − ((𝐼 + 2) − 𝐼)) = (2 − 2))
15943subidi 10390 . . . . . . . . . . . . 13 (2 − 2) = 0
160158, 159syl6eq 2701 . . . . . . . . . . . 12 (𝜑 → (2 − ((𝐼 + 2) − 𝐼)) = 0)
161157, 160syl5eq 2697 . . . . . . . . . . 11 (𝜑 → ((#‘⟨“𝑟𝑠”⟩) − ((𝐼 + 2) − 𝐼)) = 0)
162161oveq2d 6706 . . . . . . . . . 10 (𝜑 → ((#‘𝑊) + ((#‘⟨“𝑟𝑠”⟩) − ((𝐼 + 2) − 𝐼))) = ((#‘𝑊) + 0))
16323, 51eqeltrd 2730 . . . . . . . . . . 11 (𝜑 → (#‘𝑊) ∈ ℂ)
164163addid1d 10274 . . . . . . . . . 10 (𝜑 → ((#‘𝑊) + 0) = (#‘𝑊))
165162, 164, 233eqtrd 2689 . . . . . . . . 9 (𝜑 → ((#‘𝑊) + ((#‘⟨“𝑟𝑠”⟩) − ((𝐼 + 2) − 𝐼))) = 𝐿)
166165adantr 480 . . . . . . . 8 ((𝜑 ∧ (𝑟𝑇𝑠𝑇)) → ((#‘𝑊) + ((#‘⟨“𝑟𝑠”⟩) − ((𝐼 + 2) − 𝐼))) = 𝐿)
167155, 166eqtrd 2685 . . . . . . 7 ((𝜑 ∧ (𝑟𝑇𝑠𝑇)) → (#‘(𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)) = 𝐿)
168167adantrr 753 . . . . . 6 ((𝜑 ∧ ((𝑟𝑇𝑠𝑇) ∧ (((𝑊𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → (#‘(𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)) = 𝐿)
169152, 168jca 553 . . . . 5 ((𝜑 ∧ ((𝑟𝑇𝑠𝑇) ∧ (((𝑊𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → ((𝐺 Σg (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)) = ( I ↾ 𝐷) ∧ (#‘(𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)) = 𝐿))
17026adantr 480 . . . . . 6 ((𝜑 ∧ ((𝑟𝑇𝑠𝑇) ∧ (((𝑊𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → (𝐼 + 1) ∈ (0..^𝐿))
171 simprr2 1130 . . . . . . 7 ((𝜑 ∧ ((𝑟𝑇𝑠𝑇) ∧ (((𝑊𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → 𝐴 ∈ dom (𝑠 ∖ I ))
172 1nn0 11346 . . . . . . . . . . . . . . 15 1 ∈ ℕ0
173 2nn 11223 . . . . . . . . . . . . . . 15 2 ∈ ℕ
174 1lt2 11232 . . . . . . . . . . . . . . 15 1 < 2
175 elfzo0 12548 . . . . . . . . . . . . . . 15 (1 ∈ (0..^2) ↔ (1 ∈ ℕ0 ∧ 2 ∈ ℕ ∧ 1 < 2))
176172, 173, 174, 175mpbir3an 1263 . . . . . . . . . . . . . 14 1 ∈ (0..^2)
177156oveq2i 6701 . . . . . . . . . . . . . 14 (0..^(#‘⟨“𝑟𝑠”⟩)) = (0..^2)
178176, 177eleqtrri 2729 . . . . . . . . . . . . 13 1 ∈ (0..^(#‘⟨“𝑟𝑠”⟩))
179178a1i 11 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑟𝑇𝑠𝑇)) → 1 ∈ (0..^(#‘⟨“𝑟𝑠”⟩)))
180120, 153, 154, 123, 179splfv2a 13553 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟𝑇𝑠𝑇)) → ((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘(𝐼 + 1)) = (⟨“𝑟𝑠”⟩‘1))
181 s2fv1 13679 . . . . . . . . . . . 12 (𝑠𝑇 → (⟨“𝑟𝑠”⟩‘1) = 𝑠)
182181ad2antll 765 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟𝑇𝑠𝑇)) → (⟨“𝑟𝑠”⟩‘1) = 𝑠)
183180, 182eqtrd 2685 . . . . . . . . . 10 ((𝜑 ∧ (𝑟𝑇𝑠𝑇)) → ((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘(𝐼 + 1)) = 𝑠)
184183adantrr 753 . . . . . . . . 9 ((𝜑 ∧ ((𝑟𝑇𝑠𝑇) ∧ (((𝑊𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → ((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘(𝐼 + 1)) = 𝑠)
185184difeq1d 3760 . . . . . . . 8 ((𝜑 ∧ ((𝑟𝑇𝑠𝑇) ∧ (((𝑊𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘(𝐼 + 1)) ∖ I ) = (𝑠 ∖ I ))
186185dmeqd 5358 . . . . . . 7 ((𝜑 ∧ ((𝑟𝑇𝑠𝑇) ∧ (((𝑊𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘(𝐼 + 1)) ∖ I ) = dom (𝑠 ∖ I ))
187171, 186eleqtrrd 2733 . . . . . 6 ((𝜑 ∧ ((𝑟𝑇𝑠𝑇) ∧ (((𝑊𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → 𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘(𝐼 + 1)) ∖ I ))
188 fzosplitsni 12619 . . . . . . . . . . 11 (𝐼 ∈ (ℤ‘0) → (𝑗 ∈ (0..^(𝐼 + 1)) ↔ (𝑗 ∈ (0..^𝐼) ∨ 𝑗 = 𝐼)))
189 nn0uz 11760 . . . . . . . . . . 11 0 = (ℤ‘0)
190188, 189eleq2s 2748 . . . . . . . . . 10 (𝐼 ∈ ℕ0 → (𝑗 ∈ (0..^(𝐼 + 1)) ↔ (𝑗 ∈ (0..^𝐼) ∨ 𝑗 = 𝐼)))
19110, 190syl 17 . . . . . . . . 9 (𝜑 → (𝑗 ∈ (0..^(𝐼 + 1)) ↔ (𝑗 ∈ (0..^𝐼) ∨ 𝑗 = 𝐼)))
192191adantr 480 . . . . . . . 8 ((𝜑 ∧ ((𝑟𝑇𝑠𝑇) ∧ (((𝑊𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → (𝑗 ∈ (0..^(𝐼 + 1)) ↔ (𝑗 ∈ (0..^𝐼) ∨ 𝑗 = 𝐼)))
193 fveq2 6229 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 𝑗 → (𝑊𝑘) = (𝑊𝑗))
194193difeq1d 3760 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑗 → ((𝑊𝑘) ∖ I ) = ((𝑊𝑗) ∖ I ))
195194dmeqd 5358 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑗 → dom ((𝑊𝑘) ∖ I ) = dom ((𝑊𝑗) ∖ I ))
196195eleq2d 2716 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑗 → (𝐴 ∈ dom ((𝑊𝑘) ∖ I ) ↔ 𝐴 ∈ dom ((𝑊𝑗) ∖ I )))
197196notbid 307 . . . . . . . . . . . . . . 15 (𝑘 = 𝑗 → (¬ 𝐴 ∈ dom ((𝑊𝑘) ∖ I ) ↔ ¬ 𝐴 ∈ dom ((𝑊𝑗) ∖ I )))
198197rspccva 3339 . . . . . . . . . . . . . 14 ((∀𝑘 ∈ (0..^𝐼) ¬ 𝐴 ∈ dom ((𝑊𝑘) ∖ I ) ∧ 𝑗 ∈ (0..^𝐼)) → ¬ 𝐴 ∈ dom ((𝑊𝑗) ∖ I ))
19925, 198sylan 487 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0..^𝐼)) → ¬ 𝐴 ∈ dom ((𝑊𝑗) ∖ I ))
200199adantlr 751 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑟𝑇𝑠𝑇)) ∧ 𝑗 ∈ (0..^𝐼)) → ¬ 𝐴 ∈ dom ((𝑊𝑗) ∖ I ))
2011ad2antrr 762 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑟𝑇𝑠𝑇)) ∧ 𝑗 ∈ (0..^𝐼)) → 𝑊 ∈ Word 𝑇)
20218ad2antrr 762 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑟𝑇𝑠𝑇)) ∧ 𝑗 ∈ (0..^𝐼)) → 𝐼 ∈ (0...(𝐼 + 2)))
20336ad2antrr 762 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑟𝑇𝑠𝑇)) ∧ 𝑗 ∈ (0..^𝐼)) → (𝐼 + 2) ∈ (0...(#‘𝑊)))
204123adantr 480 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑟𝑇𝑠𝑇)) ∧ 𝑗 ∈ (0..^𝐼)) → ⟨“𝑟𝑠”⟩ ∈ Word 𝑇)
205 simpr 476 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑟𝑇𝑠𝑇)) ∧ 𝑗 ∈ (0..^𝐼)) → 𝑗 ∈ (0..^𝐼))
206201, 202, 203, 204, 205splfv1 13552 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑟𝑇𝑠𝑇)) ∧ 𝑗 ∈ (0..^𝐼)) → ((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) = (𝑊𝑗))
207206difeq1d 3760 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑟𝑇𝑠𝑇)) ∧ 𝑗 ∈ (0..^𝐼)) → (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) ∖ I ) = ((𝑊𝑗) ∖ I ))
208207dmeqd 5358 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑟𝑇𝑠𝑇)) ∧ 𝑗 ∈ (0..^𝐼)) → dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) ∖ I ) = dom ((𝑊𝑗) ∖ I ))
209200, 208neleqtrrd 2752 . . . . . . . . . . 11 (((𝜑 ∧ (𝑟𝑇𝑠𝑇)) ∧ 𝑗 ∈ (0..^𝐼)) → ¬ 𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) ∖ I ))
210209ex 449 . . . . . . . . . 10 ((𝜑 ∧ (𝑟𝑇𝑠𝑇)) → (𝑗 ∈ (0..^𝐼) → ¬ 𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) ∖ I )))
211210adantrr 753 . . . . . . . . 9 ((𝜑 ∧ ((𝑟𝑇𝑠𝑇) ∧ (((𝑊𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → (𝑗 ∈ (0..^𝐼) → ¬ 𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) ∖ I )))
212 simprr3 1131 . . . . . . . . . . 11 ((𝜑 ∧ ((𝑟𝑇𝑠𝑇) ∧ (((𝑊𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → ¬ 𝐴 ∈ dom (𝑟 ∖ I ))
213 0nn0 11345 . . . . . . . . . . . . . . . . . . . 20 0 ∈ ℕ0
214 2pos 11150 . . . . . . . . . . . . . . . . . . . 20 0 < 2
215 elfzo0 12548 . . . . . . . . . . . . . . . . . . . 20 (0 ∈ (0..^2) ↔ (0 ∈ ℕ0 ∧ 2 ∈ ℕ ∧ 0 < 2))
216213, 173, 214, 215mpbir3an 1263 . . . . . . . . . . . . . . . . . . 19 0 ∈ (0..^2)
217216, 177eleqtrri 2729 . . . . . . . . . . . . . . . . . 18 0 ∈ (0..^(#‘⟨“𝑟𝑠”⟩))
218217a1i 11 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑟𝑇𝑠𝑇)) → 0 ∈ (0..^(#‘⟨“𝑟𝑠”⟩)))
219120, 153, 154, 123, 218splfv2a 13553 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑟𝑇𝑠𝑇)) → ((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘(𝐼 + 0)) = (⟨“𝑟𝑠”⟩‘0))
22029addid1d 10274 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐼 + 0) = 𝐼)
221220adantr 480 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑟𝑇𝑠𝑇)) → (𝐼 + 0) = 𝐼)
222221fveq2d 6233 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑟𝑇𝑠𝑇)) → ((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘(𝐼 + 0)) = ((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝐼))
223 s2fv0 13678 . . . . . . . . . . . . . . . . 17 (𝑟𝑇 → (⟨“𝑟𝑠”⟩‘0) = 𝑟)
224223ad2antrl 764 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑟𝑇𝑠𝑇)) → (⟨“𝑟𝑠”⟩‘0) = 𝑟)
225219, 222, 2243eqtr3d 2693 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑟𝑇𝑠𝑇)) → ((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝐼) = 𝑟)
226225difeq1d 3760 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑟𝑇𝑠𝑇)) → (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝐼) ∖ I ) = (𝑟 ∖ I ))
227226dmeqd 5358 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑟𝑇𝑠𝑇)) → dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝐼) ∖ I ) = dom (𝑟 ∖ I ))
228227eleq2d 2716 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑟𝑇𝑠𝑇)) → (𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝐼) ∖ I ) ↔ 𝐴 ∈ dom (𝑟 ∖ I )))
229228adantrr 753 . . . . . . . . . . 11 ((𝜑 ∧ ((𝑟𝑇𝑠𝑇) ∧ (((𝑊𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → (𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝐼) ∖ I ) ↔ 𝐴 ∈ dom (𝑟 ∖ I )))
230212, 229mtbird 314 . . . . . . . . . 10 ((𝜑 ∧ ((𝑟𝑇𝑠𝑇) ∧ (((𝑊𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → ¬ 𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝐼) ∖ I ))
231 fveq2 6229 . . . . . . . . . . . . . 14 (𝑗 = 𝐼 → ((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) = ((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝐼))
232231difeq1d 3760 . . . . . . . . . . . . 13 (𝑗 = 𝐼 → (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) ∖ I ) = (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝐼) ∖ I ))
233232dmeqd 5358 . . . . . . . . . . . 12 (𝑗 = 𝐼 → dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) ∖ I ) = dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝐼) ∖ I ))
234233eleq2d 2716 . . . . . . . . . . 11 (𝑗 = 𝐼 → (𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) ∖ I ) ↔ 𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝐼) ∖ I )))
235234notbid 307 . . . . . . . . . 10 (𝑗 = 𝐼 → (¬ 𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) ∖ I ) ↔ ¬ 𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝐼) ∖ I )))
236230, 235syl5ibrcom 237 . . . . . . . . 9 ((𝜑 ∧ ((𝑟𝑇𝑠𝑇) ∧ (((𝑊𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → (𝑗 = 𝐼 → ¬ 𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) ∖ I )))
237211, 236jaod 394 . . . . . . . 8 ((𝜑 ∧ ((𝑟𝑇𝑠𝑇) ∧ (((𝑊𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → ((𝑗 ∈ (0..^𝐼) ∨ 𝑗 = 𝐼) → ¬ 𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) ∖ I )))
238192, 237sylbid 230 . . . . . . 7 ((𝜑 ∧ ((𝑟𝑇𝑠𝑇) ∧ (((𝑊𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → (𝑗 ∈ (0..^(𝐼 + 1)) → ¬ 𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) ∖ I )))
239238ralrimiv 2994 . . . . . 6 ((𝜑 ∧ ((𝑟𝑇𝑠𝑇) ∧ (((𝑊𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → ∀𝑗 ∈ (0..^(𝐼 + 1)) ¬ 𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) ∖ I ))
240170, 187, 2393jca 1261 . . . . 5 ((𝜑 ∧ ((𝑟𝑇𝑠𝑇) ∧ (((𝑊𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → ((𝐼 + 1) ∈ (0..^𝐿) ∧ 𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘(𝐼 + 1)) ∖ I ) ∧ ∀𝑗 ∈ (0..^(𝐼 + 1)) ¬ 𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) ∖ I )))
241 oveq2 6698 . . . . . . . . 9 (𝑤 = (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩) → (𝐺 Σg 𝑤) = (𝐺 Σg (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)))
242241eqeq1d 2653 . . . . . . . 8 (𝑤 = (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩) → ((𝐺 Σg 𝑤) = ( I ↾ 𝐷) ↔ (𝐺 Σg (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)) = ( I ↾ 𝐷)))
243 fveq2 6229 . . . . . . . . 9 (𝑤 = (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩) → (#‘𝑤) = (#‘(𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)))
244243eqeq1d 2653 . . . . . . . 8 (𝑤 = (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩) → ((#‘𝑤) = 𝐿 ↔ (#‘(𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)) = 𝐿))
245242, 244anbi12d 747 . . . . . . 7 (𝑤 = (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩) → (((𝐺 Σg 𝑤) = ( I ↾ 𝐷) ∧ (#‘𝑤) = 𝐿) ↔ ((𝐺 Σg (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)) = ( I ↾ 𝐷) ∧ (#‘(𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)) = 𝐿)))
246 fveq1 6228 . . . . . . . . . . 11 (𝑤 = (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩) → (𝑤‘(𝐼 + 1)) = ((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘(𝐼 + 1)))
247246difeq1d 3760 . . . . . . . . . 10 (𝑤 = (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩) → ((𝑤‘(𝐼 + 1)) ∖ I ) = (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘(𝐼 + 1)) ∖ I ))
248247dmeqd 5358 . . . . . . . . 9 (𝑤 = (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩) → dom ((𝑤‘(𝐼 + 1)) ∖ I ) = dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘(𝐼 + 1)) ∖ I ))
249248eleq2d 2716 . . . . . . . 8 (𝑤 = (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩) → (𝐴 ∈ dom ((𝑤‘(𝐼 + 1)) ∖ I ) ↔ 𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘(𝐼 + 1)) ∖ I )))
250 fveq1 6228 . . . . . . . . . . . . 13 (𝑤 = (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩) → (𝑤𝑗) = ((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗))
251250difeq1d 3760 . . . . . . . . . . . 12 (𝑤 = (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩) → ((𝑤𝑗) ∖ I ) = (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) ∖ I ))
252251dmeqd 5358 . . . . . . . . . . 11 (𝑤 = (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩) → dom ((𝑤𝑗) ∖ I ) = dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) ∖ I ))
253252eleq2d 2716 . . . . . . . . . 10 (𝑤 = (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩) → (𝐴 ∈ dom ((𝑤𝑗) ∖ I ) ↔ 𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) ∖ I )))
254253notbid 307 . . . . . . . . 9 (𝑤 = (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩) → (¬ 𝐴 ∈ dom ((𝑤𝑗) ∖ I ) ↔ ¬ 𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) ∖ I )))
255254ralbidv 3015 . . . . . . . 8 (𝑤 = (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩) → (∀𝑗 ∈ (0..^(𝐼 + 1)) ¬ 𝐴 ∈ dom ((𝑤𝑗) ∖ I ) ↔ ∀𝑗 ∈ (0..^(𝐼 + 1)) ¬ 𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) ∖ I )))
256249, 2553anbi23d 1442 . . . . . . 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 ))))
257245, 256anbi12d 747 . . . . . 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 )))))
258257rspcev 3340 . . . . 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 ))))
259126, 169, 240, 258syl12anc 1364 . . . 4 ((𝜑 ∧ ((𝑟𝑇𝑠𝑇) ∧ (((𝑊𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → ∃𝑤 ∈ Word 𝑇(((𝐺 Σg 𝑤) = ( I ↾ 𝐷) ∧ (#‘𝑤) = 𝐿) ∧ ((𝐼 + 1) ∈ (0..^𝐿) ∧ 𝐴 ∈ dom ((𝑤‘(𝐼 + 1)) ∖ I ) ∧ ∀𝑗 ∈ (0..^(𝐼 + 1)) ¬ 𝐴 ∈ dom ((𝑤𝑗) ∖ I ))))
260259expr 642 . . 3 ((𝜑 ∧ (𝑟𝑇𝑠𝑇)) → ((((𝑊𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )) → ∃𝑤 ∈ Word 𝑇(((𝐺 Σg 𝑤) = ( I ↾ 𝐷) ∧ (#‘𝑤) = 𝐿) ∧ ((𝐼 + 1) ∈ (0..^𝐿) ∧ 𝐴 ∈ dom ((𝑤‘(𝐼 + 1)) ∖ I ) ∧ ∀𝑗 ∈ (0..^(𝐼 + 1)) ¬ 𝐴 ∈ dom ((𝑤𝑗) ∖ I )))))
261260rexlimdvva 3067 . 2 (𝜑 → (∃𝑟𝑇𝑠𝑇 (((𝑊𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )) → ∃𝑤 ∈ Word 𝑇(((𝐺 Σg 𝑤) = ( I ↾ 𝐷) ∧ (#‘𝑤) = 𝐿) ∧ ((𝐼 + 1) ∈ (0..^𝐿) ∧ 𝐴 ∈ dom ((𝑤‘(𝐼 + 1)) ∖ I ) ∧ ∀𝑗 ∈ (0..^(𝐼 + 1)) ¬ 𝐴 ∈ dom ((𝑤𝑗) ∖ I )))))
26220, 21, 87, 89, 24psgnunilem1 17959 . 2 (𝜑 → (((𝑊𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷) ∨ ∃𝑟𝑇𝑠𝑇 (((𝑊𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I ))))
263119, 261, 262mpjaod 395 1 (𝜑 → ∃𝑤 ∈ Word 𝑇(((𝐺 Σg 𝑤) = ( I ↾ 𝐷) ∧ (#‘𝑤) = 𝐿) ∧ ((𝐼 + 1) ∈ (0..^𝐿) ∧ 𝐴 ∈ dom ((𝑤‘(𝐼 + 1)) ∖ I ) ∧ ∀𝑗 ∈ (0..^(𝐼 + 1)) ¬ 𝐴 ∈ dom ((𝑤𝑗) ∖ I ))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wo 382  wa 383  w3a 1054   = wceq 1523  wcel 2030  wral 2941  wrex 2942  cdif 3604  wss 3607  c0 3948  cop 4216  cotp 4218   class class class wbr 4685   I cid 5052  dom cdm 5143  ran crn 5144  cres 5145  ccom 5147  wf 5922  cfv 5926  (class class class)co 6690  cc 9972  cr 9973  0cc0 9974  1c1 9975   + caddc 9977   < clt 10112  cle 10113  cmin 10304  -cneg 10305  cn 11058  2c2 11108  0cn0 11330  cz 11415  cuz 11725  ...cfz 12364  ..^cfzo 12504  #chash 13157  Word cword 13323   substr csubstr 13327   splice csplice 13328  ⟨“cs2 13632  Basecbs 15904  +gcplusg 15988  0gc0g 16147   Σg cgsu 16148  Mndcmnd 17341  Grpcgrp 17469  SymGrpcsymg 17843  pmTrspcpmtr 17907
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-xor 1505  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-ot 4219  df-uni 4469  df-int 4508  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-om 7108  df-1st 7210  df-2nd 7211  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-2o 7606  df-oadd 7609  df-er 7787  df-map 7901  df-en 7998  df-dom 7999  df-sdom 8000  df-fin 8001  df-card 8803  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-nn 11059  df-2 11117  df-3 11118  df-4 11119  df-5 11120  df-6 11121  df-7 11122  df-8 11123  df-9 11124  df-n0 11331  df-z 11416  df-uz 11726  df-fz 12365  df-fzo 12505  df-seq 12842  df-hash 13158  df-word 13331  df-lsw 13332  df-concat 13333  df-s1 13334  df-substr 13335  df-splice 13336  df-s2 13639  df-struct 15906  df-ndx 15907  df-slot 15908  df-base 15910  df-sets 15911  df-ress 15912  df-plusg 16001  df-tset 16007  df-0g 16149  df-gsum 16150  df-mgm 17289  df-sgrp 17331  df-mnd 17342  df-submnd 17383  df-grp 17472  df-minusg 17473  df-subg 17638  df-symg 17844  df-pmtr 17908
This theorem is referenced by:  psgnunilem3  17962
  Copyright terms: Public domain W3C validator