Metamath Proof Explorer

Theorem dvdsrtr

Description: Divisibility is transitive. (Contributed by Mario Carneiro, 1-Dec-2014)

Ref Expression
Hypotheses dvdsr.1 
|- B = ( Base ` R )
dvdsr.2 
|- .|| = ( ||r ` R )
Assertion dvdsrtr 
|- ( ( R e. Ring /\ Y .|| Z /\ Z .|| X ) -> Y .|| X )

Proof

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 )