Step | Hyp | Ref
| Expression |
1 | | dvdsrvald.r |
. . . . . 6
โข (๐ โ ๐
โ SRing) |
2 | | reldvdsrsrg 13266 |
. . . . . 6
โข (๐
โ SRing โ Rel
(โฅrโ๐
)) |
3 | 1, 2 | syl 14 |
. . . . 5
โข (๐ โ Rel
(โฅrโ๐
)) |
4 | | dvdsrvald.2 |
. . . . . 6
โข (๐ โ โฅ =
(โฅrโ๐
)) |
5 | 4 | releqd 4712 |
. . . . 5
โข (๐ โ (Rel โฅ โ Rel
(โฅrโ๐
))) |
6 | 3, 5 | mpbird 167 |
. . . 4
โข (๐ โ Rel โฅ ) |
7 | | brrelex12 4666 |
. . . 4
โข ((Rel
โฅ
โง ๐ โฅ ๐) โ (๐ โ V โง ๐ โ V)) |
8 | 6, 7 | sylan 283 |
. . 3
โข ((๐ โง ๐ โฅ ๐) โ (๐ โ V โง ๐ โ V)) |
9 | 8 | ex 115 |
. 2
โข (๐ โ (๐ โฅ ๐ โ (๐ โ V โง ๐ โ V))) |
10 | | simplr 528 |
. . . . . 6
โข (((๐ โง ๐ โ ๐ต) โง (๐ง โ ๐ต โง (๐ง ยท ๐) = ๐)) โ ๐ โ ๐ต) |
11 | 10 | elexd 2752 |
. . . . 5
โข (((๐ โง ๐ โ ๐ต) โง (๐ง โ ๐ต โง (๐ง ยท ๐) = ๐)) โ ๐ โ V) |
12 | | simprr 531 |
. . . . . . 7
โข (((๐ โง ๐ โ ๐ต) โง (๐ง โ ๐ต โง (๐ง ยท ๐) = ๐)) โ (๐ง ยท ๐) = ๐) |
13 | 1 | ad2antrr 488 |
. . . . . . . . 9
โข (((๐ โง ๐ โ ๐ต) โง (๐ง โ ๐ต โง (๐ง ยท ๐) = ๐)) โ ๐
โ SRing) |
14 | | simprl 529 |
. . . . . . . . . 10
โข (((๐ โง ๐ โ ๐ต) โง (๐ง โ ๐ต โง (๐ง ยท ๐) = ๐)) โ ๐ง โ ๐ต) |
15 | | dvdsrvald.1 |
. . . . . . . . . . 11
โข (๐ โ ๐ต = (Baseโ๐
)) |
16 | 15 | ad2antrr 488 |
. . . . . . . . . 10
โข (((๐ โง ๐ โ ๐ต) โง (๐ง โ ๐ต โง (๐ง ยท ๐) = ๐)) โ ๐ต = (Baseโ๐
)) |
17 | 14, 16 | eleqtrd 2256 |
. . . . . . . . 9
โข (((๐ โง ๐ โ ๐ต) โง (๐ง โ ๐ต โง (๐ง ยท ๐) = ๐)) โ ๐ง โ (Baseโ๐
)) |
18 | 10, 16 | eleqtrd 2256 |
. . . . . . . . 9
โข (((๐ โง ๐ โ ๐ต) โง (๐ง โ ๐ต โง (๐ง ยท ๐) = ๐)) โ ๐ โ (Baseโ๐
)) |
19 | | eqid 2177 |
. . . . . . . . . 10
โข
(Baseโ๐
) =
(Baseโ๐
) |
20 | | eqid 2177 |
. . . . . . . . . 10
โข
(.rโ๐
) = (.rโ๐
) |
21 | 19, 20 | srgcl 13158 |
. . . . . . . . 9
โข ((๐
โ SRing โง ๐ง โ (Baseโ๐
) โง ๐ โ (Baseโ๐
)) โ (๐ง(.rโ๐
)๐) โ (Baseโ๐
)) |
22 | 13, 17, 18, 21 | syl3anc 1238 |
. . . . . . . 8
โข (((๐ โง ๐ โ ๐ต) โง (๐ง โ ๐ต โง (๐ง ยท ๐) = ๐)) โ (๐ง(.rโ๐
)๐) โ (Baseโ๐
)) |
23 | | dvdsrvald.3 |
. . . . . . . . . 10
โข (๐ โ ยท =
(.rโ๐
)) |
24 | 23 | ad2antrr 488 |
. . . . . . . . 9
โข (((๐ โง ๐ โ ๐ต) โง (๐ง โ ๐ต โง (๐ง ยท ๐) = ๐)) โ ยท =
(.rโ๐
)) |
25 | 24 | oveqd 5894 |
. . . . . . . 8
โข (((๐ โง ๐ โ ๐ต) โง (๐ง โ ๐ต โง (๐ง ยท ๐) = ๐)) โ (๐ง ยท ๐) = (๐ง(.rโ๐
)๐)) |
26 | 22, 25, 16 | 3eltr4d 2261 |
. . . . . . 7
โข (((๐ โง ๐ โ ๐ต) โง (๐ง โ ๐ต โง (๐ง ยท ๐) = ๐)) โ (๐ง ยท ๐) โ ๐ต) |
27 | 12, 26 | eqeltrrd 2255 |
. . . . . 6
โข (((๐ โง ๐ โ ๐ต) โง (๐ง โ ๐ต โง (๐ง ยท ๐) = ๐)) โ ๐ โ ๐ต) |
28 | 27 | elexd 2752 |
. . . . 5
โข (((๐ โง ๐ โ ๐ต) โง (๐ง โ ๐ต โง (๐ง ยท ๐) = ๐)) โ ๐ โ V) |
29 | 11, 28 | jca 306 |
. . . 4
โข (((๐ โง ๐ โ ๐ต) โง (๐ง โ ๐ต โง (๐ง ยท ๐) = ๐)) โ (๐ โ V โง ๐ โ V)) |
30 | 29 | rexlimdvaa 2595 |
. . 3
โข ((๐ โง ๐ โ ๐ต) โ (โ๐ง โ ๐ต (๐ง ยท ๐) = ๐ โ (๐ โ V โง ๐ โ V))) |
31 | 30 | expimpd 363 |
. 2
โข (๐ โ ((๐ โ ๐ต โง โ๐ง โ ๐ต (๐ง ยท ๐) = ๐) โ (๐ โ V โง ๐ โ V))) |
32 | 15, 4, 1, 23 | dvdsrvald 13267 |
. . . . . 6
โข (๐ โ โฅ = {โจ๐ฅ, ๐ฆโฉ โฃ (๐ฅ โ ๐ต โง โ๐ง โ ๐ต (๐ง ยท ๐ฅ) = ๐ฆ)}) |
33 | 32 | adantr 276 |
. . . . 5
โข ((๐ โง (๐ โ V โง ๐ โ V)) โ โฅ = {โจ๐ฅ, ๐ฆโฉ โฃ (๐ฅ โ ๐ต โง โ๐ง โ ๐ต (๐ง ยท ๐ฅ) = ๐ฆ)}) |
34 | 33 | breqd 4016 |
. . . 4
โข ((๐ โง (๐ โ V โง ๐ โ V)) โ (๐ โฅ ๐ โ ๐{โจ๐ฅ, ๐ฆโฉ โฃ (๐ฅ โ ๐ต โง โ๐ง โ ๐ต (๐ง ยท ๐ฅ) = ๐ฆ)}๐)) |
35 | | simpl 109 |
. . . . . . . 8
โข ((๐ฅ = ๐ โง ๐ฆ = ๐) โ ๐ฅ = ๐) |
36 | 35 | eleq1d 2246 |
. . . . . . 7
โข ((๐ฅ = ๐ โง ๐ฆ = ๐) โ (๐ฅ โ ๐ต โ ๐ โ ๐ต)) |
37 | 35 | oveq2d 5893 |
. . . . . . . . 9
โข ((๐ฅ = ๐ โง ๐ฆ = ๐) โ (๐ง ยท ๐ฅ) = (๐ง ยท ๐)) |
38 | | simpr 110 |
. . . . . . . . 9
โข ((๐ฅ = ๐ โง ๐ฆ = ๐) โ ๐ฆ = ๐) |
39 | 37, 38 | eqeq12d 2192 |
. . . . . . . 8
โข ((๐ฅ = ๐ โง ๐ฆ = ๐) โ ((๐ง ยท ๐ฅ) = ๐ฆ โ (๐ง ยท ๐) = ๐)) |
40 | 39 | rexbidv 2478 |
. . . . . . 7
โข ((๐ฅ = ๐ โง ๐ฆ = ๐) โ (โ๐ง โ ๐ต (๐ง ยท ๐ฅ) = ๐ฆ โ โ๐ง โ ๐ต (๐ง ยท ๐) = ๐)) |
41 | 36, 40 | anbi12d 473 |
. . . . . 6
โข ((๐ฅ = ๐ โง ๐ฆ = ๐) โ ((๐ฅ โ ๐ต โง โ๐ง โ ๐ต (๐ง ยท ๐ฅ) = ๐ฆ) โ (๐ โ ๐ต โง โ๐ง โ ๐ต (๐ง ยท ๐) = ๐))) |
42 | | eqid 2177 |
. . . . . 6
โข
{โจ๐ฅ, ๐ฆโฉ โฃ (๐ฅ โ ๐ต โง โ๐ง โ ๐ต (๐ง ยท ๐ฅ) = ๐ฆ)} = {โจ๐ฅ, ๐ฆโฉ โฃ (๐ฅ โ ๐ต โง โ๐ง โ ๐ต (๐ง ยท ๐ฅ) = ๐ฆ)} |
43 | 41, 42 | brabga 4266 |
. . . . 5
โข ((๐ โ V โง ๐ โ V) โ (๐{โจ๐ฅ, ๐ฆโฉ โฃ (๐ฅ โ ๐ต โง โ๐ง โ ๐ต (๐ง ยท ๐ฅ) = ๐ฆ)}๐ โ (๐ โ ๐ต โง โ๐ง โ ๐ต (๐ง ยท ๐) = ๐))) |
44 | 43 | adantl 277 |
. . . 4
โข ((๐ โง (๐ โ V โง ๐ โ V)) โ (๐{โจ๐ฅ, ๐ฆโฉ โฃ (๐ฅ โ ๐ต โง โ๐ง โ ๐ต (๐ง ยท ๐ฅ) = ๐ฆ)}๐ โ (๐ โ ๐ต โง โ๐ง โ ๐ต (๐ง ยท ๐) = ๐))) |
45 | 34, 44 | bitrd 188 |
. . 3
โข ((๐ โง (๐ โ V โง ๐ โ V)) โ (๐ โฅ ๐ โ (๐ โ ๐ต โง โ๐ง โ ๐ต (๐ง ยท ๐) = ๐))) |
46 | 45 | ex 115 |
. 2
โข (๐ โ ((๐ โ V โง ๐ โ V) โ (๐ โฅ ๐ โ (๐ โ ๐ต โง โ๐ง โ ๐ต (๐ง ยท ๐) = ๐)))) |
47 | 9, 31, 46 | pm5.21ndd 705 |
1
โข (๐ โ (๐ โฅ ๐ โ (๐ โ ๐ต โง โ๐ง โ ๐ต (๐ง ยท ๐) = ๐))) |