Metamath Proof Explorer

Theorem rhmdvdsr

Description: A ring homomorphism preserves the divisibility relation. (Contributed by Thierry Arnoux, 22-Oct-2017)

Ref Expression
Hypotheses rhmdvdsr.x 
|- X = ( Base ` R )
rhmdvdsr.m 
|- .|| = ( ||r ` R )
rhmdvdsr.n 
|- ./ = ( ||r ` S )
Assertion rhmdvdsr 
|- ( ( ( F e. ( R RingHom S ) /\ A e. X /\ B e. X ) /\ A .|| B ) -> ( F ` A ) ./ ( F ` B ) )

Proof

Step Hyp Ref Expression
1 rhmdvdsr.x 
 |-  X = ( Base ` R )
2 rhmdvdsr.m 
 |-  .|| = ( ||r ` R )
3 rhmdvdsr.n 
 |-  ./ = ( ||r ` S )
4 simpl1 
 |-  ( ( ( F e. ( R RingHom S ) /\ A e. X /\ B e. X ) /\ A .|| B ) -> F e. ( R RingHom S ) )
5 simpl2 
 |-  ( ( ( F e. ( R RingHom S ) /\ A e. X /\ B e. X ) /\ A .|| B ) -> A e. X )
6 eqid 
 |-  ( Base ` S ) = ( Base ` S )
