Step | Hyp | Ref
| Expression |
1 | | dvdsr.1 |
. . . 4
โข ๐ต = (Baseโ๐
) |
2 | | dvdsr.2 |
. . . 4
โข โฅ =
(โฅrโ๐
) |
3 | | dvdsrmul1.3 |
. . . 4
โข ยท =
(.rโ๐
) |
4 | 1, 2, 3 | dvdsr 20076 |
. . 3
โข (๐ โฅ ๐ โ (๐ โ ๐ต โง โ๐ฅ โ ๐ต (๐ฅ ยท ๐) = ๐)) |
5 | | simplll 774 |
. . . . . . . . 9
โข ((((๐
โ Ring โง ๐ โ ๐ต) โง ๐ โ ๐ต) โง ๐ฅ โ ๐ต) โ ๐
โ Ring) |
6 | | simplr 768 |
. . . . . . . . 9
โข ((((๐
โ Ring โง ๐ โ ๐ต) โง ๐ โ ๐ต) โง ๐ฅ โ ๐ต) โ ๐ โ ๐ต) |
7 | | simpllr 775 |
. . . . . . . . 9
โข ((((๐
โ Ring โง ๐ โ ๐ต) โง ๐ โ ๐ต) โง ๐ฅ โ ๐ต) โ ๐ โ ๐ต) |
8 | 1, 3 | ringcl 19982 |
. . . . . . . . 9
โข ((๐
โ Ring โง ๐ โ ๐ต โง ๐ โ ๐ต) โ (๐ ยท ๐) โ ๐ต) |
9 | 5, 6, 7, 8 | syl3anc 1372 |
. . . . . . . 8
โข ((((๐
โ Ring โง ๐ โ ๐ต) โง ๐ โ ๐ต) โง ๐ฅ โ ๐ต) โ (๐ ยท ๐) โ ๐ต) |
10 | 1, 2, 3 | dvdsrmul 20078 |
. . . . . . . 8
โข (((๐ ยท ๐) โ ๐ต โง ๐ฅ โ ๐ต) โ (๐ ยท ๐) โฅ (๐ฅ ยท (๐ ยท ๐))) |
11 | 9, 10 | sylancom 589 |
. . . . . . 7
โข ((((๐
โ Ring โง ๐ โ ๐ต) โง ๐ โ ๐ต) โง ๐ฅ โ ๐ต) โ (๐ ยท ๐) โฅ (๐ฅ ยท (๐ ยท ๐))) |
12 | | simpr 486 |
. . . . . . . 8
โข ((((๐
โ Ring โง ๐ โ ๐ต) โง ๐ โ ๐ต) โง ๐ฅ โ ๐ต) โ ๐ฅ โ ๐ต) |
13 | 1, 3 | ringass 19985 |
. . . . . . . 8
โข ((๐
โ Ring โง (๐ฅ โ ๐ต โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ ((๐ฅ ยท ๐) ยท ๐) = (๐ฅ ยท (๐ ยท ๐))) |
14 | 5, 12, 6, 7, 13 | syl13anc 1373 |
. . . . . . 7
โข ((((๐
โ Ring โง ๐ โ ๐ต) โง ๐ โ ๐ต) โง ๐ฅ โ ๐ต) โ ((๐ฅ ยท ๐) ยท ๐) = (๐ฅ ยท (๐ ยท ๐))) |
15 | 11, 14 | breqtrrd 5134 |
. . . . . 6
โข ((((๐
โ Ring โง ๐ โ ๐ต) โง ๐ โ ๐ต) โง ๐ฅ โ ๐ต) โ (๐ ยท ๐) โฅ ((๐ฅ ยท ๐) ยท ๐)) |
16 | | oveq1 7365 |
. . . . . . 7
โข ((๐ฅ ยท ๐) = ๐ โ ((๐ฅ ยท ๐) ยท ๐) = (๐ ยท ๐)) |
17 | 16 | breq2d 5118 |
. . . . . 6
โข ((๐ฅ ยท ๐) = ๐ โ ((๐ ยท ๐) โฅ ((๐ฅ ยท ๐) ยท ๐) โ (๐ ยท ๐) โฅ (๐ ยท ๐))) |
18 | 15, 17 | syl5ibcom 244 |
. . . . 5
โข ((((๐
โ Ring โง ๐ โ ๐ต) โง ๐ โ ๐ต) โง ๐ฅ โ ๐ต) โ ((๐ฅ ยท ๐) = ๐ โ (๐ ยท ๐) โฅ (๐ ยท ๐))) |
19 | 18 | rexlimdva 3153 |
. . . 4
โข (((๐
โ Ring โง ๐ โ ๐ต) โง ๐ โ ๐ต) โ (โ๐ฅ โ ๐ต (๐ฅ ยท ๐) = ๐ โ (๐ ยท ๐) โฅ (๐ ยท ๐))) |
20 | 19 | expimpd 455 |
. . 3
โข ((๐
โ Ring โง ๐ โ ๐ต) โ ((๐ โ ๐ต โง โ๐ฅ โ ๐ต (๐ฅ ยท ๐) = ๐) โ (๐ ยท ๐) โฅ (๐ ยท ๐))) |
21 | 4, 20 | biimtrid 241 |
. 2
โข ((๐
โ Ring โง ๐ โ ๐ต) โ (๐ โฅ ๐ โ (๐ ยท ๐) โฅ (๐ ยท ๐))) |
22 | 21 | 3impia 1118 |
1
โข ((๐
โ Ring โง ๐ โ ๐ต โง ๐ โฅ ๐) โ (๐ ยท ๐) โฅ (๐ ยท ๐)) |