Step | Hyp | Ref
| Expression |
1 | | df-dvdsr 13263 |
. . 3
โข
โฅr = (๐ โ V โฆ {โจ๐ฅ, ๐ฆโฉ โฃ (๐ฅ โ (Baseโ๐) โง โ๐ง โ (Baseโ๐)(๐ง(.rโ๐)๐ฅ) = ๐ฆ)}) |
2 | | fveq2 5517 |
. . . . . 6
โข (๐ = ๐
โ (Baseโ๐) = (Baseโ๐
)) |
3 | 2 | eleq2d 2247 |
. . . . 5
โข (๐ = ๐
โ (๐ฅ โ (Baseโ๐) โ ๐ฅ โ (Baseโ๐
))) |
4 | | fveq2 5517 |
. . . . . . . 8
โข (๐ = ๐
โ (.rโ๐) = (.rโ๐
)) |
5 | 4 | oveqd 5894 |
. . . . . . 7
โข (๐ = ๐
โ (๐ง(.rโ๐)๐ฅ) = (๐ง(.rโ๐
)๐ฅ)) |
6 | 5 | eqeq1d 2186 |
. . . . . 6
โข (๐ = ๐
โ ((๐ง(.rโ๐)๐ฅ) = ๐ฆ โ (๐ง(.rโ๐
)๐ฅ) = ๐ฆ)) |
7 | 2, 6 | rexeqbidv 2686 |
. . . . 5
โข (๐ = ๐
โ (โ๐ง โ (Baseโ๐)(๐ง(.rโ๐)๐ฅ) = ๐ฆ โ โ๐ง โ (Baseโ๐
)(๐ง(.rโ๐
)๐ฅ) = ๐ฆ)) |
8 | 3, 7 | anbi12d 473 |
. . . 4
โข (๐ = ๐
โ ((๐ฅ โ (Baseโ๐) โง โ๐ง โ (Baseโ๐)(๐ง(.rโ๐)๐ฅ) = ๐ฆ) โ (๐ฅ โ (Baseโ๐
) โง โ๐ง โ (Baseโ๐
)(๐ง(.rโ๐
)๐ฅ) = ๐ฆ))) |
9 | 8 | opabbidv 4071 |
. . 3
โข (๐ = ๐
โ {โจ๐ฅ, ๐ฆโฉ โฃ (๐ฅ โ (Baseโ๐) โง โ๐ง โ (Baseโ๐)(๐ง(.rโ๐)๐ฅ) = ๐ฆ)} = {โจ๐ฅ, ๐ฆโฉ โฃ (๐ฅ โ (Baseโ๐
) โง โ๐ง โ (Baseโ๐
)(๐ง(.rโ๐
)๐ฅ) = ๐ฆ)}) |
10 | | dvdsrvald.r |
. . . 4
โข (๐ โ ๐
โ SRing) |
11 | 10 | elexd 2752 |
. . 3
โข (๐ โ ๐
โ V) |
12 | | basfn 12522 |
. . . . . 6
โข Base Fn
V |
13 | | funfvex 5534 |
. . . . . . 7
โข ((Fun
Base โง ๐
โ dom
Base) โ (Baseโ๐
)
โ V) |
14 | 13 | funfni 5318 |
. . . . . 6
โข ((Base Fn
V โง ๐
โ V) โ
(Baseโ๐
) โ
V) |
15 | 12, 11, 14 | sylancr 414 |
. . . . 5
โข (๐ โ (Baseโ๐
) โ V) |
16 | | xpexg 4742 |
. . . . 5
โข
(((Baseโ๐
)
โ V โง (Baseโ๐
) โ V) โ ((Baseโ๐
) ร (Baseโ๐
)) โ V) |
17 | 15, 15, 16 | syl2anc 411 |
. . . 4
โข (๐ โ ((Baseโ๐
) ร (Baseโ๐
)) โ V) |
18 | | simprr 531 |
. . . . . . . . 9
โข (((๐ โง ๐ฅ โ (Baseโ๐
)) โง (๐ง โ (Baseโ๐
) โง (๐ง(.rโ๐
)๐ฅ) = ๐ฆ)) โ (๐ง(.rโ๐
)๐ฅ) = ๐ฆ) |
19 | 10 | ad2antrr 488 |
. . . . . . . . . 10
โข (((๐ โง ๐ฅ โ (Baseโ๐
)) โง (๐ง โ (Baseโ๐
) โง (๐ง(.rโ๐
)๐ฅ) = ๐ฆ)) โ ๐
โ SRing) |
20 | | simprl 529 |
. . . . . . . . . 10
โข (((๐ โง ๐ฅ โ (Baseโ๐
)) โง (๐ง โ (Baseโ๐
) โง (๐ง(.rโ๐
)๐ฅ) = ๐ฆ)) โ ๐ง โ (Baseโ๐
)) |
21 | | simplr 528 |
. . . . . . . . . 10
โข (((๐ โง ๐ฅ โ (Baseโ๐
)) โง (๐ง โ (Baseโ๐
) โง (๐ง(.rโ๐
)๐ฅ) = ๐ฆ)) โ ๐ฅ โ (Baseโ๐
)) |
22 | | eqid 2177 |
. . . . . . . . . . 11
โข
(Baseโ๐
) =
(Baseโ๐
) |
23 | | eqid 2177 |
. . . . . . . . . . 11
โข
(.rโ๐
) = (.rโ๐
) |
24 | 22, 23 | srgcl 13158 |
. . . . . . . . . 10
โข ((๐
โ SRing โง ๐ง โ (Baseโ๐
) โง ๐ฅ โ (Baseโ๐
)) โ (๐ง(.rโ๐
)๐ฅ) โ (Baseโ๐
)) |
25 | 19, 20, 21, 24 | syl3anc 1238 |
. . . . . . . . 9
โข (((๐ โง ๐ฅ โ (Baseโ๐
)) โง (๐ง โ (Baseโ๐
) โง (๐ง(.rโ๐
)๐ฅ) = ๐ฆ)) โ (๐ง(.rโ๐
)๐ฅ) โ (Baseโ๐
)) |
26 | 18, 25 | eqeltrrd 2255 |
. . . . . . . 8
โข (((๐ โง ๐ฅ โ (Baseโ๐
)) โง (๐ง โ (Baseโ๐
) โง (๐ง(.rโ๐
)๐ฅ) = ๐ฆ)) โ ๐ฆ โ (Baseโ๐
)) |
27 | 26 | rexlimdvaa 2595 |
. . . . . . 7
โข ((๐ โง ๐ฅ โ (Baseโ๐
)) โ (โ๐ง โ (Baseโ๐
)(๐ง(.rโ๐
)๐ฅ) = ๐ฆ โ ๐ฆ โ (Baseโ๐
))) |
28 | 27 | imdistanda 448 |
. . . . . 6
โข (๐ โ ((๐ฅ โ (Baseโ๐
) โง โ๐ง โ (Baseโ๐
)(๐ง(.rโ๐
)๐ฅ) = ๐ฆ) โ (๐ฅ โ (Baseโ๐
) โง ๐ฆ โ (Baseโ๐
)))) |
29 | 28 | ssopab2dv 4280 |
. . . . 5
โข (๐ โ {โจ๐ฅ, ๐ฆโฉ โฃ (๐ฅ โ (Baseโ๐
) โง โ๐ง โ (Baseโ๐
)(๐ง(.rโ๐
)๐ฅ) = ๐ฆ)} โ {โจ๐ฅ, ๐ฆโฉ โฃ (๐ฅ โ (Baseโ๐
) โง ๐ฆ โ (Baseโ๐
))}) |
30 | | df-xp 4634 |
. . . . 5
โข
((Baseโ๐
)
ร (Baseโ๐
)) =
{โจ๐ฅ, ๐ฆโฉ โฃ (๐ฅ โ (Baseโ๐
) โง ๐ฆ โ (Baseโ๐
))} |
31 | 29, 30 | sseqtrrdi 3206 |
. . . 4
โข (๐ โ {โจ๐ฅ, ๐ฆโฉ โฃ (๐ฅ โ (Baseโ๐
) โง โ๐ง โ (Baseโ๐
)(๐ง(.rโ๐
)๐ฅ) = ๐ฆ)} โ ((Baseโ๐
) ร (Baseโ๐
))) |
32 | 17, 31 | ssexd 4145 |
. . 3
โข (๐ โ {โจ๐ฅ, ๐ฆโฉ โฃ (๐ฅ โ (Baseโ๐
) โง โ๐ง โ (Baseโ๐
)(๐ง(.rโ๐
)๐ฅ) = ๐ฆ)} โ V) |
33 | 1, 9, 11, 32 | fvmptd3 5611 |
. 2
โข (๐ โ
(โฅrโ๐
) = {โจ๐ฅ, ๐ฆโฉ โฃ (๐ฅ โ (Baseโ๐
) โง โ๐ง โ (Baseโ๐
)(๐ง(.rโ๐
)๐ฅ) = ๐ฆ)}) |
34 | | dvdsrvald.2 |
. 2
โข (๐ โ โฅ =
(โฅrโ๐
)) |
35 | | dvdsrvald.1 |
. . . . 5
โข (๐ โ ๐ต = (Baseโ๐
)) |
36 | 35 | eleq2d 2247 |
. . . 4
โข (๐ โ (๐ฅ โ ๐ต โ ๐ฅ โ (Baseโ๐
))) |
37 | | dvdsrvald.3 |
. . . . . . 7
โข (๐ โ ยท =
(.rโ๐
)) |
38 | 37 | oveqd 5894 |
. . . . . 6
โข (๐ โ (๐ง ยท ๐ฅ) = (๐ง(.rโ๐
)๐ฅ)) |
39 | 38 | eqeq1d 2186 |
. . . . 5
โข (๐ โ ((๐ง ยท ๐ฅ) = ๐ฆ โ (๐ง(.rโ๐
)๐ฅ) = ๐ฆ)) |
40 | 35, 39 | rexeqbidv 2686 |
. . . 4
โข (๐ โ (โ๐ง โ ๐ต (๐ง ยท ๐ฅ) = ๐ฆ โ โ๐ง โ (Baseโ๐
)(๐ง(.rโ๐
)๐ฅ) = ๐ฆ)) |
41 | 36, 40 | anbi12d 473 |
. . 3
โข (๐ โ ((๐ฅ โ ๐ต โง โ๐ง โ ๐ต (๐ง ยท ๐ฅ) = ๐ฆ) โ (๐ฅ โ (Baseโ๐
) โง โ๐ง โ (Baseโ๐
)(๐ง(.rโ๐
)๐ฅ) = ๐ฆ))) |
42 | 41 | opabbidv 4071 |
. 2
โข (๐ โ {โจ๐ฅ, ๐ฆโฉ โฃ (๐ฅ โ ๐ต โง โ๐ง โ ๐ต (๐ง ยท ๐ฅ) = ๐ฆ)} = {โจ๐ฅ, ๐ฆโฉ โฃ (๐ฅ โ (Baseโ๐
) โง โ๐ง โ (Baseโ๐
)(๐ง(.rโ๐
)๐ฅ) = ๐ฆ)}) |
43 | 33, 34, 42 | 3eqtr4d 2220 |
1
โข (๐ โ โฅ = {โจ๐ฅ, ๐ฆโฉ โฃ (๐ฅ โ ๐ต โง โ๐ง โ ๐ต (๐ง ยท ๐ฅ) = ๐ฆ)}) |