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 ⊢ X = Base R
rhmdvdsr.m ⊢ ∥ ˙ = ∥ r ⁡ R
rhmdvdsr.n ⊢ × ˙ = ∥ r ⁡ S
Assertion rhmdvdsr ⊢ F ∈ R RingHom S ∧ A ∈ X ∧ B ∈ X ∧ A ∥ ˙ B → F ⁡ A × ˙ F ⁡ B

Proof

Step Hyp Ref Expression
1 rhmdvdsr.x ⊢ X = Base R
2 rhmdvdsr.m ⊢ ∥ ˙ = ∥ r ⁡ R
3 rhmdvdsr.n ⊢ × ˙ = ∥ r ⁡ S
4 simpl1 ⊢ F ∈ R RingHom S ∧ A ∈ X ∧ B ∈ X ∧ A ∥ ˙ B → F ∈ R RingHom S
5 simpl2 ⊢ F ∈ R RingHom S ∧ A ∈ X ∧ B ∈ X ∧ A ∥ ˙ B → A ∈ X
6 eqid ⊢ Base S = Base S
7 1 6 rhmf ⊢ F ∈ R RingHom S → F : X ⟶ Base S
8 7 ffvelcdmda ⊢ F ∈ R RingHom S ∧ A ∈ X → F ⁡ A ∈ Base S
9 4 5 8 syl2anc ⊢ F ∈ R RingHom S ∧ A ∈ X ∧ B ∈ X ∧ A ∥ ˙ B → F ⁡ A ∈ Base S
10 simpll1 ⊢ F ∈ R RingHom S ∧ A ∈ X ∧ B ∈ X ∧ A ∥ ˙ B ∧ c ∈ X → F ∈ R RingHom S
11 simpr ⊢ F ∈ R RingHom S ∧ A ∈ X ∧ B ∈ X ∧ A ∥ ˙ B ∧ c ∈ X → c ∈ X
12 7 ffvelcdmda ⊢ F ∈ R RingHom S ∧ c ∈ X → F ⁡ c ∈ Base S
13 10 11 12 syl2anc ⊢ F ∈ R RingHom S ∧ A ∈ X ∧ B ∈ X ∧ A ∥ ˙ B ∧ c ∈ X → F ⁡ c ∈ Base S
14 13 ralrimiva ⊢ F ∈ R RingHom S ∧ A ∈ X ∧ B ∈ X ∧ A ∥ ˙ B → ∀ c ∈ X F ⁡ c ∈ Base S
15 5 adantr ⊢ F ∈ R RingHom S ∧ A ∈ X ∧ B ∈ X ∧ A ∥ ˙ B ∧ c ∈ X → A ∈ X
16 eqid ⊢ ⋅ R = ⋅ R
17 eqid ⊢ ⋅ S = ⋅ S
18 1 16 17 rhmmul ⊢ F ∈ R RingHom S ∧ c ∈ X ∧ A ∈ X → F ⁡ c ⋅ R A = F ⁡ c ⋅ S F ⁡ A
19 10 11 15 18 syl3anc ⊢ F ∈ R RingHom S ∧ A ∈ X ∧ B ∈ X ∧ A ∥ ˙ B ∧ c ∈ X → F ⁡ c ⋅ R A = F ⁡ c ⋅ S F ⁡ A
20 19 ralrimiva ⊢ F ∈ R RingHom S ∧ A ∈ X ∧ B ∈ X ∧ A ∥ ˙ B → ∀ c ∈ X F ⁡ c ⋅ R A = F ⁡ c ⋅ S F ⁡ A
21 simpr ⊢ F ∈ R RingHom S ∧ A ∈ X ∧ B ∈ X ∧ A ∥ ˙ B → A ∥ ˙ B
22 1 2 16 dvdsr2 ⊢ A ∈ X → A ∥ ˙ B ↔ ∃ c ∈ X c ⋅ R A = B
23 22 biimpac ⊢ A ∥ ˙ B ∧ A ∈ X → ∃ c ∈ X c ⋅ R A = B
24 21 5 23 syl2anc ⊢ F ∈ R RingHom S ∧ A ∈ X ∧ B ∈ X ∧ A ∥ ˙ B → ∃ c ∈ X c ⋅ R A = B
25 r19.29 ⊢ ∀ c ∈ X F ⁡ c ⋅ R A = F ⁡ c ⋅ S F ⁡ A ∧ ∃ c ∈ X c ⋅ R A = B → ∃ c ∈ X F ⁡ c ⋅ R A = F ⁡ c ⋅ S F ⁡ A ∧ c ⋅ R A = B
26 simpl ⊢ F ⁡ c ⋅ R A = F ⁡ c ⋅ S F ⁡ A ∧ c ⋅ R A = B → F ⁡ c ⋅ R A = F ⁡ c ⋅ S F ⁡ A
27 simpr ⊢ F ⁡ c ⋅ R A = F ⁡ c ⋅ S F ⁡ A ∧ c ⋅ R A = B → c ⋅ R A = B
28 27 fveq2d ⊢ F ⁡ c ⋅ R A = F ⁡ c ⋅ S F ⁡ A ∧ c ⋅ R A = B → F ⁡ c ⋅ R A = F ⁡ B
29 26 28 eqtr3d ⊢ F ⁡ c ⋅ R A = F ⁡ c ⋅ S F ⁡ A ∧ c ⋅ R A = B → F ⁡ c ⋅ S F ⁡ A = F ⁡ B
30 29 reximi ⊢ ∃ c ∈ X F ⁡ c ⋅ R A = F ⁡ c ⋅ S F ⁡ A ∧ c ⋅ R A = B → ∃ c ∈ X F ⁡ c ⋅ S F ⁡ A = F ⁡ B
31 25 30 syl ⊢ ∀ c ∈ X F ⁡ c ⋅ R A = F ⁡ c ⋅ S F ⁡ A ∧ ∃ c ∈ X c ⋅ R A = B → ∃ c ∈ X F ⁡ c ⋅ S F ⁡ A = F ⁡ B
32 20 24 31 syl2anc ⊢ F ∈ R RingHom S ∧ A ∈ X ∧ B ∈ X ∧ A ∥ ˙ B → ∃ c ∈ X F ⁡ c ⋅ S F ⁡ A = F ⁡ B
33 r19.29 ⊢ ∀ c ∈ X F ⁡ c ∈ Base S ∧ ∃ c ∈ X F ⁡ c ⋅ S F ⁡ A = F ⁡ B → ∃ c ∈ X F ⁡ c ∈ Base S ∧ F ⁡ c ⋅ S F ⁡ A = F ⁡ B
34 14 32 33 syl2anc ⊢ F ∈ R RingHom S ∧ A ∈ X ∧ B ∈ X ∧ A ∥ ˙ B → ∃ c ∈ X F ⁡ c ∈ Base S ∧ F ⁡ c ⋅ S F ⁡ A = F ⁡ B
35 oveq1 ⊢ y = F ⁡ c → y ⋅ S F ⁡ A = F ⁡ c ⋅ S F ⁡ A
36 35 eqeq1d ⊢ y = F ⁡ c → y ⋅ S F ⁡ A = F ⁡ B ↔ F ⁡ c ⋅ S F ⁡ A = F ⁡ B
37 36 rspcev ⊢ F ⁡ c ∈ Base S ∧ F ⁡ c ⋅ S F ⁡ A = F ⁡ B → ∃ y ∈ Base S y ⋅ S F ⁡ A = F ⁡ B
38 37 rexlimivw ⊢ ∃ c ∈ X F ⁡ c ∈ Base S ∧ F ⁡ c ⋅ S F ⁡ A = F ⁡ B → ∃ y ∈ Base S y ⋅ S F ⁡ A = F ⁡ B
39 34 38 syl ⊢ F ∈ R RingHom S ∧ A ∈ X ∧ B ∈ X ∧ A ∥ ˙ B → ∃ y ∈ Base S y ⋅ S F ⁡ A = F ⁡ B
40 6 3 17 dvdsr ⊢ F ⁡ A × ˙ F ⁡ B ↔ F ⁡ A ∈ Base S ∧ ∃ y ∈ Base S y ⋅ S F ⁡ A = F ⁡ B
41 9 39 40 sylanbrc ⊢ F ∈ R RingHom S ∧ A ∈ X ∧ B ∈ X ∧ A ∥ ˙ B → F ⁡ A × ˙ F ⁡ B