Step | Hyp | Ref
| Expression |
1 | | zringbas 21022 |
. . . . . . . . . 10
โข โค =
(Baseโโคring) |
2 | | eqid 2732 |
. . . . . . . . . 10
โข
(Baseโ๐
) =
(Baseโ๐
) |
3 | 1, 2 | rhmf 20262 |
. . . . . . . . 9
โข (๐ โ (โคring
RingHom ๐
) โ ๐:โคโถ(Baseโ๐
)) |
4 | 3 | adantl 482 |
. . . . . . . 8
โข ((๐
โ Ring โง ๐ โ (โคring
RingHom ๐
)) โ ๐:โคโถ(Baseโ๐
)) |
5 | 4 | feqmptd 6960 |
. . . . . . 7
โข ((๐
โ Ring โง ๐ โ (โคring
RingHom ๐
)) โ ๐ = (๐ โ โค โฆ (๐โ๐))) |
6 | | rhmghm 20261 |
. . . . . . . . . . 11
โข (๐ โ (โคring
RingHom ๐
) โ ๐ โ (โคring
GrpHom ๐
)) |
7 | 6 | ad2antlr 725 |
. . . . . . . . . 10
โข (((๐
โ Ring โง ๐ โ (โคring
RingHom ๐
)) โง ๐ โ โค) โ ๐ โ (โคring
GrpHom ๐
)) |
8 | | simpr 485 |
. . . . . . . . . 10
โข (((๐
โ Ring โง ๐ โ (โคring
RingHom ๐
)) โง ๐ โ โค) โ ๐ โ
โค) |
9 | | 1zzd 12592 |
. . . . . . . . . 10
โข (((๐
โ Ring โง ๐ โ (โคring
RingHom ๐
)) โง ๐ โ โค) โ 1 โ
โค) |
10 | | eqid 2732 |
. . . . . . . . . . 11
โข
(.gโโคring) =
(.gโโคring) |
11 | | mulgghm2.m |
. . . . . . . . . . 11
โข ยท =
(.gโ๐
) |
12 | 1, 10, 11 | ghmmulg 19103 |
. . . . . . . . . 10
โข ((๐ โ (โคring
GrpHom ๐
) โง ๐ โ โค โง 1 โ
โค) โ (๐โ(๐(.gโโคring)1))
= (๐ ยท (๐โ1))) |
13 | 7, 8, 9, 12 | syl3anc 1371 |
. . . . . . . . 9
โข (((๐
โ Ring โง ๐ โ (โคring
RingHom ๐
)) โง ๐ โ โค) โ (๐โ(๐(.gโโคring)1))
= (๐ ยท (๐โ1))) |
14 | | ax-1cn 11167 |
. . . . . . . . . . . . 13
โข 1 โ
โ |
15 | | cnfldmulg 20976 |
. . . . . . . . . . . . 13
โข ((๐ โ โค โง 1 โ
โ) โ (๐(.gโโfld)1)
= (๐ ยท
1)) |
16 | 14, 15 | mpan2 689 |
. . . . . . . . . . . 12
โข (๐ โ โค โ (๐(.gโโfld)1)
= (๐ ยท
1)) |
17 | | 1z 12591 |
. . . . . . . . . . . . 13
โข 1 โ
โค |
18 | 16 | adantr 481 |
. . . . . . . . . . . . . 14
โข ((๐ โ โค โง 1 โ
โค) โ (๐(.gโโfld)1)
= (๐ ยท
1)) |
19 | | zringmulg 21025 |
. . . . . . . . . . . . . 14
โข ((๐ โ โค โง 1 โ
โค) โ (๐(.gโโคring)1)
= (๐ ยท
1)) |
20 | 18, 19 | eqtr4d 2775 |
. . . . . . . . . . . . 13
โข ((๐ โ โค โง 1 โ
โค) โ (๐(.gโโfld)1)
= (๐(.gโโคring)1)) |
21 | 17, 20 | mpan2 689 |
. . . . . . . . . . . 12
โข (๐ โ โค โ (๐(.gโโfld)1)
= (๐(.gโโคring)1)) |
22 | | zcn 12562 |
. . . . . . . . . . . . 13
โข (๐ โ โค โ ๐ โ
โ) |
23 | 22 | mulridd 11230 |
. . . . . . . . . . . 12
โข (๐ โ โค โ (๐ ยท 1) = ๐) |
24 | 16, 21, 23 | 3eqtr3d 2780 |
. . . . . . . . . . 11
โข (๐ โ โค โ (๐(.gโโคring)1)
= ๐) |
25 | 24 | adantl 482 |
. . . . . . . . . 10
โข (((๐
โ Ring โง ๐ โ (โคring
RingHom ๐
)) โง ๐ โ โค) โ (๐(.gโโคring)1)
= ๐) |
26 | 25 | fveq2d 6895 |
. . . . . . . . 9
โข (((๐
โ Ring โง ๐ โ (โคring
RingHom ๐
)) โง ๐ โ โค) โ (๐โ(๐(.gโโคring)1))
= (๐โ๐)) |
27 | | zring1 21028 |
. . . . . . . . . . . 12
โข 1 =
(1rโโคring) |
28 | | mulgrhm.1 |
. . . . . . . . . . . 12
โข 1 =
(1rโ๐
) |
29 | 27, 28 | rhm1 20266 |
. . . . . . . . . . 11
โข (๐ โ (โคring
RingHom ๐
) โ (๐โ1) = 1 ) |
30 | 29 | ad2antlr 725 |
. . . . . . . . . 10
โข (((๐
โ Ring โง ๐ โ (โคring
RingHom ๐
)) โง ๐ โ โค) โ (๐โ1) = 1 ) |
31 | 30 | oveq2d 7424 |
. . . . . . . . 9
โข (((๐
โ Ring โง ๐ โ (โคring
RingHom ๐
)) โง ๐ โ โค) โ (๐ ยท (๐โ1)) = (๐ ยท 1 )) |
32 | 13, 26, 31 | 3eqtr3d 2780 |
. . . . . . . 8
โข (((๐
โ Ring โง ๐ โ (โคring
RingHom ๐
)) โง ๐ โ โค) โ (๐โ๐) = (๐ ยท 1 )) |
33 | 32 | mpteq2dva 5248 |
. . . . . . 7
โข ((๐
โ Ring โง ๐ โ (โคring
RingHom ๐
)) โ (๐ โ โค โฆ (๐โ๐)) = (๐ โ โค โฆ (๐ ยท 1 ))) |
34 | 5, 33 | eqtrd 2772 |
. . . . . 6
โข ((๐
โ Ring โง ๐ โ (โคring
RingHom ๐
)) โ ๐ = (๐ โ โค โฆ (๐ ยท 1 ))) |
35 | | mulgghm2.f |
. . . . . 6
โข ๐น = (๐ โ โค โฆ (๐ ยท 1 )) |
36 | 34, 35 | eqtr4di 2790 |
. . . . 5
โข ((๐
โ Ring โง ๐ โ (โคring
RingHom ๐
)) โ ๐ = ๐น) |
37 | | velsn 4644 |
. . . . 5
โข (๐ โ {๐น} โ ๐ = ๐น) |
38 | 36, 37 | sylibr 233 |
. . . 4
โข ((๐
โ Ring โง ๐ โ (โคring
RingHom ๐
)) โ ๐ โ {๐น}) |
39 | 38 | ex 413 |
. . 3
โข (๐
โ Ring โ (๐ โ (โคring
RingHom ๐
) โ ๐ โ {๐น})) |
40 | 39 | ssrdv 3988 |
. 2
โข (๐
โ Ring โ
(โคring RingHom ๐
) โ {๐น}) |
41 | 11, 35, 28 | mulgrhm 21046 |
. . 3
โข (๐
โ Ring โ ๐น โ (โคring
RingHom ๐
)) |
42 | 41 | snssd 4812 |
. 2
โข (๐
โ Ring โ {๐น} โ
(โคring RingHom ๐
)) |
43 | 40, 42 | eqssd 3999 |
1
โข (๐
โ Ring โ
(โคring RingHom ๐
) = {๐น}) |