Step | Hyp | Ref
| Expression |
1 | | zringbas 21023 |
. . . . . . . . . 10
โข โค =
(Baseโโคring) |
2 | | eqid 2733 |
. . . . . . . . . 10
โข
(Baseโ๐
) =
(Baseโ๐
) |
3 | 1, 2 | rhmf 20263 |
. . . . . . . . 9
โข (๐ โ (โคring
RingHom ๐
) โ ๐:โคโถ(Baseโ๐
)) |
4 | 3 | adantl 483 |
. . . . . . . 8
โข ((๐
โ Ring โง ๐ โ (โคring
RingHom ๐
)) โ ๐:โคโถ(Baseโ๐
)) |
5 | 4 | feqmptd 6961 |
. . . . . . 7
โข ((๐
โ Ring โง ๐ โ (โคring
RingHom ๐
)) โ ๐ = (๐ โ โค โฆ (๐โ๐))) |
6 | | rhmghm 20262 |
. . . . . . . . . . 11
โข (๐ โ (โคring
RingHom ๐
) โ ๐ โ (โคring
GrpHom ๐
)) |
7 | 6 | ad2antlr 726 |
. . . . . . . . . 10
โข (((๐
โ Ring โง ๐ โ (โคring
RingHom ๐
)) โง ๐ โ โค) โ ๐ โ (โคring
GrpHom ๐
)) |
8 | | simpr 486 |
. . . . . . . . . 10
โข (((๐
โ Ring โง ๐ โ (โคring
RingHom ๐
)) โง ๐ โ โค) โ ๐ โ
โค) |
9 | | 1zzd 12593 |
. . . . . . . . . 10
โข (((๐
โ Ring โง ๐ โ (โคring
RingHom ๐
)) โง ๐ โ โค) โ 1 โ
โค) |
10 | | eqid 2733 |
. . . . . . . . . . 11
โข
(.gโโคring) =
(.gโโคring) |
11 | | mulgghm2.m |
. . . . . . . . . . 11
โข ยท =
(.gโ๐
) |
12 | 1, 10, 11 | ghmmulg 19104 |
. . . . . . . . . 10
โข ((๐ โ (โคring
GrpHom ๐
) โง ๐ โ โค โง 1 โ
โค) โ (๐โ(๐(.gโโคring)1))
= (๐ ยท (๐โ1))) |
13 | 7, 8, 9, 12 | syl3anc 1372 |
. . . . . . . . 9
โข (((๐
โ Ring โง ๐ โ (โคring
RingHom ๐
)) โง ๐ โ โค) โ (๐โ(๐(.gโโคring)1))
= (๐ ยท (๐โ1))) |
14 | | ax-1cn 11168 |
. . . . . . . . . . . . 13
โข 1 โ
โ |
15 | | cnfldmulg 20977 |
. . . . . . . . . . . . 13
โข ((๐ โ โค โง 1 โ
โ) โ (๐(.gโโfld)1)
= (๐ ยท
1)) |
16 | 14, 15 | mpan2 690 |
. . . . . . . . . . . 12
โข (๐ โ โค โ (๐(.gโโfld)1)
= (๐ ยท
1)) |
17 | | 1z 12592 |
. . . . . . . . . . . . 13
โข 1 โ
โค |
18 | 16 | adantr 482 |
. . . . . . . . . . . . . 14
โข ((๐ โ โค โง 1 โ
โค) โ (๐(.gโโfld)1)
= (๐ ยท
1)) |
19 | | zringmulg 21026 |
. . . . . . . . . . . . . 14
โข ((๐ โ โค โง 1 โ
โค) โ (๐(.gโโคring)1)
= (๐ ยท
1)) |
20 | 18, 19 | eqtr4d 2776 |
. . . . . . . . . . . . 13
โข ((๐ โ โค โง 1 โ
โค) โ (๐(.gโโfld)1)
= (๐(.gโโคring)1)) |
21 | 17, 20 | mpan2 690 |
. . . . . . . . . . . 12
โข (๐ โ โค โ (๐(.gโโfld)1)
= (๐(.gโโคring)1)) |
22 | | zcn 12563 |
. . . . . . . . . . . . 13
โข (๐ โ โค โ ๐ โ
โ) |
23 | 22 | mulridd 11231 |
. . . . . . . . . . . 12
โข (๐ โ โค โ (๐ ยท 1) = ๐) |
24 | 16, 21, 23 | 3eqtr3d 2781 |
. . . . . . . . . . 11
โข (๐ โ โค โ (๐(.gโโคring)1)
= ๐) |
25 | 24 | adantl 483 |
. . . . . . . . . 10
โข (((๐
โ Ring โง ๐ โ (โคring
RingHom ๐
)) โง ๐ โ โค) โ (๐(.gโโคring)1)
= ๐) |
26 | 25 | fveq2d 6896 |
. . . . . . . . 9
โข (((๐
โ Ring โง ๐ โ (โคring
RingHom ๐
)) โง ๐ โ โค) โ (๐โ(๐(.gโโคring)1))
= (๐โ๐)) |
27 | | zring1 21029 |
. . . . . . . . . . . 12
โข 1 =
(1rโโคring) |
28 | | mulgrhm.1 |
. . . . . . . . . . . 12
โข 1 =
(1rโ๐
) |
29 | 27, 28 | rhm1 20267 |
. . . . . . . . . . 11
โข (๐ โ (โคring
RingHom ๐
) โ (๐โ1) = 1 ) |
30 | 29 | ad2antlr 726 |
. . . . . . . . . 10
โข (((๐
โ Ring โง ๐ โ (โคring
RingHom ๐
)) โง ๐ โ โค) โ (๐โ1) = 1 ) |
31 | 30 | oveq2d 7425 |
. . . . . . . . 9
โข (((๐
โ Ring โง ๐ โ (โคring
RingHom ๐
)) โง ๐ โ โค) โ (๐ ยท (๐โ1)) = (๐ ยท 1 )) |
32 | 13, 26, 31 | 3eqtr3d 2781 |
. . . . . . . 8
โข (((๐
โ Ring โง ๐ โ (โคring
RingHom ๐
)) โง ๐ โ โค) โ (๐โ๐) = (๐ ยท 1 )) |
33 | 32 | mpteq2dva 5249 |
. . . . . . 7
โข ((๐
โ Ring โง ๐ โ (โคring
RingHom ๐
)) โ (๐ โ โค โฆ (๐โ๐)) = (๐ โ โค โฆ (๐ ยท 1 ))) |
34 | 5, 33 | eqtrd 2773 |
. . . . . 6
โข ((๐
โ Ring โง ๐ โ (โคring
RingHom ๐
)) โ ๐ = (๐ โ โค โฆ (๐ ยท 1 ))) |
35 | | mulgghm2.f |
. . . . . 6
โข ๐น = (๐ โ โค โฆ (๐ ยท 1 )) |
36 | 34, 35 | eqtr4di 2791 |
. . . . 5
โข ((๐
โ Ring โง ๐ โ (โคring
RingHom ๐
)) โ ๐ = ๐น) |
37 | | velsn 4645 |
. . . . 5
โข (๐ โ {๐น} โ ๐ = ๐น) |
38 | 36, 37 | sylibr 233 |
. . . 4
โข ((๐
โ Ring โง ๐ โ (โคring
RingHom ๐
)) โ ๐ โ {๐น}) |
39 | 38 | ex 414 |
. . 3
โข (๐
โ Ring โ (๐ โ (โคring
RingHom ๐
) โ ๐ โ {๐น})) |
40 | 39 | ssrdv 3989 |
. 2
โข (๐
โ Ring โ
(โคring RingHom ๐
) โ {๐น}) |
41 | 11, 35, 28 | mulgrhm 21047 |
. . 3
โข (๐
โ Ring โ ๐น โ (โคring
RingHom ๐
)) |
42 | 41 | snssd 4813 |
. 2
โข (๐
โ Ring โ {๐น} โ
(โคring RingHom ๐
)) |
43 | 40, 42 | eqssd 4000 |
1
โข (๐
โ Ring โ
(โคring RingHom ๐
) = {๐น}) |