Metamath Proof Explorer


Theorem odpmco

Description: The composition of two odd permutations is even. (Contributed by Thierry Arnoux, 15-Oct-2023)

Ref Expression
Hypotheses odpmco.s S=SymGrpD
odpmco.b B=BaseS
odpmco.a A=pmEvenD
Assertion odpmco DFinXBAYBAXYA

Proof

Step Hyp Ref Expression
1 odpmco.s S=SymGrpD
2 odpmco.b B=BaseS
3 odpmco.a A=pmEvenD
4 simp1 DFinXBAYBADFin
5 simp2 DFinXBAYBAXBA
6 5 eldifad DFinXBAYBAXB
7 simp3 DFinXBAYBAYBA
8 7 eldifad DFinXBAYBAYB
9 eqid +S=+S
10 1 2 9 symgov XBYBX+SY=XY
11 6 8 10 syl2anc DFinXBAYBAX+SY=XY
12 1 2 9 symgcl XBYBX+SYB
13 6 8 12 syl2anc DFinXBAYBAX+SYB
14 11 13 eqeltrrd DFinXBAYBAXYB
15 eqid pmSgnD=pmSgnD
16 1 15 2 psgnco DFinXBYBpmSgnDXY=pmSgnDXpmSgnDY
17 4 6 8 16 syl3anc DFinXBAYBApmSgnDXY=pmSgnDXpmSgnDY
18 3 a1i DFinXBAYBAA=pmEvenD
19 18 difeq2d DFinXBAYBABA=BpmEvenD
20 5 19 eleqtrd DFinXBAYBAXBpmEvenD
21 1 2 15 psgnodpm DFinXBpmEvenDpmSgnDX=1
22 4 20 21 syl2anc DFinXBAYBApmSgnDX=1
23 7 19 eleqtrd DFinXBAYBAYBpmEvenD
24 1 2 15 psgnodpm DFinYBpmEvenDpmSgnDY=1
25 4 23 24 syl2anc DFinXBAYBApmSgnDY=1
26 22 25 oveq12d DFinXBAYBApmSgnDXpmSgnDY=-1-1
27 neg1mulneg1e1 -1-1=1
28 26 27 eqtrdi DFinXBAYBApmSgnDXpmSgnDY=1
29 17 28 eqtrd DFinXBAYBApmSgnDXY=1
30 1 2 15 psgnevpmb DFinXYpmEvenDXYBpmSgnDXY=1
31 30 biimpar DFinXYBpmSgnDXY=1XYpmEvenD
32 4 14 29 31 syl12anc DFinXBAYBAXYpmEvenD
33 32 3 eleqtrrdi DFinXBAYBAXYA