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

Theorem psgnunilem2 17684
Description: Lemma for psgnuni 17688. 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 13131 . . . . . . 7 ∅ ∈ Word 𝑇
3 splcl 13300 . . . . . . 7 ((𝑊 ∈ Word 𝑇 ∧ ∅ ∈ Word 𝑇) → (𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩) ∈ Word 𝑇)
41, 2, 3sylancl 692 . . . . . 6 (𝜑 → (𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩) ∈ Word 𝑇)
54adantr 479 . . . . 5 ((𝜑 ∧ ((𝑊𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷)) → (𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩) ∈ Word 𝑇)
6 fzossfz 12312 . . . . . . . . . . 11 (0..^𝐿) ⊆ (0...𝐿)
7 psgnunilem2.ix . . . . . . . . . . 11 (𝜑𝐼 ∈ (0..^𝐿))
86, 7sseldi 3565 . . . . . . . . . 10 (𝜑𝐼 ∈ (0...𝐿))
9 elfznn0 12257 . . . . . . . . . 10 (𝐼 ∈ (0...𝐿) → 𝐼 ∈ ℕ0)
108, 9syl 17 . . . . . . . . 9 (𝜑𝐼 ∈ ℕ0)
11 2nn0 11156 . . . . . . . . . 10 2 ∈ ℕ0
12 nn0addcl 11175 . . . . . . . . . 10 ((𝐼 ∈ ℕ0 ∧ 2 ∈ ℕ0) → (𝐼 + 2) ∈ ℕ0)
1310, 11, 12sylancl 692 . . . . . . . . 9 (𝜑 → (𝐼 + 2) ∈ ℕ0)
1410nn0red 11199 . . . . . . . . . 10 (𝜑𝐼 ∈ ℝ)
15 nn0addge1 11186 . . . . . . . . . 10 ((𝐼 ∈ ℝ ∧ 2 ∈ ℕ0) → 𝐼 ≤ (𝐼 + 2))
1614, 11, 15sylancl 692 . . . . . . . . 9 (𝜑𝐼 ≤ (𝐼 + 2))
17 elfz2nn0 12255 . . . . . . . . 9 (𝐼 ∈ (0...(𝐼 + 2)) ↔ (𝐼 ∈ ℕ0 ∧ (𝐼 + 2) ∈ ℕ0𝐼 ≤ (𝐼 + 2)))
1810, 13, 16, 17syl3anbrc 1238 . . . . . . . 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 17683 . . . . . . . . . 10 (𝜑 → (𝐼 + 1) ∈ (0..^𝐿))
27 fzofzp1 12386 . . . . . . . . . 10 ((𝐼 + 1) ∈ (0..^𝐿) → ((𝐼 + 1) + 1) ∈ (0...𝐿))
2826, 27syl 17 . . . . . . . . 9 (𝜑 → ((𝐼 + 1) + 1) ∈ (0...𝐿))
2910nn0cnd 11200 . . . . . . . . . . 11 (𝜑𝐼 ∈ ℂ)
30 1cnd 9912 . . . . . . . . . . 11 (𝜑 → 1 ∈ ℂ)
3129, 30, 30addassd 9918 . . . . . . . . . 10 (𝜑 → ((𝐼 + 1) + 1) = (𝐼 + (1 + 1)))
32 df-2 10926 . . . . . . . . . . 11 2 = (1 + 1)
3332oveq2i 6538 . . . . . . . . . 10 (𝐼 + 2) = (𝐼 + (1 + 1))
3431, 33syl6reqr 2662 . . . . . . . . 9 (𝜑 → (𝐼 + 2) = ((𝐼 + 1) + 1))
3523oveq2d 6543 . . . . . . . . 9 (𝜑 → (0...(#‘𝑊)) = (0...𝐿))
3628, 34, 353eltr4d 2702 . . . . . . . 8 (𝜑 → (𝐼 + 2) ∈ (0...(#‘𝑊)))
372a1i 11 . . . . . . . 8 (𝜑 → ∅ ∈ Word 𝑇)
381, 18, 36, 37spllen 13302 . . . . . . 7 (𝜑 → (#‘(𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩)) = ((#‘𝑊) + ((#‘∅) − ((𝐼 + 2) − 𝐼))))
39 hash0 12971 . . . . . . . . . . 11 (#‘∅) = 0
4039oveq1i 6537 . . . . . . . . . 10 ((#‘∅) − ((𝐼 + 2) − 𝐼)) = (0 − ((𝐼 + 2) − 𝐼))
41 df-neg 10120 . . . . . . . . . 10 -((𝐼 + 2) − 𝐼) = (0 − ((𝐼 + 2) − 𝐼))
4240, 41eqtr4i 2634 . . . . . . . . 9 ((#‘∅) − ((𝐼 + 2) − 𝐼)) = -((𝐼 + 2) − 𝐼)
43 2cn 10938 . . . . . . . . . . 11 2 ∈ ℂ
44 pncan2 10139 . . . . . . . . . . 11 ((𝐼 ∈ ℂ ∧ 2 ∈ ℂ) → ((𝐼 + 2) − 𝐼) = 2)
4529, 43, 44sylancl 692 . . . . . . . . . 10 (𝜑 → ((𝐼 + 2) − 𝐼) = 2)
4645negeqd 10126 . . . . . . . . 9 (𝜑 → -((𝐼 + 2) − 𝐼) = -2)
4742, 46syl5eq 2655 . . . . . . . 8 (𝜑 → ((#‘∅) − ((𝐼 + 2) − 𝐼)) = -2)
4823, 47oveq12d 6545 . . . . . . 7 (𝜑 → ((#‘𝑊) + ((#‘∅) − ((𝐼 + 2) − 𝐼))) = (𝐿 + -2))
49 elfzel2 12166 . . . . . . . . . 10 (𝐼 ∈ (0...𝐿) → 𝐿 ∈ ℤ)
508, 49syl 17 . . . . . . . . 9 (𝜑𝐿 ∈ ℤ)
5150zcnd 11315 . . . . . . . 8 (𝜑𝐿 ∈ ℂ)
52 negsub 10180 . . . . . . . 8 ((𝐿 ∈ ℂ ∧ 2 ∈ ℂ) → (𝐿 + -2) = (𝐿 − 2))
5351, 43, 52sylancl 692 . . . . . . 7 (𝜑 → (𝐿 + -2) = (𝐿 − 2))
5438, 48, 533eqtrd 2647 . . . . . 6 (𝜑 → (#‘(𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩)) = (𝐿 − 2))
5554adantr 479 . . . . 5 ((𝜑 ∧ ((𝑊𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷)) → (#‘(𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩)) = (𝐿 − 2))
56 splid 13301 . . . . . . . . 9 ((𝑊 ∈ Word 𝑇 ∧ (𝐼 ∈ (0...(𝐼 + 2)) ∧ (𝐼 + 2) ∈ (0...(#‘𝑊)))) → (𝑊 splice ⟨𝐼, (𝐼 + 2), (𝑊 substr ⟨𝐼, (𝐼 + 2)⟩)⟩) = 𝑊)
571, 18, 36, 56syl12anc 1315 . . . . . . . 8 (𝜑 → (𝑊 splice ⟨𝐼, (𝐼 + 2), (𝑊 substr ⟨𝐼, (𝐼 + 2)⟩)⟩) = 𝑊)
5857oveq2d 6543 . . . . . . 7 (𝜑 → (𝐺 Σg (𝑊 splice ⟨𝐼, (𝐼 + 2), (𝑊 substr ⟨𝐼, (𝐼 + 2)⟩)⟩)) = (𝐺 Σg 𝑊))
5958adantr 479 . . . . . 6 ((𝜑 ∧ ((𝑊𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷)) → (𝐺 Σg (𝑊 splice ⟨𝐼, (𝐼 + 2), (𝑊 substr ⟨𝐼, (𝐼 + 2)⟩)⟩)) = (𝐺 Σg 𝑊))
60 eqid 2609 . . . . . . 7 (Base‘𝐺) = (Base‘𝐺)
6119symggrp 17589 . . . . . . . . . 10 (𝐷𝑉𝐺 ∈ Grp)
6221, 61syl 17 . . . . . . . . 9 (𝜑𝐺 ∈ Grp)
63 grpmnd 17198 . . . . . . . . 9 (𝐺 ∈ Grp → 𝐺 ∈ Mnd)
6462, 63syl 17 . . . . . . . 8 (𝜑𝐺 ∈ Mnd)
6564adantr 479 . . . . . . 7 ((𝜑 ∧ ((𝑊𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷)) → 𝐺 ∈ Mnd)
6620, 19, 60symgtrf 17658 . . . . . . . . . 10 𝑇 ⊆ (Base‘𝐺)
67 sswrd 13114 . . . . . . . . . 10 (𝑇 ⊆ (Base‘𝐺) → Word 𝑇 ⊆ Word (Base‘𝐺))
6866, 67ax-mp 5 . . . . . . . . 9 Word 𝑇 ⊆ Word (Base‘𝐺)
6968, 1sseldi 3565 . . . . . . . 8 (𝜑𝑊 ∈ Word (Base‘𝐺))
7069adantr 479 . . . . . . 7 ((𝜑 ∧ ((𝑊𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷)) → 𝑊 ∈ Word (Base‘𝐺))
7118adantr 479 . . . . . . 7 ((𝜑 ∧ ((𝑊𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷)) → 𝐼 ∈ (0...(𝐼 + 2)))
7236adantr 479 . . . . . . 7 ((𝜑 ∧ ((𝑊𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷)) → (𝐼 + 2) ∈ (0...(#‘𝑊)))
73 swrdcl 13217 . . . . . . . . 9 (𝑊 ∈ Word (Base‘𝐺) → (𝑊 substr ⟨𝐼, (𝐼 + 2)⟩) ∈ Word (Base‘𝐺))
7469, 73syl 17 . . . . . . . 8 (𝜑 → (𝑊 substr ⟨𝐼, (𝐼 + 2)⟩) ∈ Word (Base‘𝐺))
7574adantr 479 . . . . . . 7 ((𝜑 ∧ ((𝑊𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷)) → (𝑊 substr ⟨𝐼, (𝐼 + 2)⟩) ∈ Word (Base‘𝐺))
76 wrd0 13131 . . . . . . . 8 ∅ ∈ Word (Base‘𝐺)
7776a1i 11 . . . . . . 7 ((𝜑 ∧ ((𝑊𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷)) → ∅ ∈ Word (Base‘𝐺))
7823oveq2d 6543 . . . . . . . . . . . . 13 (𝜑 → (0..^(#‘𝑊)) = (0..^𝐿))
7926, 78eleqtrrd 2690 . . . . . . . . . . . 12 (𝜑 → (𝐼 + 1) ∈ (0..^(#‘𝑊)))
80 swrds2 13479 . . . . . . . . . . . 12 ((𝑊 ∈ Word 𝑇𝐼 ∈ ℕ0 ∧ (𝐼 + 1) ∈ (0..^(#‘𝑊))) → (𝑊 substr ⟨𝐼, (𝐼 + 2)⟩) = ⟨“(𝑊𝐼)(𝑊‘(𝐼 + 1))”⟩)
811, 10, 79, 80syl3anc 1317 . . . . . . . . . . 11 (𝜑 → (𝑊 substr ⟨𝐼, (𝐼 + 2)⟩) = ⟨“(𝑊𝐼)(𝑊‘(𝐼 + 1))”⟩)
8281oveq2d 6543 . . . . . . . . . 10 (𝜑 → (𝐺 Σg (𝑊 substr ⟨𝐼, (𝐼 + 2)⟩)) = (𝐺 Σg ⟨“(𝑊𝐼)(𝑊‘(𝐼 + 1))”⟩))
83 wrdf 13111 . . . . . . . . . . . . . . 15 (𝑊 ∈ Word 𝑇𝑊:(0..^(#‘𝑊))⟶𝑇)
841, 83syl 17 . . . . . . . . . . . . . 14 (𝜑𝑊:(0..^(#‘𝑊))⟶𝑇)
8578feq2d 5930 . . . . . . . . . . . . . 14 (𝜑 → (𝑊:(0..^(#‘𝑊))⟶𝑇𝑊:(0..^𝐿)⟶𝑇))
8684, 85mpbid 220 . . . . . . . . . . . . 13 (𝜑𝑊:(0..^𝐿)⟶𝑇)
8786, 7ffvelrnd 6253 . . . . . . . . . . . 12 (𝜑 → (𝑊𝐼) ∈ 𝑇)
8866, 87sseldi 3565 . . . . . . . . . . 11 (𝜑 → (𝑊𝐼) ∈ (Base‘𝐺))
8986, 26ffvelrnd 6253 . . . . . . . . . . . 12 (𝜑 → (𝑊‘(𝐼 + 1)) ∈ 𝑇)
9066, 89sseldi 3565 . . . . . . . . . . 11 (𝜑 → (𝑊‘(𝐼 + 1)) ∈ (Base‘𝐺))
91 eqid 2609 . . . . . . . . . . . 12 (+g𝐺) = (+g𝐺)
9260, 91gsumws2 17148 . . . . . . . . . . 11 ((𝐺 ∈ Mnd ∧ (𝑊𝐼) ∈ (Base‘𝐺) ∧ (𝑊‘(𝐼 + 1)) ∈ (Base‘𝐺)) → (𝐺 Σg ⟨“(𝑊𝐼)(𝑊‘(𝐼 + 1))”⟩) = ((𝑊𝐼)(+g𝐺)(𝑊‘(𝐼 + 1))))
9364, 88, 90, 92syl3anc 1317 . . . . . . . . . 10 (𝜑 → (𝐺 Σg ⟨“(𝑊𝐼)(𝑊‘(𝐼 + 1))”⟩) = ((𝑊𝐼)(+g𝐺)(𝑊‘(𝐼 + 1))))
9419, 60, 91symgov 17579 . . . . . . . . . . 11 (((𝑊𝐼) ∈ (Base‘𝐺) ∧ (𝑊‘(𝐼 + 1)) ∈ (Base‘𝐺)) → ((𝑊𝐼)(+g𝐺)(𝑊‘(𝐼 + 1))) = ((𝑊𝐼) ∘ (𝑊‘(𝐼 + 1))))
9588, 90, 94syl2anc 690 . . . . . . . . . 10 (𝜑 → ((𝑊𝐼)(+g𝐺)(𝑊‘(𝐼 + 1))) = ((𝑊𝐼) ∘ (𝑊‘(𝐼 + 1))))
9682, 93, 953eqtrd 2647 . . . . . . . . 9 (𝜑 → (𝐺 Σg (𝑊 substr ⟨𝐼, (𝐼 + 2)⟩)) = ((𝑊𝐼) ∘ (𝑊‘(𝐼 + 1))))
9796adantr 479 . . . . . . . 8 ((𝜑 ∧ ((𝑊𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷)) → (𝐺 Σg (𝑊 substr ⟨𝐼, (𝐼 + 2)⟩)) = ((𝑊𝐼) ∘ (𝑊‘(𝐼 + 1))))
98 simpr 475 . . . . . . . 8 ((𝜑 ∧ ((𝑊𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷)) → ((𝑊𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷))
9919symgid 17590 . . . . . . . . . . 11 (𝐷𝑉 → ( I ↾ 𝐷) = (0g𝐺))
10021, 99syl 17 . . . . . . . . . 10 (𝜑 → ( I ↾ 𝐷) = (0g𝐺))
101 eqid 2609 . . . . . . . . . . 11 (0g𝐺) = (0g𝐺)
102101gsum0 17047 . . . . . . . . . 10 (𝐺 Σg ∅) = (0g𝐺)
103100, 102syl6eqr 2661 . . . . . . . . 9 (𝜑 → ( I ↾ 𝐷) = (𝐺 Σg ∅))
104103adantr 479 . . . . . . . 8 ((𝜑 ∧ ((𝑊𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷)) → ( I ↾ 𝐷) = (𝐺 Σg ∅))
10597, 98, 1043eqtrd 2647 . . . . . . 7 ((𝜑 ∧ ((𝑊𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷)) → (𝐺 Σg (𝑊 substr ⟨𝐼, (𝐼 + 2)⟩)) = (𝐺 Σg ∅))
10660, 65, 70, 71, 72, 75, 77, 105gsumspl 17150 . . . . . 6 ((𝜑 ∧ ((𝑊𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷)) → (𝐺 Σg (𝑊 splice ⟨𝐼, (𝐼 + 2), (𝑊 substr ⟨𝐼, (𝐼 + 2)⟩)⟩)) = (𝐺 Σg (𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩)))
10722adantr 479 . . . . . 6 ((𝜑 ∧ ((𝑊𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷)) → (𝐺 Σg 𝑊) = ( I ↾ 𝐷))
10859, 106, 1073eqtr3d 2651 . . . . 5 ((𝜑 ∧ ((𝑊𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷)) → (𝐺 Σg (𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩)) = ( I ↾ 𝐷))
109 fveq2 6088 . . . . . . . 8 (𝑥 = (𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩) → (#‘𝑥) = (#‘(𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩)))
110109eqeq1d 2611 . . . . . . 7 (𝑥 = (𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩) → ((#‘𝑥) = (𝐿 − 2) ↔ (#‘(𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩)) = (𝐿 − 2)))
111 oveq2 6535 . . . . . . . 8 (𝑥 = (𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩) → (𝐺 Σg 𝑥) = (𝐺 Σg (𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩)))
112111eqeq1d 2611 . . . . . . 7 (𝑥 = (𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩) → ((𝐺 Σg 𝑥) = ( I ↾ 𝐷) ↔ (𝐺 Σg (𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩)) = ( I ↾ 𝐷)))
113110, 112anbi12d 742 . . . . . 6 (𝑥 = (𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩) → (((#‘𝑥) = (𝐿 − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)) ↔ ((#‘(𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩)) = (𝐿 − 2) ∧ (𝐺 Σg (𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩)) = ( I ↾ 𝐷))))
114113rspcev 3281 . . . . 5 (((𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩) ∈ Word 𝑇 ∧ ((#‘(𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩)) = (𝐿 − 2) ∧ (𝐺 Σg (𝑊 splice ⟨𝐼, (𝐼 + 2), ∅⟩)) = ( I ↾ 𝐷))) → ∃𝑥 ∈ Word 𝑇((#‘𝑥) = (𝐿 − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)))
1155, 55, 108, 114syl12anc 1315 . . . 4 ((𝜑 ∧ ((𝑊𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷)) → ∃𝑥 ∈ Word 𝑇((#‘𝑥) = (𝐿 − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)))
116 psgnunilem2.in . . . . 5 (𝜑 → ¬ ∃𝑥 ∈ Word 𝑇((#‘𝑥) = (𝐿 − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)))
117116adantr 479 . . . 4 ((𝜑 ∧ ((𝑊𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷)) → ¬ ∃𝑥 ∈ Word 𝑇((#‘𝑥) = (𝐿 − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)))
118115, 117pm2.21dd 184 . . 3 ((𝜑 ∧ ((𝑊𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷)) → ∃𝑤 ∈ Word 𝑇(((𝐺 Σg 𝑤) = ( I ↾ 𝐷) ∧ (#‘𝑤) = 𝐿) ∧ ((𝐼 + 1) ∈ (0..^𝐿) ∧ 𝐴 ∈ dom ((𝑤‘(𝐼 + 1)) ∖ I ) ∧ ∀𝑗 ∈ (0..^(𝐼 + 1)) ¬ 𝐴 ∈ dom ((𝑤𝑗) ∖ I ))))
119118ex 448 . 2 (𝜑 → (((𝑊𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷) → ∃𝑤 ∈ Word 𝑇(((𝐺 Σg 𝑤) = ( I ↾ 𝐷) ∧ (#‘𝑤) = 𝐿) ∧ ((𝐼 + 1) ∈ (0..^𝐿) ∧ 𝐴 ∈ dom ((𝑤‘(𝐼 + 1)) ∖ I ) ∧ ∀𝑗 ∈ (0..^(𝐼 + 1)) ¬ 𝐴 ∈ dom ((𝑤𝑗) ∖ I )))))
1201adantr 479 . . . . . . 7 ((𝜑 ∧ (𝑟𝑇𝑠𝑇)) → 𝑊 ∈ Word 𝑇)
121 simprl 789 . . . . . . . 8 ((𝜑 ∧ (𝑟𝑇𝑠𝑇)) → 𝑟𝑇)
122 simprr 791 . . . . . . . 8 ((𝜑 ∧ (𝑟𝑇𝑠𝑇)) → 𝑠𝑇)
123121, 122s2cld 13412 . . . . . . 7 ((𝜑 ∧ (𝑟𝑇𝑠𝑇)) → ⟨“𝑟𝑠”⟩ ∈ Word 𝑇)
124 splcl 13300 . . . . . . 7 ((𝑊 ∈ Word 𝑇 ∧ ⟨“𝑟𝑠”⟩ ∈ Word 𝑇) → (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩) ∈ Word 𝑇)
125120, 123, 124syl2anc 690 . . . . . 6 ((𝜑 ∧ (𝑟𝑇𝑠𝑇)) → (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩) ∈ Word 𝑇)
126125adantrr 748 . . . . 5 ((𝜑 ∧ ((𝑟𝑇𝑠𝑇) ∧ (((𝑊𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩) ∈ Word 𝑇)
12764adantr 479 . . . . . . . 8 ((𝜑 ∧ ((𝑟𝑇𝑠𝑇) ∧ (((𝑊𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → 𝐺 ∈ Mnd)
12869adantr 479 . . . . . . . 8 ((𝜑 ∧ ((𝑟𝑇𝑠𝑇) ∧ (((𝑊𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → 𝑊 ∈ Word (Base‘𝐺))
12918adantr 479 . . . . . . . 8 ((𝜑 ∧ ((𝑟𝑇𝑠𝑇) ∧ (((𝑊𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → 𝐼 ∈ (0...(𝐼 + 2)))
13036adantr 479 . . . . . . . 8 ((𝜑 ∧ ((𝑟𝑇𝑠𝑇) ∧ (((𝑊𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → (𝐼 + 2) ∈ (0...(#‘𝑊)))
13168, 123sseldi 3565 . . . . . . . . 9 ((𝜑 ∧ (𝑟𝑇𝑠𝑇)) → ⟨“𝑟𝑠”⟩ ∈ Word (Base‘𝐺))
132131adantrr 748 . . . . . . . 8 ((𝜑 ∧ ((𝑟𝑇𝑠𝑇) ∧ (((𝑊𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → ⟨“𝑟𝑠”⟩ ∈ Word (Base‘𝐺))
13374adantr 479 . . . . . . . 8 ((𝜑 ∧ ((𝑟𝑇𝑠𝑇) ∧ (((𝑊𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → (𝑊 substr ⟨𝐼, (𝐼 + 2)⟩) ∈ Word (Base‘𝐺))
134 simprr1 1101 . . . . . . . . 9 ((𝜑 ∧ ((𝑟𝑇𝑠𝑇) ∧ (((𝑊𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → ((𝑊𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟𝑠))
13596adantr 479 . . . . . . . . 9 ((𝜑 ∧ ((𝑟𝑇𝑠𝑇) ∧ (((𝑊𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → (𝐺 Σg (𝑊 substr ⟨𝐼, (𝐼 + 2)⟩)) = ((𝑊𝐼) ∘ (𝑊‘(𝐼 + 1))))
13664adantr 479 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑟𝑇𝑠𝑇)) → 𝐺 ∈ Mnd)
13766a1i 11 . . . . . . . . . . . . . 14 (𝜑𝑇 ⊆ (Base‘𝐺))
138137sselda 3567 . . . . . . . . . . . . 13 ((𝜑𝑟𝑇) → 𝑟 ∈ (Base‘𝐺))
139138adantrr 748 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑟𝑇𝑠𝑇)) → 𝑟 ∈ (Base‘𝐺))
140137sselda 3567 . . . . . . . . . . . . 13 ((𝜑𝑠𝑇) → 𝑠 ∈ (Base‘𝐺))
141140adantrl 747 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑟𝑇𝑠𝑇)) → 𝑠 ∈ (Base‘𝐺))
14260, 91gsumws2 17148 . . . . . . . . . . . 12 ((𝐺 ∈ Mnd ∧ 𝑟 ∈ (Base‘𝐺) ∧ 𝑠 ∈ (Base‘𝐺)) → (𝐺 Σg ⟨“𝑟𝑠”⟩) = (𝑟(+g𝐺)𝑠))
143136, 139, 141, 142syl3anc 1317 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟𝑇𝑠𝑇)) → (𝐺 Σg ⟨“𝑟𝑠”⟩) = (𝑟(+g𝐺)𝑠))
14419, 60, 91symgov 17579 . . . . . . . . . . . 12 ((𝑟 ∈ (Base‘𝐺) ∧ 𝑠 ∈ (Base‘𝐺)) → (𝑟(+g𝐺)𝑠) = (𝑟𝑠))
145139, 141, 144syl2anc 690 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟𝑇𝑠𝑇)) → (𝑟(+g𝐺)𝑠) = (𝑟𝑠))
146143, 145eqtrd 2643 . . . . . . . . . 10 ((𝜑 ∧ (𝑟𝑇𝑠𝑇)) → (𝐺 Σg ⟨“𝑟𝑠”⟩) = (𝑟𝑠))
147146adantrr 748 . . . . . . . . 9 ((𝜑 ∧ ((𝑟𝑇𝑠𝑇) ∧ (((𝑊𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → (𝐺 Σg ⟨“𝑟𝑠”⟩) = (𝑟𝑠))
148134, 135, 1473eqtr4rd 2654 . . . . . . . 8 ((𝜑 ∧ ((𝑟𝑇𝑠𝑇) ∧ (((𝑊𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → (𝐺 Σg ⟨“𝑟𝑠”⟩) = (𝐺 Σg (𝑊 substr ⟨𝐼, (𝐼 + 2)⟩)))
14960, 127, 128, 129, 130, 132, 133, 148gsumspl 17150 . . . . . . 7 ((𝜑 ∧ ((𝑟𝑇𝑠𝑇) ∧ (((𝑊𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → (𝐺 Σg (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)) = (𝐺 Σg (𝑊 splice ⟨𝐼, (𝐼 + 2), (𝑊 substr ⟨𝐼, (𝐼 + 2)⟩)⟩)))
15058adantr 479 . . . . . . 7 ((𝜑 ∧ ((𝑟𝑇𝑠𝑇) ∧ (((𝑊𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → (𝐺 Σg (𝑊 splice ⟨𝐼, (𝐼 + 2), (𝑊 substr ⟨𝐼, (𝐼 + 2)⟩)⟩)) = (𝐺 Σg 𝑊))
15122adantr 479 . . . . . . 7 ((𝜑 ∧ ((𝑟𝑇𝑠𝑇) ∧ (((𝑊𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → (𝐺 Σg 𝑊) = ( I ↾ 𝐷))
152149, 150, 1513eqtrd 2647 . . . . . 6 ((𝜑 ∧ ((𝑟𝑇𝑠𝑇) ∧ (((𝑊𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → (𝐺 Σg (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)) = ( I ↾ 𝐷))
15318adantr 479 . . . . . . . . 9 ((𝜑 ∧ (𝑟𝑇𝑠𝑇)) → 𝐼 ∈ (0...(𝐼 + 2)))
15436adantr 479 . . . . . . . . 9 ((𝜑 ∧ (𝑟𝑇𝑠𝑇)) → (𝐼 + 2) ∈ (0...(#‘𝑊)))
155120, 153, 154, 123spllen 13302 . . . . . . . 8 ((𝜑 ∧ (𝑟𝑇𝑠𝑇)) → (#‘(𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)) = ((#‘𝑊) + ((#‘⟨“𝑟𝑠”⟩) − ((𝐼 + 2) − 𝐼))))
156 s2len 13430 . . . . . . . . . . . . 13 (#‘⟨“𝑟𝑠”⟩) = 2
157156oveq1i 6537 . . . . . . . . . . . 12 ((#‘⟨“𝑟𝑠”⟩) − ((𝐼 + 2) − 𝐼)) = (2 − ((𝐼 + 2) − 𝐼))
15845oveq2d 6543 . . . . . . . . . . . . 13 (𝜑 → (2 − ((𝐼 + 2) − 𝐼)) = (2 − 2))
15943subidi 10203 . . . . . . . . . . . . 13 (2 − 2) = 0
160158, 159syl6eq 2659 . . . . . . . . . . . 12 (𝜑 → (2 − ((𝐼 + 2) − 𝐼)) = 0)
161157, 160syl5eq 2655 . . . . . . . . . . 11 (𝜑 → ((#‘⟨“𝑟𝑠”⟩) − ((𝐼 + 2) − 𝐼)) = 0)
162161oveq2d 6543 . . . . . . . . . 10 (𝜑 → ((#‘𝑊) + ((#‘⟨“𝑟𝑠”⟩) − ((𝐼 + 2) − 𝐼))) = ((#‘𝑊) + 0))
16323, 51eqeltrd 2687 . . . . . . . . . . 11 (𝜑 → (#‘𝑊) ∈ ℂ)
164163addid1d 10087 . . . . . . . . . 10 (𝜑 → ((#‘𝑊) + 0) = (#‘𝑊))
165162, 164, 233eqtrd 2647 . . . . . . . . 9 (𝜑 → ((#‘𝑊) + ((#‘⟨“𝑟𝑠”⟩) − ((𝐼 + 2) − 𝐼))) = 𝐿)
166165adantr 479 . . . . . . . 8 ((𝜑 ∧ (𝑟𝑇𝑠𝑇)) → ((#‘𝑊) + ((#‘⟨“𝑟𝑠”⟩) − ((𝐼 + 2) − 𝐼))) = 𝐿)
167155, 166eqtrd 2643 . . . . . . 7 ((𝜑 ∧ (𝑟𝑇𝑠𝑇)) → (#‘(𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)) = 𝐿)
168167adantrr 748 . . . . . 6 ((𝜑 ∧ ((𝑟𝑇𝑠𝑇) ∧ (((𝑊𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → (#‘(𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)) = 𝐿)
169152, 168jca 552 . . . . 5 ((𝜑 ∧ ((𝑟𝑇𝑠𝑇) ∧ (((𝑊𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → ((𝐺 Σg (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)) = ( I ↾ 𝐷) ∧ (#‘(𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)) = 𝐿))
17026adantr 479 . . . . . 6 ((𝜑 ∧ ((𝑟𝑇𝑠𝑇) ∧ (((𝑊𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → (𝐼 + 1) ∈ (0..^𝐿))
171 simprr2 1102 . . . . . . 7 ((𝜑 ∧ ((𝑟𝑇𝑠𝑇) ∧ (((𝑊𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → 𝐴 ∈ dom (𝑠 ∖ I ))
172 1nn0 11155 . . . . . . . . . . . . . . 15 1 ∈ ℕ0
173 2nn 11032 . . . . . . . . . . . . . . 15 2 ∈ ℕ
174 1lt2 11041 . . . . . . . . . . . . . . 15 1 < 2
175 elfzo0 12331 . . . . . . . . . . . . . . 15 (1 ∈ (0..^2) ↔ (1 ∈ ℕ0 ∧ 2 ∈ ℕ ∧ 1 < 2))
176172, 173, 174, 175mpbir3an 1236 . . . . . . . . . . . . . 14 1 ∈ (0..^2)
177156oveq2i 6538 . . . . . . . . . . . . . 14 (0..^(#‘⟨“𝑟𝑠”⟩)) = (0..^2)
178176, 177eleqtrri 2686 . . . . . . . . . . . . 13 1 ∈ (0..^(#‘⟨“𝑟𝑠”⟩))
179178a1i 11 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑟𝑇𝑠𝑇)) → 1 ∈ (0..^(#‘⟨“𝑟𝑠”⟩)))
180120, 153, 154, 123, 179splfv2a 13304 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟𝑇𝑠𝑇)) → ((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘(𝐼 + 1)) = (⟨“𝑟𝑠”⟩‘1))
181 s2fv1 13429 . . . . . . . . . . . 12 (𝑠𝑇 → (⟨“𝑟𝑠”⟩‘1) = 𝑠)
182181ad2antll 760 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟𝑇𝑠𝑇)) → (⟨“𝑟𝑠”⟩‘1) = 𝑠)
183180, 182eqtrd 2643 . . . . . . . . . 10 ((𝜑 ∧ (𝑟𝑇𝑠𝑇)) → ((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘(𝐼 + 1)) = 𝑠)
184183adantrr 748 . . . . . . . . 9 ((𝜑 ∧ ((𝑟𝑇𝑠𝑇) ∧ (((𝑊𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → ((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘(𝐼 + 1)) = 𝑠)
185184difeq1d 3688 . . . . . . . 8 ((𝜑 ∧ ((𝑟𝑇𝑠𝑇) ∧ (((𝑊𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘(𝐼 + 1)) ∖ I ) = (𝑠 ∖ I ))
186185dmeqd 5235 . . . . . . 7 ((𝜑 ∧ ((𝑟𝑇𝑠𝑇) ∧ (((𝑊𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘(𝐼 + 1)) ∖ I ) = dom (𝑠 ∖ I ))
187171, 186eleqtrrd 2690 . . . . . 6 ((𝜑 ∧ ((𝑟𝑇𝑠𝑇) ∧ (((𝑊𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → 𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘(𝐼 + 1)) ∖ I ))
188 fzosplitsni 12399 . . . . . . . . . . 11 (𝐼 ∈ (ℤ‘0) → (𝑗 ∈ (0..^(𝐼 + 1)) ↔ (𝑗 ∈ (0..^𝐼) ∨ 𝑗 = 𝐼)))
189 nn0uz 11554 . . . . . . . . . . 11 0 = (ℤ‘0)
190188, 189eleq2s 2705 . . . . . . . . . 10 (𝐼 ∈ ℕ0 → (𝑗 ∈ (0..^(𝐼 + 1)) ↔ (𝑗 ∈ (0..^𝐼) ∨ 𝑗 = 𝐼)))
19110, 190syl 17 . . . . . . . . 9 (𝜑 → (𝑗 ∈ (0..^(𝐼 + 1)) ↔ (𝑗 ∈ (0..^𝐼) ∨ 𝑗 = 𝐼)))
192191adantr 479 . . . . . . . 8 ((𝜑 ∧ ((𝑟𝑇𝑠𝑇) ∧ (((𝑊𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → (𝑗 ∈ (0..^(𝐼 + 1)) ↔ (𝑗 ∈ (0..^𝐼) ∨ 𝑗 = 𝐼)))
193 fveq2 6088 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 𝑗 → (𝑊𝑘) = (𝑊𝑗))
194193difeq1d 3688 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑗 → ((𝑊𝑘) ∖ I ) = ((𝑊𝑗) ∖ I ))
195194dmeqd 5235 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑗 → dom ((𝑊𝑘) ∖ I ) = dom ((𝑊𝑗) ∖ I ))
196195eleq2d 2672 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑗 → (𝐴 ∈ dom ((𝑊𝑘) ∖ I ) ↔ 𝐴 ∈ dom ((𝑊𝑗) ∖ I )))
197196notbid 306 . . . . . . . . . . . . . . 15 (𝑘 = 𝑗 → (¬ 𝐴 ∈ dom ((𝑊𝑘) ∖ I ) ↔ ¬ 𝐴 ∈ dom ((𝑊𝑗) ∖ I )))
198197rspccva 3280 . . . . . . . . . . . . . 14 ((∀𝑘 ∈ (0..^𝐼) ¬ 𝐴 ∈ dom ((𝑊𝑘) ∖ I ) ∧ 𝑗 ∈ (0..^𝐼)) → ¬ 𝐴 ∈ dom ((𝑊𝑗) ∖ I ))
19925, 198sylan 486 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0..^𝐼)) → ¬ 𝐴 ∈ dom ((𝑊𝑗) ∖ I ))
200199adantlr 746 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑟𝑇𝑠𝑇)) ∧ 𝑗 ∈ (0..^𝐼)) → ¬ 𝐴 ∈ dom ((𝑊𝑗) ∖ I ))
2011ad2antrr 757 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑟𝑇𝑠𝑇)) ∧ 𝑗 ∈ (0..^𝐼)) → 𝑊 ∈ Word 𝑇)
20218ad2antrr 757 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑟𝑇𝑠𝑇)) ∧ 𝑗 ∈ (0..^𝐼)) → 𝐼 ∈ (0...(𝐼 + 2)))
20336ad2antrr 757 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑟𝑇𝑠𝑇)) ∧ 𝑗 ∈ (0..^𝐼)) → (𝐼 + 2) ∈ (0...(#‘𝑊)))
204123adantr 479 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑟𝑇𝑠𝑇)) ∧ 𝑗 ∈ (0..^𝐼)) → ⟨“𝑟𝑠”⟩ ∈ Word 𝑇)
205 simpr 475 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑟𝑇𝑠𝑇)) ∧ 𝑗 ∈ (0..^𝐼)) → 𝑗 ∈ (0..^𝐼))
206201, 202, 203, 204, 205splfv1 13303 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑟𝑇𝑠𝑇)) ∧ 𝑗 ∈ (0..^𝐼)) → ((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) = (𝑊𝑗))
207206difeq1d 3688 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑟𝑇𝑠𝑇)) ∧ 𝑗 ∈ (0..^𝐼)) → (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) ∖ I ) = ((𝑊𝑗) ∖ I ))
208207dmeqd 5235 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑟𝑇𝑠𝑇)) ∧ 𝑗 ∈ (0..^𝐼)) → dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) ∖ I ) = dom ((𝑊𝑗) ∖ I ))
209200, 208neleqtrrd 2709 . . . . . . . . . . 11 (((𝜑 ∧ (𝑟𝑇𝑠𝑇)) ∧ 𝑗 ∈ (0..^𝐼)) → ¬ 𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) ∖ I ))
210209ex 448 . . . . . . . . . 10 ((𝜑 ∧ (𝑟𝑇𝑠𝑇)) → (𝑗 ∈ (0..^𝐼) → ¬ 𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) ∖ I )))
211210adantrr 748 . . . . . . . . 9 ((𝜑 ∧ ((𝑟𝑇𝑠𝑇) ∧ (((𝑊𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → (𝑗 ∈ (0..^𝐼) → ¬ 𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) ∖ I )))
212 simprr3 1103 . . . . . . . . . . 11 ((𝜑 ∧ ((𝑟𝑇𝑠𝑇) ∧ (((𝑊𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → ¬ 𝐴 ∈ dom (𝑟 ∖ I ))
213 0nn0 11154 . . . . . . . . . . . . . . . . . . . 20 0 ∈ ℕ0
214 2pos 10959 . . . . . . . . . . . . . . . . . . . 20 0 < 2
215 elfzo0 12331 . . . . . . . . . . . . . . . . . . . 20 (0 ∈ (0..^2) ↔ (0 ∈ ℕ0 ∧ 2 ∈ ℕ ∧ 0 < 2))
216213, 173, 214, 215mpbir3an 1236 . . . . . . . . . . . . . . . . . . 19 0 ∈ (0..^2)
217216, 177eleqtrri 2686 . . . . . . . . . . . . . . . . . 18 0 ∈ (0..^(#‘⟨“𝑟𝑠”⟩))
218217a1i 11 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑟𝑇𝑠𝑇)) → 0 ∈ (0..^(#‘⟨“𝑟𝑠”⟩)))
219120, 153, 154, 123, 218splfv2a 13304 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑟𝑇𝑠𝑇)) → ((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘(𝐼 + 0)) = (⟨“𝑟𝑠”⟩‘0))
22029addid1d 10087 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐼 + 0) = 𝐼)
221220adantr 479 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑟𝑇𝑠𝑇)) → (𝐼 + 0) = 𝐼)
222221fveq2d 6092 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑟𝑇𝑠𝑇)) → ((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘(𝐼 + 0)) = ((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝐼))
223 s2fv0 13428 . . . . . . . . . . . . . . . . 17 (𝑟𝑇 → (⟨“𝑟𝑠”⟩‘0) = 𝑟)
224223ad2antrl 759 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑟𝑇𝑠𝑇)) → (⟨“𝑟𝑠”⟩‘0) = 𝑟)
225219, 222, 2243eqtr3d 2651 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑟𝑇𝑠𝑇)) → ((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝐼) = 𝑟)
226225difeq1d 3688 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑟𝑇𝑠𝑇)) → (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝐼) ∖ I ) = (𝑟 ∖ I ))
227226dmeqd 5235 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑟𝑇𝑠𝑇)) → dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝐼) ∖ I ) = dom (𝑟 ∖ I ))
228227eleq2d 2672 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑟𝑇𝑠𝑇)) → (𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝐼) ∖ I ) ↔ 𝐴 ∈ dom (𝑟 ∖ I )))
229228adantrr 748 . . . . . . . . . . 11 ((𝜑 ∧ ((𝑟𝑇𝑠𝑇) ∧ (((𝑊𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → (𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝐼) ∖ I ) ↔ 𝐴 ∈ dom (𝑟 ∖ I )))
230212, 229mtbird 313 . . . . . . . . . 10 ((𝜑 ∧ ((𝑟𝑇𝑠𝑇) ∧ (((𝑊𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → ¬ 𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝐼) ∖ I ))
231 fveq2 6088 . . . . . . . . . . . . . 14 (𝑗 = 𝐼 → ((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) = ((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝐼))
232231difeq1d 3688 . . . . . . . . . . . . 13 (𝑗 = 𝐼 → (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) ∖ I ) = (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝐼) ∖ I ))
233232dmeqd 5235 . . . . . . . . . . . 12 (𝑗 = 𝐼 → dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) ∖ I ) = dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝐼) ∖ I ))
234233eleq2d 2672 . . . . . . . . . . 11 (𝑗 = 𝐼 → (𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) ∖ I ) ↔ 𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝐼) ∖ I )))
235234notbid 306 . . . . . . . . . 10 (𝑗 = 𝐼 → (¬ 𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) ∖ I ) ↔ ¬ 𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝐼) ∖ I )))
236230, 235syl5ibrcom 235 . . . . . . . . 9 ((𝜑 ∧ ((𝑟𝑇𝑠𝑇) ∧ (((𝑊𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → (𝑗 = 𝐼 → ¬ 𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) ∖ I )))
237211, 236jaod 393 . . . . . . . 8 ((𝜑 ∧ ((𝑟𝑇𝑠𝑇) ∧ (((𝑊𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → ((𝑗 ∈ (0..^𝐼) ∨ 𝑗 = 𝐼) → ¬ 𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) ∖ I )))
238192, 237sylbid 228 . . . . . . 7 ((𝜑 ∧ ((𝑟𝑇𝑠𝑇) ∧ (((𝑊𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → (𝑗 ∈ (0..^(𝐼 + 1)) → ¬ 𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) ∖ I )))
239238ralrimiv 2947 . . . . . 6 ((𝜑 ∧ ((𝑟𝑇𝑠𝑇) ∧ (((𝑊𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → ∀𝑗 ∈ (0..^(𝐼 + 1)) ¬ 𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) ∖ I ))
240170, 187, 2393jca 1234 . . . . 5 ((𝜑 ∧ ((𝑟𝑇𝑠𝑇) ∧ (((𝑊𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → ((𝐼 + 1) ∈ (0..^𝐿) ∧ 𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘(𝐼 + 1)) ∖ I ) ∧ ∀𝑗 ∈ (0..^(𝐼 + 1)) ¬ 𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) ∖ I )))
241 oveq2 6535 . . . . . . . . 9 (𝑤 = (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩) → (𝐺 Σg 𝑤) = (𝐺 Σg (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)))
242241eqeq1d 2611 . . . . . . . 8 (𝑤 = (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩) → ((𝐺 Σg 𝑤) = ( I ↾ 𝐷) ↔ (𝐺 Σg (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)) = ( I ↾ 𝐷)))
243 fveq2 6088 . . . . . . . . 9 (𝑤 = (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩) → (#‘𝑤) = (#‘(𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)))
244243eqeq1d 2611 . . . . . . . 8 (𝑤 = (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩) → ((#‘𝑤) = 𝐿 ↔ (#‘(𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)) = 𝐿))
245242, 244anbi12d 742 . . . . . . 7 (𝑤 = (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩) → (((𝐺 Σg 𝑤) = ( I ↾ 𝐷) ∧ (#‘𝑤) = 𝐿) ↔ ((𝐺 Σg (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)) = ( I ↾ 𝐷) ∧ (#‘(𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)) = 𝐿)))
246 fveq1 6087 . . . . . . . . . . 11 (𝑤 = (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩) → (𝑤‘(𝐼 + 1)) = ((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘(𝐼 + 1)))
247246difeq1d 3688 . . . . . . . . . 10 (𝑤 = (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩) → ((𝑤‘(𝐼 + 1)) ∖ I ) = (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘(𝐼 + 1)) ∖ I ))
248247dmeqd 5235 . . . . . . . . 9 (𝑤 = (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩) → dom ((𝑤‘(𝐼 + 1)) ∖ I ) = dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘(𝐼 + 1)) ∖ I ))
249248eleq2d 2672 . . . . . . . 8 (𝑤 = (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩) → (𝐴 ∈ dom ((𝑤‘(𝐼 + 1)) ∖ I ) ↔ 𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘(𝐼 + 1)) ∖ I )))
250 fveq1 6087 . . . . . . . . . . . . 13 (𝑤 = (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩) → (𝑤𝑗) = ((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗))
251250difeq1d 3688 . . . . . . . . . . . 12 (𝑤 = (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩) → ((𝑤𝑗) ∖ I ) = (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) ∖ I ))
252251dmeqd 5235 . . . . . . . . . . 11 (𝑤 = (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩) → dom ((𝑤𝑗) ∖ I ) = dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) ∖ I ))
253252eleq2d 2672 . . . . . . . . . 10 (𝑤 = (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩) → (𝐴 ∈ dom ((𝑤𝑗) ∖ I ) ↔ 𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) ∖ I )))
254253notbid 306 . . . . . . . . 9 (𝑤 = (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩) → (¬ 𝐴 ∈ dom ((𝑤𝑗) ∖ I ) ↔ ¬ 𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) ∖ I )))
255254ralbidv 2968 . . . . . . . 8 (𝑤 = (𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩) → (∀𝑗 ∈ (0..^(𝐼 + 1)) ¬ 𝐴 ∈ dom ((𝑤𝑗) ∖ I ) ↔ ∀𝑗 ∈ (0..^(𝐼 + 1)) ¬ 𝐴 ∈ dom (((𝑊 splice ⟨𝐼, (𝐼 + 2), ⟨“𝑟𝑠”⟩⟩)‘𝑗) ∖ I )))
256249, 2553anbi23d 1393 . . . . . . 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 742 . . . . . 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 3281 . . . . 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 1315 . . . 4 ((𝜑 ∧ ((𝑟𝑇𝑠𝑇) ∧ (((𝑊𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) → ∃𝑤 ∈ Word 𝑇(((𝐺 Σg 𝑤) = ( I ↾ 𝐷) ∧ (#‘𝑤) = 𝐿) ∧ ((𝐼 + 1) ∈ (0..^𝐿) ∧ 𝐴 ∈ dom ((𝑤‘(𝐼 + 1)) ∖ I ) ∧ ∀𝑗 ∈ (0..^(𝐼 + 1)) ¬ 𝐴 ∈ dom ((𝑤𝑗) ∖ I ))))
260259expr 640 . . 3 ((𝜑 ∧ (𝑟𝑇𝑠𝑇)) → ((((𝑊𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )) → ∃𝑤 ∈ Word 𝑇(((𝐺 Σg 𝑤) = ( I ↾ 𝐷) ∧ (#‘𝑤) = 𝐿) ∧ ((𝐼 + 1) ∈ (0..^𝐿) ∧ 𝐴 ∈ dom ((𝑤‘(𝐼 + 1)) ∖ I ) ∧ ∀𝑗 ∈ (0..^(𝐼 + 1)) ¬ 𝐴 ∈ dom ((𝑤𝑗) ∖ I )))))
261260rexlimdvva 3019 . 2 (𝜑 → (∃𝑟𝑇𝑠𝑇 (((𝑊𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )) → ∃𝑤 ∈ Word 𝑇(((𝐺 Σg 𝑤) = ( I ↾ 𝐷) ∧ (#‘𝑤) = 𝐿) ∧ ((𝐼 + 1) ∈ (0..^𝐿) ∧ 𝐴 ∈ dom ((𝑤‘(𝐼 + 1)) ∖ I ) ∧ ∀𝑗 ∈ (0..^(𝐼 + 1)) ¬ 𝐴 ∈ dom ((𝑤𝑗) ∖ I )))))
26220, 21, 87, 89, 24psgnunilem1 17682 . 2 (𝜑 → (((𝑊𝐼) ∘ (𝑊‘(𝐼 + 1))) = ( I ↾ 𝐷) ∨ ∃𝑟𝑇𝑠𝑇 (((𝑊𝐼) ∘ (𝑊‘(𝐼 + 1))) = (𝑟𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I ))))
263119, 261, 262mpjaod 394 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 194  wo 381  wa 382  w3a 1030   = wceq 1474  wcel 1976  wral 2895  wrex 2896  cdif 3536  wss 3539  c0 3873  cop 4130  cotp 4132   class class class wbr 4577   I cid 4938  dom cdm 5028  ran crn 5029  cres 5030  ccom 5032  wf 5786  cfv 5790  (class class class)co 6527  cc 9790  cr 9791  0cc0 9792  1c1 9793   + caddc 9795   < clt 9930  cle 9931  cmin 10117  -cneg 10118  cn 10867  2c2 10917  0cn0 11139  cz 11210  cuz 11519  ...cfz 12152  ..^cfzo 12289  #chash 12934  Word cword 13092   substr csubstr 13096   splice csplice 13097  ⟨“cs2 13383  Basecbs 15641  +gcplusg 15714  0gc0g 15869   Σg cgsu 15870  Mndcmnd 17063  Grpcgrp 17191  SymGrpcsymg 17566  pmTrspcpmtr 17630
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-rep 4693  ax-sep 4703  ax-nul 4712  ax-pow 4764  ax-pr 4828  ax-un 6824  ax-cnex 9848  ax-resscn 9849  ax-1cn 9850  ax-icn 9851  ax-addcl 9852  ax-addrcl 9853  ax-mulcl 9854  ax-mulrcl 9855  ax-mulcom 9856  ax-addass 9857  ax-mulass 9858  ax-distr 9859  ax-i2m1 9860  ax-1ne0 9861  ax-1rid 9862  ax-rnegex 9863  ax-rrecex 9864  ax-cnre 9865  ax-pre-lttri 9866  ax-pre-lttrn 9867  ax-pre-ltadd 9868  ax-pre-mulgt0 9869
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-xor 1456  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-nel 2782  df-ral 2900  df-rex 2901  df-reu 2902  df-rmo 2903  df-rab 2904  df-v 3174  df-sbc 3402  df-csb 3499  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-pss 3555  df-nul 3874  df-if 4036  df-pw 4109  df-sn 4125  df-pr 4127  df-tp 4129  df-op 4131  df-ot 4133  df-uni 4367  df-int 4405  df-iun 4451  df-br 4578  df-opab 4638  df-mpt 4639  df-tr 4675  df-eprel 4939  df-id 4943  df-po 4949  df-so 4950  df-fr 4987  df-we 4989  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-rn 5039  df-res 5040  df-ima 5041  df-pred 5583  df-ord 5629  df-on 5630  df-lim 5631  df-suc 5632  df-iota 5754  df-fun 5792  df-fn 5793  df-f 5794  df-f1 5795  df-fo 5796  df-f1o 5797  df-fv 5798  df-riota 6489  df-ov 6530  df-oprab 6531  df-mpt2 6532  df-om 6935  df-1st 7036  df-2nd 7037  df-wrecs 7271  df-recs 7332  df-rdg 7370  df-1o 7424  df-2o 7425  df-oadd 7428  df-er 7606  df-map 7723  df-en 7819  df-dom 7820  df-sdom 7821  df-fin 7822  df-card 8625  df-pnf 9932  df-mnf 9933  df-xr 9934  df-ltxr 9935  df-le 9936  df-sub 10119  df-neg 10120  df-nn 10868  df-2 10926  df-3 10927  df-4 10928  df-5 10929  df-6 10930  df-7 10931  df-8 10932  df-9 10933  df-n0 11140  df-z 11211  df-uz 11520  df-fz 12153  df-fzo 12290  df-seq 12619  df-hash 12935  df-word 13100  df-lsw 13101  df-concat 13102  df-s1 13103  df-substr 13104  df-splice 13105  df-s2 13390  df-struct 15643  df-ndx 15644  df-slot 15645  df-base 15646  df-sets 15647  df-ress 15648  df-plusg 15727  df-tset 15733  df-0g 15871  df-gsum 15872  df-mgm 17011  df-sgrp 17053  df-mnd 17064  df-submnd 17105  df-grp 17194  df-minusg 17195  df-subg 17360  df-symg 17567  df-pmtr 17631
This theorem is referenced by:  psgnunilem3  17685
  Copyright terms: Public domain W3C validator