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 )