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 | |
||
Assertion | srngnvl | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | srngcl.i | |
|
2 | srngcl.b | |
|
3 | 1 2 | srngcl | |
4 | eqid | |
|
5 | 2 1 4 | stafval | |
6 | 3 5 | syl | |
7 | 4 | srngcnv | |
8 | 7 | adantr | |
9 | 8 | fveq1d | |
10 | 2 1 4 | stafval | |
11 | 10 | adantl | |
12 | 11 | fveq2d | |
13 | 4 2 | srngf1o | |
14 | f1ocnvfv1 | |
|
15 | 13 14 | sylan | |
16 | 9 12 15 | 3eqtr3d | |
17 | 6 16 | eqtr3d | |