Step |
Hyp |
Ref |
Expression |
1 |
|
frgpmhm.m |
|- M = ( freeMnd ` ( I X. 2o ) ) |
2 |
|
frgpmhm.w |
|- W = ( Base ` M ) |
3 |
|
frgpmhm.g |
|- G = ( freeGrp ` I ) |
4 |
|
frgpmhm.r |
|- .~ = ( ~FG ` I ) |
5 |
|
frgpmhm.f |
|- F = ( x e. W |-> [ x ] .~ ) |
6 |
|
2on |
|- 2o e. On |
7 |
|
xpexg |
|- ( ( I e. V /\ 2o e. On ) -> ( I X. 2o ) e. _V ) |
8 |
6 7
|
mpan2 |
|- ( I e. V -> ( I X. 2o ) e. _V ) |
9 |
1
|
frmdmnd |
|- ( ( I X. 2o ) e. _V -> M e. Mnd ) |
10 |
8 9
|
syl |
|- ( I e. V -> M e. Mnd ) |
11 |
3
|
frgpgrp |
|- ( I e. V -> G e. Grp ) |
12 |
|
grpmnd |
|- ( G e. Grp -> G e. Mnd ) |
13 |
11 12
|
syl |
|- ( I e. V -> G e. Mnd ) |
14 |
1 2
|
frmdbas |
|- ( ( I X. 2o ) e. _V -> W = Word ( I X. 2o ) ) |
15 |
|
wrdexg |
|- ( ( I X. 2o ) e. _V -> Word ( I X. 2o ) e. _V ) |
16 |
|
fvi |
|- ( Word ( I X. 2o ) e. _V -> ( _I ` Word ( I X. 2o ) ) = Word ( I X. 2o ) ) |
17 |
15 16
|
syl |
|- ( ( I X. 2o ) e. _V -> ( _I ` Word ( I X. 2o ) ) = Word ( I X. 2o ) ) |
18 |
14 17
|
eqtr4d |
|- ( ( I X. 2o ) e. _V -> W = ( _I ` Word ( I X. 2o ) ) ) |
19 |
8 18
|
syl |
|- ( I e. V -> W = ( _I ` Word ( I X. 2o ) ) ) |
20 |
19
|
eleq2d |
|- ( I e. V -> ( x e. W <-> x e. ( _I ` Word ( I X. 2o ) ) ) ) |
21 |
20
|
biimpa |
|- ( ( I e. V /\ x e. W ) -> x e. ( _I ` Word ( I X. 2o ) ) ) |
22 |
|
eqid |
|- ( _I ` Word ( I X. 2o ) ) = ( _I ` Word ( I X. 2o ) ) |
23 |
|
eqid |
|- ( Base ` G ) = ( Base ` G ) |
24 |
3 4 22 23
|
frgpeccl |
|- ( x e. ( _I ` Word ( I X. 2o ) ) -> [ x ] .~ e. ( Base ` G ) ) |
25 |
21 24
|
syl |
|- ( ( I e. V /\ x e. W ) -> [ x ] .~ e. ( Base ` G ) ) |
26 |
25 5
|
fmptd |
|- ( I e. V -> F : W --> ( Base ` G ) ) |
27 |
22 4
|
efger |
|- .~ Er ( _I ` Word ( I X. 2o ) ) |
28 |
|
ereq2 |
|- ( W = ( _I ` Word ( I X. 2o ) ) -> ( .~ Er W <-> .~ Er ( _I ` Word ( I X. 2o ) ) ) ) |
29 |
19 28
|
syl |
|- ( I e. V -> ( .~ Er W <-> .~ Er ( _I ` Word ( I X. 2o ) ) ) ) |
30 |
27 29
|
mpbiri |
|- ( I e. V -> .~ Er W ) |
31 |
30
|
adantr |
|- ( ( I e. V /\ ( a e. W /\ b e. W ) ) -> .~ Er W ) |
32 |
2
|
fvexi |
|- W e. _V |
33 |
32
|
a1i |
|- ( ( I e. V /\ ( a e. W /\ b e. W ) ) -> W e. _V ) |
34 |
31 33 5
|
divsfval |
|- ( ( I e. V /\ ( a e. W /\ b e. W ) ) -> ( F ` ( a ++ b ) ) = [ ( a ++ b ) ] .~ ) |
35 |
|
eqid |
|- ( +g ` M ) = ( +g ` M ) |
36 |
1 2 35
|
frmdadd |
|- ( ( a e. W /\ b e. W ) -> ( a ( +g ` M ) b ) = ( a ++ b ) ) |
37 |
36
|
adantl |
|- ( ( I e. V /\ ( a e. W /\ b e. W ) ) -> ( a ( +g ` M ) b ) = ( a ++ b ) ) |
38 |
37
|
fveq2d |
|- ( ( I e. V /\ ( a e. W /\ b e. W ) ) -> ( F ` ( a ( +g ` M ) b ) ) = ( F ` ( a ++ b ) ) ) |
39 |
31 33 5
|
divsfval |
|- ( ( I e. V /\ ( a e. W /\ b e. W ) ) -> ( F ` a ) = [ a ] .~ ) |
40 |
31 33 5
|
divsfval |
|- ( ( I e. V /\ ( a e. W /\ b e. W ) ) -> ( F ` b ) = [ b ] .~ ) |
41 |
39 40
|
oveq12d |
|- ( ( I e. V /\ ( a e. W /\ b e. W ) ) -> ( ( F ` a ) ( +g ` G ) ( F ` b ) ) = ( [ a ] .~ ( +g ` G ) [ b ] .~ ) ) |
42 |
19
|
eleq2d |
|- ( I e. V -> ( a e. W <-> a e. ( _I ` Word ( I X. 2o ) ) ) ) |
43 |
19
|
eleq2d |
|- ( I e. V -> ( b e. W <-> b e. ( _I ` Word ( I X. 2o ) ) ) ) |
44 |
42 43
|
anbi12d |
|- ( I e. V -> ( ( a e. W /\ b e. W ) <-> ( a e. ( _I ` Word ( I X. 2o ) ) /\ b e. ( _I ` Word ( I X. 2o ) ) ) ) ) |
45 |
44
|
biimpa |
|- ( ( I e. V /\ ( a e. W /\ b e. W ) ) -> ( a e. ( _I ` Word ( I X. 2o ) ) /\ b e. ( _I ` Word ( I X. 2o ) ) ) ) |
46 |
|
eqid |
|- ( +g ` G ) = ( +g ` G ) |
47 |
22 3 4 46
|
frgpadd |
|- ( ( a e. ( _I ` Word ( I X. 2o ) ) /\ b e. ( _I ` Word ( I X. 2o ) ) ) -> ( [ a ] .~ ( +g ` G ) [ b ] .~ ) = [ ( a ++ b ) ] .~ ) |
48 |
45 47
|
syl |
|- ( ( I e. V /\ ( a e. W /\ b e. W ) ) -> ( [ a ] .~ ( +g ` G ) [ b ] .~ ) = [ ( a ++ b ) ] .~ ) |
49 |
41 48
|
eqtrd |
|- ( ( I e. V /\ ( a e. W /\ b e. W ) ) -> ( ( F ` a ) ( +g ` G ) ( F ` b ) ) = [ ( a ++ b ) ] .~ ) |
50 |
34 38 49
|
3eqtr4d |
|- ( ( I e. V /\ ( a e. W /\ b e. W ) ) -> ( F ` ( a ( +g ` M ) b ) ) = ( ( F ` a ) ( +g ` G ) ( F ` b ) ) ) |
51 |
50
|
ralrimivva |
|- ( I e. V -> A. a e. W A. b e. W ( F ` ( a ( +g ` M ) b ) ) = ( ( F ` a ) ( +g ` G ) ( F ` b ) ) ) |
52 |
32
|
a1i |
|- ( I e. V -> W e. _V ) |
53 |
30 52 5
|
divsfval |
|- ( I e. V -> ( F ` (/) ) = [ (/) ] .~ ) |
54 |
3 4
|
frgp0 |
|- ( I e. V -> ( G e. Grp /\ [ (/) ] .~ = ( 0g ` G ) ) ) |
55 |
54
|
simprd |
|- ( I e. V -> [ (/) ] .~ = ( 0g ` G ) ) |
56 |
53 55
|
eqtrd |
|- ( I e. V -> ( F ` (/) ) = ( 0g ` G ) ) |
57 |
26 51 56
|
3jca |
|- ( I e. V -> ( F : W --> ( Base ` G ) /\ A. a e. W A. b e. W ( F ` ( a ( +g ` M ) b ) ) = ( ( F ` a ) ( +g ` G ) ( F ` b ) ) /\ ( F ` (/) ) = ( 0g ` G ) ) ) |
58 |
1
|
frmd0 |
|- (/) = ( 0g ` M ) |
59 |
|
eqid |
|- ( 0g ` G ) = ( 0g ` G ) |
60 |
2 23 35 46 58 59
|
ismhm |
|- ( F e. ( M MndHom G ) <-> ( ( M e. Mnd /\ G e. Mnd ) /\ ( F : W --> ( Base ` G ) /\ A. a e. W A. b e. W ( F ` ( a ( +g ` M ) b ) ) = ( ( F ` a ) ( +g ` G ) ( F ` b ) ) /\ ( F ` (/) ) = ( 0g ` G ) ) ) ) |
61 |
10 13 57 60
|
syl21anbrc |
|- ( I e. V -> F e. ( M MndHom G ) ) |