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