Metamath Proof Explorer

Theorem rhmdvd

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

Ref Expression
Hypotheses rhmdvd.u 
|- U = ( Unit ` S )
rhmdvd.x 
|- X = ( Base ` R )
rhmdvd.d 
|- ./ = ( /r ` S )
rhmdvd.m 
|- .x. = ( .r ` R )
Assertion rhmdvd 
|- ( ( F e. ( R RingHom S ) /\ ( A e. X /\ B e. X /\ C e. X ) /\ ( ( F ` B ) e. U /\ ( F ` C ) e. U ) ) -> ( ( F ` A ) ./ ( F ` B ) ) = ( ( F ` ( A .x. C ) ) ./ ( F ` ( B .x. C ) ) ) )

Proof

Step Hyp Ref Expression
1 rhmdvd.u 
 |-  U = ( Unit ` S )
2 rhmdvd.x 
 |-  X = ( Base ` R )
3 rhmdvd.d 
 |-  ./ = ( /r ` S )
4 rhmdvd.m 
 |-  .x. = ( .r ` R )
5 simp1 
 |-  ( ( F e. ( R RingHom S ) /\ ( A e. X /\ B e. X /\ C e. X ) /\ ( ( F ` B ) e. U /\ ( F ` C ) e. U ) ) -> F e. ( R RingHom S ) )
6 simp21 
 |-  ( ( F e. ( R RingHom S ) /\ ( A e. X /\ B e. X /\ C e. X ) /\ ( ( F ` B ) e. U /\ ( F ` C ) e. U ) ) -> A e. X )
7 simp23 
 |-  ( ( F e. ( R RingHom S ) /\ ( A e. X /\ B e. X /\ C e. X ) /\ ( ( F ` B ) e. U /\ ( F ` C ) e. U ) ) -> C e. X )
8 eqid 
 |-  ( .r ` S ) = ( .r ` S )
9 2 4 8 rhmmul 
 |-  ( ( F e. ( R RingHom S ) /\ A e. X /\ C e. X ) -> ( F ` ( A .x. C ) ) = ( ( F ` A ) ( .r ` S ) ( F ` C ) ) )
10 5 6 7 9 syl3anc 
 |-  ( ( F e. ( R RingHom S ) /\ ( A e. X /\ B e. X /\ C e. X ) /\ ( ( F ` B ) e. U /\ ( F ` C ) e. U ) ) -> ( F ` ( A .x. C ) ) = ( ( F ` A ) ( .r ` S ) ( F ` C ) ) )
11 simp22 
 |-  ( ( F e. ( R RingHom S ) /\ ( A e. X /\ B e. X /\ C e. X ) /\ ( ( F ` B ) e. U /\ ( F ` C ) e. U ) ) -> B e. X )
12 2 4 8 rhmmul 
 |-  ( ( F e. ( R RingHom S ) /\ B e. X /\ C e. X ) -> ( F ` ( B .x. C ) ) = ( ( F ` B ) ( .r ` S ) ( F ` C ) ) )
13 5 11 7 12 syl3anc 
 |-  ( ( F e. ( R RingHom S ) /\ ( A e. X /\ B e. X /\ C e. X ) /\ ( ( F ` B ) e. U /\ ( F ` C ) e. U ) ) -> ( F ` ( B .x. C ) ) = ( ( F ` B ) ( .r ` S ) ( F ` C ) ) )
14 10 13 oveq12d 
 |-  ( ( F e. ( R RingHom S ) /\ ( A e. X /\ B e. X /\ C e. X ) /\ ( ( F ` B ) e. U /\ ( F ` C ) e. U ) ) -> ( ( F ` ( A .x. C ) ) ./ ( F ` ( B .x. C ) ) ) = ( ( ( F ` A ) ( .r ` S ) ( F ` C ) ) ./ ( ( F ` B ) ( .r ` S ) ( F ` C ) ) ) )
15 rhmrcl2 
 |-  ( F e. ( R RingHom S ) -> S e. Ring )
16 15 3ad2ant1 
 |-  ( ( F e. ( R RingHom S ) /\ ( A e. X /\ B e. X /\ C e. X ) /\ ( ( F ` B ) e. U /\ ( F ` C ) e. U ) ) -> S e. Ring )
17 eqid 
 |-  ( Base ` S ) = ( Base ` S )
18 2 17 rhmf 
 |-  ( F e. ( R RingHom S ) -> F : X --> ( Base ` S ) )
19 18 3ad2ant1 
 |-  ( ( F e. ( R RingHom S ) /\ ( A e. X /\ B e. X /\ C e. X ) /\ ( ( F ` B ) e. U /\ ( F ` C ) e. U ) ) -> F : X --> ( Base ` S ) )
20 19 6 ffvelcdmd 
 |-  ( ( F e. ( R RingHom S ) /\ ( A e. X /\ B e. X /\ C e. X ) /\ ( ( F ` B ) e. U /\ ( F ` C ) e. U ) ) -> ( F ` A ) e. ( Base ` S ) )
21 simp3l 
 |-  ( ( F e. ( R RingHom S ) /\ ( A e. X /\ B e. X /\ C e. X ) /\ ( ( F ` B ) e. U /\ ( F ` C ) e. U ) ) -> ( F ` B ) e. U )
22 simp3r 
 |-  ( ( F e. ( R RingHom S ) /\ ( A e. X /\ B e. X /\ C e. X ) /\ ( ( F ` B ) e. U /\ ( F ` C ) e. U ) ) -> ( F ` C ) e. U )
23 17 1 3 8 dvrcan5 
 |-  ( ( S e. Ring /\ ( ( F ` A ) e. ( Base ` S ) /\ ( F ` B ) e. U /\ ( F ` C ) e. U ) ) -> ( ( ( F ` A ) ( .r ` S ) ( F ` C ) ) ./ ( ( F ` B ) ( .r ` S ) ( F ` C ) ) ) = ( ( F ` A ) ./ ( F ` B ) ) )
24 16 20 21 22 23 syl13anc 
 |-  ( ( F e. ( R RingHom S ) /\ ( A e. X /\ B e. X /\ C e. X ) /\ ( ( F ` B ) e. U /\ ( F ` C ) e. U ) ) -> ( ( ( F ` A ) ( .r ` S ) ( F ` C ) ) ./ ( ( F ` B ) ( .r ` S ) ( F ` C ) ) ) = ( ( F ` A ) ./ ( F ` B ) ) )
25 14 24 eqtr2d 
 |-  ( ( F e. ( R RingHom S ) /\ ( A e. X /\ B e. X /\ C e. X ) /\ ( ( F ` B ) e. U /\ ( F ` C ) e. U ) ) -> ( ( F ` A ) ./ ( F ` B ) ) = ( ( F ` ( A .x. C ) ) ./ ( F ` ( B .x. C ) ) ) )