Step | Hyp | Ref
| Expression |
1 | | dvdsr.2 |
. . 3
โข โฅ =
(โฅrโ๐
) |
2 | | fveq2 6846 |
. . . . . . . . 9
โข (๐ = ๐
โ (Baseโ๐) = (Baseโ๐
)) |
3 | | dvdsr.1 |
. . . . . . . . 9
โข ๐ต = (Baseโ๐
) |
4 | 2, 3 | eqtr4di 2791 |
. . . . . . . 8
โข (๐ = ๐
โ (Baseโ๐) = ๐ต) |
5 | 4 | eleq2d 2820 |
. . . . . . 7
โข (๐ = ๐
โ (๐ฅ โ (Baseโ๐) โ ๐ฅ โ ๐ต)) |
6 | 4 | rexeqdv 3313 |
. . . . . . 7
โข (๐ = ๐
โ (โ๐ง โ (Baseโ๐)(๐ง(.rโ๐)๐ฅ) = ๐ฆ โ โ๐ง โ ๐ต (๐ง(.rโ๐)๐ฅ) = ๐ฆ)) |
7 | 5, 6 | anbi12d 632 |
. . . . . 6
โข (๐ = ๐
โ ((๐ฅ โ (Baseโ๐) โง โ๐ง โ (Baseโ๐)(๐ง(.rโ๐)๐ฅ) = ๐ฆ) โ (๐ฅ โ ๐ต โง โ๐ง โ ๐ต (๐ง(.rโ๐)๐ฅ) = ๐ฆ))) |
8 | | fveq2 6846 |
. . . . . . . . . . 11
โข (๐ = ๐
โ (.rโ๐) = (.rโ๐
)) |
9 | | dvdsr.3 |
. . . . . . . . . . 11
โข ยท =
(.rโ๐
) |
10 | 8, 9 | eqtr4di 2791 |
. . . . . . . . . 10
โข (๐ = ๐
โ (.rโ๐) = ยท ) |
11 | 10 | oveqd 7378 |
. . . . . . . . 9
โข (๐ = ๐
โ (๐ง(.rโ๐)๐ฅ) = (๐ง ยท ๐ฅ)) |
12 | 11 | eqeq1d 2735 |
. . . . . . . 8
โข (๐ = ๐
โ ((๐ง(.rโ๐)๐ฅ) = ๐ฆ โ (๐ง ยท ๐ฅ) = ๐ฆ)) |
13 | 12 | rexbidv 3172 |
. . . . . . 7
โข (๐ = ๐
โ (โ๐ง โ ๐ต (๐ง(.rโ๐)๐ฅ) = ๐ฆ โ โ๐ง โ ๐ต (๐ง ยท ๐ฅ) = ๐ฆ)) |
14 | 13 | anbi2d 630 |
. . . . . 6
โข (๐ = ๐
โ ((๐ฅ โ ๐ต โง โ๐ง โ ๐ต (๐ง(.rโ๐)๐ฅ) = ๐ฆ) โ (๐ฅ โ ๐ต โง โ๐ง โ ๐ต (๐ง ยท ๐ฅ) = ๐ฆ))) |
15 | 7, 14 | bitrd 279 |
. . . . 5
โข (๐ = ๐
โ ((๐ฅ โ (Baseโ๐) โง โ๐ง โ (Baseโ๐)(๐ง(.rโ๐)๐ฅ) = ๐ฆ) โ (๐ฅ โ ๐ต โง โ๐ง โ ๐ต (๐ง ยท ๐ฅ) = ๐ฆ))) |
16 | 15 | opabbidv 5175 |
. . . 4
โข (๐ = ๐
โ {โจ๐ฅ, ๐ฆโฉ โฃ (๐ฅ โ (Baseโ๐) โง โ๐ง โ (Baseโ๐)(๐ง(.rโ๐)๐ฅ) = ๐ฆ)} = {โจ๐ฅ, ๐ฆโฉ โฃ (๐ฅ โ ๐ต โง โ๐ง โ ๐ต (๐ง ยท ๐ฅ) = ๐ฆ)}) |
17 | | df-dvdsr 20078 |
. . . 4
โข
โฅr = (๐ โ V โฆ {โจ๐ฅ, ๐ฆโฉ โฃ (๐ฅ โ (Baseโ๐) โง โ๐ง โ (Baseโ๐)(๐ง(.rโ๐)๐ฅ) = ๐ฆ)}) |
18 | 3 | fvexi 6860 |
. . . . 5
โข ๐ต โ V |
19 | | eqcom 2740 |
. . . . . . . . 9
โข ((๐ง ยท ๐ฅ) = ๐ฆ โ ๐ฆ = (๐ง ยท ๐ฅ)) |
20 | 19 | rexbii 3094 |
. . . . . . . 8
โข
(โ๐ง โ
๐ต (๐ง ยท ๐ฅ) = ๐ฆ โ โ๐ง โ ๐ต ๐ฆ = (๐ง ยท ๐ฅ)) |
21 | 20 | abbii 2803 |
. . . . . . 7
โข {๐ฆ โฃ โ๐ง โ ๐ต (๐ง ยท ๐ฅ) = ๐ฆ} = {๐ฆ โฃ โ๐ง โ ๐ต ๐ฆ = (๐ง ยท ๐ฅ)} |
22 | 18 | abrexex 7899 |
. . . . . . 7
โข {๐ฆ โฃ โ๐ง โ ๐ต ๐ฆ = (๐ง ยท ๐ฅ)} โ V |
23 | 21, 22 | eqeltri 2830 |
. . . . . 6
โข {๐ฆ โฃ โ๐ง โ ๐ต (๐ง ยท ๐ฅ) = ๐ฆ} โ V |
24 | 23 | a1i 11 |
. . . . 5
โข (๐ฅ โ ๐ต โ {๐ฆ โฃ โ๐ง โ ๐ต (๐ง ยท ๐ฅ) = ๐ฆ} โ V) |
25 | 18, 24 | opabex3 7904 |
. . . 4
โข
{โจ๐ฅ, ๐ฆโฉ โฃ (๐ฅ โ ๐ต โง โ๐ง โ ๐ต (๐ง ยท ๐ฅ) = ๐ฆ)} โ V |
26 | 16, 17, 25 | fvmpt 6952 |
. . 3
โข (๐
โ V โ
(โฅrโ๐
) = {โจ๐ฅ, ๐ฆโฉ โฃ (๐ฅ โ ๐ต โง โ๐ง โ ๐ต (๐ง ยท ๐ฅ) = ๐ฆ)}) |
27 | 1, 26 | eqtrid 2785 |
. 2
โข (๐
โ V โ โฅ =
{โจ๐ฅ, ๐ฆโฉ โฃ (๐ฅ โ ๐ต โง โ๐ง โ ๐ต (๐ง ยท ๐ฅ) = ๐ฆ)}) |
28 | | fvprc 6838 |
. . . 4
โข (ยฌ
๐
โ V โ
(โฅrโ๐
) = โ
) |
29 | 1, 28 | eqtrid 2785 |
. . 3
โข (ยฌ
๐
โ V โ โฅ =
โ
) |
30 | | opabn0 5514 |
. . . . 5
โข
({โจ๐ฅ, ๐ฆโฉ โฃ (๐ฅ โ ๐ต โง โ๐ง โ ๐ต (๐ง ยท ๐ฅ) = ๐ฆ)} โ โ
โ โ๐ฅโ๐ฆ(๐ฅ โ ๐ต โง โ๐ง โ ๐ต (๐ง ยท ๐ฅ) = ๐ฆ)) |
31 | | n0i 4297 |
. . . . . . . 8
โข (๐ฅ โ ๐ต โ ยฌ ๐ต = โ
) |
32 | | fvprc 6838 |
. . . . . . . . 9
โข (ยฌ
๐
โ V โ
(Baseโ๐
) =
โ
) |
33 | 3, 32 | eqtrid 2785 |
. . . . . . . 8
โข (ยฌ
๐
โ V โ ๐ต = โ
) |
34 | 31, 33 | nsyl2 141 |
. . . . . . 7
โข (๐ฅ โ ๐ต โ ๐
โ V) |
35 | 34 | adantr 482 |
. . . . . 6
โข ((๐ฅ โ ๐ต โง โ๐ง โ ๐ต (๐ง ยท ๐ฅ) = ๐ฆ) โ ๐
โ V) |
36 | 35 | exlimivv 1936 |
. . . . 5
โข
(โ๐ฅโ๐ฆ(๐ฅ โ ๐ต โง โ๐ง โ ๐ต (๐ง ยท ๐ฅ) = ๐ฆ) โ ๐
โ V) |
37 | 30, 36 | sylbi 216 |
. . . 4
โข
({โจ๐ฅ, ๐ฆโฉ โฃ (๐ฅ โ ๐ต โง โ๐ง โ ๐ต (๐ง ยท ๐ฅ) = ๐ฆ)} โ โ
โ ๐
โ V) |
38 | 37 | necon1bi 2969 |
. . 3
โข (ยฌ
๐
โ V โ
{โจ๐ฅ, ๐ฆโฉ โฃ (๐ฅ โ ๐ต โง โ๐ง โ ๐ต (๐ง ยท ๐ฅ) = ๐ฆ)} = โ
) |
39 | 29, 38 | eqtr4d 2776 |
. 2
โข (ยฌ
๐
โ V โ โฅ =
{โจ๐ฅ, ๐ฆโฉ โฃ (๐ฅ โ ๐ต โง โ๐ง โ ๐ต (๐ง ยท ๐ฅ) = ๐ฆ)}) |
40 | 27, 39 | pm2.61i 182 |
1
โข โฅ =
{โจ๐ฅ, ๐ฆโฉ โฃ (๐ฅ โ ๐ต โง โ๐ง โ ๐ต (๐ง ยท ๐ฅ) = ๐ฆ)} |