Step |
Hyp |
Ref |
Expression |
1 |
|
dvdsr.1 |
|- B = ( Base ` R ) |
2 |
|
dvdsr.2 |
|- .|| = ( ||r ` R ) |
3 |
|
eqid |
|- ( .r ` R ) = ( .r ` R ) |
4 |
1 2 3
|
dvdsr |
|- ( X .|| Y <-> ( X e. B /\ E. x e. B ( x ( .r ` R ) X ) = Y ) ) |
5 |
1 3
|
ringcl |
|- ( ( R e. Ring /\ x e. B /\ X e. B ) -> ( x ( .r ` R ) X ) e. B ) |
6 |
5
|
3expa |
|- ( ( ( R e. Ring /\ x e. B ) /\ X e. B ) -> ( x ( .r ` R ) X ) e. B ) |
7 |
6
|
an32s |
|- ( ( ( R e. Ring /\ X e. B ) /\ x e. B ) -> ( x ( .r ` R ) X ) e. B ) |
8 |
|
eleq1 |
|- ( ( x ( .r ` R ) X ) = Y -> ( ( x ( .r ` R ) X ) e. B <-> Y e. B ) ) |
9 |
7 8
|
syl5ibcom |
|- ( ( ( R e. Ring /\ X e. B ) /\ x e. B ) -> ( ( x ( .r ` R ) X ) = Y -> Y e. B ) ) |
10 |
9
|
rexlimdva |
|- ( ( R e. Ring /\ X e. B ) -> ( E. x e. B ( x ( .r ` R ) X ) = Y -> Y e. B ) ) |
11 |
10
|
impr |
|- ( ( R e. Ring /\ ( X e. B /\ E. x e. B ( x ( .r ` R ) X ) = Y ) ) -> Y e. B ) |
12 |
4 11
|
sylan2b |
|- ( ( R e. Ring /\ X .|| Y ) -> Y e. B ) |