qqhval2lem

	Ref	Expression
Hypotheses	qqhval2.0	$⊢ B = {Base}_{R}$
	qqhval2.1	$⊢ \underset{˙}{\times} = /_{r} (R)$
	qqhval2.2	$⊢ L = ℤRHom (R)$
Assertion	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)$

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		drngring	$⊢ R \in DivRing \to R \in Ring$
5	3	zrhrhm	$⊢ R \in Ring \to L \in (ℤ_{ring} RingHom R)$
6	4 5	syl	$⊢ R \in DivRing \to L \in (ℤ_{ring} RingHom R)$
7	6	ad2antrr	$⊢ ((R \in DivRing \land chr (R) = 0) \land (X \in ℤ \land Y \in ℤ \land Y \neq 0)) \to L \in (ℤ_{ring} RingHom R)$
8		simpr1	$⊢ ((R \in DivRing \land chr (R) = 0) \land (X \in ℤ \land Y \in ℤ \land Y \neq 0)) \to X \in ℤ$
9		simpr2	$⊢ ((R \in DivRing \land chr (R) = 0) \land (X \in ℤ \land Y \in ℤ \land Y \neq 0)) \to Y \in ℤ$
10	8 9	gcdcld	$⊢ ((R \in DivRing \land chr (R) = 0) \land (X \in ℤ \land Y \in ℤ \land Y \neq 0)) \to X \gcd Y \in ℕ_{0}$
11	10	nn0zd	$⊢ ((R \in DivRing \land chr (R) = 0) \land (X \in ℤ \land Y \in ℤ \land Y \neq 0)) \to X \gcd Y \in ℤ$
12		simpr3	$⊢ ((R \in DivRing \land chr (R) = 0) \land (X \in ℤ \land Y \in ℤ \land Y \neq 0)) \to Y \neq 0$
13		gcdeq0	$⊢ (X \in ℤ \land Y \in ℤ) \to (X \gcd Y = 0 \leftrightarrow (X = 0 \land Y = 0))$
14	13	simplbda	$⊢ ((X \in ℤ \land Y \in ℤ) \land X \gcd Y = 0) \to Y = 0$
15	14	ex	$⊢ (X \in ℤ \land Y \in ℤ) \to (X \gcd Y = 0 \to Y = 0)$
16	15	necon3d	$⊢ (X \in ℤ \land Y \in ℤ) \to (Y \neq 0 \to X \gcd Y \neq 0)$
17	16	imp	$⊢ ((X \in ℤ \land Y \in ℤ) \land Y \neq 0) \to X \gcd Y \neq 0$
18	8 9 12 17	syl21anc	$⊢ ((R \in DivRing \land chr (R) = 0) \land (X \in ℤ \land Y \in ℤ \land Y \neq 0)) \to X \gcd Y \neq 0$
19		gcddvds	$⊢ (X \in ℤ \land Y \in ℤ) \to ((X \gcd Y) ∥ X \land (X \gcd Y) ∥ Y)$
20	8 9 19	syl2anc	$⊢ ((R \in DivRing \land chr (R) = 0) \land (X \in ℤ \land Y \in ℤ \land Y \neq 0)) \to ((X \gcd Y) ∥ X \land (X \gcd Y) ∥ Y)$
21	20	simpld	$⊢ ((R \in DivRing \land chr (R) = 0) \land (X \in ℤ \land Y \in ℤ \land Y \neq 0)) \to (X \gcd Y) ∥ X$
22		dvdsval2	$⊢ (X \gcd Y \in ℤ \land X \gcd Y \neq 0 \land X \in ℤ) \to ((X \gcd Y) ∥ X \leftrightarrow \frac{X}{X \gcd Y} \in ℤ)$
23	22	biimpa	$⊢ ((X \gcd Y \in ℤ \land X \gcd Y \neq 0 \land X \in ℤ) \land (X \gcd Y) ∥ X) \to \frac{X}{X \gcd Y} \in ℤ$
24	11 18 8 21 23	syl31anc	$⊢ ((R \in DivRing \land chr (R) = 0) \land (X \in ℤ \land Y \in ℤ \land Y \neq 0)) \to \frac{X}{X \gcd Y} \in ℤ$
25	20	simprd	$⊢ ((R \in DivRing \land chr (R) = 0) \land (X \in ℤ \land Y \in ℤ \land Y \neq 0)) \to (X \gcd Y) ∥ Y$
26		dvdsval2	$⊢ (X \gcd Y \in ℤ \land X \gcd Y \neq 0 \land Y \in ℤ) \to ((X \gcd Y) ∥ Y \leftrightarrow \frac{Y}{X \gcd Y} \in ℤ)$
27	26	biimpa	$⊢ ((X \gcd Y \in ℤ \land X \gcd Y \neq 0 \land Y \in ℤ) \land (X \gcd Y) ∥ Y) \to \frac{Y}{X \gcd Y} \in ℤ$
28	11 18 9 25 27	syl31anc	$⊢ ((R \in DivRing \land chr (R) = 0) \land (X \in ℤ \land Y \in ℤ \land Y \neq 0)) \to \frac{Y}{X \gcd Y} \in ℤ$
29		zringbas	$⊢ ℤ = {Base}_{ℤ_{ring}}$
30	29 1	rhmf	$⊢ L \in (ℤ_{ring} RingHom R) \to L : ℤ ⟶ B$
31	7 30	syl	$⊢ ((R \in DivRing \land chr (R) = 0) \land (X \in ℤ \land Y \in ℤ \land Y \neq 0)) \to L : ℤ ⟶ B$
32	31 28	ffvelrnd	$⊢ ((R \in DivRing \land chr (R) = 0) \land (X \in ℤ \land Y \in ℤ \land Y \neq 0)) \to L (\frac{Y}{X \gcd Y}) \in B$
33	31	ffnd	$⊢ ((R \in DivRing \land chr (R) = 0) \land (X \in ℤ \land Y \in ℤ \land Y \neq 0)) \to L Fn ℤ$
34	9	zcnd	$⊢ ((R \in DivRing \land chr (R) = 0) \land (X \in ℤ \land Y \in ℤ \land Y \neq 0)) \to Y \in ℂ$
35	11	zcnd	$⊢ ((R \in DivRing \land chr (R) = 0) \land (X \in ℤ \land Y \in ℤ \land Y \neq 0)) \to X \gcd Y \in ℂ$
36	34 35 12 18	divne0d	$⊢ ((R \in DivRing \land chr (R) = 0) \land (X \in ℤ \land Y \in ℤ \land Y \neq 0)) \to \frac{Y}{X \gcd Y} \neq 0$
37		ovex	$⊢ \frac{Y}{X \gcd Y} \in V$
38	37	elsn	$⊢ \frac{Y}{X \gcd Y} \in \{0\} \leftrightarrow \frac{Y}{X \gcd Y} = 0$
39	38	necon3bbii	$⊢ \neg \frac{Y}{X \gcd Y} \in \{0\} \leftrightarrow \frac{Y}{X \gcd Y} \neq 0$
40	36 39	sylibr	$⊢ ((R \in DivRing \land chr (R) = 0) \land (X \in ℤ \land Y \in ℤ \land Y \neq 0)) \to \neg \frac{Y}{X \gcd Y} \in \{0\}$
41	4	ad2antrr	$⊢ ((R \in DivRing \land chr (R) = 0) \land (X \in ℤ \land Y \in ℤ \land Y \neq 0)) \to R \in Ring$
42		simplr	$⊢ ((R \in DivRing \land chr (R) = 0) \land (X \in ℤ \land Y \in ℤ \land Y \neq 0)) \to chr (R) = 0$
43		eqid	$⊢ 0_{R} = 0_{R}$
44	1 3 43	zrhker	$⊢ R \in Ring \to (chr (R) = 0 \leftrightarrow L^{-1} [\{0_{R}\}] = \{0\})$
45	44	biimpa	$⊢ (R \in Ring \land chr (R) = 0) \to L^{-1} [\{0_{R}\}] = \{0\}$
46	41 42 45	syl2anc	$⊢ ((R \in DivRing \land chr (R) = 0) \land (X \in ℤ \land Y \in ℤ \land Y \neq 0)) \to L^{-1} [\{0_{R}\}] = \{0\}$
47	40 46	neleqtrrd	$⊢ ((R \in DivRing \land chr (R) = 0) \land (X \in ℤ \land Y \in ℤ \land Y \neq 0)) \to \neg \frac{Y}{X \gcd Y} \in L^{-1} [\{0_{R}\}]$
48		elpreima	$⊢ L Fn ℤ \to (\frac{Y}{X \gcd Y} \in L^{-1} [\{0_{R}\}] \leftrightarrow (\frac{Y}{X \gcd Y} \in ℤ \land L (\frac{Y}{X \gcd Y}) \in \{0_{R}\}))$
49	48	baibd	$⊢ (L Fn ℤ \land \frac{Y}{X \gcd Y} \in ℤ) \to (\frac{Y}{X \gcd Y} \in L^{-1} [\{0_{R}\}] \leftrightarrow L (\frac{Y}{X \gcd Y}) \in \{0_{R}\})$
50	49	biimprd	$⊢ (L Fn ℤ \land \frac{Y}{X \gcd Y} \in ℤ) \to (L (\frac{Y}{X \gcd Y}) \in \{0_{R}\} \to \frac{Y}{X \gcd Y} \in L^{-1} [\{0_{R}\}])$
51	50	con3dimp	$⊢ ((L Fn ℤ \land \frac{Y}{X \gcd Y} \in ℤ) \land \neg \frac{Y}{X \gcd Y} \in L^{-1} [\{0_{R}\}]) \to \neg L (\frac{Y}{X \gcd Y}) \in \{0_{R}\}$
52		fvex	$⊢ L (\frac{Y}{X \gcd Y}) \in V$
53	52	elsn	$⊢ L (\frac{Y}{X \gcd Y}) \in \{0_{R}\} \leftrightarrow L (\frac{Y}{X \gcd Y}) = 0_{R}$
54	53	necon3bbii	$⊢ \neg L (\frac{Y}{X \gcd Y}) \in \{0_{R}\} \leftrightarrow L (\frac{Y}{X \gcd Y}) \neq 0_{R}$
55	51 54	sylib	$⊢ ((L Fn ℤ \land \frac{Y}{X \gcd Y} \in ℤ) \land \neg \frac{Y}{X \gcd Y} \in L^{-1} [\{0_{R}\}]) \to L (\frac{Y}{X \gcd Y}) \neq 0_{R}$
56	33 28 47 55	syl21anc	$⊢ ((R \in DivRing \land chr (R) = 0) \land (X \in ℤ \land Y \in ℤ \land Y \neq 0)) \to L (\frac{Y}{X \gcd Y}) \neq 0_{R}$
57		eqid	$⊢ Unit (R) = Unit (R)$
58	1 57 43	drngunit	$⊢ R \in DivRing \to (L (\frac{Y}{X \gcd Y}) \in Unit (R) \leftrightarrow (L (\frac{Y}{X \gcd Y}) \in B \land L (\frac{Y}{X \gcd Y}) \neq 0_{R}))$
59	58	ad2antrr	$⊢ ((R \in DivRing \land chr (R) = 0) \land (X \in ℤ \land Y \in ℤ \land Y \neq 0)) \to (L (\frac{Y}{X \gcd Y}) \in Unit (R) \leftrightarrow (L (\frac{Y}{X \gcd Y}) \in B \land L (\frac{Y}{X \gcd Y}) \neq 0_{R}))$
60	32 56 59	mpbir2and	$⊢ ((R \in DivRing \land chr (R) = 0) \land (X \in ℤ \land Y \in ℤ \land Y \neq 0)) \to L (\frac{Y}{X \gcd Y}) \in Unit (R)$
61	31 11	ffvelrnd	$⊢ ((R \in DivRing \land chr (R) = 0) \land (X \in ℤ \land Y \in ℤ \land Y \neq 0)) \to L (X \gcd Y) \in B$
62		ovex	$⊢ X \gcd Y \in V$
63	62	elsn	$⊢ X \gcd Y \in \{0\} \leftrightarrow X \gcd Y = 0$
64	63	necon3bbii	$⊢ \neg X \gcd Y \in \{0\} \leftrightarrow X \gcd Y \neq 0$
65	18 64	sylibr	$⊢ ((R \in DivRing \land chr (R) = 0) \land (X \in ℤ \land Y \in ℤ \land Y \neq 0)) \to \neg X \gcd Y \in \{0\}$
66	65 46	neleqtrrd	$⊢ ((R \in DivRing \land chr (R) = 0) \land (X \in ℤ \land Y \in ℤ \land Y \neq 0)) \to \neg X \gcd Y \in L^{-1} [\{0_{R}\}]$
67		elpreima	$⊢ L Fn ℤ \to (X \gcd Y \in L^{-1} [\{0_{R}\}] \leftrightarrow (X \gcd Y \in ℤ \land L (X \gcd Y) \in \{0_{R}\}))$
68	67	baibd	$⊢ (L Fn ℤ \land X \gcd Y \in ℤ) \to (X \gcd Y \in L^{-1} [\{0_{R}\}] \leftrightarrow L (X \gcd Y) \in \{0_{R}\})$
69	68	biimprd	$⊢ (L Fn ℤ \land X \gcd Y \in ℤ) \to (L (X \gcd Y) \in \{0_{R}\} \to X \gcd Y \in L^{-1} [\{0_{R}\}])$
70	69	con3dimp	$⊢ ((L Fn ℤ \land X \gcd Y \in ℤ) \land \neg X \gcd Y \in L^{-1} [\{0_{R}\}]) \to \neg L (X \gcd Y) \in \{0_{R}\}$
71		fvex	$⊢ L (X \gcd Y) \in V$
72	71	elsn	$⊢ L (X \gcd Y) \in \{0_{R}\} \leftrightarrow L (X \gcd Y) = 0_{R}$
73	72	necon3bbii	$⊢ \neg L (X \gcd Y) \in \{0_{R}\} \leftrightarrow L (X \gcd Y) \neq 0_{R}$
74	70 73	sylib	$⊢ ((L Fn ℤ \land X \gcd Y \in ℤ) \land \neg X \gcd Y \in L^{-1} [\{0_{R}\}]) \to L (X \gcd Y) \neq 0_{R}$
75	33 11 66 74	syl21anc	$⊢ ((R \in DivRing \land chr (R) = 0) \land (X \in ℤ \land Y \in ℤ \land Y \neq 0)) \to L (X \gcd Y) \neq 0_{R}$
76	1 57 43	drngunit	$⊢ R \in DivRing \to (L (X \gcd Y) \in Unit (R) \leftrightarrow (L (X \gcd Y) \in B \land L (X \gcd Y) \neq 0_{R}))$
77	76	ad2antrr	$⊢ ((R \in DivRing \land chr (R) = 0) \land (X \in ℤ \land Y \in ℤ \land Y \neq 0)) \to (L (X \gcd Y) \in Unit (R) \leftrightarrow (L (X \gcd Y) \in B \land L (X \gcd Y) \neq 0_{R}))$
78	61 75 77	mpbir2and	$⊢ ((R \in DivRing \land chr (R) = 0) \land (X \in ℤ \land Y \in ℤ \land Y \neq 0)) \to L (X \gcd Y) \in Unit (R)$
79		zringmulr	$⊢ \times = \cdot_{ℤ_{ring}}$
80	57 29 2 79	rhmdvd	$⊢ (L \in (ℤ_{ring} RingHom R) \land (\frac{X}{X \gcd Y} \in ℤ \land \frac{Y}{X \gcd Y} \in ℤ \land X \gcd Y \in ℤ) \land (L (\frac{Y}{X \gcd Y}) \in Unit (R) \land L (X \gcd Y) \in Unit (R))) \to L (\frac{X}{X \gcd Y}) \underset{˙}{\times} L (\frac{Y}{X \gcd Y}) = L ((\frac{X}{X \gcd Y}) (X \gcd Y)) \underset{˙}{\times} L ((\frac{Y}{X \gcd Y}) (X \gcd Y))$
81	7 24 28 11 60 78 80	syl132anc	$⊢ ((R \in DivRing \land chr (R) = 0) \land (X \in ℤ \land Y \in ℤ \land Y \neq 0)) \to L (\frac{X}{X \gcd Y}) \underset{˙}{\times} L (\frac{Y}{X \gcd Y}) = L ((\frac{X}{X \gcd Y}) (X \gcd Y)) \underset{˙}{\times} L ((\frac{Y}{X \gcd Y}) (X \gcd Y))$
82		divnumden	$⊢ (X \in ℤ \land Y \in ℕ) \to (numer (\frac{X}{Y}) = \frac{X}{X \gcd Y} \land denom (\frac{X}{Y}) = \frac{Y}{X \gcd Y})$
83	8 82	sylan	$⊢ (((R \in DivRing \land chr (R) = 0) \land (X \in ℤ \land Y \in ℤ \land Y \neq 0)) \land Y \in ℕ) \to (numer (\frac{X}{Y}) = \frac{X}{X \gcd Y} \land denom (\frac{X}{Y}) = \frac{Y}{X \gcd Y})$
84	83	simpld	$⊢ (((R \in DivRing \land chr (R) = 0) \land (X \in ℤ \land Y \in ℤ \land Y \neq 0)) \land Y \in ℕ) \to numer (\frac{X}{Y}) = \frac{X}{X \gcd Y}$
85	84	eqcomd	$⊢ (((R \in DivRing \land chr (R) = 0) \land (X \in ℤ \land Y \in ℤ \land Y \neq 0)) \land Y \in ℕ) \to \frac{X}{X \gcd Y} = numer (\frac{X}{Y})$
86	85	fveq2d	$⊢ (((R \in DivRing \land chr (R) = 0) \land (X \in ℤ \land Y \in ℤ \land Y \neq 0)) \land Y \in ℕ) \to L (\frac{X}{X \gcd Y}) = L (numer (\frac{X}{Y}))$
87	83	simprd	$⊢ (((R \in DivRing \land chr (R) = 0) \land (X \in ℤ \land Y \in ℤ \land Y \neq 0)) \land Y \in ℕ) \to denom (\frac{X}{Y}) = \frac{Y}{X \gcd Y}$
88	87	eqcomd	$⊢ (((R \in DivRing \land chr (R) = 0) \land (X \in ℤ \land Y \in ℤ \land Y \neq 0)) \land Y \in ℕ) \to \frac{Y}{X \gcd Y} = denom (\frac{X}{Y})$
89	88	fveq2d	$⊢ (((R \in DivRing \land chr (R) = 0) \land (X \in ℤ \land Y \in ℤ \land Y \neq 0)) \land Y \in ℕ) \to L (\frac{Y}{X \gcd Y}) = L (denom (\frac{X}{Y}))$
90	86 89	oveq12d	$⊢ (((R \in DivRing \land chr (R) = 0) \land (X \in ℤ \land Y \in ℤ \land Y \neq 0)) \land Y \in ℕ) \to L (\frac{X}{X \gcd Y}) \underset{˙}{\times} L (\frac{Y}{X \gcd Y}) = L (numer (\frac{X}{Y})) \underset{˙}{\times} L (denom (\frac{X}{Y}))$
91	24	adantr	$⊢ (((R \in DivRing \land chr (R) = 0) \land (X \in ℤ \land Y \in ℤ \land Y \neq 0)) \land - Y \in ℕ) \to \frac{X}{X \gcd Y} \in ℤ$
92	91	zcnd	$⊢ (((R \in DivRing \land chr (R) = 0) \land (X \in ℤ \land Y \in ℤ \land Y \neq 0)) \land - Y \in ℕ) \to \frac{X}{X \gcd Y} \in ℂ$
93	92	mulm1d	$⊢ (((R \in DivRing \land chr (R) = 0) \land (X \in ℤ \land Y \in ℤ \land Y \neq 0)) \land - Y \in ℕ) \to -1 (\frac{X}{X \gcd Y}) = - \frac{X}{X \gcd Y}$
94		neg1cn	$⊢ - 1 \in ℂ$
95	94	a1i	$⊢ (((R \in DivRing \land chr (R) = 0) \land (X \in ℤ \land Y \in ℤ \land Y \neq 0)) \land - Y \in ℕ) \to - 1 \in ℂ$
96	95 92	mulcomd	$⊢ (((R \in DivRing \land chr (R) = 0) \land (X \in ℤ \land Y \in ℤ \land Y \neq 0)) \land - Y \in ℕ) \to -1 (\frac{X}{X \gcd Y}) = (\frac{X}{X \gcd Y}) -1$
97	93 96	eqtr3d	$⊢ (((R \in DivRing \land chr (R) = 0) \land (X \in ℤ \land Y \in ℤ \land Y \neq 0)) \land - Y \in ℕ) \to - \frac{X}{X \gcd Y} = (\frac{X}{X \gcd Y}) -1$
98	97	fveq2d	$⊢ (((R \in DivRing \land chr (R) = 0) \land (X \in ℤ \land Y \in ℤ \land Y \neq 0)) \land - Y \in ℕ) \to L (- \frac{X}{X \gcd Y}) = L ((\frac{X}{X \gcd Y}) -1)$
99	28	adantr	$⊢ (((R \in DivRing \land chr (R) = 0) \land (X \in ℤ \land Y \in ℤ \land Y \neq 0)) \land - Y \in ℕ) \to \frac{Y}{X \gcd Y} \in ℤ$
100	99	zcnd	$⊢ (((R \in DivRing \land chr (R) = 0) \land (X \in ℤ \land Y \in ℤ \land Y \neq 0)) \land - Y \in ℕ) \to \frac{Y}{X \gcd Y} \in ℂ$
101	100	mulm1d	$⊢ (((R \in DivRing \land chr (R) = 0) \land (X \in ℤ \land Y \in ℤ \land Y \neq 0)) \land - Y \in ℕ) \to -1 (\frac{Y}{X \gcd Y}) = - \frac{Y}{X \gcd Y}$
102	95 100	mulcomd	$⊢ (((R \in DivRing \land chr (R) = 0) \land (X \in ℤ \land Y \in ℤ \land Y \neq 0)) \land - Y \in ℕ) \to -1 (\frac{Y}{X \gcd Y}) = (\frac{Y}{X \gcd Y}) -1$
103	101 102	eqtr3d	$⊢ (((R \in DivRing \land chr (R) = 0) \land (X \in ℤ \land Y \in ℤ \land Y \neq 0)) \land - Y \in ℕ) \to - \frac{Y}{X \gcd Y} = (\frac{Y}{X \gcd Y}) -1$
104	103	fveq2d	$⊢ (((R \in DivRing \land chr (R) = 0) \land (X \in ℤ \land Y \in ℤ \land Y \neq 0)) \land - Y \in ℕ) \to L (- \frac{Y}{X \gcd Y}) = L ((\frac{Y}{X \gcd Y}) -1)$
105	98 104	oveq12d	$⊢ (((R \in DivRing \land chr (R) = 0) \land (X \in ℤ \land Y \in ℤ \land Y \neq 0)) \land - Y \in ℕ) \to L (- \frac{X}{X \gcd Y}) \underset{˙}{\times} L (- \frac{Y}{X \gcd Y}) = L ((\frac{X}{X \gcd Y}) -1) \underset{˙}{\times} L ((\frac{Y}{X \gcd Y}) -1)$
106	8	adantr	$⊢ (((R \in DivRing \land chr (R) = 0) \land (X \in ℤ \land Y \in ℤ \land Y \neq 0)) \land - Y \in ℕ) \to X \in ℤ$
107	9	adantr	$⊢ (((R \in DivRing \land chr (R) = 0) \land (X \in ℤ \land Y \in ℤ \land Y \neq 0)) \land - Y \in ℕ) \to Y \in ℤ$
108		simpr	$⊢ (((R \in DivRing \land chr (R) = 0) \land (X \in ℤ \land Y \in ℤ \land Y \neq 0)) \land - Y \in ℕ) \to - Y \in ℕ$
109		divnumden2	$⊢ (X \in ℤ \land Y \in ℤ \land - Y \in ℕ) \to (numer (\frac{X}{Y}) = - \frac{X}{X \gcd Y} \land denom (\frac{X}{Y}) = - \frac{Y}{X \gcd Y})$
110	106 107 108 109	syl3anc	$⊢ (((R \in DivRing \land chr (R) = 0) \land (X \in ℤ \land Y \in ℤ \land Y \neq 0)) \land - Y \in ℕ) \to (numer (\frac{X}{Y}) = - \frac{X}{X \gcd Y} \land denom (\frac{X}{Y}) = - \frac{Y}{X \gcd Y})$
111	110	simpld	$⊢ (((R \in DivRing \land chr (R) = 0) \land (X \in ℤ \land Y \in ℤ \land Y \neq 0)) \land - Y \in ℕ) \to numer (\frac{X}{Y}) = - \frac{X}{X \gcd Y}$
112	111	fveq2d	$⊢ (((R \in DivRing \land chr (R) = 0) \land (X \in ℤ \land Y \in ℤ \land Y \neq 0)) \land - Y \in ℕ) \to L (numer (\frac{X}{Y})) = L (- \frac{X}{X \gcd Y})$
113	110	simprd	$⊢ (((R \in DivRing \land chr (R) = 0) \land (X \in ℤ \land Y \in ℤ \land Y \neq 0)) \land - Y \in ℕ) \to denom (\frac{X}{Y}) = - \frac{Y}{X \gcd Y}$
114	113	fveq2d	$⊢ (((R \in DivRing \land chr (R) = 0) \land (X \in ℤ \land Y \in ℤ \land Y \neq 0)) \land - Y \in ℕ) \to L (denom (\frac{X}{Y})) = L (- \frac{Y}{X \gcd Y})$
115	112 114	oveq12d	$⊢ (((R \in DivRing \land chr (R) = 0) \land (X \in ℤ \land Y \in ℤ \land Y \neq 0)) \land - Y \in ℕ) \to L (numer (\frac{X}{Y})) \underset{˙}{\times} L (denom (\frac{X}{Y})) = L (- \frac{X}{X \gcd Y}) \underset{˙}{\times} L (- \frac{Y}{X \gcd Y})$
116	7	adantr	$⊢ (((R \in DivRing \land chr (R) = 0) \land (X \in ℤ \land Y \in ℤ \land Y \neq 0)) \land - Y \in ℕ) \to L \in (ℤ_{ring} RingHom R)$
117		1zzd	$⊢ (((R \in DivRing \land chr (R) = 0) \land (X \in ℤ \land Y \in ℤ \land Y \neq 0)) \land - Y \in ℕ) \to 1 \in ℤ$
118	117	znegcld	$⊢ (((R \in DivRing \land chr (R) = 0) \land (X \in ℤ \land Y \in ℤ \land Y \neq 0)) \land - Y \in ℕ) \to - 1 \in ℤ$
119	60	adantr	$⊢ (((R \in DivRing \land chr (R) = 0) \land (X \in ℤ \land Y \in ℤ \land Y \neq 0)) \land - Y \in ℕ) \to L (\frac{Y}{X \gcd Y}) \in Unit (R)$
120		neg1z	$⊢ - 1 \in ℤ$
121		ax-1cn	$⊢ 1 \in ℂ$
122	121	absnegi	$⊢ \|- 1\| = \|1\|$
123		abs1	$⊢ \|1\| = 1$
124	122 123	eqtri	$⊢ \|- 1\| = 1$
125		zringunit	$⊢ - 1 \in Unit (ℤ_{ring}) \leftrightarrow (- 1 \in ℤ \land \|- 1\| = 1)$
126	120 124 125	mpbir2an	$⊢ - 1 \in Unit (ℤ_{ring})$
127	126	a1i	$⊢ (((R \in DivRing \land chr (R) = 0) \land (X \in ℤ \land Y \in ℤ \land Y \neq 0)) \land - Y \in ℕ) \to - 1 \in Unit (ℤ_{ring})$
128		elrhmunit	$⊢ (L \in (ℤ_{ring} RingHom R) \land - 1 \in Unit (ℤ_{ring})) \to L (- 1) \in Unit (R)$
129	116 127 128	syl2anc	$⊢ (((R \in DivRing \land chr (R) = 0) \land (X \in ℤ \land Y \in ℤ \land Y \neq 0)) \land - Y \in ℕ) \to L (- 1) \in Unit (R)$
130	57 29 2 79	rhmdvd	$⊢ (L \in (ℤ_{ring} RingHom R) \land (\frac{X}{X \gcd Y} \in ℤ \land \frac{Y}{X \gcd Y} \in ℤ \land - 1 \in ℤ) \land (L (\frac{Y}{X \gcd Y}) \in Unit (R) \land L (- 1) \in Unit (R))) \to L (\frac{X}{X \gcd Y}) \underset{˙}{\times} L (\frac{Y}{X \gcd Y}) = L ((\frac{X}{X \gcd Y}) -1) \underset{˙}{\times} L ((\frac{Y}{X \gcd Y}) -1)$
131	116 91 99 118 119 129 130	syl132anc	$⊢ (((R \in DivRing \land chr (R) = 0) \land (X \in ℤ \land Y \in ℤ \land Y \neq 0)) \land - Y \in ℕ) \to L (\frac{X}{X \gcd Y}) \underset{˙}{\times} L (\frac{Y}{X \gcd Y}) = L ((\frac{X}{X \gcd Y}) -1) \underset{˙}{\times} L ((\frac{Y}{X \gcd Y}) -1)$
132	105 115 131	3eqtr4rd	$⊢ (((R \in DivRing \land chr (R) = 0) \land (X \in ℤ \land Y \in ℤ \land Y \neq 0)) \land - Y \in ℕ) \to L (\frac{X}{X \gcd Y}) \underset{˙}{\times} L (\frac{Y}{X \gcd Y}) = L (numer (\frac{X}{Y})) \underset{˙}{\times} L (denom (\frac{X}{Y}))$
133		simp3	$⊢ (X \in ℤ \land Y \in ℤ \land Y \neq 0) \to Y \neq 0$
134	133	neneqd	$⊢ (X \in ℤ \land Y \in ℤ \land Y \neq 0) \to \neg Y = 0$
135		simp2	$⊢ (X \in ℤ \land Y \in ℤ \land Y \neq 0) \to Y \in ℤ$
136		elz	$⊢ Y \in ℤ \leftrightarrow (Y \in ℝ \land (Y = 0 \lor Y \in ℕ \lor - Y \in ℕ))$
137	135 136	sylib	$⊢ (X \in ℤ \land Y \in ℤ \land Y \neq 0) \to (Y \in ℝ \land (Y = 0 \lor Y \in ℕ \lor - Y \in ℕ))$
138	137	simprd	$⊢ (X \in ℤ \land Y \in ℤ \land Y \neq 0) \to (Y = 0 \lor Y \in ℕ \lor - Y \in ℕ)$
139		3orass	$⊢ (Y = 0 \lor Y \in ℕ \lor - Y \in ℕ) \leftrightarrow (Y = 0 \lor (Y \in ℕ \lor - Y \in ℕ))$
140	138 139	sylib	$⊢ (X \in ℤ \land Y \in ℤ \land Y \neq 0) \to (Y = 0 \lor (Y \in ℕ \lor - Y \in ℕ))$
141		orel1	$⊢ \neg Y = 0 \to ((Y = 0 \lor (Y \in ℕ \lor - Y \in ℕ)) \to (Y \in ℕ \lor - Y \in ℕ))$
142	134 140 141	sylc	$⊢ (X \in ℤ \land Y \in ℤ \land Y \neq 0) \to (Y \in ℕ \lor - Y \in ℕ)$
143	142	adantl	$⊢ ((R \in DivRing \land chr (R) = 0) \land (X \in ℤ \land Y \in ℤ \land Y \neq 0)) \to (Y \in ℕ \lor - Y \in ℕ)$
144	90 132 143	mpjaodan	$⊢ ((R \in DivRing \land chr (R) = 0) \land (X \in ℤ \land Y \in ℤ \land Y \neq 0)) \to L (\frac{X}{X \gcd Y}) \underset{˙}{\times} L (\frac{Y}{X \gcd Y}) = L (numer (\frac{X}{Y})) \underset{˙}{\times} L (denom (\frac{X}{Y}))$
145	8	zcnd	$⊢ ((R \in DivRing \land chr (R) = 0) \land (X \in ℤ \land Y \in ℤ \land Y \neq 0)) \to X \in ℂ$
146	145 35 18	divcan1d	$⊢ ((R \in DivRing \land chr (R) = 0) \land (X \in ℤ \land Y \in ℤ \land Y \neq 0)) \to (\frac{X}{X \gcd Y}) (X \gcd Y) = X$
147	146	fveq2d	$⊢ ((R \in DivRing \land chr (R) = 0) \land (X \in ℤ \land Y \in ℤ \land Y \neq 0)) \to L ((\frac{X}{X \gcd Y}) (X \gcd Y)) = L (X)$
148	34 35 18	divcan1d	$⊢ ((R \in DivRing \land chr (R) = 0) \land (X \in ℤ \land Y \in ℤ \land Y \neq 0)) \to (\frac{Y}{X \gcd Y}) (X \gcd Y) = Y$
149	148	fveq2d	$⊢ ((R \in DivRing \land chr (R) = 0) \land (X \in ℤ \land Y \in ℤ \land Y \neq 0)) \to L ((\frac{Y}{X \gcd Y}) (X \gcd Y)) = L (Y)$
150	147 149	oveq12d	$⊢ ((R \in DivRing \land chr (R) = 0) \land (X \in ℤ \land Y \in ℤ \land Y \neq 0)) \to L ((\frac{X}{X \gcd Y}) (X \gcd Y)) \underset{˙}{\times} L ((\frac{Y}{X \gcd Y}) (X \gcd Y)) = L (X) \underset{˙}{\times} L (Y)$
151	81 144 150	3eqtr3d	$⊢ ((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)$

Metamath Proof Explorer

Theorem qqhval2lem

Proof