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	⊢ 𝑁 = ( inv_g ‘ 𝐻 )
	frgpup.t	⊢ 𝑇 = ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2_o ↦ if ( 𝑧 = ∅ , ( 𝐹 ‘ 𝑦 ) , ( 𝑁 ‘ ( 𝐹 ‘ 𝑦 ) ) ) )
	frgpup.h	⊢ ( 𝜑 → 𝐻 ∈ Grp )
	frgpup.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
	frgpup.a	⊢ ( 𝜑 → 𝐹 : 𝐼 ⟶ 𝐵 )
	frgpup.w	⊢ 𝑊 = ( I ‘ Word ( 𝐼 × 2_o ) )
	frgpup.r	⊢ ∼ = ( ~_FG ‘ 𝐼 )
Assertion	frgpuplem	⊢ ( ( 𝜑 ∧ 𝐴 ∼ 𝐶 ) → ( 𝐻 Σ_g ( 𝑇 ∘ 𝐴 ) ) = ( 𝐻 Σ_g ( 𝑇 ∘ 𝐶 ) ) )

Proof

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

Metamath Proof Explorer

Theorem frgpuplem

Proof