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 ffvelrnd
 |-  ( ( 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 ) ) ) )