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 )