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	sselid	$⊢ ((φ \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	56	grpmndd	$⊢ ((φ \land (x \in W \land n \in (0 \dots \|x\|))) \land (a \in I \land b \in 2_{𝑜})) \to H \in Mnd$
58		wrdco	$⊢ (x prefix n \in Word (I \times 2_{𝑜}) \land T : I \times 2_{𝑜} ⟶ B) \to T \circ (x prefix n) \in Word B$
59	50 52 58	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$
60		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$
61	42 52 60	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$
62		eqid	$⊢ +_{H} = +_{H}$
63	1 62	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⟩ ”⟩))$
64	57 59 61 63	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⟩ ”⟩))$
65	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⟩) ”⟩$
66		df-ov	$⊢ a T b = T (⟨a, b⟩)$
67	66	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⟩)$
68	66	fveq2i	$⊢ N (a T b) = N (T (⟨a, b⟩))$
69		df-ov	$⊢ a (y \in I, z \in 2_{𝑜} ⟼ ⟨y, 1_{𝑜} ∖ z⟩) b = (y \in I, z \in 2_{𝑜} ⟼ ⟨y, 1_{𝑜} ∖ z⟩) (⟨a, b⟩)$
70		eqid	$⊢ (y \in I, z \in 2_{𝑜} ⟼ ⟨y, 1_{𝑜} ∖ z⟩) = (y \in I, z \in 2_{𝑜} ⟼ ⟨y, 1_{𝑜} ∖ z⟩)$
71	70	efgmval	$⊢ (a \in I \land b \in 2_{𝑜}) \to a (y \in I, z \in 2_{𝑜} ⟼ ⟨y, 1_{𝑜} ∖ z⟩) b = ⟨a, 1_{𝑜} ∖ b⟩$
72	69 71	eqtr3id	$⊢ (a \in I \land b \in 2_{𝑜}) \to (y \in I, z \in 2_{𝑜} ⟼ ⟨y, 1_{𝑜} ∖ z⟩) (⟨a, b⟩) = ⟨a, 1_{𝑜} ∖ b⟩$
73	72	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⟩$
74	73	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⟩)$
75	1 2 3 4 5 6 70	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⟩))$
76	36 75	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⟩))$
77	76	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⟩))$
78	74 77	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⟩))$
79	68 78	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⟩)$
80	67 79	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⟩) ”⟩$
81	65 80	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) ”⟩$
82	81	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) ”⟩$
83		simprr	$⊢ ((φ \land (x \in W \land n \in (0 \dots \|x\|))) \land (a \in I \land b \in 2_{𝑜})) \to b \in 2_{𝑜}$
84	52 38 83	fovcdmd	$⊢ ((φ \land (x \in W \land n \in (0 \dots \|x\|))) \land (a \in I \land b \in 2_{𝑜})) \to a T b \in B$
85	1 2	grpinvcl	$⊢ (H \in Grp \land a T b \in B) \to N (a T b) \in B$
86	56 84 85	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$
87	1 62	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)$
88	57 84 86 87	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)$
89		eqid	$⊢ 0_{H} = 0_{H}$
90	1 62 89 2	grprinv	$⊢ (H \in Grp \land a T b \in B) \to (a T b) +_{H} N (a T b) = 0_{H}$
91	56 84 90	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}$
92	82 88 91	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}$
93	92	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}$
94	1	gsumwcl	$⊢ (H \in Mnd \land T \circ (x prefix n) \in Word B) \to \sum_{H} (T \circ (x prefix n)) \in B$
95	57 59 94	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$
96	1 62 89	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))$
97	56 95 96	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))$
98	93 97	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))$
99	55 64 98	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⟩ ”⟩))$
100	99	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\|⟩)))$
101		swrdcl	$⊢ x \in Word (I \times 2_{𝑜}) \to x substr ⟨n, \|x\|⟩ \in Word (I \times 2_{𝑜})$
102	35 101	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_{𝑜})$
103		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$
104	102 52 103	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$
105	1 62	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\|⟩)))$
106	57 59 104 105	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\|⟩)))$
107		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_{𝑜})$
108	50 42 107	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_{𝑜})$
109		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$
110	108 52 109	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$
111	1 62	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\|⟩)))$
112	57 110 104 111	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\|⟩)))$
113	100 106 112	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\|⟩)))$
114		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\|)$
115		lencl	$⊢ x \in Word (I \times 2_{𝑜}) \to \|x\| \in ℕ_{0}$
116	35 115	syl	$⊢ ((φ \land (x \in W \land n \in (0 \dots \|x\|))) \land (a \in I \land b \in 2_{𝑜})) \to \|x\| \in ℕ_{0}$
117		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
118	116 117	eleqtrdi	$⊢ ((φ \land (x \in W \land n \in (0 \dots \|x\|))) \land (a \in I \land b \in 2_{𝑜})) \to \|x\| \in ℤ_{\geq 0}$
119		eluzfz2	$⊢ \|x\| \in ℤ_{\geq 0} \to \|x\| \in (0 \dots \|x\|)$
120	118 119	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\|)$
121		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\|$
122	35 114 120 121	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\|$
123		pfxid	$⊢ x \in Word (I \times 2_{𝑜}) \to x prefix \|x\| = x$
124	35 123	syl	$⊢ ((φ \land (x \in W \land n \in (0 \dots \|x\|))) \land (a \in I \land b \in 2_{𝑜})) \to x prefix \|x\| = x$
125	122 124	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$
126	125	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$
127		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\|⟩))$
128	50 102 52 127	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\|⟩))$
129	126 128	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\|⟩))$
130	129	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\|⟩)))$
131		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\|⟩)$
132	32 114 114 42 131	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\|⟩)$
133	132	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\|⟩))$
134		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\|⟩))$
135	108 102 52 134	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\|⟩))$
136	133 135	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\|⟩))$
137	136	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\|⟩)))$
138	113 130 137	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⟩ ”⟩⟩))$
139		vex	$⊢ x \in V$
140		ovex	$⊢ x splice ⟨n, n, ⟨“ ⟨a, b⟩ ⟨a, 1_{𝑜} ∖ b⟩ ”⟩⟩ \in V$
141		eleq1	$⊢ u = x \to (u \in W \leftrightarrow x \in W)$
142		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)$
143	141 142	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))$
144	25 143	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))$
145		coeq2	$⊢ u = x \to T \circ u = T \circ x$
146	145	oveq2d	$⊢ u = x \to \sum_{H} (T \circ u) = \sum_{H} (T \circ x)$
147		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⟩ ”⟩⟩)$
148	147	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⟩ ”⟩⟩))$
149	146 148	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⟩ ”⟩⟩)))$
150	144 149	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⟩ ”⟩⟩))))$
151		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))\}$
152	139 140 150 151	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⟩ ”⟩⟩)))$
153	32 48 138 152	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⟩ ”⟩⟩)$
154	153	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⟩ ”⟩⟩)$
155	154	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⟩ ”⟩⟩)$
156	7	fvexi	$⊢ W \in V$
157		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)$
158	31 156 157	mpisyl	$⊢ φ \to \{⟨u, v⟩ \| (\{u, v\} \subseteq W \land \sum_{H} (T \circ u) = \sum_{H} (T \circ v))\} \in V$
159		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)$
160		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⟩ ”⟩⟩))$
161	160	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⟩ ”⟩⟩))$
162	161	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⟩ ”⟩⟩))$
163	159 162	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⟩ ”⟩⟩)))$
164	163	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⟩ ”⟩⟩)))$
165	158 164	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⟩ ”⟩⟩)))$
166	31 155 165	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⟩ ”⟩⟩))\}$
167		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))\}$
168	166 167	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))\}$
169	9 168	eqsstrid	$⊢ φ \to \underset{˙}{\sim} \subseteq \{⟨u, v⟩ \| (\{u, v\} \subseteq W \land \sum_{H} (T \circ u) = \sum_{H} (T \circ v))\}$
170	169	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)$
171	170	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$
172	7 8	efger	$⊢ \underset{˙}{\sim} Er W$
173		errel	$⊢ \underset{˙}{\sim} Er W \to Rel \underset{˙}{\sim}$
174	172 173	mp1i	$⊢ φ \to Rel \underset{˙}{\sim}$
175		brrelex12	$⊢ (Rel \underset{˙}{\sim} \land A \underset{˙}{\sim} C) \to (A \in V \land C \in V)$
176	174 175	sylan	$⊢ (φ \land A \underset{˙}{\sim} C) \to (A \in V \land C \in V)$
177		preq12	$⊢ (u = A \land v = C) \to \{u, v\} = \{A, C\}$
178	177	sseq1d	$⊢ (u = A \land v = C) \to (\{u, v\} \subseteq W \leftrightarrow \{A, C\} \subseteq W)$
179		coeq2	$⊢ u = A \to T \circ u = T \circ A$
180	179	oveq2d	$⊢ u = A \to \sum_{H} (T \circ u) = \sum_{H} (T \circ A)$
181		coeq2	$⊢ v = C \to T \circ v = T \circ C$
182	181	oveq2d	$⊢ v = C \to \sum_{H} (T \circ v) = \sum_{H} (T \circ C)$
183	180 182	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))$
184	178 183	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)))$
185	184 151	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)))$
186	176 185	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)))$
187	171 186	mpbid	$⊢ (φ \land A \underset{˙}{\sim} C) \to (\{A, C\} \subseteq W \land \sum_{H} (T \circ A) = \sum_{H} (T \circ C))$
188	187	simprd	$⊢ (φ \land A \underset{˙}{\sim} C) \to \sum_{H} (T \circ A) = \sum_{H} (T \circ C)$

Metamath Proof Explorer

Theorem frgpuplem

Proof