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	$$⊢\underset{\dot{}}{\ast }={\mathrm{*}}_R$$
	srng1.t	$$⊢\underset{\dot{}}{1}=1_R$$
Assertion	srng1	$$⊢R\in \mathrm{*-Ring}\to \underset{\dot{}}{\ast }\left(\underset{\dot{}}{1}\right)=\underset{\dot{}}{1}$$

Proof

Step	Hyp	Ref	Expression
1		srng1.i	$$⊢\underset{\dot{}}{\ast }={\mathrm{*}}_R$$
2		srng1.t	$$⊢\underset{\dot{}}{1}=1_R$$
3		srngring	$$⊢R\in \mathrm{*-Ring}\to R\in \mathrm{Ring}$$
4		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
5	4 2	ringidcl	$$⊢R\in \mathrm{Ring}\to \underset{\dot{}}{1}\in {\mathrm{Base}}_R$$
6		eqid	$$⊢{\ast }_{\mathrm{𝑟𝑓}}\left(R\right)={\ast }_{\mathrm{𝑟𝑓}}\left(R\right)$$
7	4 1 6	stafval	$$⊢\underset{\dot{}}{1}\in {\mathrm{Base}}_R\to {\ast }_{\mathrm{𝑟𝑓}}\left(R\right)\left(\underset{\dot{}}{1}\right)=\underset{\dot{}}{\ast }\left(\underset{\dot{}}{1}\right)$$
8	3 5 7	3syl	$$⊢R\in \mathrm{*-Ring}\to {\ast }_{\mathrm{𝑟𝑓}}\left(R\right)\left(\underset{\dot{}}{1}\right)=\underset{\dot{}}{\ast }\left(\underset{\dot{}}{1}\right)$$
9		eqid	$$⊢{opp}_r\left(R\right)={opp}_r\left(R\right)$$
10	9 6	srngrhm	$$⊢R\in \mathrm{*-Ring}\to {\ast }_{\mathrm{𝑟𝑓}}\left(R\right)\in \left(R\mathrm{RingHom}{opp}_r\left(R\right)\right)$$
11	9 2	oppr1	$$⊢\underset{\dot{}}{1}=1_{{opp}_r\left(R\right)}$$
12	2 11	rhm1	$$⊢{\ast }_{\mathrm{𝑟𝑓}}\left(R\right)\in \left(R\mathrm{RingHom}{opp}_r\left(R\right)\right)\to {\ast }_{\mathrm{𝑟𝑓}}\left(R\right)\left(\underset{\dot{}}{1}\right)=\underset{\dot{}}{1}$$
13	10 12	syl	$$⊢R\in \mathrm{*-Ring}\to {\ast }_{\mathrm{𝑟𝑓}}\left(R\right)\left(\underset{\dot{}}{1}\right)=\underset{\dot{}}{1}$$
14	8 13	eqtr3d	$$⊢R\in \mathrm{*-Ring}\to \underset{\dot{}}{\ast }\left(\underset{\dot{}}{1}\right)=\underset{\dot{}}{1}$$