This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )