Theorem srng0

Description: The conjugate of the ring zero is zero. (Contributed by Mario Carneiro, 7-Oct-2015)

	Ref	Expression
Hypotheses	srng0.i	$$⊢\underset{\dot{}}{\ast }={\mathrm{*}}_R$$
	srng0.z	$$⊢\underset{\dot{}}{0}=0_R$$
Assertion	srng0	$$⊢R\in \mathrm{*-Ring}\to \underset{\dot{}}{\ast }\left(\underset{\dot{}}{0}\right)=\underset{\dot{}}{0}$$

Proof

Step	Hyp	Ref	Expression
1		srng0.i	$$⊢\underset{\dot{}}{\ast }={\mathrm{*}}_R$$
2		srng0.z	$$⊢\underset{\dot{}}{0}=0_R$$
3		srngring	$$⊢R\in \mathrm{*-Ring}\to R\in \mathrm{Ring}$$
4		ringgrp	$$⊢R\in \mathrm{Ring}\to R\in \mathrm{Grp}$$
5		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
6	5 2	grpidcl	$$⊢R\in \mathrm{Grp}\to \underset{\dot{}}{0}\in {\mathrm{Base}}_R$$
7		eqid	$$⊢{\ast }_{\mathrm{𝑟𝑓}}\left(R\right)={\ast }_{\mathrm{𝑟𝑓}}\left(R\right)$$
8	5 1 7	stafval	$$⊢\underset{\dot{}}{0}\in {\mathrm{Base}}_R\to {\ast }_{\mathrm{𝑟𝑓}}\left(R\right)\left(\underset{\dot{}}{0}\right)=\underset{\dot{}}{\ast }\left(\underset{\dot{}}{0}\right)$$
9	3 4 6 8	4syl	$$⊢R\in \mathrm{*-Ring}\to {\ast }_{\mathrm{𝑟𝑓}}\left(R\right)\left(\underset{\dot{}}{0}\right)=\underset{\dot{}}{\ast }\left(\underset{\dot{}}{0}\right)$$
10		eqid	$$⊢{opp}_r\left(R\right)={opp}_r\left(R\right)$$
11	10 7	srngrhm	$$⊢R\in \mathrm{*-Ring}\to {\ast }_{\mathrm{𝑟𝑓}}\left(R\right)\in \left(R\mathrm{RingHom}{opp}_r\left(R\right)\right)$$
12		rhmghm	$$⊢{\ast }_{\mathrm{𝑟𝑓}}\left(R\right)\in \left(R\mathrm{RingHom}{opp}_r\left(R\right)\right)\to {\ast }_{\mathrm{𝑟𝑓}}\left(R\right)\in \left(R\mathrm{GrpHom}{opp}_r\left(R\right)\right)$$
13	10 2	oppr0	$$⊢\underset{\dot{}}{0}=0_{{opp}_r\left(R\right)}$$
14	2 13	ghmid	$$⊢{\ast }_{\mathrm{𝑟𝑓}}\left(R\right)\in \left(R\mathrm{GrpHom}{opp}_r\left(R\right)\right)\to {\ast }_{\mathrm{𝑟𝑓}}\left(R\right)\left(\underset{\dot{}}{0}\right)=\underset{\dot{}}{0}$$
15	11 12 14	3syl	$$⊢R\in \mathrm{*-Ring}\to {\ast }_{\mathrm{𝑟𝑓}}\left(R\right)\left(\underset{\dot{}}{0}\right)=\underset{\dot{}}{0}$$
16	9 15	eqtr3d	$$⊢R\in \mathrm{*-Ring}\to \underset{\dot{}}{\ast }\left(\underset{\dot{}}{0}\right)=\underset{\dot{}}{0}$$