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 |
|- ( Y .|| Z <-> ( Y e. B /\ E. y e. B ( y ( .r ` R ) Y ) = Z ) ) |
5 |
1 2 3
|
dvdsr |
|- ( Z .|| X <-> ( Z e. B /\ E. x e. B ( x ( .r ` R ) Z ) = X ) ) |
6 |
4 5
|
anbi12i |
|- ( ( Y .|| Z /\ Z .|| X ) <-> ( ( Y e. B /\ E. y e. B ( y ( .r ` R ) Y ) = Z ) /\ ( Z e. B /\ E. x e. B ( x ( .r ` R ) Z ) = X ) ) ) |
7 |
|
an4 |
|- ( ( ( Y e. B /\ E. y e. B ( y ( .r ` R ) Y ) = Z ) /\ ( Z e. B /\ E. x e. B ( x ( .r ` R ) Z ) = X ) ) <-> ( ( Y e. B /\ Z e. B ) /\ ( E. y e. B ( y ( .r ` R ) Y ) = Z /\ E. x e. B ( x ( .r ` R ) Z ) = X ) ) ) |
8 |
6 7
|
bitri |
|- ( ( Y .|| Z /\ Z .|| X ) <-> ( ( Y e. B /\ Z e. B ) /\ ( E. y e. B ( y ( .r ` R ) Y ) = Z /\ E. x e. B ( x ( .r ` R ) Z ) = X ) ) ) |
9 |
|
reeanv |
|- ( E. y e. B E. x e. B ( ( y ( .r ` R ) Y ) = Z /\ ( x ( .r ` R ) Z ) = X ) <-> ( E. y e. B ( y ( .r ` R ) Y ) = Z /\ E. x e. B ( x ( .r ` R ) Z ) = X ) ) |
10 |
|
simplrl |
|- ( ( ( R e. Ring /\ ( Y e. B /\ Z e. B ) ) /\ ( y e. B /\ x e. B ) ) -> Y e. B ) |
11 |
|
simpll |
|- ( ( ( R e. Ring /\ ( Y e. B /\ Z e. B ) ) /\ ( y e. B /\ x e. B ) ) -> R e. Ring ) |
12 |
|
simprr |
|- ( ( ( R e. Ring /\ ( Y e. B /\ Z e. B ) ) /\ ( y e. B /\ x e. B ) ) -> x e. B ) |
13 |
|
simprl |
|- ( ( ( R e. Ring /\ ( Y e. B /\ Z e. B ) ) /\ ( y e. B /\ x e. B ) ) -> y e. B ) |
14 |
1 3
|
ringcl |
|- ( ( R e. Ring /\ x e. B /\ y e. B ) -> ( x ( .r ` R ) y ) e. B ) |
15 |
11 12 13 14
|
syl3anc |
|- ( ( ( R e. Ring /\ ( Y e. B /\ Z e. B ) ) /\ ( y e. B /\ x e. B ) ) -> ( x ( .r ` R ) y ) e. B ) |
16 |
1 2 3
|
dvdsrmul |
|- ( ( Y e. B /\ ( x ( .r ` R ) y ) e. B ) -> Y .|| ( ( x ( .r ` R ) y ) ( .r ` R ) Y ) ) |
17 |
10 15 16
|
syl2anc |
|- ( ( ( R e. Ring /\ ( Y e. B /\ Z e. B ) ) /\ ( y e. B /\ x e. B ) ) -> Y .|| ( ( x ( .r ` R ) y ) ( .r ` R ) Y ) ) |
18 |
1 3
|
ringass |
|- ( ( R e. Ring /\ ( x e. B /\ y e. B /\ Y e. B ) ) -> ( ( x ( .r ` R ) y ) ( .r ` R ) Y ) = ( x ( .r ` R ) ( y ( .r ` R ) Y ) ) ) |
19 |
11 12 13 10 18
|
syl13anc |
|- ( ( ( R e. Ring /\ ( Y e. B /\ Z e. B ) ) /\ ( y e. B /\ x e. B ) ) -> ( ( x ( .r ` R ) y ) ( .r ` R ) Y ) = ( x ( .r ` R ) ( y ( .r ` R ) Y ) ) ) |
20 |
17 19
|
breqtrd |
|- ( ( ( R e. Ring /\ ( Y e. B /\ Z e. B ) ) /\ ( y e. B /\ x e. B ) ) -> Y .|| ( x ( .r ` R ) ( y ( .r ` R ) Y ) ) ) |
21 |
|
oveq2 |
|- ( ( y ( .r ` R ) Y ) = Z -> ( x ( .r ` R ) ( y ( .r ` R ) Y ) ) = ( x ( .r ` R ) Z ) ) |
22 |
|
id |
|- ( ( x ( .r ` R ) Z ) = X -> ( x ( .r ` R ) Z ) = X ) |
23 |
21 22
|
sylan9eq |
|- ( ( ( y ( .r ` R ) Y ) = Z /\ ( x ( .r ` R ) Z ) = X ) -> ( x ( .r ` R ) ( y ( .r ` R ) Y ) ) = X ) |
24 |
23
|
breq2d |
|- ( ( ( y ( .r ` R ) Y ) = Z /\ ( x ( .r ` R ) Z ) = X ) -> ( Y .|| ( x ( .r ` R ) ( y ( .r ` R ) Y ) ) <-> Y .|| X ) ) |
25 |
20 24
|
syl5ibcom |
|- ( ( ( R e. Ring /\ ( Y e. B /\ Z e. B ) ) /\ ( y e. B /\ x e. B ) ) -> ( ( ( y ( .r ` R ) Y ) = Z /\ ( x ( .r ` R ) Z ) = X ) -> Y .|| X ) ) |
26 |
25
|
rexlimdvva |
|- ( ( R e. Ring /\ ( Y e. B /\ Z e. B ) ) -> ( E. y e. B E. x e. B ( ( y ( .r ` R ) Y ) = Z /\ ( x ( .r ` R ) Z ) = X ) -> Y .|| X ) ) |
27 |
9 26
|
syl5bir |
|- ( ( R e. Ring /\ ( Y e. B /\ Z e. B ) ) -> ( ( E. y e. B ( y ( .r ` R ) Y ) = Z /\ E. x e. B ( x ( .r ` R ) Z ) = X ) -> Y .|| X ) ) |
28 |
27
|
expimpd |
|- ( R e. Ring -> ( ( ( Y e. B /\ Z e. B ) /\ ( E. y e. B ( y ( .r ` R ) Y ) = Z /\ E. x e. B ( x ( .r ` R ) Z ) = X ) ) -> Y .|| X ) ) |
29 |
8 28
|
syl5bi |
|- ( R e. Ring -> ( ( Y .|| Z /\ Z .|| X ) -> Y .|| X ) ) |
30 |
29
|
3impib |
|- ( ( R e. Ring /\ Y .|| Z /\ Z .|| X ) -> Y .|| X ) |