Metamath Proof Explorer

Theorem 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 ⊢ 𝐵 = ( Base ‘ 𝑅 )
qqhval2.1 ⊢ / = ( /r ‘ 𝑅 )
qqhval2.2 ⊢ 𝐿 = ( ℤRHom ‘ 𝑅 )
Assertion qqhval2 ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) → ( ℚHom ‘ 𝑅 ) = ( 𝑞 ∈ ℚ ↦ ( ( 𝐿 ‘ ( numer ‘ 𝑞 ) ) / ( 𝐿 ‘ ( denom ‘ 𝑞 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 qqhval2.0 ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 qqhval2.1 ⊢ / = ( /r ‘ 𝑅 )
3 qqhval2.2 ⊢ 𝐿 = ( ℤRHom ‘ 𝑅 )
4 elex ⊢ ( 𝑅 ∈ DivRing → 𝑅 ∈ V )
5 4 adantr ⊢ ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) → 𝑅 ∈ V )
6 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
7 2 6 3 qqhval ⊢ ( 𝑅 ∈ V → ( ℚHom ‘ 𝑅 ) = ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ( ◡ 𝐿 “ ( Unit ‘ 𝑅 ) ) ↦ ⟨ ( 𝑥 / 𝑦 ) , ( ( 𝐿 ‘ 𝑥 ) / ( 𝐿 ‘ 𝑦 ) ) ⟩ ) )
8 5 7 syl ⊢ ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) → ( ℚHom ‘ 𝑅 ) = ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ( ◡ 𝐿 “ ( Unit ‘ 𝑅 ) ) ↦ ⟨ ( 𝑥 / 𝑦 ) , ( ( 𝐿 ‘ 𝑥 ) / ( 𝐿 ‘ 𝑦 ) ) ⟩ ) )
9 eqid ⊢ ℤ = ℤ
10 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
11 1 3 10 zrhunitpreima ⊢ ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) → ( ◡ 𝐿 “ ( Unit ‘ 𝑅 ) ) = ( ℤ ∖ { 0 } ) )
12 mpoeq12 ⊢ ( ( ℤ = ℤ ∧ ( ◡ 𝐿 “ ( Unit ‘ 𝑅 ) ) = ( ℤ ∖ { 0 } ) ) → ( 𝑥 ∈ ℤ , 𝑦 ∈ ( ◡ 𝐿 “ ( Unit ‘ 𝑅 ) ) ↦ ⟨ ( 𝑥 / 𝑦 ) , ( ( 𝐿 ‘ 𝑥 ) / ( 𝐿 ‘ 𝑦 ) ) ⟩ ) = ( 𝑥 ∈ ℤ , 𝑦 ∈ ( ℤ ∖ { 0 } ) ↦ ⟨ ( 𝑥 / 𝑦 ) , ( ( 𝐿 ‘ 𝑥 ) / ( 𝐿 ‘ 𝑦 ) ) ⟩ ) )
13 9 11 12 sylancr ⊢ ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) → ( 𝑥 ∈ ℤ , 𝑦 ∈ ( ◡ 𝐿 “ ( Unit ‘ 𝑅 ) ) ↦ ⟨ ( 𝑥 / 𝑦 ) , ( ( 𝐿 ‘ 𝑥 ) / ( 𝐿 ‘ 𝑦 ) ) ⟩ ) = ( 𝑥 ∈ ℤ , 𝑦 ∈ ( ℤ ∖ { 0 } ) ↦ ⟨ ( 𝑥 / 𝑦 ) , ( ( 𝐿 ‘ 𝑥 ) / ( 𝐿 ‘ 𝑦 ) ) ⟩ ) )
14 13 rneqd ⊢ ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) → ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ( ◡ 𝐿 “ ( Unit ‘ 𝑅 ) ) ↦ ⟨ ( 𝑥 / 𝑦 ) , ( ( 𝐿 ‘ 𝑥 ) / ( 𝐿 ‘ 𝑦 ) ) ⟩ ) = ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ( ℤ ∖ { 0 } ) ↦ ⟨ ( 𝑥 / 𝑦 ) , ( ( 𝐿 ‘ 𝑥 ) / ( 𝐿 ‘ 𝑦 ) ) ⟩ ) )
15 nfv ⊢ Ⅎ 𝑒 ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 )
16 nfab1 ⊢ Ⅎ 𝑒 { 𝑒 ∣ ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ( ℤ ∖ { 0 } ) 𝑒 = ⟨ ( 𝑥 / 𝑦 ) , ( ( 𝐿 ‘ 𝑥 ) / ( 𝐿 ‘ 𝑦 ) ) ⟩ }
17 nfcv ⊢ Ⅎ 𝑒 { ⟨ 𝑞 , 𝑠 ⟩ ∣ ( 𝑞 ∈ ℚ ∧ 𝑠 = ( ( 𝐿 ‘ ( numer ‘ 𝑞 ) ) / ( 𝐿 ‘ ( denom ‘ 𝑞 ) ) ) ) }
18 simpr ⊢ ( ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ( ℤ ∖ { 0 } ) ) ) ∧ 𝑒 = ⟨ ( 𝑥 / 𝑦 ) , ( ( 𝐿 ‘ 𝑥 ) / ( 𝐿 ‘ 𝑦 ) ) ⟩ ) → 𝑒 = ⟨ ( 𝑥 / 𝑦 ) , ( ( 𝐿 ‘ 𝑥 ) / ( 𝐿 ‘ 𝑦 ) ) ⟩ )
19 zssq ⊢ ℤ ⊆ ℚ
20 simplrl ⊢ ( ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ( ℤ ∖ { 0 } ) ) ) ∧ 𝑒 = ⟨ ( 𝑥 / 𝑦 ) , ( ( 𝐿 ‘ 𝑥 ) / ( 𝐿 ‘ 𝑦 ) ) ⟩ ) → 𝑥 ∈ ℤ )
21 19 20 sselid ⊢ ( ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ( ℤ ∖ { 0 } ) ) ) ∧ 𝑒 = ⟨ ( 𝑥 / 𝑦 ) , ( ( 𝐿 ‘ 𝑥 ) / ( 𝐿 ‘ 𝑦 ) ) ⟩ ) → 𝑥 ∈ ℚ )
22 simplrr ⊢ ( ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ( ℤ ∖ { 0 } ) ) ) ∧ 𝑒 = ⟨ ( 𝑥 / 𝑦 ) , ( ( 𝐿 ‘ 𝑥 ) / ( 𝐿 ‘ 𝑦 ) ) ⟩ ) → 𝑦 ∈ ( ℤ ∖ { 0 } ) )
23 22 eldifad ⊢ ( ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ( ℤ ∖ { 0 } ) ) ) ∧ 𝑒 = ⟨ ( 𝑥 / 𝑦 ) , ( ( 𝐿 ‘ 𝑥 ) / ( 𝐿 ‘ 𝑦 ) ) ⟩ ) → 𝑦 ∈ ℤ )
24 19 23 sselid ⊢ ( ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ( ℤ ∖ { 0 } ) ) ) ∧ 𝑒 = ⟨ ( 𝑥 / 𝑦 ) , ( ( 𝐿 ‘ 𝑥 ) / ( 𝐿 ‘ 𝑦 ) ) ⟩ ) → 𝑦 ∈ ℚ )
25 22 eldifbd ⊢ ( ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ( ℤ ∖ { 0 } ) ) ) ∧ 𝑒 = ⟨ ( 𝑥 / 𝑦 ) , ( ( 𝐿 ‘ 𝑥 ) / ( 𝐿 ‘ 𝑦 ) ) ⟩ ) → ¬ 𝑦 ∈ { 0 } )
26 velsn ⊢ ( 𝑦 ∈ { 0 } ↔ 𝑦 = 0 )
27 26 necon3bbii ⊢ ( ¬ 𝑦 ∈ { 0 } ↔ 𝑦 ≠ 0 )
28 25 27 sylib ⊢ ( ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ( ℤ ∖ { 0 } ) ) ) ∧ 𝑒 = ⟨ ( 𝑥 / 𝑦 ) , ( ( 𝐿 ‘ 𝑥 ) / ( 𝐿 ‘ 𝑦 ) ) ⟩ ) → 𝑦 ≠ 0 )
29 qdivcl ⊢ ( ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) → ( 𝑥 / 𝑦 ) ∈ ℚ )
30 21 24 28 29 syl3anc ⊢ ( ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ( ℤ ∖ { 0 } ) ) ) ∧ 𝑒 = ⟨ ( 𝑥 / 𝑦 ) , ( ( 𝐿 ‘ 𝑥 ) / ( 𝐿 ‘ 𝑦 ) ) ⟩ ) → ( 𝑥 / 𝑦 ) ∈ ℚ )
31 simplll ⊢ ( ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ( ℤ ∖ { 0 } ) ) ) ∧ 𝑒 = ⟨ ( 𝑥 / 𝑦 ) , ( ( 𝐿 ‘ 𝑥 ) / ( 𝐿 ‘ 𝑦 ) ) ⟩ ) → 𝑅 ∈ DivRing )
32 simpllr ⊢ ( ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ( ℤ ∖ { 0 } ) ) ) ∧ 𝑒 = ⟨ ( 𝑥 / 𝑦 ) , ( ( 𝐿 ‘ 𝑥 ) / ( 𝐿 ‘ 𝑦 ) ) ⟩ ) → ( chr ‘ 𝑅 ) = 0 )
33 1 2 3 qqhval2lem ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ∧ 𝑦 ≠ 0 ) ) → ( ( 𝐿 ‘ ( numer ‘ ( 𝑥 / 𝑦 ) ) ) / ( 𝐿 ‘ ( denom ‘ ( 𝑥 / 𝑦 ) ) ) ) = ( ( 𝐿 ‘ 𝑥 ) / ( 𝐿 ‘ 𝑦 ) ) )
34 33 eqcomd ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ∧ 𝑦 ≠ 0 ) ) → ( ( 𝐿 ‘ 𝑥 ) / ( 𝐿 ‘ 𝑦 ) ) = ( ( 𝐿 ‘ ( numer ‘ ( 𝑥 / 𝑦 ) ) ) / ( 𝐿 ‘ ( denom ‘ ( 𝑥 / 𝑦 ) ) ) ) )
35 31 32 20 23 28 34 syl23anc ⊢ ( ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ( ℤ ∖ { 0 } ) ) ) ∧ 𝑒 = ⟨ ( 𝑥 / 𝑦 ) , ( ( 𝐿 ‘ 𝑥 ) / ( 𝐿 ‘ 𝑦 ) ) ⟩ ) → ( ( 𝐿 ‘ 𝑥 ) / ( 𝐿 ‘ 𝑦 ) ) = ( ( 𝐿 ‘ ( numer ‘ ( 𝑥 / 𝑦 ) ) ) / ( 𝐿 ‘ ( denom ‘ ( 𝑥 / 𝑦 ) ) ) ) )
36 ovex ⊢ ( 𝑥 / 𝑦 ) ∈ V
37 ovex ⊢ ( ( 𝐿 ‘ 𝑥 ) / ( 𝐿 ‘ 𝑦 ) ) ∈ V
38 opeq12 ⊢ ( ( 𝑞 = ( 𝑥 / 𝑦 ) ∧ 𝑠 = ( ( 𝐿 ‘ 𝑥 ) / ( 𝐿 ‘ 𝑦 ) ) ) → ⟨ 𝑞 , 𝑠 ⟩ = ⟨ ( 𝑥 / 𝑦 ) , ( ( 𝐿 ‘ 𝑥 ) / ( 𝐿 ‘ 𝑦 ) ) ⟩ )
39 38 eqeq2d ⊢ ( ( 𝑞 = ( 𝑥 / 𝑦 ) ∧ 𝑠 = ( ( 𝐿 ‘ 𝑥 ) / ( 𝐿 ‘ 𝑦 ) ) ) → ( 𝑒 = ⟨ 𝑞 , 𝑠 ⟩ ↔ 𝑒 = ⟨ ( 𝑥 / 𝑦 ) , ( ( 𝐿 ‘ 𝑥 ) / ( 𝐿 ‘ 𝑦 ) ) ⟩ ) )
40 simpl ⊢ ( ( 𝑞 = ( 𝑥 / 𝑦 ) ∧ 𝑠 = ( ( 𝐿 ‘ 𝑥 ) / ( 𝐿 ‘ 𝑦 ) ) ) → 𝑞 = ( 𝑥 / 𝑦 ) )
41 40 eleq1d ⊢ ( ( 𝑞 = ( 𝑥 / 𝑦 ) ∧ 𝑠 = ( ( 𝐿 ‘ 𝑥 ) / ( 𝐿 ‘ 𝑦 ) ) ) → ( 𝑞 ∈ ℚ ↔ ( 𝑥 / 𝑦 ) ∈ ℚ ) )
42 simpr ⊢ ( ( 𝑞 = ( 𝑥 / 𝑦 ) ∧ 𝑠 = ( ( 𝐿 ‘ 𝑥 ) / ( 𝐿 ‘ 𝑦 ) ) ) → 𝑠 = ( ( 𝐿 ‘ 𝑥 ) / ( 𝐿 ‘ 𝑦 ) ) )
43 40 fveq2d ⊢ ( ( 𝑞 = ( 𝑥 / 𝑦 ) ∧ 𝑠 = ( ( 𝐿 ‘ 𝑥 ) / ( 𝐿 ‘ 𝑦 ) ) ) → ( numer ‘ 𝑞 ) = ( numer ‘ ( 𝑥 / 𝑦 ) ) )
44 43 fveq2d ⊢ ( ( 𝑞 = ( 𝑥 / 𝑦 ) ∧ 𝑠 = ( ( 𝐿 ‘ 𝑥 ) / ( 𝐿 ‘ 𝑦 ) ) ) → ( 𝐿 ‘ ( numer ‘ 𝑞 ) ) = ( 𝐿 ‘ ( numer ‘ ( 𝑥 / 𝑦 ) ) ) )
45 40 fveq2d ⊢ ( ( 𝑞 = ( 𝑥 / 𝑦 ) ∧ 𝑠 = ( ( 𝐿 ‘ 𝑥 ) / ( 𝐿 ‘ 𝑦 ) ) ) → ( denom ‘ 𝑞 ) = ( denom ‘ ( 𝑥 / 𝑦 ) ) )
46 45 fveq2d ⊢ ( ( 𝑞 = ( 𝑥 / 𝑦 ) ∧ 𝑠 = ( ( 𝐿 ‘ 𝑥 ) / ( 𝐿 ‘ 𝑦 ) ) ) → ( 𝐿 ‘ ( denom ‘ 𝑞 ) ) = ( 𝐿 ‘ ( denom ‘ ( 𝑥 / 𝑦 ) ) ) )
47 44 46 oveq12d ⊢ ( ( 𝑞 = ( 𝑥 / 𝑦 ) ∧ 𝑠 = ( ( 𝐿 ‘ 𝑥 ) / ( 𝐿 ‘ 𝑦 ) ) ) → ( ( 𝐿 ‘ ( numer ‘ 𝑞 ) ) / ( 𝐿 ‘ ( denom ‘ 𝑞 ) ) ) = ( ( 𝐿 ‘ ( numer ‘ ( 𝑥 / 𝑦 ) ) ) / ( 𝐿 ‘ ( denom ‘ ( 𝑥 / 𝑦 ) ) ) ) )
48 42 47 eqeq12d ⊢ ( ( 𝑞 = ( 𝑥 / 𝑦 ) ∧ 𝑠 = ( ( 𝐿 ‘ 𝑥 ) / ( 𝐿 ‘ 𝑦 ) ) ) → ( 𝑠 = ( ( 𝐿 ‘ ( numer ‘ 𝑞 ) ) / ( 𝐿 ‘ ( denom ‘ 𝑞 ) ) ) ↔ ( ( 𝐿 ‘ 𝑥 ) / ( 𝐿 ‘ 𝑦 ) ) = ( ( 𝐿 ‘ ( numer ‘ ( 𝑥 / 𝑦 ) ) ) / ( 𝐿 ‘ ( denom ‘ ( 𝑥 / 𝑦 ) ) ) ) ) )
49 41 48 anbi12d ⊢ ( ( 𝑞 = ( 𝑥 / 𝑦 ) ∧ 𝑠 = ( ( 𝐿 ‘ 𝑥 ) / ( 𝐿 ‘ 𝑦 ) ) ) → ( ( 𝑞 ∈ ℚ ∧ 𝑠 = ( ( 𝐿 ‘ ( numer ‘ 𝑞 ) ) / ( 𝐿 ‘ ( denom ‘ 𝑞 ) ) ) ) ↔ ( ( 𝑥 / 𝑦 ) ∈ ℚ ∧ ( ( 𝐿 ‘ 𝑥 ) / ( 𝐿 ‘ 𝑦 ) ) = ( ( 𝐿 ‘ ( numer ‘ ( 𝑥 / 𝑦 ) ) ) / ( 𝐿 ‘ ( denom ‘ ( 𝑥 / 𝑦 ) ) ) ) ) ) )
50 39 49 anbi12d ⊢ ( ( 𝑞 = ( 𝑥 / 𝑦 ) ∧ 𝑠 = ( ( 𝐿 ‘ 𝑥 ) / ( 𝐿 ‘ 𝑦 ) ) ) → ( ( 𝑒 = ⟨ 𝑞 , 𝑠 ⟩ ∧ ( 𝑞 ∈ ℚ ∧ 𝑠 = ( ( 𝐿 ‘ ( numer ‘ 𝑞 ) ) / ( 𝐿 ‘ ( denom ‘ 𝑞 ) ) ) ) ) ↔ ( 𝑒 = ⟨ ( 𝑥 / 𝑦 ) , ( ( 𝐿 ‘ 𝑥 ) / ( 𝐿 ‘ 𝑦 ) ) ⟩ ∧ ( ( 𝑥 / 𝑦 ) ∈ ℚ ∧ ( ( 𝐿 ‘ 𝑥 ) / ( 𝐿 ‘ 𝑦 ) ) = ( ( 𝐿 ‘ ( numer ‘ ( 𝑥 / 𝑦 ) ) ) / ( 𝐿 ‘ ( denom ‘ ( 𝑥 / 𝑦 ) ) ) ) ) ) ) )
51 36 37 50 spc2ev ⊢ ( ( 𝑒 = ⟨ ( 𝑥 / 𝑦 ) , ( ( 𝐿 ‘ 𝑥 ) / ( 𝐿 ‘ 𝑦 ) ) ⟩ ∧ ( ( 𝑥 / 𝑦 ) ∈ ℚ ∧ ( ( 𝐿 ‘ 𝑥 ) / ( 𝐿 ‘ 𝑦 ) ) = ( ( 𝐿 ‘ ( numer ‘ ( 𝑥 / 𝑦 ) ) ) / ( 𝐿 ‘ ( denom ‘ ( 𝑥 / 𝑦 ) ) ) ) ) ) → ∃ 𝑞 ∃ 𝑠 ( 𝑒 = ⟨ 𝑞 , 𝑠 ⟩ ∧ ( 𝑞 ∈ ℚ ∧ 𝑠 = ( ( 𝐿 ‘ ( numer ‘ 𝑞 ) ) / ( 𝐿 ‘ ( denom ‘ 𝑞 ) ) ) ) ) )
52 18 30 35 51 syl12anc ⊢ ( ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ( ℤ ∖ { 0 } ) ) ) ∧ 𝑒 = ⟨ ( 𝑥 / 𝑦 ) , ( ( 𝐿 ‘ 𝑥 ) / ( 𝐿 ‘ 𝑦 ) ) ⟩ ) → ∃ 𝑞 ∃ 𝑠 ( 𝑒 = ⟨ 𝑞 , 𝑠 ⟩ ∧ ( 𝑞 ∈ ℚ ∧ 𝑠 = ( ( 𝐿 ‘ ( numer ‘ 𝑞 ) ) / ( 𝐿 ‘ ( denom ‘ 𝑞 ) ) ) ) ) )
53 52 ex ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ( ℤ ∖ { 0 } ) ) ) → ( 𝑒 = ⟨ ( 𝑥 / 𝑦 ) , ( ( 𝐿 ‘ 𝑥 ) / ( 𝐿 ‘ 𝑦 ) ) ⟩ → ∃ 𝑞 ∃ 𝑠 ( 𝑒 = ⟨ 𝑞 , 𝑠 ⟩ ∧ ( 𝑞 ∈ ℚ ∧ 𝑠 = ( ( 𝐿 ‘ ( numer ‘ 𝑞 ) ) / ( 𝐿 ‘ ( denom ‘ 𝑞 ) ) ) ) ) ) )
54 53 rexlimdvva ⊢ ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) → ( ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ( ℤ ∖ { 0 } ) 𝑒 = ⟨ ( 𝑥 / 𝑦 ) , ( ( 𝐿 ‘ 𝑥 ) / ( 𝐿 ‘ 𝑦 ) ) ⟩ → ∃ 𝑞 ∃ 𝑠 ( 𝑒 = ⟨ 𝑞 , 𝑠 ⟩ ∧ ( 𝑞 ∈ ℚ ∧ 𝑠 = ( ( 𝐿 ‘ ( numer ‘ 𝑞 ) ) / ( 𝐿 ‘ ( denom ‘ 𝑞 ) ) ) ) ) ) )
55 54 imp ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ( ℤ ∖ { 0 } ) 𝑒 = ⟨ ( 𝑥 / 𝑦 ) , ( ( 𝐿 ‘ 𝑥 ) / ( 𝐿 ‘ 𝑦 ) ) ⟩ ) → ∃ 𝑞 ∃ 𝑠 ( 𝑒 = ⟨ 𝑞 , 𝑠 ⟩ ∧ ( 𝑞 ∈ ℚ ∧ 𝑠 = ( ( 𝐿 ‘ ( numer ‘ 𝑞 ) ) / ( 𝐿 ‘ ( denom ‘ 𝑞 ) ) ) ) ) )
56 19.42vv ⊢ ( ∃ 𝑞 ∃ 𝑠 ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑒 = ⟨ 𝑞 , 𝑠 ⟩ ∧ ( 𝑞 ∈ ℚ ∧ 𝑠 = ( ( 𝐿 ‘ ( numer ‘ 𝑞 ) ) / ( 𝐿 ‘ ( denom ‘ 𝑞 ) ) ) ) ) ) ↔ ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ∃ 𝑞 ∃ 𝑠 ( 𝑒 = ⟨ 𝑞 , 𝑠 ⟩ ∧ ( 𝑞 ∈ ℚ ∧ 𝑠 = ( ( 𝐿 ‘ ( numer ‘ 𝑞 ) ) / ( 𝐿 ‘ ( denom ‘ 𝑞 ) ) ) ) ) ) )
57 simprrl ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑒 = ⟨ 𝑞 , 𝑠 ⟩ ∧ ( 𝑞 ∈ ℚ ∧ 𝑠 = ( ( 𝐿 ‘ ( numer ‘ 𝑞 ) ) / ( 𝐿 ‘ ( denom ‘ 𝑞 ) ) ) ) ) ) → 𝑞 ∈ ℚ )
58 qnumcl ⊢ ( 𝑞 ∈ ℚ → ( numer ‘ 𝑞 ) ∈ ℤ )
59 57 58 syl ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑒 = ⟨ 𝑞 , 𝑠 ⟩ ∧ ( 𝑞 ∈ ℚ ∧ 𝑠 = ( ( 𝐿 ‘ ( numer ‘ 𝑞 ) ) / ( 𝐿 ‘ ( denom ‘ 𝑞 ) ) ) ) ) ) → ( numer ‘ 𝑞 ) ∈ ℤ )
60 qdencl ⊢ ( 𝑞 ∈ ℚ → ( denom ‘ 𝑞 ) ∈ ℕ )
61 57 60 syl ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑒 = ⟨ 𝑞 , 𝑠 ⟩ ∧ ( 𝑞 ∈ ℚ ∧ 𝑠 = ( ( 𝐿 ‘ ( numer ‘ 𝑞 ) ) / ( 𝐿 ‘ ( denom ‘ 𝑞 ) ) ) ) ) ) → ( denom ‘ 𝑞 ) ∈ ℕ )
62 61 nnzd ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑒 = ⟨ 𝑞 , 𝑠 ⟩ ∧ ( 𝑞 ∈ ℚ ∧ 𝑠 = ( ( 𝐿 ‘ ( numer ‘ 𝑞 ) ) / ( 𝐿 ‘ ( denom ‘ 𝑞 ) ) ) ) ) ) → ( denom ‘ 𝑞 ) ∈ ℤ )
63 nnne0 ⊢ ( ( denom ‘ 𝑞 ) ∈ ℕ → ( denom ‘ 𝑞 ) ≠ 0 )
64 nelsn ⊢ ( ( denom ‘ 𝑞 ) ≠ 0 → ¬ ( denom ‘ 𝑞 ) ∈ { 0 } )
65 61 63 64 3syl ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑒 = ⟨ 𝑞 , 𝑠 ⟩ ∧ ( 𝑞 ∈ ℚ ∧ 𝑠 = ( ( 𝐿 ‘ ( numer ‘ 𝑞 ) ) / ( 𝐿 ‘ ( denom ‘ 𝑞 ) ) ) ) ) ) → ¬ ( denom ‘ 𝑞 ) ∈ { 0 } )
66 62 65 eldifd ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑒 = ⟨ 𝑞 , 𝑠 ⟩ ∧ ( 𝑞 ∈ ℚ ∧ 𝑠 = ( ( 𝐿 ‘ ( numer ‘ 𝑞 ) ) / ( 𝐿 ‘ ( denom ‘ 𝑞 ) ) ) ) ) ) → ( denom ‘ 𝑞 ) ∈ ( ℤ ∖ { 0 } ) )
67 simprl ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑒 = ⟨ 𝑞 , 𝑠 ⟩ ∧ ( 𝑞 ∈ ℚ ∧ 𝑠 = ( ( 𝐿 ‘ ( numer ‘ 𝑞 ) ) / ( 𝐿 ‘ ( denom ‘ 𝑞 ) ) ) ) ) ) → 𝑒 = ⟨ 𝑞 , 𝑠 ⟩ )
68 qeqnumdivden ⊢ ( 𝑞 ∈ ℚ → 𝑞 = ( ( numer ‘ 𝑞 ) / ( denom ‘ 𝑞 ) ) )
69 57 68 syl ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑒 = ⟨ 𝑞 , 𝑠 ⟩ ∧ ( 𝑞 ∈ ℚ ∧ 𝑠 = ( ( 𝐿 ‘ ( numer ‘ 𝑞 ) ) / ( 𝐿 ‘ ( denom ‘ 𝑞 ) ) ) ) ) ) → 𝑞 = ( ( numer ‘ 𝑞 ) / ( denom ‘ 𝑞 ) ) )
70 simprrr ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑒 = ⟨ 𝑞 , 𝑠 ⟩ ∧ ( 𝑞 ∈ ℚ ∧ 𝑠 = ( ( 𝐿 ‘ ( numer ‘ 𝑞 ) ) / ( 𝐿 ‘ ( denom ‘ 𝑞 ) ) ) ) ) ) → 𝑠 = ( ( 𝐿 ‘ ( numer ‘ 𝑞 ) ) / ( 𝐿 ‘ ( denom ‘ 𝑞 ) ) ) )
71 69 70 opeq12d ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑒 = ⟨ 𝑞 , 𝑠 ⟩ ∧ ( 𝑞 ∈ ℚ ∧ 𝑠 = ( ( 𝐿 ‘ ( numer ‘ 𝑞 ) ) / ( 𝐿 ‘ ( denom ‘ 𝑞 ) ) ) ) ) ) → ⟨ 𝑞 , 𝑠 ⟩ = ⟨ ( ( numer ‘ 𝑞 ) / ( denom ‘ 𝑞 ) ) , ( ( 𝐿 ‘ ( numer ‘ 𝑞 ) ) / ( 𝐿 ‘ ( denom ‘ 𝑞 ) ) ) ⟩ )
72 67 71 eqtrd ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑒 = ⟨ 𝑞 , 𝑠 ⟩ ∧ ( 𝑞 ∈ ℚ ∧ 𝑠 = ( ( 𝐿 ‘ ( numer ‘ 𝑞 ) ) / ( 𝐿 ‘ ( denom ‘ 𝑞 ) ) ) ) ) ) → 𝑒 = ⟨ ( ( numer ‘ 𝑞 ) / ( denom ‘ 𝑞 ) ) , ( ( 𝐿 ‘ ( numer ‘ 𝑞 ) ) / ( 𝐿 ‘ ( denom ‘ 𝑞 ) ) ) ⟩ )
73 oveq1 ⊢ ( 𝑥 = ( numer ‘ 𝑞 ) → ( 𝑥 / 𝑦 ) = ( ( numer ‘ 𝑞 ) / 𝑦 ) )
74 fveq2 ⊢ ( 𝑥 = ( numer ‘ 𝑞 ) → ( 𝐿 ‘ 𝑥 ) = ( 𝐿 ‘ ( numer ‘ 𝑞 ) ) )
75 74 oveq1d ⊢ ( 𝑥 = ( numer ‘ 𝑞 ) → ( ( 𝐿 ‘ 𝑥 ) / ( 𝐿 ‘ 𝑦 ) ) = ( ( 𝐿 ‘ ( numer ‘ 𝑞 ) ) / ( 𝐿 ‘ 𝑦 ) ) )
76 73 75 opeq12d ⊢ ( 𝑥 = ( numer ‘ 𝑞 ) → ⟨ ( 𝑥 / 𝑦 ) , ( ( 𝐿 ‘ 𝑥 ) / ( 𝐿 ‘ 𝑦 ) ) ⟩ = ⟨ ( ( numer ‘ 𝑞 ) / 𝑦 ) , ( ( 𝐿 ‘ ( numer ‘ 𝑞 ) ) / ( 𝐿 ‘ 𝑦 ) ) ⟩ )
77 76 eqeq2d ⊢ ( 𝑥 = ( numer ‘ 𝑞 ) → ( 𝑒 = ⟨ ( 𝑥 / 𝑦 ) , ( ( 𝐿 ‘ 𝑥 ) / ( 𝐿 ‘ 𝑦 ) ) ⟩ ↔ 𝑒 = ⟨ ( ( numer ‘ 𝑞 ) / 𝑦 ) , ( ( 𝐿 ‘ ( numer ‘ 𝑞 ) ) / ( 𝐿 ‘ 𝑦 ) ) ⟩ ) )
78 oveq2 ⊢ ( 𝑦 = ( denom ‘ 𝑞 ) → ( ( numer ‘ 𝑞 ) / 𝑦 ) = ( ( numer ‘ 𝑞 ) / ( denom ‘ 𝑞 ) ) )
79 fveq2 ⊢ ( 𝑦 = ( denom ‘ 𝑞 ) → ( 𝐿 ‘ 𝑦 ) = ( 𝐿 ‘ ( denom ‘ 𝑞 ) ) )
80 79 oveq2d ⊢ ( 𝑦 = ( denom ‘ 𝑞 ) → ( ( 𝐿 ‘ ( numer ‘ 𝑞 ) ) / ( 𝐿 ‘ 𝑦 ) ) = ( ( 𝐿 ‘ ( numer ‘ 𝑞 ) ) / ( 𝐿 ‘ ( denom ‘ 𝑞 ) ) ) )
81 78 80 opeq12d ⊢ ( 𝑦 = ( denom ‘ 𝑞 ) → ⟨ ( ( numer ‘ 𝑞 ) / 𝑦 ) , ( ( 𝐿 ‘ ( numer ‘ 𝑞 ) ) / ( 𝐿 ‘ 𝑦 ) ) ⟩ = ⟨ ( ( numer ‘ 𝑞 ) / ( denom ‘ 𝑞 ) ) , ( ( 𝐿 ‘ ( numer ‘ 𝑞 ) ) / ( 𝐿 ‘ ( denom ‘ 𝑞 ) ) ) ⟩ )
82 81 eqeq2d ⊢ ( 𝑦 = ( denom ‘ 𝑞 ) → ( 𝑒 = ⟨ ( ( numer ‘ 𝑞 ) / 𝑦 ) , ( ( 𝐿 ‘ ( numer ‘ 𝑞 ) ) / ( 𝐿 ‘ 𝑦 ) ) ⟩ ↔ 𝑒 = ⟨ ( ( numer ‘ 𝑞 ) / ( denom ‘ 𝑞 ) ) , ( ( 𝐿 ‘ ( numer ‘ 𝑞 ) ) / ( 𝐿 ‘ ( denom ‘ 𝑞 ) ) ) ⟩ ) )
83 77 82 rspc2ev ⊢ ( ( ( numer ‘ 𝑞 ) ∈ ℤ ∧ ( denom ‘ 𝑞 ) ∈ ( ℤ ∖ { 0 } ) ∧ 𝑒 = ⟨ ( ( numer ‘ 𝑞 ) / ( denom ‘ 𝑞 ) ) , ( ( 𝐿 ‘ ( numer ‘ 𝑞 ) ) / ( 𝐿 ‘ ( denom ‘ 𝑞 ) ) ) ⟩ ) → ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ( ℤ ∖ { 0 } ) 𝑒 = ⟨ ( 𝑥 / 𝑦 ) , ( ( 𝐿 ‘ 𝑥 ) / ( 𝐿 ‘ 𝑦 ) ) ⟩ )
84 59 66 72 83 syl3anc ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑒 = ⟨ 𝑞 , 𝑠 ⟩ ∧ ( 𝑞 ∈ ℚ ∧ 𝑠 = ( ( 𝐿 ‘ ( numer ‘ 𝑞 ) ) / ( 𝐿 ‘ ( denom ‘ 𝑞 ) ) ) ) ) ) → ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ( ℤ ∖ { 0 } ) 𝑒 = ⟨ ( 𝑥 / 𝑦 ) , ( ( 𝐿 ‘ 𝑥 ) / ( 𝐿 ‘ 𝑦 ) ) ⟩ )
85 84 exlimivv ⊢ ( ∃ 𝑞 ∃ 𝑠 ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑒 = ⟨ 𝑞 , 𝑠 ⟩ ∧ ( 𝑞 ∈ ℚ ∧ 𝑠 = ( ( 𝐿 ‘ ( numer ‘ 𝑞 ) ) / ( 𝐿 ‘ ( denom ‘ 𝑞 ) ) ) ) ) ) → ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ( ℤ ∖ { 0 } ) 𝑒 = ⟨ ( 𝑥 / 𝑦 ) , ( ( 𝐿 ‘ 𝑥 ) / ( 𝐿 ‘ 𝑦 ) ) ⟩ )
86 56 85 sylbir ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ∃ 𝑞 ∃ 𝑠 ( 𝑒 = ⟨ 𝑞 , 𝑠 ⟩ ∧ ( 𝑞 ∈ ℚ ∧ 𝑠 = ( ( 𝐿 ‘ ( numer ‘ 𝑞 ) ) / ( 𝐿 ‘ ( denom ‘ 𝑞 ) ) ) ) ) ) → ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ( ℤ ∖ { 0 } ) 𝑒 = ⟨ ( 𝑥 / 𝑦 ) , ( ( 𝐿 ‘ 𝑥 ) / ( 𝐿 ‘ 𝑦 ) ) ⟩ )
87 55 86 impbida ⊢ ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) → ( ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ( ℤ ∖ { 0 } ) 𝑒 = ⟨ ( 𝑥 / 𝑦 ) , ( ( 𝐿 ‘ 𝑥 ) / ( 𝐿 ‘ 𝑦 ) ) ⟩ ↔ ∃ 𝑞 ∃ 𝑠 ( 𝑒 = ⟨ 𝑞 , 𝑠 ⟩ ∧ ( 𝑞 ∈ ℚ ∧ 𝑠 = ( ( 𝐿 ‘ ( numer ‘ 𝑞 ) ) / ( 𝐿 ‘ ( denom ‘ 𝑞 ) ) ) ) ) ) )
88 abid ⊢ ( 𝑒 ∈ { 𝑒 ∣ ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ( ℤ ∖ { 0 } ) 𝑒 = ⟨ ( 𝑥 / 𝑦 ) , ( ( 𝐿 ‘ 𝑥 ) / ( 𝐿 ‘ 𝑦 ) ) ⟩ } ↔ ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ( ℤ ∖ { 0 } ) 𝑒 = ⟨ ( 𝑥 / 𝑦 ) , ( ( 𝐿 ‘ 𝑥 ) / ( 𝐿 ‘ 𝑦 ) ) ⟩ )
89 elopab ⊢ ( 𝑒 ∈ { ⟨ 𝑞 , 𝑠 ⟩ ∣ ( 𝑞 ∈ ℚ ∧ 𝑠 = ( ( 𝐿 ‘ ( numer ‘ 𝑞 ) ) / ( 𝐿 ‘ ( denom ‘ 𝑞 ) ) ) ) } ↔ ∃ 𝑞 ∃ 𝑠 ( 𝑒 = ⟨ 𝑞 , 𝑠 ⟩ ∧ ( 𝑞 ∈ ℚ ∧ 𝑠 = ( ( 𝐿 ‘ ( numer ‘ 𝑞 ) ) / ( 𝐿 ‘ ( denom ‘ 𝑞 ) ) ) ) ) )
90 87 88 89 3bitr4g ⊢ ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) → ( 𝑒 ∈ { 𝑒 ∣ ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ( ℤ ∖ { 0 } ) 𝑒 = ⟨ ( 𝑥 / 𝑦 ) , ( ( 𝐿 ‘ 𝑥 ) / ( 𝐿 ‘ 𝑦 ) ) ⟩ } ↔ 𝑒 ∈ { ⟨ 𝑞 , 𝑠 ⟩ ∣ ( 𝑞 ∈ ℚ ∧ 𝑠 = ( ( 𝐿 ‘ ( numer ‘ 𝑞 ) ) / ( 𝐿 ‘ ( denom ‘ 𝑞 ) ) ) ) } ) )
91 15 16 17 90 eqrd ⊢ ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) → { 𝑒 ∣ ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ( ℤ ∖ { 0 } ) 𝑒 = ⟨ ( 𝑥 / 𝑦 ) , ( ( 𝐿 ‘ 𝑥 ) / ( 𝐿 ‘ 𝑦 ) ) ⟩ } = { ⟨ 𝑞 , 𝑠 ⟩ ∣ ( 𝑞 ∈ ℚ ∧ 𝑠 = ( ( 𝐿 ‘ ( numer ‘ 𝑞 ) ) / ( 𝐿 ‘ ( denom ‘ 𝑞 ) ) ) ) } )
92 eqid ⊢ ( 𝑥 ∈ ℤ , 𝑦 ∈ ( ℤ ∖ { 0 } ) ↦ ⟨ ( 𝑥 / 𝑦 ) , ( ( 𝐿 ‘ 𝑥 ) / ( 𝐿 ‘ 𝑦 ) ) ⟩ ) = ( 𝑥 ∈ ℤ , 𝑦 ∈ ( ℤ ∖ { 0 } ) ↦ ⟨ ( 𝑥 / 𝑦 ) , ( ( 𝐿 ‘ 𝑥 ) / ( 𝐿 ‘ 𝑦 ) ) ⟩ )
93 92 rnmpo ⊢ ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ( ℤ ∖ { 0 } ) ↦ ⟨ ( 𝑥 / 𝑦 ) , ( ( 𝐿 ‘ 𝑥 ) / ( 𝐿 ‘ 𝑦 ) ) ⟩ ) = { 𝑒 ∣ ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ( ℤ ∖ { 0 } ) 𝑒 = ⟨ ( 𝑥 / 𝑦 ) , ( ( 𝐿 ‘ 𝑥 ) / ( 𝐿 ‘ 𝑦 ) ) ⟩ }
94 df-mpt ⊢ ( 𝑞 ∈ ℚ ↦ ( ( 𝐿 ‘ ( numer ‘ 𝑞 ) ) / ( 𝐿 ‘ ( denom ‘ 𝑞 ) ) ) ) = { ⟨ 𝑞 , 𝑠 ⟩ ∣ ( 𝑞 ∈ ℚ ∧ 𝑠 = ( ( 𝐿 ‘ ( numer ‘ 𝑞 ) ) / ( 𝐿 ‘ ( denom ‘ 𝑞 ) ) ) ) }
95 91 93 94 3eqtr4g ⊢ ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) → ran ( 𝑥 ∈ ℤ , 𝑦 ∈ ( ℤ ∖ { 0 } ) ↦ ⟨ ( 𝑥 / 𝑦 ) , ( ( 𝐿 ‘ 𝑥 ) / ( 𝐿 ‘ 𝑦 ) ) ⟩ ) = ( 𝑞 ∈ ℚ ↦ ( ( 𝐿 ‘ ( numer ‘ 𝑞 ) ) / ( 𝐿 ‘ ( denom ‘ 𝑞 ) ) ) ) )
96 8 14 95 3eqtrd ⊢ ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) → ( ℚHom ‘ 𝑅 ) = ( 𝑞 ∈ ℚ ↦ ( ( 𝐿 ‘ ( numer ‘ 𝑞 ) ) / ( 𝐿 ‘ ( denom ‘ 𝑞 ) ) ) ) )