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	⊢ ∗ = ( *𝑟 ‘ 𝑅 )
	srngcl.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
Assertion	srngnvl	⊢ ( ( 𝑅 ∈ *-Ring ∧ 𝑋 ∈ 𝐵 ) → ( ∗ ‘ ( ∗ ‘ 𝑋 ) ) = 𝑋 )

Proof

Step	Hyp	Ref	Expression
1		srngcl.i	⊢ ∗ = ( *𝑟 ‘ 𝑅 )
2		srngcl.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
3	1 2	srngcl	⊢ ( ( 𝑅 ∈ *-Ring ∧ 𝑋 ∈ 𝐵 ) → ( ∗ ‘ 𝑋 ) ∈ 𝐵 )
4		eqid	⊢ ( *rf ‘ 𝑅 ) = ( *rf ‘ 𝑅 )
5	2 1 4	stafval	⊢ ( ( ∗ ‘ 𝑋 ) ∈ 𝐵 → ( ( *rf ‘ 𝑅 ) ‘ ( ∗ ‘ 𝑋 ) ) = ( ∗ ‘ ( ∗ ‘ 𝑋 ) ) )
6	3 5	syl	⊢ ( ( 𝑅 ∈ *-Ring ∧ 𝑋 ∈ 𝐵 ) → ( ( *rf ‘ 𝑅 ) ‘ ( ∗ ‘ 𝑋 ) ) = ( ∗ ‘ ( ∗ ‘ 𝑋 ) ) )
7	4	srngcnv	⊢ ( 𝑅 ∈ *-Ring → ( *rf ‘ 𝑅 ) = ◡ ( *rf ‘ 𝑅 ) )
8	7	adantr	⊢ ( ( 𝑅 ∈ *-Ring ∧ 𝑋 ∈ 𝐵 ) → ( *rf ‘ 𝑅 ) = ◡ ( *rf ‘ 𝑅 ) )
9	8	fveq1d	⊢ ( ( 𝑅 ∈ *-Ring ∧ 𝑋 ∈ 𝐵 ) → ( ( *rf ‘ 𝑅 ) ‘ ( ( *rf ‘ 𝑅 ) ‘ 𝑋 ) ) = ( ◡ ( *rf ‘ 𝑅 ) ‘ ( ( *rf ‘ 𝑅 ) ‘ 𝑋 ) ) )
10	2 1 4	stafval	⊢ ( 𝑋 ∈ 𝐵 → ( ( *rf ‘ 𝑅 ) ‘ 𝑋 ) = ( ∗ ‘ 𝑋 ) )
11	10	adantl	⊢ ( ( 𝑅 ∈ *-Ring ∧ 𝑋 ∈ 𝐵 ) → ( ( *rf ‘ 𝑅 ) ‘ 𝑋 ) = ( ∗ ‘ 𝑋 ) )
12	11	fveq2d	⊢ ( ( 𝑅 ∈ *-Ring ∧ 𝑋 ∈ 𝐵 ) → ( ( *rf ‘ 𝑅 ) ‘ ( ( *rf ‘ 𝑅 ) ‘ 𝑋 ) ) = ( ( *rf ‘ 𝑅 ) ‘ ( ∗ ‘ 𝑋 ) ) )
13	4 2	srngf1o	⊢ ( 𝑅 ∈ *-Ring → ( *rf ‘ 𝑅 ) : 𝐵 –1-1-onto→ 𝐵 )
14		f1ocnvfv1	⊢ ( ( ( *rf ‘ 𝑅 ) : 𝐵 –1-1-onto→ 𝐵 ∧ 𝑋 ∈ 𝐵 ) → ( ◡ ( *rf ‘ 𝑅 ) ‘ ( ( *rf ‘ 𝑅 ) ‘ 𝑋 ) ) = 𝑋 )
15	13 14	sylan	⊢ ( ( 𝑅 ∈ *-Ring ∧ 𝑋 ∈ 𝐵 ) → ( ◡ ( *rf ‘ 𝑅 ) ‘ ( ( *rf ‘ 𝑅 ) ‘ 𝑋 ) ) = 𝑋 )
16	9 12 15	3eqtr3d	⊢ ( ( 𝑅 ∈ *-Ring ∧ 𝑋 ∈ 𝐵 ) → ( ( *rf ‘ 𝑅 ) ‘ ( ∗ ‘ 𝑋 ) ) = 𝑋 )
17	6 16	eqtr3d	⊢ ( ( 𝑅 ∈ *-Ring ∧ 𝑋 ∈ 𝐵 ) → ( ∗ ‘ ( ∗ ‘ 𝑋 ) ) = 𝑋 )