Theorem frgpup2

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={\mathrm{Base}}_H$$
	frgpup.n	$$⊢N={inv}_g\left(H\right)$$
	frgpup.t	$$⊢T=\left(y\in I,z\in 2_{𝑜}⟼if\left(z=\varnothing ,F\left(y\right),N\left(F\left(y\right)\right)\right)\right)$$
	frgpup.h	$$⊢\phi \to H\in \mathrm{Grp}$$
	frgpup.i	$$⊢\phi \to I\in V$$
	frgpup.a	$$⊢\phi \to F:I⟶B$$
	frgpup.w	$$⊢W=\mathrm{I}\left(\mathrm{Word}\left(I\times 2_{𝑜}\right)\right)$$
	frgpup.r	$$⊢\underset{\dot{}}{\sim }={~}_{\mathit{FG}}\left(I\right)$$
	frgpup.g	$$⊢G=\mathrm{freeGrp}\left(I\right)$$
	frgpup.x	$$⊢X={\mathrm{Base}}_G$$
	frgpup.e	$$⊢E=\mathrm{ran}\left(g\in W⟼⟨\left[g\right]\underset{\dot{}}{\sim },{\sum }_H\left(T\circ g\right)⟩\right)$$
	frgpup.u	$$⊢U={var}_{\mathit{FGrp}}\left(I\right)$$
	frgpup.y	$$⊢\phi \to A\in I$$
Assertion	frgpup2	$$⊢\phi \to E\left(U\left(A\right)\right)=F\left(A\right)$$

Proof

