# 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
`|- .* = ( *r ` R )`
srng0.z
`|- .0. = ( 0g ` R )`
Assertion srng0
`|- ( R e. *Ring -> ( .* ` .0. ) = .0. )`

### Proof

Step Hyp Ref Expression
1 srng0.i
` |-  .* = ( *r ` R )`
2 srng0.z
` |-  .0. = ( 0g ` R )`
3 srngring
` |-  ( R e. *Ring -> R e. Ring )`
4 ringgrp
` |-  ( R e. Ring -> R e. Grp )`
5 eqid
` |-  ( Base ` R ) = ( Base ` R )`
6 5 2 grpidcl
` |-  ( R e. Grp -> .0. e. ( Base ` R ) )`
7 eqid
` |-  ( *rf ` R ) = ( *rf ` R )`
8 5 1 7 stafval
` |-  ( .0. e. ( Base ` R ) -> ( ( *rf ` R ) ` .0. ) = ( .* ` .0. ) )`
9 3 4 6 8 4syl
` |-  ( R e. *Ring -> ( ( *rf ` R ) ` .0. ) = ( .* ` .0. ) )`
10 eqid
` |-  ( oppR ` R ) = ( oppR ` R )`
11 10 7 srngrhm
` |-  ( R e. *Ring -> ( *rf ` R ) e. ( R RingHom ( oppR ` R ) ) )`
12 rhmghm
` |-  ( ( *rf ` R ) e. ( R RingHom ( oppR ` R ) ) -> ( *rf ` R ) e. ( R GrpHom ( oppR ` R ) ) )`
13 10 2 oppr0
` |-  .0. = ( 0g ` ( oppR ` R ) )`
14 2 13 ghmid
` |-  ( ( *rf ` R ) e. ( R GrpHom ( oppR ` R ) ) -> ( ( *rf ` R ) ` .0. ) = .0. )`
15 11 12 14 3syl
` |-  ( R e. *Ring -> ( ( *rf ` R ) ` .0. ) = .0. )`
16 9 15 eqtr3d
` |-  ( R e. *Ring -> ( .* ` .0. ) = .0. )`