Step |
Hyp |
Ref |
Expression |
1 |
|
reefgim.1 |
โข ๐ = ( ( mulGrp โ โfld ) โพs โ+ ) |
2 |
|
rebase |
โข โ = ( Base โ โfld ) |
3 |
|
eqid |
โข ( ( mulGrp โ โfld ) โพs ( โ โ { 0 } ) ) = ( ( mulGrp โ โfld ) โพs ( โ โ { 0 } ) ) |
4 |
3
|
rpmsubg |
โข โ+ โ ( SubGrp โ ( ( mulGrp โ โfld ) โพs ( โ โ { 0 } ) ) ) |
5 |
|
cnex |
โข โ โ V |
6 |
5
|
difexi |
โข ( โ โ { 0 } ) โ V |
7 |
|
rpcndif0 |
โข ( ๐ฅ โ โ+ โ ๐ฅ โ ( โ โ { 0 } ) ) |
8 |
7
|
ssriv |
โข โ+ โ ( โ โ { 0 } ) |
9 |
|
ressabs |
โข ( ( ( โ โ { 0 } ) โ V โง โ+ โ ( โ โ { 0 } ) ) โ ( ( ( mulGrp โ โfld ) โพs ( โ โ { 0 } ) ) โพs โ+ ) = ( ( mulGrp โ โfld ) โพs โ+ ) ) |
10 |
6 8 9
|
mp2an |
โข ( ( ( mulGrp โ โfld ) โพs ( โ โ { 0 } ) ) โพs โ+ ) = ( ( mulGrp โ โfld ) โพs โ+ ) |
11 |
1 10
|
eqtr4i |
โข ๐ = ( ( ( mulGrp โ โfld ) โพs ( โ โ { 0 } ) ) โพs โ+ ) |
12 |
11
|
subgbas |
โข ( โ+ โ ( SubGrp โ ( ( mulGrp โ โfld ) โพs ( โ โ { 0 } ) ) ) โ โ+ = ( Base โ ๐ ) ) |
13 |
4 12
|
ax-mp |
โข โ+ = ( Base โ ๐ ) |
14 |
|
replusg |
โข + = ( +g โ โfld ) |
15 |
|
eqid |
โข ( mulGrp โ โfld ) = ( mulGrp โ โfld ) |
16 |
|
cnfldmul |
โข ยท = ( .r โ โfld ) |
17 |
15 16
|
mgpplusg |
โข ยท = ( +g โ ( mulGrp โ โfld ) ) |
18 |
1 17
|
ressplusg |
โข ( โ+ โ ( SubGrp โ ( ( mulGrp โ โfld ) โพs ( โ โ { 0 } ) ) ) โ ยท = ( +g โ ๐ ) ) |
19 |
4 18
|
ax-mp |
โข ยท = ( +g โ ๐ ) |
20 |
|
resubdrg |
โข ( โ โ ( SubRing โ โfld ) โง โfld โ DivRing ) |
21 |
20
|
simpli |
โข โ โ ( SubRing โ โfld ) |
22 |
|
df-refld |
โข โfld = ( โfld โพs โ ) |
23 |
22
|
subrgring |
โข ( โ โ ( SubRing โ โfld ) โ โfld โ Ring ) |
24 |
21 23
|
ax-mp |
โข โfld โ Ring |
25 |
|
ringgrp |
โข ( โfld โ Ring โ โfld โ Grp ) |
26 |
24 25
|
mp1i |
โข ( โค โ โfld โ Grp ) |
27 |
11
|
subggrp |
โข ( โ+ โ ( SubGrp โ ( ( mulGrp โ โfld ) โพs ( โ โ { 0 } ) ) ) โ ๐ โ Grp ) |
28 |
4 27
|
mp1i |
โข ( โค โ ๐ โ Grp ) |
29 |
|
reeff1o |
โข ( exp โพ โ ) : โ โ1-1-ontoโ โ+ |
30 |
|
f1of |
โข ( ( exp โพ โ ) : โ โ1-1-ontoโ โ+ โ ( exp โพ โ ) : โ โถ โ+ ) |
31 |
29 30
|
mp1i |
โข ( โค โ ( exp โพ โ ) : โ โถ โ+ ) |
32 |
|
recn |
โข ( ๐ฅ โ โ โ ๐ฅ โ โ ) |
33 |
|
recn |
โข ( ๐ฆ โ โ โ ๐ฆ โ โ ) |
34 |
|
efadd |
โข ( ( ๐ฅ โ โ โง ๐ฆ โ โ ) โ ( exp โ ( ๐ฅ + ๐ฆ ) ) = ( ( exp โ ๐ฅ ) ยท ( exp โ ๐ฆ ) ) ) |
35 |
32 33 34
|
syl2an |
โข ( ( ๐ฅ โ โ โง ๐ฆ โ โ ) โ ( exp โ ( ๐ฅ + ๐ฆ ) ) = ( ( exp โ ๐ฅ ) ยท ( exp โ ๐ฆ ) ) ) |
36 |
|
readdcl |
โข ( ( ๐ฅ โ โ โง ๐ฆ โ โ ) โ ( ๐ฅ + ๐ฆ ) โ โ ) |
37 |
36
|
fvresd |
โข ( ( ๐ฅ โ โ โง ๐ฆ โ โ ) โ ( ( exp โพ โ ) โ ( ๐ฅ + ๐ฆ ) ) = ( exp โ ( ๐ฅ + ๐ฆ ) ) ) |
38 |
|
fvres |
โข ( ๐ฅ โ โ โ ( ( exp โพ โ ) โ ๐ฅ ) = ( exp โ ๐ฅ ) ) |
39 |
|
fvres |
โข ( ๐ฆ โ โ โ ( ( exp โพ โ ) โ ๐ฆ ) = ( exp โ ๐ฆ ) ) |
40 |
38 39
|
oveqan12d |
โข ( ( ๐ฅ โ โ โง ๐ฆ โ โ ) โ ( ( ( exp โพ โ ) โ ๐ฅ ) ยท ( ( exp โพ โ ) โ ๐ฆ ) ) = ( ( exp โ ๐ฅ ) ยท ( exp โ ๐ฆ ) ) ) |
41 |
35 37 40
|
3eqtr4d |
โข ( ( ๐ฅ โ โ โง ๐ฆ โ โ ) โ ( ( exp โพ โ ) โ ( ๐ฅ + ๐ฆ ) ) = ( ( ( exp โพ โ ) โ ๐ฅ ) ยท ( ( exp โพ โ ) โ ๐ฆ ) ) ) |
42 |
41
|
adantl |
โข ( ( โค โง ( ๐ฅ โ โ โง ๐ฆ โ โ ) ) โ ( ( exp โพ โ ) โ ( ๐ฅ + ๐ฆ ) ) = ( ( ( exp โพ โ ) โ ๐ฅ ) ยท ( ( exp โพ โ ) โ ๐ฆ ) ) ) |
43 |
2 13 14 19 26 28 31 42
|
isghmd |
โข ( โค โ ( exp โพ โ ) โ ( โfld GrpHom ๐ ) ) |
44 |
43
|
mptru |
โข ( exp โพ โ ) โ ( โfld GrpHom ๐ ) |
45 |
2 13
|
isgim |
โข ( ( exp โพ โ ) โ ( โfld GrpIso ๐ ) โ ( ( exp โพ โ ) โ ( โfld GrpHom ๐ ) โง ( exp โพ โ ) : โ โ1-1-ontoโ โ+ ) ) |
46 |
44 29 45
|
mpbir2an |
โข ( exp โพ โ ) โ ( โfld GrpIso ๐ ) |