# 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 = ( *𝑟𝑅 )
srng1.t 1 = ( 1r𝑅 )
Assertion srng1 ( 𝑅 ∈ *-Ring → ( 1 ) = 1 )

### Proof

Step Hyp Ref Expression
1 srng1.i = ( *𝑟𝑅 )
2 srng1.t 1 = ( 1r𝑅 )
3 srngring ( 𝑅 ∈ *-Ring → 𝑅 ∈ Ring )
4 eqid ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
5 4 2 ringidcl ( 𝑅 ∈ Ring → 1 ∈ ( Base ‘ 𝑅 ) )
6 eqid ( *rf𝑅 ) = ( *rf𝑅 )
7 4 1 6 stafval ( 1 ∈ ( Base ‘ 𝑅 ) → ( ( *rf𝑅 ) ‘ 1 ) = ( 1 ) )
8 3 5 7 3syl ( 𝑅 ∈ *-Ring → ( ( *rf𝑅 ) ‘ 1 ) = ( 1 ) )
9 eqid ( oppr𝑅 ) = ( oppr𝑅 )
10 9 6 srngrhm ( 𝑅 ∈ *-Ring → ( *rf𝑅 ) ∈ ( 𝑅 RingHom ( oppr𝑅 ) ) )
11 9 2 oppr1 1 = ( 1r ‘ ( oppr𝑅 ) )
12 2 11 rhm1 ( ( *rf𝑅 ) ∈ ( 𝑅 RingHom ( oppr𝑅 ) ) → ( ( *rf𝑅 ) ‘ 1 ) = 1 )
13 10 12 syl ( 𝑅 ∈ *-Ring → ( ( *rf𝑅 ) ‘ 1 ) = 1 )
14 8 13 eqtr3d ( 𝑅 ∈ *-Ring → ( 1 ) = 1 )