Step | Hyp | Ref
| Expression |
1 | | rnghmrcl 46261 |
. 2
โข (๐น โ (๐
RngHomo ๐) โ (๐
โ Rng โง ๐ โ Rng)) |
2 | | isrnghm.b |
. . . . 5
โข ๐ต = (Baseโ๐
) |
3 | | isrnghm.t |
. . . . 5
โข ยท =
(.rโ๐
) |
4 | | isrnghm.m |
. . . . 5
โข โ =
(.rโ๐) |
5 | | eqid 2737 |
. . . . 5
โข
(Baseโ๐) =
(Baseโ๐) |
6 | | eqid 2737 |
. . . . 5
โข
(+gโ๐
) = (+gโ๐
) |
7 | | eqid 2737 |
. . . . 5
โข
(+gโ๐) = (+gโ๐) |
8 | 2, 3, 4, 5, 6, 7 | rnghmval 46263 |
. . . 4
โข ((๐
โ Rng โง ๐ โ Rng) โ (๐
RngHomo ๐) = {๐ โ ((Baseโ๐) โm ๐ต) โฃ โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต ((๐โ(๐ฅ(+gโ๐
)๐ฆ)) = ((๐โ๐ฅ)(+gโ๐)(๐โ๐ฆ)) โง (๐โ(๐ฅ ยท ๐ฆ)) = ((๐โ๐ฅ) โ (๐โ๐ฆ)))}) |
9 | 8 | eleq2d 2824 |
. . 3
โข ((๐
โ Rng โง ๐ โ Rng) โ (๐น โ (๐
RngHomo ๐) โ ๐น โ {๐ โ ((Baseโ๐) โm ๐ต) โฃ โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต ((๐โ(๐ฅ(+gโ๐
)๐ฆ)) = ((๐โ๐ฅ)(+gโ๐)(๐โ๐ฆ)) โง (๐โ(๐ฅ ยท ๐ฆ)) = ((๐โ๐ฅ) โ (๐โ๐ฆ)))})) |
10 | | fveq1 6846 |
. . . . . . . 8
โข (๐ = ๐น โ (๐โ(๐ฅ(+gโ๐
)๐ฆ)) = (๐นโ(๐ฅ(+gโ๐
)๐ฆ))) |
11 | | fveq1 6846 |
. . . . . . . . 9
โข (๐ = ๐น โ (๐โ๐ฅ) = (๐นโ๐ฅ)) |
12 | | fveq1 6846 |
. . . . . . . . 9
โข (๐ = ๐น โ (๐โ๐ฆ) = (๐นโ๐ฆ)) |
13 | 11, 12 | oveq12d 7380 |
. . . . . . . 8
โข (๐ = ๐น โ ((๐โ๐ฅ)(+gโ๐)(๐โ๐ฆ)) = ((๐นโ๐ฅ)(+gโ๐)(๐นโ๐ฆ))) |
14 | 10, 13 | eqeq12d 2753 |
. . . . . . 7
โข (๐ = ๐น โ ((๐โ(๐ฅ(+gโ๐
)๐ฆ)) = ((๐โ๐ฅ)(+gโ๐)(๐โ๐ฆ)) โ (๐นโ(๐ฅ(+gโ๐
)๐ฆ)) = ((๐นโ๐ฅ)(+gโ๐)(๐นโ๐ฆ)))) |
15 | | fveq1 6846 |
. . . . . . . 8
โข (๐ = ๐น โ (๐โ(๐ฅ ยท ๐ฆ)) = (๐นโ(๐ฅ ยท ๐ฆ))) |
16 | 11, 12 | oveq12d 7380 |
. . . . . . . 8
โข (๐ = ๐น โ ((๐โ๐ฅ) โ (๐โ๐ฆ)) = ((๐นโ๐ฅ) โ (๐นโ๐ฆ))) |
17 | 15, 16 | eqeq12d 2753 |
. . . . . . 7
โข (๐ = ๐น โ ((๐โ(๐ฅ ยท ๐ฆ)) = ((๐โ๐ฅ) โ (๐โ๐ฆ)) โ (๐นโ(๐ฅ ยท ๐ฆ)) = ((๐นโ๐ฅ) โ (๐นโ๐ฆ)))) |
18 | 14, 17 | anbi12d 632 |
. . . . . 6
โข (๐ = ๐น โ (((๐โ(๐ฅ(+gโ๐
)๐ฆ)) = ((๐โ๐ฅ)(+gโ๐)(๐โ๐ฆ)) โง (๐โ(๐ฅ ยท ๐ฆ)) = ((๐โ๐ฅ) โ (๐โ๐ฆ))) โ ((๐นโ(๐ฅ(+gโ๐
)๐ฆ)) = ((๐นโ๐ฅ)(+gโ๐)(๐นโ๐ฆ)) โง (๐นโ(๐ฅ ยท ๐ฆ)) = ((๐นโ๐ฅ) โ (๐นโ๐ฆ))))) |
19 | 18 | 2ralbidv 3213 |
. . . . 5
โข (๐ = ๐น โ (โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต ((๐โ(๐ฅ(+gโ๐
)๐ฆ)) = ((๐โ๐ฅ)(+gโ๐)(๐โ๐ฆ)) โง (๐โ(๐ฅ ยท ๐ฆ)) = ((๐โ๐ฅ) โ (๐โ๐ฆ))) โ โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต ((๐นโ(๐ฅ(+gโ๐
)๐ฆ)) = ((๐นโ๐ฅ)(+gโ๐)(๐นโ๐ฆ)) โง (๐นโ(๐ฅ ยท ๐ฆ)) = ((๐นโ๐ฅ) โ (๐นโ๐ฆ))))) |
20 | 19 | elrab 3650 |
. . . 4
โข (๐น โ {๐ โ ((Baseโ๐) โm ๐ต) โฃ โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต ((๐โ(๐ฅ(+gโ๐
)๐ฆ)) = ((๐โ๐ฅ)(+gโ๐)(๐โ๐ฆ)) โง (๐โ(๐ฅ ยท ๐ฆ)) = ((๐โ๐ฅ) โ (๐โ๐ฆ)))} โ (๐น โ ((Baseโ๐) โm ๐ต) โง โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต ((๐นโ(๐ฅ(+gโ๐
)๐ฆ)) = ((๐นโ๐ฅ)(+gโ๐)(๐นโ๐ฆ)) โง (๐นโ(๐ฅ ยท ๐ฆ)) = ((๐นโ๐ฅ) โ (๐นโ๐ฆ))))) |
21 | | r19.26-2 3136 |
. . . . . . 7
โข
(โ๐ฅ โ
๐ต โ๐ฆ โ ๐ต ((๐นโ(๐ฅ(+gโ๐
)๐ฆ)) = ((๐นโ๐ฅ)(+gโ๐)(๐นโ๐ฆ)) โง (๐นโ(๐ฅ ยท ๐ฆ)) = ((๐นโ๐ฅ) โ (๐นโ๐ฆ))) โ (โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต (๐นโ(๐ฅ(+gโ๐
)๐ฆ)) = ((๐นโ๐ฅ)(+gโ๐)(๐นโ๐ฆ)) โง โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต (๐นโ(๐ฅ ยท ๐ฆ)) = ((๐นโ๐ฅ) โ (๐นโ๐ฆ)))) |
22 | 21 | anbi2i 624 |
. . . . . 6
โข ((๐น โ ((Baseโ๐) โm ๐ต) โง โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต ((๐นโ(๐ฅ(+gโ๐
)๐ฆ)) = ((๐นโ๐ฅ)(+gโ๐)(๐นโ๐ฆ)) โง (๐นโ(๐ฅ ยท ๐ฆ)) = ((๐นโ๐ฅ) โ (๐นโ๐ฆ)))) โ (๐น โ ((Baseโ๐) โm ๐ต) โง (โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต (๐นโ(๐ฅ(+gโ๐
)๐ฆ)) = ((๐นโ๐ฅ)(+gโ๐)(๐นโ๐ฆ)) โง โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต (๐นโ(๐ฅ ยท ๐ฆ)) = ((๐นโ๐ฅ) โ (๐นโ๐ฆ))))) |
23 | | anass 470 |
. . . . . 6
โข (((๐น โ ((Baseโ๐) โm ๐ต) โง โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต (๐นโ(๐ฅ(+gโ๐
)๐ฆ)) = ((๐นโ๐ฅ)(+gโ๐)(๐นโ๐ฆ))) โง โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต (๐นโ(๐ฅ ยท ๐ฆ)) = ((๐นโ๐ฅ) โ (๐นโ๐ฆ))) โ (๐น โ ((Baseโ๐) โm ๐ต) โง (โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต (๐นโ(๐ฅ(+gโ๐
)๐ฆ)) = ((๐นโ๐ฅ)(+gโ๐)(๐นโ๐ฆ)) โง โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต (๐นโ(๐ฅ ยท ๐ฆ)) = ((๐นโ๐ฅ) โ (๐นโ๐ฆ))))) |
24 | 22, 23 | bitr4i 278 |
. . . . 5
โข ((๐น โ ((Baseโ๐) โm ๐ต) โง โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต ((๐นโ(๐ฅ(+gโ๐
)๐ฆ)) = ((๐นโ๐ฅ)(+gโ๐)(๐นโ๐ฆ)) โง (๐นโ(๐ฅ ยท ๐ฆ)) = ((๐นโ๐ฅ) โ (๐นโ๐ฆ)))) โ ((๐น โ ((Baseโ๐) โm ๐ต) โง โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต (๐นโ(๐ฅ(+gโ๐
)๐ฆ)) = ((๐นโ๐ฅ)(+gโ๐)(๐นโ๐ฆ))) โง โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต (๐นโ(๐ฅ ยท ๐ฆ)) = ((๐นโ๐ฅ) โ (๐นโ๐ฆ)))) |
25 | 2, 5, 6, 7 | isghm 19015 |
. . . . . . 7
โข (๐น โ (๐
GrpHom ๐) โ ((๐
โ Grp โง ๐ โ Grp) โง (๐น:๐ตโถ(Baseโ๐) โง โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต (๐นโ(๐ฅ(+gโ๐
)๐ฆ)) = ((๐นโ๐ฅ)(+gโ๐)(๐นโ๐ฆ))))) |
26 | | fvex 6860 |
. . . . . . . . . . 11
โข
(Baseโ๐)
โ V |
27 | 2 | fvexi 6861 |
. . . . . . . . . . 11
โข ๐ต โ V |
28 | 26, 27 | pm3.2i 472 |
. . . . . . . . . 10
โข
((Baseโ๐)
โ V โง ๐ต โ
V) |
29 | | elmapg 8785 |
. . . . . . . . . 10
โข
(((Baseโ๐)
โ V โง ๐ต โ V)
โ (๐น โ
((Baseโ๐)
โm ๐ต)
โ ๐น:๐ตโถ(Baseโ๐))) |
30 | 28, 29 | mp1i 13 |
. . . . . . . . 9
โข ((๐
โ Rng โง ๐ โ Rng) โ (๐น โ ((Baseโ๐) โm ๐ต) โ ๐น:๐ตโถ(Baseโ๐))) |
31 | 30 | anbi1d 631 |
. . . . . . . 8
โข ((๐
โ Rng โง ๐ โ Rng) โ ((๐น โ ((Baseโ๐) โm ๐ต) โง โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต (๐นโ(๐ฅ(+gโ๐
)๐ฆ)) = ((๐นโ๐ฅ)(+gโ๐)(๐นโ๐ฆ))) โ (๐น:๐ตโถ(Baseโ๐) โง โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต (๐นโ(๐ฅ(+gโ๐
)๐ฆ)) = ((๐นโ๐ฅ)(+gโ๐)(๐นโ๐ฆ))))) |
32 | | rngabl 46249 |
. . . . . . . . . 10
โข (๐
โ Rng โ ๐
โ Abel) |
33 | | ablgrp 19574 |
. . . . . . . . . 10
โข (๐
โ Abel โ ๐
โ Grp) |
34 | 32, 33 | syl 17 |
. . . . . . . . 9
โข (๐
โ Rng โ ๐
โ Grp) |
35 | | rngabl 46249 |
. . . . . . . . . 10
โข (๐ โ Rng โ ๐ โ Abel) |
36 | | ablgrp 19574 |
. . . . . . . . . 10
โข (๐ โ Abel โ ๐ โ Grp) |
37 | 35, 36 | syl 17 |
. . . . . . . . 9
โข (๐ โ Rng โ ๐ โ Grp) |
38 | | ibar 530 |
. . . . . . . . 9
โข ((๐
โ Grp โง ๐ โ Grp) โ ((๐น:๐ตโถ(Baseโ๐) โง โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต (๐นโ(๐ฅ(+gโ๐
)๐ฆ)) = ((๐นโ๐ฅ)(+gโ๐)(๐นโ๐ฆ))) โ ((๐
โ Grp โง ๐ โ Grp) โง (๐น:๐ตโถ(Baseโ๐) โง โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต (๐นโ(๐ฅ(+gโ๐
)๐ฆ)) = ((๐นโ๐ฅ)(+gโ๐)(๐นโ๐ฆ)))))) |
39 | 34, 37, 38 | syl2an 597 |
. . . . . . . 8
โข ((๐
โ Rng โง ๐ โ Rng) โ ((๐น:๐ตโถ(Baseโ๐) โง โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต (๐นโ(๐ฅ(+gโ๐
)๐ฆ)) = ((๐นโ๐ฅ)(+gโ๐)(๐นโ๐ฆ))) โ ((๐
โ Grp โง ๐ โ Grp) โง (๐น:๐ตโถ(Baseโ๐) โง โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต (๐นโ(๐ฅ(+gโ๐
)๐ฆ)) = ((๐นโ๐ฅ)(+gโ๐)(๐นโ๐ฆ)))))) |
40 | 31, 39 | bitr2d 280 |
. . . . . . 7
โข ((๐
โ Rng โง ๐ โ Rng) โ (((๐
โ Grp โง ๐ โ Grp) โง (๐น:๐ตโถ(Baseโ๐) โง โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต (๐นโ(๐ฅ(+gโ๐
)๐ฆ)) = ((๐นโ๐ฅ)(+gโ๐)(๐นโ๐ฆ)))) โ (๐น โ ((Baseโ๐) โm ๐ต) โง โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต (๐นโ(๐ฅ(+gโ๐
)๐ฆ)) = ((๐นโ๐ฅ)(+gโ๐)(๐นโ๐ฆ))))) |
41 | 25, 40 | bitr2id 284 |
. . . . . 6
โข ((๐
โ Rng โง ๐ โ Rng) โ ((๐น โ ((Baseโ๐) โm ๐ต) โง โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต (๐นโ(๐ฅ(+gโ๐
)๐ฆ)) = ((๐นโ๐ฅ)(+gโ๐)(๐นโ๐ฆ))) โ ๐น โ (๐
GrpHom ๐))) |
42 | 41 | anbi1d 631 |
. . . . 5
โข ((๐
โ Rng โง ๐ โ Rng) โ (((๐น โ ((Baseโ๐) โm ๐ต) โง โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต (๐นโ(๐ฅ(+gโ๐
)๐ฆ)) = ((๐นโ๐ฅ)(+gโ๐)(๐นโ๐ฆ))) โง โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต (๐นโ(๐ฅ ยท ๐ฆ)) = ((๐นโ๐ฅ) โ (๐นโ๐ฆ))) โ (๐น โ (๐
GrpHom ๐) โง โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต (๐นโ(๐ฅ ยท ๐ฆ)) = ((๐นโ๐ฅ) โ (๐นโ๐ฆ))))) |
43 | 24, 42 | bitrid 283 |
. . . 4
โข ((๐
โ Rng โง ๐ โ Rng) โ ((๐น โ ((Baseโ๐) โm ๐ต) โง โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต ((๐นโ(๐ฅ(+gโ๐
)๐ฆ)) = ((๐นโ๐ฅ)(+gโ๐)(๐นโ๐ฆ)) โง (๐นโ(๐ฅ ยท ๐ฆ)) = ((๐นโ๐ฅ) โ (๐นโ๐ฆ)))) โ (๐น โ (๐
GrpHom ๐) โง โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต (๐นโ(๐ฅ ยท ๐ฆ)) = ((๐นโ๐ฅ) โ (๐นโ๐ฆ))))) |
44 | 20, 43 | bitrid 283 |
. . 3
โข ((๐
โ Rng โง ๐ โ Rng) โ (๐น โ {๐ โ ((Baseโ๐) โm ๐ต) โฃ โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต ((๐โ(๐ฅ(+gโ๐
)๐ฆ)) = ((๐โ๐ฅ)(+gโ๐)(๐โ๐ฆ)) โง (๐โ(๐ฅ ยท ๐ฆ)) = ((๐โ๐ฅ) โ (๐โ๐ฆ)))} โ (๐น โ (๐
GrpHom ๐) โง โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต (๐นโ(๐ฅ ยท ๐ฆ)) = ((๐นโ๐ฅ) โ (๐นโ๐ฆ))))) |
45 | 9, 44 | bitrd 279 |
. 2
โข ((๐
โ Rng โง ๐ โ Rng) โ (๐น โ (๐
RngHomo ๐) โ (๐น โ (๐
GrpHom ๐) โง โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต (๐นโ(๐ฅ ยท ๐ฆ)) = ((๐นโ๐ฅ) โ (๐นโ๐ฆ))))) |
46 | 1, 45 | biadanii 821 |
1
โข (๐น โ (๐
RngHomo ๐) โ ((๐
โ Rng โง ๐ โ Rng) โง (๐น โ (๐
GrpHom ๐) โง โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต (๐นโ(๐ฅ ยท ๐ฆ)) = ((๐นโ๐ฅ) โ (๐นโ๐ฆ))))) |