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

Metamath Proof Explorer

Theorem srngnvl

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

Ref Expression
Hypotheses srngcl.i 
|- .* = ( *r ` R )
srngcl.b 
|- B = ( Base ` R )
Assertion srngnvl 
|- ( ( R e. *Ring /\ X e. B ) -> ( .* ` ( .* ` X ) ) = X )

Proof

Step Hyp Ref Expression
1 srngcl.i 
 |-  .* = ( *r ` R )
2 srngcl.b 
 |-  B = ( Base ` R )
3 1 2 srngcl 
 |-  ( ( R e. *Ring /\ X e. B ) -> ( .* ` X ) e. B )
4 eqid 
 |-  ( *rf ` R ) = ( *rf ` R )
5 2 1 4 stafval 
 |-  ( ( .* ` X ) e. B -> ( ( *rf ` R ) ` ( .* ` X ) ) = ( .* ` ( .* ` X ) ) )
6 3 5 syl 
 |-  ( ( R e. *Ring /\ X e. B ) -> ( ( *rf ` R ) ` ( .* ` X ) ) = ( .* ` ( .* ` X ) ) )
7 4 srngcnv 
 |-  ( R e. *Ring -> ( *rf ` R ) = `' ( *rf ` R ) )
8 7 adantr 
 |-  ( ( R e. *Ring /\ X e. B ) -> ( *rf ` R ) = `' ( *rf ` R ) )
9 8 fveq1d 
 |-  ( ( R e. *Ring /\ X e. B ) -> ( ( *rf ` R ) ` ( ( *rf ` R ) ` X ) ) = ( `' ( *rf ` R ) ` ( ( *rf ` R ) ` X ) ) )
10 2 1 4 stafval 
 |-  ( X e. B -> ( ( *rf ` R ) ` X ) = ( .* ` X ) )
11 10 adantl 
 |-  ( ( R e. *Ring /\ X e. B ) -> ( ( *rf ` R ) ` X ) = ( .* ` X ) )
12 11 fveq2d 
 |-  ( ( R e. *Ring /\ X e. B ) -> ( ( *rf ` R ) ` ( ( *rf ` R ) ` X ) ) = ( ( *rf ` R ) ` ( .* ` X ) ) )
13 4 2 srngf1o 
 |-  ( R e. *Ring -> ( *rf ` R ) : B -1-1-onto-> B )
14 f1ocnvfv1 
 |-  ( ( ( *rf ` R ) : B -1-1-onto-> B /\ X e. B ) -> ( `' ( *rf ` R ) ` ( ( *rf ` R ) ` X ) ) = X )
15 13 14 sylan 
 |-  ( ( R e. *Ring /\ X e. B ) -> ( `' ( *rf ` R ) ` ( ( *rf ` R ) ` X ) ) = X )
16 9 12 15 3eqtr3d 
 |-  ( ( R e. *Ring /\ X e. B ) -> ( ( *rf ` R ) ` ( .* ` X ) ) = X )
17 6 16 eqtr3d 
 |-  ( ( R e. *Ring /\ X e. B ) -> ( .* ` ( .* ` X ) ) = X )