qqhval2

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

	Ref	Expression
Hypotheses	qqhval2.0	$⊢ B = {Base}_{R}$
	qqhval2.1	$⊢ \underset{˙}{\times} = /_{r} (R)$
	qqhval2.2	$⊢ L = ℤRHom (R)$
Assertion	qqhval2	$⊢ (R \in DivRing \land chr (R) = 0) \to ℚHom (R) = (q \in ℚ ⟼ 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		elex	$⊢ R \in DivRing \to R \in V$
5	4	adantr	$⊢ (R \in DivRing \land chr (R) = 0) \to R \in V$
6		eqid	$⊢ 1_{R} = 1_{R}$
7	2 6 3	qqhval	$⊢ R \in V \to ℚHom (R) = ran (x \in ℤ, y \in L^{-1} [Unit (R)] ⟼ ⟨\frac{x}{y}, L (x) \underset{˙}{\times} L (y)⟩)$
8	5 7	syl	$⊢ (R \in DivRing \land chr (R) = 0) \to ℚHom (R) = ran (x \in ℤ, y \in L^{-1} [Unit (R)] ⟼ ⟨\frac{x}{y}, L (x) \underset{˙}{\times} L (y)⟩)$
9		eqidd	$⊢ (R \in DivRing \land chr (R) = 0) \to ℤ = ℤ$
10		eqid	$⊢ 0_{R} = 0_{R}$
11	1 3 10	zrhunitpreima	$⊢ (R \in DivRing \land chr (R) = 0) \to L^{-1} [Unit (R)] = ℤ ∖ \{0\}$
12		mpoeq12	$⊢ (ℤ = ℤ \land L^{-1} [Unit (R)] = ℤ ∖ \{0\}) \to (x \in ℤ, y \in L^{-1} [Unit (R)] ⟼ ⟨\frac{x}{y}, L (x) \underset{˙}{\times} L (y)⟩) = (x \in ℤ, y \in (ℤ ∖ \{0\}) ⟼ ⟨\frac{x}{y}, L (x) \underset{˙}{\times} L (y)⟩)$
13	9 11 12	syl2anc	$⊢ (R \in DivRing \land chr (R) = 0) \to (x \in ℤ, y \in L^{-1} [Unit (R)] ⟼ ⟨\frac{x}{y}, L (x) \underset{˙}{\times} L (y)⟩) = (x \in ℤ, y \in (ℤ ∖ \{0\}) ⟼ ⟨\frac{x}{y}, L (x) \underset{˙}{\times} L (y)⟩)$
14	13	rneqd	$⊢ (R \in DivRing \land chr (R) = 0) \to ran (x \in ℤ, y \in L^{-1} [Unit (R)] ⟼ ⟨\frac{x}{y}, L (x) \underset{˙}{\times} L (y)⟩) = ran (x \in ℤ, y \in (ℤ ∖ \{0\}) ⟼ ⟨\frac{x}{y}, L (x) \underset{˙}{\times} L (y)⟩)$
15		nfv	$⊢ Ⅎ e (R \in DivRing \land chr (R) = 0)$
16		nfab1	$⊢ \underline{Ⅎ} e \{e \| \exists x \in ℤ \exists y \in (ℤ ∖ \{0\}) e = ⟨\frac{x}{y}, L (x) \underset{˙}{\times} L (y)⟩\}$
17		nfcv	$⊢ \underline{Ⅎ} e \{⟨q, s⟩ \| (q \in ℚ \land s = L (numer (q)) \underset{˙}{\times} L (denom (q)))\}$
18		simpr	$⊢ (((R \in DivRing \land chr (R) = 0) \land (x \in ℤ \land y \in (ℤ ∖ \{0\}))) \land e = ⟨\frac{x}{y}, L (x) \underset{˙}{\times} L (y)⟩) \to e = ⟨\frac{x}{y}, L (x) \underset{˙}{\times} L (y)⟩$
19		zssq	$⊢ ℤ \subseteq ℚ$
20		simplrl	$⊢ (((R \in DivRing \land chr (R) = 0) \land (x \in ℤ \land y \in (ℤ ∖ \{0\}))) \land e = ⟨\frac{x}{y}, L (x) \underset{˙}{\times} L (y)⟩) \to x \in ℤ$
21	19 20	sselid	$⊢ (((R \in DivRing \land chr (R) = 0) \land (x \in ℤ \land y \in (ℤ ∖ \{0\}))) \land e = ⟨\frac{x}{y}, L (x) \underset{˙}{\times} L (y)⟩) \to x \in ℚ$
22		simplrr	$⊢ (((R \in DivRing \land chr (R) = 0) \land (x \in ℤ \land y \in (ℤ ∖ \{0\}))) \land e = ⟨\frac{x}{y}, L (x) \underset{˙}{\times} L (y)⟩) \to y \in (ℤ ∖ \{0\})$
23	22	eldifad	$⊢ (((R \in DivRing \land chr (R) = 0) \land (x \in ℤ \land y \in (ℤ ∖ \{0\}))) \land e = ⟨\frac{x}{y}, L (x) \underset{˙}{\times} L (y)⟩) \to y \in ℤ$
24	19 23	sselid	$⊢ (((R \in DivRing \land chr (R) = 0) \land (x \in ℤ \land y \in (ℤ ∖ \{0\}))) \land e = ⟨\frac{x}{y}, L (x) \underset{˙}{\times} L (y)⟩) \to y \in ℚ$
25	22	eldifbd	$⊢ (((R \in DivRing \land chr (R) = 0) \land (x \in ℤ \land y \in (ℤ ∖ \{0\}))) \land e = ⟨\frac{x}{y}, L (x) \underset{˙}{\times} L (y)⟩) \to \neg y \in \{0\}$
26		velsn	$⊢ y \in \{0\} \leftrightarrow y = 0$
27	26	necon3bbii	$⊢ \neg y \in \{0\} \leftrightarrow y \neq 0$
28	25 27	sylib	$⊢ (((R \in DivRing \land chr (R) = 0) \land (x \in ℤ \land y \in (ℤ ∖ \{0\}))) \land e = ⟨\frac{x}{y}, L (x) \underset{˙}{\times} L (y)⟩) \to y \neq 0$
29		qdivcl	$⊢ (x \in ℚ \land y \in ℚ \land y \neq 0) \to \frac{x}{y} \in ℚ$
30	21 24 28 29	syl3anc	$⊢ (((R \in DivRing \land chr (R) = 0) \land (x \in ℤ \land y \in (ℤ ∖ \{0\}))) \land e = ⟨\frac{x}{y}, L (x) \underset{˙}{\times} L (y)⟩) \to \frac{x}{y} \in ℚ$
31		simplll	$⊢ (((R \in DivRing \land chr (R) = 0) \land (x \in ℤ \land y \in (ℤ ∖ \{0\}))) \land e = ⟨\frac{x}{y}, L (x) \underset{˙}{\times} L (y)⟩) \to R \in DivRing$
32		simpllr	$⊢ (((R \in DivRing \land chr (R) = 0) \land (x \in ℤ \land y \in (ℤ ∖ \{0\}))) \land e = ⟨\frac{x}{y}, L (x) \underset{˙}{\times} L (y)⟩) \to chr (R) = 0$
33	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)$
34	33	eqcomd	$⊢ ((R \in DivRing \land chr (R) = 0) \land (x \in ℤ \land y \in ℤ \land y \neq 0)) \to L (x) \underset{˙}{\times} L (y) = L (numer (\frac{x}{y})) \underset{˙}{\times} L (denom (\frac{x}{y}))$
35	31 32 20 23 28 34	syl23anc	$⊢ (((R \in DivRing \land chr (R) = 0) \land (x \in ℤ \land y \in (ℤ ∖ \{0\}))) \land e = ⟨\frac{x}{y}, L (x) \underset{˙}{\times} L (y)⟩) \to L (x) \underset{˙}{\times} L (y) = L (numer (\frac{x}{y})) \underset{˙}{\times} L (denom (\frac{x}{y}))$
36		ovex	$⊢ \frac{x}{y} \in V$
37		ovex	$⊢ L (x) \underset{˙}{\times} L (y) \in V$
38		opeq12	$⊢ (q = \frac{x}{y} \land s = L (x) \underset{˙}{\times} L (y)) \to ⟨q, s⟩ = ⟨\frac{x}{y}, L (x) \underset{˙}{\times} L (y)⟩$
39	38	eqeq2d	$⊢ (q = \frac{x}{y} \land s = L (x) \underset{˙}{\times} L (y)) \to (e = ⟨q, s⟩ \leftrightarrow e = ⟨\frac{x}{y}, L (x) \underset{˙}{\times} L (y)⟩)$
40		simpl	$⊢ (q = \frac{x}{y} \land s = L (x) \underset{˙}{\times} L (y)) \to q = \frac{x}{y}$
41	40	eleq1d	$⊢ (q = \frac{x}{y} \land s = L (x) \underset{˙}{\times} L (y)) \to (q \in ℚ \leftrightarrow \frac{x}{y} \in ℚ)$
42		simpr	$⊢ (q = \frac{x}{y} \land s = L (x) \underset{˙}{\times} L (y)) \to s = L (x) \underset{˙}{\times} L (y)$
43	40	fveq2d	$⊢ (q = \frac{x}{y} \land s = L (x) \underset{˙}{\times} L (y)) \to numer (q) = numer (\frac{x}{y})$
44	43	fveq2d	$⊢ (q = \frac{x}{y} \land s = L (x) \underset{˙}{\times} L (y)) \to L (numer (q)) = L (numer (\frac{x}{y}))$
45	40	fveq2d	$⊢ (q = \frac{x}{y} \land s = L (x) \underset{˙}{\times} L (y)) \to denom (q) = denom (\frac{x}{y})$
46	45	fveq2d	$⊢ (q = \frac{x}{y} \land s = L (x) \underset{˙}{\times} L (y)) \to L (denom (q)) = L (denom (\frac{x}{y}))$
47	44 46	oveq12d	$⊢ (q = \frac{x}{y} \land s = L (x) \underset{˙}{\times} L (y)) \to L (numer (q)) \underset{˙}{\times} L (denom (q)) = L (numer (\frac{x}{y})) \underset{˙}{\times} L (denom (\frac{x}{y}))$
48	42 47	eqeq12d	$⊢ (q = \frac{x}{y} \land s = L (x) \underset{˙}{\times} L (y)) \to (s = L (numer (q)) \underset{˙}{\times} L (denom (q)) \leftrightarrow L (x) \underset{˙}{\times} L (y) = L (numer (\frac{x}{y})) \underset{˙}{\times} L (denom (\frac{x}{y})))$
49	41 48	anbi12d	$⊢ (q = \frac{x}{y} \land s = L (x) \underset{˙}{\times} L (y)) \to ((q \in ℚ \land s = L (numer (q)) \underset{˙}{\times} L (denom (q))) \leftrightarrow (\frac{x}{y} \in ℚ \land L (x) \underset{˙}{\times} L (y) = L (numer (\frac{x}{y})) \underset{˙}{\times} L (denom (\frac{x}{y}))))$
50	39 49	anbi12d	$⊢ (q = \frac{x}{y} \land s = L (x) \underset{˙}{\times} L (y)) \to ((e = ⟨q, s⟩ \land (q \in ℚ \land s = L (numer (q)) \underset{˙}{\times} L (denom (q)))) \leftrightarrow (e = ⟨\frac{x}{y}, L (x) \underset{˙}{\times} L (y)⟩ \land (\frac{x}{y} \in ℚ \land L (x) \underset{˙}{\times} L (y) = L (numer (\frac{x}{y})) \underset{˙}{\times} L (denom (\frac{x}{y})))))$
51	36 37 50	spc2ev	$⊢ (e = ⟨\frac{x}{y}, L (x) \underset{˙}{\times} L (y)⟩ \land (\frac{x}{y} \in ℚ \land L (x) \underset{˙}{\times} L (y) = L (numer (\frac{x}{y})) \underset{˙}{\times} L (denom (\frac{x}{y})))) \to \exists q \exists s (e = ⟨q, s⟩ \land (q \in ℚ \land s = L (numer (q)) \underset{˙}{\times} L (denom (q))))$
52	18 30 35 51	syl12anc	$⊢ (((R \in DivRing \land chr (R) = 0) \land (x \in ℤ \land y \in (ℤ ∖ \{0\}))) \land e = ⟨\frac{x}{y}, L (x) \underset{˙}{\times} L (y)⟩) \to \exists q \exists s (e = ⟨q, s⟩ \land (q \in ℚ \land s = L (numer (q)) \underset{˙}{\times} L (denom (q))))$
53	52	ex	$⊢ ((R \in DivRing \land chr (R) = 0) \land (x \in ℤ \land y \in (ℤ ∖ \{0\}))) \to (e = ⟨\frac{x}{y}, L (x) \underset{˙}{\times} L (y)⟩ \to \exists q \exists s (e = ⟨q, s⟩ \land (q \in ℚ \land s = L (numer (q)) \underset{˙}{\times} L (denom (q)))))$
54	53	rexlimdvva	$⊢ (R \in DivRing \land chr (R) = 0) \to (\exists x \in ℤ \exists y \in (ℤ ∖ \{0\}) e = ⟨\frac{x}{y}, L (x) \underset{˙}{\times} L (y)⟩ \to \exists q \exists s (e = ⟨q, s⟩ \land (q \in ℚ \land s = L (numer (q)) \underset{˙}{\times} L (denom (q)))))$
55	54	imp	$⊢ ((R \in DivRing \land chr (R) = 0) \land \exists x \in ℤ \exists y \in (ℤ ∖ \{0\}) e = ⟨\frac{x}{y}, L (x) \underset{˙}{\times} L (y)⟩) \to \exists q \exists s (e = ⟨q, s⟩ \land (q \in ℚ \land s = L (numer (q)) \underset{˙}{\times} L (denom (q))))$
56		19.42vv	$⊢ \exists q \exists s ((R \in DivRing \land chr (R) = 0) \land (e = ⟨q, s⟩ \land (q \in ℚ \land s = L (numer (q)) \underset{˙}{\times} L (denom (q))))) \leftrightarrow ((R \in DivRing \land chr (R) = 0) \land \exists q \exists s (e = ⟨q, s⟩ \land (q \in ℚ \land s = L (numer (q)) \underset{˙}{\times} L (denom (q)))))$
57		simprrl	$⊢ ((R \in DivRing \land chr (R) = 0) \land (e = ⟨q, s⟩ \land (q \in ℚ \land s = L (numer (q)) \underset{˙}{\times} L (denom (q))))) \to q \in ℚ$
58		qnumcl	$⊢ q \in ℚ \to numer (q) \in ℤ$
59	57 58	syl	$⊢ ((R \in DivRing \land chr (R) = 0) \land (e = ⟨q, s⟩ \land (q \in ℚ \land s = L (numer (q)) \underset{˙}{\times} L (denom (q))))) \to numer (q) \in ℤ$
60		qdencl	$⊢ q \in ℚ \to denom (q) \in ℕ$
61	57 60	syl	$⊢ ((R \in DivRing \land chr (R) = 0) \land (e = ⟨q, s⟩ \land (q \in ℚ \land s = L (numer (q)) \underset{˙}{\times} L (denom (q))))) \to denom (q) \in ℕ$
62	61	nnzd	$⊢ ((R \in DivRing \land chr (R) = 0) \land (e = ⟨q, s⟩ \land (q \in ℚ \land s = L (numer (q)) \underset{˙}{\times} L (denom (q))))) \to denom (q) \in ℤ$
63		nnne0	$⊢ denom (q) \in ℕ \to denom (q) \neq 0$
64		nelsn	$⊢ denom (q) \neq 0 \to \neg denom (q) \in \{0\}$
65	61 63 64	3syl	$⊢ ((R \in DivRing \land chr (R) = 0) \land (e = ⟨q, s⟩ \land (q \in ℚ \land s = L (numer (q)) \underset{˙}{\times} L (denom (q))))) \to \neg denom (q) \in \{0\}$
66	62 65	eldifd	$⊢ ((R \in DivRing \land chr (R) = 0) \land (e = ⟨q, s⟩ \land (q \in ℚ \land s = L (numer (q)) \underset{˙}{\times} L (denom (q))))) \to denom (q) \in (ℤ ∖ \{0\})$
67		simprl	$⊢ ((R \in DivRing \land chr (R) = 0) \land (e = ⟨q, s⟩ \land (q \in ℚ \land s = L (numer (q)) \underset{˙}{\times} L (denom (q))))) \to e = ⟨q, s⟩$
68		qeqnumdivden	$⊢ q \in ℚ \to q = \frac{numer (q)}{denom (q)}$
69	57 68	syl	$⊢ ((R \in DivRing \land chr (R) = 0) \land (e = ⟨q, s⟩ \land (q \in ℚ \land s = L (numer (q)) \underset{˙}{\times} L (denom (q))))) \to q = \frac{numer (q)}{denom (q)}$
70		simprrr	$⊢ ((R \in DivRing \land chr (R) = 0) \land (e = ⟨q, s⟩ \land (q \in ℚ \land s = L (numer (q)) \underset{˙}{\times} L (denom (q))))) \to s = L (numer (q)) \underset{˙}{\times} L (denom (q))$
71	69 70	opeq12d	$⊢ ((R \in DivRing \land chr (R) = 0) \land (e = ⟨q, s⟩ \land (q \in ℚ \land s = L (numer (q)) \underset{˙}{\times} L (denom (q))))) \to ⟨q, s⟩ = ⟨\frac{numer (q)}{denom (q)}, L (numer (q)) \underset{˙}{\times} L (denom (q))⟩$
72	67 71	eqtrd	$⊢ ((R \in DivRing \land chr (R) = 0) \land (e = ⟨q, s⟩ \land (q \in ℚ \land s = L (numer (q)) \underset{˙}{\times} L (denom (q))))) \to e = ⟨\frac{numer (q)}{denom (q)}, L (numer (q)) \underset{˙}{\times} L (denom (q))⟩$
73		oveq1	$⊢ x = numer (q) \to \frac{x}{y} = \frac{numer (q)}{y}$
74		fveq2	$⊢ x = numer (q) \to L (x) = L (numer (q))$
75	74	oveq1d	$⊢ x = numer (q) \to L (x) \underset{˙}{\times} L (y) = L (numer (q)) \underset{˙}{\times} L (y)$
76	73 75	opeq12d	$⊢ x = numer (q) \to ⟨\frac{x}{y}, L (x) \underset{˙}{\times} L (y)⟩ = ⟨\frac{numer (q)}{y}, L (numer (q)) \underset{˙}{\times} L (y)⟩$
77	76	eqeq2d	$⊢ x = numer (q) \to (e = ⟨\frac{x}{y}, L (x) \underset{˙}{\times} L (y)⟩ \leftrightarrow e = ⟨\frac{numer (q)}{y}, L (numer (q)) \underset{˙}{\times} L (y)⟩)$
78		oveq2	$⊢ y = denom (q) \to \frac{numer (q)}{y} = \frac{numer (q)}{denom (q)}$
79		fveq2	$⊢ y = denom (q) \to L (y) = L (denom (q))$
80	79	oveq2d	$⊢ y = denom (q) \to L (numer (q)) \underset{˙}{\times} L (y) = L (numer (q)) \underset{˙}{\times} L (denom (q))$
81	78 80	opeq12d	$⊢ y = denom (q) \to ⟨\frac{numer (q)}{y}, L (numer (q)) \underset{˙}{\times} L (y)⟩ = ⟨\frac{numer (q)}{denom (q)}, L (numer (q)) \underset{˙}{\times} L (denom (q))⟩$
82	81	eqeq2d	$⊢ y = denom (q) \to (e = ⟨\frac{numer (q)}{y}, L (numer (q)) \underset{˙}{\times} L (y)⟩ \leftrightarrow e = ⟨\frac{numer (q)}{denom (q)}, L (numer (q)) \underset{˙}{\times} L (denom (q))⟩)$
83	77 82	rspc2ev	$⊢ (numer (q) \in ℤ \land denom (q) \in (ℤ ∖ \{0\}) \land e = ⟨\frac{numer (q)}{denom (q)}, L (numer (q)) \underset{˙}{\times} L (denom (q))⟩) \to \exists x \in ℤ \exists y \in (ℤ ∖ \{0\}) e = ⟨\frac{x}{y}, L (x) \underset{˙}{\times} L (y)⟩$
84	59 66 72 83	syl3anc	$⊢ ((R \in DivRing \land chr (R) = 0) \land (e = ⟨q, s⟩ \land (q \in ℚ \land s = L (numer (q)) \underset{˙}{\times} L (denom (q))))) \to \exists x \in ℤ \exists y \in (ℤ ∖ \{0\}) e = ⟨\frac{x}{y}, L (x) \underset{˙}{\times} L (y)⟩$
85	84	exlimivv	$⊢ \exists q \exists s ((R \in DivRing \land chr (R) = 0) \land (e = ⟨q, s⟩ \land (q \in ℚ \land s = L (numer (q)) \underset{˙}{\times} L (denom (q))))) \to \exists x \in ℤ \exists y \in (ℤ ∖ \{0\}) e = ⟨\frac{x}{y}, L (x) \underset{˙}{\times} L (y)⟩$
86	56 85	sylbir	$⊢ ((R \in DivRing \land chr (R) = 0) \land \exists q \exists s (e = ⟨q, s⟩ \land (q \in ℚ \land s = L (numer (q)) \underset{˙}{\times} L (denom (q))))) \to \exists x \in ℤ \exists y \in (ℤ ∖ \{0\}) e = ⟨\frac{x}{y}, L (x) \underset{˙}{\times} L (y)⟩$
87	55 86	impbida	$⊢ (R \in DivRing \land chr (R) = 0) \to (\exists x \in ℤ \exists y \in (ℤ ∖ \{0\}) e = ⟨\frac{x}{y}, L (x) \underset{˙}{\times} L (y)⟩ \leftrightarrow \exists q \exists s (e = ⟨q, s⟩ \land (q \in ℚ \land s = L (numer (q)) \underset{˙}{\times} L (denom (q)))))$
88		abid	$⊢ e \in \{e \| \exists x \in ℤ \exists y \in (ℤ ∖ \{0\}) e = ⟨\frac{x}{y}, L (x) \underset{˙}{\times} L (y)⟩\} \leftrightarrow \exists x \in ℤ \exists y \in (ℤ ∖ \{0\}) e = ⟨\frac{x}{y}, L (x) \underset{˙}{\times} L (y)⟩$
89		elopab	$⊢ e \in \{⟨q, s⟩ \| (q \in ℚ \land s = L (numer (q)) \underset{˙}{\times} L (denom (q)))\} \leftrightarrow \exists q \exists s (e = ⟨q, s⟩ \land (q \in ℚ \land s = L (numer (q)) \underset{˙}{\times} L (denom (q))))$
90	87 88 89	3bitr4g	$⊢ (R \in DivRing \land chr (R) = 0) \to (e \in \{e \| \exists x \in ℤ \exists y \in (ℤ ∖ \{0\}) e = ⟨\frac{x}{y}, L (x) \underset{˙}{\times} L (y)⟩\} \leftrightarrow e \in \{⟨q, s⟩ \| (q \in ℚ \land s = L (numer (q)) \underset{˙}{\times} L (denom (q)))\})$
91	15 16 17 90	eqrd	$⊢ (R \in DivRing \land chr (R) = 0) \to \{e \| \exists x \in ℤ \exists y \in (ℤ ∖ \{0\}) e = ⟨\frac{x}{y}, L (x) \underset{˙}{\times} L (y)⟩\} = \{⟨q, s⟩ \| (q \in ℚ \land s = L (numer (q)) \underset{˙}{\times} L (denom (q)))\}$
92		eqid	$⊢ (x \in ℤ, y \in (ℤ ∖ \{0\}) ⟼ ⟨\frac{x}{y}, L (x) \underset{˙}{\times} L (y)⟩) = (x \in ℤ, y \in (ℤ ∖ \{0\}) ⟼ ⟨\frac{x}{y}, L (x) \underset{˙}{\times} L (y)⟩)$
93	92	rnmpo	$⊢ ran (x \in ℤ, y \in (ℤ ∖ \{0\}) ⟼ ⟨\frac{x}{y}, L (x) \underset{˙}{\times} L (y)⟩) = \{e \| \exists x \in ℤ \exists y \in (ℤ ∖ \{0\}) e = ⟨\frac{x}{y}, L (x) \underset{˙}{\times} L (y)⟩\}$
94		df-mpt	$⊢ (q \in ℚ ⟼ L (numer (q)) \underset{˙}{\times} L (denom (q))) = \{⟨q, s⟩ \| (q \in ℚ \land s = L (numer (q)) \underset{˙}{\times} L (denom (q)))\}$
95	91 93 94	3eqtr4g	$⊢ (R \in DivRing \land chr (R) = 0) \to ran (x \in ℤ, y \in (ℤ ∖ \{0\}) ⟼ ⟨\frac{x}{y}, L (x) \underset{˙}{\times} L (y)⟩) = (q \in ℚ ⟼ L (numer (q)) \underset{˙}{\times} L (denom (q)))$
96	8 14 95	3eqtrd	$⊢ (R \in DivRing \land chr (R) = 0) \to ℚHom (R) = (q \in ℚ ⟼ L (numer (q)) \underset{˙}{\times} L (denom (q)))$

Metamath Proof Explorer

Theorem qqhval2

Proof