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

Metamath Proof Explorer

Theorem srng0

Description: The conjugate of the ring zero is zero. (Contributed by Mario Carneiro, 7-Oct-2015)

Ref Expression
Hypotheses srng0.i ⊢ ∗ = ( *𝑟 ‘ 𝑅 )
srng0.z ⊢ 0 = ( 0g ‘ 𝑅 )
Assertion srng0 ( 𝑅 ∈ *-Ring → ( ∗ ‘ 0 ) = 0 )

Proof

Step Hyp Ref Expression
1 srng0.i ⊢ ∗ = ( *𝑟 ‘ 𝑅 )
2 srng0.z ⊢ 0 = ( 0g ‘ 𝑅 )
3 srngring ⊢ ( 𝑅 ∈ *-Ring → 𝑅 ∈ Ring )
4 ringgrp ⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Grp )
5 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
6 5 2 grpidcl ⊢ ( 𝑅 ∈ Grp → 0 ∈ ( Base ‘ 𝑅 ) )
7 eqid ⊢ ( *rf ‘ 𝑅 ) = ( *rf ‘ 𝑅 )
8 5 1 7 stafval ⊢ ( 0 ∈ ( Base ‘ 𝑅 ) → ( ( *rf ‘ 𝑅 ) ‘ 0 ) = ( ∗ ‘ 0 ) )
9 3 4 6 8 4syl ⊢ ( 𝑅 ∈ *-Ring → ( ( *rf ‘ 𝑅 ) ‘ 0 ) = ( ∗ ‘ 0 ) )
10 eqid ⊢ ( oppr ‘ 𝑅 ) = ( oppr ‘ 𝑅 )
11 10 7 srngrhm ⊢ ( 𝑅 ∈ *-Ring → ( *rf ‘ 𝑅 ) ∈ ( 𝑅 RingHom ( oppr ‘ 𝑅 ) ) )
12 rhmghm ⊢ ( ( *rf ‘ 𝑅 ) ∈ ( 𝑅 RingHom ( oppr ‘ 𝑅 ) ) → ( *rf ‘ 𝑅 ) ∈ ( 𝑅 GrpHom ( oppr ‘ 𝑅 ) ) )
13 10 2 oppr0 ⊢ 0 = ( 0g ‘ ( oppr ‘ 𝑅 ) )
14 2 13 ghmid ⊢ ( ( *rf ‘ 𝑅 ) ∈ ( 𝑅 GrpHom ( oppr ‘ 𝑅 ) ) → ( ( *rf ‘ 𝑅 ) ‘ 0 ) = 0 )
15 11 12 14 3syl ⊢ ( 𝑅 ∈ *-Ring → ( ( *rf ‘ 𝑅 ) ‘ 0 ) = 0 )
16 9 15 eqtr3d ⊢ ( 𝑅 ∈ *-Ring → ( ∗ ‘ 0 ) = 0 )