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

Metamath Proof Explorer

Theorem srng1

Description: The conjugate of the ring identity is the identity. (This is sometimes taken as an axiom, and indeed the proof here follows because we defined *r to be a ring homomorphism, which preserves 1; nevertheless, it is redundant, as can be seen from the proof of issrngd .) (Contributed by Mario Carneiro, 6-Oct-2015)

Ref Expression
Hypotheses srng1.i 
|- .* = ( *r ` R )
srng1.t 
|- .1. = ( 1r ` R )
Assertion srng1 
|- ( R e. *Ring -> ( .* ` .1. ) = .1. )

Proof

Step Hyp Ref Expression
1 srng1.i 
 |-  .* = ( *r ` R )
2 srng1.t 
 |-  .1. = ( 1r ` R )
3 srngring 
 |-  ( R e. *Ring -> R e. Ring )
4 eqid 
 |-  ( Base ` R ) = ( Base ` R )
5 4 2 ringidcl 
 |-  ( R e. Ring -> .1. e. ( Base ` R ) )
6 eqid 
 |-  ( *rf ` R ) = ( *rf ` R )
7 4 1 6 stafval 
 |-  ( .1. e. ( Base ` R ) -> ( ( *rf ` R ) ` .1. ) = ( .* ` .1. ) )
8 3 5 7 3syl 
 |-  ( R e. *Ring -> ( ( *rf ` R ) ` .1. ) = ( .* ` .1. ) )
9 eqid 
 |-  ( oppR ` R ) = ( oppR ` R )
10 9 6 srngrhm 
 |-  ( R e. *Ring -> ( *rf ` R ) e. ( R RingHom ( oppR ` R ) ) )
11 9 2 oppr1 
 |-  .1. = ( 1r ` ( oppR ` R ) )
12 2 11 rhm1 
 |-  ( ( *rf ` R ) e. ( R RingHom ( oppR ` R ) ) -> ( ( *rf ` R ) ` .1. ) = .1. )
13 10 12 syl 
 |-  ( R e. *Ring -> ( ( *rf ` R ) ` .1. ) = .1. )
14 8 13 eqtr3d 
 |-  ( R e. *Ring -> ( .* ` .1. ) = .1. )