Metamath Proof Explorer


Theorem rhmdvd

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

Ref Expression
Hypotheses rhmdvd.u 𝑈 = ( Unit ‘ 𝑆 )
rhmdvd.x 𝑋 = ( Base ‘ 𝑅 )
rhmdvd.d / = ( /r𝑆 )
rhmdvd.m · = ( .r𝑅 )
Assertion rhmdvd ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ ( 𝐴𝑋𝐵𝑋𝐶𝑋 ) ∧ ( ( 𝐹𝐵 ) ∈ 𝑈 ∧ ( 𝐹𝐶 ) ∈ 𝑈 ) ) → ( ( 𝐹𝐴 ) / ( 𝐹𝐵 ) ) = ( ( 𝐹 ‘ ( 𝐴 · 𝐶 ) ) / ( 𝐹 ‘ ( 𝐵 · 𝐶 ) ) ) )

Proof

Step Hyp Ref Expression
1 rhmdvd.u 𝑈 = ( Unit ‘ 𝑆 )
2 rhmdvd.x 𝑋 = ( Base ‘ 𝑅 )
3 rhmdvd.d / = ( /r𝑆 )
4 rhmdvd.m · = ( .r𝑅 )
5 simp1 ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ ( 𝐴𝑋𝐵𝑋𝐶𝑋 ) ∧ ( ( 𝐹𝐵 ) ∈ 𝑈 ∧ ( 𝐹𝐶 ) ∈ 𝑈 ) ) → 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) )
6 simp21 ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ ( 𝐴𝑋𝐵𝑋𝐶𝑋 ) ∧ ( ( 𝐹𝐵 ) ∈ 𝑈 ∧ ( 𝐹𝐶 ) ∈ 𝑈 ) ) → 𝐴𝑋 )
7 simp23 ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ ( 𝐴𝑋𝐵𝑋𝐶𝑋 ) ∧ ( ( 𝐹𝐵 ) ∈ 𝑈 ∧ ( 𝐹𝐶 ) ∈ 𝑈 ) ) → 𝐶𝑋 )
8 eqid ( .r𝑆 ) = ( .r𝑆 )
9 2 4 8 rhmmul ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐴𝑋𝐶𝑋 ) → ( 𝐹 ‘ ( 𝐴 · 𝐶 ) ) = ( ( 𝐹𝐴 ) ( .r𝑆 ) ( 𝐹𝐶 ) ) )
10 5 6 7 9 syl3anc ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ ( 𝐴𝑋𝐵𝑋𝐶𝑋 ) ∧ ( ( 𝐹𝐵 ) ∈ 𝑈 ∧ ( 𝐹𝐶 ) ∈ 𝑈 ) ) → ( 𝐹 ‘ ( 𝐴 · 𝐶 ) ) = ( ( 𝐹𝐴 ) ( .r𝑆 ) ( 𝐹𝐶 ) ) )
11 simp22 ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ ( 𝐴𝑋𝐵𝑋𝐶𝑋 ) ∧ ( ( 𝐹𝐵 ) ∈ 𝑈 ∧ ( 𝐹𝐶 ) ∈ 𝑈 ) ) → 𝐵𝑋 )
12 2 4 8 rhmmul ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐵𝑋𝐶𝑋 ) → ( 𝐹 ‘ ( 𝐵 · 𝐶 ) ) = ( ( 𝐹𝐵 ) ( .r𝑆 ) ( 𝐹𝐶 ) ) )
13 5 11 7 12 syl3anc ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ ( 𝐴𝑋𝐵𝑋𝐶𝑋 ) ∧ ( ( 𝐹𝐵 ) ∈ 𝑈 ∧ ( 𝐹𝐶 ) ∈ 𝑈 ) ) → ( 𝐹 ‘ ( 𝐵 · 𝐶 ) ) = ( ( 𝐹𝐵 ) ( .r𝑆 ) ( 𝐹𝐶 ) ) )
14 10 13 oveq12d ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ ( 𝐴𝑋𝐵𝑋𝐶𝑋 ) ∧ ( ( 𝐹𝐵 ) ∈ 𝑈 ∧ ( 𝐹𝐶 ) ∈ 𝑈 ) ) → ( ( 𝐹 ‘ ( 𝐴 · 𝐶 ) ) / ( 𝐹 ‘ ( 𝐵 · 𝐶 ) ) ) = ( ( ( 𝐹𝐴 ) ( .r𝑆 ) ( 𝐹𝐶 ) ) / ( ( 𝐹𝐵 ) ( .r𝑆 ) ( 𝐹𝐶 ) ) ) )
15 rhmrcl2 ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → 𝑆 ∈ Ring )
16 15 3ad2ant1 ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ ( 𝐴𝑋𝐵𝑋𝐶𝑋 ) ∧ ( ( 𝐹𝐵 ) ∈ 𝑈 ∧ ( 𝐹𝐶 ) ∈ 𝑈 ) ) → 𝑆 ∈ Ring )
17 eqid ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
18 2 17 rhmf ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → 𝐹 : 𝑋 ⟶ ( Base ‘ 𝑆 ) )
19 18 3ad2ant1 ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ ( 𝐴𝑋𝐵𝑋𝐶𝑋 ) ∧ ( ( 𝐹𝐵 ) ∈ 𝑈 ∧ ( 𝐹𝐶 ) ∈ 𝑈 ) ) → 𝐹 : 𝑋 ⟶ ( Base ‘ 𝑆 ) )
20 19 6 ffvelrnd ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ ( 𝐴𝑋𝐵𝑋𝐶𝑋 ) ∧ ( ( 𝐹𝐵 ) ∈ 𝑈 ∧ ( 𝐹𝐶 ) ∈ 𝑈 ) ) → ( 𝐹𝐴 ) ∈ ( Base ‘ 𝑆 ) )
21 simp3l ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ ( 𝐴𝑋𝐵𝑋𝐶𝑋 ) ∧ ( ( 𝐹𝐵 ) ∈ 𝑈 ∧ ( 𝐹𝐶 ) ∈ 𝑈 ) ) → ( 𝐹𝐵 ) ∈ 𝑈 )
22 simp3r ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ ( 𝐴𝑋𝐵𝑋𝐶𝑋 ) ∧ ( ( 𝐹𝐵 ) ∈ 𝑈 ∧ ( 𝐹𝐶 ) ∈ 𝑈 ) ) → ( 𝐹𝐶 ) ∈ 𝑈 )
23 17 1 3 8 dvrcan5 ( ( 𝑆 ∈ Ring ∧ ( ( 𝐹𝐴 ) ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹𝐵 ) ∈ 𝑈 ∧ ( 𝐹𝐶 ) ∈ 𝑈 ) ) → ( ( ( 𝐹𝐴 ) ( .r𝑆 ) ( 𝐹𝐶 ) ) / ( ( 𝐹𝐵 ) ( .r𝑆 ) ( 𝐹𝐶 ) ) ) = ( ( 𝐹𝐴 ) / ( 𝐹𝐵 ) ) )
24 16 20 21 22 23 syl13anc ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ ( 𝐴𝑋𝐵𝑋𝐶𝑋 ) ∧ ( ( 𝐹𝐵 ) ∈ 𝑈 ∧ ( 𝐹𝐶 ) ∈ 𝑈 ) ) → ( ( ( 𝐹𝐴 ) ( .r𝑆 ) ( 𝐹𝐶 ) ) / ( ( 𝐹𝐵 ) ( .r𝑆 ) ( 𝐹𝐶 ) ) ) = ( ( 𝐹𝐴 ) / ( 𝐹𝐵 ) ) )
25 14 24 eqtr2d ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ ( 𝐴𝑋𝐵𝑋𝐶𝑋 ) ∧ ( ( 𝐹𝐵 ) ∈ 𝑈 ∧ ( 𝐹𝐶 ) ∈ 𝑈 ) ) → ( ( 𝐹𝐴 ) / ( 𝐹𝐵 ) ) = ( ( 𝐹 ‘ ( 𝐴 · 𝐶 ) ) / ( 𝐹 ‘ ( 𝐵 · 𝐶 ) ) ) )