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	|- .* = ( *r ` R )
	srngcl.b	|- B = ( Base ` R )
Assertion	srngcl	|- ( ( R e. *Ring /\ X e. B ) -> ( .* ` X ) e. B )

Proof

Step	Hyp	Ref	Expression
1		srngcl.i	|- .* = ( *r ` R )
2		srngcl.b	|- B = ( Base ` R )
3		eqid	|- ( *rf ` R ) = ( *rf ` R )
4	2 1 3	stafval	|- ( X e. B -> ( ( *rf ` R ) ` X ) = ( .* ` X ) )
5	4	adantl	|- ( ( R e. *Ring /\ X e. B ) -> ( ( *rf ` R ) ` X ) = ( .* ` X ) )
6	3 2	srngf1o	|- ( R e. *Ring -> ( *rf ` R ) : B -1-1-onto-> B )
7		f1of	|- ( ( *rf ` R ) : B -1-1-onto-> B -> ( *rf ` R ) : B --> B )
8	6 7	syl	|- ( R e. *Ring -> ( *rf ` R ) : B --> B )
9	8	ffvelcdmda	|- ( ( R e. *Ring /\ X e. B ) -> ( ( *rf ` R ) ` X ) e. B )
10	5 9	eqeltrrd	|- ( ( R e. *Ring /\ X e. B ) -> ( .* ` X ) e. B )