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 ) )`
` |-  ( ( 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 ) )`
` |-  ( ( R e. *Ring /\ X e. B ) -> ( ( *rf ` R ) ` X ) = ( .* ` X ) )`
` |-  ( ( R e. *Ring /\ X e. B ) -> ( ( *rf ` R ) ` ( ( *rf ` R ) ` X ) ) = ( ( *rf ` R ) ` ( .* ` X ) ) )`
` |-  ( R e. *Ring -> ( *rf ` R ) : B -1-1-onto-> B )`
` |-  ( ( ( *rf ` R ) : B -1-1-onto-> B /\ X e. B ) -> ( `' ( *rf ` R ) ` ( ( *rf ` R ) ` X ) ) = X )`
` |-  ( ( R e. *Ring /\ X e. B ) -> ( `' ( *rf ` R ) ` ( ( *rf ` R ) ` X ) ) = X )`
` |-  ( ( R e. *Ring /\ X e. B ) -> ( ( *rf ` R ) ` ( .* ` X ) ) = X )`
` |-  ( ( R e. *Ring /\ X e. B ) -> ( .* ` ( .* ` X ) ) = X )`