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
srngcl.b B=BaseR
Assertion srngnvl R*-RingXB˙˙X=X

Proof

Step Hyp Ref Expression
1 srngcl.i ˙=*R
2 srngcl.b B=BaseR
3 1 2 srngcl R*-RingXB˙XB
4 eqid 𝑟𝑓R=𝑟𝑓R
5 2 1 4 stafval ˙XB𝑟𝑓R˙X=˙˙X
6 3 5 syl R*-RingXB𝑟𝑓R˙X=˙˙X
7 4 srngcnv R*-Ring𝑟𝑓R=𝑟𝑓R-1
8 7 adantr R*-RingXB𝑟𝑓R=𝑟𝑓R-1
9 8 fveq1d R*-RingXB𝑟𝑓R𝑟𝑓RX=𝑟𝑓R-1𝑟𝑓RX
10 2 1 4 stafval XB𝑟𝑓RX=˙X
11 10 adantl R*-RingXB𝑟𝑓RX=˙X
12 11 fveq2d R*-RingXB𝑟𝑓R𝑟𝑓RX=𝑟𝑓R˙X
13 4 2 srngf1o R*-Ring𝑟𝑓R:B1-1 ontoB
14 f1ocnvfv1 𝑟𝑓R:B1-1 ontoBXB𝑟𝑓R-1𝑟𝑓RX=X
15 13 14 sylan R*-RingXB𝑟𝑓R-1𝑟𝑓RX=X
16 9 12 15 3eqtr3d R*-RingXB𝑟𝑓R˙X=X
17 6 16 eqtr3d R*-RingXB˙˙X=X