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	sselid	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑛 ∈ ( 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	56	grpmndd	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2_o ) ) → 𝐻 ∈ Mnd )
58		wrdco	⊢ ( ( ( 𝑥 prefix 𝑛 ) ∈ Word ( 𝐼 × 2_o ) ∧ 𝑇 : ( 𝐼 × 2_o ) ⟶ 𝐵 ) → ( 𝑇 ∘ ( 𝑥 prefix 𝑛 ) ) ∈ Word 𝐵 )
59	50 52 58	syl2anc	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2_o ) ) → ( 𝑇 ∘ ( 𝑥 prefix 𝑛 ) ) ∈ Word 𝐵 )
60		wrdco	⊢ ( ( ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ ”⟩ ∈ Word ( 𝐼 × 2_o ) ∧ 𝑇 : ( 𝐼 × 2_o ) ⟶ 𝐵 ) → ( 𝑇 ∘ ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ ”⟩ ) ∈ Word 𝐵 )
61	42 52 60	syl2anc	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2_o ) ) → ( 𝑇 ∘ ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ ”⟩ ) ∈ Word 𝐵 )
62		eqid	⊢ ( +_g ‘ 𝐻 ) = ( +_g ‘ 𝐻 )
63	1 62	gsumccat	⊢ ( ( 𝐻 ∈ Mnd ∧ ( 𝑇 ∘ ( 𝑥 prefix 𝑛 ) ) ∈ Word 𝐵 ∧ ( 𝑇 ∘ ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ ”⟩ ) ∈ Word 𝐵 ) → ( 𝐻 Σ_g ( ( 𝑇 ∘ ( 𝑥 prefix 𝑛 ) ) ++ ( 𝑇 ∘ ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ ”⟩ ) ) ) = ( ( 𝐻 Σ_g ( 𝑇 ∘ ( 𝑥 prefix 𝑛 ) ) ) ( +_g ‘ 𝐻 ) ( 𝐻 Σ_g ( 𝑇 ∘ ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ ”⟩ ) ) ) )
64	57 59 61 63	syl3anc	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2_o ) ) → ( 𝐻 Σ_g ( ( 𝑇 ∘ ( 𝑥 prefix 𝑛 ) ) ++ ( 𝑇 ∘ ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ ”⟩ ) ) ) = ( ( 𝐻 Σ_g ( 𝑇 ∘ ( 𝑥 prefix 𝑛 ) ) ) ( +_g ‘ 𝐻 ) ( 𝐻 Σ_g ( 𝑇 ∘ ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ ”⟩ ) ) ) )
65	52 37 41	s2co	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2_o ) ) → ( 𝑇 ∘ ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ ”⟩ ) = ⟨“ ( 𝑇 ‘ ⟨ 𝑎 , 𝑏 ⟩ ) ( 𝑇 ‘ ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ ) ”⟩ )
66		df-ov	⊢ ( 𝑎 𝑇 𝑏 ) = ( 𝑇 ‘ ⟨ 𝑎 , 𝑏 ⟩ )
67	66	a1i	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2_o ) ) → ( 𝑎 𝑇 𝑏 ) = ( 𝑇 ‘ ⟨ 𝑎 , 𝑏 ⟩ ) )
68	66	fveq2i	⊢ ( 𝑁 ‘ ( 𝑎 𝑇 𝑏 ) ) = ( 𝑁 ‘ ( 𝑇 ‘ ⟨ 𝑎 , 𝑏 ⟩ ) )
69		df-ov	⊢ ( 𝑎 ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2_o ↦ ⟨ 𝑦 , ( 1_o ∖ 𝑧 ) ⟩ ) 𝑏 ) = ( ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2_o ↦ ⟨ 𝑦 , ( 1_o ∖ 𝑧 ) ⟩ ) ‘ ⟨ 𝑎 , 𝑏 ⟩ )
70		eqid	⊢ ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2_o ↦ ⟨ 𝑦 , ( 1_o ∖ 𝑧 ) ⟩ ) = ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2_o ↦ ⟨ 𝑦 , ( 1_o ∖ 𝑧 ) ⟩ )
71	70	efgmval	⊢ ( ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2_o ) → ( 𝑎 ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2_o ↦ ⟨ 𝑦 , ( 1_o ∖ 𝑧 ) ⟩ ) 𝑏 ) = ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ )
72	69 71	eqtr3id	⊢ ( ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2_o ) → ( ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2_o ↦ ⟨ 𝑦 , ( 1_o ∖ 𝑧 ) ⟩ ) ‘ ⟨ 𝑎 , 𝑏 ⟩ ) = ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ )
73	72	adantl	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2_o ) ) → ( ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2_o ↦ ⟨ 𝑦 , ( 1_o ∖ 𝑧 ) ⟩ ) ‘ ⟨ 𝑎 , 𝑏 ⟩ ) = ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ )
74	73	fveq2d	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2_o ) ) → ( 𝑇 ‘ ( ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2_o ↦ ⟨ 𝑦 , ( 1_o ∖ 𝑧 ) ⟩ ) ‘ ⟨ 𝑎 , 𝑏 ⟩ ) ) = ( 𝑇 ‘ ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ ) )
75	1 2 3 4 5 6 70	frgpuptinv	⊢ ( ( 𝜑 ∧ ⟨ 𝑎 , 𝑏 ⟩ ∈ ( 𝐼 × 2_o ) ) → ( 𝑇 ‘ ( ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2_o ↦ ⟨ 𝑦 , ( 1_o ∖ 𝑧 ) ⟩ ) ‘ ⟨ 𝑎 , 𝑏 ⟩ ) ) = ( 𝑁 ‘ ( 𝑇 ‘ ⟨ 𝑎 , 𝑏 ⟩ ) ) )
76	36 75	sylan2	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2_o ) ) → ( 𝑇 ‘ ( ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2_o ↦ ⟨ 𝑦 , ( 1_o ∖ 𝑧 ) ⟩ ) ‘ ⟨ 𝑎 , 𝑏 ⟩ ) ) = ( 𝑁 ‘ ( 𝑇 ‘ ⟨ 𝑎 , 𝑏 ⟩ ) ) )
77	76	adantlr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2_o ) ) → ( 𝑇 ‘ ( ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2_o ↦ ⟨ 𝑦 , ( 1_o ∖ 𝑧 ) ⟩ ) ‘ ⟨ 𝑎 , 𝑏 ⟩ ) ) = ( 𝑁 ‘ ( 𝑇 ‘ ⟨ 𝑎 , 𝑏 ⟩ ) ) )
78	74 77	eqtr3d	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2_o ) ) → ( 𝑇 ‘ ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ ) = ( 𝑁 ‘ ( 𝑇 ‘ ⟨ 𝑎 , 𝑏 ⟩ ) ) )
79	68 78	eqtr4id	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2_o ) ) → ( 𝑁 ‘ ( 𝑎 𝑇 𝑏 ) ) = ( 𝑇 ‘ ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ ) )
80	67 79	s2eqd	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2_o ) ) → ⟨“ ( 𝑎 𝑇 𝑏 ) ( 𝑁 ‘ ( 𝑎 𝑇 𝑏 ) ) ”⟩ = ⟨“ ( 𝑇 ‘ ⟨ 𝑎 , 𝑏 ⟩ ) ( 𝑇 ‘ ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ ) ”⟩ )
81	65 80	eqtr4d	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2_o ) ) → ( 𝑇 ∘ ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ ”⟩ ) = ⟨“ ( 𝑎 𝑇 𝑏 ) ( 𝑁 ‘ ( 𝑎 𝑇 𝑏 ) ) ”⟩ )
82	81	oveq2d	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2_o ) ) → ( 𝐻 Σ_g ( 𝑇 ∘ ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ ”⟩ ) ) = ( 𝐻 Σ_g ⟨“ ( 𝑎 𝑇 𝑏 ) ( 𝑁 ‘ ( 𝑎 𝑇 𝑏 ) ) ”⟩ ) )
83		simprr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2_o ) ) → 𝑏 ∈ 2_o )
84	52 38 83	fovrnd	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2_o ) ) → ( 𝑎 𝑇 𝑏 ) ∈ 𝐵 )
85	1 2	grpinvcl	⊢ ( ( 𝐻 ∈ Grp ∧ ( 𝑎 𝑇 𝑏 ) ∈ 𝐵 ) → ( 𝑁 ‘ ( 𝑎 𝑇 𝑏 ) ) ∈ 𝐵 )
86	56 84 85	syl2anc	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2_o ) ) → ( 𝑁 ‘ ( 𝑎 𝑇 𝑏 ) ) ∈ 𝐵 )
87	1 62	gsumws2	⊢ ( ( 𝐻 ∈ Mnd ∧ ( 𝑎 𝑇 𝑏 ) ∈ 𝐵 ∧ ( 𝑁 ‘ ( 𝑎 𝑇 𝑏 ) ) ∈ 𝐵 ) → ( 𝐻 Σ_g ⟨“ ( 𝑎 𝑇 𝑏 ) ( 𝑁 ‘ ( 𝑎 𝑇 𝑏 ) ) ”⟩ ) = ( ( 𝑎 𝑇 𝑏 ) ( +_g ‘ 𝐻 ) ( 𝑁 ‘ ( 𝑎 𝑇 𝑏 ) ) ) )
88	57 84 86 87	syl3anc	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2_o ) ) → ( 𝐻 Σ_g ⟨“ ( 𝑎 𝑇 𝑏 ) ( 𝑁 ‘ ( 𝑎 𝑇 𝑏 ) ) ”⟩ ) = ( ( 𝑎 𝑇 𝑏 ) ( +_g ‘ 𝐻 ) ( 𝑁 ‘ ( 𝑎 𝑇 𝑏 ) ) ) )
89		eqid	⊢ ( 0_g ‘ 𝐻 ) = ( 0_g ‘ 𝐻 )
90	1 62 89 2	grprinv	⊢ ( ( 𝐻 ∈ Grp ∧ ( 𝑎 𝑇 𝑏 ) ∈ 𝐵 ) → ( ( 𝑎 𝑇 𝑏 ) ( +_g ‘ 𝐻 ) ( 𝑁 ‘ ( 𝑎 𝑇 𝑏 ) ) ) = ( 0_g ‘ 𝐻 ) )
91	56 84 90	syl2anc	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2_o ) ) → ( ( 𝑎 𝑇 𝑏 ) ( +_g ‘ 𝐻 ) ( 𝑁 ‘ ( 𝑎 𝑇 𝑏 ) ) ) = ( 0_g ‘ 𝐻 ) )
92	82 88 91	3eqtrd	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2_o ) ) → ( 𝐻 Σ_g ( 𝑇 ∘ ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ ”⟩ ) ) = ( 0_g ‘ 𝐻 ) )
93	92	oveq2d	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2_o ) ) → ( ( 𝐻 Σ_g ( 𝑇 ∘ ( 𝑥 prefix 𝑛 ) ) ) ( +_g ‘ 𝐻 ) ( 𝐻 Σ_g ( 𝑇 ∘ ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ ”⟩ ) ) ) = ( ( 𝐻 Σ_g ( 𝑇 ∘ ( 𝑥 prefix 𝑛 ) ) ) ( +_g ‘ 𝐻 ) ( 0_g ‘ 𝐻 ) ) )
94	1	gsumwcl	⊢ ( ( 𝐻 ∈ Mnd ∧ ( 𝑇 ∘ ( 𝑥 prefix 𝑛 ) ) ∈ Word 𝐵 ) → ( 𝐻 Σ_g ( 𝑇 ∘ ( 𝑥 prefix 𝑛 ) ) ) ∈ 𝐵 )
95	57 59 94	syl2anc	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2_o ) ) → ( 𝐻 Σ_g ( 𝑇 ∘ ( 𝑥 prefix 𝑛 ) ) ) ∈ 𝐵 )
96	1 62 89	grprid	⊢ ( ( 𝐻 ∈ Grp ∧ ( 𝐻 Σ_g ( 𝑇 ∘ ( 𝑥 prefix 𝑛 ) ) ) ∈ 𝐵 ) → ( ( 𝐻 Σ_g ( 𝑇 ∘ ( 𝑥 prefix 𝑛 ) ) ) ( +_g ‘ 𝐻 ) ( 0_g ‘ 𝐻 ) ) = ( 𝐻 Σ_g ( 𝑇 ∘ ( 𝑥 prefix 𝑛 ) ) ) )
97	56 95 96	syl2anc	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2_o ) ) → ( ( 𝐻 Σ_g ( 𝑇 ∘ ( 𝑥 prefix 𝑛 ) ) ) ( +_g ‘ 𝐻 ) ( 0_g ‘ 𝐻 ) ) = ( 𝐻 Σ_g ( 𝑇 ∘ ( 𝑥 prefix 𝑛 ) ) ) )
98	93 97	eqtrd	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2_o ) ) → ( ( 𝐻 Σ_g ( 𝑇 ∘ ( 𝑥 prefix 𝑛 ) ) ) ( +_g ‘ 𝐻 ) ( 𝐻 Σ_g ( 𝑇 ∘ ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ ”⟩ ) ) ) = ( 𝐻 Σ_g ( 𝑇 ∘ ( 𝑥 prefix 𝑛 ) ) ) )
99	55 64 98	3eqtrrd	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2_o ) ) → ( 𝐻 Σ_g ( 𝑇 ∘ ( 𝑥 prefix 𝑛 ) ) ) = ( 𝐻 Σ_g ( 𝑇 ∘ ( ( 𝑥 prefix 𝑛 ) ++ ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ ”⟩ ) ) ) )
100	99	oveq1d	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2_o ) ) → ( ( 𝐻 Σ_g ( 𝑇 ∘ ( 𝑥 prefix 𝑛 ) ) ) ( +_g ‘ 𝐻 ) ( 𝐻 Σ_g ( 𝑇 ∘ ( 𝑥 substr ⟨ 𝑛 , ( ♯ ‘ 𝑥 ) ⟩ ) ) ) ) = ( ( 𝐻 Σ_g ( 𝑇 ∘ ( ( 𝑥 prefix 𝑛 ) ++ ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ ”⟩ ) ) ) ( +_g ‘ 𝐻 ) ( 𝐻 Σ_g ( 𝑇 ∘ ( 𝑥 substr ⟨ 𝑛 , ( ♯ ‘ 𝑥 ) ⟩ ) ) ) ) )
101		swrdcl	⊢ ( 𝑥 ∈ Word ( 𝐼 × 2_o ) → ( 𝑥 substr ⟨ 𝑛 , ( ♯ ‘ 𝑥 ) ⟩ ) ∈ Word ( 𝐼 × 2_o ) )
102	35 101	syl	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2_o ) ) → ( 𝑥 substr ⟨ 𝑛 , ( ♯ ‘ 𝑥 ) ⟩ ) ∈ Word ( 𝐼 × 2_o ) )
103		wrdco	⊢ ( ( ( 𝑥 substr ⟨ 𝑛 , ( ♯ ‘ 𝑥 ) ⟩ ) ∈ Word ( 𝐼 × 2_o ) ∧ 𝑇 : ( 𝐼 × 2_o ) ⟶ 𝐵 ) → ( 𝑇 ∘ ( 𝑥 substr ⟨ 𝑛 , ( ♯ ‘ 𝑥 ) ⟩ ) ) ∈ Word 𝐵 )
104	102 52 103	syl2anc	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2_o ) ) → ( 𝑇 ∘ ( 𝑥 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 ... ( ♯ ‘ 𝑥 ) ) ) ) ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2_o ) ) → ( 𝐻 Σ_g ( ( 𝑇 ∘ ( 𝑥 prefix 𝑛 ) ) ++ ( 𝑇 ∘ ( 𝑥 substr ⟨ 𝑛 , ( ♯ ‘ 𝑥 ) ⟩ ) ) ) ) = ( ( 𝐻 Σ_g ( 𝑇 ∘ ( 𝑥 prefix 𝑛 ) ) ) ( +_g ‘ 𝐻 ) ( 𝐻 Σ_g ( 𝑇 ∘ ( 𝑥 substr ⟨ 𝑛 , ( ♯ ‘ 𝑥 ) ⟩ ) ) ) ) )
107		ccatcl	⊢ ( ( ( 𝑥 prefix 𝑛 ) ∈ Word ( 𝐼 × 2_o ) ∧ ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ ”⟩ ∈ Word ( 𝐼 × 2_o ) ) → ( ( 𝑥 prefix 𝑛 ) ++ ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ ”⟩ ) ∈ Word ( 𝐼 × 2_o ) )
108	50 42 107	syl2anc	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2_o ) ) → ( ( 𝑥 prefix 𝑛 ) ++ ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ ”⟩ ) ∈ Word ( 𝐼 × 2_o ) )
109		wrdco	⊢ ( ( ( ( 𝑥 prefix 𝑛 ) ++ ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ ”⟩ ) ∈ Word ( 𝐼 × 2_o ) ∧ 𝑇 : ( 𝐼 × 2_o ) ⟶ 𝐵 ) → ( 𝑇 ∘ ( ( 𝑥 prefix 𝑛 ) ++ ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ ”⟩ ) ) ∈ Word 𝐵 )
110	108 52 109	syl2anc	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2_o ) ) → ( 𝑇 ∘ ( ( 𝑥 prefix 𝑛 ) ++ ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ ”⟩ ) ) ∈ Word 𝐵 )
111	1 62	gsumccat	⊢ ( ( 𝐻 ∈ Mnd ∧ ( 𝑇 ∘ ( ( 𝑥 prefix 𝑛 ) ++ ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ ”⟩ ) ) ∈ Word 𝐵 ∧ ( 𝑇 ∘ ( 𝑥 substr ⟨ 𝑛 , ( ♯ ‘ 𝑥 ) ⟩ ) ) ∈ Word 𝐵 ) → ( 𝐻 Σ_g ( ( 𝑇 ∘ ( ( 𝑥 prefix 𝑛 ) ++ ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ ”⟩ ) ) ++ ( 𝑇 ∘ ( 𝑥 substr ⟨ 𝑛 , ( ♯ ‘ 𝑥 ) ⟩ ) ) ) ) = ( ( 𝐻 Σ_g ( 𝑇 ∘ ( ( 𝑥 prefix 𝑛 ) ++ ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ ”⟩ ) ) ) ( +_g ‘ 𝐻 ) ( 𝐻 Σ_g ( 𝑇 ∘ ( 𝑥 substr ⟨ 𝑛 , ( ♯ ‘ 𝑥 ) ⟩ ) ) ) ) )
112	57 110 104 111	syl3anc	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2_o ) ) → ( 𝐻 Σ_g ( ( 𝑇 ∘ ( ( 𝑥 prefix 𝑛 ) ++ ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ ”⟩ ) ) ++ ( 𝑇 ∘ ( 𝑥 substr ⟨ 𝑛 , ( ♯ ‘ 𝑥 ) ⟩ ) ) ) ) = ( ( 𝐻 Σ_g ( 𝑇 ∘ ( ( 𝑥 prefix 𝑛 ) ++ ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ ”⟩ ) ) ) ( +_g ‘ 𝐻 ) ( 𝐻 Σ_g ( 𝑇 ∘ ( 𝑥 substr ⟨ 𝑛 , ( ♯ ‘ 𝑥 ) ⟩ ) ) ) ) )
113	100 106 112	3eqtr4d	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2_o ) ) → ( 𝐻 Σ_g ( ( 𝑇 ∘ ( 𝑥 prefix 𝑛 ) ) ++ ( 𝑇 ∘ ( 𝑥 substr ⟨ 𝑛 , ( ♯ ‘ 𝑥 ) ⟩ ) ) ) ) = ( 𝐻 Σ_g ( ( 𝑇 ∘ ( ( 𝑥 prefix 𝑛 ) ++ ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ ”⟩ ) ) ++ ( 𝑇 ∘ ( 𝑥 substr ⟨ 𝑛 , ( ♯ ‘ 𝑥 ) ⟩ ) ) ) ) )
114		simplrr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2_o ) ) → 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) )
115		lencl	⊢ ( 𝑥 ∈ Word ( 𝐼 × 2_o ) → ( ♯ ‘ 𝑥 ) ∈ ℕ₀ )
116	35 115	syl	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2_o ) ) → ( ♯ ‘ 𝑥 ) ∈ ℕ₀ )
117		nn0uz	⊢ ℕ₀ = ( ℤ_≥ ‘ 0 )
118	116 117	eleqtrdi	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2_o ) ) → ( ♯ ‘ 𝑥 ) ∈ ( ℤ_≥ ‘ 0 ) )
119		eluzfz2	⊢ ( ( ♯ ‘ 𝑥 ) ∈ ( ℤ_≥ ‘ 0 ) → ( ♯ ‘ 𝑥 ) ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) )
120	118 119	syl	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2_o ) ) → ( ♯ ‘ 𝑥 ) ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) )
121		ccatpfx	⊢ ( ( 𝑥 ∈ Word ( 𝐼 × 2_o ) ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ∧ ( ♯ ‘ 𝑥 ) ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) → ( ( 𝑥 prefix 𝑛 ) ++ ( 𝑥 substr ⟨ 𝑛 , ( ♯ ‘ 𝑥 ) ⟩ ) ) = ( 𝑥 prefix ( ♯ ‘ 𝑥 ) ) )
122	35 114 120 121	syl3anc	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2_o ) ) → ( ( 𝑥 prefix 𝑛 ) ++ ( 𝑥 substr ⟨ 𝑛 , ( ♯ ‘ 𝑥 ) ⟩ ) ) = ( 𝑥 prefix ( ♯ ‘ 𝑥 ) ) )
123		pfxid	⊢ ( 𝑥 ∈ Word ( 𝐼 × 2_o ) → ( 𝑥 prefix ( ♯ ‘ 𝑥 ) ) = 𝑥 )
124	35 123	syl	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2_o ) ) → ( 𝑥 prefix ( ♯ ‘ 𝑥 ) ) = 𝑥 )
125	122 124	eqtrd	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2_o ) ) → ( ( 𝑥 prefix 𝑛 ) ++ ( 𝑥 substr ⟨ 𝑛 , ( ♯ ‘ 𝑥 ) ⟩ ) ) = 𝑥 )
126	125	coeq2d	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2_o ) ) → ( 𝑇 ∘ ( ( 𝑥 prefix 𝑛 ) ++ ( 𝑥 substr ⟨ 𝑛 , ( ♯ ‘ 𝑥 ) ⟩ ) ) ) = ( 𝑇 ∘ 𝑥 ) )
127		ccatco	⊢ ( ( ( 𝑥 prefix 𝑛 ) ∈ Word ( 𝐼 × 2_o ) ∧ ( 𝑥 substr ⟨ 𝑛 , ( ♯ ‘ 𝑥 ) ⟩ ) ∈ Word ( 𝐼 × 2_o ) ∧ 𝑇 : ( 𝐼 × 2_o ) ⟶ 𝐵 ) → ( 𝑇 ∘ ( ( 𝑥 prefix 𝑛 ) ++ ( 𝑥 substr ⟨ 𝑛 , ( ♯ ‘ 𝑥 ) ⟩ ) ) ) = ( ( 𝑇 ∘ ( 𝑥 prefix 𝑛 ) ) ++ ( 𝑇 ∘ ( 𝑥 substr ⟨ 𝑛 , ( ♯ ‘ 𝑥 ) ⟩ ) ) ) )
128	50 102 52 127	syl3anc	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2_o ) ) → ( 𝑇 ∘ ( ( 𝑥 prefix 𝑛 ) ++ ( 𝑥 substr ⟨ 𝑛 , ( ♯ ‘ 𝑥 ) ⟩ ) ) ) = ( ( 𝑇 ∘ ( 𝑥 prefix 𝑛 ) ) ++ ( 𝑇 ∘ ( 𝑥 substr ⟨ 𝑛 , ( ♯ ‘ 𝑥 ) ⟩ ) ) ) )
129	126 128	eqtr3d	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2_o ) ) → ( 𝑇 ∘ 𝑥 ) = ( ( 𝑇 ∘ ( 𝑥 prefix 𝑛 ) ) ++ ( 𝑇 ∘ ( 𝑥 substr ⟨ 𝑛 , ( ♯ ‘ 𝑥 ) ⟩ ) ) ) )
130	129	oveq2d	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2_o ) ) → ( 𝐻 Σ_g ( 𝑇 ∘ 𝑥 ) ) = ( 𝐻 Σ_g ( ( 𝑇 ∘ ( 𝑥 prefix 𝑛 ) ) ++ ( 𝑇 ∘ ( 𝑥 substr ⟨ 𝑛 , ( ♯ ‘ 𝑥 ) ⟩ ) ) ) ) )
131		splval	⊢ ( ( 𝑥 ∈ 𝑊 ∧ ( 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ∧ ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ ”⟩ ∈ Word ( 𝐼 × 2_o ) ) ) → ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ ”⟩ ⟩ ) = ( ( ( 𝑥 prefix 𝑛 ) ++ ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ ”⟩ ) ++ ( 𝑥 substr ⟨ 𝑛 , ( ♯ ‘ 𝑥 ) ⟩ ) ) )
132	32 114 114 42 131	syl13anc	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2_o ) ) → ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ ”⟩ ⟩ ) = ( ( ( 𝑥 prefix 𝑛 ) ++ ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ ”⟩ ) ++ ( 𝑥 substr ⟨ 𝑛 , ( ♯ ‘ 𝑥 ) ⟩ ) ) )
133	132	coeq2d	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2_o ) ) → ( 𝑇 ∘ ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ ”⟩ ⟩ ) ) = ( 𝑇 ∘ ( ( ( 𝑥 prefix 𝑛 ) ++ ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ ”⟩ ) ++ ( 𝑥 substr ⟨ 𝑛 , ( ♯ ‘ 𝑥 ) ⟩ ) ) ) )
134		ccatco	⊢ ( ( ( ( 𝑥 prefix 𝑛 ) ++ ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ ”⟩ ) ∈ Word ( 𝐼 × 2_o ) ∧ ( 𝑥 substr ⟨ 𝑛 , ( ♯ ‘ 𝑥 ) ⟩ ) ∈ Word ( 𝐼 × 2_o ) ∧ 𝑇 : ( 𝐼 × 2_o ) ⟶ 𝐵 ) → ( 𝑇 ∘ ( ( ( 𝑥 prefix 𝑛 ) ++ ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ ”⟩ ) ++ ( 𝑥 substr ⟨ 𝑛 , ( ♯ ‘ 𝑥 ) ⟩ ) ) ) = ( ( 𝑇 ∘ ( ( 𝑥 prefix 𝑛 ) ++ ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ ”⟩ ) ) ++ ( 𝑇 ∘ ( 𝑥 substr ⟨ 𝑛 , ( ♯ ‘ 𝑥 ) ⟩ ) ) ) )
135	108 102 52 134	syl3anc	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2_o ) ) → ( 𝑇 ∘ ( ( ( 𝑥 prefix 𝑛 ) ++ ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ ”⟩ ) ++ ( 𝑥 substr ⟨ 𝑛 , ( ♯ ‘ 𝑥 ) ⟩ ) ) ) = ( ( 𝑇 ∘ ( ( 𝑥 prefix 𝑛 ) ++ ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ ”⟩ ) ) ++ ( 𝑇 ∘ ( 𝑥 substr ⟨ 𝑛 , ( ♯ ‘ 𝑥 ) ⟩ ) ) ) )
136	133 135	eqtrd	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2_o ) ) → ( 𝑇 ∘ ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ ”⟩ ⟩ ) ) = ( ( 𝑇 ∘ ( ( 𝑥 prefix 𝑛 ) ++ ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ ”⟩ ) ) ++ ( 𝑇 ∘ ( 𝑥 substr ⟨ 𝑛 , ( ♯ ‘ 𝑥 ) ⟩ ) ) ) )
137	136	oveq2d	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2_o ) ) → ( 𝐻 Σ_g ( 𝑇 ∘ ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ ”⟩ ⟩ ) ) ) = ( 𝐻 Σ_g ( ( 𝑇 ∘ ( ( 𝑥 prefix 𝑛 ) ++ ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ ”⟩ ) ) ++ ( 𝑇 ∘ ( 𝑥 substr ⟨ 𝑛 , ( ♯ ‘ 𝑥 ) ⟩ ) ) ) ) )
138	113 130 137	3eqtr4d	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2_o ) ) → ( 𝐻 Σ_g ( 𝑇 ∘ 𝑥 ) ) = ( 𝐻 Σ_g ( 𝑇 ∘ ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ ”⟩ ⟩ ) ) ) )
139		vex	⊢ 𝑥 ∈ V
140		ovex	⊢ ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ ”⟩ ⟩ ) ∈ V
141		eleq1	⊢ ( 𝑢 = 𝑥 → ( 𝑢 ∈ 𝑊 ↔ 𝑥 ∈ 𝑊 ) )
142		eleq1	⊢ ( 𝑣 = ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ ”⟩ ⟩ ) → ( 𝑣 ∈ 𝑊 ↔ ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ ”⟩ ⟩ ) ∈ 𝑊 ) )
143	141 142	bi2anan9	⊢ ( ( 𝑢 = 𝑥 ∧ 𝑣 = ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ ”⟩ ⟩ ) ) → ( ( 𝑢 ∈ 𝑊 ∧ 𝑣 ∈ 𝑊 ) ↔ ( 𝑥 ∈ 𝑊 ∧ ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ ”⟩ ⟩ ) ∈ 𝑊 ) ) )
144	25 143	bitr3id	⊢ ( ( 𝑢 = 𝑥 ∧ 𝑣 = ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ ”⟩ ⟩ ) ) → ( { 𝑢 , 𝑣 } ⊆ 𝑊 ↔ ( 𝑥 ∈ 𝑊 ∧ ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ ”⟩ ⟩ ) ∈ 𝑊 ) ) )
145		coeq2	⊢ ( 𝑢 = 𝑥 → ( 𝑇 ∘ 𝑢 ) = ( 𝑇 ∘ 𝑥 ) )
146	145	oveq2d	⊢ ( 𝑢 = 𝑥 → ( 𝐻 Σ_g ( 𝑇 ∘ 𝑢 ) ) = ( 𝐻 Σ_g ( 𝑇 ∘ 𝑥 ) ) )
147		coeq2	⊢ ( 𝑣 = ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ ”⟩ ⟩ ) → ( 𝑇 ∘ 𝑣 ) = ( 𝑇 ∘ ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ ”⟩ ⟩ ) ) )
148	147	oveq2d	⊢ ( 𝑣 = ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ ”⟩ ⟩ ) → ( 𝐻 Σ_g ( 𝑇 ∘ 𝑣 ) ) = ( 𝐻 Σ_g ( 𝑇 ∘ ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ ”⟩ ⟩ ) ) ) )
149	146 148	eqeqan12d	⊢ ( ( 𝑢 = 𝑥 ∧ 𝑣 = ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ ”⟩ ⟩ ) ) → ( ( 𝐻 Σ_g ( 𝑇 ∘ 𝑢 ) ) = ( 𝐻 Σ_g ( 𝑇 ∘ 𝑣 ) ) ↔ ( 𝐻 Σ_g ( 𝑇 ∘ 𝑥 ) ) = ( 𝐻 Σ_g ( 𝑇 ∘ ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ ”⟩ ⟩ ) ) ) ) )
150	144 149	anbi12d	⊢ ( ( 𝑢 = 𝑥 ∧ 𝑣 = ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ ”⟩ ⟩ ) ) → ( ( { 𝑢 , 𝑣 } ⊆ 𝑊 ∧ ( 𝐻 Σ_g ( 𝑇 ∘ 𝑢 ) ) = ( 𝐻 Σ_g ( 𝑇 ∘ 𝑣 ) ) ) ↔ ( ( 𝑥 ∈ 𝑊 ∧ ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ ”⟩ ⟩ ) ∈ 𝑊 ) ∧ ( 𝐻 Σ_g ( 𝑇 ∘ 𝑥 ) ) = ( 𝐻 Σ_g ( 𝑇 ∘ ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ ”⟩ ⟩ ) ) ) ) ) )
151		eqid	⊢ { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( { 𝑢 , 𝑣 } ⊆ 𝑊 ∧ ( 𝐻 Σ_g ( 𝑇 ∘ 𝑢 ) ) = ( 𝐻 Σ_g ( 𝑇 ∘ 𝑣 ) ) ) } = { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( { 𝑢 , 𝑣 } ⊆ 𝑊 ∧ ( 𝐻 Σ_g ( 𝑇 ∘ 𝑢 ) ) = ( 𝐻 Σ_g ( 𝑇 ∘ 𝑣 ) ) ) }
152	139 140 150 151	braba	⊢ ( 𝑥 { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( { 𝑢 , 𝑣 } ⊆ 𝑊 ∧ ( 𝐻 Σ_g ( 𝑇 ∘ 𝑢 ) ) = ( 𝐻 Σ_g ( 𝑇 ∘ 𝑣 ) ) ) } ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ ”⟩ ⟩ ) ↔ ( ( 𝑥 ∈ 𝑊 ∧ ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ ”⟩ ⟩ ) ∈ 𝑊 ) ∧ ( 𝐻 Σ_g ( 𝑇 ∘ 𝑥 ) ) = ( 𝐻 Σ_g ( 𝑇 ∘ ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ ”⟩ ⟩ ) ) ) ) )
153	32 48 138 152	syl21anbrc	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2_o ) ) → 𝑥 { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( { 𝑢 , 𝑣 } ⊆ 𝑊 ∧ ( 𝐻 Σ_g ( 𝑇 ∘ 𝑢 ) ) = ( 𝐻 Σ_g ( 𝑇 ∘ 𝑣 ) ) ) } ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ ”⟩ ⟩ ) )
154	153	ralrimivva	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) → ∀ 𝑎 ∈ 𝐼 ∀ 𝑏 ∈ 2_o 𝑥 { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( { 𝑢 , 𝑣 } ⊆ 𝑊 ∧ ( 𝐻 Σ_g ( 𝑇 ∘ 𝑢 ) ) = ( 𝐻 Σ_g ( 𝑇 ∘ 𝑣 ) ) ) } ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ ”⟩ ⟩ ) )
155	154	ralrimivva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑊 ∀ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ∀ 𝑎 ∈ 𝐼 ∀ 𝑏 ∈ 2_o 𝑥 { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( { 𝑢 , 𝑣 } ⊆ 𝑊 ∧ ( 𝐻 Σ_g ( 𝑇 ∘ 𝑢 ) ) = ( 𝐻 Σ_g ( 𝑇 ∘ 𝑣 ) ) ) } ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ ”⟩ ⟩ ) )
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 ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ ”⟩ ⟩ ) ↔ 𝑥 { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( { 𝑢 , 𝑣 } ⊆ 𝑊 ∧ ( 𝐻 Σ_g ( 𝑇 ∘ 𝑢 ) ) = ( 𝐻 Σ_g ( 𝑇 ∘ 𝑣 ) ) ) } ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ ”⟩ ⟩ ) ) )
161	160	2ralbidv	⊢ ( 𝑟 = { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( { 𝑢 , 𝑣 } ⊆ 𝑊 ∧ ( 𝐻 Σ_g ( 𝑇 ∘ 𝑢 ) ) = ( 𝐻 Σ_g ( 𝑇 ∘ 𝑣 ) ) ) } → ( ∀ 𝑎 ∈ 𝐼 ∀ 𝑏 ∈ 2_o 𝑥 𝑟 ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ ”⟩ ⟩ ) ↔ ∀ 𝑎 ∈ 𝐼 ∀ 𝑏 ∈ 2_o 𝑥 { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( { 𝑢 , 𝑣 } ⊆ 𝑊 ∧ ( 𝐻 Σ_g ( 𝑇 ∘ 𝑢 ) ) = ( 𝐻 Σ_g ( 𝑇 ∘ 𝑣 ) ) ) } ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ ”⟩ ⟩ ) ) )
162	161	2ralbidv	⊢ ( 𝑟 = { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( { 𝑢 , 𝑣 } ⊆ 𝑊 ∧ ( 𝐻 Σ_g ( 𝑇 ∘ 𝑢 ) ) = ( 𝐻 Σ_g ( 𝑇 ∘ 𝑣 ) ) ) } → ( ∀ 𝑥 ∈ 𝑊 ∀ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ∀ 𝑎 ∈ 𝐼 ∀ 𝑏 ∈ 2_o 𝑥 𝑟 ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ ”⟩ ⟩ ) ↔ ∀ 𝑥 ∈ 𝑊 ∀ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ∀ 𝑎 ∈ 𝐼 ∀ 𝑏 ∈ 2_o 𝑥 { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( { 𝑢 , 𝑣 } ⊆ 𝑊 ∧ ( 𝐻 Σ_g ( 𝑇 ∘ 𝑢 ) ) = ( 𝐻 Σ_g ( 𝑇 ∘ 𝑣 ) ) ) } ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ ”⟩ ⟩ ) ) )
163	159 162	anbi12d	⊢ ( 𝑟 = { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( { 𝑢 , 𝑣 } ⊆ 𝑊 ∧ ( 𝐻 Σ_g ( 𝑇 ∘ 𝑢 ) ) = ( 𝐻 Σ_g ( 𝑇 ∘ 𝑣 ) ) ) } → ( ( 𝑟 Er 𝑊 ∧ ∀ 𝑥 ∈ 𝑊 ∀ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ∀ 𝑎 ∈ 𝐼 ∀ 𝑏 ∈ 2_o 𝑥 𝑟 ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ ”⟩ ⟩ ) ) ↔ ( { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( { 𝑢 , 𝑣 } ⊆ 𝑊 ∧ ( 𝐻 Σ_g ( 𝑇 ∘ 𝑢 ) ) = ( 𝐻 Σ_g ( 𝑇 ∘ 𝑣 ) ) ) } Er 𝑊 ∧ ∀ 𝑥 ∈ 𝑊 ∀ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ∀ 𝑎 ∈ 𝐼 ∀ 𝑏 ∈ 2_o 𝑥 { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( { 𝑢 , 𝑣 } ⊆ 𝑊 ∧ ( 𝐻 Σ_g ( 𝑇 ∘ 𝑢 ) ) = ( 𝐻 Σ_g ( 𝑇 ∘ 𝑣 ) ) ) } ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ ”⟩ ⟩ ) ) ) )
164	163	elabg	⊢ ( { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( { 𝑢 , 𝑣 } ⊆ 𝑊 ∧ ( 𝐻 Σ_g ( 𝑇 ∘ 𝑢 ) ) = ( 𝐻 Σ_g ( 𝑇 ∘ 𝑣 ) ) ) } ∈ V → ( { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( { 𝑢 , 𝑣 } ⊆ 𝑊 ∧ ( 𝐻 Σ_g ( 𝑇 ∘ 𝑢 ) ) = ( 𝐻 Σ_g ( 𝑇 ∘ 𝑣 ) ) ) } ∈ { 𝑟 ∣ ( 𝑟 Er 𝑊 ∧ ∀ 𝑥 ∈ 𝑊 ∀ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ∀ 𝑎 ∈ 𝐼 ∀ 𝑏 ∈ 2_o 𝑥 𝑟 ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ ”⟩ ⟩ ) ) } ↔ ( { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( { 𝑢 , 𝑣 } ⊆ 𝑊 ∧ ( 𝐻 Σ_g ( 𝑇 ∘ 𝑢 ) ) = ( 𝐻 Σ_g ( 𝑇 ∘ 𝑣 ) ) ) } Er 𝑊 ∧ ∀ 𝑥 ∈ 𝑊 ∀ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ∀ 𝑎 ∈ 𝐼 ∀ 𝑏 ∈ 2_o 𝑥 { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( { 𝑢 , 𝑣 } ⊆ 𝑊 ∧ ( 𝐻 Σ_g ( 𝑇 ∘ 𝑢 ) ) = ( 𝐻 Σ_g ( 𝑇 ∘ 𝑣 ) ) ) } ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ ”⟩ ⟩ ) ) ) )
165	158 164	syl	⊢ ( 𝜑 → ( { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( { 𝑢 , 𝑣 } ⊆ 𝑊 ∧ ( 𝐻 Σ_g ( 𝑇 ∘ 𝑢 ) ) = ( 𝐻 Σ_g ( 𝑇 ∘ 𝑣 ) ) ) } ∈ { 𝑟 ∣ ( 𝑟 Er 𝑊 ∧ ∀ 𝑥 ∈ 𝑊 ∀ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ∀ 𝑎 ∈ 𝐼 ∀ 𝑏 ∈ 2_o 𝑥 𝑟 ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ ”⟩ ⟩ ) ) } ↔ ( { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( { 𝑢 , 𝑣 } ⊆ 𝑊 ∧ ( 𝐻 Σ_g ( 𝑇 ∘ 𝑢 ) ) = ( 𝐻 Σ_g ( 𝑇 ∘ 𝑣 ) ) ) } Er 𝑊 ∧ ∀ 𝑥 ∈ 𝑊 ∀ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ∀ 𝑎 ∈ 𝐼 ∀ 𝑏 ∈ 2_o 𝑥 { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( { 𝑢 , 𝑣 } ⊆ 𝑊 ∧ ( 𝐻 Σ_g ( 𝑇 ∘ 𝑢 ) ) = ( 𝐻 Σ_g ( 𝑇 ∘ 𝑣 ) ) ) } ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ ”⟩ ⟩ ) ) ) )
166	31 155 165	mpbir2and	⊢ ( 𝜑 → { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( { 𝑢 , 𝑣 } ⊆ 𝑊 ∧ ( 𝐻 Σ_g ( 𝑇 ∘ 𝑢 ) ) = ( 𝐻 Σ_g ( 𝑇 ∘ 𝑣 ) ) ) } ∈ { 𝑟 ∣ ( 𝑟 Er 𝑊 ∧ ∀ 𝑥 ∈ 𝑊 ∀ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ∀ 𝑎 ∈ 𝐼 ∀ 𝑏 ∈ 2_o 𝑥 𝑟 ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ ”⟩ ⟩ ) ) } )
167		intss1	⊢ ( { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( { 𝑢 , 𝑣 } ⊆ 𝑊 ∧ ( 𝐻 Σ_g ( 𝑇 ∘ 𝑢 ) ) = ( 𝐻 Σ_g ( 𝑇 ∘ 𝑣 ) ) ) } ∈ { 𝑟 ∣ ( 𝑟 Er 𝑊 ∧ ∀ 𝑥 ∈ 𝑊 ∀ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ∀ 𝑎 ∈ 𝐼 ∀ 𝑏 ∈ 2_o 𝑥 𝑟 ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ ”⟩ ⟩ ) ) } → ∩ { 𝑟 ∣ ( 𝑟 Er 𝑊 ∧ ∀ 𝑥 ∈ 𝑊 ∀ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ∀ 𝑎 ∈ 𝐼 ∀ 𝑏 ∈ 2_o 𝑥 𝑟 ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ ”⟩ ⟩ ) ) } ⊆ { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( { 𝑢 , 𝑣 } ⊆ 𝑊 ∧ ( 𝐻 Σ_g ( 𝑇 ∘ 𝑢 ) ) = ( 𝐻 Σ_g ( 𝑇 ∘ 𝑣 ) ) ) } )
168	166 167	syl	⊢ ( 𝜑 → ∩ { 𝑟 ∣ ( 𝑟 Er 𝑊 ∧ ∀ 𝑥 ∈ 𝑊 ∀ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ∀ 𝑎 ∈ 𝐼 ∀ 𝑏 ∈ 2_o 𝑥 𝑟 ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ ”⟩ ⟩ ) ) } ⊆ { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( { 𝑢 , 𝑣 } ⊆ 𝑊 ∧ ( 𝐻 Σ_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 ( 𝑇 ∘ 𝐶 ) ) )

Metamath Proof Explorer

Theorem frgpuplem

Proof