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

Theorem frgpuplem 18231
 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 18176 . . . . . 6 = {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑥𝑊𝑛 ∈ (0...(#‘𝑥))∀𝑎𝐼𝑏 ∈ 2𝑜 𝑥𝑟(𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩⟩))}
4 coeq2 5313 . . . . . . . . . . . . 13 (𝑢 = 𝑣 → (𝑇𝑢) = (𝑇𝑣))
54oveq2d 6706 . . . . . . . . . . . 12 (𝑢 = 𝑣 → (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))
6 eqid 2651 . . . . . . . . . . . 12 {⟨𝑢, 𝑣⟩ ∣ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣))} = {⟨𝑢, 𝑣⟩ ∣ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣))}
75, 6eqer 7822 . . . . . . . . . . 11 {⟨𝑢, 𝑣⟩ ∣ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣))} Er V
87a1i 11 . . . . . . . . . 10 (𝜑 → {⟨𝑢, 𝑣⟩ ∣ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣))} Er V)
9 ssv 3658 . . . . . . . . . . 11 𝑊 ⊆ V
109a1i 11 . . . . . . . . . 10 (𝜑𝑊 ⊆ V)
118, 10erinxp 7864 . . . . . . . . 9 (𝜑 → ({⟨𝑢, 𝑣⟩ ∣ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣))} ∩ (𝑊 × 𝑊)) Er 𝑊)
12 df-xp 5149 . . . . . . . . . . . . 13 (𝑊 × 𝑊) = {⟨𝑢, 𝑣⟩ ∣ (𝑢𝑊𝑣𝑊)}
1312ineq1i 3843 . . . . . . . . . . . 12 ((𝑊 × 𝑊) ∩ {⟨𝑢, 𝑣⟩ ∣ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣))}) = ({⟨𝑢, 𝑣⟩ ∣ (𝑢𝑊𝑣𝑊)} ∩ {⟨𝑢, 𝑣⟩ ∣ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣))})
14 incom 3838 . . . . . . . . . . . 12 ((𝑊 × 𝑊) ∩ {⟨𝑢, 𝑣⟩ ∣ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣))}) = ({⟨𝑢, 𝑣⟩ ∣ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣))} ∩ (𝑊 × 𝑊))
15 inopab 5285 . . . . . . . . . . . 12 ({⟨𝑢, 𝑣⟩ ∣ (𝑢𝑊𝑣𝑊)} ∩ {⟨𝑢, 𝑣⟩ ∣ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣))}) = {⟨𝑢, 𝑣⟩ ∣ ((𝑢𝑊𝑣𝑊) ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))}
1613, 14, 153eqtr3i 2681 . . . . . . . . . . 11 ({⟨𝑢, 𝑣⟩ ∣ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣))} ∩ (𝑊 × 𝑊)) = {⟨𝑢, 𝑣⟩ ∣ ((𝑢𝑊𝑣𝑊) ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))}
17 vex 3234 . . . . . . . . . . . . . 14 𝑢 ∈ V
18 vex 3234 . . . . . . . . . . . . . 14 𝑣 ∈ V
1917, 18prss 4383 . . . . . . . . . . . . 13 ((𝑢𝑊𝑣𝑊) ↔ {𝑢, 𝑣} ⊆ 𝑊)
2019anbi1i 731 . . . . . . . . . . . 12 (((𝑢𝑊𝑣𝑊) ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣))) ↔ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣))))
2120opabbii 4750 . . . . . . . . . . 11 {⟨𝑢, 𝑣⟩ ∣ ((𝑢𝑊𝑣𝑊) ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))} = {⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))}
2216, 21eqtri 2673 . . . . . . . . . 10 ({⟨𝑢, 𝑣⟩ ∣ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣))} ∩ (𝑊 × 𝑊)) = {⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))}
23 ereq1 7794 . . . . . . . . . 10 (({⟨𝑢, 𝑣⟩ ∣ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣))} ∩ (𝑊 × 𝑊)) = {⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))} → (({⟨𝑢, 𝑣⟩ ∣ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣))} ∩ (𝑊 × 𝑊)) Er 𝑊 ↔ {⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))} Er 𝑊))
2422, 23ax-mp 5 . . . . . . . . 9 (({⟨𝑢, 𝑣⟩ ∣ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣))} ∩ (𝑊 × 𝑊)) Er 𝑊 ↔ {⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))} Er 𝑊)
2511, 24sylib 208 . . . . . . . 8 (𝜑 → {⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))} Er 𝑊)
26 simplrl 817 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → 𝑥𝑊)
27 fviss 6295 . . . . . . . . . . . . . . . 16 ( I ‘Word (𝐼 × 2𝑜)) ⊆ Word (𝐼 × 2𝑜)
281, 27eqsstri 3668 . . . . . . . . . . . . . . 15 𝑊 ⊆ Word (𝐼 × 2𝑜)
2928, 26sseldi 3634 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → 𝑥 ∈ Word (𝐼 × 2𝑜))
30 opelxpi 5182 . . . . . . . . . . . . . . . 16 ((𝑎𝐼𝑏 ∈ 2𝑜) → ⟨𝑎, 𝑏⟩ ∈ (𝐼 × 2𝑜))
3130adantl 481 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → ⟨𝑎, 𝑏⟩ ∈ (𝐼 × 2𝑜))
32 simprl 809 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → 𝑎𝐼)
33 2oconcl 7628 . . . . . . . . . . . . . . . . 17 (𝑏 ∈ 2𝑜 → (1𝑜𝑏) ∈ 2𝑜)
3433ad2antll 765 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → (1𝑜𝑏) ∈ 2𝑜)
35 opelxpi 5182 . . . . . . . . . . . . . . . 16 ((𝑎𝐼 ∧ (1𝑜𝑏) ∈ 2𝑜) → ⟨𝑎, (1𝑜𝑏)⟩ ∈ (𝐼 × 2𝑜))
3632, 34, 35syl2anc 694 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → ⟨𝑎, (1𝑜𝑏)⟩ ∈ (𝐼 × 2𝑜))
3731, 36s2cld 13662 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩ ∈ Word (𝐼 × 2𝑜))
38 splcl 13549 . . . . . . . . . . . . . 14 ((𝑥 ∈ Word (𝐼 × 2𝑜) ∧ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩ ∈ Word (𝐼 × 2𝑜)) → (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩⟩) ∈ Word (𝐼 × 2𝑜))
3929, 37, 38syl2anc 694 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩⟩) ∈ Word (𝐼 × 2𝑜))
401efgrcl 18174 . . . . . . . . . . . . . . 15 (𝑥𝑊 → (𝐼 ∈ V ∧ 𝑊 = Word (𝐼 × 2𝑜)))
4126, 40syl 17 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → (𝐼 ∈ V ∧ 𝑊 = Word (𝐼 × 2𝑜)))
4241simprd 478 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → 𝑊 = Word (𝐼 × 2𝑜))
4339, 42eleqtrrd 2733 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩⟩) ∈ 𝑊)
4426, 43jca 553 . . . . . . . . . . 11 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → (𝑥𝑊 ∧ (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩⟩) ∈ 𝑊))
45 swrdcl 13464 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ Word (𝐼 × 2𝑜) → (𝑥 substr ⟨0, 𝑛⟩) ∈ Word (𝐼 × 2𝑜))
4629, 45syl 17 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → (𝑥 substr ⟨0, 𝑛⟩) ∈ Word (𝐼 × 2𝑜))
47 frgpup.b . . . . . . . . . . . . . . . . . . 19 𝐵 = (Base‘𝐻)
48 frgpup.n . . . . . . . . . . . . . . . . . . 19 𝑁 = (invg𝐻)
49 frgpup.t . . . . . . . . . . . . . . . . . . 19 𝑇 = (𝑦𝐼, 𝑧 ∈ 2𝑜 ↦ if(𝑧 = ∅, (𝐹𝑦), (𝑁‘(𝐹𝑦))))
50 frgpup.h . . . . . . . . . . . . . . . . . . 19 (𝜑𝐻 ∈ Grp)
51 frgpup.i . . . . . . . . . . . . . . . . . . 19 (𝜑𝐼𝑉)
52 frgpup.a . . . . . . . . . . . . . . . . . . 19 (𝜑𝐹:𝐼𝐵)
5347, 48, 49, 50, 51, 52frgpuptf 18229 . . . . . . . . . . . . . . . . . 18 (𝜑𝑇:(𝐼 × 2𝑜)⟶𝐵)
5453ad2antrr 762 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → 𝑇:(𝐼 × 2𝑜)⟶𝐵)
55 ccatco 13627 . . . . . . . . . . . . . . . . 17 (((𝑥 substr ⟨0, 𝑛⟩) ∈ Word (𝐼 × 2𝑜) ∧ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩ ∈ Word (𝐼 × 2𝑜) ∧ 𝑇:(𝐼 × 2𝑜)⟶𝐵) → (𝑇 ∘ ((𝑥 substr ⟨0, 𝑛⟩) ++ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩)) = ((𝑇 ∘ (𝑥 substr ⟨0, 𝑛⟩)) ++ (𝑇 ∘ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩)))
5646, 37, 54, 55syl3anc 1366 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → (𝑇 ∘ ((𝑥 substr ⟨0, 𝑛⟩) ++ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩)) = ((𝑇 ∘ (𝑥 substr ⟨0, 𝑛⟩)) ++ (𝑇 ∘ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩)))
5756oveq2d 6706 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → (𝐻 Σg (𝑇 ∘ ((𝑥 substr ⟨0, 𝑛⟩) ++ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩))) = (𝐻 Σg ((𝑇 ∘ (𝑥 substr ⟨0, 𝑛⟩)) ++ (𝑇 ∘ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩))))
5850ad2antrr 762 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → 𝐻 ∈ Grp)
59 grpmnd 17476 . . . . . . . . . . . . . . . . 17 (𝐻 ∈ Grp → 𝐻 ∈ Mnd)
6058, 59syl 17 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → 𝐻 ∈ Mnd)
61 wrdco 13623 . . . . . . . . . . . . . . . . 17 (((𝑥 substr ⟨0, 𝑛⟩) ∈ Word (𝐼 × 2𝑜) ∧ 𝑇:(𝐼 × 2𝑜)⟶𝐵) → (𝑇 ∘ (𝑥 substr ⟨0, 𝑛⟩)) ∈ Word 𝐵)
6246, 54, 61syl2anc 694 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → (𝑇 ∘ (𝑥 substr ⟨0, 𝑛⟩)) ∈ Word 𝐵)
63 wrdco 13623 . . . . . . . . . . . . . . . . 17 ((⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩ ∈ Word (𝐼 × 2𝑜) ∧ 𝑇:(𝐼 × 2𝑜)⟶𝐵) → (𝑇 ∘ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩) ∈ Word 𝐵)
6437, 54, 63syl2anc 694 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → (𝑇 ∘ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩) ∈ Word 𝐵)
65 eqid 2651 . . . . . . . . . . . . . . . . 17 (+g𝐻) = (+g𝐻)
6647, 65gsumccat 17425 . . . . . . . . . . . . . . . 16 ((𝐻 ∈ Mnd ∧ (𝑇 ∘ (𝑥 substr ⟨0, 𝑛⟩)) ∈ Word 𝐵 ∧ (𝑇 ∘ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩) ∈ Word 𝐵) → (𝐻 Σg ((𝑇 ∘ (𝑥 substr ⟨0, 𝑛⟩)) ++ (𝑇 ∘ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩))) = ((𝐻 Σg (𝑇 ∘ (𝑥 substr ⟨0, 𝑛⟩)))(+g𝐻)(𝐻 Σg (𝑇 ∘ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩))))
6760, 62, 64, 66syl3anc 1366 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → (𝐻 Σg ((𝑇 ∘ (𝑥 substr ⟨0, 𝑛⟩)) ++ (𝑇 ∘ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩))) = ((𝐻 Σg (𝑇 ∘ (𝑥 substr ⟨0, 𝑛⟩)))(+g𝐻)(𝐻 Σg (𝑇 ∘ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩))))
6854, 31, 36s2co 13711 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → (𝑇 ∘ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩) = ⟨“(𝑇‘⟨𝑎, 𝑏⟩)(𝑇‘⟨𝑎, (1𝑜𝑏)⟩)”⟩)
69 df-ov 6693 . . . . . . . . . . . . . . . . . . . . . 22 (𝑎𝑇𝑏) = (𝑇‘⟨𝑎, 𝑏⟩)
7069a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → (𝑎𝑇𝑏) = (𝑇‘⟨𝑎, 𝑏⟩))
71 df-ov 6693 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑎(𝑦𝐼, 𝑧 ∈ 2𝑜 ↦ ⟨𝑦, (1𝑜𝑧)⟩)𝑏) = ((𝑦𝐼, 𝑧 ∈ 2𝑜 ↦ ⟨𝑦, (1𝑜𝑧)⟩)‘⟨𝑎, 𝑏⟩)
72 eqid 2651 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑦𝐼, 𝑧 ∈ 2𝑜 ↦ ⟨𝑦, (1𝑜𝑧)⟩) = (𝑦𝐼, 𝑧 ∈ 2𝑜 ↦ ⟨𝑦, (1𝑜𝑧)⟩)
7372efgmval 18171 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑎𝐼𝑏 ∈ 2𝑜) → (𝑎(𝑦𝐼, 𝑧 ∈ 2𝑜 ↦ ⟨𝑦, (1𝑜𝑧)⟩)𝑏) = ⟨𝑎, (1𝑜𝑏)⟩)
7471, 73syl5eqr 2699 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑎𝐼𝑏 ∈ 2𝑜) → ((𝑦𝐼, 𝑧 ∈ 2𝑜 ↦ ⟨𝑦, (1𝑜𝑧)⟩)‘⟨𝑎, 𝑏⟩) = ⟨𝑎, (1𝑜𝑏)⟩)
7574adantl 481 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → ((𝑦𝐼, 𝑧 ∈ 2𝑜 ↦ ⟨𝑦, (1𝑜𝑧)⟩)‘⟨𝑎, 𝑏⟩) = ⟨𝑎, (1𝑜𝑏)⟩)
7675fveq2d 6233 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → (𝑇‘((𝑦𝐼, 𝑧 ∈ 2𝑜 ↦ ⟨𝑦, (1𝑜𝑧)⟩)‘⟨𝑎, 𝑏⟩)) = (𝑇‘⟨𝑎, (1𝑜𝑏)⟩))
7747, 48, 49, 50, 51, 52, 72frgpuptinv 18230 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ ⟨𝑎, 𝑏⟩ ∈ (𝐼 × 2𝑜)) → (𝑇‘((𝑦𝐼, 𝑧 ∈ 2𝑜 ↦ ⟨𝑦, (1𝑜𝑧)⟩)‘⟨𝑎, 𝑏⟩)) = (𝑁‘(𝑇‘⟨𝑎, 𝑏⟩)))
7830, 77sylan2 490 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → (𝑇‘((𝑦𝐼, 𝑧 ∈ 2𝑜 ↦ ⟨𝑦, (1𝑜𝑧)⟩)‘⟨𝑎, 𝑏⟩)) = (𝑁‘(𝑇‘⟨𝑎, 𝑏⟩)))
7978adantlr 751 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → (𝑇‘((𝑦𝐼, 𝑧 ∈ 2𝑜 ↦ ⟨𝑦, (1𝑜𝑧)⟩)‘⟨𝑎, 𝑏⟩)) = (𝑁‘(𝑇‘⟨𝑎, 𝑏⟩)))
8076, 79eqtr3d 2687 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → (𝑇‘⟨𝑎, (1𝑜𝑏)⟩) = (𝑁‘(𝑇‘⟨𝑎, 𝑏⟩)))
8169fveq2i 6232 . . . . . . . . . . . . . . . . . . . . . 22 (𝑁‘(𝑎𝑇𝑏)) = (𝑁‘(𝑇‘⟨𝑎, 𝑏⟩))
8280, 81syl6reqr 2704 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → (𝑁‘(𝑎𝑇𝑏)) = (𝑇‘⟨𝑎, (1𝑜𝑏)⟩))
8370, 82s2eqd 13654 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → ⟨“(𝑎𝑇𝑏)(𝑁‘(𝑎𝑇𝑏))”⟩ = ⟨“(𝑇‘⟨𝑎, 𝑏⟩)(𝑇‘⟨𝑎, (1𝑜𝑏)⟩)”⟩)
8468, 83eqtr4d 2688 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → (𝑇 ∘ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩) = ⟨“(𝑎𝑇𝑏)(𝑁‘(𝑎𝑇𝑏))”⟩)
8584oveq2d 6706 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → (𝐻 Σg (𝑇 ∘ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩)) = (𝐻 Σg ⟨“(𝑎𝑇𝑏)(𝑁‘(𝑎𝑇𝑏))”⟩))
86 simprr 811 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → 𝑏 ∈ 2𝑜)
8754, 32, 86fovrnd 6848 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → (𝑎𝑇𝑏) ∈ 𝐵)
8847, 48grpinvcl 17514 . . . . . . . . . . . . . . . . . . . 20 ((𝐻 ∈ Grp ∧ (𝑎𝑇𝑏) ∈ 𝐵) → (𝑁‘(𝑎𝑇𝑏)) ∈ 𝐵)
8958, 87, 88syl2anc 694 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → (𝑁‘(𝑎𝑇𝑏)) ∈ 𝐵)
9047, 65gsumws2 17426 . . . . . . . . . . . . . . . . . . 19 ((𝐻 ∈ Mnd ∧ (𝑎𝑇𝑏) ∈ 𝐵 ∧ (𝑁‘(𝑎𝑇𝑏)) ∈ 𝐵) → (𝐻 Σg ⟨“(𝑎𝑇𝑏)(𝑁‘(𝑎𝑇𝑏))”⟩) = ((𝑎𝑇𝑏)(+g𝐻)(𝑁‘(𝑎𝑇𝑏))))
9160, 87, 89, 90syl3anc 1366 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → (𝐻 Σg ⟨“(𝑎𝑇𝑏)(𝑁‘(𝑎𝑇𝑏))”⟩) = ((𝑎𝑇𝑏)(+g𝐻)(𝑁‘(𝑎𝑇𝑏))))
92 eqid 2651 . . . . . . . . . . . . . . . . . . . 20 (0g𝐻) = (0g𝐻)
9347, 65, 92, 48grprinv 17516 . . . . . . . . . . . . . . . . . . 19 ((𝐻 ∈ Grp ∧ (𝑎𝑇𝑏) ∈ 𝐵) → ((𝑎𝑇𝑏)(+g𝐻)(𝑁‘(𝑎𝑇𝑏))) = (0g𝐻))
9458, 87, 93syl2anc 694 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → ((𝑎𝑇𝑏)(+g𝐻)(𝑁‘(𝑎𝑇𝑏))) = (0g𝐻))
9585, 91, 943eqtrd 2689 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → (𝐻 Σg (𝑇 ∘ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩)) = (0g𝐻))
9695oveq2d 6706 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → ((𝐻 Σg (𝑇 ∘ (𝑥 substr ⟨0, 𝑛⟩)))(+g𝐻)(𝐻 Σg (𝑇 ∘ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩))) = ((𝐻 Σg (𝑇 ∘ (𝑥 substr ⟨0, 𝑛⟩)))(+g𝐻)(0g𝐻)))
9747gsumwcl 17424 . . . . . . . . . . . . . . . . . 18 ((𝐻 ∈ Mnd ∧ (𝑇 ∘ (𝑥 substr ⟨0, 𝑛⟩)) ∈ Word 𝐵) → (𝐻 Σg (𝑇 ∘ (𝑥 substr ⟨0, 𝑛⟩))) ∈ 𝐵)
9860, 62, 97syl2anc 694 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → (𝐻 Σg (𝑇 ∘ (𝑥 substr ⟨0, 𝑛⟩))) ∈ 𝐵)
9947, 65, 92grprid 17500 . . . . . . . . . . . . . . . . 17 ((𝐻 ∈ Grp ∧ (𝐻 Σg (𝑇 ∘ (𝑥 substr ⟨0, 𝑛⟩))) ∈ 𝐵) → ((𝐻 Σg (𝑇 ∘ (𝑥 substr ⟨0, 𝑛⟩)))(+g𝐻)(0g𝐻)) = (𝐻 Σg (𝑇 ∘ (𝑥 substr ⟨0, 𝑛⟩))))
10058, 98, 99syl2anc 694 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → ((𝐻 Σg (𝑇 ∘ (𝑥 substr ⟨0, 𝑛⟩)))(+g𝐻)(0g𝐻)) = (𝐻 Σg (𝑇 ∘ (𝑥 substr ⟨0, 𝑛⟩))))
10196, 100eqtrd 2685 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → ((𝐻 Σg (𝑇 ∘ (𝑥 substr ⟨0, 𝑛⟩)))(+g𝐻)(𝐻 Σg (𝑇 ∘ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩))) = (𝐻 Σg (𝑇 ∘ (𝑥 substr ⟨0, 𝑛⟩))))
10257, 67, 1013eqtrrd 2690 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → (𝐻 Σg (𝑇 ∘ (𝑥 substr ⟨0, 𝑛⟩))) = (𝐻 Σg (𝑇 ∘ ((𝑥 substr ⟨0, 𝑛⟩) ++ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩))))
103102oveq1d 6705 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → ((𝐻 Σg (𝑇 ∘ (𝑥 substr ⟨0, 𝑛⟩)))(+g𝐻)(𝐻 Σg (𝑇 ∘ (𝑥 substr ⟨𝑛, (#‘𝑥)⟩)))) = ((𝐻 Σg (𝑇 ∘ ((𝑥 substr ⟨0, 𝑛⟩) ++ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩)))(+g𝐻)(𝐻 Σg (𝑇 ∘ (𝑥 substr ⟨𝑛, (#‘𝑥)⟩)))))
104 swrdcl 13464 . . . . . . . . . . . . . . . 16 (𝑥 ∈ Word (𝐼 × 2𝑜) → (𝑥 substr ⟨𝑛, (#‘𝑥)⟩) ∈ Word (𝐼 × 2𝑜))
10529, 104syl 17 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → (𝑥 substr ⟨𝑛, (#‘𝑥)⟩) ∈ Word (𝐼 × 2𝑜))
106 wrdco 13623 . . . . . . . . . . . . . . 15 (((𝑥 substr ⟨𝑛, (#‘𝑥)⟩) ∈ Word (𝐼 × 2𝑜) ∧ 𝑇:(𝐼 × 2𝑜)⟶𝐵) → (𝑇 ∘ (𝑥 substr ⟨𝑛, (#‘𝑥)⟩)) ∈ Word 𝐵)
107105, 54, 106syl2anc 694 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → (𝑇 ∘ (𝑥 substr ⟨𝑛, (#‘𝑥)⟩)) ∈ Word 𝐵)
10847, 65gsumccat 17425 . . . . . . . . . . . . . 14 ((𝐻 ∈ Mnd ∧ (𝑇 ∘ (𝑥 substr ⟨0, 𝑛⟩)) ∈ Word 𝐵 ∧ (𝑇 ∘ (𝑥 substr ⟨𝑛, (#‘𝑥)⟩)) ∈ Word 𝐵) → (𝐻 Σg ((𝑇 ∘ (𝑥 substr ⟨0, 𝑛⟩)) ++ (𝑇 ∘ (𝑥 substr ⟨𝑛, (#‘𝑥)⟩)))) = ((𝐻 Σg (𝑇 ∘ (𝑥 substr ⟨0, 𝑛⟩)))(+g𝐻)(𝐻 Σg (𝑇 ∘ (𝑥 substr ⟨𝑛, (#‘𝑥)⟩)))))
10960, 62, 107, 108syl3anc 1366 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → (𝐻 Σg ((𝑇 ∘ (𝑥 substr ⟨0, 𝑛⟩)) ++ (𝑇 ∘ (𝑥 substr ⟨𝑛, (#‘𝑥)⟩)))) = ((𝐻 Σg (𝑇 ∘ (𝑥 substr ⟨0, 𝑛⟩)))(+g𝐻)(𝐻 Σg (𝑇 ∘ (𝑥 substr ⟨𝑛, (#‘𝑥)⟩)))))
110 ccatcl 13392 . . . . . . . . . . . . . . . 16 (((𝑥 substr ⟨0, 𝑛⟩) ∈ Word (𝐼 × 2𝑜) ∧ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩ ∈ Word (𝐼 × 2𝑜)) → ((𝑥 substr ⟨0, 𝑛⟩) ++ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩) ∈ Word (𝐼 × 2𝑜))
11146, 37, 110syl2anc 694 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → ((𝑥 substr ⟨0, 𝑛⟩) ++ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩) ∈ Word (𝐼 × 2𝑜))
112 wrdco 13623 . . . . . . . . . . . . . . 15 ((((𝑥 substr ⟨0, 𝑛⟩) ++ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩) ∈ Word (𝐼 × 2𝑜) ∧ 𝑇:(𝐼 × 2𝑜)⟶𝐵) → (𝑇 ∘ ((𝑥 substr ⟨0, 𝑛⟩) ++ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩)) ∈ Word 𝐵)
113111, 54, 112syl2anc 694 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → (𝑇 ∘ ((𝑥 substr ⟨0, 𝑛⟩) ++ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩)) ∈ Word 𝐵)
11447, 65gsumccat 17425 . . . . . . . . . . . . . 14 ((𝐻 ∈ Mnd ∧ (𝑇 ∘ ((𝑥 substr ⟨0, 𝑛⟩) ++ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩)) ∈ Word 𝐵 ∧ (𝑇 ∘ (𝑥 substr ⟨𝑛, (#‘𝑥)⟩)) ∈ Word 𝐵) → (𝐻 Σg ((𝑇 ∘ ((𝑥 substr ⟨0, 𝑛⟩) ++ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩)) ++ (𝑇 ∘ (𝑥 substr ⟨𝑛, (#‘𝑥)⟩)))) = ((𝐻 Σg (𝑇 ∘ ((𝑥 substr ⟨0, 𝑛⟩) ++ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩)))(+g𝐻)(𝐻 Σg (𝑇 ∘ (𝑥 substr ⟨𝑛, (#‘𝑥)⟩)))))
11560, 113, 107, 114syl3anc 1366 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → (𝐻 Σg ((𝑇 ∘ ((𝑥 substr ⟨0, 𝑛⟩) ++ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩)) ++ (𝑇 ∘ (𝑥 substr ⟨𝑛, (#‘𝑥)⟩)))) = ((𝐻 Σg (𝑇 ∘ ((𝑥 substr ⟨0, 𝑛⟩) ++ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩)))(+g𝐻)(𝐻 Σg (𝑇 ∘ (𝑥 substr ⟨𝑛, (#‘𝑥)⟩)))))
116103, 109, 1153eqtr4d 2695 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → (𝐻 Σg ((𝑇 ∘ (𝑥 substr ⟨0, 𝑛⟩)) ++ (𝑇 ∘ (𝑥 substr ⟨𝑛, (#‘𝑥)⟩)))) = (𝐻 Σg ((𝑇 ∘ ((𝑥 substr ⟨0, 𝑛⟩) ++ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩)) ++ (𝑇 ∘ (𝑥 substr ⟨𝑛, (#‘𝑥)⟩)))))
117 simplrr 818 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → 𝑛 ∈ (0...(#‘𝑥)))
118 elfzuz 12376 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ (0...(#‘𝑥)) → 𝑛 ∈ (ℤ‘0))
119 eluzfz1 12386 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ (ℤ‘0) → 0 ∈ (0...𝑛))
120117, 118, 1193syl 18 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → 0 ∈ (0...𝑛))
121 lencl 13356 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ Word (𝐼 × 2𝑜) → (#‘𝑥) ∈ ℕ0)
12229, 121syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → (#‘𝑥) ∈ ℕ0)
123 nn0uz 11760 . . . . . . . . . . . . . . . . . . 19 0 = (ℤ‘0)
124122, 123syl6eleq 2740 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → (#‘𝑥) ∈ (ℤ‘0))
125 eluzfz2 12387 . . . . . . . . . . . . . . . . . 18 ((#‘𝑥) ∈ (ℤ‘0) → (#‘𝑥) ∈ (0...(#‘𝑥)))
126124, 125syl 17 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → (#‘𝑥) ∈ (0...(#‘𝑥)))
127 ccatswrd 13502 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ Word (𝐼 × 2𝑜) ∧ (0 ∈ (0...𝑛) ∧ 𝑛 ∈ (0...(#‘𝑥)) ∧ (#‘𝑥) ∈ (0...(#‘𝑥)))) → ((𝑥 substr ⟨0, 𝑛⟩) ++ (𝑥 substr ⟨𝑛, (#‘𝑥)⟩)) = (𝑥 substr ⟨0, (#‘𝑥)⟩))
12829, 120, 117, 126, 127syl13anc 1368 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → ((𝑥 substr ⟨0, 𝑛⟩) ++ (𝑥 substr ⟨𝑛, (#‘𝑥)⟩)) = (𝑥 substr ⟨0, (#‘𝑥)⟩))
129 swrdid 13474 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ Word (𝐼 × 2𝑜) → (𝑥 substr ⟨0, (#‘𝑥)⟩) = 𝑥)
13029, 129syl 17 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → (𝑥 substr ⟨0, (#‘𝑥)⟩) = 𝑥)
131128, 130eqtrd 2685 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → ((𝑥 substr ⟨0, 𝑛⟩) ++ (𝑥 substr ⟨𝑛, (#‘𝑥)⟩)) = 𝑥)
132131coeq2d 5317 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → (𝑇 ∘ ((𝑥 substr ⟨0, 𝑛⟩) ++ (𝑥 substr ⟨𝑛, (#‘𝑥)⟩))) = (𝑇𝑥))
133 ccatco 13627 . . . . . . . . . . . . . . 15 (((𝑥 substr ⟨0, 𝑛⟩) ∈ Word (𝐼 × 2𝑜) ∧ (𝑥 substr ⟨𝑛, (#‘𝑥)⟩) ∈ Word (𝐼 × 2𝑜) ∧ 𝑇:(𝐼 × 2𝑜)⟶𝐵) → (𝑇 ∘ ((𝑥 substr ⟨0, 𝑛⟩) ++ (𝑥 substr ⟨𝑛, (#‘𝑥)⟩))) = ((𝑇 ∘ (𝑥 substr ⟨0, 𝑛⟩)) ++ (𝑇 ∘ (𝑥 substr ⟨𝑛, (#‘𝑥)⟩))))
13446, 105, 54, 133syl3anc 1366 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → (𝑇 ∘ ((𝑥 substr ⟨0, 𝑛⟩) ++ (𝑥 substr ⟨𝑛, (#‘𝑥)⟩))) = ((𝑇 ∘ (𝑥 substr ⟨0, 𝑛⟩)) ++ (𝑇 ∘ (𝑥 substr ⟨𝑛, (#‘𝑥)⟩))))
135132, 134eqtr3d 2687 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → (𝑇𝑥) = ((𝑇 ∘ (𝑥 substr ⟨0, 𝑛⟩)) ++ (𝑇 ∘ (𝑥 substr ⟨𝑛, (#‘𝑥)⟩))))
136135oveq2d 6706 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → (𝐻 Σg (𝑇𝑥)) = (𝐻 Σg ((𝑇 ∘ (𝑥 substr ⟨0, 𝑛⟩)) ++ (𝑇 ∘ (𝑥 substr ⟨𝑛, (#‘𝑥)⟩)))))
137 splval 13548 . . . . . . . . . . . . . . . 16 ((𝑥𝑊 ∧ (𝑛 ∈ (0...(#‘𝑥)) ∧ 𝑛 ∈ (0...(#‘𝑥)) ∧ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩ ∈ Word (𝐼 × 2𝑜))) → (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩⟩) = (((𝑥 substr ⟨0, 𝑛⟩) ++ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩) ++ (𝑥 substr ⟨𝑛, (#‘𝑥)⟩)))
13826, 117, 117, 37, 137syl13anc 1368 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩⟩) = (((𝑥 substr ⟨0, 𝑛⟩) ++ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩) ++ (𝑥 substr ⟨𝑛, (#‘𝑥)⟩)))
139138coeq2d 5317 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → (𝑇 ∘ (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩⟩)) = (𝑇 ∘ (((𝑥 substr ⟨0, 𝑛⟩) ++ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩) ++ (𝑥 substr ⟨𝑛, (#‘𝑥)⟩))))
140 ccatco 13627 . . . . . . . . . . . . . . 15 ((((𝑥 substr ⟨0, 𝑛⟩) ++ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩) ∈ Word (𝐼 × 2𝑜) ∧ (𝑥 substr ⟨𝑛, (#‘𝑥)⟩) ∈ Word (𝐼 × 2𝑜) ∧ 𝑇:(𝐼 × 2𝑜)⟶𝐵) → (𝑇 ∘ (((𝑥 substr ⟨0, 𝑛⟩) ++ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩) ++ (𝑥 substr ⟨𝑛, (#‘𝑥)⟩))) = ((𝑇 ∘ ((𝑥 substr ⟨0, 𝑛⟩) ++ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩)) ++ (𝑇 ∘ (𝑥 substr ⟨𝑛, (#‘𝑥)⟩))))
141111, 105, 54, 140syl3anc 1366 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → (𝑇 ∘ (((𝑥 substr ⟨0, 𝑛⟩) ++ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩) ++ (𝑥 substr ⟨𝑛, (#‘𝑥)⟩))) = ((𝑇 ∘ ((𝑥 substr ⟨0, 𝑛⟩) ++ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩)) ++ (𝑇 ∘ (𝑥 substr ⟨𝑛, (#‘𝑥)⟩))))
142139, 141eqtrd 2685 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → (𝑇 ∘ (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩⟩)) = ((𝑇 ∘ ((𝑥 substr ⟨0, 𝑛⟩) ++ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩)) ++ (𝑇 ∘ (𝑥 substr ⟨𝑛, (#‘𝑥)⟩))))
143142oveq2d 6706 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → (𝐻 Σg (𝑇 ∘ (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩⟩))) = (𝐻 Σg ((𝑇 ∘ ((𝑥 substr ⟨0, 𝑛⟩) ++ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩)) ++ (𝑇 ∘ (𝑥 substr ⟨𝑛, (#‘𝑥)⟩)))))
144116, 136, 1433eqtr4d 2695 . . . . . . . . . . 11 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → (𝐻 Σg (𝑇𝑥)) = (𝐻 Σg (𝑇 ∘ (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩⟩))))
145 vex 3234 . . . . . . . . . . . 12 𝑥 ∈ V
146 ovex 6718 . . . . . . . . . . . 12 (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩⟩) ∈ V
147 eleq1 2718 . . . . . . . . . . . . . . 15 (𝑢 = 𝑥 → (𝑢𝑊𝑥𝑊))
148 eleq1 2718 . . . . . . . . . . . . . . 15 (𝑣 = (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩⟩) → (𝑣𝑊 ↔ (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩⟩) ∈ 𝑊))
149147, 148bi2anan9 935 . . . . . . . . . . . . . 14 ((𝑢 = 𝑥𝑣 = (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩⟩)) → ((𝑢𝑊𝑣𝑊) ↔ (𝑥𝑊 ∧ (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩⟩) ∈ 𝑊)))
15019, 149syl5bbr 274 . . . . . . . . . . . . 13 ((𝑢 = 𝑥𝑣 = (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩⟩)) → ({𝑢, 𝑣} ⊆ 𝑊 ↔ (𝑥𝑊 ∧ (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩⟩) ∈ 𝑊)))
151 coeq2 5313 . . . . . . . . . . . . . . 15 (𝑢 = 𝑥 → (𝑇𝑢) = (𝑇𝑥))
152151oveq2d 6706 . . . . . . . . . . . . . 14 (𝑢 = 𝑥 → (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑥)))
153 coeq2 5313 . . . . . . . . . . . . . . 15 (𝑣 = (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩⟩) → (𝑇𝑣) = (𝑇 ∘ (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩⟩)))
154153oveq2d 6706 . . . . . . . . . . . . . 14 (𝑣 = (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩⟩) → (𝐻 Σg (𝑇𝑣)) = (𝐻 Σg (𝑇 ∘ (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩⟩))))
155152, 154eqeqan12d 2667 . . . . . . . . . . . . 13 ((𝑢 = 𝑥𝑣 = (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩⟩)) → ((𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)) ↔ (𝐻 Σg (𝑇𝑥)) = (𝐻 Σg (𝑇 ∘ (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩⟩)))))
156150, 155anbi12d 747 . . . . . . . . . . . 12 ((𝑢 = 𝑥𝑣 = (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩⟩)) → (({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣))) ↔ ((𝑥𝑊 ∧ (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩⟩) ∈ 𝑊) ∧ (𝐻 Σg (𝑇𝑥)) = (𝐻 Σg (𝑇 ∘ (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩⟩))))))
157 eqid 2651 . . . . . . . . . . . 12 {⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))} = {⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))}
158145, 146, 156, 157braba 5021 . . . . . . . . . . 11 (𝑥{⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))} (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩⟩) ↔ ((𝑥𝑊 ∧ (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩⟩) ∈ 𝑊) ∧ (𝐻 Σg (𝑇𝑥)) = (𝐻 Σg (𝑇 ∘ (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩⟩)))))
15944, 144, 158sylanbrc 699 . . . . . . . . . 10 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2𝑜)) → 𝑥{⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))} (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩⟩))
160159ralrimivva 3000 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(#‘𝑥)))) → ∀𝑎𝐼𝑏 ∈ 2𝑜 𝑥{⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))} (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩⟩))
161160ralrimivva 3000 . . . . . . . 8 (𝜑 → ∀𝑥𝑊𝑛 ∈ (0...(#‘𝑥))∀𝑎𝐼𝑏 ∈ 2𝑜 𝑥{⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))} (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩⟩))
162 fvex 6239 . . . . . . . . . . 11 ( I ‘Word (𝐼 × 2𝑜)) ∈ V
1631, 162eqeltri 2726 . . . . . . . . . 10 𝑊 ∈ V
164 erex 7811 . . . . . . . . . 10 ({⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))} Er 𝑊 → (𝑊 ∈ V → {⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))} ∈ V))
16525, 163, 164mpisyl 21 . . . . . . . . 9 (𝜑 → {⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))} ∈ V)
166 ereq1 7794 . . . . . . . . . . 11 (𝑟 = {⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))} → (𝑟 Er 𝑊 ↔ {⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))} Er 𝑊))
167 breq 4687 . . . . . . . . . . . . 13 (𝑟 = {⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))} → (𝑥𝑟(𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩⟩) ↔ 𝑥{⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))} (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩⟩)))
1681672ralbidv 3018 . . . . . . . . . . . 12 (𝑟 = {⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))} → (∀𝑎𝐼𝑏 ∈ 2𝑜 𝑥𝑟(𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩⟩) ↔ ∀𝑎𝐼𝑏 ∈ 2𝑜 𝑥{⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))} (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩⟩)))
1691682ralbidv 3018 . . . . . . . . . . 11 (𝑟 = {⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))} → (∀𝑥𝑊𝑛 ∈ (0...(#‘𝑥))∀𝑎𝐼𝑏 ∈ 2𝑜 𝑥𝑟(𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩⟩) ↔ ∀𝑥𝑊𝑛 ∈ (0...(#‘𝑥))∀𝑎𝐼𝑏 ∈ 2𝑜 𝑥{⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))} (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩⟩)))
170166, 169anbi12d 747 . . . . . . . . . 10 (𝑟 = {⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))} → ((𝑟 Er 𝑊 ∧ ∀𝑥𝑊𝑛 ∈ (0...(#‘𝑥))∀𝑎𝐼𝑏 ∈ 2𝑜 𝑥𝑟(𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩⟩)) ↔ ({⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))} Er 𝑊 ∧ ∀𝑥𝑊𝑛 ∈ (0...(#‘𝑥))∀𝑎𝐼𝑏 ∈ 2𝑜 𝑥{⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))} (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩⟩))))
171170elabg 3383 . . . . . . . . 9 ({⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))} ∈ V → ({⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))} ∈ {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑥𝑊𝑛 ∈ (0...(#‘𝑥))∀𝑎𝐼𝑏 ∈ 2𝑜 𝑥𝑟(𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩⟩))} ↔ ({⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))} Er 𝑊 ∧ ∀𝑥𝑊𝑛 ∈ (0...(#‘𝑥))∀𝑎𝐼𝑏 ∈ 2𝑜 𝑥{⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))} (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩⟩))))
172165, 171syl 17 . . . . . . . 8 (𝜑 → ({⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))} ∈ {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑥𝑊𝑛 ∈ (0...(#‘𝑥))∀𝑎𝐼𝑏 ∈ 2𝑜 𝑥𝑟(𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩⟩))} ↔ ({⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))} Er 𝑊 ∧ ∀𝑥𝑊𝑛 ∈ (0...(#‘𝑥))∀𝑎𝐼𝑏 ∈ 2𝑜 𝑥{⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))} (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩⟩))))
17325, 161, 172mpbir2and 977 . . . . . . 7 (𝜑 → {⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))} ∈ {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑥𝑊𝑛 ∈ (0...(#‘𝑥))∀𝑎𝐼𝑏 ∈ 2𝑜 𝑥𝑟(𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩⟩))})
174 intss1 4524 . . . . . . 7 ({⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))} ∈ {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑥𝑊𝑛 ∈ (0...(#‘𝑥))∀𝑎𝐼𝑏 ∈ 2𝑜 𝑥𝑟(𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩⟩))} → {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑥𝑊𝑛 ∈ (0...(#‘𝑥))∀𝑎𝐼𝑏 ∈ 2𝑜 𝑥𝑟(𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩⟩))} ⊆ {⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))})
175173, 174syl 17 . . . . . 6 (𝜑 {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑥𝑊𝑛 ∈ (0...(#‘𝑥))∀𝑎𝐼𝑏 ∈ 2𝑜 𝑥𝑟(𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜𝑏)⟩”⟩⟩))} ⊆ {⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))})
1763, 175syl5eqss 3682 . . . . 5 (𝜑 ⊆ {⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))})
177176ssbrd 4728 . . . 4 (𝜑 → (𝐴 𝐶𝐴{⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))}𝐶))
178177imp 444 . . 3 ((𝜑𝐴 𝐶) → 𝐴{⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))}𝐶)
1791, 2efger 18177 . . . . . 6 Er 𝑊
180 errel 7796 . . . . . 6 ( Er 𝑊 → Rel )
181179, 180mp1i 13 . . . . 5 (𝜑 → Rel )
182 brrelex12 5189 . . . . 5 ((Rel 𝐴 𝐶) → (𝐴 ∈ V ∧ 𝐶 ∈ V))
183181, 182sylan 487 . . . 4 ((𝜑𝐴 𝐶) → (𝐴 ∈ V ∧ 𝐶 ∈ V))
184 preq12 4302 . . . . . . 7 ((𝑢 = 𝐴𝑣 = 𝐶) → {𝑢, 𝑣} = {𝐴, 𝐶})
185184sseq1d 3665 . . . . . 6 ((𝑢 = 𝐴𝑣 = 𝐶) → ({𝑢, 𝑣} ⊆ 𝑊 ↔ {𝐴, 𝐶} ⊆ 𝑊))
186 coeq2 5313 . . . . . . . 8 (𝑢 = 𝐴 → (𝑇𝑢) = (𝑇𝐴))
187186oveq2d 6706 . . . . . . 7 (𝑢 = 𝐴 → (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝐴)))
188 coeq2 5313 . . . . . . . 8 (𝑣 = 𝐶 → (𝑇𝑣) = (𝑇𝐶))
189188oveq2d 6706 . . . . . . 7 (𝑣 = 𝐶 → (𝐻 Σg (𝑇𝑣)) = (𝐻 Σg (𝑇𝐶)))
190187, 189eqeqan12d 2667 . . . . . 6 ((𝑢 = 𝐴𝑣 = 𝐶) → ((𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)) ↔ (𝐻 Σg (𝑇𝐴)) = (𝐻 Σg (𝑇𝐶))))
191185, 190anbi12d 747 . . . . 5 ((𝑢 = 𝐴𝑣 = 𝐶) → (({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣))) ↔ ({𝐴, 𝐶} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝐴)) = (𝐻 Σg (𝑇𝐶)))))
192191, 157brabga 5018 . . . 4 ((𝐴 ∈ V ∧ 𝐶 ∈ V) → (𝐴{⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))}𝐶 ↔ ({𝐴, 𝐶} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝐴)) = (𝐻 Σg (𝑇𝐶)))))
193183, 192syl 17 . . 3 ((𝜑𝐴 𝐶) → (𝐴{⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))}𝐶 ↔ ({𝐴, 𝐶} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝐴)) = (𝐻 Σg (𝑇𝐶)))))
194178, 193mpbid 222 . 2 ((𝜑𝐴 𝐶) → ({𝐴, 𝐶} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝐴)) = (𝐻 Σg (𝑇𝐶))))
195194simprd 478 1 ((𝜑𝐴 𝐶) → (𝐻 Σg (𝑇𝐴)) = (𝐻 Σg (𝑇𝐶)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383   = wceq 1523   ∈ wcel 2030  {cab 2637  ∀wral 2941  Vcvv 3231   ∖ cdif 3604   ∩ cin 3606   ⊆ wss 3607  ∅c0 3948  ifcif 4119  {cpr 4212  ⟨cop 4216  ⟨cotp 4218  ∩ cint 4507   class class class wbr 4685  {copab 4745   I cid 5052   × cxp 5141   ∘ ccom 5147  Rel wrel 5148  ⟶wf 5922  ‘cfv 5926  (class class class)co 6690   ↦ cmpt2 6692  1𝑜c1o 7598  2𝑜c2o 7599   Er wer 7784  0cc0 9974  ℕ0cn0 11330  ℤ≥cuz 11725  ...cfz 12364  #chash 13157  Word cword 13323   ++ cconcat 13325   substr csubstr 13327   splice csplice 13328  ⟨“cs2 13632  Basecbs 15904  +gcplusg 15988  0gc0g 16147   Σg cgsu 16148  Mndcmnd 17341  Grpcgrp 17469  invgcminusg 17470   ~FG cefg 18165 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-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-iin 4555  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-pm 7902  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-n0 11331  df-z 11416  df-uz 11726  df-fz 12365  df-fzo 12505  df-seq 12842  df-hash 13158  df-word 13331  df-concat 13333  df-s1 13334  df-substr 13335  df-splice 13336  df-s2 13639  df-ndx 15907  df-slot 15908  df-base 15910  df-sets 15911  df-ress 15912  df-plusg 16001  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-efg 18168 This theorem is referenced by:  frgpupf  18232
 Copyright terms: Public domain W3C validator