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	⊢ 𝐵 = ( Base ‘ 𝐻 )
	frgpup.n	⊢ 𝑁 = ( invg ‘ 𝐻 )
	frgpup.t	⊢ 𝑇 = ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2o ↦ if ( 𝑧 = ∅ , ( 𝐹 ‘ 𝑦 ) , ( 𝑁 ‘ ( 𝐹 ‘ 𝑦 ) ) ) )
	frgpup.h	⊢ ( 𝜑 → 𝐻 ∈ Grp )
	frgpup.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
	frgpup.a	⊢ ( 𝜑 → 𝐹 : 𝐼 ⟶ 𝐵 )
	frgpup.w	⊢ 𝑊 = ( I ‘ Word ( 𝐼 × 2o ) )
	frgpup.r	⊢ ∼ = ( ~FG ‘ 𝐼 )
	frgpup.g	⊢ 𝐺 = ( freeGrp ‘ 𝐼 )
	frgpup.x	⊢ 𝑋 = ( Base ‘ 𝐺 )
	frgpup.e	⊢ 𝐸 = ran ( 𝑔 ∈ 𝑊 ↦ ⟨ [ 𝑔 ] ∼ , ( 𝐻 Σg ( 𝑇 ∘ 𝑔 ) ) ⟩ )
	frgpup.u	⊢ 𝑈 = ( varFGrp ‘ 𝐼 )
	frgpup.y	⊢ ( 𝜑 → 𝐴 ∈ 𝐼 )
