Metamath Proof Explorer

Theorem qqhval

Description: Value of the canonical homormorphism from the rational number to a field. (Contributed by Thierry Arnoux, 22-Oct-2017)

Ref Expression
Hypotheses qqhval.1 ⊢ × ˙ = / r ⁡ R
qqhval.2 ⊢ 1 ˙ = 1 R
qqhval.3 ⊢ L = ℤRHom ⁡ R
Assertion qqhval ⊢ R ∈ V → ℚHom ⁡ R = ran ⁡ x ∈ ℤ , y ∈ L -1 Unit ⁡ R ⟼ x y L ⁡ x × ˙ L ⁡ y

Proof

Step Hyp Ref Expression
1 qqhval.1 ⊢ × ˙ = / r ⁡ R
2 qqhval.2 ⊢ 1 ˙ = 1 R
3 qqhval.3 ⊢ L = ℤRHom ⁡ R
4 eqidd ⊢ f = R → ℤ = ℤ
5 fveq2 ⊢ f = R → ℤRHom ⁡ f = ℤRHom ⁡ R
6 5 3 eqtr4di ⊢ f = R → ℤRHom ⁡ f = L
7 6 cnveqd ⊢ f = R → ℤRHom ⁡ f -1 = L -1
8 fveq2 ⊢ f = R → Unit ⁡ f = Unit ⁡ R
9 7 8 imaeq12d ⊢ f = R → ℤRHom ⁡ f -1 Unit ⁡ f = L -1 Unit ⁡ R
10 fveq2 ⊢ f = R → / r ⁡ f = / r ⁡ R
11 10 1 eqtr4di ⊢ f = R → / r ⁡ f = × ˙
12 6 fveq1d ⊢ f = R → ℤRHom ⁡ f ⁡ x = L ⁡ x
13 6 fveq1d ⊢ f = R → ℤRHom ⁡ f ⁡ y = L ⁡ y
14 11 12 13 oveq123d ⊢ f = R → ℤRHom ⁡ f ⁡ x / r ⁡ f ℤRHom ⁡ f ⁡ y = L ⁡ x × ˙ L ⁡ y
15 14 opeq2d ⊢ f = R → x y ℤRHom ⁡ f ⁡ x / r ⁡ f ℤRHom ⁡ f ⁡ y = x y L ⁡ x × ˙ L ⁡ y
16 4 9 15 mpoeq123dv ⊢ f = R → x ∈ ℤ , y ∈ ℤRHom ⁡ f -1 Unit ⁡ f ⟼ x y ℤRHom ⁡ f ⁡ x / r ⁡ f ℤRHom ⁡ f ⁡ y = x ∈ ℤ , y ∈ L -1 Unit ⁡ R ⟼ x y L ⁡ x × ˙ L ⁡ y
17 16 rneqd ⊢ f = R → ran ⁡ x ∈ ℤ , y ∈ ℤRHom ⁡ f -1 Unit ⁡ f ⟼ x y ℤRHom ⁡ f ⁡ x / r ⁡ f ℤRHom ⁡ f ⁡ y = ran ⁡ x ∈ ℤ , y ∈ L -1 Unit ⁡ R ⟼ x y L ⁡ x × ˙ L ⁡ y
18 df-qqh ⊢ ℚHom = f ∈ V ⟼ ran ⁡ x ∈ ℤ , y ∈ ℤRHom ⁡ f -1 Unit ⁡ f ⟼ x y ℤRHom ⁡ f ⁡ x / r ⁡ f ℤRHom ⁡ f ⁡ y
19 zex ⊢ ℤ ∈ V
20 3 fvexi ⊢ L ∈ V
21 20 cnvex ⊢ L -1 ∈ V
22 imaexg ⊢ L -1 ∈ V → L -1 Unit ⁡ R ∈ V
23 21 22 ax-mp ⊢ L -1 Unit ⁡ R ∈ V
24 19 23 mpoex ⊢ x ∈ ℤ , y ∈ L -1 Unit ⁡ R ⟼ x y L ⁡ x × ˙ L ⁡ y ∈ V
25 24 rnex ⊢ ran ⁡ x ∈ ℤ , y ∈ L -1 Unit ⁡ R ⟼ x y L ⁡ x × ˙ L ⁡ y ∈ V
26 17 18 25 fvmpt ⊢ R ∈ V → ℚHom ⁡ R = ran ⁡ x ∈ ℤ , y ∈ L -1 Unit ⁡ R ⟼ x y L ⁡ x × ˙ L ⁡ y