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 ⊢ 𝑆 = ( SymGrp ‘ 𝐷 )
odpmco.b ⊢ 𝐵 = ( Base ‘ 𝑆 )
odpmco.a ⊢ 𝐴 = ( pmEven ‘ 𝐷 )
Assertion odpmco ( ( 𝐷 ∈ Fin ∧ 𝑋 ∈ ( 𝐵 ∖ 𝐴 ) ∧ 𝑌 ∈ ( 𝐵 ∖ 𝐴 ) ) → ( 𝑋 ∘ 𝑌 ) ∈ 𝐴 )

Proof

Step Hyp Ref Expression
1 odpmco.s ⊢ 𝑆 = ( SymGrp ‘ 𝐷 )
2 odpmco.b ⊢ 𝐵 = ( Base ‘ 𝑆 )
3 odpmco.a ⊢ 𝐴 = ( pmEven ‘ 𝐷 )
4 simp1 ⊢ ( ( 𝐷 ∈ Fin ∧ 𝑋 ∈ ( 𝐵 ∖ 𝐴 ) ∧ 𝑌 ∈ ( 𝐵 ∖ 𝐴 ) ) → 𝐷 ∈ Fin )
5 simp2 ⊢ ( ( 𝐷 ∈ Fin ∧ 𝑋 ∈ ( 𝐵 ∖ 𝐴 ) ∧ 𝑌 ∈ ( 𝐵 ∖ 𝐴 ) ) → 𝑋 ∈ ( 𝐵 ∖ 𝐴 ) )
6 5 eldifad ⊢ ( ( 𝐷 ∈ Fin ∧ 𝑋 ∈ ( 𝐵 ∖ 𝐴 ) ∧ 𝑌 ∈ ( 𝐵 ∖ 𝐴 ) ) → 𝑋 ∈ 𝐵 )
7 simp3 ⊢ ( ( 𝐷 ∈ Fin ∧ 𝑋 ∈ ( 𝐵 ∖ 𝐴 ) ∧ 𝑌 ∈ ( 𝐵 ∖ 𝐴 ) ) → 𝑌 ∈ ( 𝐵 ∖ 𝐴 ) )
8 7 eldifad ⊢ ( ( 𝐷 ∈ Fin ∧ 𝑋 ∈ ( 𝐵 ∖ 𝐴 ) ∧ 𝑌 ∈ ( 𝐵 ∖ 𝐴 ) ) → 𝑌 ∈ 𝐵 )
9 eqid ⊢ ( +g ‘ 𝑆 ) = ( +g ‘ 𝑆 )
10 1 2 9 symgov ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ( +g ‘ 𝑆 ) 𝑌 ) = ( 𝑋 ∘ 𝑌 ) )
11 6 8 10 syl2anc ⊢ ( ( 𝐷 ∈ Fin ∧ 𝑋 ∈ ( 𝐵 ∖ 𝐴 ) ∧ 𝑌 ∈ ( 𝐵 ∖ 𝐴 ) ) → ( 𝑋 ( +g ‘ 𝑆 ) 𝑌 ) = ( 𝑋 ∘ 𝑌 ) )
12 1 2 9 symgcl ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ( +g ‘ 𝑆 ) 𝑌 ) ∈ 𝐵 )
13 6 8 12 syl2anc ⊢ ( ( 𝐷 ∈ Fin ∧ 𝑋 ∈ ( 𝐵 ∖ 𝐴 ) ∧ 𝑌 ∈ ( 𝐵 ∖ 𝐴 ) ) → ( 𝑋 ( +g ‘ 𝑆 ) 𝑌 ) ∈ 𝐵 )
14 11 13 eqeltrrd ⊢ ( ( 𝐷 ∈ Fin ∧ 𝑋 ∈ ( 𝐵 ∖ 𝐴 ) ∧ 𝑌 ∈ ( 𝐵 ∖ 𝐴 ) ) → ( 𝑋 ∘ 𝑌 ) ∈ 𝐵 )
15 eqid ⊢ ( pmSgn ‘ 𝐷 ) = ( pmSgn ‘ 𝐷 )
16 1 15 2 psgnco ⊢ ( ( 𝐷 ∈ Fin ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( pmSgn ‘ 𝐷 ) ‘ ( 𝑋 ∘ 𝑌 ) ) = ( ( ( pmSgn ‘ 𝐷 ) ‘ 𝑋 ) · ( ( pmSgn ‘ 𝐷 ) ‘ 𝑌 ) ) )
17 4 6 8 16 syl3anc ⊢ ( ( 𝐷 ∈ Fin ∧ 𝑋 ∈ ( 𝐵 ∖ 𝐴 ) ∧ 𝑌 ∈ ( 𝐵 ∖ 𝐴 ) ) → ( ( pmSgn ‘ 𝐷 ) ‘ ( 𝑋 ∘ 𝑌 ) ) = ( ( ( pmSgn ‘ 𝐷 ) ‘ 𝑋 ) · ( ( pmSgn ‘ 𝐷 ) ‘ 𝑌 ) ) )
18 3 a1i ⊢ ( ( 𝐷 ∈ Fin ∧ 𝑋 ∈ ( 𝐵 ∖ 𝐴 ) ∧ 𝑌 ∈ ( 𝐵 ∖ 𝐴 ) ) → 𝐴 = ( pmEven ‘ 𝐷 ) )
19 18 difeq2d ⊢ ( ( 𝐷 ∈ Fin ∧ 𝑋 ∈ ( 𝐵 ∖ 𝐴 ) ∧ 𝑌 ∈ ( 𝐵 ∖ 𝐴 ) ) → ( 𝐵 ∖ 𝐴 ) = ( 𝐵 ∖ ( pmEven ‘ 𝐷 ) ) )
20 5 19 eleqtrd ⊢ ( ( 𝐷 ∈ Fin ∧ 𝑋 ∈ ( 𝐵 ∖ 𝐴 ) ∧ 𝑌 ∈ ( 𝐵 ∖ 𝐴 ) ) → 𝑋 ∈ ( 𝐵 ∖ ( pmEven ‘ 𝐷 ) ) )
21 1 2 15 psgnodpm ⊢ ( ( 𝐷 ∈ Fin ∧ 𝑋 ∈ ( 𝐵 ∖ ( pmEven ‘ 𝐷 ) ) ) → ( ( pmSgn ‘ 𝐷 ) ‘ 𝑋 ) = - 1 )
22 4 20 21 syl2anc ⊢ ( ( 𝐷 ∈ Fin ∧ 𝑋 ∈ ( 𝐵 ∖ 𝐴 ) ∧ 𝑌 ∈ ( 𝐵 ∖ 𝐴 ) ) → ( ( pmSgn ‘ 𝐷 ) ‘ 𝑋 ) = - 1 )
23 7 19 eleqtrd ⊢ ( ( 𝐷 ∈ Fin ∧ 𝑋 ∈ ( 𝐵 ∖ 𝐴 ) ∧ 𝑌 ∈ ( 𝐵 ∖ 𝐴 ) ) → 𝑌 ∈ ( 𝐵 ∖ ( pmEven ‘ 𝐷 ) ) )
24 1 2 15 psgnodpm ⊢ ( ( 𝐷 ∈ Fin ∧ 𝑌 ∈ ( 𝐵 ∖ ( pmEven ‘ 𝐷 ) ) ) → ( ( pmSgn ‘ 𝐷 ) ‘ 𝑌 ) = - 1 )
25 4 23 24 syl2anc ⊢ ( ( 𝐷 ∈ Fin ∧ 𝑋 ∈ ( 𝐵 ∖ 𝐴 ) ∧ 𝑌 ∈ ( 𝐵 ∖ 𝐴 ) ) → ( ( pmSgn ‘ 𝐷 ) ‘ 𝑌 ) = - 1 )
26 22 25 oveq12d ⊢ ( ( 𝐷 ∈ Fin ∧ 𝑋 ∈ ( 𝐵 ∖ 𝐴 ) ∧ 𝑌 ∈ ( 𝐵 ∖ 𝐴 ) ) → ( ( ( pmSgn ‘ 𝐷 ) ‘ 𝑋 ) · ( ( pmSgn ‘ 𝐷 ) ‘ 𝑌 ) ) = ( - 1 · - 1 ) )
27 neg1mulneg1e1 ⊢ ( - 1 · - 1 ) = 1
28 26 27 eqtrdi ⊢ ( ( 𝐷 ∈ Fin ∧ 𝑋 ∈ ( 𝐵 ∖ 𝐴 ) ∧ 𝑌 ∈ ( 𝐵 ∖ 𝐴 ) ) → ( ( ( pmSgn ‘ 𝐷 ) ‘ 𝑋 ) · ( ( pmSgn ‘ 𝐷 ) ‘ 𝑌 ) ) = 1 )
29 17 28 eqtrd ⊢ ( ( 𝐷 ∈ Fin ∧ 𝑋 ∈ ( 𝐵 ∖ 𝐴 ) ∧ 𝑌 ∈ ( 𝐵 ∖ 𝐴 ) ) → ( ( pmSgn ‘ 𝐷 ) ‘ ( 𝑋 ∘ 𝑌 ) ) = 1 )
30 1 2 15 psgnevpmb ⊢ ( 𝐷 ∈ Fin → ( ( 𝑋 ∘ 𝑌 ) ∈ ( pmEven ‘ 𝐷 ) ↔ ( ( 𝑋 ∘ 𝑌 ) ∈ 𝐵 ∧ ( ( pmSgn ‘ 𝐷 ) ‘ ( 𝑋 ∘ 𝑌 ) ) = 1 ) ) )
31 30 biimpar ⊢ ( ( 𝐷 ∈ Fin ∧ ( ( 𝑋 ∘ 𝑌 ) ∈ 𝐵 ∧ ( ( pmSgn ‘ 𝐷 ) ‘ ( 𝑋 ∘ 𝑌 ) ) = 1 ) ) → ( 𝑋 ∘ 𝑌 ) ∈ ( pmEven ‘ 𝐷 ) )
32 4 14 29 31 syl12anc ⊢ ( ( 𝐷 ∈ Fin ∧ 𝑋 ∈ ( 𝐵 ∖ 𝐴 ) ∧ 𝑌 ∈ ( 𝐵 ∖ 𝐴 ) ) → ( 𝑋 ∘ 𝑌 ) ∈ ( pmEven ‘ 𝐷 ) )
33 32 3 eleqtrrdi ⊢ ( ( 𝐷 ∈ Fin ∧ 𝑋 ∈ ( 𝐵 ∖ 𝐴 ) ∧ 𝑌 ∈ ( 𝐵 ∖ 𝐴 ) ) → ( 𝑋 ∘ 𝑌 ) ∈ 𝐴 )