Theorem qqh0

Description: The image of 0 by the QQHom homomorphism is the ring's zero. (Contributed by Thierry Arnoux, 22-Oct-2017)

	Ref	Expression
Hypotheses	qqhval2.0	⊢ 𝐵 = ( Base ‘ 𝑅 )
	qqhval2.1	⊢ / = ( /r ‘ 𝑅 )
	qqhval2.2	⊢ 𝐿 = ( ℤRHom ‘ 𝑅 )
Assertion	qqh0	⊢ ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) → ( ( ℚHom ‘ 𝑅 ) ‘ 0 ) = ( 0g ‘ 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		qqhval2.0	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		qqhval2.1	⊢ / = ( /r ‘ 𝑅 )
3		qqhval2.2	⊢ 𝐿 = ( ℤRHom ‘ 𝑅 )
4		zssq	⊢ ℤ ⊆ ℚ
5		0z	⊢ 0 ∈ ℤ
6	4 5	sselii	⊢ 0 ∈ ℚ
7	1 2 3	qqhvval	⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ 0 ∈ ℚ ) → ( ( ℚHom ‘ 𝑅 ) ‘ 0 ) = ( ( 𝐿 ‘ ( numer ‘ 0 ) ) / ( 𝐿 ‘ ( denom ‘ 0 ) ) ) )
8	6 7	mpan2	⊢ ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) → ( ( ℚHom ‘ 𝑅 ) ‘ 0 ) = ( ( 𝐿 ‘ ( numer ‘ 0 ) ) / ( 𝐿 ‘ ( denom ‘ 0 ) ) ) )
9		1z	⊢ 1 ∈ ℤ
10		gcd0id	⊢ ( 1 ∈ ℤ → ( 0 gcd 1 ) = ( abs ‘ 1 ) )
11	9 10	ax-mp	⊢ ( 0 gcd 1 ) = ( abs ‘ 1 )
12		abs1	⊢ ( abs ‘ 1 ) = 1
13	11 12	eqtri	⊢ ( 0 gcd 1 ) = 1
14		0cn	⊢ 0 ∈ ℂ
15	14	div1i	⊢ ( 0 / 1 ) = 0
16	15	eqcomi	⊢ 0 = ( 0 / 1 )
17	13 16	pm3.2i	⊢ ( ( 0 gcd 1 ) = 1 ∧ 0 = ( 0 / 1 ) )
18		1nn	⊢ 1 ∈ ℕ
19		qnumdenbi	⊢ ( ( 0 ∈ ℚ ∧ 0 ∈ ℤ ∧ 1 ∈ ℕ ) → ( ( ( 0 gcd 1 ) = 1 ∧ 0 = ( 0 / 1 ) ) ↔ ( ( numer ‘ 0 ) = 0 ∧ ( denom ‘ 0 ) = 1 ) ) )
20	6 5 18 19	mp3an	⊢ ( ( ( 0 gcd 1 ) = 1 ∧ 0 = ( 0 / 1 ) ) ↔ ( ( numer ‘ 0 ) = 0 ∧ ( denom ‘ 0 ) = 1 ) )
21	17 20	mpbi	⊢ ( ( numer ‘ 0 ) = 0 ∧ ( denom ‘ 0 ) = 1 )
22	21	simpli	⊢ ( numer ‘ 0 ) = 0
23	22	fveq2i	⊢ ( 𝐿 ‘ ( numer ‘ 0 ) ) = ( 𝐿 ‘ 0 )
24	21	simpri	⊢ ( denom ‘ 0 ) = 1
25	24	fveq2i	⊢ ( 𝐿 ‘ ( denom ‘ 0 ) ) = ( 𝐿 ‘ 1 )
26	23 25	oveq12i	⊢ ( ( 𝐿 ‘ ( numer ‘ 0 ) ) / ( 𝐿 ‘ ( denom ‘ 0 ) ) ) = ( ( 𝐿 ‘ 0 ) / ( 𝐿 ‘ 1 ) )
27		drngring	⊢ ( 𝑅 ∈ DivRing → 𝑅 ∈ Ring )
28		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
29	3 28	zrh0	⊢ ( 𝑅 ∈ Ring → ( 𝐿 ‘ 0 ) = ( 0g ‘ 𝑅 ) )
30		eqid	⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
31	3 30	zrh1	⊢ ( 𝑅 ∈ Ring → ( 𝐿 ‘ 1 ) = ( 1r ‘ 𝑅 ) )
32	29 31	oveq12d	⊢ ( 𝑅 ∈ Ring → ( ( 𝐿 ‘ 0 ) / ( 𝐿 ‘ 1 ) ) = ( ( 0g ‘ 𝑅 ) / ( 1r ‘ 𝑅 ) ) )
33	27 32	syl	⊢ ( 𝑅 ∈ DivRing → ( ( 𝐿 ‘ 0 ) / ( 𝐿 ‘ 1 ) ) = ( ( 0g ‘ 𝑅 ) / ( 1r ‘ 𝑅 ) ) )
34		drnggrp	⊢ ( 𝑅 ∈ DivRing → 𝑅 ∈ Grp )
35	1 28	grpidcl	⊢ ( 𝑅 ∈ Grp → ( 0g ‘ 𝑅 ) ∈ 𝐵 )
36	34 35	syl	⊢ ( 𝑅 ∈ DivRing → ( 0g ‘ 𝑅 ) ∈ 𝐵 )
37	1 2 30	dvr1	⊢ ( ( 𝑅 ∈ Ring ∧ ( 0g ‘ 𝑅 ) ∈ 𝐵 ) → ( ( 0g ‘ 𝑅 ) / ( 1r ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) )
38	27 36 37	syl2anc	⊢ ( 𝑅 ∈ DivRing → ( ( 0g ‘ 𝑅 ) / ( 1r ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) )
39	33 38	eqtrd	⊢ ( 𝑅 ∈ DivRing → ( ( 𝐿 ‘ 0 ) / ( 𝐿 ‘ 1 ) ) = ( 0g ‘ 𝑅 ) )
40	26 39	eqtrid	⊢ ( 𝑅 ∈ DivRing → ( ( 𝐿 ‘ ( numer ‘ 0 ) ) / ( 𝐿 ‘ ( denom ‘ 0 ) ) ) = ( 0g ‘ 𝑅 ) )
41	40	adantr	⊢ ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) → ( ( 𝐿 ‘ ( numer ‘ 0 ) ) / ( 𝐿 ‘ ( denom ‘ 0 ) ) ) = ( 0g ‘ 𝑅 ) )
42	8 41	eqtrd	⊢ ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) → ( ( ℚHom ‘ 𝑅 ) ‘ 0 ) = ( 0g ‘ 𝑅 ) )