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 
|- .* = ( *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. )