This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem zrh1

Description: Interpretation of 1 in a ring. (Contributed by Stefan O'Rear, 6-Sep-2015)

Ref Expression
Hypotheses zrh1.l ⊢ L = ℤRHom ⁡ R
zrh1.o ⊢ 1 ˙ = 1 R
Assertion zrh1 ⊢ R ∈ Ring → L ⁡ 1 = 1 ˙

Proof

Step Hyp Ref Expression
1 zrh1.l ⊢ L = ℤRHom ⁡ R
2 zrh1.o ⊢ 1 ˙ = 1 R
3 1 zrhrhm ⊢ R ∈ Ring → L ∈ ℤ ring RingHom R
4 zring1 ⊢ 1 = 1 ℤ ring
5 4 2 rhm1 ⊢ L ∈ ℤ ring RingHom R → L ⁡ 1 = 1 ˙
6 3 5 syl ⊢ R ∈ Ring → L ⁡ 1 = 1 ˙