rhmdvd

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

	Ref	Expression
Hypotheses	rhmdvd.u	$⊢ U = Unit (S)$
	rhmdvd.x	$⊢ X = {Base}_{R}$
	rhmdvd.d	$⊢ \underset{˙}{\times} = /_{r} (S)$
	rhmdvd.m	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
Assertion	rhmdvd	$⊢ (F \in (R RingHom S) \land (A \in X \land B \in X \land C \in X) \land (F (B) \in U \land F (C) \in U)) \to F (A) \underset{˙}{\times} F (B) = F (A \underset{˙}{\cdot} C) \underset{˙}{\times} F (B \underset{˙}{\cdot} C)$

Proof

Step	Hyp	Ref	Expression
1		rhmdvd.u	$⊢ U = Unit (S)$
2		rhmdvd.x	$⊢ X = {Base}_{R}$
3		rhmdvd.d	$⊢ \underset{˙}{\times} = /_{r} (S)$
4		rhmdvd.m	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
5		simp1	$⊢ (F \in (R RingHom S) \land (A \in X \land B \in X \land C \in X) \land (F (B) \in U \land F (C) \in U)) \to F \in (R RingHom S)$
6		simp21	$⊢ (F \in (R RingHom S) \land (A \in X \land B \in X \land C \in X) \land (F (B) \in U \land F (C) \in U)) \to A \in X$
7		simp23	$⊢ (F \in (R RingHom S) \land (A \in X \land B \in X \land C \in X) \land (F (B) \in U \land F (C) \in U)) \to C \in X$
8		eqid	$⊢ \cdot_{S} = \cdot_{S}$
9	2 4 8	rhmmul	$⊢ (F \in (R RingHom S) \land A \in X \land C \in X) \to F (A \underset{˙}{\cdot} C) = F (A) \cdot_{S} F (C)$
10	5 6 7 9	syl3anc	$⊢ (F \in (R RingHom S) \land (A \in X \land B \in X \land C \in X) \land (F (B) \in U \land F (C) \in U)) \to F (A \underset{˙}{\cdot} C) = F (A) \cdot_{S} F (C)$
11		simp22	$⊢ (F \in (R RingHom S) \land (A \in X \land B \in X \land C \in X) \land (F (B) \in U \land F (C) \in U)) \to B \in X$
12	2 4 8	rhmmul	$⊢ (F \in (R RingHom S) \land B \in X \land C \in X) \to F (B \underset{˙}{\cdot} C) = F (B) \cdot_{S} F (C)$
13	5 11 7 12	syl3anc	$⊢ (F \in (R RingHom S) \land (A \in X \land B \in X \land C \in X) \land (F (B) \in U \land F (C) \in U)) \to F (B \underset{˙}{\cdot} C) = F (B) \cdot_{S} F (C)$
14	10 13	oveq12d	$⊢ (F \in (R RingHom S) \land (A \in X \land B \in X \land C \in X) \land (F (B) \in U \land F (C) \in U)) \to F (A \underset{˙}{\cdot} C) \underset{˙}{\times} F (B \underset{˙}{\cdot} C) = (F (A) \cdot_{S} F (C)) \underset{˙}{\times} (F (B) \cdot_{S} F (C))$
15		rhmrcl2	$⊢ F \in (R RingHom S) \to S \in Ring$
16	15	3ad2ant1	$⊢ (F \in (R RingHom S) \land (A \in X \land B \in X \land C \in X) \land (F (B) \in U \land F (C) \in U)) \to S \in Ring$
17		eqid	$⊢ {Base}_{S} = {Base}_{S}$
18	2 17	rhmf	$⊢ F \in (R RingHom S) \to F : X ⟶ {Base}_{S}$
19	18	3ad2ant1	$⊢ (F \in (R RingHom S) \land (A \in X \land B \in X \land C \in X) \land (F (B) \in U \land F (C) \in U)) \to F : X ⟶ {Base}_{S}$
20	19 6	ffvelrnd	$⊢ (F \in (R RingHom S) \land (A \in X \land B \in X \land C \in X) \land (F (B) \in U \land F (C) \in U)) \to F (A) \in {Base}_{S}$
21		simp3l	$⊢ (F \in (R RingHom S) \land (A \in X \land B \in X \land C \in X) \land (F (B) \in U \land F (C) \in U)) \to F (B) \in U$
22		simp3r	$⊢ (F \in (R RingHom S) \land (A \in X \land B \in X \land C \in X) \land (F (B) \in U \land F (C) \in U)) \to F (C) \in U$
23	17 1 3 8	dvrcan5	$⊢ (S \in Ring \land (F (A) \in {Base}_{S} \land F (B) \in U \land F (C) \in U)) \to (F (A) \cdot_{S} F (C)) \underset{˙}{\times} (F (B) \cdot_{S} F (C)) = F (A) \underset{˙}{\times} F (B)$
24	16 20 21 22 23	syl13anc	$⊢ (F \in (R RingHom S) \land (A \in X \land B \in X \land C \in X) \land (F (B) \in U \land F (C) \in U)) \to (F (A) \cdot_{S} F (C)) \underset{˙}{\times} (F (B) \cdot_{S} F (C)) = F (A) \underset{˙}{\times} F (B)$
25	14 24	eqtr2d	$⊢ (F \in (R RingHom S) \land (A \in X \land B \in X \land C \in X) \land (F (B) \in U \land F (C) \in U)) \to F (A) \underset{˙}{\times} F (B) = F (A \underset{˙}{\cdot} C) \underset{˙}{\times} F (B \underset{˙}{\cdot} C)$

Metamath Proof Explorer

Theorem rhmdvd

Proof