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 = ( SymGrp ` D )
odpmco.b 
|- B = ( Base ` S )
odpmco.a 
|- A = ( pmEven ` D )
Assertion odpmco 
|- ( ( D e. Fin /\ X e. ( B \ A ) /\ Y e. ( B \ A ) ) -> ( X o. Y ) e. A )

Proof

Step Hyp Ref Expression
1 odpmco.s 
 |-  S = ( SymGrp ` D )
2 odpmco.b 
 |-  B = ( Base ` S )
3 odpmco.a 
 |-  A = ( pmEven ` D )
4 simp1 
 |-  ( ( D e. Fin /\ X e. ( B \ A ) /\ Y e. ( B \ A ) ) -> D e. Fin )
5 simp2 
 |-  ( ( D e. Fin /\ X e. ( B \ A ) /\ Y e. ( B \ A ) ) -> X e. ( B \ A ) )
6 5 eldifad 
 |-  ( ( D e. Fin /\ X e. ( B \ A ) /\ Y e. ( B \ A ) ) -> X e. B )
7 simp3 
 |-  ( ( D e. Fin /\ X e. ( B \ A ) /\ Y e. ( B \ A ) ) -> Y e. ( B \ A ) )
8 7 eldifad 
 |-  ( ( D e. Fin /\ X e. ( B \ A ) /\ Y e. ( B \ A ) ) -> Y e. B )
9 eqid 
 |-  ( +g ` S ) = ( +g ` S )
10 1 2 9 symgov 
 |-  ( ( X e. B /\ Y e. B ) -> ( X ( +g ` S ) Y ) = ( X o. Y ) )
11 6 8 10 syl2anc 
 |-  ( ( D e. Fin /\ X e. ( B \ A ) /\ Y e. ( B \ A ) ) -> ( X ( +g ` S ) Y ) = ( X o. Y ) )
12 1 2 9 symgcl 
 |-  ( ( X e. B /\ Y e. B ) -> ( X ( +g ` S ) Y ) e. B )
13 6 8 12 syl2anc 
 |-  ( ( D e. Fin /\ X e. ( B \ A ) /\ Y e. ( B \ A ) ) -> ( X ( +g ` S ) Y ) e. B )
14 11 13 eqeltrrd 
 |-  ( ( D e. Fin /\ X e. ( B \ A ) /\ Y e. ( B \ A ) ) -> ( X o. Y ) e. B )
15 eqid 
 |-  ( pmSgn ` D ) = ( pmSgn ` D )
16 1 15 2 psgnco 
 |-  ( ( D e. Fin /\ X e. B /\ Y e. B ) -> ( ( pmSgn ` D ) ` ( X o. Y ) ) = ( ( ( pmSgn ` D ) ` X ) x. ( ( pmSgn ` D ) ` Y ) ) )
17 4 6 8 16 syl3anc 
 |-  ( ( D e. Fin /\ X e. ( B \ A ) /\ Y e. ( B \ A ) ) -> ( ( pmSgn ` D ) ` ( X o. Y ) ) = ( ( ( pmSgn ` D ) ` X ) x. ( ( pmSgn ` D ) ` Y ) ) )
18 3 a1i 
 |-  ( ( D e. Fin /\ X e. ( B \ A ) /\ Y e. ( B \ A ) ) -> A = ( pmEven ` D ) )
19 18 difeq2d 
 |-  ( ( D e. Fin /\ X e. ( B \ A ) /\ Y e. ( B \ A ) ) -> ( B \ A ) = ( B \ ( pmEven ` D ) ) )
20 5 19 eleqtrd 
 |-  ( ( D e. Fin /\ X e. ( B \ A ) /\ Y e. ( B \ A ) ) -> X e. ( B \ ( pmEven ` D ) ) )
21 1 2 15 psgnodpm 
 |-  ( ( D e. Fin /\ X e. ( B \ ( pmEven ` D ) ) ) -> ( ( pmSgn ` D ) ` X ) = -u 1 )
22 4 20 21 syl2anc 
 |-  ( ( D e. Fin /\ X e. ( B \ A ) /\ Y e. ( B \ A ) ) -> ( ( pmSgn ` D ) ` X ) = -u 1 )
23 7 19 eleqtrd 
 |-  ( ( D e. Fin /\ X e. ( B \ A ) /\ Y e. ( B \ A ) ) -> Y e. ( B \ ( pmEven ` D ) ) )
24 1 2 15 psgnodpm 
 |-  ( ( D e. Fin /\ Y e. ( B \ ( pmEven ` D ) ) ) -> ( ( pmSgn ` D ) ` Y ) = -u 1 )
25 4 23 24 syl2anc 
 |-  ( ( D e. Fin /\ X e. ( B \ A ) /\ Y e. ( B \ A ) ) -> ( ( pmSgn ` D ) ` Y ) = -u 1 )
26 22 25 oveq12d 
 |-  ( ( D e. Fin /\ X e. ( B \ A ) /\ Y e. ( B \ A ) ) -> ( ( ( pmSgn ` D ) ` X ) x. ( ( pmSgn ` D ) ` Y ) ) = ( -u 1 x. -u 1 ) )
27 neg1mulneg1e1 
 |-  ( -u 1 x. -u 1 ) = 1
28 26 27 eqtrdi 
 |-  ( ( D e. Fin /\ X e. ( B \ A ) /\ Y e. ( B \ A ) ) -> ( ( ( pmSgn ` D ) ` X ) x. ( ( pmSgn ` D ) ` Y ) ) = 1 )
29 17 28 eqtrd 
 |-  ( ( D e. Fin /\ X e. ( B \ A ) /\ Y e. ( B \ A ) ) -> ( ( pmSgn ` D ) ` ( X o. Y ) ) = 1 )
30 1 2 15 psgnevpmb 
 |-  ( D e. Fin -> ( ( X o. Y ) e. ( pmEven ` D ) <-> ( ( X o. Y ) e. B /\ ( ( pmSgn ` D ) ` ( X o. Y ) ) = 1 ) ) )
31 30 biimpar 
 |-  ( ( D e. Fin /\ ( ( X o. Y ) e. B /\ ( ( pmSgn ` D ) ` ( X o. Y ) ) = 1 ) ) -> ( X o. Y ) e. ( pmEven ` D ) )
32 4 14 29 31 syl12anc 
 |-  ( ( D e. Fin /\ X e. ( B \ A ) /\ Y e. ( B \ A ) ) -> ( X o. Y ) e. ( pmEven ` D ) )
33 32 3 eleqtrrdi 
 |-  ( ( D e. Fin /\ X e. ( B \ A ) /\ Y e. ( B \ A ) ) -> ( X o. Y ) e. A )