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 𝑋 = ( Base ‘ 𝑅 )
rhmdvdsr.m = ( ∥r𝑅 )
rhmdvdsr.n / = ( ∥r𝑆 )
Assertion rhmdvdsr ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐴𝑋𝐵𝑋 ) ∧ 𝐴 𝐵 ) → ( 𝐹𝐴 ) / ( 𝐹𝐵 ) )

Proof

Step Hyp Ref Expression
1 rhmdvdsr.x 𝑋 = ( Base ‘ 𝑅 )
2 rhmdvdsr.m = ( ∥r𝑅 )
3 rhmdvdsr.n / = ( ∥r𝑆 )
4 simpl1 ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐴𝑋𝐵𝑋 ) ∧ 𝐴 𝐵 ) → 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) )
5 simpl2 ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐴𝑋𝐵𝑋 ) ∧ 𝐴 𝐵 ) → 𝐴𝑋 )
6 eqid ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
7 1 6 rhmf ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → 𝐹 : 𝑋 ⟶ ( Base ‘ 𝑆 ) )
8 7 ffvelrnda ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐴𝑋 ) → ( 𝐹𝐴 ) ∈ ( Base ‘ 𝑆 ) )
9 4 5 8 syl2anc ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐴𝑋𝐵𝑋 ) ∧ 𝐴 𝐵 ) → ( 𝐹𝐴 ) ∈ ( Base ‘ 𝑆 ) )
10 simpll1 ( ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐴𝑋𝐵𝑋 ) ∧ 𝐴 𝐵 ) ∧ 𝑐𝑋 ) → 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) )
11 simpr ( ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐴𝑋𝐵𝑋 ) ∧ 𝐴 𝐵 ) ∧ 𝑐𝑋 ) → 𝑐𝑋 )
12 7 ffvelrnda ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝑐𝑋 ) → ( 𝐹𝑐 ) ∈ ( Base ‘ 𝑆 ) )
13 10 11 12 syl2anc ( ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐴𝑋𝐵𝑋 ) ∧ 𝐴 𝐵 ) ∧ 𝑐𝑋 ) → ( 𝐹𝑐 ) ∈ ( Base ‘ 𝑆 ) )
14 13 ralrimiva ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐴𝑋𝐵𝑋 ) ∧ 𝐴 𝐵 ) → ∀ 𝑐𝑋 ( 𝐹𝑐 ) ∈ ( Base ‘ 𝑆 ) )
15 5 adantr ( ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐴𝑋𝐵𝑋 ) ∧ 𝐴 𝐵 ) ∧ 𝑐𝑋 ) → 𝐴𝑋 )
16 eqid ( .r𝑅 ) = ( .r𝑅 )
17 eqid ( .r𝑆 ) = ( .r𝑆 )
18 1 16 17 rhmmul ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝑐𝑋𝐴𝑋 ) → ( 𝐹 ‘ ( 𝑐 ( .r𝑅 ) 𝐴 ) ) = ( ( 𝐹𝑐 ) ( .r𝑆 ) ( 𝐹𝐴 ) ) )
19 10 11 15 18 syl3anc ( ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐴𝑋𝐵𝑋 ) ∧ 𝐴 𝐵 ) ∧ 𝑐𝑋 ) → ( 𝐹 ‘ ( 𝑐 ( .r𝑅 ) 𝐴 ) ) = ( ( 𝐹𝑐 ) ( .r𝑆 ) ( 𝐹𝐴 ) ) )
20 19 ralrimiva ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐴𝑋𝐵𝑋 ) ∧ 𝐴 𝐵 ) → ∀ 𝑐𝑋 ( 𝐹 ‘ ( 𝑐 ( .r𝑅 ) 𝐴 ) ) = ( ( 𝐹𝑐 ) ( .r𝑆 ) ( 𝐹𝐴 ) ) )
21 simpr ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐴𝑋𝐵𝑋 ) ∧ 𝐴 𝐵 ) → 𝐴 𝐵 )
22 1 2 16 dvdsr2 ( 𝐴𝑋 → ( 𝐴 𝐵 ↔ ∃ 𝑐𝑋 ( 𝑐 ( .r𝑅 ) 𝐴 ) = 𝐵 ) )
23 22 biimpac ( ( 𝐴 𝐵𝐴𝑋 ) → ∃ 𝑐𝑋 ( 𝑐 ( .r𝑅 ) 𝐴 ) = 𝐵 )
24 21 5 23 syl2anc ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐴𝑋𝐵𝑋 ) ∧ 𝐴 𝐵 ) → ∃ 𝑐𝑋 ( 𝑐 ( .r𝑅 ) 𝐴 ) = 𝐵 )
25 r19.29 ( ( ∀ 𝑐𝑋 ( 𝐹 ‘ ( 𝑐 ( .r𝑅 ) 𝐴 ) ) = ( ( 𝐹𝑐 ) ( .r𝑆 ) ( 𝐹𝐴 ) ) ∧ ∃ 𝑐𝑋 ( 𝑐 ( .r𝑅 ) 𝐴 ) = 𝐵 ) → ∃ 𝑐𝑋 ( ( 𝐹 ‘ ( 𝑐 ( .r𝑅 ) 𝐴 ) ) = ( ( 𝐹𝑐 ) ( .r𝑆 ) ( 𝐹𝐴 ) ) ∧ ( 𝑐 ( .r𝑅 ) 𝐴 ) = 𝐵 ) )
26 simpl ( ( ( 𝐹 ‘ ( 𝑐 ( .r𝑅 ) 𝐴 ) ) = ( ( 𝐹𝑐 ) ( .r𝑆 ) ( 𝐹𝐴 ) ) ∧ ( 𝑐 ( .r𝑅 ) 𝐴 ) = 𝐵 ) → ( 𝐹 ‘ ( 𝑐 ( .r𝑅 ) 𝐴 ) ) = ( ( 𝐹𝑐 ) ( .r𝑆 ) ( 𝐹𝐴 ) ) )
27 simpr ( ( ( 𝐹 ‘ ( 𝑐 ( .r𝑅 ) 𝐴 ) ) = ( ( 𝐹𝑐 ) ( .r𝑆 ) ( 𝐹𝐴 ) ) ∧ ( 𝑐 ( .r𝑅 ) 𝐴 ) = 𝐵 ) → ( 𝑐 ( .r𝑅 ) 𝐴 ) = 𝐵 )
28 27 fveq2d ( ( ( 𝐹 ‘ ( 𝑐 ( .r𝑅 ) 𝐴 ) ) = ( ( 𝐹𝑐 ) ( .r𝑆 ) ( 𝐹𝐴 ) ) ∧ ( 𝑐 ( .r𝑅 ) 𝐴 ) = 𝐵 ) → ( 𝐹 ‘ ( 𝑐 ( .r𝑅 ) 𝐴 ) ) = ( 𝐹𝐵 ) )
29 26 28 eqtr3d ( ( ( 𝐹 ‘ ( 𝑐 ( .r𝑅 ) 𝐴 ) ) = ( ( 𝐹𝑐 ) ( .r𝑆 ) ( 𝐹𝐴 ) ) ∧ ( 𝑐 ( .r𝑅 ) 𝐴 ) = 𝐵 ) → ( ( 𝐹𝑐 ) ( .r𝑆 ) ( 𝐹𝐴 ) ) = ( 𝐹𝐵 ) )
30 29 reximi ( ∃ 𝑐𝑋 ( ( 𝐹 ‘ ( 𝑐 ( .r𝑅 ) 𝐴 ) ) = ( ( 𝐹𝑐 ) ( .r𝑆 ) ( 𝐹𝐴 ) ) ∧ ( 𝑐 ( .r𝑅 ) 𝐴 ) = 𝐵 ) → ∃ 𝑐𝑋 ( ( 𝐹𝑐 ) ( .r𝑆 ) ( 𝐹𝐴 ) ) = ( 𝐹𝐵 ) )
31 25 30 syl ( ( ∀ 𝑐𝑋 ( 𝐹 ‘ ( 𝑐 ( .r𝑅 ) 𝐴 ) ) = ( ( 𝐹𝑐 ) ( .r𝑆 ) ( 𝐹𝐴 ) ) ∧ ∃ 𝑐𝑋 ( 𝑐 ( .r𝑅 ) 𝐴 ) = 𝐵 ) → ∃ 𝑐𝑋 ( ( 𝐹𝑐 ) ( .r𝑆 ) ( 𝐹𝐴 ) ) = ( 𝐹𝐵 ) )
32 20 24 31 syl2anc ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐴𝑋𝐵𝑋 ) ∧ 𝐴 𝐵 ) → ∃ 𝑐𝑋 ( ( 𝐹𝑐 ) ( .r𝑆 ) ( 𝐹𝐴 ) ) = ( 𝐹𝐵 ) )
33 r19.29 ( ( ∀ 𝑐𝑋 ( 𝐹𝑐 ) ∈ ( Base ‘ 𝑆 ) ∧ ∃ 𝑐𝑋 ( ( 𝐹𝑐 ) ( .r𝑆 ) ( 𝐹𝐴 ) ) = ( 𝐹𝐵 ) ) → ∃ 𝑐𝑋 ( ( 𝐹𝑐 ) ∈ ( Base ‘ 𝑆 ) ∧ ( ( 𝐹𝑐 ) ( .r𝑆 ) ( 𝐹𝐴 ) ) = ( 𝐹𝐵 ) ) )
34 14 32 33 syl2anc ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐴𝑋𝐵𝑋 ) ∧ 𝐴 𝐵 ) → ∃ 𝑐𝑋 ( ( 𝐹𝑐 ) ∈ ( Base ‘ 𝑆 ) ∧ ( ( 𝐹𝑐 ) ( .r𝑆 ) ( 𝐹𝐴 ) ) = ( 𝐹𝐵 ) ) )
35 oveq1 ( 𝑦 = ( 𝐹𝑐 ) → ( 𝑦 ( .r𝑆 ) ( 𝐹𝐴 ) ) = ( ( 𝐹𝑐 ) ( .r𝑆 ) ( 𝐹𝐴 ) ) )
36 35 eqeq1d ( 𝑦 = ( 𝐹𝑐 ) → ( ( 𝑦 ( .r𝑆 ) ( 𝐹𝐴 ) ) = ( 𝐹𝐵 ) ↔ ( ( 𝐹𝑐 ) ( .r𝑆 ) ( 𝐹𝐴 ) ) = ( 𝐹𝐵 ) ) )
37 36 rspcev ( ( ( 𝐹𝑐 ) ∈ ( Base ‘ 𝑆 ) ∧ ( ( 𝐹𝑐 ) ( .r𝑆 ) ( 𝐹𝐴 ) ) = ( 𝐹𝐵 ) ) → ∃ 𝑦 ∈ ( Base ‘ 𝑆 ) ( 𝑦 ( .r𝑆 ) ( 𝐹𝐴 ) ) = ( 𝐹𝐵 ) )
38 37 rexlimivw ( ∃ 𝑐𝑋 ( ( 𝐹𝑐 ) ∈ ( Base ‘ 𝑆 ) ∧ ( ( 𝐹𝑐 ) ( .r𝑆 ) ( 𝐹𝐴 ) ) = ( 𝐹𝐵 ) ) → ∃ 𝑦 ∈ ( Base ‘ 𝑆 ) ( 𝑦 ( .r𝑆 ) ( 𝐹𝐴 ) ) = ( 𝐹𝐵 ) )
39 34 38 syl ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐴𝑋𝐵𝑋 ) ∧ 𝐴 𝐵 ) → ∃ 𝑦 ∈ ( Base ‘ 𝑆 ) ( 𝑦 ( .r𝑆 ) ( 𝐹𝐴 ) ) = ( 𝐹𝐵 ) )
40 6 3 17 dvdsr ( ( 𝐹𝐴 ) / ( 𝐹𝐵 ) ↔ ( ( 𝐹𝐴 ) ∈ ( Base ‘ 𝑆 ) ∧ ∃ 𝑦 ∈ ( Base ‘ 𝑆 ) ( 𝑦 ( .r𝑆 ) ( 𝐹𝐴 ) ) = ( 𝐹𝐵 ) ) )
41 9 39 40 sylanbrc ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐴𝑋𝐵𝑋 ) ∧ 𝐴 𝐵 ) → ( 𝐹𝐴 ) / ( 𝐹𝐵 ) )