frgpup3lem

Description: The evaluation map has the intended behavior on the generators. (Contributed by Mario Carneiro, 2-Oct-2015) (Revised by Mario Carneiro, 28-Feb-2016)

	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)$
	frgpup.g	$⊢ G = freeGrp (I)$
	frgpup.x	$⊢ X = {Base}_{G}$
	frgpup.e	$⊢ E = ran (g \in W ⟼ ⟨[g] \underset{˙}{\sim}, \sum_{H} (T \circ g)⟩)$
	frgpup.u	$⊢ U = {var}_{FGrp} (I)$
	frgpup3.k	$⊢ φ \to K \in (G GrpHom H)$
	frgpup3.e	$⊢ φ \to K \circ U = F$
Assertion	frgpup3lem	$⊢ φ \to K = E$

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		frgpup.g	$⊢ G = freeGrp (I)$
10		frgpup.x	$⊢ X = {Base}_{G}$
11		frgpup.e	$⊢ E = ran (g \in W ⟼ ⟨[g] \underset{˙}{\sim}, \sum_{H} (T \circ g)⟩)$
12		frgpup.u	$⊢ U = {var}_{FGrp} (I)$
13		frgpup3.k	$⊢ φ \to K \in (G GrpHom H)$
14		frgpup3.e	$⊢ φ \to K \circ U = F$
15	10 1	ghmf	$⊢ K \in (G GrpHom H) \to K : X ⟶ B$
16		ffn	$⊢ K : X ⟶ B \to K Fn X$
17	13 15 16	3syl	$⊢ φ \to K Fn X$
18	1 2 3 4 5 6 7 8 9 10 11	frgpup1	$⊢ φ \to E \in (G GrpHom H)$
19	10 1	ghmf	$⊢ E \in (G GrpHom H) \to E : X ⟶ B$
20		ffn	$⊢ E : X ⟶ B \to E Fn X$
21	18 19 20	3syl	$⊢ φ \to E Fn X$
22		eqid	$⊢ freeMnd (I \times 2_{𝑜}) = freeMnd (I \times 2_{𝑜})$
23	9 22 8	frgpval	$⊢ I \in V \to G = freeMnd (I \times 2_{𝑜}) /_{𝑠} \underset{˙}{\sim}$
24	5 23	syl	$⊢ φ \to G = freeMnd (I \times 2_{𝑜}) /_{𝑠} \underset{˙}{\sim}$
25		2on	$⊢ 2_{𝑜} \in On$
26		xpexg	$⊢ (I \in V \land 2_{𝑜} \in On) \to I \times 2_{𝑜} \in V$
27	5 25 26	sylancl	$⊢ φ \to I \times 2_{𝑜} \in V$
28		wrdexg	$⊢ I \times 2_{𝑜} \in V \to Word (I \times 2_{𝑜}) \in V$
29		fvi	$⊢ Word (I \times 2_{𝑜}) \in V \to I (Word (I \times 2_{𝑜})) = Word (I \times 2_{𝑜})$
30	27 28 29	3syl	$⊢ φ \to I (Word (I \times 2_{𝑜})) = Word (I \times 2_{𝑜})$
31	7 30	eqtrid	$⊢ φ \to W = Word (I \times 2_{𝑜})$
32		eqid	$⊢ {Base}_{freeMnd (I \times 2_{𝑜})} = {Base}_{freeMnd (I \times 2_{𝑜})}$
33	22 32	frmdbas	$⊢ I \times 2_{𝑜} \in V \to {Base}_{freeMnd (I \times 2_{𝑜})} = Word (I \times 2_{𝑜})$
34	27 33	syl	$⊢ φ \to {Base}_{freeMnd (I \times 2_{𝑜})} = Word (I \times 2_{𝑜})$
35	31 34	eqtr4d	$⊢ φ \to W = {Base}_{freeMnd (I \times 2_{𝑜})}$
36	8	fvexi	$⊢ \underset{˙}{\sim} \in V$
37	36	a1i	$⊢ φ \to \underset{˙}{\sim} \in V$
38		fvexd	$⊢ φ \to freeMnd (I \times 2_{𝑜}) \in V$
39	24 35 37 38	qusbas	$⊢ φ \to W / \underset{˙}{\sim} = {Base}_{G}$
40	10 39	eqtr4id	$⊢ φ \to X = W / \underset{˙}{\sim}$
41		eqimss	$⊢ X = W / \underset{˙}{\sim} \to X \subseteq W / \underset{˙}{\sim}$
42	40 41	syl	$⊢ φ \to X \subseteq W / \underset{˙}{\sim}$
43	42	sselda	$⊢ (φ \land a \in X) \to a \in (W / \underset{˙}{\sim})$
44		eqid	$⊢ W / \underset{˙}{\sim} = W / \underset{˙}{\sim}$
45		fveq2	$⊢ [t] \underset{˙}{\sim} = a \to K ([t] \underset{˙}{\sim}) = K (a)$
46		fveq2	$⊢ [t] \underset{˙}{\sim} = a \to E ([t] \underset{˙}{\sim}) = E (a)$
47	45 46	eqeq12d	$⊢ [t] \underset{˙}{\sim} = a \to (K ([t] \underset{˙}{\sim}) = E ([t] \underset{˙}{\sim}) \leftrightarrow K (a) = E (a))$
48		simpr	$⊢ (φ \land t \in W) \to t \in W$
49	31	adantr	$⊢ (φ \land t \in W) \to W = Word (I \times 2_{𝑜})$
50	48 49	eleqtrd	$⊢ (φ \land t \in W) \to t \in Word (I \times 2_{𝑜})$
51		wrdf	$⊢ t \in Word (I \times 2_{𝑜}) \to t : (0 ..^\|t\|) ⟶ I \times 2_{𝑜}$
52	50 51	syl	$⊢ (φ \land t \in W) \to t : (0 ..^\|t\|) ⟶ I \times 2_{𝑜}$
53	52	ffvelrnda	$⊢ ((φ \land t \in W) \land n \in (0 ..^\|t\|)) \to t (n) \in (I \times 2_{𝑜})$
54		elxp2	$⊢ t (n) \in (I \times 2_{𝑜}) \leftrightarrow \exists i \in I \exists j \in 2_{𝑜} t (n) = ⟨i, j⟩$
55	53 54	sylib	$⊢ ((φ \land t \in W) \land n \in (0 ..^\|t\|)) \to \exists i \in I \exists j \in 2_{𝑜} t (n) = ⟨i, j⟩$
56		fveq2	$⊢ y = i \to F (y) = F (i)$
57	56	fveq2d	$⊢ y = i \to N (F (y)) = N (F (i))$
58	56 57	ifeq12d	$⊢ y = i \to if (z = \emptyset, F (y), N (F (y))) = if (z = \emptyset, F (i), N (F (i)))$
59		eqeq1	$⊢ z = j \to (z = \emptyset \leftrightarrow j = \emptyset)$
60	59	ifbid	$⊢ z = j \to if (z = \emptyset, F (i), N (F (i))) = if (j = \emptyset, F (i), N (F (i)))$
61		fvex	$⊢ F (i) \in V$
62		fvex	$⊢ N (F (i)) \in V$
63	61 62	ifex	$⊢ if (j = \emptyset, F (i), N (F (i))) \in V$
64	58 60 3 63	ovmpo	$⊢ (i \in I \land j \in 2_{𝑜}) \to i T j = if (j = \emptyset, F (i), N (F (i)))$
65	64	adantl	$⊢ (φ \land (i \in I \land j \in 2_{𝑜})) \to i T j = if (j = \emptyset, F (i), N (F (i)))$
66		elpri	$⊢ j \in \{\emptyset, 1_{𝑜}\} \to (j = \emptyset \lor j = 1_{𝑜})$
67		df2o3	$⊢ 2_{𝑜} = \{\emptyset, 1_{𝑜}\}$
68	66 67	eleq2s	$⊢ j \in 2_{𝑜} \to (j = \emptyset \lor j = 1_{𝑜})$
69	14	adantr	$⊢ (φ \land i \in I) \to K \circ U = F$
70	69	fveq1d	$⊢ (φ \land i \in I) \to (K \circ U) (i) = F (i)$
71	8 12 9 10	vrgpf	$⊢ I \in V \to U : I ⟶ X$
72	5 71	syl	$⊢ φ \to U : I ⟶ X$
73		fvco3	$⊢ (U : I ⟶ X \land i \in I) \to (K \circ U) (i) = K (U (i))$
74	72 73	sylan	$⊢ (φ \land i \in I) \to (K \circ U) (i) = K (U (i))$
75	70 74	eqtr3d	$⊢ (φ \land i \in I) \to F (i) = K (U (i))$
76	75	adantr	$⊢ ((φ \land i \in I) \land j = \emptyset) \to F (i) = K (U (i))$
77		iftrue	$⊢ j = \emptyset \to if (j = \emptyset, F (i), N (F (i))) = F (i)$
78	77	adantl	$⊢ ((φ \land i \in I) \land j = \emptyset) \to if (j = \emptyset, F (i), N (F (i))) = F (i)$
79		simpr	$⊢ ((φ \land i \in I) \land j = \emptyset) \to j = \emptyset$
80	79	opeq2d	$⊢ ((φ \land i \in I) \land j = \emptyset) \to ⟨i, j⟩ = ⟨i, \emptyset⟩$
81	80	s1eqd	$⊢ ((φ \land i \in I) \land j = \emptyset) \to ⟨“ ⟨i, j⟩ ”⟩ = ⟨“ ⟨i, \emptyset⟩ ”⟩$
82	81	eceq1d	$⊢ ((φ \land i \in I) \land j = \emptyset) \to [⟨“ ⟨i, j⟩ ”⟩] \underset{˙}{\sim} = [⟨“ ⟨i, \emptyset⟩ ”⟩] \underset{˙}{\sim}$
83	8 12	vrgpval	$⊢ (I \in V \land i \in I) \to U (i) = [⟨“ ⟨i, \emptyset⟩ ”⟩] \underset{˙}{\sim}$
84	5 83	sylan	$⊢ (φ \land i \in I) \to U (i) = [⟨“ ⟨i, \emptyset⟩ ”⟩] \underset{˙}{\sim}$
85	84	adantr	$⊢ ((φ \land i \in I) \land j = \emptyset) \to U (i) = [⟨“ ⟨i, \emptyset⟩ ”⟩] \underset{˙}{\sim}$
86	82 85	eqtr4d	$⊢ ((φ \land i \in I) \land j = \emptyset) \to [⟨“ ⟨i, j⟩ ”⟩] \underset{˙}{\sim} = U (i)$
87	86	fveq2d	$⊢ ((φ \land i \in I) \land j = \emptyset) \to K ([⟨“ ⟨i, j⟩ ”⟩] \underset{˙}{\sim}) = K (U (i))$
88	76 78 87	3eqtr4d	$⊢ ((φ \land i \in I) \land j = \emptyset) \to if (j = \emptyset, F (i), N (F (i))) = K ([⟨“ ⟨i, j⟩ ”⟩] \underset{˙}{\sim})$
89	75	fveq2d	$⊢ (φ \land i \in I) \to N (F (i)) = N (K (U (i)))$
90	72	ffvelrnda	$⊢ (φ \land i \in I) \to U (i) \in X$
91		eqid	$⊢ {inv}_{g} (G) = {inv}_{g} (G)$
92	10 91 2	ghminv	$⊢ (K \in (G GrpHom H) \land U (i) \in X) \to K ({inv}_{g} (G) (U (i))) = N (K (U (i)))$
93	13 90 92	syl2an2r	$⊢ (φ \land i \in I) \to K ({inv}_{g} (G) (U (i))) = N (K (U (i)))$
94	89 93	eqtr4d	$⊢ (φ \land i \in I) \to N (F (i)) = K ({inv}_{g} (G) (U (i)))$
95	94	adantr	$⊢ ((φ \land i \in I) \land j = 1_{𝑜}) \to N (F (i)) = K ({inv}_{g} (G) (U (i)))$
96		1n0	$⊢ 1_{𝑜} \neq \emptyset$
97		simpr	$⊢ ((φ \land i \in I) \land j = 1_{𝑜}) \to j = 1_{𝑜}$
98	97	neeq1d	$⊢ ((φ \land i \in I) \land j = 1_{𝑜}) \to (j \neq \emptyset \leftrightarrow 1_{𝑜} \neq \emptyset)$
99	96 98	mpbiri	$⊢ ((φ \land i \in I) \land j = 1_{𝑜}) \to j \neq \emptyset$
100		ifnefalse	$⊢ j \neq \emptyset \to if (j = \emptyset, F (i), N (F (i))) = N (F (i))$
101	99 100	syl	$⊢ ((φ \land i \in I) \land j = 1_{𝑜}) \to if (j = \emptyset, F (i), N (F (i))) = N (F (i))$
102	97	opeq2d	$⊢ ((φ \land i \in I) \land j = 1_{𝑜}) \to ⟨i, j⟩ = ⟨i, 1_{𝑜}⟩$
103	102	s1eqd	$⊢ ((φ \land i \in I) \land j = 1_{𝑜}) \to ⟨“ ⟨i, j⟩ ”⟩ = ⟨“ ⟨i, 1_{𝑜}⟩ ”⟩$
104	103	eceq1d	$⊢ ((φ \land i \in I) \land j = 1_{𝑜}) \to [⟨“ ⟨i, j⟩ ”⟩] \underset{˙}{\sim} = [⟨“ ⟨i, 1_{𝑜}⟩ ”⟩] \underset{˙}{\sim}$
105	8 12 9 91	vrgpinv	$⊢ (I \in V \land i \in I) \to {inv}_{g} (G) (U (i)) = [⟨“ ⟨i, 1_{𝑜}⟩ ”⟩] \underset{˙}{\sim}$
106	5 105	sylan	$⊢ (φ \land i \in I) \to {inv}_{g} (G) (U (i)) = [⟨“ ⟨i, 1_{𝑜}⟩ ”⟩] \underset{˙}{\sim}$
107	106	adantr	$⊢ ((φ \land i \in I) \land j = 1_{𝑜}) \to {inv}_{g} (G) (U (i)) = [⟨“ ⟨i, 1_{𝑜}⟩ ”⟩] \underset{˙}{\sim}$
108	104 107	eqtr4d	$⊢ ((φ \land i \in I) \land j = 1_{𝑜}) \to [⟨“ ⟨i, j⟩ ”⟩] \underset{˙}{\sim} = {inv}_{g} (G) (U (i))$
109	108	fveq2d	$⊢ ((φ \land i \in I) \land j = 1_{𝑜}) \to K ([⟨“ ⟨i, j⟩ ”⟩] \underset{˙}{\sim}) = K ({inv}_{g} (G) (U (i)))$
110	95 101 109	3eqtr4d	$⊢ ((φ \land i \in I) \land j = 1_{𝑜}) \to if (j = \emptyset, F (i), N (F (i))) = K ([⟨“ ⟨i, j⟩ ”⟩] \underset{˙}{\sim})$
111	88 110	jaodan	$⊢ ((φ \land i \in I) \land (j = \emptyset \lor j = 1_{𝑜})) \to if (j = \emptyset, F (i), N (F (i))) = K ([⟨“ ⟨i, j⟩ ”⟩] \underset{˙}{\sim})$
112	68 111	sylan2	$⊢ ((φ \land i \in I) \land j \in 2_{𝑜}) \to if (j = \emptyset, F (i), N (F (i))) = K ([⟨“ ⟨i, j⟩ ”⟩] \underset{˙}{\sim})$
113	112	anasss	$⊢ (φ \land (i \in I \land j \in 2_{𝑜})) \to if (j = \emptyset, F (i), N (F (i))) = K ([⟨“ ⟨i, j⟩ ”⟩] \underset{˙}{\sim})$
114	65 113	eqtrd	$⊢ (φ \land (i \in I \land j \in 2_{𝑜})) \to i T j = K ([⟨“ ⟨i, j⟩ ”⟩] \underset{˙}{\sim})$
115		fveq2	$⊢ t (n) = ⟨i, j⟩ \to T (t (n)) = T (⟨i, j⟩)$
116		df-ov	$⊢ i T j = T (⟨i, j⟩)$
117	115 116	eqtr4di	$⊢ t (n) = ⟨i, j⟩ \to T (t (n)) = i T j$
118		s1eq	$⊢ t (n) = ⟨i, j⟩ \to ⟨“ t (n) ”⟩ = ⟨“ ⟨i, j⟩ ”⟩$
119	118	eceq1d	$⊢ t (n) = ⟨i, j⟩ \to [⟨“ t (n) ”⟩] \underset{˙}{\sim} = [⟨“ ⟨i, j⟩ ”⟩] \underset{˙}{\sim}$
120	119	fveq2d	$⊢ t (n) = ⟨i, j⟩ \to K ([⟨“ t (n) ”⟩] \underset{˙}{\sim}) = K ([⟨“ ⟨i, j⟩ ”⟩] \underset{˙}{\sim})$
121	117 120	eqeq12d	$⊢ t (n) = ⟨i, j⟩ \to (T (t (n)) = K ([⟨“ t (n) ”⟩] \underset{˙}{\sim}) \leftrightarrow i T j = K ([⟨“ ⟨i, j⟩ ”⟩] \underset{˙}{\sim}))$
122	114 121	syl5ibrcom	$⊢ (φ \land (i \in I \land j \in 2_{𝑜})) \to (t (n) = ⟨i, j⟩ \to T (t (n)) = K ([⟨“ t (n) ”⟩] \underset{˙}{\sim}))$
123	122	rexlimdvva	$⊢ φ \to (\exists i \in I \exists j \in 2_{𝑜} t (n) = ⟨i, j⟩ \to T (t (n)) = K ([⟨“ t (n) ”⟩] \underset{˙}{\sim}))$
124	123	ad2antrr	$⊢ ((φ \land t \in W) \land n \in (0 ..^\|t\|)) \to (\exists i \in I \exists j \in 2_{𝑜} t (n) = ⟨i, j⟩ \to T (t (n)) = K ([⟨“ t (n) ”⟩] \underset{˙}{\sim}))$
125	55 124	mpd	$⊢ ((φ \land t \in W) \land n \in (0 ..^\|t\|)) \to T (t (n)) = K ([⟨“ t (n) ”⟩] \underset{˙}{\sim})$
126	125	mpteq2dva	$⊢ (φ \land t \in W) \to (n \in (0 ..^\|t\|) ⟼ T (t (n))) = (n \in (0 ..^\|t\|) ⟼ K ([⟨“ t (n) ”⟩] \underset{˙}{\sim}))$
127	1 2 3 4 5 6	frgpuptf	$⊢ φ \to T : I \times 2_{𝑜} ⟶ B$
128		fcompt	$⊢ (T : I \times 2_{𝑜} ⟶ B \land t : (0 ..^\|t\|) ⟶ I \times 2_{𝑜}) \to T \circ t = (n \in (0 ..^\|t\|) ⟼ T (t (n)))$
129	127 52 128	syl2an2r	$⊢ (φ \land t \in W) \to T \circ t = (n \in (0 ..^\|t\|) ⟼ T (t (n)))$
130	53	s1cld	$⊢ ((φ \land t \in W) \land n \in (0 ..^\|t\|)) \to ⟨“ t (n) ”⟩ \in Word (I \times 2_{𝑜})$
131	31	ad2antrr	$⊢ ((φ \land t \in W) \land n \in (0 ..^\|t\|)) \to W = Word (I \times 2_{𝑜})$
132	130 131	eleqtrrd	$⊢ ((φ \land t \in W) \land n \in (0 ..^\|t\|)) \to ⟨“ t (n) ”⟩ \in W$
133	9 8 7 10	frgpeccl	$⊢ ⟨“ t (n) ”⟩ \in W \to [⟨“ t (n) ”⟩] \underset{˙}{\sim} \in X$
134	132 133	syl	$⊢ ((φ \land t \in W) \land n \in (0 ..^\|t\|)) \to [⟨“ t (n) ”⟩] \underset{˙}{\sim} \in X$
135	52	feqmptd	$⊢ (φ \land t \in W) \to t = (n \in (0 ..^\|t\|) ⟼ t (n))$
136	5	adantr	$⊢ (φ \land t \in W) \to I \in V$
137	136 25 26	sylancl	$⊢ (φ \land t \in W) \to I \times 2_{𝑜} \in V$
138		eqid	$⊢ {var}_{FMnd} (I \times 2_{𝑜}) = {var}_{FMnd} (I \times 2_{𝑜})$
139	138	vrmdfval	$⊢ I \times 2_{𝑜} \in V \to {var}_{FMnd} (I \times 2_{𝑜}) = (w \in (I \times 2_{𝑜}) ⟼ ⟨“ w ”⟩)$
140	137 139	syl	$⊢ (φ \land t \in W) \to {var}_{FMnd} (I \times 2_{𝑜}) = (w \in (I \times 2_{𝑜}) ⟼ ⟨“ w ”⟩)$
141		s1eq	$⊢ w = t (n) \to ⟨“ w ”⟩ = ⟨“ t (n) ”⟩$
142	53 135 140 141	fmptco	$⊢ (φ \land t \in W) \to {var}_{FMnd} (I \times 2_{𝑜}) \circ t = (n \in (0 ..^\|t\|) ⟼ ⟨“ t (n) ”⟩)$
143		eqidd	$⊢ (φ \land t \in W) \to (w \in W ⟼ [w] \underset{˙}{\sim}) = (w \in W ⟼ [w] \underset{˙}{\sim})$
144		eceq1	$⊢ w = ⟨“ t (n) ”⟩ \to [w] \underset{˙}{\sim} = [⟨“ t (n) ”⟩] \underset{˙}{\sim}$
145	132 142 143 144	fmptco	$⊢ (φ \land t \in W) \to (w \in W ⟼ [w] \underset{˙}{\sim}) \circ ({var}_{FMnd} (I \times 2_{𝑜}) \circ t) = (n \in (0 ..^\|t\|) ⟼ [⟨“ t (n) ”⟩] \underset{˙}{\sim})$
146	13	adantr	$⊢ (φ \land t \in W) \to K \in (G GrpHom H)$
147	146 15	syl	$⊢ (φ \land t \in W) \to K : X ⟶ B$
148	147	feqmptd	$⊢ (φ \land t \in W) \to K = (w \in X ⟼ K (w))$
149		fveq2	$⊢ w = [⟨“ t (n) ”⟩] \underset{˙}{\sim} \to K (w) = K ([⟨“ t (n) ”⟩] \underset{˙}{\sim})$
150	134 145 148 149	fmptco	$⊢ (φ \land t \in W) \to K \circ ((w \in W ⟼ [w] \underset{˙}{\sim}) \circ ({var}_{FMnd} (I \times 2_{𝑜}) \circ t)) = (n \in (0 ..^\|t\|) ⟼ K ([⟨“ t (n) ”⟩] \underset{˙}{\sim}))$
151	126 129 150	3eqtr4d	$⊢ (φ \land t \in W) \to T \circ t = K \circ ((w \in W ⟼ [w] \underset{˙}{\sim}) \circ ({var}_{FMnd} (I \times 2_{𝑜}) \circ t))$
152	151	oveq2d	$⊢ (φ \land t \in W) \to \sum_{H} (T \circ t) = \sum_{H} (K \circ ((w \in W ⟼ [w] \underset{˙}{\sim}) \circ ({var}_{FMnd} (I \times 2_{𝑜}) \circ t)))$
153	1 2 3 4 5 6 7 8 9 10 11	frgpupval	$⊢ (φ \land t \in W) \to E ([t] \underset{˙}{\sim}) = \sum_{H} (T \circ t)$
154		ghmmhm	$⊢ K \in (G GrpHom H) \to K \in (G MndHom H)$
155	146 154	syl	$⊢ (φ \land t \in W) \to K \in (G MndHom H)$
156	138	vrmdf	$⊢ I \times 2_{𝑜} \in V \to {var}_{FMnd} (I \times 2_{𝑜}) : I \times 2_{𝑜} ⟶ Word (I \times 2_{𝑜})$
157	137 156	syl	$⊢ (φ \land t \in W) \to {var}_{FMnd} (I \times 2_{𝑜}) : I \times 2_{𝑜} ⟶ Word (I \times 2_{𝑜})$
158	49	feq3d	$⊢ (φ \land t \in W) \to ({var}_{FMnd} (I \times 2_{𝑜}) : I \times 2_{𝑜} ⟶ W \leftrightarrow {var}_{FMnd} (I \times 2_{𝑜}) : I \times 2_{𝑜} ⟶ Word (I \times 2_{𝑜}))$
159	157 158	mpbird	$⊢ (φ \land t \in W) \to {var}_{FMnd} (I \times 2_{𝑜}) : I \times 2_{𝑜} ⟶ W$
160		wrdco	$⊢ (t \in Word (I \times 2_{𝑜}) \land {var}_{FMnd} (I \times 2_{𝑜}) : I \times 2_{𝑜} ⟶ W) \to {var}_{FMnd} (I \times 2_{𝑜}) \circ t \in Word W$
161	50 159 160	syl2anc	$⊢ (φ \land t \in W) \to {var}_{FMnd} (I \times 2_{𝑜}) \circ t \in Word W$
162	35	adantr	$⊢ (φ \land t \in W) \to W = {Base}_{freeMnd (I \times 2_{𝑜})}$
163	162	mpteq1d	$⊢ (φ \land t \in W) \to (w \in W ⟼ [w] \underset{˙}{\sim}) = (w \in {Base}_{freeMnd (I \times 2_{𝑜})} ⟼ [w] \underset{˙}{\sim})$
164		eqid	$⊢ (w \in {Base}_{freeMnd (I \times 2_{𝑜})} ⟼ [w] \underset{˙}{\sim}) = (w \in {Base}_{freeMnd (I \times 2_{𝑜})} ⟼ [w] \underset{˙}{\sim})$
165	22 32 9 8 164	frgpmhm	$⊢ I \in V \to (w \in {Base}_{freeMnd (I \times 2_{𝑜})} ⟼ [w] \underset{˙}{\sim}) \in (freeMnd (I \times 2_{𝑜}) MndHom G)$
166	136 165	syl	$⊢ (φ \land t \in W) \to (w \in {Base}_{freeMnd (I \times 2_{𝑜})} ⟼ [w] \underset{˙}{\sim}) \in (freeMnd (I \times 2_{𝑜}) MndHom G)$
167	163 166	eqeltrd	$⊢ (φ \land t \in W) \to (w \in W ⟼ [w] \underset{˙}{\sim}) \in (freeMnd (I \times 2_{𝑜}) MndHom G)$
168	32 10	mhmf	$⊢ (w \in W ⟼ [w] \underset{˙}{\sim}) \in (freeMnd (I \times 2_{𝑜}) MndHom G) \to (w \in W ⟼ [w] \underset{˙}{\sim}) : {Base}_{freeMnd (I \times 2_{𝑜})} ⟶ X$
169	167 168	syl	$⊢ (φ \land t \in W) \to (w \in W ⟼ [w] \underset{˙}{\sim}) : {Base}_{freeMnd (I \times 2_{𝑜})} ⟶ X$
170	162	feq2d	$⊢ (φ \land t \in W) \to ((w \in W ⟼ [w] \underset{˙}{\sim}) : W ⟶ X \leftrightarrow (w \in W ⟼ [w] \underset{˙}{\sim}) : {Base}_{freeMnd (I \times 2_{𝑜})} ⟶ X)$
171	169 170	mpbird	$⊢ (φ \land t \in W) \to (w \in W ⟼ [w] \underset{˙}{\sim}) : W ⟶ X$
172		wrdco	$⊢ ({var}_{FMnd} (I \times 2_{𝑜}) \circ t \in Word W \land (w \in W ⟼ [w] \underset{˙}{\sim}) : W ⟶ X) \to (w \in W ⟼ [w] \underset{˙}{\sim}) \circ ({var}_{FMnd} (I \times 2_{𝑜}) \circ t) \in Word X$
173	161 171 172	syl2anc	$⊢ (φ \land t \in W) \to (w \in W ⟼ [w] \underset{˙}{\sim}) \circ ({var}_{FMnd} (I \times 2_{𝑜}) \circ t) \in Word X$
174	10	gsumwmhm	$⊢ (K \in (G MndHom H) \land (w \in W ⟼ [w] \underset{˙}{\sim}) \circ ({var}_{FMnd} (I \times 2_{𝑜}) \circ t) \in Word X) \to K (\sum_{G} ((w \in W ⟼ [w] \underset{˙}{\sim}) \circ ({var}_{FMnd} (I \times 2_{𝑜}) \circ t))) = \sum_{H} (K \circ ((w \in W ⟼ [w] \underset{˙}{\sim}) \circ ({var}_{FMnd} (I \times 2_{𝑜}) \circ t)))$
175	155 173 174	syl2anc	$⊢ (φ \land t \in W) \to K (\sum_{G} ((w \in W ⟼ [w] \underset{˙}{\sim}) \circ ({var}_{FMnd} (I \times 2_{𝑜}) \circ t))) = \sum_{H} (K \circ ((w \in W ⟼ [w] \underset{˙}{\sim}) \circ ({var}_{FMnd} (I \times 2_{𝑜}) \circ t)))$
176	152 153 175	3eqtr4d	$⊢ (φ \land t \in W) \to E ([t] \underset{˙}{\sim}) = K (\sum_{G} ((w \in W ⟼ [w] \underset{˙}{\sim}) \circ ({var}_{FMnd} (I \times 2_{𝑜}) \circ t)))$
177	22 138	frmdgsum	$⊢ (I \times 2_{𝑜} \in V \land t \in Word (I \times 2_{𝑜})) \to \sum_{freeMnd (I \times 2_{𝑜})} ({var}_{FMnd} (I \times 2_{𝑜}) \circ t) = t$
178	27 50 177	syl2an2r	$⊢ (φ \land t \in W) \to \sum_{freeMnd (I \times 2_{𝑜})} ({var}_{FMnd} (I \times 2_{𝑜}) \circ t) = t$
179	178	fveq2d	$⊢ (φ \land t \in W) \to (w \in W ⟼ [w] \underset{˙}{\sim}) (\sum_{freeMnd (I \times 2_{𝑜})} ({var}_{FMnd} (I \times 2_{𝑜}) \circ t)) = (w \in W ⟼ [w] \underset{˙}{\sim}) (t)$
180		wrdco	$⊢ (t \in Word (I \times 2_{𝑜}) \land {var}_{FMnd} (I \times 2_{𝑜}) : I \times 2_{𝑜} ⟶ Word (I \times 2_{𝑜})) \to {var}_{FMnd} (I \times 2_{𝑜}) \circ t \in Word Word (I \times 2_{𝑜})$
181	50 157 180	syl2anc	$⊢ (φ \land t \in W) \to {var}_{FMnd} (I \times 2_{𝑜}) \circ t \in Word Word (I \times 2_{𝑜})$
182	34	adantr	$⊢ (φ \land t \in W) \to {Base}_{freeMnd (I \times 2_{𝑜})} = Word (I \times 2_{𝑜})$
183		wrdeq	$⊢ {Base}_{freeMnd (I \times 2_{𝑜})} = Word (I \times 2_{𝑜}) \to Word {Base}_{freeMnd (I \times 2_{𝑜})} = Word Word (I \times 2_{𝑜})$
184	182 183	syl	$⊢ (φ \land t \in W) \to Word {Base}_{freeMnd (I \times 2_{𝑜})} = Word Word (I \times 2_{𝑜})$
185	181 184	eleqtrrd	$⊢ (φ \land t \in W) \to {var}_{FMnd} (I \times 2_{𝑜}) \circ t \in Word {Base}_{freeMnd (I \times 2_{𝑜})}$
186	32	gsumwmhm	$⊢ ((w \in W ⟼ [w] \underset{˙}{\sim}) \in (freeMnd (I \times 2_{𝑜}) MndHom G) \land {var}_{FMnd} (I \times 2_{𝑜}) \circ t \in Word {Base}_{freeMnd (I \times 2_{𝑜})}) \to (w \in W ⟼ [w] \underset{˙}{\sim}) (\sum_{freeMnd (I \times 2_{𝑜})} ({var}_{FMnd} (I \times 2_{𝑜}) \circ t)) = \sum_{G} ((w \in W ⟼ [w] \underset{˙}{\sim}) \circ ({var}_{FMnd} (I \times 2_{𝑜}) \circ t))$
187	167 185 186	syl2anc	$⊢ (φ \land t \in W) \to (w \in W ⟼ [w] \underset{˙}{\sim}) (\sum_{freeMnd (I \times 2_{𝑜})} ({var}_{FMnd} (I \times 2_{𝑜}) \circ t)) = \sum_{G} ((w \in W ⟼ [w] \underset{˙}{\sim}) \circ ({var}_{FMnd} (I \times 2_{𝑜}) \circ t))$
188	7 8	efger	$⊢ \underset{˙}{\sim} Er W$
189	188	a1i	$⊢ (φ \land t \in W) \to \underset{˙}{\sim} Er W$
190	7	fvexi	$⊢ W \in V$
191	190	a1i	$⊢ (φ \land t \in W) \to W \in V$
192		eqid	$⊢ (w \in W ⟼ [w] \underset{˙}{\sim}) = (w \in W ⟼ [w] \underset{˙}{\sim})$
193	189 191 192	divsfval	$⊢ (φ \land t \in W) \to (w \in W ⟼ [w] \underset{˙}{\sim}) (t) = [t] \underset{˙}{\sim}$
194	179 187 193	3eqtr3d	$⊢ (φ \land t \in W) \to \sum_{G} ((w \in W ⟼ [w] \underset{˙}{\sim}) \circ ({var}_{FMnd} (I \times 2_{𝑜}) \circ t)) = [t] \underset{˙}{\sim}$
195	194	fveq2d	$⊢ (φ \land t \in W) \to K (\sum_{G} ((w \in W ⟼ [w] \underset{˙}{\sim}) \circ ({var}_{FMnd} (I \times 2_{𝑜}) \circ t))) = K ([t] \underset{˙}{\sim})$
196	176 195	eqtr2d	$⊢ (φ \land t \in W) \to K ([t] \underset{˙}{\sim}) = E ([t] \underset{˙}{\sim})$
197	44 47 196	ectocld	$⊢ (φ \land a \in (W / \underset{˙}{\sim})) \to K (a) = E (a)$
198	43 197	syldan	$⊢ (φ \land a \in X) \to K (a) = E (a)$
199	17 21 198	eqfnfvd	$⊢ φ \to K = E$

Metamath Proof Explorer

Theorem frgpup3lem

Proof