Metamath Proof Explorer

Theorem dvdsrmul1

Description: The divisibility relation is preserved under right-multiplication. (Contributed by Mario Carneiro, 1-Dec-2014)

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

Proof

Step Hyp Ref Expression
1 dvdsr.1 
 |-  B = ( Base ` R )
2 dvdsr.2 
 |-  .|| = ( ||r ` R )
3 dvdsrmul1.3 
 |-  .x. = ( .r ` R )
4 1 2 3 dvdsr 
 |-  ( X .|| Y <-> ( X e. B /\ E. x e. B ( x .x. X ) = Y ) )
5 simplll 
 |-  ( ( ( ( R e. Ring /\ Z e. B ) /\ X e. B ) /\ x e. B ) -> R e. Ring )
6 simplr 
 |-  ( ( ( ( R e. Ring /\ Z e. B ) /\ X e. B ) /\ x e. B ) -> X e. B )
7 simpllr 
 |-  ( ( ( ( R e. Ring /\ Z e. B ) /\ X e. B ) /\ x e. B ) -> Z e. B )
8 1 3 ringcl 
 |-  ( ( R e. Ring /\ X e. B /\ Z e. B ) -> ( X .x. Z ) e. B )
9 5 6 7 8 syl3anc 
 |-  ( ( ( ( R e. Ring /\ Z e. B ) /\ X e. B ) /\ x e. B ) -> ( X .x. Z ) e. B )
10 1 2 3 dvdsrmul 
 |-  ( ( ( X .x. Z ) e. B /\ x e. B ) -> ( X .x. Z ) .|| ( x .x. ( X .x. Z ) ) )
11 9 10 sylancom 
 |-  ( ( ( ( R e. Ring /\ Z e. B ) /\ X e. B ) /\ x e. B ) -> ( X .x. Z ) .|| ( x .x. ( X .x. Z ) ) )
12 simpr 
 |-  ( ( ( ( R e. Ring /\ Z e. B ) /\ X e. B ) /\ x e. B ) -> x e. B )
13 1 3 ringass 
 |-  ( ( R e. Ring /\ ( x e. B /\ X e. B /\ Z e. B ) ) -> ( ( x .x. X ) .x. Z ) = ( x .x. ( X .x. Z ) ) )
14 5 12 6 7 13 syl13anc 
 |-  ( ( ( ( R e. Ring /\ Z e. B ) /\ X e. B ) /\ x e. B ) -> ( ( x .x. X ) .x. Z ) = ( x .x. ( X .x. Z ) ) )
15 11 14 breqtrrd 
 |-  ( ( ( ( R e. Ring /\ Z e. B ) /\ X e. B ) /\ x e. B ) -> ( X .x. Z ) .|| ( ( x .x. X ) .x. Z ) )
16 oveq1 
 |-  ( ( x .x. X ) = Y -> ( ( x .x. X ) .x. Z ) = ( Y .x. Z ) )
17 16 breq2d 
 |-  ( ( x .x. X ) = Y -> ( ( X .x. Z ) .|| ( ( x .x. X ) .x. Z ) <-> ( X .x. Z ) .|| ( Y .x. Z ) ) )
18 15 17 syl5ibcom 
 |-  ( ( ( ( R e. Ring /\ Z e. B ) /\ X e. B ) /\ x e. B ) -> ( ( x .x. X ) = Y -> ( X .x. Z ) .|| ( Y .x. Z ) ) )
19 18 rexlimdva 
 |-  ( ( ( R e. Ring /\ Z e. B ) /\ X e. B ) -> ( E. x e. B ( x .x. X ) = Y -> ( X .x. Z ) .|| ( Y .x. Z ) ) )
20 19 expimpd 
 |-  ( ( R e. Ring /\ Z e. B ) -> ( ( X e. B /\ E. x e. B ( x .x. X ) = Y ) -> ( X .x. Z ) .|| ( Y .x. Z ) ) )
21 4 20 syl5bi 
 |-  ( ( R e. Ring /\ Z e. B ) -> ( X .|| Y -> ( X .x. Z ) .|| ( Y .x. Z ) ) )
22 21 3impia 
 |-  ( ( R e. Ring /\ Z e. B /\ X .|| Y ) -> ( X .x. Z ) .|| ( Y .x. Z ) )