Step | Hyp | Ref
| Expression |
1 | | zringbas 20898 |
. 2
โข โค =
(Baseโโคring) |
2 | | zring1 20903 |
. 2
โข 1 =
(1rโโคring) |
3 | | mulgrhm.1 |
. 2
โข 1 =
(1rโ๐
) |
4 | | zringmulr 20901 |
. 2
โข ยท
= (.rโโคring) |
5 | | eqid 2733 |
. 2
โข
(.rโ๐
) = (.rโ๐
) |
6 | | zringring 20895 |
. . 3
โข
โคring โ Ring |
7 | 6 | a1i 11 |
. 2
โข (๐
โ Ring โ
โคring โ Ring) |
8 | | id 22 |
. 2
โข (๐
โ Ring โ ๐
โ Ring) |
9 | | 1z 12541 |
. . . 4
โข 1 โ
โค |
10 | | oveq1 7368 |
. . . . 5
โข (๐ = 1 โ (๐ ยท 1 ) = (1 ยท 1 )) |
11 | | mulgghm2.f |
. . . . 5
โข ๐น = (๐ โ โค โฆ (๐ ยท 1 )) |
12 | | ovex 7394 |
. . . . 5
โข (1 ยท 1 ) โ
V |
13 | 10, 11, 12 | fvmpt 6952 |
. . . 4
โข (1 โ
โค โ (๐นโ1)
= (1 ยท 1 )) |
14 | 9, 13 | ax-mp 5 |
. . 3
โข (๐นโ1) = (1 ยท 1
) |
15 | | eqid 2733 |
. . . . 5
โข
(Baseโ๐
) =
(Baseโ๐
) |
16 | 15, 3 | ringidcl 19997 |
. . . 4
โข (๐
โ Ring โ 1 โ
(Baseโ๐
)) |
17 | | mulgghm2.m |
. . . . 5
โข ยท =
(.gโ๐
) |
18 | 15, 17 | mulg1 18891 |
. . . 4
โข ( 1 โ
(Baseโ๐
) โ (1
ยท
1 ) =
1
) |
19 | 16, 18 | syl 17 |
. . 3
โข (๐
โ Ring โ (1 ยท 1 ) = 1
) |
20 | 14, 19 | eqtrid 2785 |
. 2
โข (๐
โ Ring โ (๐นโ1) = 1 ) |
21 | | ringgrp 19977 |
. . . . . . . 8
โข (๐
โ Ring โ ๐
โ Grp) |
22 | 21 | adantr 482 |
. . . . . . 7
โข ((๐
โ Ring โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ ๐
โ Grp) |
23 | | simprr 772 |
. . . . . . 7
โข ((๐
โ Ring โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ ๐ฆ โ
โค) |
24 | 16 | adantr 482 |
. . . . . . 7
โข ((๐
โ Ring โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ 1 โ
(Baseโ๐
)) |
25 | 15, 17 | mulgcl 18901 |
. . . . . . 7
โข ((๐
โ Grp โง ๐ฆ โ โค โง 1 โ
(Baseโ๐
)) โ
(๐ฆ ยท 1 ) โ (Baseโ๐
)) |
26 | 22, 23, 24, 25 | syl3anc 1372 |
. . . . . 6
โข ((๐
โ Ring โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ (๐ฆ ยท 1 ) โ (Baseโ๐
)) |
27 | 15, 5, 3 | ringlidm 20000 |
. . . . . 6
โข ((๐
โ Ring โง (๐ฆ ยท 1 ) โ (Baseโ๐
)) โ ( 1 (.rโ๐
)(๐ฆ ยท 1 )) = (๐ฆ ยท 1 )) |
28 | 26, 27 | syldan 592 |
. . . . 5
โข ((๐
โ Ring โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ ( 1
(.rโ๐
)(๐ฆ ยท 1 )) = (๐ฆ ยท 1 )) |
29 | 28 | oveq2d 7377 |
. . . 4
โข ((๐
โ Ring โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ (๐ฅ ยท ( 1
(.rโ๐
)(๐ฆ ยท 1 ))) = (๐ฅ ยท (๐ฆ ยท 1 ))) |
30 | | simpl 484 |
. . . . 5
โข ((๐
โ Ring โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ ๐
โ Ring) |
31 | | simprl 770 |
. . . . 5
โข ((๐
โ Ring โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ ๐ฅ โ
โค) |
32 | 15, 17, 5 | mulgass2 20033 |
. . . . 5
โข ((๐
โ Ring โง (๐ฅ โ โค โง 1 โ
(Baseโ๐
) โง (๐ฆ ยท 1 ) โ (Baseโ๐
))) โ ((๐ฅ ยท 1
)(.rโ๐
)(๐ฆ ยท 1 )) = (๐ฅ ยท ( 1
(.rโ๐
)(๐ฆ ยท 1 )))) |
33 | 30, 31, 24, 26, 32 | syl13anc 1373 |
. . . 4
โข ((๐
โ Ring โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ ((๐ฅ ยท 1
)(.rโ๐
)(๐ฆ ยท 1 )) = (๐ฅ ยท ( 1
(.rโ๐
)(๐ฆ ยท 1 )))) |
34 | 15, 17 | mulgass 18921 |
. . . . 5
โข ((๐
โ Grp โง (๐ฅ โ โค โง ๐ฆ โ โค โง 1 โ
(Baseโ๐
))) โ
((๐ฅ ยท ๐ฆ) ยท 1 ) = (๐ฅ ยท (๐ฆ ยท 1 ))) |
35 | 22, 31, 23, 24, 34 | syl13anc 1373 |
. . . 4
โข ((๐
โ Ring โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ ((๐ฅ ยท ๐ฆ) ยท 1 ) = (๐ฅ ยท (๐ฆ ยท 1 ))) |
36 | 29, 33, 35 | 3eqtr4rd 2784 |
. . 3
โข ((๐
โ Ring โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ ((๐ฅ ยท ๐ฆ) ยท 1 ) = ((๐ฅ ยท 1
)(.rโ๐
)(๐ฆ ยท 1 ))) |
37 | | zmulcl 12560 |
. . . . 5
โข ((๐ฅ โ โค โง ๐ฆ โ โค) โ (๐ฅ ยท ๐ฆ) โ โค) |
38 | 37 | adantl 483 |
. . . 4
โข ((๐
โ Ring โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ (๐ฅ ยท ๐ฆ) โ โค) |
39 | | oveq1 7368 |
. . . . 5
โข (๐ = (๐ฅ ยท ๐ฆ) โ (๐ ยท 1 ) = ((๐ฅ ยท ๐ฆ) ยท 1 )) |
40 | | ovex 7394 |
. . . . 5
โข ((๐ฅ ยท ๐ฆ) ยท 1 ) โ
V |
41 | 39, 11, 40 | fvmpt 6952 |
. . . 4
โข ((๐ฅ ยท ๐ฆ) โ โค โ (๐นโ(๐ฅ ยท ๐ฆ)) = ((๐ฅ ยท ๐ฆ) ยท 1 )) |
42 | 38, 41 | syl 17 |
. . 3
โข ((๐
โ Ring โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ (๐นโ(๐ฅ ยท ๐ฆ)) = ((๐ฅ ยท ๐ฆ) ยท 1 )) |
43 | | oveq1 7368 |
. . . . . 6
โข (๐ = ๐ฅ โ (๐ ยท 1 ) = (๐ฅ ยท 1 )) |
44 | | ovex 7394 |
. . . . . 6
โข (๐ฅ ยท 1 ) โ
V |
45 | 43, 11, 44 | fvmpt 6952 |
. . . . 5
โข (๐ฅ โ โค โ (๐นโ๐ฅ) = (๐ฅ ยท 1 )) |
46 | | oveq1 7368 |
. . . . . 6
โข (๐ = ๐ฆ โ (๐ ยท 1 ) = (๐ฆ ยท 1 )) |
47 | | ovex 7394 |
. . . . . 6
โข (๐ฆ ยท 1 ) โ
V |
48 | 46, 11, 47 | fvmpt 6952 |
. . . . 5
โข (๐ฆ โ โค โ (๐นโ๐ฆ) = (๐ฆ ยท 1 )) |
49 | 45, 48 | oveqan12d 7380 |
. . . 4
โข ((๐ฅ โ โค โง ๐ฆ โ โค) โ ((๐นโ๐ฅ)(.rโ๐
)(๐นโ๐ฆ)) = ((๐ฅ ยท 1
)(.rโ๐
)(๐ฆ ยท 1 ))) |
50 | 49 | adantl 483 |
. . 3
โข ((๐
โ Ring โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ ((๐นโ๐ฅ)(.rโ๐
)(๐นโ๐ฆ)) = ((๐ฅ ยท 1
)(.rโ๐
)(๐ฆ ยท 1 ))) |
51 | 36, 42, 50 | 3eqtr4d 2783 |
. 2
โข ((๐
โ Ring โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ (๐นโ(๐ฅ ยท ๐ฆ)) = ((๐นโ๐ฅ)(.rโ๐
)(๐นโ๐ฆ))) |
52 | 17, 11, 15 | mulgghm2 20920 |
. . 3
โข ((๐
โ Grp โง 1 โ
(Baseโ๐
)) โ
๐น โ
(โคring GrpHom ๐
)) |
53 | 21, 16, 52 | syl2anc 585 |
. 2
โข (๐
โ Ring โ ๐น โ (โคring
GrpHom ๐
)) |
54 | 1, 2, 3, 4, 5, 7, 8, 20, 51, 53 | isrhm2d 20170 |
1
โข (๐
โ Ring โ ๐น โ (โคring
RingHom ๐
)) |