Step	Hyp	Ref	Expression
1		frgpup.b	$$⊢B={\mathrm{Base}}_H$$
2		frgpup.n	$$⊢N={inv}_g\left(H\right)$$
3		frgpup.t	$$⊢T=\left(y\in I,z\in 2_{𝑜}⟼if\left(z=\varnothing ,F\left(y\right),N\left(F\left(y\right)\right)\right)\right)$$
4		frgpup.h	$$⊢\phi \to H\in \mathrm{Grp}$$
5		frgpup.i	$$⊢\phi \to I\in V$$
6		frgpup.a	$$⊢\phi \to F:I⟶B$$
7		frgpup.w	$$⊢W=\mathrm{I}\left(\mathrm{Word}\left(I\times 2_{𝑜}\right)\right)$$
8		frgpup.r	$$⊢\underset{\dot{}}{\sim }={~}_{\mathit{FG}}\left(I\right)$$
9		frgpup.g	$$⊢G=\mathrm{freeGrp}\left(I\right)$$
10		frgpup.x	$$⊢X={\mathrm{Base}}_G$$
11		frgpup.e	$$⊢E=\mathrm{ran}\left(g\in W⟼⟨\left[g\right]\underset{\dot{}}{\sim },{\sum }_H\left(T\circ g\right)⟩\right)$$
12		frgpup.u	$$⊢U={var}_{\mathit{FGrp}}\left(I\right)$$
13		frgpup.y	$$⊢\phi \to A\in I$$
14	8 12	vrgpval	$$⊢\left(I\in V\wedge A\in I\right)\to U\left(A\right)=\left[⟨“⟨A,\varnothing ⟩”⟩\right]\underset{\dot{}}{\sim }$$
15	5 13 14	syl2anc	$$⊢\phi \to U\left(A\right)=\left[⟨“⟨A,\varnothing ⟩”⟩\right]\underset{\dot{}}{\sim }$$
16	15	fveq2d	$$⊢\phi \to E\left(U\left(A\right)\right)=E\left(\left[⟨“⟨A,\varnothing ⟩”⟩\right]\underset{\dot{}}{\sim }\right)$$
17		0ex	$$⊢\varnothing \in \mathrm{V}$$
18	17	prid1	$$⊢\varnothing \in \left\{\varnothing ,1_{𝑜}\right\}$$
19		df2o3	$$⊢2_{𝑜}=\left\{\varnothing ,1_{𝑜}\right\}$$
20	18 19	eleqtrri	$$⊢\varnothing \in 2_{𝑜}$$
21		opelxpi	$$⊢\left(A\in I\wedge \varnothing \in 2_{𝑜}\right)\to ⟨A,\varnothing ⟩\in \left(I\times 2_{𝑜}\right)$$
22	13 20 21	sylancl	$$⊢\phi \to ⟨A,\varnothing ⟩\in \left(I\times 2_{𝑜}\right)$$
23	22	s1cld	$$⊢\phi \to ⟨“⟨A,\varnothing ⟩”⟩\in \mathrm{Word}\left(I\times 2_{𝑜}\right)$$
24		2on	$$⊢2_{𝑜}\in \mathrm{On}$$
25		xpexg	$$⊢\left(I\in V\wedge 2_{𝑜}\in \mathrm{On}\right)\to I\times 2_{𝑜}\in \mathrm{V}$$
26	5 24 25	sylancl	$$⊢\phi \to I\times 2_{𝑜}\in \mathrm{V}$$
27		wrdexg	$$⊢I\times 2_{𝑜}\in \mathrm{V}\to \mathrm{Word}\left(I\times 2_{𝑜}\right)\in \mathrm{V}$$
28		fvi	$$⊢\mathrm{Word}\left(I\times 2_{𝑜}\right)\in \mathrm{V}\to \mathrm{I}\left(\mathrm{Word}\left(I\times 2_{𝑜}\right)\right)=\mathrm{Word}\left(I\times 2_{𝑜}\right)$$
29	26 27 28	3syl	$$⊢\phi \to \mathrm{I}\left(\mathrm{Word}\left(I\times 2_{𝑜}\right)\right)=\mathrm{Word}\left(I\times 2_{𝑜}\right)$$
30	7 29	syl5eq	$$⊢\phi \to W=\mathrm{Word}\left(I\times 2_{𝑜}\right)$$
31	23 30	eleqtrrd	$$⊢\phi \to ⟨“⟨A,\varnothing ⟩”⟩\in W$$
32	1 2 3 4 5 6 7 8 9 10 11	frgpupval	$$⊢\left(\phi \wedge ⟨“⟨A,\varnothing ⟩”⟩\in W\right)\to E\left(\left[⟨“⟨A,\varnothing ⟩”⟩\right]\underset{\dot{}}{\sim }\right)={\sum }_H\left(T\circ ⟨“⟨A,\varnothing ⟩”⟩\right)$$
33	31 32	mpdan	$$⊢\phi \to E\left(\left[⟨“⟨A,\varnothing ⟩”⟩\right]\underset{\dot{}}{\sim }\right)={\sum }_H\left(T\circ ⟨“⟨A,\varnothing ⟩”⟩\right)$$
34	1 2 3 4 5 6	frgpuptf	$$⊢\phi \to T:I\times 2_{𝑜}⟶B$$
35		s1co	$$⊢\left(⟨A,\varnothing ⟩\in \left(I\times 2_{𝑜}\right)\wedge T:I\times 2_{𝑜}⟶B\right)\to T\circ ⟨“⟨A,\varnothing ⟩”⟩=⟨“T\left(⟨A,\varnothing ⟩\right)”⟩$$
36	22 34 35	syl2anc	$$⊢\phi \to T\circ ⟨“⟨A,\varnothing ⟩”⟩=⟨“T\left(⟨A,\varnothing ⟩\right)”⟩$$
37		df-ov	$$⊢AT\varnothing =T\left(⟨A,\varnothing ⟩\right)$$
38		iftrue	$$⊢z=\varnothing \to if\left(z=\varnothing ,F\left(y\right),N\left(F\left(y\right)\right)\right)=F\left(y\right)$$
39		fveq2	$$⊢y=A\to F\left(y\right)=F\left(A\right)$$
40	38 39	sylan9eqr	$$⊢\left(y=A\wedge z=\varnothing \right)\to if\left(z=\varnothing ,F\left(y\right),N\left(F\left(y\right)\right)\right)=F\left(A\right)$$
41		fvex	$$⊢F\left(A\right)\in \mathrm{V}$$
42	40 3 41	ovmpoa	$$⊢\left(A\in I\wedge \varnothing \in 2_{𝑜}\right)\to AT\varnothing =F\left(A\right)$$
43	13 20 42	sylancl	$$⊢\phi \to AT\varnothing =F\left(A\right)$$
44	37 43	syl5eqr	$$⊢\phi \to T\left(⟨A,\varnothing ⟩\right)=F\left(A\right)$$
45	44	s1eqd	$$⊢\phi \to ⟨“T\left(⟨A,\varnothing ⟩\right)”⟩=⟨“F\left(A\right)”⟩$$
46	36 45	eqtrd	$$⊢\phi \to T\circ ⟨“⟨A,\varnothing ⟩”⟩=⟨“F\left(A\right)”⟩$$
47	46	oveq2d	$$⊢\phi \to {\sum }_H\left(T\circ ⟨“⟨A,\varnothing ⟩”⟩\right)={\sum }_H⟨“F\left(A\right)”⟩$$
48	6 13	ffvelrnd	$$⊢\phi \to F\left(A\right)\in B$$
49	1	gsumws1	$$⊢F\left(A\right)\in B\to {\sum }_H⟨“F\left(A\right)”⟩=F\left(A\right)$$
50	48 49	syl	$$⊢\phi \to {\sum }_H⟨“F\left(A\right)”⟩=F\left(A\right)$$
51	47 50	eqtrd	$$⊢\phi \to {\sum }_H\left(T\circ ⟨“⟨A,\varnothing ⟩”⟩\right)=F\left(A\right)$$
52	16 33 51	3eqtrd	$$⊢\phi \to E\left(U\left(A\right)\right)=F\left(A\right)$$