This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 eqtrid ⊢ ( 𝜑 → 𝑊 = 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 ffvelcdmd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐴 ) ∈ 𝐵 )
49 1 gsumws1 ⊢ ( ( 𝐹 ‘ 𝐴 ) ∈ 𝐵 → ( 𝐻 Σg ⟨“ ( 𝐹 ‘ 𝐴 ) ”⟩ ) = ( 𝐹 ‘ 𝐴 ) )
50 48 49 syl ⊢ ( 𝜑 → ( 𝐻 Σg ⟨“ ( 𝐹 ‘ 𝐴 ) ”⟩ ) = ( 𝐹 ‘ 𝐴 ) )
51 47 50 eqtrd ⊢ ( 𝜑 → ( 𝐻 Σg ( 𝑇 ∘ ⟨“ ⟨ 𝐴 , ∅ ⟩ ”⟩ ) ) = ( 𝐹 ‘ 𝐴 ) )
52 16 33 51 3eqtrd ⊢ ( 𝜑 → ( 𝐸 ‘ ( 𝑈 ‘ 𝐴 ) ) = ( 𝐹 ‘ 𝐴 ) )