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 ffvelcdmda ⊢ ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐴 ∈ 𝑋 ) → ( 𝐹 ‘ 𝐴 ) ∈ ( Base ‘ 𝑆 ) )
9 4 5 8 syl2anc ⊢ ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ 𝐴 ∥ 𝐵 ) → ( 𝐹 ‘ 𝐴 ) ∈ ( Base ‘ 𝑆 ) )
10 simpll1 ⊢ ( ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ 𝐴 ∥ 𝐵 ) ∧ 𝑐 ∈ 𝑋 ) → 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) )
11 simpr ⊢ ( ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ 𝐴 ∥ 𝐵 ) ∧ 𝑐 ∈ 𝑋 ) → 𝑐 ∈ 𝑋 )
12 7 ffvelcdmda ⊢ ( ( 𝐹 ∈ ( 𝑅 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 𝑆 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ 𝐴 ∥ 𝐵 ) → ( 𝐹 ‘ 𝐴 ) / ( 𝐹 ‘ 𝐵 ) )