Assertion	frgpup2	⊢ ( 𝜑 → ( 𝐸 ‘ ( 𝑈 ‘ 𝐴 ) ) = ( 𝐹 ‘ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		frgpup.b	⊢ 𝐵 = ( Base ‘ 𝐻 )
2		frgpup.n	⊢ 𝑁 = ( invg ‘ 𝐻 )
3		frgpup.t	⊢ 𝑇 = ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2o ↦ if ( 𝑧 = ∅ , ( 𝐹 ‘ 𝑦 ) , ( 𝑁 ‘ ( 𝐹 ‘ 𝑦 ) ) ) )
4		frgpup.h	⊢ ( 𝜑 → 𝐻 ∈ Grp )
5		frgpup.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
6		frgpup.a	⊢ ( 𝜑 → 𝐹 : 𝐼 ⟶ 𝐵 )
7		frgpup.w	⊢ 𝑊 = ( I ‘ Word ( 𝐼 × 2o ) )
8		frgpup.r	⊢ ∼ = ( ~FG ‘ 𝐼 )
9		frgpup.g	⊢ 𝐺 = ( freeGrp ‘ 𝐼 )
10		frgpup.x	⊢ 𝑋 = ( Base ‘ 𝐺 )
11		frgpup.e	⊢ 𝐸 = ran ( 𝑔 ∈ 𝑊 ↦ ⟨ [ 𝑔 ] ∼ , ( 𝐻 Σg ( 𝑇 ∘ 𝑔 ) ) ⟩ )
12		frgpup.u	⊢ 𝑈 = ( varFGrp ‘ 𝐼 )
13		frgpup.y	⊢ ( 𝜑 → 𝐴 ∈ 𝐼 )
14	8 12	vrgpval	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐴 ∈ 𝐼 ) → ( 𝑈 ‘ 𝐴 ) = [ ⟨“ ⟨ 𝐴 , ∅ ⟩ ”⟩ ] ∼ )
15	5 13 14	syl2anc	⊢ ( 𝜑 → ( 𝑈 ‘ 𝐴 ) = [ ⟨“ ⟨ 𝐴 , ∅ ⟩ ”⟩ ] ∼ )
16	15	fveq2d	⊢ ( 𝜑 → ( 𝐸 ‘ ( 𝑈 ‘ 𝐴 ) ) = ( 𝐸 ‘ [ ⟨“ ⟨ 𝐴 , ∅ ⟩ ”⟩ ] ∼ ) )
17		0ex	⊢ ∅ ∈ V
18	17	prid1	⊢ ∅ ∈ { ∅ , 1o }
19		df2o3	⊢ 2o = { ∅ , 1o }
20	18 19	eleqtrri	⊢ ∅ ∈ 2o
21		opelxpi	⊢ ( ( 𝐴 ∈ 𝐼 ∧ ∅ ∈ 2o ) → ⟨ 𝐴 , ∅ ⟩ ∈ ( 𝐼 × 2o ) )
22	13 20 21	sylancl	⊢ ( 𝜑 → ⟨ 𝐴 , ∅ ⟩ ∈ ( 𝐼 × 2o ) )
23	22	s1cld	⊢ ( 𝜑 → ⟨“ ⟨ 𝐴 , ∅ ⟩ ”⟩ ∈ Word ( 𝐼 × 2o ) )
24		2on	⊢ 2o ∈ On
25		xpexg	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 2o ∈ On ) → ( 𝐼 × 2o ) ∈ V )
26	5 24 25	sylancl	⊢ ( 𝜑 → ( 𝐼 × 2o ) ∈ V )
27		wrdexg	⊢ ( ( 𝐼 × 2o ) ∈ V → Word ( 𝐼 × 2o ) ∈ V )
28		fvi	⊢ ( Word ( 𝐼 × 2o ) ∈ V → ( I ‘ Word ( 𝐼 × 2o ) ) = Word ( 𝐼 × 2o ) )
29	26 27 28	3syl	⊢ ( 𝜑 → ( I ‘ Word ( 𝐼 × 2o ) ) = Word ( 𝐼 × 2o ) )
30	7 29	syl5eq	⊢ ( 𝜑 → 𝑊 = Word ( 𝐼 × 2o ) )
31	23 30	eleqtrrd	⊢ ( 𝜑 → ⟨“ ⟨ 𝐴 , ∅ ⟩ ”⟩ ∈ 𝑊 )
32	1 2 3 4 5 6 7 8 9 10 11	frgpupval	⊢ ( ( 𝜑 ∧ ⟨“ ⟨ 𝐴 , ∅ ⟩ ”⟩ ∈ 𝑊 ) → ( 𝐸 ‘ [ ⟨“ ⟨ 𝐴 , ∅ ⟩ ”⟩ ] ∼ ) = ( 𝐻 Σg ( 𝑇 ∘ ⟨“ ⟨ 𝐴 , ∅ ⟩ ”⟩ ) ) )
33	31 32	mpdan	⊢ ( 𝜑 → ( 𝐸 ‘ [ ⟨“ ⟨ 𝐴 , ∅ ⟩ ”⟩ ] ∼ ) = ( 𝐻 Σg ( 𝑇 ∘ ⟨“ ⟨ 𝐴 , ∅ ⟩ ”⟩ ) ) )
34	1 2 3 4 5 6	frgpuptf	⊢ ( 𝜑 → 𝑇 : ( 𝐼 × 2o ) ⟶ 𝐵 )
35		s1co	⊢ ( ( ⟨ 𝐴 , ∅ ⟩ ∈ ( 𝐼 × 2o ) ∧ 𝑇 : ( 𝐼 × 2o ) ⟶ 𝐵 ) → ( 𝑇 ∘ ⟨“ ⟨ 𝐴 , ∅ ⟩ ”⟩ ) = ⟨“ ( 𝑇 ‘ ⟨ 𝐴 , ∅ ⟩ ) ”⟩ )
36	22 34 35	syl2anc	⊢ ( 𝜑 → ( 𝑇 ∘ ⟨“ ⟨ 𝐴 , ∅ ⟩ ”⟩ ) = ⟨“ ( 𝑇 ‘ ⟨ 𝐴 , ∅ ⟩ ) ”⟩ )
37		df-ov	⊢ ( 𝐴 𝑇 ∅ ) = ( 𝑇 ‘ ⟨ 𝐴 , ∅ ⟩ )
38		iftrue	⊢ ( 𝑧 = ∅ → if ( 𝑧 = ∅ , ( 𝐹 ‘ 𝑦 ) , ( 𝑁 ‘ ( 𝐹 ‘ 𝑦 ) ) ) = ( 𝐹 ‘ 𝑦 ) )
39		fveq2	⊢ ( 𝑦 = 𝐴 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝐴 ) )
40	38 39	sylan9eqr	⊢ ( ( 𝑦 = 𝐴 ∧ 𝑧 = ∅ ) → if ( 𝑧 = ∅ , ( 𝐹 ‘ 𝑦 ) , ( 𝑁 ‘ ( 𝐹 ‘ 𝑦 ) ) ) = ( 𝐹 ‘ 𝐴 ) )
41		fvex	⊢ ( 𝐹 ‘ 𝐴 ) ∈ V
42	40 3 41	ovmpoa	⊢ ( ( 𝐴 ∈ 𝐼 ∧ ∅ ∈ 2o ) → ( 𝐴 𝑇 ∅ ) = ( 𝐹 ‘ 𝐴 ) )
43	13 20 42	sylancl	⊢ ( 𝜑 → ( 𝐴 𝑇 ∅ ) = ( 𝐹 ‘ 𝐴 ) )
44	37 43	eqtr3id	⊢ ( 𝜑 → ( 𝑇 ‘ ⟨ 𝐴 , ∅ ⟩ ) = ( 𝐹 ‘ 𝐴 ) )
45	44	s1eqd	⊢ ( 𝜑 → ⟨“ ( 𝑇 ‘ ⟨ 𝐴 , ∅ ⟩ ) ”⟩ = ⟨“ ( 𝐹 ‘ 𝐴 ) ”⟩ )
46	36 45	eqtrd	⊢ ( 𝜑 → ( 𝑇 ∘ ⟨“ ⟨ 𝐴 , ∅ ⟩ ”⟩ ) = ⟨“ ( 𝐹 ‘ 𝐴 ) ”⟩ )
47	46	oveq2d	⊢ ( 𝜑 → ( 𝐻 Σg ( 𝑇 ∘ ⟨“ ⟨ 𝐴 , ∅ ⟩ ”⟩ ) ) = ( 𝐻 Σg ⟨“ ( 𝐹 ‘ 𝐴 ) ”⟩ ) )
48	6 13	ffvelrnd	⊢ ( 𝜑 → ( 𝐹 ‘ 𝐴 ) ∈ 𝐵 )
49	1	gsumws1	⊢ ( ( 𝐹 ‘ 𝐴 ) ∈ 𝐵 → ( 𝐻 Σg ⟨“ ( 𝐹 ‘ 𝐴 ) ”⟩ ) = ( 𝐹 ‘ 𝐴 ) )
50	48 49	syl	⊢ ( 𝜑 → ( 𝐻 Σg ⟨“ ( 𝐹 ‘ 𝐴 ) ”⟩ ) = ( 𝐹 ‘ 𝐴 ) )
51	47 50	eqtrd	⊢ ( 𝜑 → ( 𝐻 Σg ( 𝑇 ∘ ⟨“ ⟨ 𝐴 , ∅ ⟩ ”⟩ ) ) = ( 𝐹 ‘ 𝐴 ) )
52	16 33 51	3eqtrd	⊢ ( 𝜑 → ( 𝐸 ‘ ( 𝑈 ‘ 𝐴 ) ) = ( 𝐹 ‘ 𝐴 ) )