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 |
⊢ ( 𝜑 → ( 𝐸 ‘ ( 𝑈 ‘ 𝐴 ) ) = ( 𝐹 ‘ 𝐴 ) ) |