Metamath Proof Explorer

Theorem zrhrhmb

Description: The ZRHom homomorphism is the unique ring homomorphism from Z . (Contributed by Mario Carneiro, 15-Jun-2015) (Revised by AV, 12-Jun-2019)

Ref Expression
Hypothesis zrhval.l ⊢ L = ℤRHom ⁡ R
Assertion zrhrhmb ⊢ R ∈ Ring → F ∈ ℤ ring RingHom R ↔ F = L

Proof

Step Hyp Ref Expression
1 zrhval.l ⊢ L = ℤRHom ⁡ R
2 eqid ⊢ ⋅ R = ⋅ R
3 eqid ⊢ n ∈ ℤ ⟼ n ⋅ R 1 R = n ∈ ℤ ⟼ n ⋅ R 1 R
4 eqid ⊢ 1 R = 1 R
5 2 3 4 mulgrhm2 ⊢ R ∈ Ring → ℤ ring RingHom R = n ∈ ℤ ⟼ n ⋅ R 1 R
6 1 2 4 zrhval2 ⊢ R ∈ Ring → L = n ∈ ℤ ⟼ n ⋅ R 1 R
7 6 sneqd ⊢ R ∈ Ring → L = n ∈ ℤ ⟼ n ⋅ R 1 R
8 5 7 eqtr4d ⊢ R ∈ Ring → ℤ ring RingHom R = L
9 8 eleq2d ⊢ R ∈ Ring → F ∈ ℤ ring RingHom R ↔ F ∈ L
10 1 fvexi ⊢ L ∈ V
11 10 elsn2 ⊢ F ∈ L ↔ F = L
12 9 11 bitrdi ⊢ R ∈ Ring → F ∈ ℤ ring RingHom R ↔ F = L