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 ffvelcdmd ⊢ ( ( 𝐹 ∈ ( 𝑅 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 𝑆 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ∧ ( ( 𝐹 ‘ 𝐵 ) ∈ 𝑈 ∧ ( 𝐹 ‘ 𝐶 ) ∈ 𝑈 ) ) → ( ( 𝐹 ‘ 𝐴 ) / ( 𝐹 ‘ 𝐵 ) ) = ( ( 𝐹 ‘ ( 𝐴 · 𝐶 ) ) / ( 𝐹 ‘ ( 𝐵 · 𝐶 ) ) ) )