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	$⊢ B = {Base}_{H}$
	frgpup.n	$⊢ N = {inv}_{g} (H)$
	frgpup.t	$⊢ T = (y \in I, z \in 2_{𝑜} ⟼ if (z = \emptyset, F (y), N (F (y))))$
	frgpup.h	$⊢ φ \to H \in Grp$
	frgpup.i	$⊢ φ \to I \in V$
	frgpup.a	$⊢ φ \to F : I ⟶ B$
	frgpup.w	$⊢ W = I (Word (I \times 2_{𝑜}))$
	frgpup.r	$⊢ \underset{˙}{\sim} = ~_{FG} (I)$
Assertion	frgpuplem	$⊢ (φ \land A \underset{˙}{\sim} C) \to \sum_{H} (T \circ A) = \sum_{H} (T \circ C)$

Proof

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

Metamath Proof Explorer

Theorem frgpuplem

Proof