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

Metamath Proof Explorer

Theorem zrhval2

Description: Alternate value of the ZRHom homomorphism. (Contributed by Mario Carneiro, 12-Jun-2015)

Ref Expression
Hypotheses zrhval.l ⊢ 𝐿 = ( ℤRHom ‘ 𝑅 )
zrhval2.m ⊢ · = ( .g ‘ 𝑅 )
zrhval2.1 ⊢ 1 = ( 1r ‘ 𝑅 )
Assertion zrhval2 ( 𝑅 ∈ Ring → 𝐿 = ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 1 ) ) )

Proof

Step Hyp Ref Expression
1 zrhval.l ⊢ 𝐿 = ( ℤRHom ‘ 𝑅 )
2 zrhval2.m ⊢ · = ( .g ‘ 𝑅 )
3 zrhval2.1 ⊢ 1 = ( 1r ‘ 𝑅 )
4 1 zrhval ⊢ 𝐿 = ∪ ( ℤring RingHom 𝑅 )
5 eqid ⊢ ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 1 ) ) = ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 1 ) )
6 2 5 3 mulgrhm2 ⊢ ( 𝑅 ∈ Ring → ( ℤring RingHom 𝑅 ) = { ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 1 ) ) } )
7 6 unieqd ⊢ ( 𝑅 ∈ Ring → ∪ ( ℤring RingHom 𝑅 ) = ∪ { ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 1 ) ) } )
8 zex ⊢ ℤ ∈ V
9 8 mptex ⊢ ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 1 ) ) ∈ V
10 9 unisn ⊢ ∪ { ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 1 ) ) } = ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 1 ) )
11 7 10 eqtrdi ⊢ ( 𝑅 ∈ Ring → ∪ ( ℤring RingHom 𝑅 ) = ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 1 ) ) )
12 4 11 eqtrid ⊢ ( 𝑅 ∈ Ring → 𝐿 = ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 1 ) ) )