Step | Hyp | Ref
| Expression |
1 | | dvdsr.1 |
. . . . 5
โข ๐ต = (Baseโ๐
) |
2 | 1 | a1i 9 |
. . . 4
โข ((๐
โ Ring โง ๐ โ ๐ต) โ ๐ต = (Baseโ๐
)) |
3 | | dvdsr.2 |
. . . . 5
โข โฅ =
(โฅrโ๐
) |
4 | 3 | a1i 9 |
. . . 4
โข ((๐
โ Ring โง ๐ โ ๐ต) โ โฅ =
(โฅrโ๐
)) |
5 | | ringsrg 13224 |
. . . . 5
โข (๐
โ Ring โ ๐
โ SRing) |
6 | 5 | adantr 276 |
. . . 4
โข ((๐
โ Ring โง ๐ โ ๐ต) โ ๐
โ SRing) |
7 | | dvdsrmul1.3 |
. . . . 5
โข ยท =
(.rโ๐
) |
8 | 7 | a1i 9 |
. . . 4
โข ((๐
โ Ring โง ๐ โ ๐ต) โ ยท =
(.rโ๐
)) |
9 | 2, 4, 6, 8 | dvdsrd 13263 |
. . 3
โข ((๐
โ Ring โง ๐ โ ๐ต) โ (๐ โฅ ๐ โ (๐ โ ๐ต โง โ๐ฅ โ ๐ต (๐ฅ ยท ๐) = ๐))) |
10 | 1 | a1i 9 |
. . . . . . . 8
โข ((((๐
โ Ring โง ๐ โ ๐ต) โง ๐ โ ๐ต) โง ๐ฅ โ ๐ต) โ ๐ต = (Baseโ๐
)) |
11 | 3 | a1i 9 |
. . . . . . . 8
โข ((((๐
โ Ring โง ๐ โ ๐ต) โง ๐ โ ๐ต) โง ๐ฅ โ ๐ต) โ โฅ =
(โฅrโ๐
)) |
12 | | simplll 533 |
. . . . . . . . 9
โข ((((๐
โ Ring โง ๐ โ ๐ต) โง ๐ โ ๐ต) โง ๐ฅ โ ๐ต) โ ๐
โ Ring) |
13 | 12, 5 | syl 14 |
. . . . . . . 8
โข ((((๐
โ Ring โง ๐ โ ๐ต) โง ๐ โ ๐ต) โง ๐ฅ โ ๐ต) โ ๐
โ SRing) |
14 | 7 | a1i 9 |
. . . . . . . 8
โข ((((๐
โ Ring โง ๐ โ ๐ต) โง ๐ โ ๐ต) โง ๐ฅ โ ๐ต) โ ยท =
(.rโ๐
)) |
15 | | simplr 528 |
. . . . . . . . 9
โข ((((๐
โ Ring โง ๐ โ ๐ต) โง ๐ โ ๐ต) โง ๐ฅ โ ๐ต) โ ๐ โ ๐ต) |
16 | | simpllr 534 |
. . . . . . . . 9
โข ((((๐
โ Ring โง ๐ โ ๐ต) โง ๐ โ ๐ต) โง ๐ฅ โ ๐ต) โ ๐ โ ๐ต) |
17 | 1, 7 | ringcl 13196 |
. . . . . . . . 9
โข ((๐
โ Ring โง ๐ โ ๐ต โง ๐ โ ๐ต) โ (๐ ยท ๐) โ ๐ต) |
18 | 12, 15, 16, 17 | syl3anc 1238 |
. . . . . . . 8
โข ((((๐
โ Ring โง ๐ โ ๐ต) โง ๐ โ ๐ต) โง ๐ฅ โ ๐ต) โ (๐ ยท ๐) โ ๐ต) |
19 | | simpr 110 |
. . . . . . . 8
โข ((((๐
โ Ring โง ๐ โ ๐ต) โง ๐ โ ๐ต) โง ๐ฅ โ ๐ต) โ ๐ฅ โ ๐ต) |
20 | 10, 11, 13, 14, 18, 19 | dvdsrmuld 13265 |
. . . . . . 7
โข ((((๐
โ Ring โง ๐ โ ๐ต) โง ๐ โ ๐ต) โง ๐ฅ โ ๐ต) โ (๐ ยท ๐) โฅ (๐ฅ ยท (๐ ยท ๐))) |
21 | 1, 7 | ringass 13199 |
. . . . . . . 8
โข ((๐
โ Ring โง (๐ฅ โ ๐ต โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ ((๐ฅ ยท ๐) ยท ๐) = (๐ฅ ยท (๐ ยท ๐))) |
22 | 12, 19, 15, 16, 21 | syl13anc 1240 |
. . . . . . 7
โข ((((๐
โ Ring โง ๐ โ ๐ต) โง ๐ โ ๐ต) โง ๐ฅ โ ๐ต) โ ((๐ฅ ยท ๐) ยท ๐) = (๐ฅ ยท (๐ ยท ๐))) |
23 | 20, 22 | breqtrrd 4032 |
. . . . . 6
โข ((((๐
โ Ring โง ๐ โ ๐ต) โง ๐ โ ๐ต) โง ๐ฅ โ ๐ต) โ (๐ ยท ๐) โฅ ((๐ฅ ยท ๐) ยท ๐)) |
24 | | oveq1 5882 |
. . . . . . 7
โข ((๐ฅ ยท ๐) = ๐ โ ((๐ฅ ยท ๐) ยท ๐) = (๐ ยท ๐)) |
25 | 24 | breq2d 4016 |
. . . . . 6
โข ((๐ฅ ยท ๐) = ๐ โ ((๐ ยท ๐) โฅ ((๐ฅ ยท ๐) ยท ๐) โ (๐ ยท ๐) โฅ (๐ ยท ๐))) |
26 | 23, 25 | syl5ibcom 155 |
. . . . 5
โข ((((๐
โ Ring โง ๐ โ ๐ต) โง ๐ โ ๐ต) โง ๐ฅ โ ๐ต) โ ((๐ฅ ยท ๐) = ๐ โ (๐ ยท ๐) โฅ (๐ ยท ๐))) |
27 | 26 | rexlimdva 2594 |
. . . 4
โข (((๐
โ Ring โง ๐ โ ๐ต) โง ๐ โ ๐ต) โ (โ๐ฅ โ ๐ต (๐ฅ ยท ๐) = ๐ โ (๐ ยท ๐) โฅ (๐ ยท ๐))) |
28 | 27 | expimpd 363 |
. . 3
โข ((๐
โ Ring โง ๐ โ ๐ต) โ ((๐ โ ๐ต โง โ๐ฅ โ ๐ต (๐ฅ ยท ๐) = ๐) โ (๐ ยท ๐) โฅ (๐ ยท ๐))) |
29 | 9, 28 | sylbid 150 |
. 2
โข ((๐
โ Ring โง ๐ โ ๐ต) โ (๐ โฅ ๐ โ (๐ ยท ๐) โฅ (๐ ยท ๐))) |
30 | 29 | 3impia 1200 |
1
โข ((๐
โ Ring โง ๐ โ ๐ต โง ๐ โฅ ๐) โ (๐ ยท ๐) โฅ (๐ ยท ๐)) |