Step | Hyp | Ref
| Expression |
1 | | dvdsr.2 |
. . . 4
โข โฅ =
(โฅrโ๐
) |
2 | 1 | reldvdsr 20081 |
. . 3
โข Rel โฅ |
3 | 2 | brrelex12i 5691 |
. 2
โข (๐ โฅ ๐ โ (๐ โ V โง ๐ โ V)) |
4 | | elex 3465 |
. . 3
โข (๐ โ ๐ต โ ๐ โ V) |
5 | | id 22 |
. . . . 5
โข ((๐ง ยท ๐) = ๐ โ (๐ง ยท ๐) = ๐) |
6 | | ovex 7394 |
. . . . 5
โข (๐ง ยท ๐) โ V |
7 | 5, 6 | eqeltrrdi 2843 |
. . . 4
โข ((๐ง ยท ๐) = ๐ โ ๐ โ V) |
8 | 7 | rexlimivw 3145 |
. . 3
โข
(โ๐ง โ
๐ต (๐ง ยท ๐) = ๐ โ ๐ โ V) |
9 | 4, 8 | anim12i 614 |
. 2
โข ((๐ โ ๐ต โง โ๐ง โ ๐ต (๐ง ยท ๐) = ๐) โ (๐ โ V โง ๐ โ V)) |
10 | | simpl 484 |
. . . . 5
โข ((๐ฅ = ๐ โง ๐ฆ = ๐) โ ๐ฅ = ๐) |
11 | 10 | eleq1d 2819 |
. . . 4
โข ((๐ฅ = ๐ โง ๐ฆ = ๐) โ (๐ฅ โ ๐ต โ ๐ โ ๐ต)) |
12 | 10 | oveq2d 7377 |
. . . . . 6
โข ((๐ฅ = ๐ โง ๐ฆ = ๐) โ (๐ง ยท ๐ฅ) = (๐ง ยท ๐)) |
13 | | simpr 486 |
. . . . . 6
โข ((๐ฅ = ๐ โง ๐ฆ = ๐) โ ๐ฆ = ๐) |
14 | 12, 13 | eqeq12d 2749 |
. . . . 5
โข ((๐ฅ = ๐ โง ๐ฆ = ๐) โ ((๐ง ยท ๐ฅ) = ๐ฆ โ (๐ง ยท ๐) = ๐)) |
15 | 14 | rexbidv 3172 |
. . . 4
โข ((๐ฅ = ๐ โง ๐ฆ = ๐) โ (โ๐ง โ ๐ต (๐ง ยท ๐ฅ) = ๐ฆ โ โ๐ง โ ๐ต (๐ง ยท ๐) = ๐)) |
16 | 11, 15 | anbi12d 632 |
. . 3
โข ((๐ฅ = ๐ โง ๐ฆ = ๐) โ ((๐ฅ โ ๐ต โง โ๐ง โ ๐ต (๐ง ยท ๐ฅ) = ๐ฆ) โ (๐ โ ๐ต โง โ๐ง โ ๐ต (๐ง ยท ๐) = ๐))) |
17 | | dvdsr.1 |
. . . 4
โข ๐ต = (Baseโ๐
) |
18 | | dvdsr.3 |
. . . 4
โข ยท =
(.rโ๐
) |
19 | 17, 1, 18 | dvdsrval 20082 |
. . 3
โข โฅ =
{โจ๐ฅ, ๐ฆโฉ โฃ (๐ฅ โ ๐ต โง โ๐ง โ ๐ต (๐ง ยท ๐ฅ) = ๐ฆ)} |
20 | 16, 19 | brabga 5495 |
. 2
โข ((๐ โ V โง ๐ โ V) โ (๐ โฅ ๐ โ (๐ โ ๐ต โง โ๐ง โ ๐ต (๐ง ยท ๐) = ๐))) |
21 | 3, 9, 20 | pm5.21nii 380 |
1
โข (๐ โฅ ๐ โ (๐ โ ๐ต โง โ๐ง โ ๐ต (๐ง ยท ๐) = ๐)) |