Metamath Proof Explorer

Theorem qqhvq

Description: The image of a quotient by the QQHom homomorphism. (Contributed by Thierry Arnoux, 28-Oct-2017)

		Ref	Expression
	Hypotheses	qqhval2.0	$⊢ B = {Base}_{R}$
		qqhval2.1	$⊢ \underset{˙}{\times} = /_{r} (R)$
		qqhval2.2	$⊢ L = ℤRHom (R)$
	Assertion	qqhvq	$⊢ ((R \in DivRing \land chr (R) = 0) \land (X \in ℤ \land Y \in ℤ \land Y \neq 0)) \to ℚHom (R) (\frac{X}{Y}) = L (X) \underset{˙}{\times} L (Y)$

Proof

Step	Hyp	Ref	Expression
1		qqhval2.0	$⊢ B = {Base}_{R}$
2		qqhval2.1	$⊢ \underset{˙}{\times} = /_{r} (R)$
3		qqhval2.2	$⊢ L = ℤRHom (R)$
4		zssq	$⊢ ℤ \subseteq ℚ$
5		simpr1	$⊢ ((R \in DivRing \land chr (R) = 0) \land (X \in ℤ \land Y \in ℤ \land Y \neq 0)) \to X \in ℤ$
6	4 5	sseldi	$⊢ ((R \in DivRing \land chr (R) = 0) \land (X \in ℤ \land Y \in ℤ \land Y \neq 0)) \to X \in ℚ$
7		simpr2	$⊢ ((R \in DivRing \land chr (R) = 0) \land (X \in ℤ \land Y \in ℤ \land Y \neq 0)) \to Y \in ℤ$
8	4 7	sseldi	$⊢ ((R \in DivRing \land chr (R) = 0) \land (X \in ℤ \land Y \in ℤ \land Y \neq 0)) \to Y \in ℚ$
9		simpr3	$⊢ ((R \in DivRing \land chr (R) = 0) \land (X \in ℤ \land Y \in ℤ \land Y \neq 0)) \to Y \neq 0$
10		qdivcl	$⊢ (X \in ℚ \land Y \in ℚ \land Y \neq 0) \to \frac{X}{Y} \in ℚ$
11	6 8 9 10	syl3anc	$⊢ ((R \in DivRing \land chr (R) = 0) \land (X \in ℤ \land Y \in ℤ \land Y \neq 0)) \to \frac{X}{Y} \in ℚ$
12	1 2 3	qqhvval	$⊢ ((R \in DivRing \land chr (R) = 0) \land \frac{X}{Y} \in ℚ) \to ℚHom (R) (\frac{X}{Y}) = L (numer (\frac{X}{Y})) \underset{˙}{\times} L (denom (\frac{X}{Y}))$
13	11 12	syldan	$⊢ ((R \in DivRing \land chr (R) = 0) \land (X \in ℤ \land Y \in ℤ \land Y \neq 0)) \to ℚHom (R) (\frac{X}{Y}) = L (numer (\frac{X}{Y})) \underset{˙}{\times} L (denom (\frac{X}{Y}))$
14	1 2 3	qqhval2lem	$⊢ ((R \in DivRing \land chr (R) = 0) \land (X \in ℤ \land Y \in ℤ \land Y \neq 0)) \to L (numer (\frac{X}{Y})) \underset{˙}{\times} L (denom (\frac{X}{Y})) = L (X) \underset{˙}{\times} L (Y)$
15	13 14	eqtrd	$⊢ ((R \in DivRing \land chr (R) = 0) \land (X \in ℤ \land Y \in ℤ \land Y \neq 0)) \to ℚHom (R) (\frac{X}{Y}) = L (X) \underset{˙}{\times} L (Y)$