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

Theorem frgpuplem 19804
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 𝑇 = (𝑦𝐼, 𝑧 ∈ 2o ↦ if(𝑧 = ∅, (𝐹𝑦), (𝑁‘(𝐹𝑦))))
frgpup.h (𝜑𝐻 ∈ Grp)
frgpup.i (𝜑𝐼𝑉)
frgpup.a (𝜑𝐹:𝐼𝐵)
frgpup.w 𝑊 = ( I ‘Word (𝐼 × 2o))
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 (𝐼 × 2o))
2 frgpup.r . . . . . . 7 = ( ~FG𝐼)
31, 2efgval 19749 . . . . . 6 = {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑥𝑊𝑛 ∈ (0...(♯‘𝑥))∀𝑎𝐼𝑏 ∈ 2o 𝑥𝑟(𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩⟩))}
4 coeq2 5871 . . . . . . . . . . . . 13 (𝑢 = 𝑣 → (𝑇𝑢) = (𝑇𝑣))
54oveq2d 7446 . . . . . . . . . . . 12 (𝑢 = 𝑣 → (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))
6 eqid 2734 . . . . . . . . . . . 12 {⟨𝑢, 𝑣⟩ ∣ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣))} = {⟨𝑢, 𝑣⟩ ∣ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣))}
75, 6eqer 8779 . . . . . . . . . . 11 {⟨𝑢, 𝑣⟩ ∣ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣))} Er V
87a1i 11 . . . . . . . . . 10 (𝜑 → {⟨𝑢, 𝑣⟩ ∣ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣))} Er V)
9 ssv 4019 . . . . . . . . . . 11 𝑊 ⊆ V
109a1i 11 . . . . . . . . . 10 (𝜑𝑊 ⊆ V)
118, 10erinxp 8829 . . . . . . . . 9 (𝜑 → ({⟨𝑢, 𝑣⟩ ∣ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣))} ∩ (𝑊 × 𝑊)) Er 𝑊)
12 df-xp 5694 . . . . . . . . . . . . 13 (𝑊 × 𝑊) = {⟨𝑢, 𝑣⟩ ∣ (𝑢𝑊𝑣𝑊)}
1312ineq1i 4223 . . . . . . . . . . . 12 ((𝑊 × 𝑊) ∩ {⟨𝑢, 𝑣⟩ ∣ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣))}) = ({⟨𝑢, 𝑣⟩ ∣ (𝑢𝑊𝑣𝑊)} ∩ {⟨𝑢, 𝑣⟩ ∣ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣))})
14 incom 4216 . . . . . . . . . . . 12 ((𝑊 × 𝑊) ∩ {⟨𝑢, 𝑣⟩ ∣ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣))}) = ({⟨𝑢, 𝑣⟩ ∣ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣))} ∩ (𝑊 × 𝑊))
15 inopab 5841 . . . . . . . . . . . 12 ({⟨𝑢, 𝑣⟩ ∣ (𝑢𝑊𝑣𝑊)} ∩ {⟨𝑢, 𝑣⟩ ∣ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣))}) = {⟨𝑢, 𝑣⟩ ∣ ((𝑢𝑊𝑣𝑊) ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))}
1613, 14, 153eqtr3i 2770 . . . . . . . . . . 11 ({⟨𝑢, 𝑣⟩ ∣ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣))} ∩ (𝑊 × 𝑊)) = {⟨𝑢, 𝑣⟩ ∣ ((𝑢𝑊𝑣𝑊) ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))}
17 vex 3481 . . . . . . . . . . . . . 14 𝑢 ∈ V
18 vex 3481 . . . . . . . . . . . . . 14 𝑣 ∈ V
1917, 18prss 4824 . . . . . . . . . . . . 13 ((𝑢𝑊𝑣𝑊) ↔ {𝑢, 𝑣} ⊆ 𝑊)
2019anbi1i 624 . . . . . . . . . . . 12 (((𝑢𝑊𝑣𝑊) ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣))) ↔ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣))))
2120opabbii 5214 . . . . . . . . . . 11 {⟨𝑢, 𝑣⟩ ∣ ((𝑢𝑊𝑣𝑊) ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))} = {⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))}
2216, 21eqtri 2762 . . . . . . . . . 10 ({⟨𝑢, 𝑣⟩ ∣ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣))} ∩ (𝑊 × 𝑊)) = {⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))}
23 ereq1 8750 . . . . . . . . . 10 (({⟨𝑢, 𝑣⟩ ∣ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣))} ∩ (𝑊 × 𝑊)) = {⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))} → (({⟨𝑢, 𝑣⟩ ∣ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣))} ∩ (𝑊 × 𝑊)) Er 𝑊 ↔ {⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))} Er 𝑊))
2422, 23ax-mp 5 . . . . . . . . 9 (({⟨𝑢, 𝑣⟩ ∣ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣))} ∩ (𝑊 × 𝑊)) Er 𝑊 ↔ {⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))} Er 𝑊)
2511, 24sylib 218 . . . . . . . 8 (𝜑 → {⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))} Er 𝑊)
26 simplrl 777 . . . . . . . . . . 11 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2o)) → 𝑥𝑊)
27 fviss 6985 . . . . . . . . . . . . . . 15 ( I ‘Word (𝐼 × 2o)) ⊆ Word (𝐼 × 2o)
281, 27eqsstri 4029 . . . . . . . . . . . . . 14 𝑊 ⊆ Word (𝐼 × 2o)
2928, 26sselid 3992 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2o)) → 𝑥 ∈ Word (𝐼 × 2o))
30 opelxpi 5725 . . . . . . . . . . . . . . 15 ((𝑎𝐼𝑏 ∈ 2o) → ⟨𝑎, 𝑏⟩ ∈ (𝐼 × 2o))
3130adantl 481 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2o)) → ⟨𝑎, 𝑏⟩ ∈ (𝐼 × 2o))
32 simprl 771 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2o)) → 𝑎𝐼)
33 2oconcl 8539 . . . . . . . . . . . . . . . 16 (𝑏 ∈ 2o → (1o𝑏) ∈ 2o)
3433ad2antll 729 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2o)) → (1o𝑏) ∈ 2o)
3532, 34opelxpd 5727 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2o)) → ⟨𝑎, (1o𝑏)⟩ ∈ (𝐼 × 2o))
3631, 35s2cld 14906 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2o)) → ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩ ∈ Word (𝐼 × 2o))
37 splcl 14786 . . . . . . . . . . . . 13 ((𝑥 ∈ Word (𝐼 × 2o) ∧ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩ ∈ Word (𝐼 × 2o)) → (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩⟩) ∈ Word (𝐼 × 2o))
3829, 36, 37syl2anc 584 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2o)) → (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩⟩) ∈ Word (𝐼 × 2o))
391efgrcl 19747 . . . . . . . . . . . . . 14 (𝑥𝑊 → (𝐼 ∈ V ∧ 𝑊 = Word (𝐼 × 2o)))
4026, 39syl 17 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2o)) → (𝐼 ∈ V ∧ 𝑊 = Word (𝐼 × 2o)))
4140simprd 495 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2o)) → 𝑊 = Word (𝐼 × 2o))
4238, 41eleqtrrd 2841 . . . . . . . . . . 11 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2o)) → (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩⟩) ∈ 𝑊)
43 pfxcl 14711 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ Word (𝐼 × 2o) → (𝑥 prefix 𝑛) ∈ Word (𝐼 × 2o))
4429, 43syl 17 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2o)) → (𝑥 prefix 𝑛) ∈ Word (𝐼 × 2o))
45 frgpup.b . . . . . . . . . . . . . . . . . . 19 𝐵 = (Base‘𝐻)
46 frgpup.n . . . . . . . . . . . . . . . . . . 19 𝑁 = (invg𝐻)
47 frgpup.t . . . . . . . . . . . . . . . . . . 19 𝑇 = (𝑦𝐼, 𝑧 ∈ 2o ↦ if(𝑧 = ∅, (𝐹𝑦), (𝑁‘(𝐹𝑦))))
48 frgpup.h . . . . . . . . . . . . . . . . . . 19 (𝜑𝐻 ∈ Grp)
49 frgpup.i . . . . . . . . . . . . . . . . . . 19 (𝜑𝐼𝑉)
50 frgpup.a . . . . . . . . . . . . . . . . . . 19 (𝜑𝐹:𝐼𝐵)
5145, 46, 47, 48, 49, 50frgpuptf 19802 . . . . . . . . . . . . . . . . . 18 (𝜑𝑇:(𝐼 × 2o)⟶𝐵)
5251ad2antrr 726 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2o)) → 𝑇:(𝐼 × 2o)⟶𝐵)
53 ccatco 14870 . . . . . . . . . . . . . . . . 17 (((𝑥 prefix 𝑛) ∈ Word (𝐼 × 2o) ∧ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩ ∈ Word (𝐼 × 2o) ∧ 𝑇:(𝐼 × 2o)⟶𝐵) → (𝑇 ∘ ((𝑥 prefix 𝑛) ++ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩)) = ((𝑇 ∘ (𝑥 prefix 𝑛)) ++ (𝑇 ∘ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩)))
5444, 36, 52, 53syl3anc 1370 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2o)) → (𝑇 ∘ ((𝑥 prefix 𝑛) ++ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩)) = ((𝑇 ∘ (𝑥 prefix 𝑛)) ++ (𝑇 ∘ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩)))
5554oveq2d 7446 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2o)) → (𝐻 Σg (𝑇 ∘ ((𝑥 prefix 𝑛) ++ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩))) = (𝐻 Σg ((𝑇 ∘ (𝑥 prefix 𝑛)) ++ (𝑇 ∘ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩))))
5648ad2antrr 726 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2o)) → 𝐻 ∈ Grp)
5756grpmndd 18976 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2o)) → 𝐻 ∈ Mnd)
58 wrdco 14866 . . . . . . . . . . . . . . . . 17 (((𝑥 prefix 𝑛) ∈ Word (𝐼 × 2o) ∧ 𝑇:(𝐼 × 2o)⟶𝐵) → (𝑇 ∘ (𝑥 prefix 𝑛)) ∈ Word 𝐵)
5944, 52, 58syl2anc 584 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2o)) → (𝑇 ∘ (𝑥 prefix 𝑛)) ∈ Word 𝐵)
60 wrdco 14866 . . . . . . . . . . . . . . . . 17 ((⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩ ∈ Word (𝐼 × 2o) ∧ 𝑇:(𝐼 × 2o)⟶𝐵) → (𝑇 ∘ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩) ∈ Word 𝐵)
6136, 52, 60syl2anc 584 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2o)) → (𝑇 ∘ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩) ∈ Word 𝐵)
62 eqid 2734 . . . . . . . . . . . . . . . . 17 (+g𝐻) = (+g𝐻)
6345, 62gsumccat 18866 . . . . . . . . . . . . . . . 16 ((𝐻 ∈ Mnd ∧ (𝑇 ∘ (𝑥 prefix 𝑛)) ∈ Word 𝐵 ∧ (𝑇 ∘ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩) ∈ Word 𝐵) → (𝐻 Σg ((𝑇 ∘ (𝑥 prefix 𝑛)) ++ (𝑇 ∘ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩))) = ((𝐻 Σg (𝑇 ∘ (𝑥 prefix 𝑛)))(+g𝐻)(𝐻 Σg (𝑇 ∘ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩))))
6457, 59, 61, 63syl3anc 1370 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2o)) → (𝐻 Σg ((𝑇 ∘ (𝑥 prefix 𝑛)) ++ (𝑇 ∘ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩))) = ((𝐻 Σg (𝑇 ∘ (𝑥 prefix 𝑛)))(+g𝐻)(𝐻 Σg (𝑇 ∘ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩))))
6552, 31, 35s2co 14955 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2o)) → (𝑇 ∘ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩) = ⟨“(𝑇‘⟨𝑎, 𝑏⟩)(𝑇‘⟨𝑎, (1o𝑏)⟩)”⟩)
66 df-ov 7433 . . . . . . . . . . . . . . . . . . . . . 22 (𝑎𝑇𝑏) = (𝑇‘⟨𝑎, 𝑏⟩)
6766a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2o)) → (𝑎𝑇𝑏) = (𝑇‘⟨𝑎, 𝑏⟩))
6866fveq2i 6909 . . . . . . . . . . . . . . . . . . . . . 22 (𝑁‘(𝑎𝑇𝑏)) = (𝑁‘(𝑇‘⟨𝑎, 𝑏⟩))
69 df-ov 7433 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑎(𝑦𝐼, 𝑧 ∈ 2o ↦ ⟨𝑦, (1o𝑧)⟩)𝑏) = ((𝑦𝐼, 𝑧 ∈ 2o ↦ ⟨𝑦, (1o𝑧)⟩)‘⟨𝑎, 𝑏⟩)
70 eqid 2734 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑦𝐼, 𝑧 ∈ 2o ↦ ⟨𝑦, (1o𝑧)⟩) = (𝑦𝐼, 𝑧 ∈ 2o ↦ ⟨𝑦, (1o𝑧)⟩)
7170efgmval 19744 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑎𝐼𝑏 ∈ 2o) → (𝑎(𝑦𝐼, 𝑧 ∈ 2o ↦ ⟨𝑦, (1o𝑧)⟩)𝑏) = ⟨𝑎, (1o𝑏)⟩)
7269, 71eqtr3id 2788 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑎𝐼𝑏 ∈ 2o) → ((𝑦𝐼, 𝑧 ∈ 2o ↦ ⟨𝑦, (1o𝑧)⟩)‘⟨𝑎, 𝑏⟩) = ⟨𝑎, (1o𝑏)⟩)
7372adantl 481 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2o)) → ((𝑦𝐼, 𝑧 ∈ 2o ↦ ⟨𝑦, (1o𝑧)⟩)‘⟨𝑎, 𝑏⟩) = ⟨𝑎, (1o𝑏)⟩)
7473fveq2d 6910 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2o)) → (𝑇‘((𝑦𝐼, 𝑧 ∈ 2o ↦ ⟨𝑦, (1o𝑧)⟩)‘⟨𝑎, 𝑏⟩)) = (𝑇‘⟨𝑎, (1o𝑏)⟩))
7545, 46, 47, 48, 49, 50, 70frgpuptinv 19803 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ ⟨𝑎, 𝑏⟩ ∈ (𝐼 × 2o)) → (𝑇‘((𝑦𝐼, 𝑧 ∈ 2o ↦ ⟨𝑦, (1o𝑧)⟩)‘⟨𝑎, 𝑏⟩)) = (𝑁‘(𝑇‘⟨𝑎, 𝑏⟩)))
7630, 75sylan2 593 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑎𝐼𝑏 ∈ 2o)) → (𝑇‘((𝑦𝐼, 𝑧 ∈ 2o ↦ ⟨𝑦, (1o𝑧)⟩)‘⟨𝑎, 𝑏⟩)) = (𝑁‘(𝑇‘⟨𝑎, 𝑏⟩)))
7776adantlr 715 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2o)) → (𝑇‘((𝑦𝐼, 𝑧 ∈ 2o ↦ ⟨𝑦, (1o𝑧)⟩)‘⟨𝑎, 𝑏⟩)) = (𝑁‘(𝑇‘⟨𝑎, 𝑏⟩)))
7874, 77eqtr3d 2776 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2o)) → (𝑇‘⟨𝑎, (1o𝑏)⟩) = (𝑁‘(𝑇‘⟨𝑎, 𝑏⟩)))
7968, 78eqtr4id 2793 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2o)) → (𝑁‘(𝑎𝑇𝑏)) = (𝑇‘⟨𝑎, (1o𝑏)⟩))
8067, 79s2eqd 14898 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2o)) → ⟨“(𝑎𝑇𝑏)(𝑁‘(𝑎𝑇𝑏))”⟩ = ⟨“(𝑇‘⟨𝑎, 𝑏⟩)(𝑇‘⟨𝑎, (1o𝑏)⟩)”⟩)
8165, 80eqtr4d 2777 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2o)) → (𝑇 ∘ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩) = ⟨“(𝑎𝑇𝑏)(𝑁‘(𝑎𝑇𝑏))”⟩)
8281oveq2d 7446 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2o)) → (𝐻 Σg (𝑇 ∘ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩)) = (𝐻 Σg ⟨“(𝑎𝑇𝑏)(𝑁‘(𝑎𝑇𝑏))”⟩))
83 simprr 773 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2o)) → 𝑏 ∈ 2o)
8452, 32, 83fovcdmd 7604 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2o)) → (𝑎𝑇𝑏) ∈ 𝐵)
8545, 46grpinvcl 19017 . . . . . . . . . . . . . . . . . . . 20 ((𝐻 ∈ Grp ∧ (𝑎𝑇𝑏) ∈ 𝐵) → (𝑁‘(𝑎𝑇𝑏)) ∈ 𝐵)
8656, 84, 85syl2anc 584 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2o)) → (𝑁‘(𝑎𝑇𝑏)) ∈ 𝐵)
8745, 62gsumws2 18867 . . . . . . . . . . . . . . . . . . 19 ((𝐻 ∈ Mnd ∧ (𝑎𝑇𝑏) ∈ 𝐵 ∧ (𝑁‘(𝑎𝑇𝑏)) ∈ 𝐵) → (𝐻 Σg ⟨“(𝑎𝑇𝑏)(𝑁‘(𝑎𝑇𝑏))”⟩) = ((𝑎𝑇𝑏)(+g𝐻)(𝑁‘(𝑎𝑇𝑏))))
8857, 84, 86, 87syl3anc 1370 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2o)) → (𝐻 Σg ⟨“(𝑎𝑇𝑏)(𝑁‘(𝑎𝑇𝑏))”⟩) = ((𝑎𝑇𝑏)(+g𝐻)(𝑁‘(𝑎𝑇𝑏))))
89 eqid 2734 . . . . . . . . . . . . . . . . . . . 20 (0g𝐻) = (0g𝐻)
9045, 62, 89, 46grprinv 19020 . . . . . . . . . . . . . . . . . . 19 ((𝐻 ∈ Grp ∧ (𝑎𝑇𝑏) ∈ 𝐵) → ((𝑎𝑇𝑏)(+g𝐻)(𝑁‘(𝑎𝑇𝑏))) = (0g𝐻))
9156, 84, 90syl2anc 584 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2o)) → ((𝑎𝑇𝑏)(+g𝐻)(𝑁‘(𝑎𝑇𝑏))) = (0g𝐻))
9282, 88, 913eqtrd 2778 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2o)) → (𝐻 Σg (𝑇 ∘ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩)) = (0g𝐻))
9392oveq2d 7446 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2o)) → ((𝐻 Σg (𝑇 ∘ (𝑥 prefix 𝑛)))(+g𝐻)(𝐻 Σg (𝑇 ∘ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩))) = ((𝐻 Σg (𝑇 ∘ (𝑥 prefix 𝑛)))(+g𝐻)(0g𝐻)))
9445gsumwcl 18864 . . . . . . . . . . . . . . . . . 18 ((𝐻 ∈ Mnd ∧ (𝑇 ∘ (𝑥 prefix 𝑛)) ∈ Word 𝐵) → (𝐻 Σg (𝑇 ∘ (𝑥 prefix 𝑛))) ∈ 𝐵)
9557, 59, 94syl2anc 584 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2o)) → (𝐻 Σg (𝑇 ∘ (𝑥 prefix 𝑛))) ∈ 𝐵)
9645, 62, 89grprid 18998 . . . . . . . . . . . . . . . . 17 ((𝐻 ∈ Grp ∧ (𝐻 Σg (𝑇 ∘ (𝑥 prefix 𝑛))) ∈ 𝐵) → ((𝐻 Σg (𝑇 ∘ (𝑥 prefix 𝑛)))(+g𝐻)(0g𝐻)) = (𝐻 Σg (𝑇 ∘ (𝑥 prefix 𝑛))))
9756, 95, 96syl2anc 584 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2o)) → ((𝐻 Σg (𝑇 ∘ (𝑥 prefix 𝑛)))(+g𝐻)(0g𝐻)) = (𝐻 Σg (𝑇 ∘ (𝑥 prefix 𝑛))))
9893, 97eqtrd 2774 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2o)) → ((𝐻 Σg (𝑇 ∘ (𝑥 prefix 𝑛)))(+g𝐻)(𝐻 Σg (𝑇 ∘ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩))) = (𝐻 Σg (𝑇 ∘ (𝑥 prefix 𝑛))))
9955, 64, 983eqtrrd 2779 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2o)) → (𝐻 Σg (𝑇 ∘ (𝑥 prefix 𝑛))) = (𝐻 Σg (𝑇 ∘ ((𝑥 prefix 𝑛) ++ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩))))
10099oveq1d 7445 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2o)) → ((𝐻 Σg (𝑇 ∘ (𝑥 prefix 𝑛)))(+g𝐻)(𝐻 Σg (𝑇 ∘ (𝑥 substr ⟨𝑛, (♯‘𝑥)⟩)))) = ((𝐻 Σg (𝑇 ∘ ((𝑥 prefix 𝑛) ++ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩)))(+g𝐻)(𝐻 Σg (𝑇 ∘ (𝑥 substr ⟨𝑛, (♯‘𝑥)⟩)))))
101 swrdcl 14679 . . . . . . . . . . . . . . . 16 (𝑥 ∈ Word (𝐼 × 2o) → (𝑥 substr ⟨𝑛, (♯‘𝑥)⟩) ∈ Word (𝐼 × 2o))
10229, 101syl 17 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2o)) → (𝑥 substr ⟨𝑛, (♯‘𝑥)⟩) ∈ Word (𝐼 × 2o))
103 wrdco 14866 . . . . . . . . . . . . . . 15 (((𝑥 substr ⟨𝑛, (♯‘𝑥)⟩) ∈ Word (𝐼 × 2o) ∧ 𝑇:(𝐼 × 2o)⟶𝐵) → (𝑇 ∘ (𝑥 substr ⟨𝑛, (♯‘𝑥)⟩)) ∈ Word 𝐵)
104102, 52, 103syl2anc 584 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2o)) → (𝑇 ∘ (𝑥 substr ⟨𝑛, (♯‘𝑥)⟩)) ∈ Word 𝐵)
10545, 62gsumccat 18866 . . . . . . . . . . . . . 14 ((𝐻 ∈ Mnd ∧ (𝑇 ∘ (𝑥 prefix 𝑛)) ∈ Word 𝐵 ∧ (𝑇 ∘ (𝑥 substr ⟨𝑛, (♯‘𝑥)⟩)) ∈ Word 𝐵) → (𝐻 Σg ((𝑇 ∘ (𝑥 prefix 𝑛)) ++ (𝑇 ∘ (𝑥 substr ⟨𝑛, (♯‘𝑥)⟩)))) = ((𝐻 Σg (𝑇 ∘ (𝑥 prefix 𝑛)))(+g𝐻)(𝐻 Σg (𝑇 ∘ (𝑥 substr ⟨𝑛, (♯‘𝑥)⟩)))))
10657, 59, 104, 105syl3anc 1370 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2o)) → (𝐻 Σg ((𝑇 ∘ (𝑥 prefix 𝑛)) ++ (𝑇 ∘ (𝑥 substr ⟨𝑛, (♯‘𝑥)⟩)))) = ((𝐻 Σg (𝑇 ∘ (𝑥 prefix 𝑛)))(+g𝐻)(𝐻 Σg (𝑇 ∘ (𝑥 substr ⟨𝑛, (♯‘𝑥)⟩)))))
107 ccatcl 14608 . . . . . . . . . . . . . . . 16 (((𝑥 prefix 𝑛) ∈ Word (𝐼 × 2o) ∧ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩ ∈ Word (𝐼 × 2o)) → ((𝑥 prefix 𝑛) ++ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩) ∈ Word (𝐼 × 2o))
10844, 36, 107syl2anc 584 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2o)) → ((𝑥 prefix 𝑛) ++ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩) ∈ Word (𝐼 × 2o))
109 wrdco 14866 . . . . . . . . . . . . . . 15 ((((𝑥 prefix 𝑛) ++ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩) ∈ Word (𝐼 × 2o) ∧ 𝑇:(𝐼 × 2o)⟶𝐵) → (𝑇 ∘ ((𝑥 prefix 𝑛) ++ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩)) ∈ Word 𝐵)
110108, 52, 109syl2anc 584 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2o)) → (𝑇 ∘ ((𝑥 prefix 𝑛) ++ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩)) ∈ Word 𝐵)
11145, 62gsumccat 18866 . . . . . . . . . . . . . 14 ((𝐻 ∈ Mnd ∧ (𝑇 ∘ ((𝑥 prefix 𝑛) ++ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩)) ∈ Word 𝐵 ∧ (𝑇 ∘ (𝑥 substr ⟨𝑛, (♯‘𝑥)⟩)) ∈ Word 𝐵) → (𝐻 Σg ((𝑇 ∘ ((𝑥 prefix 𝑛) ++ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩)) ++ (𝑇 ∘ (𝑥 substr ⟨𝑛, (♯‘𝑥)⟩)))) = ((𝐻 Σg (𝑇 ∘ ((𝑥 prefix 𝑛) ++ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩)))(+g𝐻)(𝐻 Σg (𝑇 ∘ (𝑥 substr ⟨𝑛, (♯‘𝑥)⟩)))))
11257, 110, 104, 111syl3anc 1370 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2o)) → (𝐻 Σg ((𝑇 ∘ ((𝑥 prefix 𝑛) ++ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩)) ++ (𝑇 ∘ (𝑥 substr ⟨𝑛, (♯‘𝑥)⟩)))) = ((𝐻 Σg (𝑇 ∘ ((𝑥 prefix 𝑛) ++ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩)))(+g𝐻)(𝐻 Σg (𝑇 ∘ (𝑥 substr ⟨𝑛, (♯‘𝑥)⟩)))))
113100, 106, 1123eqtr4d 2784 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2o)) → (𝐻 Σg ((𝑇 ∘ (𝑥 prefix 𝑛)) ++ (𝑇 ∘ (𝑥 substr ⟨𝑛, (♯‘𝑥)⟩)))) = (𝐻 Σg ((𝑇 ∘ ((𝑥 prefix 𝑛) ++ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩)) ++ (𝑇 ∘ (𝑥 substr ⟨𝑛, (♯‘𝑥)⟩)))))
114 simplrr 778 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2o)) → 𝑛 ∈ (0...(♯‘𝑥)))
115 lencl 14567 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ Word (𝐼 × 2o) → (♯‘𝑥) ∈ ℕ0)
11629, 115syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2o)) → (♯‘𝑥) ∈ ℕ0)
117 nn0uz 12917 . . . . . . . . . . . . . . . . . . 19 0 = (ℤ‘0)
118116, 117eleqtrdi 2848 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2o)) → (♯‘𝑥) ∈ (ℤ‘0))
119 eluzfz2 13568 . . . . . . . . . . . . . . . . . 18 ((♯‘𝑥) ∈ (ℤ‘0) → (♯‘𝑥) ∈ (0...(♯‘𝑥)))
120118, 119syl 17 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2o)) → (♯‘𝑥) ∈ (0...(♯‘𝑥)))
121 ccatpfx 14735 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ Word (𝐼 × 2o) ∧ 𝑛 ∈ (0...(♯‘𝑥)) ∧ (♯‘𝑥) ∈ (0...(♯‘𝑥))) → ((𝑥 prefix 𝑛) ++ (𝑥 substr ⟨𝑛, (♯‘𝑥)⟩)) = (𝑥 prefix (♯‘𝑥)))
12229, 114, 120, 121syl3anc 1370 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2o)) → ((𝑥 prefix 𝑛) ++ (𝑥 substr ⟨𝑛, (♯‘𝑥)⟩)) = (𝑥 prefix (♯‘𝑥)))
123 pfxid 14718 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ Word (𝐼 × 2o) → (𝑥 prefix (♯‘𝑥)) = 𝑥)
12429, 123syl 17 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2o)) → (𝑥 prefix (♯‘𝑥)) = 𝑥)
125122, 124eqtrd 2774 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2o)) → ((𝑥 prefix 𝑛) ++ (𝑥 substr ⟨𝑛, (♯‘𝑥)⟩)) = 𝑥)
126125coeq2d 5875 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2o)) → (𝑇 ∘ ((𝑥 prefix 𝑛) ++ (𝑥 substr ⟨𝑛, (♯‘𝑥)⟩))) = (𝑇𝑥))
127 ccatco 14870 . . . . . . . . . . . . . . 15 (((𝑥 prefix 𝑛) ∈ Word (𝐼 × 2o) ∧ (𝑥 substr ⟨𝑛, (♯‘𝑥)⟩) ∈ Word (𝐼 × 2o) ∧ 𝑇:(𝐼 × 2o)⟶𝐵) → (𝑇 ∘ ((𝑥 prefix 𝑛) ++ (𝑥 substr ⟨𝑛, (♯‘𝑥)⟩))) = ((𝑇 ∘ (𝑥 prefix 𝑛)) ++ (𝑇 ∘ (𝑥 substr ⟨𝑛, (♯‘𝑥)⟩))))
12844, 102, 52, 127syl3anc 1370 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2o)) → (𝑇 ∘ ((𝑥 prefix 𝑛) ++ (𝑥 substr ⟨𝑛, (♯‘𝑥)⟩))) = ((𝑇 ∘ (𝑥 prefix 𝑛)) ++ (𝑇 ∘ (𝑥 substr ⟨𝑛, (♯‘𝑥)⟩))))
129126, 128eqtr3d 2776 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2o)) → (𝑇𝑥) = ((𝑇 ∘ (𝑥 prefix 𝑛)) ++ (𝑇 ∘ (𝑥 substr ⟨𝑛, (♯‘𝑥)⟩))))
130129oveq2d 7446 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2o)) → (𝐻 Σg (𝑇𝑥)) = (𝐻 Σg ((𝑇 ∘ (𝑥 prefix 𝑛)) ++ (𝑇 ∘ (𝑥 substr ⟨𝑛, (♯‘𝑥)⟩)))))
131 splval 14785 . . . . . . . . . . . . . . . 16 ((𝑥𝑊 ∧ (𝑛 ∈ (0...(♯‘𝑥)) ∧ 𝑛 ∈ (0...(♯‘𝑥)) ∧ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩ ∈ Word (𝐼 × 2o))) → (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩⟩) = (((𝑥 prefix 𝑛) ++ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩) ++ (𝑥 substr ⟨𝑛, (♯‘𝑥)⟩)))
13226, 114, 114, 36, 131syl13anc 1371 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2o)) → (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩⟩) = (((𝑥 prefix 𝑛) ++ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩) ++ (𝑥 substr ⟨𝑛, (♯‘𝑥)⟩)))
133132coeq2d 5875 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2o)) → (𝑇 ∘ (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩⟩)) = (𝑇 ∘ (((𝑥 prefix 𝑛) ++ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩) ++ (𝑥 substr ⟨𝑛, (♯‘𝑥)⟩))))
134 ccatco 14870 . . . . . . . . . . . . . . 15 ((((𝑥 prefix 𝑛) ++ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩) ∈ Word (𝐼 × 2o) ∧ (𝑥 substr ⟨𝑛, (♯‘𝑥)⟩) ∈ Word (𝐼 × 2o) ∧ 𝑇:(𝐼 × 2o)⟶𝐵) → (𝑇 ∘ (((𝑥 prefix 𝑛) ++ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩) ++ (𝑥 substr ⟨𝑛, (♯‘𝑥)⟩))) = ((𝑇 ∘ ((𝑥 prefix 𝑛) ++ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩)) ++ (𝑇 ∘ (𝑥 substr ⟨𝑛, (♯‘𝑥)⟩))))
135108, 102, 52, 134syl3anc 1370 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2o)) → (𝑇 ∘ (((𝑥 prefix 𝑛) ++ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩) ++ (𝑥 substr ⟨𝑛, (♯‘𝑥)⟩))) = ((𝑇 ∘ ((𝑥 prefix 𝑛) ++ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩)) ++ (𝑇 ∘ (𝑥 substr ⟨𝑛, (♯‘𝑥)⟩))))
136133, 135eqtrd 2774 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2o)) → (𝑇 ∘ (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩⟩)) = ((𝑇 ∘ ((𝑥 prefix 𝑛) ++ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩)) ++ (𝑇 ∘ (𝑥 substr ⟨𝑛, (♯‘𝑥)⟩))))
137136oveq2d 7446 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2o)) → (𝐻 Σg (𝑇 ∘ (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩⟩))) = (𝐻 Σg ((𝑇 ∘ ((𝑥 prefix 𝑛) ++ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩)) ++ (𝑇 ∘ (𝑥 substr ⟨𝑛, (♯‘𝑥)⟩)))))
138113, 130, 1373eqtr4d 2784 . . . . . . . . . . 11 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2o)) → (𝐻 Σg (𝑇𝑥)) = (𝐻 Σg (𝑇 ∘ (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩⟩))))
139 vex 3481 . . . . . . . . . . . 12 𝑥 ∈ V
140 ovex 7463 . . . . . . . . . . . 12 (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩⟩) ∈ V
141 eleq1 2826 . . . . . . . . . . . . . . 15 (𝑢 = 𝑥 → (𝑢𝑊𝑥𝑊))
142 eleq1 2826 . . . . . . . . . . . . . . 15 (𝑣 = (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩⟩) → (𝑣𝑊 ↔ (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩⟩) ∈ 𝑊))
143141, 142bi2anan9 638 . . . . . . . . . . . . . 14 ((𝑢 = 𝑥𝑣 = (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩⟩)) → ((𝑢𝑊𝑣𝑊) ↔ (𝑥𝑊 ∧ (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩⟩) ∈ 𝑊)))
14419, 143bitr3id 285 . . . . . . . . . . . . 13 ((𝑢 = 𝑥𝑣 = (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩⟩)) → ({𝑢, 𝑣} ⊆ 𝑊 ↔ (𝑥𝑊 ∧ (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩⟩) ∈ 𝑊)))
145 coeq2 5871 . . . . . . . . . . . . . . 15 (𝑢 = 𝑥 → (𝑇𝑢) = (𝑇𝑥))
146145oveq2d 7446 . . . . . . . . . . . . . 14 (𝑢 = 𝑥 → (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑥)))
147 coeq2 5871 . . . . . . . . . . . . . . 15 (𝑣 = (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩⟩) → (𝑇𝑣) = (𝑇 ∘ (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩⟩)))
148147oveq2d 7446 . . . . . . . . . . . . . 14 (𝑣 = (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩⟩) → (𝐻 Σg (𝑇𝑣)) = (𝐻 Σg (𝑇 ∘ (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩⟩))))
149146, 148eqeqan12d 2748 . . . . . . . . . . . . 13 ((𝑢 = 𝑥𝑣 = (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩⟩)) → ((𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)) ↔ (𝐻 Σg (𝑇𝑥)) = (𝐻 Σg (𝑇 ∘ (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩⟩)))))
150144, 149anbi12d 632 . . . . . . . . . . . 12 ((𝑢 = 𝑥𝑣 = (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩⟩)) → (({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣))) ↔ ((𝑥𝑊 ∧ (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩⟩) ∈ 𝑊) ∧ (𝐻 Σg (𝑇𝑥)) = (𝐻 Σg (𝑇 ∘ (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩⟩))))))
151 eqid 2734 . . . . . . . . . . . 12 {⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))} = {⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))}
152139, 140, 150, 151braba 5546 . . . . . . . . . . 11 (𝑥{⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))} (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩⟩) ↔ ((𝑥𝑊 ∧ (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩⟩) ∈ 𝑊) ∧ (𝐻 Σg (𝑇𝑥)) = (𝐻 Σg (𝑇 ∘ (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩⟩)))))
15326, 42, 138, 152syl21anbrc 1343 . . . . . . . . . 10 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2o)) → 𝑥{⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))} (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩⟩))
154153ralrimivva 3199 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) → ∀𝑎𝐼𝑏 ∈ 2o 𝑥{⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))} (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩⟩))
155154ralrimivva 3199 . . . . . . . 8 (𝜑 → ∀𝑥𝑊𝑛 ∈ (0...(♯‘𝑥))∀𝑎𝐼𝑏 ∈ 2o 𝑥{⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))} (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩⟩))
1561fvexi 6920 . . . . . . . . . 10 𝑊 ∈ V
157 erex 8767 . . . . . . . . . 10 ({⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))} Er 𝑊 → (𝑊 ∈ V → {⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))} ∈ V))
15825, 156, 157mpisyl 21 . . . . . . . . 9 (𝜑 → {⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))} ∈ V)
159 ereq1 8750 . . . . . . . . . . 11 (𝑟 = {⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))} → (𝑟 Er 𝑊 ↔ {⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))} Er 𝑊))
160 breq 5149 . . . . . . . . . . . . 13 (𝑟 = {⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))} → (𝑥𝑟(𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩⟩) ↔ 𝑥{⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))} (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩⟩)))
1611602ralbidv 3218 . . . . . . . . . . . 12 (𝑟 = {⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))} → (∀𝑎𝐼𝑏 ∈ 2o 𝑥𝑟(𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩⟩) ↔ ∀𝑎𝐼𝑏 ∈ 2o 𝑥{⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))} (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩⟩)))
1621612ralbidv 3218 . . . . . . . . . . 11 (𝑟 = {⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))} → (∀𝑥𝑊𝑛 ∈ (0...(♯‘𝑥))∀𝑎𝐼𝑏 ∈ 2o 𝑥𝑟(𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩⟩) ↔ ∀𝑥𝑊𝑛 ∈ (0...(♯‘𝑥))∀𝑎𝐼𝑏 ∈ 2o 𝑥{⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))} (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩⟩)))
163159, 162anbi12d 632 . . . . . . . . . 10 (𝑟 = {⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))} → ((𝑟 Er 𝑊 ∧ ∀𝑥𝑊𝑛 ∈ (0...(♯‘𝑥))∀𝑎𝐼𝑏 ∈ 2o 𝑥𝑟(𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩⟩)) ↔ ({⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))} Er 𝑊 ∧ ∀𝑥𝑊𝑛 ∈ (0...(♯‘𝑥))∀𝑎𝐼𝑏 ∈ 2o 𝑥{⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))} (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩⟩))))
164163elabg 3676 . . . . . . . . 9 ({⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))} ∈ V → ({⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))} ∈ {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑥𝑊𝑛 ∈ (0...(♯‘𝑥))∀𝑎𝐼𝑏 ∈ 2o 𝑥𝑟(𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩⟩))} ↔ ({⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))} Er 𝑊 ∧ ∀𝑥𝑊𝑛 ∈ (0...(♯‘𝑥))∀𝑎𝐼𝑏 ∈ 2o 𝑥{⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))} (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩⟩))))
165158, 164syl 17 . . . . . . . 8 (𝜑 → ({⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))} ∈ {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑥𝑊𝑛 ∈ (0...(♯‘𝑥))∀𝑎𝐼𝑏 ∈ 2o 𝑥𝑟(𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩⟩))} ↔ ({⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))} Er 𝑊 ∧ ∀𝑥𝑊𝑛 ∈ (0...(♯‘𝑥))∀𝑎𝐼𝑏 ∈ 2o 𝑥{⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))} (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩⟩))))
16625, 155, 165mpbir2and 713 . . . . . . 7 (𝜑 → {⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))} ∈ {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑥𝑊𝑛 ∈ (0...(♯‘𝑥))∀𝑎𝐼𝑏 ∈ 2o 𝑥𝑟(𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩⟩))})
167 intss1 4967 . . . . . . 7 ({⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))} ∈ {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑥𝑊𝑛 ∈ (0...(♯‘𝑥))∀𝑎𝐼𝑏 ∈ 2o 𝑥𝑟(𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩⟩))} → {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑥𝑊𝑛 ∈ (0...(♯‘𝑥))∀𝑎𝐼𝑏 ∈ 2o 𝑥𝑟(𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩⟩))} ⊆ {⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))})
168166, 167syl 17 . . . . . 6 (𝜑 {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑥𝑊𝑛 ∈ (0...(♯‘𝑥))∀𝑎𝐼𝑏 ∈ 2o 𝑥𝑟(𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩⟩))} ⊆ {⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))})
1693, 168eqsstrid 4043 . . . . 5 (𝜑 ⊆ {⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))})
170169ssbrd 5190 . . . 4 (𝜑 → (𝐴 𝐶𝐴{⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))}𝐶))
171170imp 406 . . 3 ((𝜑𝐴 𝐶) → 𝐴{⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))}𝐶)
1721, 2efger 19750 . . . . . 6 Er 𝑊
173 errel 8752 . . . . . 6 ( Er 𝑊 → Rel )
174172, 173mp1i 13 . . . . 5 (𝜑 → Rel )
175 brrelex12 5740 . . . . 5 ((Rel 𝐴 𝐶) → (𝐴 ∈ V ∧ 𝐶 ∈ V))
176174, 175sylan 580 . . . 4 ((𝜑𝐴 𝐶) → (𝐴 ∈ V ∧ 𝐶 ∈ V))
177 preq12 4739 . . . . . . 7 ((𝑢 = 𝐴𝑣 = 𝐶) → {𝑢, 𝑣} = {𝐴, 𝐶})
178177sseq1d 4026 . . . . . 6 ((𝑢 = 𝐴𝑣 = 𝐶) → ({𝑢, 𝑣} ⊆ 𝑊 ↔ {𝐴, 𝐶} ⊆ 𝑊))
179 coeq2 5871 . . . . . . . 8 (𝑢 = 𝐴 → (𝑇𝑢) = (𝑇𝐴))
180179oveq2d 7446 . . . . . . 7 (𝑢 = 𝐴 → (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝐴)))
181 coeq2 5871 . . . . . . . 8 (𝑣 = 𝐶 → (𝑇𝑣) = (𝑇𝐶))
182181oveq2d 7446 . . . . . . 7 (𝑣 = 𝐶 → (𝐻 Σg (𝑇𝑣)) = (𝐻 Σg (𝑇𝐶)))
183180, 182eqeqan12d 2748 . . . . . 6 ((𝑢 = 𝐴𝑣 = 𝐶) → ((𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)) ↔ (𝐻 Σg (𝑇𝐴)) = (𝐻 Σg (𝑇𝐶))))
184178, 183anbi12d 632 . . . . 5 ((𝑢 = 𝐴𝑣 = 𝐶) → (({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣))) ↔ ({𝐴, 𝐶} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝐴)) = (𝐻 Σg (𝑇𝐶)))))
185184, 151brabga 5543 . . . 4 ((𝐴 ∈ V ∧ 𝐶 ∈ V) → (𝐴{⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))}𝐶 ↔ ({𝐴, 𝐶} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝐴)) = (𝐻 Σg (𝑇𝐶)))))
186176, 185syl 17 . . 3 ((𝜑𝐴 𝐶) → (𝐴{⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))}𝐶 ↔ ({𝐴, 𝐶} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝐴)) = (𝐻 Σg (𝑇𝐶)))))
187171, 186mpbid 232 . 2 ((𝜑𝐴 𝐶) → ({𝐴, 𝐶} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝐴)) = (𝐻 Σg (𝑇𝐶))))
188187simprd 495 1 ((𝜑𝐴 𝐶) → (𝐻 Σg (𝑇𝐴)) = (𝐻 Σg (𝑇𝐶)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395   = wceq 1536  wcel 2105  {cab 2711  wral 3058  Vcvv 3477  cdif 3959  cin 3961  wss 3962  c0 4338  ifcif 4530  {cpr 4632  cop 4636  cotp 4638   cint 4950   class class class wbr 5147  {copab 5209   I cid 5581   × cxp 5686  ccom 5692  Rel wrel 5693  wf 6558  cfv 6562  (class class class)co 7430  cmpo 7432  1oc1o 8497  2oc2o 8498   Er wer 8740  0cc0 11152  0cn0 12523  cuz 12875  ...cfz 13543  chash 14365  Word cword 14548   ++ cconcat 14604   substr csubstr 14674   prefix cpfx 14704   splice csplice 14783  ⟨“cs2 14876  Basecbs 17244  +gcplusg 17297  0gc0g 17485   Σg cgsu 17486  Mndcmnd 18759  Grpcgrp 18963  invgcminusg 18964   ~FG cefg 19738
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-rep 5284  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753  ax-cnex 11208  ax-resscn 11209  ax-1cn 11210  ax-icn 11211  ax-addcl 11212  ax-addrcl 11213  ax-mulcl 11214  ax-mulrcl 11215  ax-mulcom 11216  ax-addass 11217  ax-mulass 11218  ax-distr 11219  ax-i2m1 11220  ax-1ne0 11221  ax-1rid 11222  ax-rnegex 11223  ax-rrecex 11224  ax-cnre 11225  ax-pre-lttri 11226  ax-pre-lttrn 11227  ax-pre-ltadd 11228  ax-pre-mulgt0 11229
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-rmo 3377  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-ot 4639  df-uni 4912  df-int 4951  df-iun 4997  df-iin 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5582  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-we 5642  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-pred 6322  df-ord 6388  df-on 6389  df-lim 6390  df-suc 6391  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-riota 7387  df-ov 7433  df-oprab 7434  df-mpo 7435  df-om 7887  df-1st 8012  df-2nd 8013  df-frecs 8304  df-wrecs 8335  df-recs 8409  df-rdg 8448  df-1o 8504  df-2o 8505  df-er 8743  df-map 8866  df-en 8984  df-dom 8985  df-sdom 8986  df-fin 8987  df-card 9976  df-pnf 11294  df-mnf 11295  df-xr 11296  df-ltxr 11297  df-le 11298  df-sub 11491  df-neg 11492  df-nn 12264  df-2 12326  df-n0 12524  df-z 12611  df-uz 12876  df-fz 13544  df-fzo 13691  df-seq 14039  df-hash 14366  df-word 14549  df-concat 14605  df-s1 14630  df-substr 14675  df-pfx 14705  df-splice 14784  df-s2 14883  df-sets 17197  df-slot 17215  df-ndx 17227  df-base 17245  df-ress 17274  df-plusg 17310  df-0g 17487  df-gsum 17488  df-mgm 18665  df-sgrp 18744  df-mnd 18760  df-submnd 18809  df-grp 18966  df-minusg 18967  df-efg 19741
This theorem is referenced by:  frgpupf  19805
  Copyright terms: Public domain W3C validator