Metamath Proof Explorer

Theorem qqhvval

Description: Value of the canonical homormorphism from the rational number when the target ring is a division ring. (Contributed by Thierry Arnoux, 30-Oct-2017)

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

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	1 2 3	qqhval2	$⊢ (R \in DivRing \land chr (R) = 0) \to ℚHom (R) = (q \in ℚ ⟼ L (numer (q)) \underset{˙}{\times} L (denom (q)))$
5	4	adantr	$⊢ ((R \in DivRing \land chr (R) = 0) \land Q \in ℚ) \to ℚHom (R) = (q \in ℚ ⟼ L (numer (q)) \underset{˙}{\times} L (denom (q)))$
6		simpr	$⊢ (((R \in DivRing \land chr (R) = 0) \land Q \in ℚ) \land q = Q) \to q = Q$
7	6	fveq2d	$⊢ (((R \in DivRing \land chr (R) = 0) \land Q \in ℚ) \land q = Q) \to numer (q) = numer (Q)$
8	7	fveq2d	$⊢ (((R \in DivRing \land chr (R) = 0) \land Q \in ℚ) \land q = Q) \to L (numer (q)) = L (numer (Q))$
9	6	fveq2d	$⊢ (((R \in DivRing \land chr (R) = 0) \land Q \in ℚ) \land q = Q) \to denom (q) = denom (Q)$
10	9	fveq2d	$⊢ (((R \in DivRing \land chr (R) = 0) \land Q \in ℚ) \land q = Q) \to L (denom (q)) = L (denom (Q))$
11	8 10	oveq12d	$⊢ (((R \in DivRing \land chr (R) = 0) \land Q \in ℚ) \land q = Q) \to L (numer (q)) \underset{˙}{\times} L (denom (q)) = L (numer (Q)) \underset{˙}{\times} L (denom (Q))$
12		simpr	$⊢ ((R \in DivRing \land chr (R) = 0) \land Q \in ℚ) \to Q \in ℚ$
13		ovexd	$⊢ ((R \in DivRing \land chr (R) = 0) \land Q \in ℚ) \to L (numer (Q)) \underset{˙}{\times} L (denom (Q)) \in V$
14	5 11 12 13	fvmptd	$⊢ ((R \in DivRing \land chr (R) = 0) \land Q \in ℚ) \to ℚHom (R) (Q) = L (numer (Q)) \underset{˙}{\times} L (denom (Q))$