This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem frgpuplem

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)

Ref Expression
Hypotheses 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 frgpuplem ( ( 𝜑 ∧ 𝐴 ∼ 𝐶 ) → ( 𝐻 Σg ( 𝑇 ∘ 𝐴 ) ) = ( 𝐻 Σg ( 𝑇 ∘ 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 frgpup.b ⊢ 𝐵 = ( Base ‘ 𝐻 )
2 frgpup.n ⊢ 𝑁 = ( invg ‘ 𝐻 )
3 frgpup.t ⊢ 𝑇 = ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2o ↦ if ( 𝑧 = ∅ , ( 𝐹 ‘ 𝑦 ) , ( 𝑁 ‘ ( 𝐹 ‘ 𝑦 ) ) ) )
4 frgpup.h ⊢ ( 𝜑 → 𝐻 ∈ Grp )
5 frgpup.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
6 frgpup.a ⊢ ( 𝜑 → 𝐹 : 𝐼 ⟶ 𝐵 )
7 frgpup.w ⊢ 𝑊 = ( I ‘ Word ( 𝐼 × 2o ) )
8 frgpup.r ⊢ ∼ = ( ~FG ‘ 𝐼 )
9 7 8 efgval ⊢ ∼ = ∩ { 𝑟 ∣ ( 𝑟 Er 𝑊 ∧ ∀ 𝑥 ∈ 𝑊 ∀ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ∀ 𝑎 ∈ 𝐼 ∀ 𝑏 ∈ 2o 𝑥 𝑟 ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1o ∖ 𝑏 ) ⟩ ”⟩ ⟩ ) ) }
10 coeq2 ⊢ ( 𝑢 = 𝑣 → ( 𝑇 ∘ 𝑢 ) = ( 𝑇 ∘ 𝑣 ) )
11 10 oveq2d ⊢ ( 𝑢 = 𝑣 → ( 𝐻 Σg ( 𝑇 ∘ 𝑢 ) ) = ( 𝐻 Σg ( 𝑇 ∘ 𝑣 ) ) )
12 eqid ⊢ { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( 𝐻 Σg ( 𝑇 ∘ 𝑢 ) ) = ( 𝐻 Σg ( 𝑇 ∘ 𝑣 ) ) } = { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( 𝐻 Σg ( 𝑇 ∘ 𝑢 ) ) = ( 𝐻 Σg ( 𝑇 ∘ 𝑣 ) ) }
13 11 12 eqer ⊢ { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( 𝐻 Σg ( 𝑇 ∘ 𝑢 ) ) = ( 𝐻 Σg ( 𝑇 ∘ 𝑣 ) ) } Er V
14 13 a1i ⊢ ( 𝜑 → { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( 𝐻 Σg ( 𝑇 ∘ 𝑢 ) ) = ( 𝐻 Σg ( 𝑇 ∘ 𝑣 ) ) } Er V )
15 ssv ⊢ 𝑊 ⊆ V
16 15 a1i ⊢ ( 𝜑 → 𝑊 ⊆ V )
17 14 16 erinxp ⊢ ( 𝜑 → ( { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( 𝐻 Σg ( 𝑇 ∘ 𝑢 ) ) = ( 𝐻 Σg ( 𝑇 ∘ 𝑣 ) ) } ∩ ( 𝑊 × 𝑊 ) ) Er 𝑊 )
18 df-xp ⊢ ( 𝑊 × 𝑊 ) = { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( 𝑢 ∈ 𝑊 ∧ 𝑣 ∈ 𝑊 ) }
19 18 ineq1i ⊢ ( ( 𝑊 × 𝑊 ) ∩ { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( 𝐻 Σg ( 𝑇 ∘ 𝑢 ) ) = ( 𝐻 Σg ( 𝑇 ∘ 𝑣 ) ) } ) = ( { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( 𝑢 ∈ 𝑊 ∧ 𝑣 ∈ 𝑊 ) } ∩ { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( 𝐻 Σg ( 𝑇 ∘ 𝑢 ) ) = ( 𝐻 Σg ( 𝑇 ∘ 𝑣 ) ) } )
20 incom ⊢ ( ( 𝑊 × 𝑊 ) ∩ { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( 𝐻 Σg ( 𝑇 ∘ 𝑢 ) ) = ( 𝐻 Σg ( 𝑇 ∘ 𝑣 ) ) } ) = ( { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( 𝐻 Σg ( 𝑇 ∘ 𝑢 ) ) = ( 𝐻 Σg ( 𝑇 ∘ 𝑣 ) ) } ∩ ( 𝑊 × 𝑊 ) )
21 inopab ⊢ ( { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( 𝑢 ∈ 𝑊 ∧ 𝑣 ∈ 𝑊 ) } ∩ { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( 𝐻 Σg ( 𝑇 ∘ 𝑢 ) ) = ( 𝐻 Σg ( 𝑇 ∘ 𝑣 ) ) } ) = { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( ( 𝑢 ∈ 𝑊 ∧ 𝑣 ∈ 𝑊 ) ∧ ( 𝐻 Σg ( 𝑇 ∘ 𝑢 ) ) = ( 𝐻 Σg ( 𝑇 ∘ 𝑣 ) ) ) }
22 19 20 21 3eqtr3i ⊢ ( { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( 𝐻 Σg ( 𝑇 ∘ 𝑢 ) ) = ( 𝐻 Σg ( 𝑇 ∘ 𝑣 ) ) } ∩ ( 𝑊 × 𝑊 ) ) = { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( ( 𝑢 ∈ 𝑊 ∧ 𝑣 ∈ 𝑊 ) ∧ ( 𝐻 Σg ( 𝑇 ∘ 𝑢 ) ) = ( 𝐻 Σg ( 𝑇 ∘ 𝑣 ) ) ) }
23 vex ⊢ 𝑢 ∈ V
24 vex ⊢ 𝑣 ∈ V
25 23 24 prss ⊢ ( ( 𝑢 ∈ 𝑊 ∧ 𝑣 ∈ 𝑊 ) ↔ { 𝑢 , 𝑣 } ⊆ 𝑊 )
26 25 anbi1i ⊢ ( ( ( 𝑢 ∈ 𝑊 ∧ 𝑣 ∈ 𝑊 ) ∧ ( 𝐻 Σg ( 𝑇 ∘ 𝑢 ) ) = ( 𝐻 Σg ( 𝑇 ∘ 𝑣 ) ) ) ↔ ( { 𝑢 , 𝑣 } ⊆ 𝑊 ∧ ( 𝐻 Σg ( 𝑇 ∘ 𝑢 ) ) = ( 𝐻 Σg ( 𝑇 ∘ 𝑣 ) ) ) )
27 26 opabbii ⊢ { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( ( 𝑢 ∈ 𝑊 ∧ 𝑣 ∈ 𝑊 ) ∧ ( 𝐻 Σg ( 𝑇 ∘ 𝑢 ) ) = ( 𝐻 Σg ( 𝑇 ∘ 𝑣 ) ) ) } = { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( { 𝑢 , 𝑣 } ⊆ 𝑊 ∧ ( 𝐻 Σg ( 𝑇 ∘ 𝑢 ) ) = ( 𝐻 Σg ( 𝑇 ∘ 𝑣 ) ) ) }
28 22 27 eqtri ⊢ ( { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( 𝐻 Σg ( 𝑇 ∘ 𝑢 ) ) = ( 𝐻 Σg ( 𝑇 ∘ 𝑣 ) ) } ∩ ( 𝑊 × 𝑊 ) ) = { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( { 𝑢 , 𝑣 } ⊆ 𝑊 ∧ ( 𝐻 Σg ( 𝑇 ∘ 𝑢 ) ) = ( 𝐻 Σg ( 𝑇 ∘ 𝑣 ) ) ) }
29 ereq1 ⊢ ( ( { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( 𝐻 Σg ( 𝑇 ∘ 𝑢 ) ) = ( 𝐻 Σg ( 𝑇 ∘ 𝑣 ) ) } ∩ ( 𝑊 × 𝑊 ) ) = { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( { 𝑢 , 𝑣 } ⊆ 𝑊 ∧ ( 𝐻 Σg ( 𝑇 ∘ 𝑢 ) ) = ( 𝐻 Σg ( 𝑇 ∘ 𝑣 ) ) ) } → ( ( { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( 𝐻 Σg ( 𝑇 ∘ 𝑢 ) ) = ( 𝐻 Σg ( 𝑇 ∘ 𝑣 ) ) } ∩ ( 𝑊 × 𝑊 ) ) Er 𝑊 ↔ { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( { 𝑢 , 𝑣 } ⊆ 𝑊 ∧ ( 𝐻 Σg ( 𝑇 ∘ 𝑢 ) ) = ( 𝐻 Σg ( 𝑇 ∘ 𝑣 ) ) ) } Er 𝑊 ) )
30 28 29 ax-mp ⊢ ( ( { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( 𝐻 Σg ( 𝑇 ∘ 𝑢 ) ) = ( 𝐻 Σg ( 𝑇 ∘ 𝑣 ) ) } ∩ ( 𝑊 × 𝑊 ) ) Er 𝑊 ↔ { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( { 𝑢 , 𝑣 } ⊆ 𝑊 ∧ ( 𝐻 Σg ( 𝑇 ∘ 𝑢 ) ) = ( 𝐻 Σg ( 𝑇 ∘ 𝑣 ) ) ) } Er 𝑊 )
31 17 30 sylib ⊢ ( 𝜑 → { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( { 𝑢 , 𝑣 } ⊆ 𝑊 ∧ ( 𝐻 Σg ( 𝑇 ∘ 𝑢 ) ) = ( 𝐻 Σg ( 𝑇 ∘ 𝑣 ) ) ) } Er 𝑊 )
32 simplrl ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o ) ) → 𝑥 ∈ 𝑊 )
33 fviss ⊢ ( I ‘ Word ( 𝐼 × 2o ) ) ⊆ Word ( 𝐼 × 2o )
34 7 33 eqsstri ⊢ 𝑊 ⊆ Word ( 𝐼 × 2o )
35 34 32 sselid ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o ) ) → 𝑥 ∈ Word ( 𝐼 × 2o ) )
36 opelxpi ⊢ ( ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o ) → ⟨ 𝑎 , 𝑏 ⟩ ∈ ( 𝐼 × 2o ) )
37 36 adantl ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o ) ) → ⟨ 𝑎 , 𝑏 ⟩ ∈ ( 𝐼 × 2o ) )
38 simprl ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o ) ) → 𝑎 ∈ 𝐼 )
39 2oconcl ⊢ ( 𝑏 ∈ 2o → ( 1o ∖ 𝑏 ) ∈ 2o )
40 39 ad2antll ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o ) ) → ( 1o ∖ 𝑏 ) ∈ 2o )
41 38 40 opelxpd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o ) ) → ⟨ 𝑎 , ( 1o ∖ 𝑏 ) ⟩ ∈ ( 𝐼 × 2o ) )
42 37 41 s2cld ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o ) ) → ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1o ∖ 𝑏 ) ⟩ ”⟩ ∈ Word ( 𝐼 × 2o ) )
43 splcl ⊢ ( ( 𝑥 ∈ Word ( 𝐼 × 2o ) ∧ ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1o ∖ 𝑏 ) ⟩ ”⟩ ∈ Word ( 𝐼 × 2o ) ) → ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1o ∖ 𝑏 ) ⟩ ”⟩ ⟩ ) ∈ Word ( 𝐼 × 2o ) )
44 35 42 43 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o ) ) → ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1o ∖ 𝑏 ) ⟩ ”⟩ ⟩ ) ∈ Word ( 𝐼 × 2o ) )
45 7 efgrcl ⊢ ( 𝑥 ∈ 𝑊 → ( 𝐼 ∈ V ∧ 𝑊 = Word ( 𝐼 × 2o ) ) )
46 32 45 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o ) ) → ( 𝐼 ∈ V ∧ 𝑊 = Word ( 𝐼 × 2o ) ) )
47 46 simprd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o ) ) → 𝑊 = Word ( 𝐼 × 2o ) )
48 44 47 eleqtrrd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o ) ) → ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1o ∖ 𝑏 ) ⟩ ”⟩ ⟩ ) ∈ 𝑊 )
49 pfxcl ⊢ ( 𝑥 ∈ Word ( 𝐼 × 2o ) → ( 𝑥 prefix 𝑛 ) ∈ Word ( 𝐼 × 2o ) )
50 35 49 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o ) ) → ( 𝑥 prefix 𝑛 ) ∈ Word ( 𝐼 × 2o ) )
51 1 2 3 4 5 6 frgpuptf ⊢ ( 𝜑 → 𝑇 : ( 𝐼 × 2o ) ⟶ 𝐵 )
52 51 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o ) ) → 𝑇 : ( 𝐼 × 2o ) ⟶ 𝐵 )
53 ccatco ⊢ ( ( ( 𝑥 prefix 𝑛 ) ∈ Word ( 𝐼 × 2o ) ∧ ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1o ∖ 𝑏 ) ⟩ ”⟩ ∈ Word ( 𝐼 × 2o ) ∧ 𝑇 : ( 𝐼 × 2o ) ⟶ 𝐵 ) → ( 𝑇 ∘ ( ( 𝑥 prefix 𝑛 ) ++ ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1o ∖ 𝑏 ) ⟩ ”⟩ ) ) = ( ( 𝑇 ∘ ( 𝑥 prefix 𝑛 ) ) ++ ( 𝑇 ∘ ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1o ∖ 𝑏 ) ⟩ ”⟩ ) ) )
54 50 42 52 53 syl3anc ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o ) ) → ( 𝑇 ∘ ( ( 𝑥 prefix 𝑛 ) ++ ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1o ∖ 𝑏 ) ⟩ ”⟩ ) ) = ( ( 𝑇 ∘ ( 𝑥 prefix 𝑛 ) ) ++ ( 𝑇 ∘ ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1o ∖ 𝑏 ) ⟩ ”⟩ ) ) )
55 54 oveq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o ) ) → ( 𝐻 Σg ( 𝑇 ∘ ( ( 𝑥 prefix 𝑛 ) ++ ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1o ∖ 𝑏 ) ⟩ ”⟩ ) ) ) = ( 𝐻 Σg ( ( 𝑇 ∘ ( 𝑥 prefix 𝑛 ) ) ++ ( 𝑇 ∘ ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1o ∖ 𝑏 ) ⟩ ”⟩ ) ) ) )
56 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o ) ) → 𝐻 ∈ Grp )
57 56 grpmndd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o ) ) → 𝐻 ∈ Mnd )
58 wrdco ⊢ ( ( ( 𝑥 prefix 𝑛 ) ∈ Word ( 𝐼 × 2o ) ∧ 𝑇 : ( 𝐼 × 2o ) ⟶ 𝐵 ) → ( 𝑇 ∘ ( 𝑥 prefix 𝑛 ) ) ∈ Word 𝐵 )
59 50 52 58 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o ) ) → ( 𝑇 ∘ ( 𝑥 prefix 𝑛 ) ) ∈ Word 𝐵 )
60 wrdco ⊢ ( ( ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1o ∖ 𝑏 ) ⟩ ”⟩ ∈ Word ( 𝐼 × 2o ) ∧ 𝑇 : ( 𝐼 × 2o ) ⟶ 𝐵 ) → ( 𝑇 ∘ ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1o ∖ 𝑏 ) ⟩ ”⟩ ) ∈ Word 𝐵 )
61 42 52 60 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o ) ) → ( 𝑇 ∘ ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1o ∖ 𝑏 ) ⟩ ”⟩ ) ∈ Word 𝐵 )
62 eqid ⊢ ( +g ‘ 𝐻 ) = ( +g ‘ 𝐻 )
63 1 62 gsumccat ⊢ ( ( 𝐻 ∈ Mnd ∧ ( 𝑇 ∘ ( 𝑥 prefix 𝑛 ) ) ∈ Word 𝐵 ∧ ( 𝑇 ∘ ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1o ∖ 𝑏 ) ⟩ ”⟩ ) ∈ Word 𝐵 ) → ( 𝐻 Σg ( ( 𝑇 ∘ ( 𝑥 prefix 𝑛 ) ) ++ ( 𝑇 ∘ ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1o ∖ 𝑏 ) ⟩ ”⟩ ) ) ) = ( ( 𝐻 Σg ( 𝑇 ∘ ( 𝑥 prefix 𝑛 ) ) ) ( +g ‘ 𝐻 ) ( 𝐻 Σg ( 𝑇 ∘ ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1o ∖ 𝑏 ) ⟩ ”⟩ ) ) ) )
64 57 59 61 63 syl3anc ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o ) ) → ( 𝐻 Σg ( ( 𝑇 ∘ ( 𝑥 prefix 𝑛 ) ) ++ ( 𝑇 ∘ ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1o ∖ 𝑏 ) ⟩ ”⟩ ) ) ) = ( ( 𝐻 Σg ( 𝑇 ∘ ( 𝑥 prefix 𝑛 ) ) ) ( +g ‘ 𝐻 ) ( 𝐻 Σg ( 𝑇 ∘ ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1o ∖ 𝑏 ) ⟩ ”⟩ ) ) ) )
65 52 37 41 s2co ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o ) ) → ( 𝑇 ∘ ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1o ∖ 𝑏 ) ⟩ ”⟩ ) = ⟨“ ( 𝑇 ‘ ⟨ 𝑎 , 𝑏 ⟩ ) ( 𝑇 ‘ ⟨ 𝑎 , ( 1o ∖ 𝑏 ) ⟩ ) ”⟩ )
66 df-ov ⊢ ( 𝑎 𝑇 𝑏 ) = ( 𝑇 ‘ ⟨ 𝑎 , 𝑏 ⟩ )
67 66 a1i ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o ) ) → ( 𝑎 𝑇 𝑏 ) = ( 𝑇 ‘ ⟨ 𝑎 , 𝑏 ⟩ ) )
68 66 fveq2i ⊢ ( 𝑁 ‘ ( 𝑎 𝑇 𝑏 ) ) = ( 𝑁 ‘ ( 𝑇 ‘ ⟨ 𝑎 , 𝑏 ⟩ ) )
69 df-ov ⊢ ( 𝑎 ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2o ↦ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ ) 𝑏 ) = ( ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2o ↦ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ ) ‘ ⟨ 𝑎 , 𝑏 ⟩ )
70 eqid ⊢ ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2o ↦ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ ) = ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2o ↦ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ )
71 70 efgmval ⊢ ( ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o ) → ( 𝑎 ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2o ↦ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ ) 𝑏 ) = ⟨ 𝑎 , ( 1o ∖ 𝑏 ) ⟩ )
72 69 71 eqtr3id ⊢ ( ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o ) → ( ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2o ↦ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ ) ‘ ⟨ 𝑎 , 𝑏 ⟩ ) = ⟨ 𝑎 , ( 1o ∖ 𝑏 ) ⟩ )
73 72 adantl ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o ) ) → ( ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2o ↦ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ ) ‘ ⟨ 𝑎 , 𝑏 ⟩ ) = ⟨ 𝑎 , ( 1o ∖ 𝑏 ) ⟩ )
74 73 fveq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o ) ) → ( 𝑇 ‘ ( ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2o ↦ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ ) ‘ ⟨ 𝑎 , 𝑏 ⟩ ) ) = ( 𝑇 ‘ ⟨ 𝑎 , ( 1o ∖ 𝑏 ) ⟩ ) )
75 1 2 3 4 5 6 70 frgpuptinv ⊢ ( ( 𝜑 ∧ ⟨ 𝑎 , 𝑏 ⟩ ∈ ( 𝐼 × 2o ) ) → ( 𝑇 ‘ ( ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2o ↦ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ ) ‘ ⟨ 𝑎 , 𝑏 ⟩ ) ) = ( 𝑁 ‘ ( 𝑇 ‘ ⟨ 𝑎 , 𝑏 ⟩ ) ) )
76 36 75 sylan2 ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o ) ) → ( 𝑇 ‘ ( ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2o ↦ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ ) ‘ ⟨ 𝑎 , 𝑏 ⟩ ) ) = ( 𝑁 ‘ ( 𝑇 ‘ ⟨ 𝑎 , 𝑏 ⟩ ) ) )
77 76 adantlr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o ) ) → ( 𝑇 ‘ ( ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2o ↦ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ ) ‘ ⟨ 𝑎 , 𝑏 ⟩ ) ) = ( 𝑁 ‘ ( 𝑇 ‘ ⟨ 𝑎 , 𝑏 ⟩ ) ) )
78 74 77 eqtr3d ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o ) ) → ( 𝑇 ‘ ⟨ 𝑎 , ( 1o ∖ 𝑏 ) ⟩ ) = ( 𝑁 ‘ ( 𝑇 ‘ ⟨ 𝑎 , 𝑏 ⟩ ) ) )
79 68 78 eqtr4id ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o ) ) → ( 𝑁 ‘ ( 𝑎 𝑇 𝑏 ) ) = ( 𝑇 ‘ ⟨ 𝑎 , ( 1o ∖ 𝑏 ) ⟩ ) )
80 67 79 s2eqd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o ) ) → ⟨“ ( 𝑎 𝑇 𝑏 ) ( 𝑁 ‘ ( 𝑎 𝑇 𝑏 ) ) ”⟩ = ⟨“ ( 𝑇 ‘ ⟨ 𝑎 , 𝑏 ⟩ ) ( 𝑇 ‘ ⟨ 𝑎 , ( 1o ∖ 𝑏 ) ⟩ ) ”⟩ )
81 65 80 eqtr4d ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o ) ) → ( 𝑇 ∘ ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1o ∖ 𝑏 ) ⟩ ”⟩ ) = ⟨“ ( 𝑎 𝑇 𝑏 ) ( 𝑁 ‘ ( 𝑎 𝑇 𝑏 ) ) ”⟩ )
82 81 oveq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o ) ) → ( 𝐻 Σg ( 𝑇 ∘ ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1o ∖ 𝑏 ) ⟩ ”⟩ ) ) = ( 𝐻 Σg ⟨“ ( 𝑎 𝑇 𝑏 ) ( 𝑁 ‘ ( 𝑎 𝑇 𝑏 ) ) ”⟩ ) )
83 simprr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o ) ) → 𝑏 ∈ 2o )
84 52 38 83 fovcdmd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o ) ) → ( 𝑎 𝑇 𝑏 ) ∈ 𝐵 )
85 1 2 grpinvcl ⊢ ( ( 𝐻 ∈ Grp ∧ ( 𝑎 𝑇 𝑏 ) ∈ 𝐵 ) → ( 𝑁 ‘ ( 𝑎 𝑇 𝑏 ) ) ∈ 𝐵 )
86 56 84 85 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o ) ) → ( 𝑁 ‘ ( 𝑎 𝑇 𝑏 ) ) ∈ 𝐵 )
87 1 62 gsumws2 ⊢ ( ( 𝐻 ∈ Mnd ∧ ( 𝑎 𝑇 𝑏 ) ∈ 𝐵 ∧ ( 𝑁 ‘ ( 𝑎 𝑇 𝑏 ) ) ∈ 𝐵 ) → ( 𝐻 Σg ⟨“ ( 𝑎 𝑇 𝑏 ) ( 𝑁 ‘ ( 𝑎 𝑇 𝑏 ) ) ”⟩ ) = ( ( 𝑎 𝑇 𝑏 ) ( +g ‘ 𝐻 ) ( 𝑁 ‘ ( 𝑎 𝑇 𝑏 ) ) ) )
88 57 84 86 87 syl3anc ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o ) ) → ( 𝐻 Σg ⟨“ ( 𝑎 𝑇 𝑏 ) ( 𝑁 ‘ ( 𝑎 𝑇 𝑏 ) ) ”⟩ ) = ( ( 𝑎 𝑇 𝑏 ) ( +g ‘ 𝐻 ) ( 𝑁 ‘ ( 𝑎 𝑇 𝑏 ) ) ) )
89 eqid ⊢ ( 0g ‘ 𝐻 ) = ( 0g ‘ 𝐻 )
90 1 62 89 2 grprinv ⊢ ( ( 𝐻 ∈ Grp ∧ ( 𝑎 𝑇 𝑏 ) ∈ 𝐵 ) → ( ( 𝑎 𝑇 𝑏 ) ( +g ‘ 𝐻 ) ( 𝑁 ‘ ( 𝑎 𝑇 𝑏 ) ) ) = ( 0g ‘ 𝐻 ) )
91 56 84 90 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o ) ) → ( ( 𝑎 𝑇 𝑏 ) ( +g ‘ 𝐻 ) ( 𝑁 ‘ ( 𝑎 𝑇 𝑏 ) ) ) = ( 0g ‘ 𝐻 ) )
92 82 88 91 3eqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o ) ) → ( 𝐻 Σg ( 𝑇 ∘ ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1o ∖ 𝑏 ) ⟩ ”⟩ ) ) = ( 0g ‘ 𝐻 ) )
93 92 oveq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o ) ) → ( ( 𝐻 Σg ( 𝑇 ∘ ( 𝑥 prefix 𝑛 ) ) ) ( +g ‘ 𝐻 ) ( 𝐻 Σg ( 𝑇 ∘ ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1o ∖ 𝑏 ) ⟩ ”⟩ ) ) ) = ( ( 𝐻 Σg ( 𝑇 ∘ ( 𝑥 prefix 𝑛 ) ) ) ( +g ‘ 𝐻 ) ( 0g ‘ 𝐻 ) ) )
94 1 gsumwcl ⊢ ( ( 𝐻 ∈ Mnd ∧ ( 𝑇 ∘ ( 𝑥 prefix 𝑛 ) ) ∈ Word 𝐵 ) → ( 𝐻 Σg ( 𝑇 ∘ ( 𝑥 prefix 𝑛 ) ) ) ∈ 𝐵 )
95 57 59 94 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o ) ) → ( 𝐻 Σg ( 𝑇 ∘ ( 𝑥 prefix 𝑛 ) ) ) ∈ 𝐵 )
96 1 62 89 grprid ⊢ ( ( 𝐻 ∈ Grp ∧ ( 𝐻 Σg ( 𝑇 ∘ ( 𝑥 prefix 𝑛 ) ) ) ∈ 𝐵 ) → ( ( 𝐻 Σg ( 𝑇 ∘ ( 𝑥 prefix 𝑛 ) ) ) ( +g ‘ 𝐻 ) ( 0g ‘ 𝐻 ) ) = ( 𝐻 Σg ( 𝑇 ∘ ( 𝑥 prefix 𝑛 ) ) ) )
97 56 95 96 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o ) ) → ( ( 𝐻 Σg ( 𝑇 ∘ ( 𝑥 prefix 𝑛 ) ) ) ( +g ‘ 𝐻 ) ( 0g ‘ 𝐻 ) ) = ( 𝐻 Σg ( 𝑇 ∘ ( 𝑥 prefix 𝑛 ) ) ) )
98 93 97 eqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o ) ) → ( ( 𝐻 Σg ( 𝑇 ∘ ( 𝑥 prefix 𝑛 ) ) ) ( +g ‘ 𝐻 ) ( 𝐻 Σg ( 𝑇 ∘ ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1o ∖ 𝑏 ) ⟩ ”⟩ ) ) ) = ( 𝐻 Σg ( 𝑇 ∘ ( 𝑥 prefix 𝑛 ) ) ) )
99 55 64 98 3eqtrrd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o ) ) → ( 𝐻 Σg ( 𝑇 ∘ ( 𝑥 prefix 𝑛 ) ) ) = ( 𝐻 Σg ( 𝑇 ∘ ( ( 𝑥 prefix 𝑛 ) ++ ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1o ∖ 𝑏 ) ⟩ ”⟩ ) ) ) )
100 99 oveq1d ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o ) ) → ( ( 𝐻 Σg ( 𝑇 ∘ ( 𝑥 prefix 𝑛 ) ) ) ( +g ‘ 𝐻 ) ( 𝐻 Σg ( 𝑇 ∘ ( 𝑥 substr ⟨ 𝑛 , ( ♯ ‘ 𝑥 ) ⟩ ) ) ) ) = ( ( 𝐻 Σg ( 𝑇 ∘ ( ( 𝑥 prefix 𝑛 ) ++ ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1o ∖ 𝑏 ) ⟩ ”⟩ ) ) ) ( +g ‘ 𝐻 ) ( 𝐻 Σg ( 𝑇 ∘ ( 𝑥 substr ⟨ 𝑛 , ( ♯ ‘ 𝑥 ) ⟩ ) ) ) ) )
101 swrdcl ⊢ ( 𝑥 ∈ Word ( 𝐼 × 2o ) → ( 𝑥 substr ⟨ 𝑛 , ( ♯ ‘ 𝑥 ) ⟩ ) ∈ Word ( 𝐼 × 2o ) )
102 35 101 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o ) ) → ( 𝑥 substr ⟨ 𝑛 , ( ♯ ‘ 𝑥 ) ⟩ ) ∈ Word ( 𝐼 × 2o ) )
103 wrdco ⊢ ( ( ( 𝑥 substr ⟨ 𝑛 , ( ♯ ‘ 𝑥 ) ⟩ ) ∈ Word ( 𝐼 × 2o ) ∧ 𝑇 : ( 𝐼 × 2o ) ⟶ 𝐵 ) → ( 𝑇 ∘ ( 𝑥 substr ⟨ 𝑛 , ( ♯ ‘ 𝑥 ) ⟩ ) ) ∈ Word 𝐵 )
104 102 52 103 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o ) ) → ( 𝑇 ∘ ( 𝑥 substr ⟨ 𝑛 , ( ♯ ‘ 𝑥 ) ⟩ ) ) ∈ Word 𝐵 )
105 1 62 gsumccat ⊢ ( ( 𝐻 ∈ Mnd ∧ ( 𝑇 ∘ ( 𝑥 prefix 𝑛 ) ) ∈ Word 𝐵 ∧ ( 𝑇 ∘ ( 𝑥 substr ⟨ 𝑛 , ( ♯ ‘ 𝑥 ) ⟩ ) ) ∈ Word 𝐵 ) → ( 𝐻 Σg ( ( 𝑇 ∘ ( 𝑥 prefix 𝑛 ) ) ++ ( 𝑇 ∘ ( 𝑥 substr ⟨ 𝑛 , ( ♯ ‘ 𝑥 ) ⟩ ) ) ) ) = ( ( 𝐻 Σg ( 𝑇 ∘ ( 𝑥 prefix 𝑛 ) ) ) ( +g ‘ 𝐻 ) ( 𝐻 Σg ( 𝑇 ∘ ( 𝑥 substr ⟨ 𝑛 , ( ♯ ‘ 𝑥 ) ⟩ ) ) ) ) )
106 57 59 104 105 syl3anc ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o ) ) → ( 𝐻 Σg ( ( 𝑇 ∘ ( 𝑥 prefix 𝑛 ) ) ++ ( 𝑇 ∘ ( 𝑥 substr ⟨ 𝑛 , ( ♯ ‘ 𝑥 ) ⟩ ) ) ) ) = ( ( 𝐻 Σg ( 𝑇 ∘ ( 𝑥 prefix 𝑛 ) ) ) ( +g ‘ 𝐻 ) ( 𝐻 Σg ( 𝑇 ∘ ( 𝑥 substr ⟨ 𝑛 , ( ♯ ‘ 𝑥 ) ⟩ ) ) ) ) )
107 ccatcl ⊢ ( ( ( 𝑥 prefix 𝑛 ) ∈ Word ( 𝐼 × 2o ) ∧ ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1o ∖ 𝑏 ) ⟩ ”⟩ ∈ Word ( 𝐼 × 2o ) ) → ( ( 𝑥 prefix 𝑛 ) ++ ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1o ∖ 𝑏 ) ⟩ ”⟩ ) ∈ Word ( 𝐼 × 2o ) )
108 50 42 107 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o ) ) → ( ( 𝑥 prefix 𝑛 ) ++ ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1o ∖ 𝑏 ) ⟩ ”⟩ ) ∈ Word ( 𝐼 × 2o ) )
109 wrdco ⊢ ( ( ( ( 𝑥 prefix 𝑛 ) ++ ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1o ∖ 𝑏 ) ⟩ ”⟩ ) ∈ Word ( 𝐼 × 2o ) ∧ 𝑇 : ( 𝐼 × 2o ) ⟶ 𝐵 ) → ( 𝑇 ∘ ( ( 𝑥 prefix 𝑛 ) ++ ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1o ∖ 𝑏 ) ⟩ ”⟩ ) ) ∈ Word 𝐵 )
110 108 52 109 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o ) ) → ( 𝑇 ∘ ( ( 𝑥 prefix 𝑛 ) ++ ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1o ∖ 𝑏 ) ⟩ ”⟩ ) ) ∈ Word 𝐵 )
111 1 62 gsumccat ⊢ ( ( 𝐻 ∈ Mnd ∧ ( 𝑇 ∘ ( ( 𝑥 prefix 𝑛 ) ++ ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1o ∖ 𝑏 ) ⟩ ”⟩ ) ) ∈ Word 𝐵 ∧ ( 𝑇 ∘ ( 𝑥 substr ⟨ 𝑛 , ( ♯ ‘ 𝑥 ) ⟩ ) ) ∈ Word 𝐵 ) → ( 𝐻 Σg ( ( 𝑇 ∘ ( ( 𝑥 prefix 𝑛 ) ++ ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1o ∖ 𝑏 ) ⟩ ”⟩ ) ) ++ ( 𝑇 ∘ ( 𝑥 substr ⟨ 𝑛 , ( ♯ ‘ 𝑥 ) ⟩ ) ) ) ) = ( ( 𝐻 Σg ( 𝑇 ∘ ( ( 𝑥 prefix 𝑛 ) ++ ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1o ∖ 𝑏 ) ⟩ ”⟩ ) ) ) ( +g ‘ 𝐻 ) ( 𝐻 Σg ( 𝑇 ∘ ( 𝑥 substr ⟨ 𝑛 , ( ♯ ‘ 𝑥 ) ⟩ ) ) ) ) )
112 57 110 104 111 syl3anc ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o ) ) → ( 𝐻 Σg ( ( 𝑇 ∘ ( ( 𝑥 prefix 𝑛 ) ++ ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1o ∖ 𝑏 ) ⟩ ”⟩ ) ) ++ ( 𝑇 ∘ ( 𝑥 substr ⟨ 𝑛 , ( ♯ ‘ 𝑥 ) ⟩ ) ) ) ) = ( ( 𝐻 Σg ( 𝑇 ∘ ( ( 𝑥 prefix 𝑛 ) ++ ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1o ∖ 𝑏 ) ⟩ ”⟩ ) ) ) ( +g ‘ 𝐻 ) ( 𝐻 Σg ( 𝑇 ∘ ( 𝑥 substr ⟨ 𝑛 , ( ♯ ‘ 𝑥 ) ⟩ ) ) ) ) )
113 100 106 112 3eqtr4d ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o ) ) → ( 𝐻 Σg ( ( 𝑇 ∘ ( 𝑥 prefix 𝑛 ) ) ++ ( 𝑇 ∘ ( 𝑥 substr ⟨ 𝑛 , ( ♯ ‘ 𝑥 ) ⟩ ) ) ) ) = ( 𝐻 Σg ( ( 𝑇 ∘ ( ( 𝑥 prefix 𝑛 ) ++ ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1o ∖ 𝑏 ) ⟩ ”⟩ ) ) ++ ( 𝑇 ∘ ( 𝑥 substr ⟨ 𝑛 , ( ♯ ‘ 𝑥 ) ⟩ ) ) ) ) )
114 simplrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o ) ) → 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) )
115 lencl ⊢ ( 𝑥 ∈ Word ( 𝐼 × 2o ) → ( ♯ ‘ 𝑥 ) ∈ ℕ0 )
116 35 115 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o ) ) → ( ♯ ‘ 𝑥 ) ∈ ℕ0 )
117 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
118 116 117 eleqtrdi ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o ) ) → ( ♯ ‘ 𝑥 ) ∈ ( ℤ≥ ‘ 0 ) )
119 eluzfz2 ⊢ ( ( ♯ ‘ 𝑥 ) ∈ ( ℤ≥ ‘ 0 ) → ( ♯ ‘ 𝑥 ) ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) )
120 118 119 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o ) ) → ( ♯ ‘ 𝑥 ) ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) )
121 ccatpfx ⊢ ( ( 𝑥 ∈ Word ( 𝐼 × 2o ) ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ∧ ( ♯ ‘ 𝑥 ) ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) → ( ( 𝑥 prefix 𝑛 ) ++ ( 𝑥 substr ⟨ 𝑛 , ( ♯ ‘ 𝑥 ) ⟩ ) ) = ( 𝑥 prefix ( ♯ ‘ 𝑥 ) ) )
122 35 114 120 121 syl3anc ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o ) ) → ( ( 𝑥 prefix 𝑛 ) ++ ( 𝑥 substr ⟨ 𝑛 , ( ♯ ‘ 𝑥 ) ⟩ ) ) = ( 𝑥 prefix ( ♯ ‘ 𝑥 ) ) )
123 pfxid ⊢ ( 𝑥 ∈ Word ( 𝐼 × 2o ) → ( 𝑥 prefix ( ♯ ‘ 𝑥 ) ) = 𝑥 )
124 35 123 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o ) ) → ( 𝑥 prefix ( ♯ ‘ 𝑥 ) ) = 𝑥 )
125 122 124 eqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o ) ) → ( ( 𝑥 prefix 𝑛 ) ++ ( 𝑥 substr ⟨ 𝑛 , ( ♯ ‘ 𝑥 ) ⟩ ) ) = 𝑥 )
126 125 coeq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o ) ) → ( 𝑇 ∘ ( ( 𝑥 prefix 𝑛 ) ++ ( 𝑥 substr ⟨ 𝑛 , ( ♯ ‘ 𝑥 ) ⟩ ) ) ) = ( 𝑇 ∘ 𝑥 ) )
127 ccatco ⊢ ( ( ( 𝑥 prefix 𝑛 ) ∈ Word ( 𝐼 × 2o ) ∧ ( 𝑥 substr ⟨ 𝑛 , ( ♯ ‘ 𝑥 ) ⟩ ) ∈ Word ( 𝐼 × 2o ) ∧ 𝑇 : ( 𝐼 × 2o ) ⟶ 𝐵 ) → ( 𝑇 ∘ ( ( 𝑥 prefix 𝑛 ) ++ ( 𝑥 substr ⟨ 𝑛 , ( ♯ ‘ 𝑥 ) ⟩ ) ) ) = ( ( 𝑇 ∘ ( 𝑥 prefix 𝑛 ) ) ++ ( 𝑇 ∘ ( 𝑥 substr ⟨ 𝑛 , ( ♯ ‘ 𝑥 ) ⟩ ) ) ) )
128 50 102 52 127 syl3anc ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o ) ) → ( 𝑇 ∘ ( ( 𝑥 prefix 𝑛 ) ++ ( 𝑥 substr ⟨ 𝑛 , ( ♯ ‘ 𝑥 ) ⟩ ) ) ) = ( ( 𝑇 ∘ ( 𝑥 prefix 𝑛 ) ) ++ ( 𝑇 ∘ ( 𝑥 substr ⟨ 𝑛 , ( ♯ ‘ 𝑥 ) ⟩ ) ) ) )
129 126 128 eqtr3d ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o ) ) → ( 𝑇 ∘ 𝑥 ) = ( ( 𝑇 ∘ ( 𝑥 prefix 𝑛 ) ) ++ ( 𝑇 ∘ ( 𝑥 substr ⟨ 𝑛 , ( ♯ ‘ 𝑥 ) ⟩ ) ) ) )
130 129 oveq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o ) ) → ( 𝐻 Σg ( 𝑇 ∘ 𝑥 ) ) = ( 𝐻 Σg ( ( 𝑇 ∘ ( 𝑥 prefix 𝑛 ) ) ++ ( 𝑇 ∘ ( 𝑥 substr ⟨ 𝑛 , ( ♯ ‘ 𝑥 ) ⟩ ) ) ) ) )
131 splval ⊢ ( ( 𝑥 ∈ 𝑊 ∧ ( 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ∧ ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1o ∖ 𝑏 ) ⟩ ”⟩ ∈ Word ( 𝐼 × 2o ) ) ) → ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1o ∖ 𝑏 ) ⟩ ”⟩ ⟩ ) = ( ( ( 𝑥 prefix 𝑛 ) ++ ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1o ∖ 𝑏 ) ⟩ ”⟩ ) ++ ( 𝑥 substr ⟨ 𝑛 , ( ♯ ‘ 𝑥 ) ⟩ ) ) )
132 32 114 114 42 131 syl13anc ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o ) ) → ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1o ∖ 𝑏 ) ⟩ ”⟩ ⟩ ) = ( ( ( 𝑥 prefix 𝑛 ) ++ ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1o ∖ 𝑏 ) ⟩ ”⟩ ) ++ ( 𝑥 substr ⟨ 𝑛 , ( ♯ ‘ 𝑥 ) ⟩ ) ) )
133 132 coeq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o ) ) → ( 𝑇 ∘ ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1o ∖ 𝑏 ) ⟩ ”⟩ ⟩ ) ) = ( 𝑇 ∘ ( ( ( 𝑥 prefix 𝑛 ) ++ ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1o ∖ 𝑏 ) ⟩ ”⟩ ) ++ ( 𝑥 substr ⟨ 𝑛 , ( ♯ ‘ 𝑥 ) ⟩ ) ) ) )
134 ccatco ⊢ ( ( ( ( 𝑥 prefix 𝑛 ) ++ ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1o ∖ 𝑏 ) ⟩ ”⟩ ) ∈ Word ( 𝐼 × 2o ) ∧ ( 𝑥 substr ⟨ 𝑛 , ( ♯ ‘ 𝑥 ) ⟩ ) ∈ Word ( 𝐼 × 2o ) ∧ 𝑇 : ( 𝐼 × 2o ) ⟶ 𝐵 ) → ( 𝑇 ∘ ( ( ( 𝑥 prefix 𝑛 ) ++ ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1o ∖ 𝑏 ) ⟩ ”⟩ ) ++ ( 𝑥 substr ⟨ 𝑛 , ( ♯ ‘ 𝑥 ) ⟩ ) ) ) = ( ( 𝑇 ∘ ( ( 𝑥 prefix 𝑛 ) ++ ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1o ∖ 𝑏 ) ⟩ ”⟩ ) ) ++ ( 𝑇 ∘ ( 𝑥 substr ⟨ 𝑛 , ( ♯ ‘ 𝑥 ) ⟩ ) ) ) )
135 108 102 52 134 syl3anc ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o ) ) → ( 𝑇 ∘ ( ( ( 𝑥 prefix 𝑛 ) ++ ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1o ∖ 𝑏 ) ⟩ ”⟩ ) ++ ( 𝑥 substr ⟨ 𝑛 , ( ♯ ‘ 𝑥 ) ⟩ ) ) ) = ( ( 𝑇 ∘ ( ( 𝑥 prefix 𝑛 ) ++ ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1o ∖ 𝑏 ) ⟩ ”⟩ ) ) ++ ( 𝑇 ∘ ( 𝑥 substr ⟨ 𝑛 , ( ♯ ‘ 𝑥 ) ⟩ ) ) ) )
136 133 135 eqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o ) ) → ( 𝑇 ∘ ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1o ∖ 𝑏 ) ⟩ ”⟩ ⟩ ) ) = ( ( 𝑇 ∘ ( ( 𝑥 prefix 𝑛 ) ++ ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1o ∖ 𝑏 ) ⟩ ”⟩ ) ) ++ ( 𝑇 ∘ ( 𝑥 substr ⟨ 𝑛 , ( ♯ ‘ 𝑥 ) ⟩ ) ) ) )
137 136 oveq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o ) ) → ( 𝐻 Σg ( 𝑇 ∘ ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1o ∖ 𝑏 ) ⟩ ”⟩ ⟩ ) ) ) = ( 𝐻 Σg ( ( 𝑇 ∘ ( ( 𝑥 prefix 𝑛 ) ++ ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1o ∖ 𝑏 ) ⟩ ”⟩ ) ) ++ ( 𝑇 ∘ ( 𝑥 substr ⟨ 𝑛 , ( ♯ ‘ 𝑥 ) ⟩ ) ) ) ) )
138 113 130 137 3eqtr4d ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o ) ) → ( 𝐻 Σg ( 𝑇 ∘ 𝑥 ) ) = ( 𝐻 Σg ( 𝑇 ∘ ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1o ∖ 𝑏 ) ⟩ ”⟩ ⟩ ) ) ) )
139 vex ⊢ 𝑥 ∈ V
140 ovex ⊢ ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1o ∖ 𝑏 ) ⟩ ”⟩ ⟩ ) ∈ V
141 eleq1 ⊢ ( 𝑢 = 𝑥 → ( 𝑢 ∈ 𝑊 ↔ 𝑥 ∈ 𝑊 ) )
142 eleq1 ⊢ ( 𝑣 = ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1o ∖ 𝑏 ) ⟩ ”⟩ ⟩ ) → ( 𝑣 ∈ 𝑊 ↔ ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1o ∖ 𝑏 ) ⟩ ”⟩ ⟩ ) ∈ 𝑊 ) )
143 141 142 bi2anan9 ⊢ ( ( 𝑢 = 𝑥 ∧ 𝑣 = ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1o ∖ 𝑏 ) ⟩ ”⟩ ⟩ ) ) → ( ( 𝑢 ∈ 𝑊 ∧ 𝑣 ∈ 𝑊 ) ↔ ( 𝑥 ∈ 𝑊 ∧ ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1o ∖ 𝑏 ) ⟩ ”⟩ ⟩ ) ∈ 𝑊 ) ) )
144 25 143 bitr3id ⊢ ( ( 𝑢 = 𝑥 ∧ 𝑣 = ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1o ∖ 𝑏 ) ⟩ ”⟩ ⟩ ) ) → ( { 𝑢 , 𝑣 } ⊆ 𝑊 ↔ ( 𝑥 ∈ 𝑊 ∧ ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1o ∖ 𝑏 ) ⟩ ”⟩ ⟩ ) ∈ 𝑊 ) ) )
145 coeq2 ⊢ ( 𝑢 = 𝑥 → ( 𝑇 ∘ 𝑢 ) = ( 𝑇 ∘ 𝑥 ) )
146 145 oveq2d ⊢ ( 𝑢 = 𝑥 → ( 𝐻 Σg ( 𝑇 ∘ 𝑢 ) ) = ( 𝐻 Σg ( 𝑇 ∘ 𝑥 ) ) )
147 coeq2 ⊢ ( 𝑣 = ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1o ∖ 𝑏 ) ⟩ ”⟩ ⟩ ) → ( 𝑇 ∘ 𝑣 ) = ( 𝑇 ∘ ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1o ∖ 𝑏 ) ⟩ ”⟩ ⟩ ) ) )
148 147 oveq2d ⊢ ( 𝑣 = ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1o ∖ 𝑏 ) ⟩ ”⟩ ⟩ ) → ( 𝐻 Σg ( 𝑇 ∘ 𝑣 ) ) = ( 𝐻 Σg ( 𝑇 ∘ ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1o ∖ 𝑏 ) ⟩ ”⟩ ⟩ ) ) ) )
149 146 148 eqeqan12d ⊢ ( ( 𝑢 = 𝑥 ∧ 𝑣 = ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1o ∖ 𝑏 ) ⟩ ”⟩ ⟩ ) ) → ( ( 𝐻 Σg ( 𝑇 ∘ 𝑢 ) ) = ( 𝐻 Σg ( 𝑇 ∘ 𝑣 ) ) ↔ ( 𝐻 Σg ( 𝑇 ∘ 𝑥 ) ) = ( 𝐻 Σg ( 𝑇 ∘ ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1o ∖ 𝑏 ) ⟩ ”⟩ ⟩ ) ) ) ) )
150 144 149 anbi12d ⊢ ( ( 𝑢 = 𝑥 ∧ 𝑣 = ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1o ∖ 𝑏 ) ⟩ ”⟩ ⟩ ) ) → ( ( { 𝑢 , 𝑣 } ⊆ 𝑊 ∧ ( 𝐻 Σg ( 𝑇 ∘ 𝑢 ) ) = ( 𝐻 Σg ( 𝑇 ∘ 𝑣 ) ) ) ↔ ( ( 𝑥 ∈ 𝑊 ∧ ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1o ∖ 𝑏 ) ⟩ ”⟩ ⟩ ) ∈ 𝑊 ) ∧ ( 𝐻 Σg ( 𝑇 ∘ 𝑥 ) ) = ( 𝐻 Σg ( 𝑇 ∘ ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1o ∖ 𝑏 ) ⟩ ”⟩ ⟩ ) ) ) ) ) )
151 eqid ⊢ { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( { 𝑢 , 𝑣 } ⊆ 𝑊 ∧ ( 𝐻 Σg ( 𝑇 ∘ 𝑢 ) ) = ( 𝐻 Σg ( 𝑇 ∘ 𝑣 ) ) ) } = { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( { 𝑢 , 𝑣 } ⊆ 𝑊 ∧ ( 𝐻 Σg ( 𝑇 ∘ 𝑢 ) ) = ( 𝐻 Σg ( 𝑇 ∘ 𝑣 ) ) ) }
152 139 140 150 151 braba ⊢ ( 𝑥 { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( { 𝑢 , 𝑣 } ⊆ 𝑊 ∧ ( 𝐻 Σg ( 𝑇 ∘ 𝑢 ) ) = ( 𝐻 Σg ( 𝑇 ∘ 𝑣 ) ) ) } ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1o ∖ 𝑏 ) ⟩ ”⟩ ⟩ ) ↔ ( ( 𝑥 ∈ 𝑊 ∧ ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1o ∖ 𝑏 ) ⟩ ”⟩ ⟩ ) ∈ 𝑊 ) ∧ ( 𝐻 Σg ( 𝑇 ∘ 𝑥 ) ) = ( 𝐻 Σg ( 𝑇 ∘ ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1o ∖ 𝑏 ) ⟩ ”⟩ ⟩ ) ) ) ) )
153 32 48 138 152 syl21anbrc ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o ) ) → 𝑥 { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( { 𝑢 , 𝑣 } ⊆ 𝑊 ∧ ( 𝐻 Σg ( 𝑇 ∘ 𝑢 ) ) = ( 𝐻 Σg ( 𝑇 ∘ 𝑣 ) ) ) } ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1o ∖ 𝑏 ) ⟩ ”⟩ ⟩ ) )
154 153 ralrimivva ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) → ∀ 𝑎 ∈ 𝐼 ∀ 𝑏 ∈ 2o 𝑥 { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( { 𝑢 , 𝑣 } ⊆ 𝑊 ∧ ( 𝐻 Σg ( 𝑇 ∘ 𝑢 ) ) = ( 𝐻 Σg ( 𝑇 ∘ 𝑣 ) ) ) } ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1o ∖ 𝑏 ) ⟩ ”⟩ ⟩ ) )
155 154 ralrimivva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑊 ∀ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ∀ 𝑎 ∈ 𝐼 ∀ 𝑏 ∈ 2o 𝑥 { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( { 𝑢 , 𝑣 } ⊆ 𝑊 ∧ ( 𝐻 Σg ( 𝑇 ∘ 𝑢 ) ) = ( 𝐻 Σg ( 𝑇 ∘ 𝑣 ) ) ) } ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1o ∖ 𝑏 ) ⟩ ”⟩ ⟩ ) )
156 7 fvexi ⊢ 𝑊 ∈ V
157 erex ⊢ ( { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( { 𝑢 , 𝑣 } ⊆ 𝑊 ∧ ( 𝐻 Σg ( 𝑇 ∘ 𝑢 ) ) = ( 𝐻 Σg ( 𝑇 ∘ 𝑣 ) ) ) } Er 𝑊 → ( 𝑊 ∈ V → { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( { 𝑢 , 𝑣 } ⊆ 𝑊 ∧ ( 𝐻 Σg ( 𝑇 ∘ 𝑢 ) ) = ( 𝐻 Σg ( 𝑇 ∘ 𝑣 ) ) ) } ∈ V ) )
158 31 156 157 mpisyl ⊢ ( 𝜑 → { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( { 𝑢 , 𝑣 } ⊆ 𝑊 ∧ ( 𝐻 Σg ( 𝑇 ∘ 𝑢 ) ) = ( 𝐻 Σg ( 𝑇 ∘ 𝑣 ) ) ) } ∈ V )
159 ereq1 ⊢ ( 𝑟 = { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( { 𝑢 , 𝑣 } ⊆ 𝑊 ∧ ( 𝐻 Σg ( 𝑇 ∘ 𝑢 ) ) = ( 𝐻 Σg ( 𝑇 ∘ 𝑣 ) ) ) } → ( 𝑟 Er 𝑊 ↔ { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( { 𝑢 , 𝑣 } ⊆ 𝑊 ∧ ( 𝐻 Σg ( 𝑇 ∘ 𝑢 ) ) = ( 𝐻 Σg ( 𝑇 ∘ 𝑣 ) ) ) } Er 𝑊 ) )
160 breq ⊢ ( 𝑟 = { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( { 𝑢 , 𝑣 } ⊆ 𝑊 ∧ ( 𝐻 Σg ( 𝑇 ∘ 𝑢 ) ) = ( 𝐻 Σg ( 𝑇 ∘ 𝑣 ) ) ) } → ( 𝑥 𝑟 ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1o ∖ 𝑏 ) ⟩ ”⟩ ⟩ ) ↔ 𝑥 { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( { 𝑢 , 𝑣 } ⊆ 𝑊 ∧ ( 𝐻 Σg ( 𝑇 ∘ 𝑢 ) ) = ( 𝐻 Σg ( 𝑇 ∘ 𝑣 ) ) ) } ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1o ∖ 𝑏 ) ⟩ ”⟩ ⟩ ) ) )
161 160 2ralbidv ⊢ ( 𝑟 = { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( { 𝑢 , 𝑣 } ⊆ 𝑊 ∧ ( 𝐻 Σg ( 𝑇 ∘ 𝑢 ) ) = ( 𝐻 Σg ( 𝑇 ∘ 𝑣 ) ) ) } → ( ∀ 𝑎 ∈ 𝐼 ∀ 𝑏 ∈ 2o 𝑥 𝑟 ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1o ∖ 𝑏 ) ⟩ ”⟩ ⟩ ) ↔ ∀ 𝑎 ∈ 𝐼 ∀ 𝑏 ∈ 2o 𝑥 { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( { 𝑢 , 𝑣 } ⊆ 𝑊 ∧ ( 𝐻 Σg ( 𝑇 ∘ 𝑢 ) ) = ( 𝐻 Σg ( 𝑇 ∘ 𝑣 ) ) ) } ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1o ∖ 𝑏 ) ⟩ ”⟩ ⟩ ) ) )
162 161 2ralbidv ⊢ ( 𝑟 = { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( { 𝑢 , 𝑣 } ⊆ 𝑊 ∧ ( 𝐻 Σg ( 𝑇 ∘ 𝑢 ) ) = ( 𝐻 Σg ( 𝑇 ∘ 𝑣 ) ) ) } → ( ∀ 𝑥 ∈ 𝑊 ∀ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ∀ 𝑎 ∈ 𝐼 ∀ 𝑏 ∈ 2o 𝑥 𝑟 ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1o ∖ 𝑏 ) ⟩ ”⟩ ⟩ ) ↔ ∀ 𝑥 ∈ 𝑊 ∀ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ∀ 𝑎 ∈ 𝐼 ∀ 𝑏 ∈ 2o 𝑥 { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( { 𝑢 , 𝑣 } ⊆ 𝑊 ∧ ( 𝐻 Σg ( 𝑇 ∘ 𝑢 ) ) = ( 𝐻 Σg ( 𝑇 ∘ 𝑣 ) ) ) } ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1o ∖ 𝑏 ) ⟩ ”⟩ ⟩ ) ) )
163 159 162 anbi12d ⊢ ( 𝑟 = { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( { 𝑢 , 𝑣 } ⊆ 𝑊 ∧ ( 𝐻 Σg ( 𝑇 ∘ 𝑢 ) ) = ( 𝐻 Σg ( 𝑇 ∘ 𝑣 ) ) ) } → ( ( 𝑟 Er 𝑊 ∧ ∀ 𝑥 ∈ 𝑊 ∀ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ∀ 𝑎 ∈ 𝐼 ∀ 𝑏 ∈ 2o 𝑥 𝑟 ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1o ∖ 𝑏 ) ⟩ ”⟩ ⟩ ) ) ↔ ( { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( { 𝑢 , 𝑣 } ⊆ 𝑊 ∧ ( 𝐻 Σg ( 𝑇 ∘ 𝑢 ) ) = ( 𝐻 Σg ( 𝑇 ∘ 𝑣 ) ) ) } Er 𝑊 ∧ ∀ 𝑥 ∈ 𝑊 ∀ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ∀ 𝑎 ∈ 𝐼 ∀ 𝑏 ∈ 2o 𝑥 { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( { 𝑢 , 𝑣 } ⊆ 𝑊 ∧ ( 𝐻 Σg ( 𝑇 ∘ 𝑢 ) ) = ( 𝐻 Σg ( 𝑇 ∘ 𝑣 ) ) ) } ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1o ∖ 𝑏 ) ⟩ ”⟩ ⟩ ) ) ) )
164 163 elabg ⊢ ( { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( { 𝑢 , 𝑣 } ⊆ 𝑊 ∧ ( 𝐻 Σg ( 𝑇 ∘ 𝑢 ) ) = ( 𝐻 Σg ( 𝑇 ∘ 𝑣 ) ) ) } ∈ V → ( { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( { 𝑢 , 𝑣 } ⊆ 𝑊 ∧ ( 𝐻 Σg ( 𝑇 ∘ 𝑢 ) ) = ( 𝐻 Σg ( 𝑇 ∘ 𝑣 ) ) ) } ∈ { 𝑟 ∣ ( 𝑟 Er 𝑊 ∧ ∀ 𝑥 ∈ 𝑊 ∀ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ∀ 𝑎 ∈ 𝐼 ∀ 𝑏 ∈ 2o 𝑥 𝑟 ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1o ∖ 𝑏 ) ⟩ ”⟩ ⟩ ) ) } ↔ ( { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( { 𝑢 , 𝑣 } ⊆ 𝑊 ∧ ( 𝐻 Σg ( 𝑇 ∘ 𝑢 ) ) = ( 𝐻 Σg ( 𝑇 ∘ 𝑣 ) ) ) } Er 𝑊 ∧ ∀ 𝑥 ∈ 𝑊 ∀ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ∀ 𝑎 ∈ 𝐼 ∀ 𝑏 ∈ 2o 𝑥 { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( { 𝑢 , 𝑣 } ⊆ 𝑊 ∧ ( 𝐻 Σg ( 𝑇 ∘ 𝑢 ) ) = ( 𝐻 Σg ( 𝑇 ∘ 𝑣 ) ) ) } ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1o ∖ 𝑏 ) ⟩ ”⟩ ⟩ ) ) ) )
165 158 164 syl ⊢ ( 𝜑 → ( { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( { 𝑢 , 𝑣 } ⊆ 𝑊 ∧ ( 𝐻 Σg ( 𝑇 ∘ 𝑢 ) ) = ( 𝐻 Σg ( 𝑇 ∘ 𝑣 ) ) ) } ∈ { 𝑟 ∣ ( 𝑟 Er 𝑊 ∧ ∀ 𝑥 ∈ 𝑊 ∀ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ∀ 𝑎 ∈ 𝐼 ∀ 𝑏 ∈ 2o 𝑥 𝑟 ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1o ∖ 𝑏 ) ⟩ ”⟩ ⟩ ) ) } ↔ ( { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( { 𝑢 , 𝑣 } ⊆ 𝑊 ∧ ( 𝐻 Σg ( 𝑇 ∘ 𝑢 ) ) = ( 𝐻 Σg ( 𝑇 ∘ 𝑣 ) ) ) } Er 𝑊 ∧ ∀ 𝑥 ∈ 𝑊 ∀ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ∀ 𝑎 ∈ 𝐼 ∀ 𝑏 ∈ 2o 𝑥 { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( { 𝑢 , 𝑣 } ⊆ 𝑊 ∧ ( 𝐻 Σg ( 𝑇 ∘ 𝑢 ) ) = ( 𝐻 Σg ( 𝑇 ∘ 𝑣 ) ) ) } ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1o ∖ 𝑏 ) ⟩ ”⟩ ⟩ ) ) ) )
166 31 155 165 mpbir2and ⊢ ( 𝜑 → { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( { 𝑢 , 𝑣 } ⊆ 𝑊 ∧ ( 𝐻 Σg ( 𝑇 ∘ 𝑢 ) ) = ( 𝐻 Σg ( 𝑇 ∘ 𝑣 ) ) ) } ∈ { 𝑟 ∣ ( 𝑟 Er 𝑊 ∧ ∀ 𝑥 ∈ 𝑊 ∀ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ∀ 𝑎 ∈ 𝐼 ∀ 𝑏 ∈ 2o 𝑥 𝑟 ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1o ∖ 𝑏 ) ⟩ ”⟩ ⟩ ) ) } )
167 intss1 ⊢ ( { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( { 𝑢 , 𝑣 } ⊆ 𝑊 ∧ ( 𝐻 Σg ( 𝑇 ∘ 𝑢 ) ) = ( 𝐻 Σg ( 𝑇 ∘ 𝑣 ) ) ) } ∈ { 𝑟 ∣ ( 𝑟 Er 𝑊 ∧ ∀ 𝑥 ∈ 𝑊 ∀ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ∀ 𝑎 ∈ 𝐼 ∀ 𝑏 ∈ 2o 𝑥 𝑟 ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1o ∖ 𝑏 ) ⟩ ”⟩ ⟩ ) ) } → ∩ { 𝑟 ∣ ( 𝑟 Er 𝑊 ∧ ∀ 𝑥 ∈ 𝑊 ∀ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ∀ 𝑎 ∈ 𝐼 ∀ 𝑏 ∈ 2o 𝑥 𝑟 ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1o ∖ 𝑏 ) ⟩ ”⟩ ⟩ ) ) } ⊆ { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( { 𝑢 , 𝑣 } ⊆ 𝑊 ∧ ( 𝐻 Σg ( 𝑇 ∘ 𝑢 ) ) = ( 𝐻 Σg ( 𝑇 ∘ 𝑣 ) ) ) } )
168 166 167 syl ⊢ ( 𝜑 → ∩ { 𝑟 ∣ ( 𝑟 Er 𝑊 ∧ ∀ 𝑥 ∈ 𝑊 ∀ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ∀ 𝑎 ∈ 𝐼 ∀ 𝑏 ∈ 2o 𝑥 𝑟 ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1o ∖ 𝑏 ) ⟩ ”⟩ ⟩ ) ) } ⊆ { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( { 𝑢 , 𝑣 } ⊆ 𝑊 ∧ ( 𝐻 Σg ( 𝑇 ∘ 𝑢 ) ) = ( 𝐻 Σg ( 𝑇 ∘ 𝑣 ) ) ) } )
169 9 168 eqsstrid ⊢ ( 𝜑 → ∼ ⊆ { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( { 𝑢 , 𝑣 } ⊆ 𝑊 ∧ ( 𝐻 Σg ( 𝑇 ∘ 𝑢 ) ) = ( 𝐻 Σg ( 𝑇 ∘ 𝑣 ) ) ) } )
170 169 ssbrd ⊢ ( 𝜑 → ( 𝐴 ∼ 𝐶 → 𝐴 { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( { 𝑢 , 𝑣 } ⊆ 𝑊 ∧ ( 𝐻 Σg ( 𝑇 ∘ 𝑢 ) ) = ( 𝐻 Σg ( 𝑇 ∘ 𝑣 ) ) ) } 𝐶 ) )
171 170 imp ⊢ ( ( 𝜑 ∧ 𝐴 ∼ 𝐶 ) → 𝐴 { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( { 𝑢 , 𝑣 } ⊆ 𝑊 ∧ ( 𝐻 Σg ( 𝑇 ∘ 𝑢 ) ) = ( 𝐻 Σg ( 𝑇 ∘ 𝑣 ) ) ) } 𝐶 )
172 7 8 efger ⊢ ∼ Er 𝑊
173 errel ⊢ ( ∼ Er 𝑊 → Rel ∼ )
174 172 173 mp1i ⊢ ( 𝜑 → Rel ∼ )
175 brrelex12 ⊢ ( ( Rel ∼ ∧ 𝐴 ∼ 𝐶 ) → ( 𝐴 ∈ V ∧ 𝐶 ∈ V ) )
176 174 175 sylan ⊢ ( ( 𝜑 ∧ 𝐴 ∼ 𝐶 ) → ( 𝐴 ∈ V ∧ 𝐶 ∈ V ) )
177 preq12 ⊢ ( ( 𝑢 = 𝐴 ∧ 𝑣 = 𝐶 ) → { 𝑢 , 𝑣 } = { 𝐴 , 𝐶 } )
178 177 sseq1d ⊢ ( ( 𝑢 = 𝐴 ∧ 𝑣 = 𝐶 ) → ( { 𝑢 , 𝑣 } ⊆ 𝑊 ↔ { 𝐴 , 𝐶 } ⊆ 𝑊 ) )
179 coeq2 ⊢ ( 𝑢 = 𝐴 → ( 𝑇 ∘ 𝑢 ) = ( 𝑇 ∘ 𝐴 ) )
180 179 oveq2d ⊢ ( 𝑢 = 𝐴 → ( 𝐻 Σg ( 𝑇 ∘ 𝑢 ) ) = ( 𝐻 Σg ( 𝑇 ∘ 𝐴 ) ) )
181 coeq2 ⊢ ( 𝑣 = 𝐶 → ( 𝑇 ∘ 𝑣 ) = ( 𝑇 ∘ 𝐶 ) )
182 181 oveq2d ⊢ ( 𝑣 = 𝐶 → ( 𝐻 Σg ( 𝑇 ∘ 𝑣 ) ) = ( 𝐻 Σg ( 𝑇 ∘ 𝐶 ) ) )
183 180 182 eqeqan12d ⊢ ( ( 𝑢 = 𝐴 ∧ 𝑣 = 𝐶 ) → ( ( 𝐻 Σg ( 𝑇 ∘ 𝑢 ) ) = ( 𝐻 Σg ( 𝑇 ∘ 𝑣 ) ) ↔ ( 𝐻 Σg ( 𝑇 ∘ 𝐴 ) ) = ( 𝐻 Σg ( 𝑇 ∘ 𝐶 ) ) ) )
184 178 183 anbi12d ⊢ ( ( 𝑢 = 𝐴 ∧ 𝑣 = 𝐶 ) → ( ( { 𝑢 , 𝑣 } ⊆ 𝑊 ∧ ( 𝐻 Σg ( 𝑇 ∘ 𝑢 ) ) = ( 𝐻 Σg ( 𝑇 ∘ 𝑣 ) ) ) ↔ ( { 𝐴 , 𝐶 } ⊆ 𝑊 ∧ ( 𝐻 Σg ( 𝑇 ∘ 𝐴 ) ) = ( 𝐻 Σg ( 𝑇 ∘ 𝐶 ) ) ) ) )
185 184 151 brabga ⊢ ( ( 𝐴 ∈ V ∧ 𝐶 ∈ V ) → ( 𝐴 { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( { 𝑢 , 𝑣 } ⊆ 𝑊 ∧ ( 𝐻 Σg ( 𝑇 ∘ 𝑢 ) ) = ( 𝐻 Σg ( 𝑇 ∘ 𝑣 ) ) ) } 𝐶 ↔ ( { 𝐴 , 𝐶 } ⊆ 𝑊 ∧ ( 𝐻 Σg ( 𝑇 ∘ 𝐴 ) ) = ( 𝐻 Σg ( 𝑇 ∘ 𝐶 ) ) ) ) )
186 176 185 syl ⊢ ( ( 𝜑 ∧ 𝐴 ∼ 𝐶 ) → ( 𝐴 { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( { 𝑢 , 𝑣 } ⊆ 𝑊 ∧ ( 𝐻 Σg ( 𝑇 ∘ 𝑢 ) ) = ( 𝐻 Σg ( 𝑇 ∘ 𝑣 ) ) ) } 𝐶 ↔ ( { 𝐴 , 𝐶 } ⊆ 𝑊 ∧ ( 𝐻 Σg ( 𝑇 ∘ 𝐴 ) ) = ( 𝐻 Σg ( 𝑇 ∘ 𝐶 ) ) ) ) )
187 171 186 mpbid ⊢ ( ( 𝜑 ∧ 𝐴 ∼ 𝐶 ) → ( { 𝐴 , 𝐶 } ⊆ 𝑊 ∧ ( 𝐻 Σg ( 𝑇 ∘ 𝐴 ) ) = ( 𝐻 Σg ( 𝑇 ∘ 𝐶 ) ) ) )
188 187 simprd ⊢ ( ( 𝜑 ∧ 𝐴 ∼ 𝐶 ) → ( 𝐻 Σg ( 𝑇 ∘ 𝐴 ) ) = ( 𝐻 Σg ( 𝑇 ∘ 𝐶 ) ) )