evpmodpmf1o

Description: The function for performing an even permutation after a fixed odd permutation is one to one onto all odd permutations. (Contributed by SO, 9-Jul-2018)

	Ref	Expression
Hypotheses	evpmodpmf1o.s	$⊢ S = SymGrp (D)$
	evpmodpmf1o.p	$⊢ P = {Base}_{S}$
Assertion	evpmodpmf1o	$⊢ (D \in Fin \land F \in (P ∖ pmEven (D))) \to (f \in pmEven (D) ⟼ F +_{S} f) : pmEven (D) \underset{1-1 onto}{⟶} P ∖ pmEven (D)$

Proof

Step	Hyp	Ref	Expression
1		evpmodpmf1o.s	$⊢ S = SymGrp (D)$
2		evpmodpmf1o.p	$⊢ P = {Base}_{S}$
3		simpll	$⊢ ((D \in Fin \land F \in (P ∖ pmEven (D))) \land f \in pmEven (D)) \to D \in Fin$
4	1	symggrp	$⊢ D \in Fin \to S \in Grp$
5	4	ad2antrr	$⊢ ((D \in Fin \land F \in (P ∖ pmEven (D))) \land f \in pmEven (D)) \to S \in Grp$
6		eldifi	$⊢ F \in (P ∖ pmEven (D)) \to F \in P$
7	6	ad2antlr	$⊢ ((D \in Fin \land F \in (P ∖ pmEven (D))) \land f \in pmEven (D)) \to F \in P$
8	1 2	evpmss	$⊢ pmEven (D) \subseteq P$
9	8	sseli	$⊢ f \in pmEven (D) \to f \in P$
10	9	adantl	$⊢ ((D \in Fin \land F \in (P ∖ pmEven (D))) \land f \in pmEven (D)) \to f \in P$
11		eqid	$⊢ +_{S} = +_{S}$
12	2 11	grpcl	$⊢ (S \in Grp \land F \in P \land f \in P) \to F +_{S} f \in P$
13	5 7 10 12	syl3anc	$⊢ ((D \in Fin \land F \in (P ∖ pmEven (D))) \land f \in pmEven (D)) \to F +_{S} f \in P$
14		eqid	$⊢ pmSgn (D) = pmSgn (D)$
15		eqid	$⊢ {mulGrp}_{ℂ_{fld}} ↾_{𝑠} \{1, - 1\} = {mulGrp}_{ℂ_{fld}} ↾_{𝑠} \{1, - 1\}$
16	1 14 15	psgnghm2	$⊢ D \in Fin \to pmSgn (D) \in (S GrpHom ({mulGrp}_{ℂ_{fld}} ↾_{𝑠} \{1, - 1\}))$
17	16	ad2antrr	$⊢ ((D \in Fin \land F \in (P ∖ pmEven (D))) \land f \in pmEven (D)) \to pmSgn (D) \in (S GrpHom ({mulGrp}_{ℂ_{fld}} ↾_{𝑠} \{1, - 1\}))$
18		prex	$⊢ \{1, - 1\} \in V$
19		eqid	$⊢ {mulGrp}_{ℂ_{fld}} = {mulGrp}_{ℂ_{fld}}$
20		cnfldmul	$⊢ \times = \cdot_{ℂ_{fld}}$
21	19 20	mgpplusg	$⊢ \times = +_{{mulGrp}_{ℂ_{fld}}}$
22	15 21	ressplusg	$⊢ \{1, - 1\} \in V \to \times = +_{({mulGrp}_{ℂ_{fld}} ↾_{𝑠} \{1, - 1\})}$
23	18 22	ax-mp	$⊢ \times = +_{({mulGrp}_{ℂ_{fld}} ↾_{𝑠} \{1, - 1\})}$
24	2 11 23	ghmlin	$⊢ (pmSgn (D) \in (S GrpHom ({mulGrp}_{ℂ_{fld}} ↾_{𝑠} \{1, - 1\})) \land F \in P \land f \in P) \to pmSgn (D) (F +_{S} f) = pmSgn (D) (F) pmSgn (D) (f)$
25	17 7 10 24	syl3anc	$⊢ ((D \in Fin \land F \in (P ∖ pmEven (D))) \land f \in pmEven (D)) \to pmSgn (D) (F +_{S} f) = pmSgn (D) (F) pmSgn (D) (f)$
26	1 2 14	psgnodpm	$⊢ (D \in Fin \land F \in (P ∖ pmEven (D))) \to pmSgn (D) (F) = - 1$
27	26	adantr	$⊢ ((D \in Fin \land F \in (P ∖ pmEven (D))) \land f \in pmEven (D)) \to pmSgn (D) (F) = - 1$
28	1 2 14	psgnevpm	$⊢ (D \in Fin \land f \in pmEven (D)) \to pmSgn (D) (f) = 1$
29	28	adantlr	$⊢ ((D \in Fin \land F \in (P ∖ pmEven (D))) \land f \in pmEven (D)) \to pmSgn (D) (f) = 1$
30	27 29	oveq12d	$⊢ ((D \in Fin \land F \in (P ∖ pmEven (D))) \land f \in pmEven (D)) \to pmSgn (D) (F) pmSgn (D) (f) = -1 \cdot 1$
31		ax-1cn	$⊢ 1 \in ℂ$
32	31	mulm1i	$⊢ -1 \cdot 1 = - 1$
33	30 32	eqtrdi	$⊢ ((D \in Fin \land F \in (P ∖ pmEven (D))) \land f \in pmEven (D)) \to pmSgn (D) (F) pmSgn (D) (f) = - 1$
34	25 33	eqtrd	$⊢ ((D \in Fin \land F \in (P ∖ pmEven (D))) \land f \in pmEven (D)) \to pmSgn (D) (F +_{S} f) = - 1$
35	1 2 14	psgnodpmr	$⊢ (D \in Fin \land F +_{S} f \in P \land pmSgn (D) (F +_{S} f) = - 1) \to F +_{S} f \in (P ∖ pmEven (D))$
36	3 13 34 35	syl3anc	$⊢ ((D \in Fin \land F \in (P ∖ pmEven (D))) \land f \in pmEven (D)) \to F +_{S} f \in (P ∖ pmEven (D))$
37	36	fmpttd	$⊢ (D \in Fin \land F \in (P ∖ pmEven (D))) \to (f \in pmEven (D) ⟼ F +_{S} f) : pmEven (D) ⟶ P ∖ pmEven (D)$
38	4	ad2antrr	$⊢ ((D \in Fin \land F \in (P ∖ pmEven (D))) \land g \in (P ∖ pmEven (D))) \to S \in Grp$
39		eqid	$⊢ {inv}_{g} (S) = {inv}_{g} (S)$
40	2 39	grpinvcl	$⊢ (S \in Grp \land F \in P) \to {inv}_{g} (S) (F) \in P$
41	4 6 40	syl2an	$⊢ (D \in Fin \land F \in (P ∖ pmEven (D))) \to {inv}_{g} (S) (F) \in P$
42	41	adantr	$⊢ ((D \in Fin \land F \in (P ∖ pmEven (D))) \land g \in (P ∖ pmEven (D))) \to {inv}_{g} (S) (F) \in P$
43		eldifi	$⊢ g \in (P ∖ pmEven (D)) \to g \in P$
44	43	adantl	$⊢ ((D \in Fin \land F \in (P ∖ pmEven (D))) \land g \in (P ∖ pmEven (D))) \to g \in P$
45	2 11	grpcl	$⊢ (S \in Grp \land {inv}_{g} (S) (F) \in P \land g \in P) \to {inv}_{g} (S) (F) +_{S} g \in P$
46	38 42 44 45	syl3anc	$⊢ ((D \in Fin \land F \in (P ∖ pmEven (D))) \land g \in (P ∖ pmEven (D))) \to {inv}_{g} (S) (F) +_{S} g \in P$
47	16	ad2antrr	$⊢ ((D \in Fin \land F \in (P ∖ pmEven (D))) \land g \in (P ∖ pmEven (D))) \to pmSgn (D) \in (S GrpHom ({mulGrp}_{ℂ_{fld}} ↾_{𝑠} \{1, - 1\}))$
48	2 11 23	ghmlin	$⊢ (pmSgn (D) \in (S GrpHom ({mulGrp}_{ℂ_{fld}} ↾_{𝑠} \{1, - 1\})) \land {inv}_{g} (S) (F) \in P \land g \in P) \to pmSgn (D) ({inv}_{g} (S) (F) +_{S} g) = pmSgn (D) ({inv}_{g} (S) (F)) pmSgn (D) (g)$
49	47 42 44 48	syl3anc	$⊢ ((D \in Fin \land F \in (P ∖ pmEven (D))) \land g \in (P ∖ pmEven (D))) \to pmSgn (D) ({inv}_{g} (S) (F) +_{S} g) = pmSgn (D) ({inv}_{g} (S) (F)) pmSgn (D) (g)$
50	1 2 39	symginv	$⊢ F \in P \to {inv}_{g} (S) (F) = F^{-1}$
51	6 50	syl	$⊢ F \in (P ∖ pmEven (D)) \to {inv}_{g} (S) (F) = F^{-1}$
52	51	ad2antlr	$⊢ ((D \in Fin \land F \in (P ∖ pmEven (D))) \land g \in (P ∖ pmEven (D))) \to {inv}_{g} (S) (F) = F^{-1}$
53	52	fveq2d	$⊢ ((D \in Fin \land F \in (P ∖ pmEven (D))) \land g \in (P ∖ pmEven (D))) \to pmSgn (D) ({inv}_{g} (S) (F)) = pmSgn (D) (F^{-1})$
54	1 2 14	psgnodpm	$⊢ (D \in Fin \land g \in (P ∖ pmEven (D))) \to pmSgn (D) (g) = - 1$
55	54	adantlr	$⊢ ((D \in Fin \land F \in (P ∖ pmEven (D))) \land g \in (P ∖ pmEven (D))) \to pmSgn (D) (g) = - 1$
56	53 55	oveq12d	$⊢ ((D \in Fin \land F \in (P ∖ pmEven (D))) \land g \in (P ∖ pmEven (D))) \to pmSgn (D) ({inv}_{g} (S) (F)) pmSgn (D) (g) = pmSgn (D) (F^{-1}) -1$
57		simpll	$⊢ ((D \in Fin \land F \in (P ∖ pmEven (D))) \land g \in (P ∖ pmEven (D))) \to D \in Fin$
58	6	ad2antlr	$⊢ ((D \in Fin \land F \in (P ∖ pmEven (D))) \land g \in (P ∖ pmEven (D))) \to F \in P$
59	1 14 2	psgninv	$⊢ (D \in Fin \land F \in P) \to pmSgn (D) (F^{-1}) = pmSgn (D) (F)$
60	57 58 59	syl2anc	$⊢ ((D \in Fin \land F \in (P ∖ pmEven (D))) \land g \in (P ∖ pmEven (D))) \to pmSgn (D) (F^{-1}) = pmSgn (D) (F)$
61	26	adantr	$⊢ ((D \in Fin \land F \in (P ∖ pmEven (D))) \land g \in (P ∖ pmEven (D))) \to pmSgn (D) (F) = - 1$
62	60 61	eqtrd	$⊢ ((D \in Fin \land F \in (P ∖ pmEven (D))) \land g \in (P ∖ pmEven (D))) \to pmSgn (D) (F^{-1}) = - 1$
63	62	oveq1d	$⊢ ((D \in Fin \land F \in (P ∖ pmEven (D))) \land g \in (P ∖ pmEven (D))) \to pmSgn (D) (F^{-1}) -1 = -1 -1$
64		neg1mulneg1e1	$⊢ -1 -1 = 1$
65	63 64	eqtrdi	$⊢ ((D \in Fin \land F \in (P ∖ pmEven (D))) \land g \in (P ∖ pmEven (D))) \to pmSgn (D) (F^{-1}) -1 = 1$
66	49 56 65	3eqtrd	$⊢ ((D \in Fin \land F \in (P ∖ pmEven (D))) \land g \in (P ∖ pmEven (D))) \to pmSgn (D) ({inv}_{g} (S) (F) +_{S} g) = 1$
67	1 2 14	psgnevpmb	$⊢ D \in Fin \to ({inv}_{g} (S) (F) +_{S} g \in pmEven (D) \leftrightarrow ({inv}_{g} (S) (F) +_{S} g \in P \land pmSgn (D) ({inv}_{g} (S) (F) +_{S} g) = 1))$
68	67	ad2antrr	$⊢ ((D \in Fin \land F \in (P ∖ pmEven (D))) \land g \in (P ∖ pmEven (D))) \to ({inv}_{g} (S) (F) +_{S} g \in pmEven (D) \leftrightarrow ({inv}_{g} (S) (F) +_{S} g \in P \land pmSgn (D) ({inv}_{g} (S) (F) +_{S} g) = 1))$
69	46 66 68	mpbir2and	$⊢ ((D \in Fin \land F \in (P ∖ pmEven (D))) \land g \in (P ∖ pmEven (D))) \to {inv}_{g} (S) (F) +_{S} g \in pmEven (D)$
70	69	fmpttd	$⊢ (D \in Fin \land F \in (P ∖ pmEven (D))) \to (g \in (P ∖ pmEven (D)) ⟼ {inv}_{g} (S) (F) +_{S} g) : P ∖ pmEven (D) ⟶ pmEven (D)$
71		eqidd	$⊢ (D \in Fin \land F \in (P ∖ pmEven (D))) \to (f \in pmEven (D) ⟼ F +_{S} f) = (f \in pmEven (D) ⟼ F +_{S} f)$
72		eqidd	$⊢ (D \in Fin \land F \in (P ∖ pmEven (D))) \to (g \in (P ∖ pmEven (D)) ⟼ {inv}_{g} (S) (F) +_{S} g) = (g \in (P ∖ pmEven (D)) ⟼ {inv}_{g} (S) (F) +_{S} g)$
73		oveq2	$⊢ g = F +_{S} f \to {inv}_{g} (S) (F) +_{S} g = {inv}_{g} (S) (F) +_{S} (F +_{S} f)$
74	36 71 72 73	fmptco	$⊢ (D \in Fin \land F \in (P ∖ pmEven (D))) \to (g \in (P ∖ pmEven (D)) ⟼ {inv}_{g} (S) (F) +_{S} g) \circ (f \in pmEven (D) ⟼ F +_{S} f) = (f \in pmEven (D) ⟼ {inv}_{g} (S) (F) +_{S} (F +_{S} f))$
75		eqid	$⊢ 0_{S} = 0_{S}$
76	2 11 75 39	grplinv	$⊢ (S \in Grp \land F \in P) \to {inv}_{g} (S) (F) +_{S} F = 0_{S}$
77	5 7 76	syl2anc	$⊢ ((D \in Fin \land F \in (P ∖ pmEven (D))) \land f \in pmEven (D)) \to {inv}_{g} (S) (F) +_{S} F = 0_{S}$
78	77	oveq1d	$⊢ ((D \in Fin \land F \in (P ∖ pmEven (D))) \land f \in pmEven (D)) \to ({inv}_{g} (S) (F) +_{S} F) +_{S} f = 0_{S} +_{S} f$
79	41	adantr	$⊢ ((D \in Fin \land F \in (P ∖ pmEven (D))) \land f \in pmEven (D)) \to {inv}_{g} (S) (F) \in P$
80	2 11	grpass	$⊢ (S \in Grp \land ({inv}_{g} (S) (F) \in P \land F \in P \land f \in P)) \to ({inv}_{g} (S) (F) +_{S} F) +_{S} f = {inv}_{g} (S) (F) +_{S} (F +_{S} f)$
81	5 79 7 10 80	syl13anc	$⊢ ((D \in Fin \land F \in (P ∖ pmEven (D))) \land f \in pmEven (D)) \to ({inv}_{g} (S) (F) +_{S} F) +_{S} f = {inv}_{g} (S) (F) +_{S} (F +_{S} f)$
82	2 11 75	grplid	$⊢ (S \in Grp \land f \in P) \to 0_{S} +_{S} f = f$
83	5 10 82	syl2anc	$⊢ ((D \in Fin \land F \in (P ∖ pmEven (D))) \land f \in pmEven (D)) \to 0_{S} +_{S} f = f$
84	78 81 83	3eqtr3d	$⊢ ((D \in Fin \land F \in (P ∖ pmEven (D))) \land f \in pmEven (D)) \to {inv}_{g} (S) (F) +_{S} (F +_{S} f) = f$
85	84	mpteq2dva	$⊢ (D \in Fin \land F \in (P ∖ pmEven (D))) \to (f \in pmEven (D) ⟼ {inv}_{g} (S) (F) +_{S} (F +_{S} f)) = (f \in pmEven (D) ⟼ f)$
86	74 85	eqtrd	$⊢ (D \in Fin \land F \in (P ∖ pmEven (D))) \to (g \in (P ∖ pmEven (D)) ⟼ {inv}_{g} (S) (F) +_{S} g) \circ (f \in pmEven (D) ⟼ F +_{S} f) = (f \in pmEven (D) ⟼ f)$
87		mptresid	$⊢ {I ↾}_{pmEven (D)} = (f \in pmEven (D) ⟼ f)$
88	86 87	eqtr4di	$⊢ (D \in Fin \land F \in (P ∖ pmEven (D))) \to (g \in (P ∖ pmEven (D)) ⟼ {inv}_{g} (S) (F) +_{S} g) \circ (f \in pmEven (D) ⟼ F +_{S} f) = {I ↾}_{pmEven (D)}$
89		oveq2	$⊢ f = {inv}_{g} (S) (F) +_{S} g \to F +_{S} f = F +_{S} ({inv}_{g} (S) (F) +_{S} g)$
90	69 72 71 89	fmptco	$⊢ (D \in Fin \land F \in (P ∖ pmEven (D))) \to (f \in pmEven (D) ⟼ F +_{S} f) \circ (g \in (P ∖ pmEven (D)) ⟼ {inv}_{g} (S) (F) +_{S} g) = (g \in (P ∖ pmEven (D)) ⟼ F +_{S} ({inv}_{g} (S) (F) +_{S} g))$
91	2 11 75 39	grprinv	$⊢ (S \in Grp \land F \in P) \to F +_{S} {inv}_{g} (S) (F) = 0_{S}$
92	4 6 91	syl2an	$⊢ (D \in Fin \land F \in (P ∖ pmEven (D))) \to F +_{S} {inv}_{g} (S) (F) = 0_{S}$
93	92	oveq1d	$⊢ (D \in Fin \land F \in (P ∖ pmEven (D))) \to (F +_{S} {inv}_{g} (S) (F)) +_{S} g = 0_{S} +_{S} g$
94	93	adantr	$⊢ ((D \in Fin \land F \in (P ∖ pmEven (D))) \land g \in (P ∖ pmEven (D))) \to (F +_{S} {inv}_{g} (S) (F)) +_{S} g = 0_{S} +_{S} g$
95	2 11	grpass	$⊢ (S \in Grp \land (F \in P \land {inv}_{g} (S) (F) \in P \land g \in P)) \to (F +_{S} {inv}_{g} (S) (F)) +_{S} g = F +_{S} ({inv}_{g} (S) (F) +_{S} g)$
96	38 58 42 44 95	syl13anc	$⊢ ((D \in Fin \land F \in (P ∖ pmEven (D))) \land g \in (P ∖ pmEven (D))) \to (F +_{S} {inv}_{g} (S) (F)) +_{S} g = F +_{S} ({inv}_{g} (S) (F) +_{S} g)$
97	2 11 75	grplid	$⊢ (S \in Grp \land g \in P) \to 0_{S} +_{S} g = g$
98	38 44 97	syl2anc	$⊢ ((D \in Fin \land F \in (P ∖ pmEven (D))) \land g \in (P ∖ pmEven (D))) \to 0_{S} +_{S} g = g$
99	94 96 98	3eqtr3d	$⊢ ((D \in Fin \land F \in (P ∖ pmEven (D))) \land g \in (P ∖ pmEven (D))) \to F +_{S} ({inv}_{g} (S) (F) +_{S} g) = g$
100	99	mpteq2dva	$⊢ (D \in Fin \land F \in (P ∖ pmEven (D))) \to (g \in (P ∖ pmEven (D)) ⟼ F +_{S} ({inv}_{g} (S) (F) +_{S} g)) = (g \in (P ∖ pmEven (D)) ⟼ g)$
101	90 100	eqtrd	$⊢ (D \in Fin \land F \in (P ∖ pmEven (D))) \to (f \in pmEven (D) ⟼ F +_{S} f) \circ (g \in (P ∖ pmEven (D)) ⟼ {inv}_{g} (S) (F) +_{S} g) = (g \in (P ∖ pmEven (D)) ⟼ g)$
102		mptresid	$⊢ {I ↾}_{(P ∖ pmEven (D))} = (g \in (P ∖ pmEven (D)) ⟼ g)$
103	101 102	eqtr4di	$⊢ (D \in Fin \land F \in (P ∖ pmEven (D))) \to (f \in pmEven (D) ⟼ F +_{S} f) \circ (g \in (P ∖ pmEven (D)) ⟼ {inv}_{g} (S) (F) +_{S} g) = {I ↾}_{(P ∖ pmEven (D))}$
104	37 70 88 103	fcof1od	$⊢ (D \in Fin \land F \in (P ∖ pmEven (D))) \to (f \in pmEven (D) ⟼ F +_{S} f) : pmEven (D) \underset{1-1 onto}{⟶} P ∖ pmEven (D)$

Metamath Proof Explorer

Theorem evpmodpmf1o

Proof