# 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 ${⊢}{B}={\mathrm{Base}}_{{R}}$
Assertion srngnvl

### Proof

Step Hyp Ref Expression
1 srngcl.i
2 srngcl.b ${⊢}{B}={\mathrm{Base}}_{{R}}$
3 1 2 srngcl
4 eqid ${⊢}{\ast }_{\mathrm{𝑟𝑓}}\left({R}\right)={\ast }_{\mathrm{𝑟𝑓}}\left({R}\right)$
5 2 1 4 stafval
6 3 5 syl
7 4 srngcnv ${⊢}{R}\in \mathrm{*-Ring}\to {\ast }_{\mathrm{𝑟𝑓}}\left({R}\right)={{\ast }_{\mathrm{𝑟𝑓}}\left({R}\right)}^{-1}$
8 7 adantr ${⊢}\left({R}\in \mathrm{*-Ring}\wedge {X}\in {B}\right)\to {\ast }_{\mathrm{𝑟𝑓}}\left({R}\right)={{\ast }_{\mathrm{𝑟𝑓}}\left({R}\right)}^{-1}$
9 8 fveq1d ${⊢}\left({R}\in \mathrm{*-Ring}\wedge {X}\in {B}\right)\to {\ast }_{\mathrm{𝑟𝑓}}\left({R}\right)\left({\ast }_{\mathrm{𝑟𝑓}}\left({R}\right)\left({X}\right)\right)={{\ast }_{\mathrm{𝑟𝑓}}\left({R}\right)}^{-1}\left({\ast }_{\mathrm{𝑟𝑓}}\left({R}\right)\left({X}\right)\right)$
10 2 1 4 stafval
11 10 adantl
12 11 fveq2d
13 4 2 srngf1o ${⊢}{R}\in \mathrm{*-Ring}\to {\ast }_{\mathrm{𝑟𝑓}}\left({R}\right):{B}\underset{1-1 onto}{⟶}{B}$
14 f1ocnvfv1 ${⊢}\left({\ast }_{\mathrm{𝑟𝑓}}\left({R}\right):{B}\underset{1-1 onto}{⟶}{B}\wedge {X}\in {B}\right)\to {{\ast }_{\mathrm{𝑟𝑓}}\left({R}\right)}^{-1}\left({\ast }_{\mathrm{𝑟𝑓}}\left({R}\right)\left({X}\right)\right)={X}$
15 13 14 sylan ${⊢}\left({R}\in \mathrm{*-Ring}\wedge {X}\in {B}\right)\to {{\ast }_{\mathrm{𝑟𝑓}}\left({R}\right)}^{-1}\left({\ast }_{\mathrm{𝑟𝑓}}\left({R}\right)\left({X}\right)\right)={X}$
16 9 12 15 3eqtr3d
17 6 16 eqtr3d