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