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 \in Fin \land X \in (B ∖ A) \land Y \in (B ∖ A)) \to X \circ Y \in 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 \in Fin \land X \in (B ∖ A) \land Y \in (B ∖ A)) \to D \in Fin$
5		simp2	$⊢ (D \in Fin \land X \in (B ∖ A) \land Y \in (B ∖ A)) \to X \in (B ∖ A)$
6	5	eldifad	$⊢ (D \in Fin \land X \in (B ∖ A) \land Y \in (B ∖ A)) \to X \in B$
7		simp3	$⊢ (D \in Fin \land X \in (B ∖ A) \land Y \in (B ∖ A)) \to Y \in (B ∖ A)$
8	7	eldifad	$⊢ (D \in Fin \land X \in (B ∖ A) \land Y \in (B ∖ A)) \to Y \in B$
9		eqid	$⊢ +_{S} = +_{S}$
10	1 2 9	symgov	$⊢ (X \in B \land Y \in B) \to X +_{S} Y = X \circ Y$
11	6 8 10	syl2anc	$⊢ (D \in Fin \land X \in (B ∖ A) \land Y \in (B ∖ A)) \to X +_{S} Y = X \circ Y$
12	1 2 9	symgcl	$⊢ (X \in B \land Y \in B) \to X +_{S} Y \in B$
13	6 8 12	syl2anc	$⊢ (D \in Fin \land X \in (B ∖ A) \land Y \in (B ∖ A)) \to X +_{S} Y \in B$
14	11 13	eqeltrrd	$⊢ (D \in Fin \land X \in (B ∖ A) \land Y \in (B ∖ A)) \to X \circ Y \in B$
15		eqid	$⊢ pmSgn (D) = pmSgn (D)$
16	1 15 2	psgnco	$⊢ (D \in Fin \land X \in B \land Y \in B) \to pmSgn (D) (X \circ Y) = pmSgn (D) (X) pmSgn (D) (Y)$
17	4 6 8 16	syl3anc	$⊢ (D \in Fin \land X \in (B ∖ A) \land Y \in (B ∖ A)) \to pmSgn (D) (X \circ Y) = pmSgn (D) (X) pmSgn (D) (Y)$
18	3	a1i	$⊢ (D \in Fin \land X \in (B ∖ A) \land Y \in (B ∖ A)) \to A = pmEven (D)$
19	18	difeq2d	$⊢ (D \in Fin \land X \in (B ∖ A) \land Y \in (B ∖ A)) \to B ∖ A = B ∖ pmEven (D)$
20	5 19	eleqtrd	$⊢ (D \in Fin \land X \in (B ∖ A) \land Y \in (B ∖ A)) \to X \in (B ∖ pmEven (D))$
21	1 2 15	psgnodpm	$⊢ (D \in Fin \land X \in (B ∖ pmEven (D))) \to pmSgn (D) (X) = - 1$
22	4 20 21	syl2anc	$⊢ (D \in Fin \land X \in (B ∖ A) \land Y \in (B ∖ A)) \to pmSgn (D) (X) = - 1$
23	7 19	eleqtrd	$⊢ (D \in Fin \land X \in (B ∖ A) \land Y \in (B ∖ A)) \to Y \in (B ∖ pmEven (D))$
24	1 2 15	psgnodpm	$⊢ (D \in Fin \land Y \in (B ∖ pmEven (D))) \to pmSgn (D) (Y) = - 1$
25	4 23 24	syl2anc	$⊢ (D \in Fin \land X \in (B ∖ A) \land Y \in (B ∖ A)) \to pmSgn (D) (Y) = - 1$
26	22 25	oveq12d	$⊢ (D \in Fin \land X \in (B ∖ A) \land Y \in (B ∖ A)) \to pmSgn (D) (X) pmSgn (D) (Y) = -1 -1$
27		neg1mulneg1e1	$⊢ -1 -1 = 1$
28	26 27	eqtrdi	$⊢ (D \in Fin \land X \in (B ∖ A) \land Y \in (B ∖ A)) \to pmSgn (D) (X) pmSgn (D) (Y) = 1$
29	17 28	eqtrd	$⊢ (D \in Fin \land X \in (B ∖ A) \land Y \in (B ∖ A)) \to pmSgn (D) (X \circ Y) = 1$
30	1 2 15	psgnevpmb	$⊢ D \in Fin \to (X \circ Y \in pmEven (D) \leftrightarrow (X \circ Y \in B \land pmSgn (D) (X \circ Y) = 1))$
31	30	biimpar	$⊢ (D \in Fin \land (X \circ Y \in B \land pmSgn (D) (X \circ Y) = 1)) \to X \circ Y \in pmEven (D)$
32	4 14 29 31	syl12anc	$⊢ (D \in Fin \land X \in (B ∖ A) \land Y \in (B ∖ A)) \to X \circ Y \in pmEven (D)$
33	32 3	eleqtrrdi	$⊢ (D \in Fin \land X \in (B ∖ A) \land Y \in (B ∖ A)) \to X \circ Y \in A$

Metamath Proof Explorer

Theorem odpmco

Proof