7 1 6 rhmf 
 |-  ( F e. ( R RingHom S ) -> F : X --> ( Base ` S ) )
8 7 ffvelrnda 
 |-  ( ( F e. ( R RingHom S ) /\ A e. X ) -> ( F ` A ) e. ( Base ` S ) )
9 4 5 8 syl2anc 
 |-  ( ( ( F e. ( R RingHom S ) /\ A e. X /\ B e. X ) /\ A .|| B ) -> ( F ` A ) e. ( Base ` S ) )
10 simpll1 
 |-  ( ( ( ( F e. ( R RingHom S ) /\ A e. X /\ B e. X ) /\ A .|| B ) /\ c e. X ) -> F e. ( R RingHom S ) )
11 simpr 
 |-  ( ( ( ( F e. ( R RingHom S ) /\ A e. X /\ B e. X ) /\ A .|| B ) /\ c e. X ) -> c e. X )
12 7 ffvelrnda 
 |-  ( ( F e. ( R RingHom S ) /\ c e. X ) -> ( F ` c ) e. ( Base ` S ) )
13 10 11 12 syl2anc 
 |-  ( ( ( ( F e. ( R RingHom S ) /\ A e. X /\ B e. X ) /\ A .|| B ) /\ c e. X ) -> ( F ` c ) e. ( Base ` S ) )
14 13 ralrimiva 
 |-  ( ( ( F e. ( R RingHom S ) /\ A e. X /\ B e. X ) /\ A .|| B ) -> A. c e. X ( F ` c ) e. ( Base ` S ) )
15 5 adantr 
 |-  ( ( ( ( F e. ( R RingHom S ) /\ A e. X /\ B e. X ) /\ A .|| B ) /\ c e. X ) -> A e. X )
16 eqid 
 |-  ( .r ` R ) = ( .r ` R )
17 eqid 
 |-  ( .r ` S ) = ( .r ` S )
18 1 16 17 rhmmul 
 |-  ( ( F e. ( R RingHom S ) /\ c e. X /\ A e. X ) -> ( F ` ( c ( .r ` R ) A ) ) = ( ( F ` c ) ( .r ` S ) ( F ` A ) ) )
19 10 11 15 18 syl3anc 
 |-  ( ( ( ( F e. ( R RingHom S ) /\ A e. X /\ B e. X ) /\ A .|| B ) /\ c e. X ) -> ( F ` ( c ( .r ` R ) A ) ) = ( ( F ` c ) ( .r ` S ) ( F ` A ) ) )
20 19 ralrimiva 
 |-  ( ( ( F e. ( R RingHom S ) /\ A e. X /\ B e. X ) /\ A .|| B ) -> A. c e. X ( F ` ( c ( .r ` R ) A ) ) = ( ( F ` c ) ( .r ` S ) ( F ` A ) ) )
21 simpr 
 |-  ( ( ( F e. ( R RingHom S ) /\ A e. X /\ B e. X ) /\ A .|| B ) -> A .|| B )
22 1 2 16 dvdsr2 
 |-  ( A e. X -> ( A .|| B <-> E. c e. X ( c ( .r ` R ) A ) = B ) )
23 22 biimpac 
 |-  ( ( A .|| B /\ A e. X ) -> E. c e. X ( c ( .r ` R ) A ) = B )
24 21 5 23 syl2anc 
 |-  ( ( ( F e. ( R RingHom S ) /\ A e. X /\ B e. X ) /\ A .|| B ) -> E. c e. X ( c ( .r ` R ) A ) = B )
25 r19.29 
 |-  ( ( A. c e. X ( F ` ( c ( .r ` R ) A ) ) = ( ( F ` c ) ( .r ` S ) ( F ` A ) ) /\ E. c e. X ( c ( .r ` R ) A ) = B ) -> E. c e. X ( ( F ` ( c ( .r ` R ) A ) ) = ( ( F ` c ) ( .r ` S ) ( F ` A ) ) /\ ( c ( .r ` R ) A ) = B ) )
26 simpl 
 |-  ( ( ( F ` ( c ( .r ` R ) A ) ) = ( ( F ` c ) ( .r ` S ) ( F ` A ) ) /\ ( c ( .r ` R ) A ) = B ) -> ( F ` ( c ( .r ` R ) A ) ) = ( ( F ` c ) ( .r ` S ) ( F ` A ) ) )
27 simpr 
 |-  ( ( ( F ` ( c ( .r ` R ) A ) ) = ( ( F ` c ) ( .r ` S ) ( F ` A ) ) /\ ( c ( .r ` R ) A ) = B ) -> ( c ( .r ` R ) A ) = B )
28 27 fveq2d 
 |-  ( ( ( F ` ( c ( .r ` R ) A ) ) = ( ( F ` c ) ( .r ` S ) ( F ` A ) ) /\ ( c ( .r ` R ) A ) = B ) -> ( F ` ( c ( .r ` R ) A ) ) = ( F ` B ) )
29 26 28 eqtr3d 
 |-  ( ( ( F ` ( c ( .r ` R ) A ) ) = ( ( F ` c ) ( .r ` S ) ( F ` A ) ) /\ ( c ( .r ` R ) A ) = B ) -> ( ( F ` c ) ( .r ` S ) ( F ` A ) ) = ( F ` B ) )
30 29 reximi 
 |-  ( E. c e. X ( ( F ` ( c ( .r ` R ) A ) ) = ( ( F ` c ) ( .r ` S ) ( F ` A ) ) /\ ( c ( .r ` R ) A ) = B ) -> E. c e. X ( ( F ` c ) ( .r ` S ) ( F ` A ) ) = ( F ` B ) )
31 25 30 syl 
 |-  ( ( A. c e. X ( F ` ( c ( .r ` R ) A ) ) = ( ( F ` c ) ( .r ` S ) ( F ` A ) ) /\ E. c e. X ( c ( .r ` R ) A ) = B ) -> E. c e. X ( ( F ` c ) ( .r ` S ) ( F ` A ) ) = ( F ` B ) )
32 20 24 31 syl2anc 
 |-  ( ( ( F e. ( R RingHom S ) /\ A e. X /\ B e. X ) /\ A .|| B ) -> E. c e. X ( ( F ` c ) ( .r ` S ) ( F ` A ) ) = ( F ` B ) )
33 r19.29 
 |-  ( ( A. c e. X ( F ` c ) e. ( Base ` S ) /\ E. c e. X ( ( F ` c ) ( .r ` S ) ( F ` A ) ) = ( F ` B ) ) -> E. c e. X ( ( F ` c ) e. ( Base ` S ) /\ ( ( F ` c ) ( .r ` S ) ( F ` A ) ) = ( F ` B ) ) )
34 14 32 33 syl2anc 
 |-  ( ( ( F e. ( R RingHom S ) /\ A e. X /\ B e. X ) /\ A .|| B ) -> E. c e. X ( ( F ` c ) e. ( Base ` S ) /\ ( ( F ` c ) ( .r ` S ) ( F ` A ) ) = ( F ` B ) ) )
35 oveq1 
 |-  ( y = ( F ` c ) -> ( y ( .r ` S ) ( F ` A ) ) = ( ( F ` c ) ( .r ` S ) ( F ` A ) ) )
36 35 eqeq1d 
 |-  ( y = ( F ` c ) -> ( ( y ( .r ` S ) ( F ` A ) ) = ( F ` B ) <-> ( ( F ` c ) ( .r ` S ) ( F ` A ) ) = ( F ` B ) ) )
37 36 rspcev 
 |-  ( ( ( F ` c ) e. ( Base ` S ) /\ ( ( F ` c ) ( .r ` S ) ( F ` A ) ) = ( F ` B ) ) -> E. y e. ( Base ` S ) ( y ( .r ` S ) ( F ` A ) ) = ( F ` B ) )
38 37 rexlimivw 
 |-  ( E. c e. X ( ( F ` c ) e. ( Base ` S ) /\ ( ( F ` c ) ( .r ` S ) ( F ` A ) ) = ( F ` B ) ) -> E. y e. ( Base ` S ) ( y ( .r ` S ) ( F ` A ) ) = ( F ` B ) )
39 34 38 syl 
 |-  ( ( ( F e. ( R RingHom S ) /\ A e. X /\ B e. X ) /\ A .|| B ) -> E. y e. ( Base ` S ) ( y ( .r ` S ) ( F ` A ) ) = ( F ` B ) )
40 6 3 17 dvdsr 
 |-  ( ( F ` A ) ./ ( F ` B ) <-> ( ( F ` A ) e. ( Base ` S ) /\ E. y e. ( Base ` S ) ( y ( .r ` S ) ( F ` A ) ) = ( F ` B ) ) )
41 9 39 40 sylanbrc 
 |-  ( ( ( F e. ( R RingHom S ) /\ A e. X /\ B e. X ) /\ A .|| B ) -> ( F ` A ) ./ ( F ` B ) )