# 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 )