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

Theorem frgpuplem 19790
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 19735 . . . . . 6 = {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑥𝑊𝑛 ∈ (0...(♯‘𝑥))∀𝑎𝐼𝑏 ∈ 2o 𝑥𝑟(𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩⟩))}
4 coeq2 5869 . . . . . . . . . . . . 13 (𝑢 = 𝑣 → (𝑇𝑢) = (𝑇𝑣))
54oveq2d 7447 . . . . . . . . . . . 12 (𝑢 = 𝑣 → (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))
6 eqid 2737 . . . . . . . . . . . 12 {⟨𝑢, 𝑣⟩ ∣ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣))} = {⟨𝑢, 𝑣⟩ ∣ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣))}
75, 6eqer 8781 . . . . . . . . . . 11 {⟨𝑢, 𝑣⟩ ∣ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣))} Er V
87a1i 11 . . . . . . . . . 10 (𝜑 → {⟨𝑢, 𝑣⟩ ∣ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣))} Er V)
9 ssv 4008 . . . . . . . . . . 11 𝑊 ⊆ V
109a1i 11 . . . . . . . . . 10 (𝜑𝑊 ⊆ V)
118, 10erinxp 8831 . . . . . . . . 9 (𝜑 → ({⟨𝑢, 𝑣⟩ ∣ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣))} ∩ (𝑊 × 𝑊)) Er 𝑊)
12 df-xp 5691 . . . . . . . . . . . . 13 (𝑊 × 𝑊) = {⟨𝑢, 𝑣⟩ ∣ (𝑢𝑊𝑣𝑊)}
1312ineq1i 4216 . . . . . . . . . . . 12 ((𝑊 × 𝑊) ∩ {⟨𝑢, 𝑣⟩ ∣ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣))}) = ({⟨𝑢, 𝑣⟩ ∣ (𝑢𝑊𝑣𝑊)} ∩ {⟨𝑢, 𝑣⟩ ∣ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣))})
14 incom 4209 . . . . . . . . . . . 12 ((𝑊 × 𝑊) ∩ {⟨𝑢, 𝑣⟩ ∣ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣))}) = ({⟨𝑢, 𝑣⟩ ∣ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣))} ∩ (𝑊 × 𝑊))
15 inopab 5839 . . . . . . . . . . . 12 ({⟨𝑢, 𝑣⟩ ∣ (𝑢𝑊𝑣𝑊)} ∩ {⟨𝑢, 𝑣⟩ ∣ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣))}) = {⟨𝑢, 𝑣⟩ ∣ ((𝑢𝑊𝑣𝑊) ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))}
1613, 14, 153eqtr3i 2773 . . . . . . . . . . 11 ({⟨𝑢, 𝑣⟩ ∣ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣))} ∩ (𝑊 × 𝑊)) = {⟨𝑢, 𝑣⟩ ∣ ((𝑢𝑊𝑣𝑊) ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))}
17 vex 3484 . . . . . . . . . . . . . 14 𝑢 ∈ V
18 vex 3484 . . . . . . . . . . . . . 14 𝑣 ∈ V
1917, 18prss 4820 . . . . . . . . . . . . 13 ((𝑢𝑊𝑣𝑊) ↔ {𝑢, 𝑣} ⊆ 𝑊)
2019anbi1i 624 . . . . . . . . . . . 12 (((𝑢𝑊𝑣𝑊) ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣))) ↔ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣))))
2120opabbii 5210 . . . . . . . . . . 11 {⟨𝑢, 𝑣⟩ ∣ ((𝑢𝑊𝑣𝑊) ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))} = {⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))}
2216, 21eqtri 2765 . . . . . . . . . 10 ({⟨𝑢, 𝑣⟩ ∣ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣))} ∩ (𝑊 × 𝑊)) = {⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))}
23 ereq1 8752 . . . . . . . . . 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 6986 . . . . . . . . . . . . . . 15 ( I ‘Word (𝐼 × 2o)) ⊆ Word (𝐼 × 2o)
281, 27eqsstri 4030 . . . . . . . . . . . . . 14 𝑊 ⊆ Word (𝐼 × 2o)
2928, 26sselid 3981 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2o)) → 𝑥 ∈ Word (𝐼 × 2o))
30 opelxpi 5722 . . . . . . . . . . . . . . 15 ((𝑎𝐼𝑏 ∈ 2o) → ⟨𝑎, 𝑏⟩ ∈ (𝐼 × 2o))
3130adantl 481 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2o)) → ⟨𝑎, 𝑏⟩ ∈ (𝐼 × 2o))
32 simprl 771 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2o)) → 𝑎𝐼)
33 2oconcl 8541 . . . . . . . . . . . . . . . 16 (𝑏 ∈ 2o → (1o𝑏) ∈ 2o)
3433ad2antll 729 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2o)) → (1o𝑏) ∈ 2o)
3532, 34opelxpd 5724 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2o)) → ⟨𝑎, (1o𝑏)⟩ ∈ (𝐼 × 2o))
3631, 35s2cld 14910 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2o)) → ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩ ∈ Word (𝐼 × 2o))
37 splcl 14790 . . . . . . . . . . . . 13 ((𝑥 ∈ Word (𝐼 × 2o) ∧ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩ ∈ Word (𝐼 × 2o)) → (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩⟩) ∈ Word (𝐼 × 2o))
3829, 36, 37syl2anc 584 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2o)) → (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩⟩) ∈ Word (𝐼 × 2o))
391efgrcl 19733 . . . . . . . . . . . . . 14 (𝑥𝑊 → (𝐼 ∈ V ∧ 𝑊 = Word (𝐼 × 2o)))
4026, 39syl 17 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2o)) → (𝐼 ∈ V ∧ 𝑊 = Word (𝐼 × 2o)))
4140simprd 495 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2o)) → 𝑊 = Word (𝐼 × 2o))
4238, 41eleqtrrd 2844 . . . . . . . . . . 11 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2o)) → (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩⟩) ∈ 𝑊)
43 pfxcl 14715 . . . . . . . . . . . . . . . . . 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 19788 . . . . . . . . . . . . . . . . . 18 (𝜑𝑇:(𝐼 × 2o)⟶𝐵)
5251ad2antrr 726 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2o)) → 𝑇:(𝐼 × 2o)⟶𝐵)
53 ccatco 14874 . . . . . . . . . . . . . . . . 17 (((𝑥 prefix 𝑛) ∈ Word (𝐼 × 2o) ∧ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩ ∈ Word (𝐼 × 2o) ∧ 𝑇:(𝐼 × 2o)⟶𝐵) → (𝑇 ∘ ((𝑥 prefix 𝑛) ++ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩)) = ((𝑇 ∘ (𝑥 prefix 𝑛)) ++ (𝑇 ∘ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩)))
5444, 36, 52, 53syl3anc 1373 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2o)) → (𝑇 ∘ ((𝑥 prefix 𝑛) ++ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩)) = ((𝑇 ∘ (𝑥 prefix 𝑛)) ++ (𝑇 ∘ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩)))
5554oveq2d 7447 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2o)) → (𝐻 Σg (𝑇 ∘ ((𝑥 prefix 𝑛) ++ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩))) = (𝐻 Σg ((𝑇 ∘ (𝑥 prefix 𝑛)) ++ (𝑇 ∘ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩))))
5648ad2antrr 726 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2o)) → 𝐻 ∈ Grp)
5756grpmndd 18964 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2o)) → 𝐻 ∈ Mnd)
58 wrdco 14870 . . . . . . . . . . . . . . . . 17 (((𝑥 prefix 𝑛) ∈ Word (𝐼 × 2o) ∧ 𝑇:(𝐼 × 2o)⟶𝐵) → (𝑇 ∘ (𝑥 prefix 𝑛)) ∈ Word 𝐵)
5944, 52, 58syl2anc 584 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2o)) → (𝑇 ∘ (𝑥 prefix 𝑛)) ∈ Word 𝐵)
60 wrdco 14870 . . . . . . . . . . . . . . . . 17 ((⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩ ∈ Word (𝐼 × 2o) ∧ 𝑇:(𝐼 × 2o)⟶𝐵) → (𝑇 ∘ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩) ∈ Word 𝐵)
6136, 52, 60syl2anc 584 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2o)) → (𝑇 ∘ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩) ∈ Word 𝐵)
62 eqid 2737 . . . . . . . . . . . . . . . . 17 (+g𝐻) = (+g𝐻)
6345, 62gsumccat 18854 . . . . . . . . . . . . . . . 16 ((𝐻 ∈ Mnd ∧ (𝑇 ∘ (𝑥 prefix 𝑛)) ∈ Word 𝐵 ∧ (𝑇 ∘ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩) ∈ Word 𝐵) → (𝐻 Σg ((𝑇 ∘ (𝑥 prefix 𝑛)) ++ (𝑇 ∘ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩))) = ((𝐻 Σg (𝑇 ∘ (𝑥 prefix 𝑛)))(+g𝐻)(𝐻 Σg (𝑇 ∘ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩))))
6457, 59, 61, 63syl3anc 1373 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2o)) → (𝐻 Σg ((𝑇 ∘ (𝑥 prefix 𝑛)) ++ (𝑇 ∘ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩))) = ((𝐻 Σg (𝑇 ∘ (𝑥 prefix 𝑛)))(+g𝐻)(𝐻 Σg (𝑇 ∘ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩))))
6552, 31, 35s2co 14959 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2o)) → (𝑇 ∘ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩) = ⟨“(𝑇‘⟨𝑎, 𝑏⟩)(𝑇‘⟨𝑎, (1o𝑏)⟩)”⟩)
66 df-ov 7434 . . . . . . . . . . . . . . . . . . . . . 22 (𝑎𝑇𝑏) = (𝑇‘⟨𝑎, 𝑏⟩)
6766a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2o)) → (𝑎𝑇𝑏) = (𝑇‘⟨𝑎, 𝑏⟩))
6866fveq2i 6909 . . . . . . . . . . . . . . . . . . . . . 22 (𝑁‘(𝑎𝑇𝑏)) = (𝑁‘(𝑇‘⟨𝑎, 𝑏⟩))
69 df-ov 7434 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑎(𝑦𝐼, 𝑧 ∈ 2o ↦ ⟨𝑦, (1o𝑧)⟩)𝑏) = ((𝑦𝐼, 𝑧 ∈ 2o ↦ ⟨𝑦, (1o𝑧)⟩)‘⟨𝑎, 𝑏⟩)
70 eqid 2737 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑦𝐼, 𝑧 ∈ 2o ↦ ⟨𝑦, (1o𝑧)⟩) = (𝑦𝐼, 𝑧 ∈ 2o ↦ ⟨𝑦, (1o𝑧)⟩)
7170efgmval 19730 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑎𝐼𝑏 ∈ 2o) → (𝑎(𝑦𝐼, 𝑧 ∈ 2o ↦ ⟨𝑦, (1o𝑧)⟩)𝑏) = ⟨𝑎, (1o𝑏)⟩)
7269, 71eqtr3id 2791 . . . . . . . . . . . . . . . . . . . . . . . . 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 19789 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ ⟨𝑎, 𝑏⟩ ∈ (𝐼 × 2o)) → (𝑇‘((𝑦𝐼, 𝑧 ∈ 2o ↦ ⟨𝑦, (1o𝑧)⟩)‘⟨𝑎, 𝑏⟩)) = (𝑁‘(𝑇‘⟨𝑎, 𝑏⟩)))
7630, 75sylan2 593 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑎𝐼𝑏 ∈ 2o)) → (𝑇‘((𝑦𝐼, 𝑧 ∈ 2o ↦ ⟨𝑦, (1o𝑧)⟩)‘⟨𝑎, 𝑏⟩)) = (𝑁‘(𝑇‘⟨𝑎, 𝑏⟩)))
7776adantlr 715 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2o)) → (𝑇‘((𝑦𝐼, 𝑧 ∈ 2o ↦ ⟨𝑦, (1o𝑧)⟩)‘⟨𝑎, 𝑏⟩)) = (𝑁‘(𝑇‘⟨𝑎, 𝑏⟩)))
7874, 77eqtr3d 2779 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2o)) → (𝑇‘⟨𝑎, (1o𝑏)⟩) = (𝑁‘(𝑇‘⟨𝑎, 𝑏⟩)))
7968, 78eqtr4id 2796 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2o)) → (𝑁‘(𝑎𝑇𝑏)) = (𝑇‘⟨𝑎, (1o𝑏)⟩))
8067, 79s2eqd 14902 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2o)) → ⟨“(𝑎𝑇𝑏)(𝑁‘(𝑎𝑇𝑏))”⟩ = ⟨“(𝑇‘⟨𝑎, 𝑏⟩)(𝑇‘⟨𝑎, (1o𝑏)⟩)”⟩)
8165, 80eqtr4d 2780 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2o)) → (𝑇 ∘ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩) = ⟨“(𝑎𝑇𝑏)(𝑁‘(𝑎𝑇𝑏))”⟩)
8281oveq2d 7447 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2o)) → (𝐻 Σg (𝑇 ∘ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩)) = (𝐻 Σg ⟨“(𝑎𝑇𝑏)(𝑁‘(𝑎𝑇𝑏))”⟩))
83 simprr 773 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2o)) → 𝑏 ∈ 2o)
8452, 32, 83fovcdmd 7605 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2o)) → (𝑎𝑇𝑏) ∈ 𝐵)
8545, 46grpinvcl 19005 . . . . . . . . . . . . . . . . . . . 20 ((𝐻 ∈ Grp ∧ (𝑎𝑇𝑏) ∈ 𝐵) → (𝑁‘(𝑎𝑇𝑏)) ∈ 𝐵)
8656, 84, 85syl2anc 584 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2o)) → (𝑁‘(𝑎𝑇𝑏)) ∈ 𝐵)
8745, 62gsumws2 18855 . . . . . . . . . . . . . . . . . . 19 ((𝐻 ∈ Mnd ∧ (𝑎𝑇𝑏) ∈ 𝐵 ∧ (𝑁‘(𝑎𝑇𝑏)) ∈ 𝐵) → (𝐻 Σg ⟨“(𝑎𝑇𝑏)(𝑁‘(𝑎𝑇𝑏))”⟩) = ((𝑎𝑇𝑏)(+g𝐻)(𝑁‘(𝑎𝑇𝑏))))
8857, 84, 86, 87syl3anc 1373 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2o)) → (𝐻 Σg ⟨“(𝑎𝑇𝑏)(𝑁‘(𝑎𝑇𝑏))”⟩) = ((𝑎𝑇𝑏)(+g𝐻)(𝑁‘(𝑎𝑇𝑏))))
89 eqid 2737 . . . . . . . . . . . . . . . . . . . 20 (0g𝐻) = (0g𝐻)
9045, 62, 89, 46grprinv 19008 . . . . . . . . . . . . . . . . . . 19 ((𝐻 ∈ Grp ∧ (𝑎𝑇𝑏) ∈ 𝐵) → ((𝑎𝑇𝑏)(+g𝐻)(𝑁‘(𝑎𝑇𝑏))) = (0g𝐻))
9156, 84, 90syl2anc 584 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2o)) → ((𝑎𝑇𝑏)(+g𝐻)(𝑁‘(𝑎𝑇𝑏))) = (0g𝐻))
9282, 88, 913eqtrd 2781 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2o)) → (𝐻 Σg (𝑇 ∘ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩)) = (0g𝐻))
9392oveq2d 7447 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2o)) → ((𝐻 Σg (𝑇 ∘ (𝑥 prefix 𝑛)))(+g𝐻)(𝐻 Σg (𝑇 ∘ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩))) = ((𝐻 Σg (𝑇 ∘ (𝑥 prefix 𝑛)))(+g𝐻)(0g𝐻)))
9445gsumwcl 18852 . . . . . . . . . . . . . . . . . 18 ((𝐻 ∈ Mnd ∧ (𝑇 ∘ (𝑥 prefix 𝑛)) ∈ Word 𝐵) → (𝐻 Σg (𝑇 ∘ (𝑥 prefix 𝑛))) ∈ 𝐵)
9557, 59, 94syl2anc 584 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2o)) → (𝐻 Σg (𝑇 ∘ (𝑥 prefix 𝑛))) ∈ 𝐵)
9645, 62, 89grprid 18986 . . . . . . . . . . . . . . . . 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 2777 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2o)) → ((𝐻 Σg (𝑇 ∘ (𝑥 prefix 𝑛)))(+g𝐻)(𝐻 Σg (𝑇 ∘ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩))) = (𝐻 Σg (𝑇 ∘ (𝑥 prefix 𝑛))))
9955, 64, 983eqtrrd 2782 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2o)) → (𝐻 Σg (𝑇 ∘ (𝑥 prefix 𝑛))) = (𝐻 Σg (𝑇 ∘ ((𝑥 prefix 𝑛) ++ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩))))
10099oveq1d 7446 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2o)) → ((𝐻 Σg (𝑇 ∘ (𝑥 prefix 𝑛)))(+g𝐻)(𝐻 Σg (𝑇 ∘ (𝑥 substr ⟨𝑛, (♯‘𝑥)⟩)))) = ((𝐻 Σg (𝑇 ∘ ((𝑥 prefix 𝑛) ++ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩)))(+g𝐻)(𝐻 Σg (𝑇 ∘ (𝑥 substr ⟨𝑛, (♯‘𝑥)⟩)))))
101 swrdcl 14683 . . . . . . . . . . . . . . . 16 (𝑥 ∈ Word (𝐼 × 2o) → (𝑥 substr ⟨𝑛, (♯‘𝑥)⟩) ∈ Word (𝐼 × 2o))
10229, 101syl 17 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2o)) → (𝑥 substr ⟨𝑛, (♯‘𝑥)⟩) ∈ Word (𝐼 × 2o))
103 wrdco 14870 . . . . . . . . . . . . . . 15 (((𝑥 substr ⟨𝑛, (♯‘𝑥)⟩) ∈ Word (𝐼 × 2o) ∧ 𝑇:(𝐼 × 2o)⟶𝐵) → (𝑇 ∘ (𝑥 substr ⟨𝑛, (♯‘𝑥)⟩)) ∈ Word 𝐵)
104102, 52, 103syl2anc 584 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2o)) → (𝑇 ∘ (𝑥 substr ⟨𝑛, (♯‘𝑥)⟩)) ∈ Word 𝐵)
10545, 62gsumccat 18854 . . . . . . . . . . . . . 14 ((𝐻 ∈ Mnd ∧ (𝑇 ∘ (𝑥 prefix 𝑛)) ∈ Word 𝐵 ∧ (𝑇 ∘ (𝑥 substr ⟨𝑛, (♯‘𝑥)⟩)) ∈ Word 𝐵) → (𝐻 Σg ((𝑇 ∘ (𝑥 prefix 𝑛)) ++ (𝑇 ∘ (𝑥 substr ⟨𝑛, (♯‘𝑥)⟩)))) = ((𝐻 Σg (𝑇 ∘ (𝑥 prefix 𝑛)))(+g𝐻)(𝐻 Σg (𝑇 ∘ (𝑥 substr ⟨𝑛, (♯‘𝑥)⟩)))))
10657, 59, 104, 105syl3anc 1373 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2o)) → (𝐻 Σg ((𝑇 ∘ (𝑥 prefix 𝑛)) ++ (𝑇 ∘ (𝑥 substr ⟨𝑛, (♯‘𝑥)⟩)))) = ((𝐻 Σg (𝑇 ∘ (𝑥 prefix 𝑛)))(+g𝐻)(𝐻 Σg (𝑇 ∘ (𝑥 substr ⟨𝑛, (♯‘𝑥)⟩)))))
107 ccatcl 14612 . . . . . . . . . . . . . . . 16 (((𝑥 prefix 𝑛) ∈ Word (𝐼 × 2o) ∧ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩ ∈ Word (𝐼 × 2o)) → ((𝑥 prefix 𝑛) ++ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩) ∈ Word (𝐼 × 2o))
10844, 36, 107syl2anc 584 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2o)) → ((𝑥 prefix 𝑛) ++ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩) ∈ Word (𝐼 × 2o))
109 wrdco 14870 . . . . . . . . . . . . . . 15 ((((𝑥 prefix 𝑛) ++ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩) ∈ Word (𝐼 × 2o) ∧ 𝑇:(𝐼 × 2o)⟶𝐵) → (𝑇 ∘ ((𝑥 prefix 𝑛) ++ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩)) ∈ Word 𝐵)
110108, 52, 109syl2anc 584 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2o)) → (𝑇 ∘ ((𝑥 prefix 𝑛) ++ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩)) ∈ Word 𝐵)
11145, 62gsumccat 18854 . . . . . . . . . . . . . 14 ((𝐻 ∈ Mnd ∧ (𝑇 ∘ ((𝑥 prefix 𝑛) ++ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩)) ∈ Word 𝐵 ∧ (𝑇 ∘ (𝑥 substr ⟨𝑛, (♯‘𝑥)⟩)) ∈ Word 𝐵) → (𝐻 Σg ((𝑇 ∘ ((𝑥 prefix 𝑛) ++ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩)) ++ (𝑇 ∘ (𝑥 substr ⟨𝑛, (♯‘𝑥)⟩)))) = ((𝐻 Σg (𝑇 ∘ ((𝑥 prefix 𝑛) ++ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩)))(+g𝐻)(𝐻 Σg (𝑇 ∘ (𝑥 substr ⟨𝑛, (♯‘𝑥)⟩)))))
11257, 110, 104, 111syl3anc 1373 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2o)) → (𝐻 Σg ((𝑇 ∘ ((𝑥 prefix 𝑛) ++ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩)) ++ (𝑇 ∘ (𝑥 substr ⟨𝑛, (♯‘𝑥)⟩)))) = ((𝐻 Σg (𝑇 ∘ ((𝑥 prefix 𝑛) ++ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩)))(+g𝐻)(𝐻 Σg (𝑇 ∘ (𝑥 substr ⟨𝑛, (♯‘𝑥)⟩)))))
113100, 106, 1123eqtr4d 2787 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2o)) → (𝐻 Σg ((𝑇 ∘ (𝑥 prefix 𝑛)) ++ (𝑇 ∘ (𝑥 substr ⟨𝑛, (♯‘𝑥)⟩)))) = (𝐻 Σg ((𝑇 ∘ ((𝑥 prefix 𝑛) ++ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩)) ++ (𝑇 ∘ (𝑥 substr ⟨𝑛, (♯‘𝑥)⟩)))))
114 simplrr 778 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2o)) → 𝑛 ∈ (0...(♯‘𝑥)))
115 lencl 14571 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ Word (𝐼 × 2o) → (♯‘𝑥) ∈ ℕ0)
11629, 115syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2o)) → (♯‘𝑥) ∈ ℕ0)
117 nn0uz 12920 . . . . . . . . . . . . . . . . . . 19 0 = (ℤ‘0)
118116, 117eleqtrdi 2851 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2o)) → (♯‘𝑥) ∈ (ℤ‘0))
119 eluzfz2 13572 . . . . . . . . . . . . . . . . . 18 ((♯‘𝑥) ∈ (ℤ‘0) → (♯‘𝑥) ∈ (0...(♯‘𝑥)))
120118, 119syl 17 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2o)) → (♯‘𝑥) ∈ (0...(♯‘𝑥)))
121 ccatpfx 14739 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ Word (𝐼 × 2o) ∧ 𝑛 ∈ (0...(♯‘𝑥)) ∧ (♯‘𝑥) ∈ (0...(♯‘𝑥))) → ((𝑥 prefix 𝑛) ++ (𝑥 substr ⟨𝑛, (♯‘𝑥)⟩)) = (𝑥 prefix (♯‘𝑥)))
12229, 114, 120, 121syl3anc 1373 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2o)) → ((𝑥 prefix 𝑛) ++ (𝑥 substr ⟨𝑛, (♯‘𝑥)⟩)) = (𝑥 prefix (♯‘𝑥)))
123 pfxid 14722 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ Word (𝐼 × 2o) → (𝑥 prefix (♯‘𝑥)) = 𝑥)
12429, 123syl 17 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2o)) → (𝑥 prefix (♯‘𝑥)) = 𝑥)
125122, 124eqtrd 2777 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2o)) → ((𝑥 prefix 𝑛) ++ (𝑥 substr ⟨𝑛, (♯‘𝑥)⟩)) = 𝑥)
126125coeq2d 5873 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2o)) → (𝑇 ∘ ((𝑥 prefix 𝑛) ++ (𝑥 substr ⟨𝑛, (♯‘𝑥)⟩))) = (𝑇𝑥))
127 ccatco 14874 . . . . . . . . . . . . . . 15 (((𝑥 prefix 𝑛) ∈ Word (𝐼 × 2o) ∧ (𝑥 substr ⟨𝑛, (♯‘𝑥)⟩) ∈ Word (𝐼 × 2o) ∧ 𝑇:(𝐼 × 2o)⟶𝐵) → (𝑇 ∘ ((𝑥 prefix 𝑛) ++ (𝑥 substr ⟨𝑛, (♯‘𝑥)⟩))) = ((𝑇 ∘ (𝑥 prefix 𝑛)) ++ (𝑇 ∘ (𝑥 substr ⟨𝑛, (♯‘𝑥)⟩))))
12844, 102, 52, 127syl3anc 1373 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2o)) → (𝑇 ∘ ((𝑥 prefix 𝑛) ++ (𝑥 substr ⟨𝑛, (♯‘𝑥)⟩))) = ((𝑇 ∘ (𝑥 prefix 𝑛)) ++ (𝑇 ∘ (𝑥 substr ⟨𝑛, (♯‘𝑥)⟩))))
129126, 128eqtr3d 2779 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2o)) → (𝑇𝑥) = ((𝑇 ∘ (𝑥 prefix 𝑛)) ++ (𝑇 ∘ (𝑥 substr ⟨𝑛, (♯‘𝑥)⟩))))
130129oveq2d 7447 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2o)) → (𝐻 Σg (𝑇𝑥)) = (𝐻 Σg ((𝑇 ∘ (𝑥 prefix 𝑛)) ++ (𝑇 ∘ (𝑥 substr ⟨𝑛, (♯‘𝑥)⟩)))))
131 splval 14789 . . . . . . . . . . . . . . . 16 ((𝑥𝑊 ∧ (𝑛 ∈ (0...(♯‘𝑥)) ∧ 𝑛 ∈ (0...(♯‘𝑥)) ∧ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩ ∈ Word (𝐼 × 2o))) → (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩⟩) = (((𝑥 prefix 𝑛) ++ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩) ++ (𝑥 substr ⟨𝑛, (♯‘𝑥)⟩)))
13226, 114, 114, 36, 131syl13anc 1374 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2o)) → (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩⟩) = (((𝑥 prefix 𝑛) ++ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩) ++ (𝑥 substr ⟨𝑛, (♯‘𝑥)⟩)))
133132coeq2d 5873 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2o)) → (𝑇 ∘ (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩⟩)) = (𝑇 ∘ (((𝑥 prefix 𝑛) ++ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩) ++ (𝑥 substr ⟨𝑛, (♯‘𝑥)⟩))))
134 ccatco 14874 . . . . . . . . . . . . . . 15 ((((𝑥 prefix 𝑛) ++ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩) ∈ Word (𝐼 × 2o) ∧ (𝑥 substr ⟨𝑛, (♯‘𝑥)⟩) ∈ Word (𝐼 × 2o) ∧ 𝑇:(𝐼 × 2o)⟶𝐵) → (𝑇 ∘ (((𝑥 prefix 𝑛) ++ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩) ++ (𝑥 substr ⟨𝑛, (♯‘𝑥)⟩))) = ((𝑇 ∘ ((𝑥 prefix 𝑛) ++ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩)) ++ (𝑇 ∘ (𝑥 substr ⟨𝑛, (♯‘𝑥)⟩))))
135108, 102, 52, 134syl3anc 1373 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2o)) → (𝑇 ∘ (((𝑥 prefix 𝑛) ++ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩) ++ (𝑥 substr ⟨𝑛, (♯‘𝑥)⟩))) = ((𝑇 ∘ ((𝑥 prefix 𝑛) ++ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩)) ++ (𝑇 ∘ (𝑥 substr ⟨𝑛, (♯‘𝑥)⟩))))
136133, 135eqtrd 2777 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2o)) → (𝑇 ∘ (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩⟩)) = ((𝑇 ∘ ((𝑥 prefix 𝑛) ++ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩)) ++ (𝑇 ∘ (𝑥 substr ⟨𝑛, (♯‘𝑥)⟩))))
137136oveq2d 7447 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2o)) → (𝐻 Σg (𝑇 ∘ (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩⟩))) = (𝐻 Σg ((𝑇 ∘ ((𝑥 prefix 𝑛) ++ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩)) ++ (𝑇 ∘ (𝑥 substr ⟨𝑛, (♯‘𝑥)⟩)))))
138113, 130, 1373eqtr4d 2787 . . . . . . . . . . 11 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2o)) → (𝐻 Σg (𝑇𝑥)) = (𝐻 Σg (𝑇 ∘ (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩⟩))))
139 vex 3484 . . . . . . . . . . . 12 𝑥 ∈ V
140 ovex 7464 . . . . . . . . . . . 12 (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩⟩) ∈ V
141 eleq1 2829 . . . . . . . . . . . . . . 15 (𝑢 = 𝑥 → (𝑢𝑊𝑥𝑊))
142 eleq1 2829 . . . . . . . . . . . . . . 15 (𝑣 = (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩⟩) → (𝑣𝑊 ↔ (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩⟩) ∈ 𝑊))
143141, 142bi2anan9 638 . . . . . . . . . . . . . 14 ((𝑢 = 𝑥𝑣 = (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩⟩)) → ((𝑢𝑊𝑣𝑊) ↔ (𝑥𝑊 ∧ (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩⟩) ∈ 𝑊)))
14419, 143bitr3id 285 . . . . . . . . . . . . 13 ((𝑢 = 𝑥𝑣 = (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩⟩)) → ({𝑢, 𝑣} ⊆ 𝑊 ↔ (𝑥𝑊 ∧ (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩⟩) ∈ 𝑊)))
145 coeq2 5869 . . . . . . . . . . . . . . 15 (𝑢 = 𝑥 → (𝑇𝑢) = (𝑇𝑥))
146145oveq2d 7447 . . . . . . . . . . . . . 14 (𝑢 = 𝑥 → (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑥)))
147 coeq2 5869 . . . . . . . . . . . . . . 15 (𝑣 = (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩⟩) → (𝑇𝑣) = (𝑇 ∘ (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩⟩)))
148147oveq2d 7447 . . . . . . . . . . . . . 14 (𝑣 = (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩⟩) → (𝐻 Σg (𝑇𝑣)) = (𝐻 Σg (𝑇 ∘ (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩⟩))))
149146, 148eqeqan12d 2751 . . . . . . . . . . . . 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 2737 . . . . . . . . . . . 12 {⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))} = {⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))}
152139, 140, 150, 151braba 5542 . . . . . . . . . . 11 (𝑥{⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))} (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩⟩) ↔ ((𝑥𝑊 ∧ (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩⟩) ∈ 𝑊) ∧ (𝐻 Σg (𝑇𝑥)) = (𝐻 Σg (𝑇 ∘ (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩⟩)))))
15326, 42, 138, 152syl21anbrc 1345 . . . . . . . . . 10 (((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) ∧ (𝑎𝐼𝑏 ∈ 2o)) → 𝑥{⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))} (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩⟩))
154153ralrimivva 3202 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝑊𝑛 ∈ (0...(♯‘𝑥)))) → ∀𝑎𝐼𝑏 ∈ 2o 𝑥{⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))} (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩⟩))
155154ralrimivva 3202 . . . . . . . 8 (𝜑 → ∀𝑥𝑊𝑛 ∈ (0...(♯‘𝑥))∀𝑎𝐼𝑏 ∈ 2o 𝑥{⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))} (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩⟩))
1561fvexi 6920 . . . . . . . . . 10 𝑊 ∈ V
157 erex 8769 . . . . . . . . . 10 ({⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))} Er 𝑊 → (𝑊 ∈ V → {⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))} ∈ V))
15825, 156, 157mpisyl 21 . . . . . . . . 9 (𝜑 → {⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))} ∈ V)
159 ereq1 8752 . . . . . . . . . . 11 (𝑟 = {⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))} → (𝑟 Er 𝑊 ↔ {⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))} Er 𝑊))
160 breq 5145 . . . . . . . . . . . . 13 (𝑟 = {⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))} → (𝑥𝑟(𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩⟩) ↔ 𝑥{⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))} (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩⟩)))
1611602ralbidv 3221 . . . . . . . . . . . 12 (𝑟 = {⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))} → (∀𝑎𝐼𝑏 ∈ 2o 𝑥𝑟(𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩⟩) ↔ ∀𝑎𝐼𝑏 ∈ 2o 𝑥{⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))} (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1o𝑏)⟩”⟩⟩)))
1621612ralbidv 3221 . . . . . . . . . . 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 4963 . . . . . . 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 4022 . . . . 5 (𝜑 ⊆ {⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))})
170169ssbrd 5186 . . . 4 (𝜑 → (𝐴 𝐶𝐴{⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))}𝐶))
171170imp 406 . . 3 ((𝜑𝐴 𝐶) → 𝐴{⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)))}𝐶)
1721, 2efger 19736 . . . . . 6 Er 𝑊
173 errel 8754 . . . . . 6 ( Er 𝑊 → Rel )
174172, 173mp1i 13 . . . . 5 (𝜑 → Rel )
175 brrelex12 5737 . . . . 5 ((Rel 𝐴 𝐶) → (𝐴 ∈ V ∧ 𝐶 ∈ V))
176174, 175sylan 580 . . . 4 ((𝜑𝐴 𝐶) → (𝐴 ∈ V ∧ 𝐶 ∈ V))
177 preq12 4735 . . . . . . 7 ((𝑢 = 𝐴𝑣 = 𝐶) → {𝑢, 𝑣} = {𝐴, 𝐶})
178177sseq1d 4015 . . . . . 6 ((𝑢 = 𝐴𝑣 = 𝐶) → ({𝑢, 𝑣} ⊆ 𝑊 ↔ {𝐴, 𝐶} ⊆ 𝑊))
179 coeq2 5869 . . . . . . . 8 (𝑢 = 𝐴 → (𝑇𝑢) = (𝑇𝐴))
180179oveq2d 7447 . . . . . . 7 (𝑢 = 𝐴 → (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝐴)))
181 coeq2 5869 . . . . . . . 8 (𝑣 = 𝐶 → (𝑇𝑣) = (𝑇𝐶))
182181oveq2d 7447 . . . . . . 7 (𝑣 = 𝐶 → (𝐻 Σg (𝑇𝑣)) = (𝐻 Σg (𝑇𝐶)))
183180, 182eqeqan12d 2751 . . . . . 6 ((𝑢 = 𝐴𝑣 = 𝐶) → ((𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣)) ↔ (𝐻 Σg (𝑇𝐴)) = (𝐻 Σg (𝑇𝐶))))
184178, 183anbi12d 632 . . . . 5 ((𝑢 = 𝐴𝑣 = 𝐶) → (({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝑢)) = (𝐻 Σg (𝑇𝑣))) ↔ ({𝐴, 𝐶} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇𝐴)) = (𝐻 Σg (𝑇𝐶)))))
185184, 151brabga 5539 . . . 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 1540  wcel 2108  {cab 2714  wral 3061  Vcvv 3480  cdif 3948  cin 3950  wss 3951  c0 4333  ifcif 4525  {cpr 4628  cop 4632  cotp 4634   cint 4946   class class class wbr 5143  {copab 5205   I cid 5577   × cxp 5683  ccom 5689  Rel wrel 5690  wf 6557  cfv 6561  (class class class)co 7431  cmpo 7433  1oc1o 8499  2oc2o 8500   Er wer 8742  0cc0 11155  0cn0 12526  cuz 12878  ...cfz 13547  chash 14369  Word cword 14552   ++ cconcat 14608   substr csubstr 14678   prefix cpfx 14708   splice csplice 14787  ⟨“cs2 14880  Basecbs 17247  +gcplusg 17297  0gc0g 17484   Σg cgsu 17485  Mndcmnd 18747  Grpcgrp 18951  invgcminusg 18952   ~FG cefg 19724
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-cnex 11211  ax-resscn 11212  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-addrcl 11216  ax-mulcl 11217  ax-mulrcl 11218  ax-mulcom 11219  ax-addass 11220  ax-mulass 11221  ax-distr 11222  ax-i2m1 11223  ax-1ne0 11224  ax-1rid 11225  ax-rnegex 11226  ax-rrecex 11227  ax-cnre 11228  ax-pre-lttri 11229  ax-pre-lttrn 11230  ax-pre-ltadd 11231  ax-pre-mulgt0 11232
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3380  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-ot 4635  df-uni 4908  df-int 4947  df-iun 4993  df-iin 4994  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-om 7888  df-1st 8014  df-2nd 8015  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-1o 8506  df-2o 8507  df-er 8745  df-map 8868  df-en 8986  df-dom 8987  df-sdom 8988  df-fin 8989  df-card 9979  df-pnf 11297  df-mnf 11298  df-xr 11299  df-ltxr 11300  df-le 11301  df-sub 11494  df-neg 11495  df-nn 12267  df-2 12329  df-n0 12527  df-z 12614  df-uz 12879  df-fz 13548  df-fzo 13695  df-seq 14043  df-hash 14370  df-word 14553  df-concat 14609  df-s1 14634  df-substr 14679  df-pfx 14709  df-splice 14788  df-s2 14887  df-sets 17201  df-slot 17219  df-ndx 17231  df-base 17248  df-ress 17275  df-plusg 17310  df-0g 17486  df-gsum 17487  df-mgm 18653  df-sgrp 18732  df-mnd 18748  df-submnd 18797  df-grp 18954  df-minusg 18955  df-efg 19727
This theorem is referenced by:  frgpupf  19791
  Copyright terms: Public domain W3C validator