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

Theorem frgpuplem 18467
Description: Any assignment of the generators to target elements can be extended (uniquely) to a homomorphism from a free monoid to an arbitrary other monoid. (Contributed by Mario Carneiro, 2-Oct-2015.)
Hypotheses
Ref Expression
frgpup.b 𝐵 = (Base‘𝐻)
frgpup.n 𝑁 = (invg𝐻)
frgpup.t 𝑇 = (𝑦𝐼, 𝑧 ∈ 2𝑜 ↦ if(𝑧 = ∅, (𝐹𝑦), (𝑁‘(𝐹𝑦))))
frgpup.h (𝜑𝐻 ∈ Grp)
frgpup.i (𝜑𝐼𝑉)
frgpup.a (𝜑𝐹:𝐼𝐵)
frgpup.w 𝑊 = ( I ‘Word (𝐼 × 2𝑜))
frgpup.r = ( ~FG𝐼)
Assertion
Ref Expression
frgpuplem ((𝜑𝐴 𝐶) → (𝐻 Σg (𝑇𝐴)) = (𝐻 Σg (𝑇𝐶)))
Distinct variable groups:   𝑦,𝑧,𝐴   𝑦,𝐹,𝑧   𝑦,𝑁,𝑧   𝑦,𝐵,𝑧   𝜑,𝑦,𝑧   𝑦,𝐼,𝑧
Allowed substitution hints:   𝐶(𝑦,𝑧)   (𝑦,𝑧)   𝑇(𝑦,𝑧)   𝐻(𝑦,𝑧)   𝑉(𝑦,𝑧)   𝑊(𝑦,𝑧)

