Description: The value of the group operation of the symmetric group on A . (Contributed by Paul Chapman, 25-Feb-2008) (Revised by Mario Carneiro, 28-Jan-2015) (Revised by AV, 30-Mar-2024)
Ref | Expression | ||
---|---|---|---|
Hypotheses | symgov.1 | |
|
symgov.2 | |
||
symgov.3 | |
||
Assertion | symgov | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | symgov.1 | |
|
2 | symgov.2 | |
|
3 | symgov.3 | |
|
4 | eqid | |
|
5 | 1 4 3 | symgplusg | |
6 | 5 | a1i | |
7 | simpl | |
|
8 | simpr | |
|
9 | 7 8 | coeq12d | |
10 | 9 | adantl | |
11 | 1 2 | symgbasmap | |
12 | 11 | adantr | |
13 | 1 2 | symgbasmap | |
14 | 13 | adantl | |
15 | coexg | |
|
16 | 6 10 12 14 15 | ovmpod | |