Description: The composition of two odd permutations is even. (Contributed by Thierry Arnoux, 15-Oct-2023)
Ref | Expression | ||
---|---|---|---|
Hypotheses | odpmco.s | |
|
odpmco.b | |
||
odpmco.a | |
||
Assertion | odpmco | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | odpmco.s | |
|
2 | odpmco.b | |
|
3 | odpmco.a | |
|
4 | simp1 | |
|
5 | simp2 | |
|
6 | 5 | eldifad | |
7 | simp3 | |
|
8 | 7 | eldifad | |
9 | eqid | |
|
10 | 1 2 9 | symgov | |
11 | 6 8 10 | syl2anc | |
12 | 1 2 9 | symgcl | |
13 | 6 8 12 | syl2anc | |
14 | 11 13 | eqeltrrd | |
15 | eqid | |
|
16 | 1 15 2 | psgnco | |
17 | 4 6 8 16 | syl3anc | |
18 | 3 | a1i | |
19 | 18 | difeq2d | |
20 | 5 19 | eleqtrd | |
21 | 1 2 15 | psgnodpm | |
22 | 4 20 21 | syl2anc | |
23 | 7 19 | eleqtrd | |
24 | 1 2 15 | psgnodpm | |
25 | 4 23 24 | syl2anc | |
26 | 22 25 | oveq12d | |
27 | neg1mulneg1e1 | |
|
28 | 26 27 | eqtrdi | |
29 | 17 28 | eqtrd | |
30 | 1 2 15 | psgnevpmb | |
31 | 30 | biimpar | |
32 | 4 14 29 31 | syl12anc | |
33 | 32 3 | eleqtrrdi | |