Proof of Theorem frgpuplem
Dummy variables 𝑎 𝑏 𝑢 𝑣 𝑛 𝑟 𝑥 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 frgpup.w . . . . . . 7 𝑊 = ( I ‘Word (𝐼 × 2𝑜))
2 frgpup.r . . . . . . 7 = ( ~FG𝐼)
31, 2efgval 18410 . . . . . 6 = {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑥𝑊𝑛 ∈ (0...(♯‘𝑥))∀𝑎𝐼𝑏 ∈ 2𝑜 𝑥𝑟(𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩⟩))}
4 coeq2 5451 . . . . . . . . . . . . 13 (𝑢 = 𝑣 → (𝑇𝑢) = (𝑇𝑣))
54oveq2d 6862 . . . . . . . . . . . 12 (𝑢 = 𝑣 → (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))
6 eqid 2765 . . . . . . . . . . . 12 {⟨𝑢, 𝑣⟩ ∣ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣))} = {⟨𝑢, 𝑣⟩ ∣ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣))}
75, 6eqer 7986 . . . . . . . . . . 11 {⟨𝑢, 𝑣⟩ ∣ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣))} Er V
87a1i 11 . . . . . . . . . 10 (𝜑 → {⟨𝑢, 𝑣⟩ ∣ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣))} Er V)
9 ssv 3787 . . . . . . . . . . 11 𝑊 ⊆ V
109a1i 11 . . . . . . . . . 10 (𝜑𝑊 ⊆ V)
118, 10erinxp 8028 . . . . . . . . 9 (𝜑 → ({⟨𝑢, 𝑣⟩ ∣ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣))} ∩ (𝑊 × 𝑊)) Er 𝑊)
12 df-xp 5285 . . . . . . . . . . . . 13 (𝑊 × 𝑊) = {⟨𝑢, 𝑣⟩ ∣ (𝑢𝑊𝑣𝑊)}
1312ineq1i 3974 . . . . . . . . . . . 12 ((𝑊 × 𝑊) ∩ {⟨𝑢, 𝑣⟩ ∣ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣))}) = ({⟨𝑢, 𝑣⟩ ∣ (𝑢𝑊𝑣𝑊)} ∩ {⟨𝑢, 𝑣⟩ ∣ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣))})
14 incom 3969 . . . . . . . . . . . 12 ((𝑊 × 𝑊) ∩ {⟨𝑢, 𝑣⟩ ∣ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣))}) = ({⟨𝑢, 𝑣⟩ ∣ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣))} ∩ (𝑊 × 𝑊))
15 inopab 5423 . . . . . . . . . . . 12 ({⟨𝑢, 𝑣⟩ ∣ (𝑢𝑊𝑣𝑊)} ∩ {⟨𝑢, 𝑣⟩ ∣ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣))}) = {⟨𝑢, 𝑣⟩ ∣ ((𝑢𝑊𝑣𝑊) ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))}
1613, 14, 153eqtr3i 2795 . . . . . . . . . . 11 ({⟨𝑢, 𝑣⟩ ∣ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣))} ∩ (𝑊 × 𝑊)) = {⟨𝑢, 𝑣⟩ ∣ ((𝑢𝑊𝑣𝑊) ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))}
17 vex 3353 . . . . . . . . . . . . . 14 𝑢 ∈ V
18 vex 3353 . . . . . . . . . . . . . 14 𝑣 ∈ V
1917, 18prss 4507 . . . . . . . . . . . . 13 ((𝑢𝑊𝑣𝑊) ↔ {𝑢, 𝑣} ⊆ 𝑊)
2019anbi1i 617 . . . . . . . . . . . 12 (((𝑢𝑊𝑣𝑊) ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣))) ↔ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣))))
2120opabbii 4878 . . . . . . . . . . 11 {⟨𝑢, 𝑣⟩ ∣ ((𝑢𝑊𝑣𝑊) ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))} = {⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))}
2216, 21eqtri 2787 . . . . . . . . . 10 ({⟨𝑢, 𝑣⟩ ∣ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣))} ∩ (𝑊 × 𝑊)) = {⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))}
23 ereq1 7958 . . . . . . . . . 10 (({⟨𝑢, 𝑣⟩ ∣ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣))} ∩ (𝑊 × 𝑊)) = {⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))} → (({⟨𝑢, 𝑣⟩ ∣ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣))} ∩ (𝑊 × 𝑊)) Er 𝑊 ↔ {⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))} Er 𝑊))
2422, 23ax-mp 5 . . . . . . . . 9 (({⟨𝑢, 𝑣⟩ ∣ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣))} ∩ (𝑊 × 𝑊)) Er 𝑊 ↔ {⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))} Er 𝑊)
2511, 24sylib 209 . . . . . . . 8 (𝜑 → {⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))} Er 𝑊)
26 simplrl 795 . . . . . . . . . . 11 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → 𝑥𝑊)
27 fviss 6449 . . . . . . . . . . . . . . 15 ( I ‘Word (𝐼 × 2𝑜)) ⊆ Word (𝐼 × 2𝑜)
281, 27eqsstri 3797 . . . . . . . . . . . . . 14 𝑊 ⊆ Word (𝐼 × 2𝑜)
2928, 26sseldi 3761 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → 𝑥 ∈ Word (𝐼 × 2𝑜))
30 opelxpi 5316 . . . . . . . . . . . . . . 15 ((𝑎𝐼𝑏 ∈ 2𝑜) → ⟨𝑎, 𝑏⟩ ∈ (𝐼 × 2𝑜))
3130adantl 473 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → ⟨𝑎, 𝑏⟩ ∈ (𝐼 × 2𝑜))
32 simprl 787 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → 𝑎𝐼)
33 2oconcl 7792 . . . . . . . . . . . . . . . 16 (𝑏 ∈ 2𝑜 → (1𝑜𝑏) ∈ 2𝑜)
3433ad2antll 720 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → (1𝑜𝑏) ∈ 2𝑜)
3532, 34opelxpd 5317 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → ⟨𝑎, (1𝑜𝑏)⟩ ∈ (𝐼 × 2𝑜))
3631, 35s2cld 13916 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩ ∈ Word (𝐼 × 2𝑜))
37 splcl 13786 . . . . . . . . . . . . 13 ((𝑥 ∈ Word (𝐼 × 2𝑜) ∧ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩ ∈ Word (𝐼 × 2𝑜)) → (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩⟩) ∈ Word (𝐼 × 2𝑜))
3829, 36, 37syl2anc 579 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩⟩) ∈ Word (𝐼 × 2𝑜))
391efgrcl 18408 . . . . . . . . . . . . . 14 (𝑥𝑊 → (𝐼 ∈ V ∧ 𝑊 = Word (𝐼 × 2𝑜)))
4026, 39syl 17 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → (𝐼 ∈ V ∧ 𝑊 = Word (𝐼 × 2𝑜)))
4140simprd 489 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → 𝑊 = Word (𝐼 × 2𝑜))
4238, 41eleqtrrd 2847 . . . . . . . . . . 11 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩⟩) ∈ 𝑊)
43 pfxcl 13680 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ Word (𝐼 × 2𝑜) → (𝑥 prefix 𝑛) ∈ Word (𝐼 × 2𝑜))
4429, 43syl 17 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → (𝑥 prefix 𝑛) ∈ Word (𝐼 × 2𝑜))
45 frgpup.b . . . . . . . . . . . . . . . . . . 19 𝐵 = (Base‘𝐻)
46 frgpup.n . . . . . . . . . . . . . . . . . . 19 𝑁 = (invg𝐻)
47 frgpup.t . . . . . . . . . . . . . . . . . . 19 𝑇 = (𝑦𝐼, 𝑧 ∈ 2𝑜 ↦ if(𝑧 = ∅, (𝐹𝑦), (𝑁‘(𝐹𝑦))))
48 frgpup.h . . . . . . . . . . . . . . . . . . 19 (𝜑𝐻 ∈ Grp)
49 frgpup.i . . . . . . . . . . . . . . . . . . 19 (𝜑𝐼𝑉)
50 frgpup.a . . . . . . . . . . . . . . . . . . 19 (𝜑𝐹:𝐼𝐵)
5145, 46, 47, 48, 49, 50frgpuptf 18465 . . . . . . . . . . . . . . . . . 18 (𝜑𝑇:(𝐼 × 2𝑜)⟶𝐵)
5251ad2antrr 717 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → 𝑇:(𝐼 × 2𝑜)⟶𝐵)
53 ccatco 13880 . . . . . . . . . . . . . . . . 17 (((𝑥 prefix 𝑛) ∈ Word (𝐼 × 2𝑜) ∧ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩ ∈ Word (𝐼 × 2𝑜) ∧ 𝑇:(𝐼 × 2𝑜)⟶𝐵) → (𝑇 ∘ ((𝑥 prefix 𝑛) ++ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩)) = ((𝑇 ∘ (𝑥 prefix 𝑛)) ++ (𝑇 ∘ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩)))
5444, 36, 52, 53syl3anc 1490 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → (𝑇 ∘ ((𝑥 prefix 𝑛) ++ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩)) = ((𝑇 ∘ (𝑥 prefix 𝑛)) ++ (𝑇 ∘ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩)))
5554oveq2d 6862 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → (𝐻 Σg (𝑇 ∘ ((𝑥 prefix 𝑛) ++ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩))) = (𝐻 Σg ((𝑇 ∘ (𝑥 prefix 𝑛)) ++ (𝑇 ∘ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩))))
5648ad2antrr 717 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → 𝐻 ∈ Grp)
57 grpmnd 17712 . . . . . . . . . . . . . . . . 17 (𝐻 ∈ Grp → 𝐻 ∈ Mnd)
5856, 57syl 17 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → 𝐻 ∈ Mnd)
59 wrdco 13876 . . . . . . . . . . . . . . . . 17 (((𝑥 prefix 𝑛) ∈ Word (𝐼 × 2𝑜) ∧ 𝑇:(𝐼 × 2𝑜)⟶𝐵) → (𝑇 ∘ (𝑥 prefix 𝑛)) ∈ Word 𝐵)
6044, 52, 59syl2anc 579 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → (𝑇 ∘ (𝑥 prefix 𝑛)) ∈ Word 𝐵)
61 wrdco 13876 . . . . . . . . . . . . . . . . 17 ((⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩ ∈ Word (𝐼 × 2𝑜) ∧ 𝑇:(𝐼 × 2𝑜)⟶𝐵) → (𝑇 ∘ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩) ∈ Word 𝐵)
6236, 52, 61syl2anc 579 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → (𝑇 ∘ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩) ∈ Word 𝐵)
63 eqid 2765 . . . . . . . . . . . . . . . . 17 (+g𝐻) = (+g𝐻)
6445, 63gsumccat 17660 . . . . . . . . . . . . . . . 16 ((𝐻 ∈ Mnd ∧ (𝑇 ∘ (𝑥 prefix 𝑛)) ∈ Word 𝐵 ∧ (𝑇 ∘ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩) ∈ Word 𝐵) → (𝐻 Σg ((𝑇 ∘ (𝑥 prefix 𝑛)) ++ (𝑇 ∘ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩))) = ((𝐻 Σg (𝑇 ∘ (𝑥 prefix 𝑛)))(+g𝐻)(𝐻 Σg (𝑇 ∘ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩))))
6558, 60, 62, 64syl3anc 1490 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → (𝐻 Σg ((𝑇 ∘ (𝑥 prefix 𝑛)) ++ (𝑇 ∘ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩))) = ((𝐻 Σg (𝑇 ∘ (𝑥 prefix 𝑛)))(+g𝐻)(𝐻 Σg (𝑇 ∘ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩))))
6652, 31, 35s2co 13965 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → (𝑇 ∘ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩) = ⟨“(𝑇‘⟨𝑎, 𝑏⟩)(𝑇‘⟨𝑎, (1𝑜𝑏)⟩)”⟩)
67 df-ov 6849 . . . . . . . . . . . . . . . . . . . . . 22 (𝑎𝑇𝑏) = (𝑇‘⟨𝑎, 𝑏⟩)
6867a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → (𝑎𝑇𝑏) = (𝑇‘⟨𝑎, 𝑏⟩))
69 df-ov 6849 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑎(𝑦𝐼, 𝑧 ∈ 2𝑜 ↦ ⟨𝑦, (1𝑜𝑧)⟩)𝑏) = ((𝑦𝐼, 𝑧 ∈ 2𝑜 ↦ ⟨𝑦, (1𝑜𝑧)⟩)‘⟨𝑎, 𝑏⟩)
70 eqid 2765 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑦𝐼, 𝑧 ∈ 2𝑜 ↦ ⟨𝑦, (1𝑜𝑧)⟩) = (𝑦𝐼, 𝑧 ∈ 2𝑜 ↦ ⟨𝑦, (1𝑜𝑧)⟩)
7170efgmval 18405 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑎𝐼𝑏 ∈ 2𝑜) → (𝑎(𝑦𝐼, 𝑧 ∈ 2𝑜 ↦ ⟨𝑦, (1𝑜𝑧)⟩)𝑏) = ⟨𝑎, (1𝑜𝑏)⟩)
7269, 71syl5eqr 2813 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑎𝐼𝑏 ∈ 2𝑜) → ((𝑦𝐼, 𝑧 ∈ 2𝑜 ↦ ⟨𝑦, (1𝑜𝑧)⟩)‘⟨𝑎, 𝑏⟩) = ⟨𝑎, (1𝑜𝑏)⟩)
7372adantl 473 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → ((𝑦𝐼, 𝑧 ∈ 2𝑜 ↦ ⟨𝑦, (1𝑜𝑧)⟩)‘⟨𝑎, 𝑏⟩) = ⟨𝑎, (1𝑜𝑏)⟩)
7473fveq2d 6383 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → (𝑇‘((𝑦𝐼, 𝑧 ∈ 2𝑜 ↦ ⟨𝑦, (1𝑜𝑧)⟩)‘⟨𝑎, 𝑏⟩)) = (𝑇‘⟨𝑎, (1𝑜𝑏)⟩))
7545, 46, 47, 48, 49, 50, 70frgpuptinv 18466 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ ⟨𝑎, 𝑏⟩ ∈ (𝐼 × 2𝑜)) → (𝑇‘((𝑦𝐼, 𝑧 ∈ 2𝑜 ↦ ⟨𝑦, (1𝑜𝑧)⟩)‘⟨𝑎, 𝑏⟩)) = (𝑁‘(𝑇‘⟨𝑎, 𝑏⟩)))
7630, 75sylan2 586 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → (𝑇‘((𝑦𝐼, 𝑧 ∈ 2𝑜 ↦ ⟨𝑦, (1𝑜𝑧)⟩)‘⟨𝑎, 𝑏⟩)) = (𝑁‘(𝑇‘⟨𝑎, 𝑏⟩)))
7776adantlr 706 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → (𝑇‘((𝑦𝐼, 𝑧 ∈ 2𝑜 ↦ ⟨𝑦, (1𝑜𝑧)⟩)‘⟨𝑎, 𝑏⟩)) = (𝑁‘(𝑇‘⟨𝑎, 𝑏⟩)))
7874, 77eqtr3d 2801 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → (𝑇‘⟨𝑎, (1𝑜𝑏)⟩) = (𝑁‘(𝑇‘⟨𝑎, 𝑏⟩)))
7967fveq2i 6382 . . . . . . . . . . . . . . . . . . . . . 22 (𝑁‘(𝑎𝑇𝑏)) = (𝑁‘(𝑇‘⟨𝑎, 𝑏⟩))
8078, 79syl6reqr 2818 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → (𝑁‘(𝑎𝑇𝑏)) = (𝑇‘⟨𝑎, (1𝑜𝑏)⟩))
8168, 80s2eqd 13908 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → ⟨“(𝑎𝑇𝑏)(𝑁‘(𝑎𝑇𝑏))”⟩ = ⟨“(𝑇‘⟨𝑎, 𝑏⟩)(𝑇‘⟨𝑎, (1𝑜𝑏)⟩)”⟩)
8266, 81eqtr4d 2802 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → (𝑇 ∘ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩) = ⟨“(𝑎𝑇𝑏)(𝑁‘(𝑎𝑇𝑏))”⟩)
8382oveq2d 6862 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → (𝐻 Σg (𝑇 ∘ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩)) = (𝐻 Σg ⟨“(𝑎𝑇𝑏)(𝑁‘(𝑎𝑇𝑏))”⟩))
84 simprr 789 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → 𝑏 ∈ 2𝑜)
8552, 32, 84fovrnd 7008 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → (𝑎𝑇𝑏) ∈ 𝐵)
8645, 46grpinvcl 17750 . . . . . . . . . . . . . . . . . . . 20 ((𝐻 ∈ Grp ∧ (𝑎𝑇𝑏) ∈ 𝐵) → (𝑁‘(𝑎𝑇𝑏)) ∈ 𝐵)
8756, 85, 86syl2anc 579 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → (𝑁‘(𝑎𝑇𝑏)) ∈ 𝐵)
8845, 63gsumws2 17661 . . . . . . . . . . . . . . . . . . 19 ((𝐻 ∈ Mnd ∧ (𝑎𝑇𝑏) ∈ 𝐵 ∧ (𝑁‘(𝑎𝑇𝑏)) ∈ 𝐵) → (𝐻 Σg ⟨“(𝑎𝑇𝑏)(𝑁‘(𝑎𝑇𝑏))”⟩) = ((𝑎𝑇𝑏)(+g𝐻)(𝑁‘(𝑎𝑇𝑏))))
8958, 85, 87, 88syl3anc 1490 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → (𝐻 Σg ⟨“(𝑎𝑇𝑏)(𝑁‘(𝑎𝑇𝑏))”⟩) = ((𝑎𝑇𝑏)(+g𝐻)(𝑁‘(𝑎𝑇𝑏))))
90 eqid 2765 . . . . . . . . . . . . . . . . . . . 20 (0g𝐻) = (0g𝐻)
9145, 63, 90, 46grprinv 17752 . . . . . . . . . . . . . . . . . . 19 ((𝐻 ∈ Grp ∧ (𝑎𝑇𝑏) ∈ 𝐵) → ((𝑎𝑇𝑏)(+g𝐻)(𝑁‘(𝑎𝑇𝑏))) = (0g𝐻))
9256, 85, 91syl2anc 579 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → ((𝑎𝑇𝑏)(+g𝐻)(𝑁‘(𝑎𝑇𝑏))) = (0g𝐻))
9383, 89, 923eqtrd 2803 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → (𝐻 Σg (𝑇 ∘ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩)) = (0g𝐻))
9493oveq2d 6862 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → ((𝐻 Σg (𝑇 ∘ (𝑥 prefix 𝑛)))(+g𝐻)(𝐻 Σg (𝑇 ∘ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩))) = ((𝐻 Σg (𝑇 ∘ (𝑥 prefix 𝑛)))(+g𝐻)(0g𝐻)))
9545gsumwcl 17659 . . . . . . . . . . . . . . . . . 18 ((𝐻 ∈ Mnd ∧ (𝑇 ∘ (𝑥 prefix 𝑛)) ∈ Word 𝐵) → (𝐻 Σg (𝑇 ∘ (𝑥 prefix 𝑛))) ∈ 𝐵)
9658, 60, 95syl2anc 579 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → (𝐻 Σg (𝑇 ∘ (𝑥 prefix 𝑛))) ∈ 𝐵)
9745, 63, 90grprid 17736 . . . . . . . . . . . . . . . . 17 ((𝐻 ∈ Grp ∧ (𝐻 Σg (𝑇 ∘ (𝑥 prefix 𝑛))) ∈ 𝐵) → ((𝐻 Σg (𝑇 ∘ (𝑥 prefix 𝑛)))(+g𝐻)(0g𝐻)) = (𝐻 Σg (𝑇 ∘ (𝑥 prefix 𝑛))))
9856, 96, 97syl2anc 579 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → ((𝐻 Σg (𝑇 ∘ (𝑥 prefix 𝑛)))(+g𝐻)(0g𝐻)) = (𝐻 Σg (𝑇 ∘ (𝑥 prefix 𝑛))))
9994, 98eqtrd 2799 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → ((𝐻 Σg (𝑇 ∘ (𝑥 prefix 𝑛)))(+g𝐻)(𝐻 Σg (𝑇 ∘ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩))) = (𝐻 Σg (𝑇 ∘ (𝑥 prefix 𝑛))))
10055, 65, 993eqtrrd 2804 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → (𝐻 Σg (𝑇 ∘ (𝑥 prefix 𝑛))) = (𝐻 Σg (𝑇 ∘ ((𝑥 prefix 𝑛) ++ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩))))
101100oveq1d 6861 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → ((𝐻 Σg (𝑇 ∘ (𝑥 prefix 𝑛)))(+g𝐻)(𝐻 Σg (𝑇 ∘ (𝑥 substr ⟨𝑛, (♯‘𝑥)⟩)))) = ((𝐻 Σg (𝑇 ∘ ((𝑥 prefix 𝑛) ++ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩)))(+g𝐻)(𝐻 Σg (𝑇 ∘ (𝑥 substr ⟨𝑛, (♯‘𝑥)⟩)))))
102 swrdcl 13629 . . . . . . . . . . . . . . . 16 (𝑥 ∈ Word (𝐼 × 2𝑜) → (𝑥 substr ⟨𝑛, (♯‘𝑥)⟩) ∈ Word (𝐼 × 2𝑜))
10329, 102syl 17 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → (𝑥 substr ⟨𝑛, (♯‘𝑥)⟩) ∈ Word (𝐼 × 2𝑜))
104 wrdco 13876 . . . . . . . . . . . . . . 15 (((𝑥 substr ⟨𝑛, (♯‘𝑥)⟩) ∈ Word (𝐼 × 2𝑜) ∧ 𝑇:(𝐼 × 2𝑜)⟶𝐵) → (𝑇 ∘ (𝑥 substr ⟨𝑛, (♯‘𝑥)⟩)) ∈ Word 𝐵)
105103, 52, 104syl2anc 579 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → (𝑇 ∘ (𝑥 substr ⟨𝑛, (♯‘𝑥)⟩)) ∈ Word 𝐵)
10645, 63gsumccat 17660 . . . . . . . . . . . . . 14 ((𝐻 ∈ Mnd ∧ (𝑇 ∘ (𝑥 prefix 𝑛)) ∈ Word 𝐵 ∧ (𝑇 ∘ (𝑥 substr ⟨𝑛, (♯‘𝑥)⟩)) ∈ Word 𝐵) → (𝐻 Σg ((𝑇 ∘ (𝑥 prefix 𝑛)) ++ (𝑇 ∘ (𝑥 substr ⟨𝑛, (♯‘𝑥)⟩)))) = ((𝐻 Σg (𝑇 ∘ (𝑥 prefix 𝑛)))(+g𝐻)(𝐻 Σg (𝑇 ∘ (𝑥 substr ⟨𝑛, (♯‘𝑥)⟩)))))
10758, 60, 105, 106syl3anc 1490 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → (𝐻 Σg ((𝑇 ∘ (𝑥 prefix 𝑛)) ++ (𝑇 ∘ (𝑥 substr ⟨𝑛, (♯‘𝑥)⟩)))) = ((𝐻 Σg (𝑇 ∘ (𝑥 prefix 𝑛)))(+g𝐻)(𝐻 Σg (𝑇 ∘ (𝑥 substr ⟨𝑛, (♯‘𝑥)⟩)))))
108 ccatcl 13553 . . . . . . . . . . . . . . . 16 (((𝑥 prefix 𝑛) ∈ Word (𝐼 × 2𝑜) ∧ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩ ∈ Word (𝐼 × 2𝑜)) → ((𝑥 prefix 𝑛) ++ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩) ∈ Word (𝐼 × 2𝑜))
10944, 36, 108syl2anc 579 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → ((𝑥 prefix 𝑛) ++ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩) ∈ Word (𝐼 × 2𝑜))
110 wrdco 13876 . . . . . . . . . . . . . . 15 ((((𝑥 prefix 𝑛) ++ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩) ∈ Word (𝐼 × 2𝑜) ∧ 𝑇:(𝐼 × 2𝑜)⟶𝐵) → (𝑇 ∘ ((𝑥 prefix 𝑛) ++ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩)) ∈ Word 𝐵)
111109, 52, 110syl2anc 579 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → (𝑇 ∘ ((𝑥 prefix 𝑛) ++ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩)) ∈ Word 𝐵)
11245, 63gsumccat 17660 . . . . . . . . . . . . . 14 ((𝐻 ∈ Mnd ∧ (𝑇 ∘ ((𝑥 prefix 𝑛) ++ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩)) ∈ Word 𝐵 ∧ (𝑇 ∘ (𝑥 substr ⟨𝑛, (♯‘𝑥)⟩)) ∈ Word 𝐵) → (𝐻 Σg ((𝑇 ∘ ((𝑥 prefix 𝑛) ++ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩)) ++ (𝑇 ∘ (𝑥 substr ⟨𝑛, (♯‘𝑥)⟩)))) = ((𝐻 Σg (𝑇 ∘ ((𝑥 prefix 𝑛) ++ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩)))(+g𝐻)(𝐻 Σg (𝑇 ∘ (𝑥 substr ⟨𝑛, (♯‘𝑥)⟩)))))
11358, 111, 105, 112syl3anc 1490 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → (𝐻 Σg ((𝑇 ∘ ((𝑥 prefix 𝑛) ++ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩)) ++ (𝑇 ∘ (𝑥 substr ⟨𝑛, (♯‘𝑥)⟩)))) = ((𝐻 Σg (𝑇 ∘ ((𝑥 prefix 𝑛) ++ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩)))(+g𝐻)(𝐻 Σg (𝑇 ∘ (𝑥 substr ⟨𝑛, (♯‘𝑥)⟩)))))
114101, 107, 1133eqtr4d 2809 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → (𝐻 Σg ((𝑇 ∘ (𝑥 prefix 𝑛)) ++ (𝑇 ∘ (𝑥 substr ⟨𝑛, (♯‘𝑥)⟩)))) = (𝐻 Σg ((𝑇 ∘ ((𝑥 prefix 𝑛) ++ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩)) ++ (𝑇 ∘ (𝑥 substr ⟨𝑛, (♯‘𝑥)⟩)))))
115 simplrr 796 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → 𝑛 ∈ (0...(♯‘𝑥)))
116 lencl 13512 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ Word (𝐼 × 2𝑜) → (♯‘𝑥) ∈ ℕ0)
11729, 116syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → (♯‘𝑥) ∈ ℕ0)
118 nn0uz 11929 . . . . . . . . . . . . . . . . . . 19 0 = (ℤ‘0)
119117, 118syl6eleq 2854 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → (♯‘𝑥) ∈ (ℤ‘0))
120 eluzfz2 12563 . . . . . . . . . . . . . . . . . 18 ((♯‘𝑥) ∈ (ℤ‘0) → (♯‘𝑥) ∈ (0...(♯‘𝑥)))
121119, 120syl 17 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → (♯‘𝑥) ∈ (0...(♯‘𝑥)))
122 ccatpfx 13704 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ Word (𝐼 × 2𝑜) ∧ 𝑛 ∈ (0...(♯‘𝑥)) ∧ (♯‘𝑥) ∈ (0...(♯‘𝑥))) → ((𝑥 prefix 𝑛) ++ (𝑥 substr ⟨𝑛, (♯‘𝑥)⟩)) = (𝑥 prefix (♯‘𝑥)))
12329, 115, 121, 122syl3anc 1490 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → ((𝑥 prefix 𝑛) ++ (𝑥 substr ⟨𝑛, (♯‘𝑥)⟩)) = (𝑥 prefix (♯‘𝑥)))
124 pfxid 13687 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ Word (𝐼 × 2𝑜) → (𝑥 prefix (♯‘𝑥)) = 𝑥)
12529, 124syl 17 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → (𝑥 prefix (♯‘𝑥)) = 𝑥)
126123, 125eqtrd 2799 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → ((𝑥 prefix 𝑛) ++ (𝑥 substr ⟨𝑛, (♯‘𝑥)⟩)) = 𝑥)
127126coeq2d 5455 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → (𝑇 ∘ ((𝑥 prefix 𝑛) ++ (𝑥 substr ⟨𝑛, (♯‘𝑥)⟩))) = (𝑇𝑥))
128 ccatco 13880 . . . . . . . . . . . . . . 15 (((𝑥 prefix 𝑛) ∈ Word (𝐼 × 2𝑜) ∧ (𝑥 substr ⟨𝑛, (♯‘𝑥)⟩) ∈ Word (𝐼 × 2𝑜) ∧ 𝑇:(𝐼 × 2𝑜)⟶𝐵) → (𝑇 ∘ ((𝑥 prefix 𝑛) ++ (𝑥 substr ⟨𝑛, (♯‘𝑥)⟩))) = ((𝑇 ∘ (𝑥 prefix 𝑛)) ++ (𝑇 ∘ (𝑥 substr ⟨𝑛, (♯‘𝑥)⟩))))
12944, 103, 52, 128syl3anc 1490 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → (𝑇 ∘ ((𝑥 prefix 𝑛) ++ (𝑥 substr ⟨𝑛, (♯‘𝑥)⟩))) = ((𝑇 ∘ (𝑥 prefix 𝑛)) ++ (𝑇 ∘ (𝑥 substr ⟨𝑛, (♯‘𝑥)⟩))))
130127, 129eqtr3d 2801 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → (𝑇𝑥) = ((𝑇 ∘ (𝑥 prefix 𝑛)) ++ (𝑇 ∘ (𝑥 substr ⟨𝑛, (♯‘𝑥)⟩))))
131130oveq2d 6862 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → (𝐻 Σg (𝑇𝑥)) = (𝐻 Σg ((𝑇 ∘ (𝑥 prefix 𝑛)) ++ (𝑇 ∘ (𝑥 substr ⟨𝑛, (♯‘𝑥)⟩)))))
132 splval 13784 . . . . . . . . . . . . . . . 16 ((𝑥𝑊 ∧ (𝑛 ∈ (0...(♯‘𝑥)) ∧ 𝑛 ∈ (0...(♯‘𝑥)) ∧ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩ ∈ Word (𝐼 × 2𝑜))) → (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩⟩) = (((𝑥 prefix 𝑛) ++ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩) ++ (𝑥 substr ⟨𝑛, (♯‘𝑥)⟩)))
13326, 115, 115, 36, 132syl13anc 1491 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩⟩) = (((𝑥 prefix 𝑛) ++ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩) ++ (𝑥 substr ⟨𝑛, (♯‘𝑥)⟩)))
134133coeq2d 5455 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → (𝑇 ∘ (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩⟩)) = (𝑇 ∘ (((𝑥 prefix 𝑛) ++ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩) ++ (𝑥 substr ⟨𝑛, (♯‘𝑥)⟩))))
135 ccatco 13880 . . . . . . . . . . . . . . 15 ((((𝑥 prefix 𝑛) ++ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩) ∈ Word (𝐼 × 2𝑜) ∧ (𝑥 substr ⟨𝑛, (♯‘𝑥)⟩) ∈ Word (𝐼 × 2𝑜) ∧ 𝑇:(𝐼 × 2𝑜)⟶𝐵) → (𝑇 ∘ (((𝑥 prefix 𝑛) ++ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩) ++ (𝑥 substr ⟨𝑛, (♯‘𝑥)⟩))) = ((𝑇 ∘ ((𝑥 prefix 𝑛) ++ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩)) ++ (𝑇 ∘ (𝑥 substr ⟨𝑛, (♯‘𝑥)⟩))))
136109, 103, 52, 135syl3anc 1490 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → (𝑇 ∘ (((𝑥 prefix 𝑛) ++ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩) ++ (𝑥 substr ⟨𝑛, (♯‘𝑥)⟩))) = ((𝑇 ∘ ((𝑥 prefix 𝑛) ++ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩)) ++ (𝑇 ∘ (𝑥 substr ⟨𝑛, (♯‘𝑥)⟩))))
137134, 136eqtrd 2799 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → (𝑇 ∘ (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩⟩)) = ((𝑇 ∘ ((𝑥 prefix 𝑛) ++ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩)) ++ (𝑇 ∘ (𝑥 substr ⟨𝑛, (♯‘𝑥)⟩))))
138137oveq2d 6862 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → (𝐻 Σg (𝑇 ∘ (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩⟩))) = (𝐻 Σg ((𝑇 ∘ ((𝑥 prefix 𝑛) ++ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩)) ++ (𝑇 ∘ (𝑥 substr ⟨𝑛, (♯‘𝑥)⟩)))))
139114, 131, 1383eqtr4d 2809 . . . . . . . . . . 11 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → (𝐻 Σg (𝑇𝑥)) = (𝐻 Σg (𝑇 ∘ (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩⟩))))
140 vex 3353 . . . . . . . . . . . 12 𝑥 ∈ V
141 ovex 6878 . . . . . . . . . . . 12 (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩⟩) ∈ V
142 eleq1 2832 . . . . . . . . . . . . . . 15 (𝑢 = 𝑥 → (𝑢𝑊𝑥𝑊))
143 eleq1 2832 . . . . . . . . . . . . . . 15 (𝑣 = (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩⟩) → (𝑣𝑊 ↔ (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩⟩) ∈ 𝑊))
144142, 143bi2anan9 629 . . . . . . . . . . . . . 14 ((𝑢 = 𝑥𝑣 = (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩⟩)) → ((𝑢𝑊𝑣𝑊) ↔ (𝑥𝑊 ∧ (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩⟩) ∈ 𝑊)))
14519, 144syl5bbr 276 . . . . . . . . . . . . 13 ((𝑢 = 𝑥𝑣 = (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩⟩)) → ({𝑢, 𝑣} ⊆ 𝑊 ↔ (𝑥𝑊 ∧ (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩⟩) ∈ 𝑊)))
146 coeq2 5451 . . . . . . . . . . . . . . 15 (𝑢 = 𝑥 → (𝑇𝑢) = (𝑇𝑥))
147146oveq2d 6862 . . . . . . . . . . . . . 14 (𝑢 = 𝑥 → (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑥)))
148 coeq2 5451 . . . . . . . . . . . . . . 15 (𝑣 = (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩⟩) → (𝑇𝑣) = (𝑇 ∘ (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩⟩)))
149148oveq2d 6862 . . . . . . . . . . . . . 14 (𝑣 = (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩⟩) → (𝐻 Σg (𝑇𝑣)) = (𝐻 Σg (𝑇 ∘ (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩⟩))))
150147, 149eqeqan12d 2781 . . . . . . . . . . . . 13 ((𝑢 = 𝑥𝑣 = (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩⟩)) → ((𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)) ↔ (𝐻 Σg (𝑇𝑥)) = (𝐻 Σg (𝑇 ∘ (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩⟩)))))
151145, 150anbi12d 624 . . . . . . . . . . . 12 ((𝑢 = 𝑥𝑣 = (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩⟩)) → (({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣))) ↔ ((𝑥𝑊 ∧ (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩⟩) ∈ 𝑊) ∧ (𝐻 Σg (𝑇𝑥)) = (𝐻 Σg (𝑇 ∘ (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩⟩))))))
152 eqid 2765 . . . . . . . . . . . 12 {⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))} = {⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))}
153140, 141, 151, 152braba 5155 . . . . . . . . . . 11 (𝑥{⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))} (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩⟩) ↔ ((𝑥𝑊 ∧ (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩⟩) ∈ 𝑊) ∧ (𝐻 Σg (𝑇𝑥)) = (𝐻 Σg (𝑇 ∘ (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩⟩)))))
15426, 42, 139, 153syl21anbrc 1444 . . . . . . . . . 10 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → 𝑥{⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))} (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩⟩))
155154ralrimivva 3118 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) → ∀𝑎𝐼𝑏 ∈ 2𝑜 𝑥{⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))} (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩⟩))
156155ralrimivva 3118 . . . . . . . 8 (𝜑 → ∀𝑥𝑊𝑛 ∈ (0...(♯‘𝑥))∀𝑎𝐼𝑏 ∈ 2𝑜 𝑥{⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))} (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩⟩))
1571fvexi 6393 . . . . . . . . . 10 𝑊 ∈ V
158 erex 7975 . . . . . . . . . 10 ({⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))} Er 𝑊 → (𝑊 ∈ V → {⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))} ∈ V))
15925, 157, 158mpisyl 21 . . . . . . . . 9 (𝜑 → {⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))} ∈ V)
160 ereq1 7958 . . . . . . . . . . 11 (𝑟 = {⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))} → (𝑟 Er 𝑊 ↔ {⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))} Er 𝑊))
161 breq 4813 . . . . . . . . . . . . 13 (𝑟 = {⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))} → (𝑥𝑟(𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩⟩) ↔ 𝑥{⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))} (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩⟩)))
1621612ralbidv 3136 . . . . . . . . . . . 12 (𝑟 = {⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))} → (∀𝑎𝐼𝑏 ∈ 2𝑜 𝑥𝑟(𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩⟩) ↔ ∀𝑎𝐼𝑏 ∈ 2𝑜 𝑥{⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))} (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩⟩)))
1631622ralbidv 3136 . . . . . . . . . . 11 (𝑟 = {⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))} → (∀𝑥𝑊𝑛 ∈ (0...(♯‘𝑥))∀𝑎𝐼𝑏 ∈ 2𝑜 𝑥𝑟(𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩⟩) ↔ ∀𝑥𝑊𝑛 ∈ (0...(♯‘𝑥))∀𝑎𝐼𝑏 ∈ 2𝑜 𝑥{⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))} (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩⟩)))
164160, 163anbi12d 624 . . . . . . . . . 10 (𝑟 = {⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))} → ((𝑟 Er 𝑊 ∧ ∀𝑥𝑊𝑛 ∈ (0...(♯‘𝑥))∀𝑎𝐼𝑏 ∈ 2𝑜 𝑥𝑟(𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩⟩)) ↔ ({⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))} Er 𝑊 ∧ ∀𝑥𝑊𝑛 ∈ (0...(♯‘𝑥))∀𝑎𝐼𝑏 ∈ 2𝑜 𝑥{⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))} (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩⟩))))
165164elabg 3505 . . . . . . . . 9 ({⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))} ∈ V → ({⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))} ∈ {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑥𝑊𝑛 ∈ (0...(♯‘𝑥))∀𝑎𝐼𝑏 ∈ 2𝑜 𝑥𝑟(𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩⟩))} ↔ ({⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))} Er 𝑊 ∧ ∀𝑥𝑊𝑛 ∈ (0...(♯‘𝑥))∀𝑎𝐼𝑏 ∈ 2𝑜 𝑥{⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))} (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩⟩))))
166159, 165syl 17 . . . . . . . 8 (𝜑 → ({⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))} ∈ {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑥𝑊𝑛 ∈ (0...(♯‘𝑥))∀𝑎𝐼𝑏 ∈ 2𝑜 𝑥𝑟(𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩⟩))} ↔ ({⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))} Er 𝑊 ∧ ∀𝑥𝑊𝑛 ∈ (0...(♯‘𝑥))∀𝑎𝐼𝑏 ∈ 2𝑜 𝑥{⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))} (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩⟩))))
16725, 156, 166mpbir2and 704 . . . . . . 7 (𝜑 → {⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))} ∈ {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑥𝑊𝑛 ∈ (0...(♯‘𝑥))∀𝑎𝐼𝑏 ∈ 2𝑜 𝑥𝑟(𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩⟩))})
168 intss1 4650 . . . . . . 7 ({⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))} ∈ {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑥𝑊𝑛 ∈ (0...(♯‘𝑥))∀𝑎𝐼𝑏 ∈ 2𝑜 𝑥𝑟(𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩⟩))} → {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑥𝑊𝑛 ∈ (0...(♯‘𝑥))∀𝑎𝐼𝑏 ∈ 2𝑜 𝑥𝑟(𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩⟩))} ⊆ {⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))})
169167, 168syl 17 . . . . . 6 (𝜑 {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑥𝑊𝑛 ∈ (0...(♯‘𝑥))∀𝑎𝐼𝑏 ∈ 2𝑜 𝑥𝑟(𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩⟩))} ⊆ {⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))})
1703, 169syl5eqss 3811 . . . . 5 (𝜑 ⊆ {⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))})
171170ssbrd 4854 . . . 4 (𝜑 → (𝐴 𝐶𝐴{⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))}𝐶))
172171imp 395 . . 3 ((𝜑𝐴 𝐶) → 𝐴{⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))}𝐶)
1731, 2efger 18411 . . . . . 6 Er 𝑊
174 errel 7960 . . . . . 6 ( Er 𝑊 → Rel )
175173, 174mp1i 13 . . . . 5 (𝜑 → Rel )
176 brrelex12 5326 . . . . 5 ((Rel 𝐴 𝐶) → (𝐴 ∈ V ∧ 𝐶 ∈ V))
177175, 176sylan 575 . . . 4 ((𝜑𝐴 𝐶) → (𝐴 ∈ V ∧ 𝐶 ∈ V))
178 preq12 4427 . . . . . . 7 ((𝑢 = 𝐴𝑣 = 𝐶) → {𝑢, 𝑣} = {𝐴, 𝐶})
179178sseq1d 3794 . . . . . 6 ((𝑢 = 𝐴𝑣 = 𝐶) → ({𝑢, 𝑣} ⊆ 𝑊 ↔ {𝐴, 𝐶} ⊆ 𝑊))
180 coeq2 5451 . . . . . . . 8 (𝑢 = 𝐴 → (𝑇𝑢) = (𝑇𝐴))
181180oveq2d 6862 . . . . . . 7 (𝑢 = 𝐴 → (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝐴)))
182 coeq2 5451 . . . . . . . 8 (𝑣 = 𝐶 → (𝑇𝑣) = (𝑇𝐶))
183182oveq2d 6862 . . . . . . 7 (𝑣 = 𝐶 → (𝐻 Σg (𝑇𝑣)) = (𝐻 Σg (𝑇𝐶)))
184181, 183eqeqan12d 2781 . . . . . 6 ((𝑢 = 𝐴𝑣 = 𝐶) → ((𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)) ↔ (𝐻 Σg (𝑇𝐴)) = (𝐻 Σg (𝑇𝐶))))
185179, 184anbi12d 624 . . . . 5 ((𝑢 = 𝐴𝑣 = 𝐶) → (({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣))) ↔ ({𝐴, 𝐶} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝐴)) = (𝐻 Σg (𝑇𝐶)))))
186185, 152brabga 5152 . . . 4 ((𝐴 ∈ V ∧ 𝐶 ∈ V) → (𝐴{⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))}𝐶 ↔ ({𝐴, 𝐶} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝐴)) = (𝐻 Σg (𝑇𝐶)))))
187177, 186syl 17 . . 3 ((𝜑𝐴 𝐶) → (𝐴{⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))}𝐶 ↔ ({𝐴, 𝐶} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝐴)) = (𝐻 Σg (𝑇𝐶)))))
188172, 187mpbid 223 . 2 ((𝜑𝐴 𝐶) → ({𝐴, 𝐶} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝐴)) = (𝐻 Σg (𝑇𝐶))))
189188simprd 489 1 ((𝜑𝐴 𝐶) → (𝐻 Σg (𝑇𝐴)) = (𝐻 Σg (𝑇𝐶)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384   = wceq 1652  wcel 2155  {cab 2751  wral 3055  Vcvv 3350  cdif 3731  cin 3733  wss 3734  c0 4081  ifcif 4245  {cpr 4338  cop 4342  cotp 4344   cint 4635   class class class wbr 4811  {copab 4873   I cid 5186   × cxp 5277  ccom 5283  Rel wrel 5284  wf 6066  cfv 6070  (class class class)co 6846  cmpt2 6848  1𝑜c1o 7761  2𝑜c2o 7762   Er wer 7948  0cc0 10193  0cn0 11543  cuz 11893  ...cfz 12540  chash 13328  Word cword 13493   ++ cconcat 13549   substr csubstr 13624   prefix cpfx 13673   splice csplice 13779  ⟨“cs2 13886  Basecbs 16146  +gcplusg 16230  0gc0g 16382   Σg cgsu 16383  Mndcmnd 17576  Grpcgrp 17705  invgcminusg 17706   ~FG cefg 18399
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-rep 4932  ax-sep 4943  ax-nul 4951  ax-pow 5003  ax-pr 5064  ax-un 7151  ax-cnex 10249  ax-resscn 10250  ax-1cn 10251  ax-icn 10252  ax-addcl 10253  ax-addrcl 10254  ax-mulcl 10255  ax-mulrcl 10256  ax-mulcom 10257  ax-addass 10258  ax-mulass 10259  ax-distr 10260  ax-i2m1 10261  ax-1ne0 10262  ax-1rid 10263  ax-rnegex 10264  ax-rrecex 10265  ax-cnre 10266  ax-pre-lttri 10267  ax-pre-lttrn 10268  ax-pre-ltadd 10269  ax-pre-mulgt0 10270
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-nel 3041  df-ral 3060  df-rex 3061  df-reu 3062  df-rmo 3063  df-rab 3064  df-v 3352  df-sbc 3599  df-csb 3694  df-dif 3737  df-un 3739  df-in 3741  df-ss 3748  df-pss 3750  df-nul 4082  df-if 4246  df-pw 4319  df-sn 4337  df-pr 4339  df-tp 4341  df-op 4343  df-ot 4345  df-uni 4597  df-int 4636  df-iun 4680  df-iin 4681  df-br 4812  df-opab 4874  df-mpt 4891  df-tr 4914  df-id 5187  df-eprel 5192  df-po 5200  df-so 5201  df-fr 5238  df-we 5240  df-xp 5285  df-rel 5286  df-cnv 5287  df-co 5288  df-dm 5289  df-rn 5290  df-res 5291  df-ima 5292  df-pred 5867  df-ord 5913  df-on 5914  df-lim 5915  df-suc 5916  df-iota 6033  df-fun 6072  df-fn 6073  df-f 6074  df-f1 6075  df-fo 6076  df-f1o 6077  df-fv 6078  df-riota 6807  df-ov 6849  df-oprab 6850  df-mpt2 6851  df-om 7268  df-1st 7370  df-2nd 7371  df-wrecs 7614  df-recs 7676  df-rdg 7714  df-1o 7768  df-2o 7769  df-oadd 7772  df-er 7951  df-map 8066  df-pm 8067  df-en 8165  df-dom 8166  df-sdom 8167  df-fin 8168  df-card 9020  df-pnf 10334  df-mnf 10335  df-xr 10336  df-ltxr 10337  df-le 10338  df-sub 10527  df-neg 10528  df-nn 11280  df-2 11340  df-n0 11544  df-z 11630  df-uz 11894  df-fz 12541  df-fzo 12681  df-seq 13016  df-hash 13329  df-word 13494  df-concat 13550  df-s1 13575  df-substr 13625  df-pfx 13674  df-splice 13781  df-s2 13893  df-ndx 16149  df-slot 16150  df-base 16152  df-sets 16153  df-ress 16154  df-plusg 16243  df-0g 16384  df-gsum 16385  df-mgm 17524  df-sgrp 17566  df-mnd 17577  df-submnd 17618  df-grp 17708  df-minusg 17709  df-efg 18402
This theorem is referenced by:  frgpupf  18468
  Copyright terms: Public domain W3C validator