Theorem frgpuplem 18008

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	⊢ 𝑇 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦ if(𝑧 = ∅, (𝐹‘𝑦), (𝑁‘(𝐹‘𝑦))))
frgpup.h	⊢ (𝜑 → 𝐻 ∈ Grp)
frgpup.i	⊢ (𝜑 → 𝐼 ∈ 𝑉)
frgpup.a	⊢ (𝜑 → 𝐹:𝐼⟶𝐵)
frgpup.w	⊢ 𝑊 = ( I ‘Word (𝐼 × 2𝑜))
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.

Step	Hyp	Ref	Expression
1		frgpup.w	. . . . . . 7 ⊢ 𝑊 = ( I ‘Word (𝐼 × 2𝑜))
2		frgpup.r	. . . . . . 7 ⊢ ∼ = ( ~FG ‘𝐼)
3	1, 2	efgval 17953	. . . . . 6 ⊢ ∼ = ∩ {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(#‘𝑥))∀𝑎 ∈ 𝐼 ∀𝑏 ∈ 2𝑜 𝑥𝑟(𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜 ∖ 𝑏)⟩”⟩⟩))}
4		coeq2 5202	. . . . . . . . . . . . 13 ⊢ (𝑢 = 𝑣 → (𝑇 ∘ 𝑢) = (𝑇 ∘ 𝑣))
5	4	oveq2d 6565	. . . . . . . . . . . 12 ⊢ (𝑢 = 𝑣 → (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))
6		eqid 2610	. . . . . . . . . . . 12 ⊢ {⟨𝑢, 𝑣⟩ ∣ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣))} = {⟨𝑢, 𝑣⟩ ∣ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣))}
7	5, 6	eqer 7664	. . . . . . . . . . 11 ⊢ {⟨𝑢, 𝑣⟩ ∣ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣))} Er V
8	7	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → {⟨𝑢, 𝑣⟩ ∣ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣))} Er V)
9		ssv 3588	. . . . . . . . . . 11 ⊢ 𝑊 ⊆ V
10	9	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → 𝑊 ⊆ V)
11	8, 10	erinxp 7708	. . . . . . . . 9 ⊢ (𝜑 → ({⟨𝑢, 𝑣⟩ ∣ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣))} ∩ (𝑊 × 𝑊)) Er 𝑊)
12		df-xp 5044	. . . . . . . . . . . . 13 ⊢ (𝑊 × 𝑊) = {⟨𝑢, 𝑣⟩ ∣ (𝑢 ∈ 𝑊 ∧ 𝑣 ∈ 𝑊)}
13	12	ineq1i 3772	. . . . . . . . . . . 12 ⊢ ((𝑊 × 𝑊) ∩ {⟨𝑢, 𝑣⟩ ∣ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣))}) = ({⟨𝑢, 𝑣⟩ ∣ (𝑢 ∈ 𝑊 ∧ 𝑣 ∈ 𝑊)} ∩ {⟨𝑢, 𝑣⟩ ∣ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣))})
14		incom 3767	. . . . . . . . . . . 12 ⊢ ((𝑊 × 𝑊) ∩ {⟨𝑢, 𝑣⟩ ∣ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣))}) = ({⟨𝑢, 𝑣⟩ ∣ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣))} ∩ (𝑊 × 𝑊))
15		inopab 5174	. . . . . . . . . . . 12 ⊢ ({⟨𝑢, 𝑣⟩ ∣ (𝑢 ∈ 𝑊 ∧ 𝑣 ∈ 𝑊)} ∩ {⟨𝑢, 𝑣⟩ ∣ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣))}) = {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝑊 ∧ 𝑣 ∈ 𝑊) ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))}
16	13, 14, 15	3eqtr3i 2640	. . . . . . . . . . 11 ⊢ ({⟨𝑢, 𝑣⟩ ∣ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣))} ∩ (𝑊 × 𝑊)) = {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝑊 ∧ 𝑣 ∈ 𝑊) ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))}
17		vex 3176	. . . . . . . . . . . . . 14 ⊢ 𝑢 ∈ V
18		vex 3176	. . . . . . . . . . . . . 14 ⊢ 𝑣 ∈ V
19	17, 18	prss 4291	. . . . . . . . . . . . 13 ⊢ ((𝑢 ∈ 𝑊 ∧ 𝑣 ∈ 𝑊) ↔ {𝑢, 𝑣} ⊆ 𝑊)
20	19	anbi1i 727	. . . . . . . . . . . 12 ⊢ (((𝑢 ∈ 𝑊 ∧ 𝑣 ∈ 𝑊) ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣))) ↔ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣))))
21	20	opabbii 4649	. . . . . . . . . . 11 ⊢ {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝑊 ∧ 𝑣 ∈ 𝑊) ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))} = {⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))}
22	16, 21	eqtri 2632	. . . . . . . . . 10 ⊢ ({⟨𝑢, 𝑣⟩ ∣ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣))} ∩ (𝑊 × 𝑊)) = {⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))}
23		ereq1 7636	. . . . . . . . . 10 ⊢ (({⟨𝑢, 𝑣⟩ ∣ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣))} ∩ (𝑊 × 𝑊)) = {⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))} → (({⟨𝑢, 𝑣⟩ ∣ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣))} ∩ (𝑊 × 𝑊)) Er 𝑊 ↔ {⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))} Er 𝑊))
24	22, 23	ax-mp 5	. . . . . . . . 9 ⊢ (({⟨𝑢, 𝑣⟩ ∣ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣))} ∩ (𝑊 × 𝑊)) Er 𝑊 ↔ {⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))} Er 𝑊)
25	11, 24	sylib 207	. . . . . . . 8 ⊢ (𝜑 → {⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))} Er 𝑊)
26		simplrl 796	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → 𝑥 ∈ 𝑊)
27		fviss 6166	. . . . . . . . . . . . . . . 16 ⊢ ( I ‘Word (𝐼 × 2𝑜)) ⊆ Word (𝐼 × 2𝑜)
28	1, 27	eqsstri 3598	. . . . . . . . . . . . . . 15 ⊢ 𝑊 ⊆ Word (𝐼 × 2𝑜)
29	28, 26	sseldi 3566	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → 𝑥 ∈ Word (𝐼 × 2𝑜))
30		opelxpi 5072	. . . . . . . . . . . . . . . 16 ⊢ ((𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜) → ⟨𝑎, 𝑏⟩ ∈ (𝐼 × 2𝑜))
31	30	adantl 481	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → ⟨𝑎, 𝑏⟩ ∈ (𝐼 × 2𝑜))
32		simprl 790	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → 𝑎 ∈ 𝐼)
33		2oconcl 7470	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 ∈ 2𝑜 → (1𝑜 ∖ 𝑏) ∈ 2𝑜)
34	33	ad2antll 761	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → (1𝑜 ∖ 𝑏) ∈ 2𝑜)
35		opelxpi 5072	. . . . . . . . . . . . . . . 16 ⊢ ((𝑎 ∈ 𝐼 ∧ (1𝑜 ∖ 𝑏) ∈ 2𝑜) → ⟨𝑎, (1𝑜 ∖ 𝑏)⟩ ∈ (𝐼 × 2𝑜))
36	32, 34, 35	syl2anc 691	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → ⟨𝑎, (1𝑜 ∖ 𝑏)⟩ ∈ (𝐼 × 2𝑜))
37	31, 36	s2cld 13466	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜 ∖ 𝑏)⟩”⟩ ∈ Word (𝐼 × 2𝑜))
38		splcl 13354	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ Word (𝐼 × 2𝑜) ∧ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜 ∖ 𝑏)⟩”⟩ ∈ Word (𝐼 × 2𝑜)) → (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜 ∖ 𝑏)⟩”⟩⟩) ∈ Word (𝐼 × 2𝑜))
39	29, 37, 38	syl2anc 691	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜 ∖ 𝑏)⟩”⟩⟩) ∈ Word (𝐼 × 2𝑜))
40	1	efgrcl 17951	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ 𝑊 → (𝐼 ∈ V ∧ 𝑊 = Word (𝐼 × 2𝑜)))
41	26, 40	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → (𝐼 ∈ V ∧ 𝑊 = Word (𝐼 × 2𝑜)))
42	41	simprd 478	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → 𝑊 = Word (𝐼 × 2𝑜))
43	39, 42	eleqtrrd 2691	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜 ∖ 𝑏)⟩”⟩⟩) ∈ 𝑊)
44	26, 43	jca 553	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → (𝑥 ∈ 𝑊 ∧ (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜 ∖ 𝑏)⟩”⟩⟩) ∈ 𝑊))
45		swrdcl 13271	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ Word (𝐼 × 2𝑜) → (𝑥 substr ⟨0, 𝑛⟩) ∈ Word (𝐼 × 2𝑜))
46	29, 45	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → (𝑥 substr ⟨0, 𝑛⟩) ∈ Word (𝐼 × 2𝑜))
47		frgpup.b	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝐵 = (Base‘𝐻)
48		frgpup.n	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑁 = (invg‘𝐻)
49		frgpup.t	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑇 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦ if(𝑧 = ∅, (𝐹‘𝑦), (𝑁‘(𝐹‘𝑦))))
50		frgpup.h	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐻 ∈ Grp)
51		frgpup.i	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐼 ∈ 𝑉)
52		frgpup.a	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐹:𝐼⟶𝐵)
53	47, 48, 49, 50, 51, 52	frgpuptf 18006	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑇:(𝐼 × 2𝑜)⟶𝐵)
54	53	ad2antrr 758	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → 𝑇:(𝐼 × 2𝑜)⟶𝐵)
55		ccatco 13432	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑥 substr ⟨0, 𝑛⟩) ∈ Word (𝐼 × 2𝑜) ∧ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜 ∖ 𝑏)⟩”⟩ ∈ Word (𝐼 × 2𝑜) ∧ 𝑇:(𝐼 × 2𝑜)⟶𝐵) → (𝑇 ∘ ((𝑥 substr ⟨0, 𝑛⟩) ++ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜 ∖ 𝑏)⟩”⟩)) = ((𝑇 ∘ (𝑥 substr ⟨0, 𝑛⟩)) ++ (𝑇 ∘ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜 ∖ 𝑏)⟩”⟩)))
56	46, 37, 54, 55	syl3anc 1318	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → (𝑇 ∘ ((𝑥 substr ⟨0, 𝑛⟩) ++ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜 ∖ 𝑏)⟩”⟩)) = ((𝑇 ∘ (𝑥 substr ⟨0, 𝑛⟩)) ++ (𝑇 ∘ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜 ∖ 𝑏)⟩”⟩)))
57	56	oveq2d 6565	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → (𝐻 Σg (𝑇 ∘ ((𝑥 substr ⟨0, 𝑛⟩) ++ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜 ∖ 𝑏)⟩”⟩))) = (𝐻 Σg ((𝑇 ∘ (𝑥 substr ⟨0, 𝑛⟩)) ++ (𝑇 ∘ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜 ∖ 𝑏)⟩”⟩))))
58	50	ad2antrr 758	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → 𝐻 ∈ Grp)
59		grpmnd 17252	. . . . . . . . . . . . . . . . 17 ⊢ (𝐻 ∈ Grp → 𝐻 ∈ Mnd)
60	58, 59	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → 𝐻 ∈ Mnd)
61		wrdco 13428	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑥 substr ⟨0, 𝑛⟩) ∈ Word (𝐼 × 2𝑜) ∧ 𝑇:(𝐼 × 2𝑜)⟶𝐵) → (𝑇 ∘ (𝑥 substr ⟨0, 𝑛⟩)) ∈ Word 𝐵)
62	46, 54, 61	syl2anc 691	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → (𝑇 ∘ (𝑥 substr ⟨0, 𝑛⟩)) ∈ Word 𝐵)
63		wrdco 13428	. . . . . . . . . . . . . . . . 17 ⊢ ((⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜 ∖ 𝑏)⟩”⟩ ∈ Word (𝐼 × 2𝑜) ∧ 𝑇:(𝐼 × 2𝑜)⟶𝐵) → (𝑇 ∘ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜 ∖ 𝑏)⟩”⟩) ∈ Word 𝐵)
64	37, 54, 63	syl2anc 691	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → (𝑇 ∘ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜 ∖ 𝑏)⟩”⟩) ∈ Word 𝐵)
65		eqid 2610	. . . . . . . . . . . . . . . . 17 ⊢ (+g‘𝐻) = (+g‘𝐻)
66	47, 65	gsumccat 17201	. . . . . . . . . . . . . . . 16 ⊢ ((𝐻 ∈ Mnd ∧ (𝑇 ∘ (𝑥 substr ⟨0, 𝑛⟩)) ∈ Word 𝐵 ∧ (𝑇 ∘ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜 ∖ 𝑏)⟩”⟩) ∈ Word 𝐵) → (𝐻 Σg ((𝑇 ∘ (𝑥 substr ⟨0, 𝑛⟩)) ++ (𝑇 ∘ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜 ∖ 𝑏)⟩”⟩))) = ((𝐻 Σg (𝑇 ∘ (𝑥 substr ⟨0, 𝑛⟩)))(+g‘𝐻)(𝐻 Σg (𝑇 ∘ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜 ∖ 𝑏)⟩”⟩))))
67	60, 62, 64, 66	syl3anc 1318	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → (𝐻 Σg ((𝑇 ∘ (𝑥 substr ⟨0, 𝑛⟩)) ++ (𝑇 ∘ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜 ∖ 𝑏)⟩”⟩))) = ((𝐻 Σg (𝑇 ∘ (𝑥 substr ⟨0, 𝑛⟩)))(+g‘𝐻)(𝐻 Σg (𝑇 ∘ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜 ∖ 𝑏)⟩”⟩))))
68	54, 31, 36	s2co 13515	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → (𝑇 ∘ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜 ∖ 𝑏)⟩”⟩) = ⟨“(𝑇‘⟨𝑎, 𝑏⟩)(𝑇‘⟨𝑎, (1𝑜 ∖ 𝑏)⟩)”⟩)
69		df-ov 6552	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑎𝑇𝑏) = (𝑇‘⟨𝑎, 𝑏⟩)
70	69	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → (𝑎𝑇𝑏) = (𝑇‘⟨𝑎, 𝑏⟩))
71		df-ov 6552	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑎(𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦ ⟨𝑦, (1𝑜 ∖ 𝑧)⟩)𝑏) = ((𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦ ⟨𝑦, (1𝑜 ∖ 𝑧)⟩)‘⟨𝑎, 𝑏⟩)
72		eqid 2610	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦ ⟨𝑦, (1𝑜 ∖ 𝑧)⟩) = (𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦ ⟨𝑦, (1𝑜 ∖ 𝑧)⟩)
73	72	efgmval 17948	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜) → (𝑎(𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦ ⟨𝑦, (1𝑜 ∖ 𝑧)⟩)𝑏) = ⟨𝑎, (1𝑜 ∖ 𝑏)⟩)
74	71, 73	syl5eqr 2658	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜) → ((𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦ ⟨𝑦, (1𝑜 ∖ 𝑧)⟩)‘⟨𝑎, 𝑏⟩) = ⟨𝑎, (1𝑜 ∖ 𝑏)⟩)
75	74	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → ((𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦ ⟨𝑦, (1𝑜 ∖ 𝑧)⟩)‘⟨𝑎, 𝑏⟩) = ⟨𝑎, (1𝑜 ∖ 𝑏)⟩)
76	75	fveq2d 6107	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → (𝑇‘((𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦ ⟨𝑦, (1𝑜 ∖ 𝑧)⟩)‘⟨𝑎, 𝑏⟩)) = (𝑇‘⟨𝑎, (1𝑜 ∖ 𝑏)⟩))
77	47, 48, 49, 50, 51, 52, 72	frgpuptinv 18007	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ ⟨𝑎, 𝑏⟩ ∈ (𝐼 × 2𝑜)) → (𝑇‘((𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦ ⟨𝑦, (1𝑜 ∖ 𝑧)⟩)‘⟨𝑎, 𝑏⟩)) = (𝑁‘(𝑇‘⟨𝑎, 𝑏⟩)))
78	30, 77	sylan2 490	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → (𝑇‘((𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦ ⟨𝑦, (1𝑜 ∖ 𝑧)⟩)‘⟨𝑎, 𝑏⟩)) = (𝑁‘(𝑇‘⟨𝑎, 𝑏⟩)))
79	78	adantlr 747	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → (𝑇‘((𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦ ⟨𝑦, (1𝑜 ∖ 𝑧)⟩)‘⟨𝑎, 𝑏⟩)) = (𝑁‘(𝑇‘⟨𝑎, 𝑏⟩)))
80	76, 79	eqtr3d 2646	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → (𝑇‘⟨𝑎, (1𝑜 ∖ 𝑏)⟩) = (𝑁‘(𝑇‘⟨𝑎, 𝑏⟩)))
81	69	fveq2i 6106	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑁‘(𝑎𝑇𝑏)) = (𝑁‘(𝑇‘⟨𝑎, 𝑏⟩))
82	80, 81	syl6reqr 2663	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → (𝑁‘(𝑎𝑇𝑏)) = (𝑇‘⟨𝑎, (1𝑜 ∖ 𝑏)⟩))
83	70, 82	s2eqd 13459	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → ⟨“(𝑎𝑇𝑏)(𝑁‘(𝑎𝑇𝑏))”⟩ = ⟨“(𝑇‘⟨𝑎, 𝑏⟩)(𝑇‘⟨𝑎, (1𝑜 ∖ 𝑏)⟩)”⟩)
84	68, 83	eqtr4d 2647	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → (𝑇 ∘ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜 ∖ 𝑏)⟩”⟩) = ⟨“(𝑎𝑇𝑏)(𝑁‘(𝑎𝑇𝑏))”⟩)
85	84	oveq2d 6565	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → (𝐻 Σg (𝑇 ∘ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜 ∖ 𝑏)⟩”⟩)) = (𝐻 Σg ⟨“(𝑎𝑇𝑏)(𝑁‘(𝑎𝑇𝑏))”⟩))
86		simprr 792	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → 𝑏 ∈ 2𝑜)
87	54, 32, 86	fovrnd 6704	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → (𝑎𝑇𝑏) ∈ 𝐵)
88	47, 48	grpinvcl 17290	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐻 ∈ Grp ∧ (𝑎𝑇𝑏) ∈ 𝐵) → (𝑁‘(𝑎𝑇𝑏)) ∈ 𝐵)
89	58, 87, 88	syl2anc 691	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → (𝑁‘(𝑎𝑇𝑏)) ∈ 𝐵)
90	47, 65	gsumws2 17202	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐻 ∈ Mnd ∧ (𝑎𝑇𝑏) ∈ 𝐵 ∧ (𝑁‘(𝑎𝑇𝑏)) ∈ 𝐵) → (𝐻 Σg ⟨“(𝑎𝑇𝑏)(𝑁‘(𝑎𝑇𝑏))”⟩) = ((𝑎𝑇𝑏)(+g‘𝐻)(𝑁‘(𝑎𝑇𝑏))))
91	60, 87, 89, 90	syl3anc 1318	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → (𝐻 Σg ⟨“(𝑎𝑇𝑏)(𝑁‘(𝑎𝑇𝑏))”⟩) = ((𝑎𝑇𝑏)(+g‘𝐻)(𝑁‘(𝑎𝑇𝑏))))
92		eqid 2610	. . . . . . . . . . . . . . . . . . . 20 ⊢ (0g‘𝐻) = (0g‘𝐻)
93	47, 65, 92, 48	grprinv 17292	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐻 ∈ Grp ∧ (𝑎𝑇𝑏) ∈ 𝐵) → ((𝑎𝑇𝑏)(+g‘𝐻)(𝑁‘(𝑎𝑇𝑏))) = (0g‘𝐻))
94	58, 87, 93	syl2anc 691	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → ((𝑎𝑇𝑏)(+g‘𝐻)(𝑁‘(𝑎𝑇𝑏))) = (0g‘𝐻))
95	85, 91, 94	3eqtrd 2648	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → (𝐻 Σg (𝑇 ∘ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜 ∖ 𝑏)⟩”⟩)) = (0g‘𝐻))
96	95	oveq2d 6565	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → ((𝐻 Σg (𝑇 ∘ (𝑥 substr ⟨0, 𝑛⟩)))(+g‘𝐻)(𝐻 Σg (𝑇 ∘ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜 ∖ 𝑏)⟩”⟩))) = ((𝐻 Σg (𝑇 ∘ (𝑥 substr ⟨0, 𝑛⟩)))(+g‘𝐻)(0g‘𝐻)))
97	47	gsumwcl 17200	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐻 ∈ Mnd ∧ (𝑇 ∘ (𝑥 substr ⟨0, 𝑛⟩)) ∈ Word 𝐵) → (𝐻 Σg (𝑇 ∘ (𝑥 substr ⟨0, 𝑛⟩))) ∈ 𝐵)
98	60, 62, 97	syl2anc 691	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → (𝐻 Σg (𝑇 ∘ (𝑥 substr ⟨0, 𝑛⟩))) ∈ 𝐵)
99	47, 65, 92	grprid 17276	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐻 ∈ Grp ∧ (𝐻 Σg (𝑇 ∘ (𝑥 substr ⟨0, 𝑛⟩))) ∈ 𝐵) → ((𝐻 Σg (𝑇 ∘ (𝑥 substr ⟨0, 𝑛⟩)))(+g‘𝐻)(0g‘𝐻)) = (𝐻 Σg (𝑇 ∘ (𝑥 substr ⟨0, 𝑛⟩))))
100	58, 98, 99	syl2anc 691	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → ((𝐻 Σg (𝑇 ∘ (𝑥 substr ⟨0, 𝑛⟩)))(+g‘𝐻)(0g‘𝐻)) = (𝐻 Σg (𝑇 ∘ (𝑥 substr ⟨0, 𝑛⟩))))
101	96, 100	eqtrd 2644	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → ((𝐻 Σg (𝑇 ∘ (𝑥 substr ⟨0, 𝑛⟩)))(+g‘𝐻)(𝐻 Σg (𝑇 ∘ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜 ∖ 𝑏)⟩”⟩))) = (𝐻 Σg (𝑇 ∘ (𝑥 substr ⟨0, 𝑛⟩))))
102	57, 67, 101	3eqtrrd 2649	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → (𝐻 Σg (𝑇 ∘ (𝑥 substr ⟨0, 𝑛⟩))) = (𝐻 Σg (𝑇 ∘ ((𝑥 substr ⟨0, 𝑛⟩) ++ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜 ∖ 𝑏)⟩”⟩))))
103	102	oveq1d 6564	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → ((𝐻 Σg (𝑇 ∘ (𝑥 substr ⟨0, 𝑛⟩)))(+g‘𝐻)(𝐻 Σg (𝑇 ∘ (𝑥 substr ⟨𝑛, (#‘𝑥)⟩)))) = ((𝐻 Σg (𝑇 ∘ ((𝑥 substr ⟨0, 𝑛⟩) ++ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜 ∖ 𝑏)⟩”⟩)))(+g‘𝐻)(𝐻 Σg (𝑇 ∘ (𝑥 substr ⟨𝑛, (#‘𝑥)⟩)))))
104		swrdcl 13271	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ Word (𝐼 × 2𝑜) → (𝑥 substr ⟨𝑛, (#‘𝑥)⟩) ∈ Word (𝐼 × 2𝑜))
105	29, 104	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → (𝑥 substr ⟨𝑛, (#‘𝑥)⟩) ∈ Word (𝐼 × 2𝑜))
106		wrdco 13428	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 substr ⟨𝑛, (#‘𝑥)⟩) ∈ Word (𝐼 × 2𝑜) ∧ 𝑇:(𝐼 × 2𝑜)⟶𝐵) → (𝑇 ∘ (𝑥 substr ⟨𝑛, (#‘𝑥)⟩)) ∈ Word 𝐵)
107	105, 54, 106	syl2anc 691	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → (𝑇 ∘ (𝑥 substr ⟨𝑛, (#‘𝑥)⟩)) ∈ Word 𝐵)
108	47, 65	gsumccat 17201	. . . . . . . . . . . . . 14 ⊢ ((𝐻 ∈ Mnd ∧ (𝑇 ∘ (𝑥 substr ⟨0, 𝑛⟩)) ∈ Word 𝐵 ∧ (𝑇 ∘ (𝑥 substr ⟨𝑛, (#‘𝑥)⟩)) ∈ Word 𝐵) → (𝐻 Σg ((𝑇 ∘ (𝑥 substr ⟨0, 𝑛⟩)) ++ (𝑇 ∘ (𝑥 substr ⟨𝑛, (#‘𝑥)⟩)))) = ((𝐻 Σg (𝑇 ∘ (𝑥 substr ⟨0, 𝑛⟩)))(+g‘𝐻)(𝐻 Σg (𝑇 ∘ (𝑥 substr ⟨𝑛, (#‘𝑥)⟩)))))
109	60, 62, 107, 108	syl3anc 1318	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → (𝐻 Σg ((𝑇 ∘ (𝑥 substr ⟨0, 𝑛⟩)) ++ (𝑇 ∘ (𝑥 substr ⟨𝑛, (#‘𝑥)⟩)))) = ((𝐻 Σg (𝑇 ∘ (𝑥 substr ⟨0, 𝑛⟩)))(+g‘𝐻)(𝐻 Σg (𝑇 ∘ (𝑥 substr ⟨𝑛, (#‘𝑥)⟩)))))
110		ccatcl 13212	. . . . . . . . . . . . . . . 16 ⊢ (((𝑥 substr ⟨0, 𝑛⟩) ∈ Word (𝐼 × 2𝑜) ∧ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜 ∖ 𝑏)⟩”⟩ ∈ Word (𝐼 × 2𝑜)) → ((𝑥 substr ⟨0, 𝑛⟩) ++ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜 ∖ 𝑏)⟩”⟩) ∈ Word (𝐼 × 2𝑜))
111	46, 37, 110	syl2anc 691	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → ((𝑥 substr ⟨0, 𝑛⟩) ++ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜 ∖ 𝑏)⟩”⟩) ∈ Word (𝐼 × 2𝑜))
112		wrdco 13428	. . . . . . . . . . . . . . 15 ⊢ ((((𝑥 substr ⟨0, 𝑛⟩) ++ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜 ∖ 𝑏)⟩”⟩) ∈ Word (𝐼 × 2𝑜) ∧ 𝑇:(𝐼 × 2𝑜)⟶𝐵) → (𝑇 ∘ ((𝑥 substr ⟨0, 𝑛⟩) ++ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜 ∖ 𝑏)⟩”⟩)) ∈ Word 𝐵)
113	111, 54, 112	syl2anc 691	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → (𝑇 ∘ ((𝑥 substr ⟨0, 𝑛⟩) ++ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜 ∖ 𝑏)⟩”⟩)) ∈ Word 𝐵)
114	47, 65	gsumccat 17201	. . . . . . . . . . . . . 14 ⊢ ((𝐻 ∈ Mnd ∧ (𝑇 ∘ ((𝑥 substr ⟨0, 𝑛⟩) ++ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜 ∖ 𝑏)⟩”⟩)) ∈ Word 𝐵 ∧ (𝑇 ∘ (𝑥 substr ⟨𝑛, (#‘𝑥)⟩)) ∈ Word 𝐵) → (𝐻 Σg ((𝑇 ∘ ((𝑥 substr ⟨0, 𝑛⟩) ++ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜 ∖ 𝑏)⟩”⟩)) ++ (𝑇 ∘ (𝑥 substr ⟨𝑛, (#‘𝑥)⟩)))) = ((𝐻 Σg (𝑇 ∘ ((𝑥 substr ⟨0, 𝑛⟩) ++ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜 ∖ 𝑏)⟩”⟩)))(+g‘𝐻)(𝐻 Σg (𝑇 ∘ (𝑥 substr ⟨𝑛, (#‘𝑥)⟩)))))
115	60, 113, 107, 114	syl3anc 1318	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → (𝐻 Σg ((𝑇 ∘ ((𝑥 substr ⟨0, 𝑛⟩) ++ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜 ∖ 𝑏)⟩”⟩)) ++ (𝑇 ∘ (𝑥 substr ⟨𝑛, (#‘𝑥)⟩)))) = ((𝐻 Σg (𝑇 ∘ ((𝑥 substr ⟨0, 𝑛⟩) ++ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜 ∖ 𝑏)⟩”⟩)))(+g‘𝐻)(𝐻 Σg (𝑇 ∘ (𝑥 substr ⟨𝑛, (#‘𝑥)⟩)))))
116	103, 109, 115	3eqtr4d 2654	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → (𝐻 Σg ((𝑇 ∘ (𝑥 substr ⟨0, 𝑛⟩)) ++ (𝑇 ∘ (𝑥 substr ⟨𝑛, (#‘𝑥)⟩)))) = (𝐻 Σg ((𝑇 ∘ ((𝑥 substr ⟨0, 𝑛⟩) ++ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜 ∖ 𝑏)⟩”⟩)) ++ (𝑇 ∘ (𝑥 substr ⟨𝑛, (#‘𝑥)⟩)))))
117		simplrr 797	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → 𝑛 ∈ (0...(#‘𝑥)))
118		elfzuz 12209	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ (0...(#‘𝑥)) → 𝑛 ∈ (ℤ≥‘0))
119		eluzfz1 12219	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ (ℤ≥‘0) → 0 ∈ (0...𝑛))
120	117, 118, 119	3syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → 0 ∈ (0...𝑛))
121		lencl 13179	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ Word (𝐼 × 2𝑜) → (#‘𝑥) ∈ ℕ0)
122	29, 121	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → (#‘𝑥) ∈ ℕ0)
123		nn0uz 11598	. . . . . . . . . . . . . . . . . . 19 ⊢ ℕ0 = (ℤ≥‘0)
124	122, 123	syl6eleq 2698	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → (#‘𝑥) ∈ (ℤ≥‘0))
125		eluzfz2 12220	. . . . . . . . . . . . . . . . . 18 ⊢ ((#‘𝑥) ∈ (ℤ≥‘0) → (#‘𝑥) ∈ (0...(#‘𝑥)))
126	124, 125	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → (#‘𝑥) ∈ (0...(#‘𝑥)))
127		ccatswrd 13308	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ Word (𝐼 × 2𝑜) ∧ (0 ∈ (0...𝑛) ∧ 𝑛 ∈ (0...(#‘𝑥)) ∧ (#‘𝑥) ∈ (0...(#‘𝑥)))) → ((𝑥 substr ⟨0, 𝑛⟩) ++ (𝑥 substr ⟨𝑛, (#‘𝑥)⟩)) = (𝑥 substr ⟨0, (#‘𝑥)⟩))
128	29, 120, 117, 126, 127	syl13anc 1320	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → ((𝑥 substr ⟨0, 𝑛⟩) ++ (𝑥 substr ⟨𝑛, (#‘𝑥)⟩)) = (𝑥 substr ⟨0, (#‘𝑥)⟩))
129		swrdid 13280	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ Word (𝐼 × 2𝑜) → (𝑥 substr ⟨0, (#‘𝑥)⟩) = 𝑥)
130	29, 129	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → (𝑥 substr ⟨0, (#‘𝑥)⟩) = 𝑥)
131	128, 130	eqtrd 2644	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → ((𝑥 substr ⟨0, 𝑛⟩) ++ (𝑥 substr ⟨𝑛, (#‘𝑥)⟩)) = 𝑥)
132	131	coeq2d 5206	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → (𝑇 ∘ ((𝑥 substr ⟨0, 𝑛⟩) ++ (𝑥 substr ⟨𝑛, (#‘𝑥)⟩))) = (𝑇 ∘ 𝑥))
133		ccatco 13432	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 substr ⟨0, 𝑛⟩) ∈ Word (𝐼 × 2𝑜) ∧ (𝑥 substr ⟨𝑛, (#‘𝑥)⟩) ∈ Word (𝐼 × 2𝑜) ∧ 𝑇:(𝐼 × 2𝑜)⟶𝐵) → (𝑇 ∘ ((𝑥 substr ⟨0, 𝑛⟩) ++ (𝑥 substr ⟨𝑛, (#‘𝑥)⟩))) = ((𝑇 ∘ (𝑥 substr ⟨0, 𝑛⟩)) ++ (𝑇 ∘ (𝑥 substr ⟨𝑛, (#‘𝑥)⟩))))
134	46, 105, 54, 133	syl3anc 1318	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → (𝑇 ∘ ((𝑥 substr ⟨0, 𝑛⟩) ++ (𝑥 substr ⟨𝑛, (#‘𝑥)⟩))) = ((𝑇 ∘ (𝑥 substr ⟨0, 𝑛⟩)) ++ (𝑇 ∘ (𝑥 substr ⟨𝑛, (#‘𝑥)⟩))))
135	132, 134	eqtr3d 2646	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → (𝑇 ∘ 𝑥) = ((𝑇 ∘ (𝑥 substr ⟨0, 𝑛⟩)) ++ (𝑇 ∘ (𝑥 substr ⟨𝑛, (#‘𝑥)⟩))))
136	135	oveq2d 6565	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → (𝐻 Σg (𝑇 ∘ 𝑥)) = (𝐻 Σg ((𝑇 ∘ (𝑥 substr ⟨0, 𝑛⟩)) ++ (𝑇 ∘ (𝑥 substr ⟨𝑛, (#‘𝑥)⟩)))))
137		splval 13353	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ 𝑊 ∧ (𝑛 ∈ (0...(#‘𝑥)) ∧ 𝑛 ∈ (0...(#‘𝑥)) ∧ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜 ∖ 𝑏)⟩”⟩ ∈ Word (𝐼 × 2𝑜))) → (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜 ∖ 𝑏)⟩”⟩⟩) = (((𝑥 substr ⟨0, 𝑛⟩) ++ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜 ∖ 𝑏)⟩”⟩) ++ (𝑥 substr ⟨𝑛, (#‘𝑥)⟩)))
138	26, 117, 117, 37, 137	syl13anc 1320	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜 ∖ 𝑏)⟩”⟩⟩) = (((𝑥 substr ⟨0, 𝑛⟩) ++ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜 ∖ 𝑏)⟩”⟩) ++ (𝑥 substr ⟨𝑛, (#‘𝑥)⟩)))
139	138	coeq2d 5206	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → (𝑇 ∘ (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜 ∖ 𝑏)⟩”⟩⟩)) = (𝑇 ∘ (((𝑥 substr ⟨0, 𝑛⟩) ++ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜 ∖ 𝑏)⟩”⟩) ++ (𝑥 substr ⟨𝑛, (#‘𝑥)⟩))))
140		ccatco 13432	. . . . . . . . . . . . . . 15 ⊢ ((((𝑥 substr ⟨0, 𝑛⟩) ++ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜 ∖ 𝑏)⟩”⟩) ∈ Word (𝐼 × 2𝑜) ∧ (𝑥 substr ⟨𝑛, (#‘𝑥)⟩) ∈ Word (𝐼 × 2𝑜) ∧ 𝑇:(𝐼 × 2𝑜)⟶𝐵) → (𝑇 ∘ (((𝑥 substr ⟨0, 𝑛⟩) ++ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜 ∖ 𝑏)⟩”⟩) ++ (𝑥 substr ⟨𝑛, (#‘𝑥)⟩))) = ((𝑇 ∘ ((𝑥 substr ⟨0, 𝑛⟩) ++ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜 ∖ 𝑏)⟩”⟩)) ++ (𝑇 ∘ (𝑥 substr ⟨𝑛, (#‘𝑥)⟩))))
141	111, 105, 54, 140	syl3anc 1318	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → (𝑇 ∘ (((𝑥 substr ⟨0, 𝑛⟩) ++ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜 ∖ 𝑏)⟩”⟩) ++ (𝑥 substr ⟨𝑛, (#‘𝑥)⟩))) = ((𝑇 ∘ ((𝑥 substr ⟨0, 𝑛⟩) ++ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜 ∖ 𝑏)⟩”⟩)) ++ (𝑇 ∘ (𝑥 substr ⟨𝑛, (#‘𝑥)⟩))))
142	139, 141	eqtrd 2644	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → (𝑇 ∘ (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜 ∖ 𝑏)⟩”⟩⟩)) = ((𝑇 ∘ ((𝑥 substr ⟨0, 𝑛⟩) ++ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜 ∖ 𝑏)⟩”⟩)) ++ (𝑇 ∘ (𝑥 substr ⟨𝑛, (#‘𝑥)⟩))))
143	142	oveq2d 6565	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → (𝐻 Σg (𝑇 ∘ (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜 ∖ 𝑏)⟩”⟩⟩))) = (𝐻 Σg ((𝑇 ∘ ((𝑥 substr ⟨0, 𝑛⟩) ++ ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜 ∖ 𝑏)⟩”⟩)) ++ (𝑇 ∘ (𝑥 substr ⟨𝑛, (#‘𝑥)⟩)))))
144	116, 136, 143	3eqtr4d 2654	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → (𝐻 Σg (𝑇 ∘ 𝑥)) = (𝐻 Σg (𝑇 ∘ (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜 ∖ 𝑏)⟩”⟩⟩))))
145		vex 3176	. . . . . . . . . . . 12 ⊢ 𝑥 ∈ V
146		ovex 6577	. . . . . . . . . . . 12 ⊢ (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜 ∖ 𝑏)⟩”⟩⟩) ∈ V
147		eleq1 2676	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = 𝑥 → (𝑢 ∈ 𝑊 ↔ 𝑥 ∈ 𝑊))
148		eleq1 2676	. . . . . . . . . . . . . . 15 ⊢ (𝑣 = (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜 ∖ 𝑏)⟩”⟩⟩) → (𝑣 ∈ 𝑊 ↔ (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜 ∖ 𝑏)⟩”⟩⟩) ∈ 𝑊))
149	147, 148	bi2anan9 913	. . . . . . . . . . . . . 14 ⊢ ((𝑢 = 𝑥 ∧ 𝑣 = (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜 ∖ 𝑏)⟩”⟩⟩)) → ((𝑢 ∈ 𝑊 ∧ 𝑣 ∈ 𝑊) ↔ (𝑥 ∈ 𝑊 ∧ (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜 ∖ 𝑏)⟩”⟩⟩) ∈ 𝑊)))
150	19, 149	syl5bbr 273	. . . . . . . . . . . . 13 ⊢ ((𝑢 = 𝑥 ∧ 𝑣 = (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜 ∖ 𝑏)⟩”⟩⟩)) → ({𝑢, 𝑣} ⊆ 𝑊 ↔ (𝑥 ∈ 𝑊 ∧ (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜 ∖ 𝑏)⟩”⟩⟩) ∈ 𝑊)))
151		coeq2 5202	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = 𝑥 → (𝑇 ∘ 𝑢) = (𝑇 ∘ 𝑥))
152	151	oveq2d 6565	. . . . . . . . . . . . . 14 ⊢ (𝑢 = 𝑥 → (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑥)))
153		coeq2 5202	. . . . . . . . . . . . . . 15 ⊢ (𝑣 = (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜 ∖ 𝑏)⟩”⟩⟩) → (𝑇 ∘ 𝑣) = (𝑇 ∘ (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜 ∖ 𝑏)⟩”⟩⟩)))
154	153	oveq2d 6565	. . . . . . . . . . . . . 14 ⊢ (𝑣 = (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜 ∖ 𝑏)⟩”⟩⟩) → (𝐻 Σg (𝑇 ∘ 𝑣)) = (𝐻 Σg (𝑇 ∘ (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜 ∖ 𝑏)⟩”⟩⟩))))
155	152, 154	eqeqan12d 2626	. . . . . . . . . . . . 13 ⊢ ((𝑢 = 𝑥 ∧ 𝑣 = (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜 ∖ 𝑏)⟩”⟩⟩)) → ((𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)) ↔ (𝐻 Σg (𝑇 ∘ 𝑥)) = (𝐻 Σg (𝑇 ∘ (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜 ∖ 𝑏)⟩”⟩⟩)))))
156	150, 155	anbi12d 743	. . . . . . . . . . . 12 ⊢ ((𝑢 = 𝑥 ∧ 𝑣 = (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜 ∖ 𝑏)⟩”⟩⟩)) → (({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣))) ↔ ((𝑥 ∈ 𝑊 ∧ (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜 ∖ 𝑏)⟩”⟩⟩) ∈ 𝑊) ∧ (𝐻 Σg (𝑇 ∘ 𝑥)) = (𝐻 Σg (𝑇 ∘ (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜 ∖ 𝑏)⟩”⟩⟩))))))
157		eqid 2610	. . . . . . . . . . . 12 ⊢ {⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))} = {⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))}
158	145, 146, 156, 157	braba 4917	. . . . . . . . . . 11 ⊢ (𝑥{⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))} (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜 ∖ 𝑏)⟩”⟩⟩) ↔ ((𝑥 ∈ 𝑊 ∧ (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜 ∖ 𝑏)⟩”⟩⟩) ∈ 𝑊) ∧ (𝐻 Σg (𝑇 ∘ 𝑥)) = (𝐻 Σg (𝑇 ∘ (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜 ∖ 𝑏)⟩”⟩⟩)))))
159	44, 144, 158	sylanbrc 695	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜)) → 𝑥{⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))} (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜 ∖ 𝑏)⟩”⟩⟩))
160	159	ralrimivva 2954	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑛 ∈ (0...(#‘𝑥)))) → ∀𝑎 ∈ 𝐼 ∀𝑏 ∈ 2𝑜 𝑥{⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))} (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜 ∖ 𝑏)⟩”⟩⟩))
161	160	ralrimivva 2954	. . . . . . . 8 ⊢ (𝜑 → ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(#‘𝑥))∀𝑎 ∈ 𝐼 ∀𝑏 ∈ 2𝑜 𝑥{⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))} (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜 ∖ 𝑏)⟩”⟩⟩))
162		fvex 6113	. . . . . . . . . . 11 ⊢ ( I ‘Word (𝐼 × 2𝑜)) ∈ V
163	1, 162	eqeltri 2684	. . . . . . . . . 10 ⊢ 𝑊 ∈ V
164		erex 7653	. . . . . . . . . 10 ⊢ ({⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))} Er 𝑊 → (𝑊 ∈ V → {⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))} ∈ V))
165	25, 163, 164	mpisyl 21	. . . . . . . . 9 ⊢ (𝜑 → {⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))} ∈ V)
166		ereq1 7636	. . . . . . . . . . 11 ⊢ (𝑟 = {⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))} → (𝑟 Er 𝑊 ↔ {⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))} Er 𝑊))
167		breq 4585	. . . . . . . . . . . . 13 ⊢ (𝑟 = {⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))} → (𝑥𝑟(𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜 ∖ 𝑏)⟩”⟩⟩) ↔ 𝑥{⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))} (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜 ∖ 𝑏)⟩”⟩⟩)))
168	167	2ralbidv 2972	. . . . . . . . . . . 12 ⊢ (𝑟 = {⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))} → (∀𝑎 ∈ 𝐼 ∀𝑏 ∈ 2𝑜 𝑥𝑟(𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜 ∖ 𝑏)⟩”⟩⟩) ↔ ∀𝑎 ∈ 𝐼 ∀𝑏 ∈ 2𝑜 𝑥{⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))} (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜 ∖ 𝑏)⟩”⟩⟩)))
169	168	2ralbidv 2972	. . . . . . . . . . 11 ⊢ (𝑟 = {⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))} → (∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(#‘𝑥))∀𝑎 ∈ 𝐼 ∀𝑏 ∈ 2𝑜 𝑥𝑟(𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜 ∖ 𝑏)⟩”⟩⟩) ↔ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(#‘𝑥))∀𝑎 ∈ 𝐼 ∀𝑏 ∈ 2𝑜 𝑥{⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))} (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜 ∖ 𝑏)⟩”⟩⟩)))
170	166, 169	anbi12d 743	. . . . . . . . . 10 ⊢ (𝑟 = {⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))} → ((𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(#‘𝑥))∀𝑎 ∈ 𝐼 ∀𝑏 ∈ 2𝑜 𝑥𝑟(𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜 ∖ 𝑏)⟩”⟩⟩)) ↔ ({⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))} Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(#‘𝑥))∀𝑎 ∈ 𝐼 ∀𝑏 ∈ 2𝑜 𝑥{⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))} (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜 ∖ 𝑏)⟩”⟩⟩))))
171	170	elabg 3320	. . . . . . . . 9 ⊢ ({⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))} ∈ V → ({⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))} ∈ {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(#‘𝑥))∀𝑎 ∈ 𝐼 ∀𝑏 ∈ 2𝑜 𝑥𝑟(𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜 ∖ 𝑏)⟩”⟩⟩))} ↔ ({⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))} Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(#‘𝑥))∀𝑎 ∈ 𝐼 ∀𝑏 ∈ 2𝑜 𝑥{⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))} (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜 ∖ 𝑏)⟩”⟩⟩))))
172	165, 171	syl 17	. . . . . . . 8 ⊢ (𝜑 → ({⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))} ∈ {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(#‘𝑥))∀𝑎 ∈ 𝐼 ∀𝑏 ∈ 2𝑜 𝑥𝑟(𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜 ∖ 𝑏)⟩”⟩⟩))} ↔ ({⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))} Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(#‘𝑥))∀𝑎 ∈ 𝐼 ∀𝑏 ∈ 2𝑜 𝑥{⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))} (𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜 ∖ 𝑏)⟩”⟩⟩))))
173	25, 161, 172	mpbir2and 959	. . . . . . 7 ⊢ (𝜑 → {⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))} ∈ {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(#‘𝑥))∀𝑎 ∈ 𝐼 ∀𝑏 ∈ 2𝑜 𝑥𝑟(𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜 ∖ 𝑏)⟩”⟩⟩))})
174		intss1 4427	. . . . . . 7 ⊢ ({⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))} ∈ {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(#‘𝑥))∀𝑎 ∈ 𝐼 ∀𝑏 ∈ 2𝑜 𝑥𝑟(𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜 ∖ 𝑏)⟩”⟩⟩))} → ∩ {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(#‘𝑥))∀𝑎 ∈ 𝐼 ∀𝑏 ∈ 2𝑜 𝑥𝑟(𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜 ∖ 𝑏)⟩”⟩⟩))} ⊆ {⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))})
175	173, 174	syl 17	. . . . . 6 ⊢ (𝜑 → ∩ {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(#‘𝑥))∀𝑎 ∈ 𝐼 ∀𝑏 ∈ 2𝑜 𝑥𝑟(𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑎, 𝑏⟩⟨𝑎, (1𝑜 ∖ 𝑏)⟩”⟩⟩))} ⊆ {⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))})
176	3, 175	syl5eqss 3612	. . . . 5 ⊢ (𝜑 → ∼ ⊆ {⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))})
177	176	ssbrd 4626	. . . 4 ⊢ (𝜑 → (𝐴 ∼ 𝐶 → 𝐴{⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))}𝐶))
178	177	imp 444	. . 3 ⊢ ((𝜑 ∧ 𝐴 ∼ 𝐶) → 𝐴{⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))}𝐶)
179	1, 2	efger 17954	. . . . . 6 ⊢ ∼ Er 𝑊
180		errel 7638	. . . . . 6 ⊢ ( ∼ Er 𝑊 → Rel ∼ )
181	179, 180	mp1i 13	. . . . 5 ⊢ (𝜑 → Rel ∼ )
182		brrelex12 5079	. . . . 5 ⊢ ((Rel ∼ ∧ 𝐴 ∼ 𝐶) → (𝐴 ∈ V ∧ 𝐶 ∈ V))
183	181, 182	sylan 487	. . . 4 ⊢ ((𝜑 ∧ 𝐴 ∼ 𝐶) → (𝐴 ∈ V ∧ 𝐶 ∈ V))
184		preq12 4214	. . . . . . 7 ⊢ ((𝑢 = 𝐴 ∧ 𝑣 = 𝐶) → {𝑢, 𝑣} = {𝐴, 𝐶})
185	184	sseq1d 3595	. . . . . 6 ⊢ ((𝑢 = 𝐴 ∧ 𝑣 = 𝐶) → ({𝑢, 𝑣} ⊆ 𝑊 ↔ {𝐴, 𝐶} ⊆ 𝑊))
186		coeq2 5202	. . . . . . . 8 ⊢ (𝑢 = 𝐴 → (𝑇 ∘ 𝑢) = (𝑇 ∘ 𝐴))
187	186	oveq2d 6565	. . . . . . 7 ⊢ (𝑢 = 𝐴 → (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝐴)))
188		coeq2 5202	. . . . . . . 8 ⊢ (𝑣 = 𝐶 → (𝑇 ∘ 𝑣) = (𝑇 ∘ 𝐶))
189	188	oveq2d 6565	. . . . . . 7 ⊢ (𝑣 = 𝐶 → (𝐻 Σg (𝑇 ∘ 𝑣)) = (𝐻 Σg (𝑇 ∘ 𝐶)))
190	187, 189	eqeqan12d 2626	. . . . . 6 ⊢ ((𝑢 = 𝐴 ∧ 𝑣 = 𝐶) → ((𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)) ↔ (𝐻 Σg (𝑇 ∘ 𝐴)) = (𝐻 Σg (𝑇 ∘ 𝐶))))
191	185, 190	anbi12d 743	. . . . 5 ⊢ ((𝑢 = 𝐴 ∧ 𝑣 = 𝐶) → (({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣))) ↔ ({𝐴, 𝐶} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝐴)) = (𝐻 Σg (𝑇 ∘ 𝐶)))))
192	191, 157	brabga 4914	. . . 4 ⊢ ((𝐴 ∈ V ∧ 𝐶 ∈ V) → (𝐴{⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))}𝐶 ↔ ({𝐴, 𝐶} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝐴)) = (𝐻 Σg (𝑇 ∘ 𝐶)))))
193	183, 192	syl 17	. . 3 ⊢ ((𝜑 ∧ 𝐴 ∼ 𝐶) → (𝐴{⟨𝑢, 𝑣⟩ ∣ ({𝑢, 𝑣} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝑢)) = (𝐻 Σg (𝑇 ∘ 𝑣)))}𝐶 ↔ ({𝐴, 𝐶} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝐴)) = (𝐻 Σg (𝑇 ∘ 𝐶)))))
194	178, 193	mpbid 221	. 2 ⊢ ((𝜑 ∧ 𝐴 ∼ 𝐶) → ({𝐴, 𝐶} ⊆ 𝑊 ∧ (𝐻 Σg (𝑇 ∘ 𝐴)) = (𝐻 Σg (𝑇 ∘ 𝐶))))
195	194	simprd 478	1 ⊢ ((𝜑 ∧ 𝐴 ∼ 𝐶) → (𝐻 Σg (𝑇 ∘ 𝐴)) = (𝐻 Σg (𝑇 ∘ 𝐶)))

Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   = wceq 1475   ∈ wcel 1977  {cab 2596  ∀wral 2896  Vcvv 3173   ∖ cdif 3537   ∩ cin 3539   ⊆ wss 3540  ∅c0 3874  ifcif 4036  {cpr 4127  ⟨cop 4131  ⟨cotp 4133  ∩ cint 4410   class class class wbr 4583  {copab 4642   I cid 4948   × cxp 5036   ∘ ccom 5042  Rel wrel 5043  ⟶wf 5800  ‘cfv 5804  (class class class)co 6549   ↦ cmpt2 6551  1_𝑜c1o 7440  2_𝑜c2o 7441   Er wer 7626  0cc0 9815  ℕ₀cn0 11169  ℤ_≥cuz 11563  ...cfz 12197  #chash 12979  Word cword 13146   ++ cconcat 13148   substr csubstr 13150   splice csplice 13151  ⟨“cs2 13437  Basecbs 15695  +_gcplusg 15768  0_gc0g 15923   Σ_g cgsu 15924  Mndcmnd 17117  Grpcgrp 17245  inv_gcminusg 17246   ~_FG cefg 17942

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-ot 4134  df-uni 4373  df-int 4411  df-iun 4457  df-iin 4458  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-1st 7059  df-2nd 7060  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-2o 7448  df-oadd 7451  df-er 7629  df-map 7746  df-pm 7747  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845  df-card 8648  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-nn 10898  df-2 10956  df-n0 11170  df-z 11255  df-uz 11564  df-fz 12198  df-fzo 12335  df-seq 12664  df-hash 12980  df-word 13154  df-concat 13156  df-s1 13157  df-substr 13158  df-splice 13159  df-s2 13444  df-ndx 15698  df-slot 15699  df-base 15700  df-sets 15701  df-ress 15702  df-plusg 15781  df-0g 15925  df-gsum 15926  df-mgm 17065  df-sgrp 17107  df-mnd 17118  df-submnd 17159  df-grp 17248  df-minusg 17249  df-efg 17945

This theorem is referenced by:  frgpupf  18009