Step | Hyp | Ref
| Expression |
1 | | ringrng 46251 |
. . 3
โข (๐
โ Ring โ ๐
โ Rng) |
2 | | isringrng.b |
. . . . 5
โข ๐ต = (Baseโ๐
) |
3 | | isringrng.t |
. . . . 5
โข ยท =
(.rโ๐
) |
4 | 2, 3 | ringideu 19992 |
. . . 4
โข (๐
โ Ring โ
โ!๐ฅ โ ๐ต โ๐ฆ โ ๐ต ((๐ฅ ยท ๐ฆ) = ๐ฆ โง (๐ฆ ยท ๐ฅ) = ๐ฆ)) |
5 | | reurex 3360 |
. . . 4
โข
(โ!๐ฅ โ
๐ต โ๐ฆ โ ๐ต ((๐ฅ ยท ๐ฆ) = ๐ฆ โง (๐ฆ ยท ๐ฅ) = ๐ฆ) โ โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต ((๐ฅ ยท ๐ฆ) = ๐ฆ โง (๐ฆ ยท ๐ฅ) = ๐ฆ)) |
6 | 4, 5 | syl 17 |
. . 3
โข (๐
โ Ring โ โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต ((๐ฅ ยท ๐ฆ) = ๐ฆ โง (๐ฆ ยท ๐ฅ) = ๐ฆ)) |
7 | 1, 6 | jca 513 |
. 2
โข (๐
โ Ring โ (๐
โ Rng โง โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต ((๐ฅ ยท ๐ฆ) = ๐ฆ โง (๐ฆ ยท ๐ฅ) = ๐ฆ))) |
8 | | rngabl 46249 |
. . . . 5
โข (๐
โ Rng โ ๐
โ Abel) |
9 | | ablgrp 19574 |
. . . . 5
โข (๐
โ Abel โ ๐
โ Grp) |
10 | 8, 9 | syl 17 |
. . . 4
โข (๐
โ Rng โ ๐
โ Grp) |
11 | 10 | adantr 482 |
. . 3
โข ((๐
โ Rng โง โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต ((๐ฅ ยท ๐ฆ) = ๐ฆ โง (๐ฆ ยท ๐ฅ) = ๐ฆ)) โ ๐
โ Grp) |
12 | | eqid 2737 |
. . . . . 6
โข
(mulGrpโ๐
) =
(mulGrpโ๐
) |
13 | 12 | rngmgp 46250 |
. . . . 5
โข (๐
โ Rng โ
(mulGrpโ๐
) โ
Smgrp) |
14 | 13 | anim1i 616 |
. . . 4
โข ((๐
โ Rng โง โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต ((๐ฅ ยท ๐ฆ) = ๐ฆ โง (๐ฆ ยท ๐ฅ) = ๐ฆ)) โ ((mulGrpโ๐
) โ Smgrp โง โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต ((๐ฅ ยท ๐ฆ) = ๐ฆ โง (๐ฆ ยท ๐ฅ) = ๐ฆ))) |
15 | 12, 2 | mgpbas 19909 |
. . . . 5
โข ๐ต =
(Baseโ(mulGrpโ๐
)) |
16 | 12, 3 | mgpplusg 19907 |
. . . . 5
โข ยท =
(+gโ(mulGrpโ๐
)) |
17 | 15, 16 | ismnddef 18565 |
. . . 4
โข
((mulGrpโ๐
)
โ Mnd โ ((mulGrpโ๐
) โ Smgrp โง โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต ((๐ฅ ยท ๐ฆ) = ๐ฆ โง (๐ฆ ยท ๐ฅ) = ๐ฆ))) |
18 | 14, 17 | sylibr 233 |
. . 3
โข ((๐
โ Rng โง โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต ((๐ฅ ยท ๐ฆ) = ๐ฆ โง (๐ฆ ยท ๐ฅ) = ๐ฆ)) โ (mulGrpโ๐
) โ Mnd) |
19 | | eqid 2737 |
. . . . . 6
โข
(+gโ๐
) = (+gโ๐
) |
20 | 2, 12, 19, 3 | isrng 46248 |
. . . . 5
โข (๐
โ Rng โ (๐
โ Abel โง
(mulGrpโ๐
) โ
Smgrp โง โ๐ฅ
โ ๐ต โ๐ฆ โ ๐ต โ๐ง โ ๐ต ((๐ฅ ยท (๐ฆ(+gโ๐
)๐ง)) = ((๐ฅ ยท ๐ฆ)(+gโ๐
)(๐ฅ ยท ๐ง)) โง ((๐ฅ(+gโ๐
)๐ฆ) ยท ๐ง) = ((๐ฅ ยท ๐ง)(+gโ๐
)(๐ฆ ยท ๐ง))))) |
21 | 20 | simp3bi 1148 |
. . . 4
โข (๐
โ Rng โ โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต โ๐ง โ ๐ต ((๐ฅ ยท (๐ฆ(+gโ๐
)๐ง)) = ((๐ฅ ยท ๐ฆ)(+gโ๐
)(๐ฅ ยท ๐ง)) โง ((๐ฅ(+gโ๐
)๐ฆ) ยท ๐ง) = ((๐ฅ ยท ๐ง)(+gโ๐
)(๐ฆ ยท ๐ง)))) |
22 | 21 | adantr 482 |
. . 3
โข ((๐
โ Rng โง โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต ((๐ฅ ยท ๐ฆ) = ๐ฆ โง (๐ฆ ยท ๐ฅ) = ๐ฆ)) โ โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต โ๐ง โ ๐ต ((๐ฅ ยท (๐ฆ(+gโ๐
)๐ง)) = ((๐ฅ ยท ๐ฆ)(+gโ๐
)(๐ฅ ยท ๐ง)) โง ((๐ฅ(+gโ๐
)๐ฆ) ยท ๐ง) = ((๐ฅ ยท ๐ง)(+gโ๐
)(๐ฆ ยท ๐ง)))) |
23 | 2, 12, 19, 3 | isring 19975 |
. . 3
โข (๐
โ Ring โ (๐
โ Grp โง
(mulGrpโ๐
) โ Mnd
โง โ๐ฅ โ
๐ต โ๐ฆ โ ๐ต โ๐ง โ ๐ต ((๐ฅ ยท (๐ฆ(+gโ๐
)๐ง)) = ((๐ฅ ยท ๐ฆ)(+gโ๐
)(๐ฅ ยท ๐ง)) โง ((๐ฅ(+gโ๐
)๐ฆ) ยท ๐ง) = ((๐ฅ ยท ๐ง)(+gโ๐
)(๐ฆ ยท ๐ง))))) |
24 | 11, 18, 22, 23 | syl3anbrc 1344 |
. 2
โข ((๐
โ Rng โง โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต ((๐ฅ ยท ๐ฆ) = ๐ฆ โง (๐ฆ ยท ๐ฅ) = ๐ฆ)) โ ๐
โ Ring) |
25 | 7, 24 | impbii 208 |
1
โข (๐
โ Ring โ (๐
โ Rng โง โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต ((๐ฅ ยท ๐ฆ) = ๐ฆ โง (๐ฆ ยท ๐ฅ) = ๐ฆ))) |