Theorem srngcl

Description: The involution function in a star ring is closed in the ring. (Contributed by Mario Carneiro, 6-Oct-2015)

	Ref	Expression
Hypotheses	srngcl.i	$$⊢\underset{\dot{}}{\ast }={\mathrm{*}}_R$$
	srngcl.b	$$⊢B={\mathrm{Base}}_R$$
Assertion	srngcl	$$⊢\left(R\in \mathrm{*-Ring}\wedge X\in B\right)\to \underset{\dot{}}{\ast }\left(X\right)\in B$$

Proof

Step	Hyp	Ref	Expression
1		srngcl.i	$$⊢\underset{\dot{}}{\ast }={\mathrm{*}}_R$$
2		srngcl.b	$$⊢B={\mathrm{Base}}_R$$
3		eqid	$$⊢{\ast }_{\mathrm{𝑟𝑓}}\left(R\right)={\ast }_{\mathrm{𝑟𝑓}}\left(R\right)$$
4	2 1 3	stafval	$$⊢X\in B\to {\ast }_{\mathrm{𝑟𝑓}}\left(R\right)\left(X\right)=\underset{\dot{}}{\ast }\left(X\right)$$
5	4	adantl	$$⊢\left(R\in \mathrm{*-Ring}\wedge X\in B\right)\to {\ast }_{\mathrm{𝑟𝑓}}\left(R\right)\left(X\right)=\underset{\dot{}}{\ast }\left(X\right)$$
6	3 2	srngf1o	$$⊢R\in \mathrm{*-Ring}\to {\ast }_{\mathrm{𝑟𝑓}}\left(R\right):B\underset{1-1\; onto}{⟶}B$$
7		f1of	$$⊢{\ast }_{\mathrm{𝑟𝑓}}\left(R\right):B\underset{1-1\; onto}{⟶}B\to {\ast }_{\mathrm{𝑟𝑓}}\left(R\right):B⟶B$$
8	6 7	syl	$$⊢R\in \mathrm{*-Ring}\to {\ast }_{\mathrm{𝑟𝑓}}\left(R\right):B⟶B$$
9	8	ffvelcdmda	$$⊢\left(R\in \mathrm{*-Ring}\wedge X\in B\right)\to {\ast }_{\mathrm{𝑟𝑓}}\left(R\right)\left(X\right)\in B$$
10	5 9	eqeltrrd	$$⊢\left(R\in \mathrm{*-Ring}\wedge X\in B\right)\to \underset{\dot{}}{\ast }\left(X\right)\in B$$