# 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 = ( *𝑟𝑅 )
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 ∧ 𝑋𝐵 ) → ( ‘ ( 𝑋 ) ) = 𝑋 )