psgndif

Description: Embedding of permutation signs restricted to a set without a single element into a ring. (Contributed by AV, 31-Jan-2019)

	Ref	Expression
Hypotheses	psgndif.p	$⊢ P = {Base}_{SymGrp (N)}$
	psgndif.s	$⊢ S = pmSgn (N)$
	psgndif.z	$⊢ Z = pmSgn (N ∖ \{K\})$
Assertion	psgndif	$⊢ (N \in Fin \land K \in N) \to (Q \in \{q \in P \| q (K) = K\} \to Z ({Q ↾}_{(N ∖ \{K\})}) = S (Q))$

Proof

Step	Hyp	Ref	Expression
1		psgndif.p	$⊢ P = {Base}_{SymGrp (N)}$
2		psgndif.s	$⊢ S = pmSgn (N)$
3		psgndif.z	$⊢ Z = pmSgn (N ∖ \{K\})$
4		eqid	$⊢ ran pmTrsp (N ∖ \{K\}) = ran pmTrsp (N ∖ \{K\})$
5		eqid	$⊢ SymGrp (N ∖ \{K\}) = SymGrp (N ∖ \{K\})$
6		eqid	$⊢ SymGrp (N) = SymGrp (N)$
7		eqid	$⊢ ran pmTrsp (N) = ran pmTrsp (N)$
8	1 4 5 6 7	psgnfix2	$⊢ (N \in Fin \land K \in N) \to (Q \in \{q \in P \| q (K) = K\} \to \exists r \in Word ran pmTrsp (N) Q = \sum_{SymGrp (N)} r)$
9	8	imp	$⊢ ((N \in Fin \land K \in N) \land Q \in \{q \in P \| q (K) = K\}) \to \exists r \in Word ran pmTrsp (N) Q = \sum_{SymGrp (N)} r$
10	9	ad2antrr	$⊢ ((((N \in Fin \land K \in N) \land Q \in \{q \in P \| q (K) = K\}) \land w \in Word ran pmTrsp (N ∖ \{K\})) \land ({Q ↾}_{(N ∖ \{K\})} = \sum_{SymGrp (N ∖ \{K\})} w \land s = {(- 1)}^{\|w\|})) \to \exists r \in Word ran pmTrsp (N) Q = \sum_{SymGrp (N)} r$
11	1 4 5 6 7	psgndiflemA	$⊢ ((N \in Fin \land K \in N) \land Q \in \{q \in P \| q (K) = K\}) \to ((w \in Word ran pmTrsp (N ∖ \{K\}) \land {Q ↾}_{(N ∖ \{K\})} = \sum_{SymGrp (N ∖ \{K\})} w \land r \in Word ran pmTrsp (N)) \to (Q = \sum_{SymGrp (N)} r \to {(- 1)}^{\|w\|} = {(- 1)}^{\|r\|}))$
12	11	imp	$⊢ (((N \in Fin \land K \in N) \land Q \in \{q \in P \| q (K) = K\}) \land (w \in Word ran pmTrsp (N ∖ \{K\}) \land {Q ↾}_{(N ∖ \{K\})} = \sum_{SymGrp (N ∖ \{K\})} w \land r \in Word ran pmTrsp (N))) \to (Q = \sum_{SymGrp (N)} r \to {(- 1)}^{\|w\|} = {(- 1)}^{\|r\|})$
13	12	3anassrs	$⊢ (((((N \in Fin \land K \in N) \land Q \in \{q \in P \| q (K) = K\}) \land w \in Word ran pmTrsp (N ∖ \{K\})) \land {Q ↾}_{(N ∖ \{K\})} = \sum_{SymGrp (N ∖ \{K\})} w) \land r \in Word ran pmTrsp (N)) \to (Q = \sum_{SymGrp (N)} r \to {(- 1)}^{\|w\|} = {(- 1)}^{\|r\|})$
14	13	adantlrr	$⊢ (((((N \in Fin \land K \in N) \land Q \in \{q \in P \| q (K) = K\}) \land w \in Word ran pmTrsp (N ∖ \{K\})) \land ({Q ↾}_{(N ∖ \{K\})} = \sum_{SymGrp (N ∖ \{K\})} w \land s = {(- 1)}^{\|w\|})) \land r \in Word ran pmTrsp (N)) \to (Q = \sum_{SymGrp (N)} r \to {(- 1)}^{\|w\|} = {(- 1)}^{\|r\|})$
15		eqeq1	$⊢ s = {(- 1)}^{\|w\|} \to (s = {(- 1)}^{\|r\|} \leftrightarrow {(- 1)}^{\|w\|} = {(- 1)}^{\|r\|})$
16	15	ad2antll	$⊢ ((((N \in Fin \land K \in N) \land Q \in \{q \in P \| q (K) = K\}) \land w \in Word ran pmTrsp (N ∖ \{K\})) \land ({Q ↾}_{(N ∖ \{K\})} = \sum_{SymGrp (N ∖ \{K\})} w \land s = {(- 1)}^{\|w\|})) \to (s = {(- 1)}^{\|r\|} \leftrightarrow {(- 1)}^{\|w\|} = {(- 1)}^{\|r\|})$
17	16	adantr	$⊢ (((((N \in Fin \land K \in N) \land Q \in \{q \in P \| q (K) = K\}) \land w \in Word ran pmTrsp (N ∖ \{K\})) \land ({Q ↾}_{(N ∖ \{K\})} = \sum_{SymGrp (N ∖ \{K\})} w \land s = {(- 1)}^{\|w\|})) \land r \in Word ran pmTrsp (N)) \to (s = {(- 1)}^{\|r\|} \leftrightarrow {(- 1)}^{\|w\|} = {(- 1)}^{\|r\|})$
18	14 17	sylibrd	$⊢ (((((N \in Fin \land K \in N) \land Q \in \{q \in P \| q (K) = K\}) \land w \in Word ran pmTrsp (N ∖ \{K\})) \land ({Q ↾}_{(N ∖ \{K\})} = \sum_{SymGrp (N ∖ \{K\})} w \land s = {(- 1)}^{\|w\|})) \land r \in Word ran pmTrsp (N)) \to (Q = \sum_{SymGrp (N)} r \to s = {(- 1)}^{\|r\|})$
19	18	ralrimiva	$⊢ ((((N \in Fin \land K \in N) \land Q \in \{q \in P \| q (K) = K\}) \land w \in Word ran pmTrsp (N ∖ \{K\})) \land ({Q ↾}_{(N ∖ \{K\})} = \sum_{SymGrp (N ∖ \{K\})} w \land s = {(- 1)}^{\|w\|})) \to \forall r \in Word ran pmTrsp (N) (Q = \sum_{SymGrp (N)} r \to s = {(- 1)}^{\|r\|})$
20	10 19	r19.29imd	$⊢ ((((N \in Fin \land K \in N) \land Q \in \{q \in P \| q (K) = K\}) \land w \in Word ran pmTrsp (N ∖ \{K\})) \land ({Q ↾}_{(N ∖ \{K\})} = \sum_{SymGrp (N ∖ \{K\})} w \land s = {(- 1)}^{\|w\|})) \to \exists r \in Word ran pmTrsp (N) (Q = \sum_{SymGrp (N)} r \land s = {(- 1)}^{\|r\|})$
21	20	rexlimdva2	$⊢ ((N \in Fin \land K \in N) \land Q \in \{q \in P \| q (K) = K\}) \to (\exists w \in Word ran pmTrsp (N ∖ \{K\}) ({Q ↾}_{(N ∖ \{K\})} = \sum_{SymGrp (N ∖ \{K\})} w \land s = {(- 1)}^{\|w\|}) \to \exists r \in Word ran pmTrsp (N) (Q = \sum_{SymGrp (N)} r \land s = {(- 1)}^{\|r\|}))$
22	1 4 5	psgnfix1	$⊢ (N \in Fin \land K \in N) \to (Q \in \{q \in P \| q (K) = K\} \to \exists w \in Word ran pmTrsp (N ∖ \{K\}) {Q ↾}_{(N ∖ \{K\})} = \sum_{SymGrp (N ∖ \{K\})} w)$
23	22	imp	$⊢ ((N \in Fin \land K \in N) \land Q \in \{q \in P \| q (K) = K\}) \to \exists w \in Word ran pmTrsp (N ∖ \{K\}) {Q ↾}_{(N ∖ \{K\})} = \sum_{SymGrp (N ∖ \{K\})} w$
24	23	ad2antrr	$⊢ ((((N \in Fin \land K \in N) \land Q \in \{q \in P \| q (K) = K\}) \land r \in Word ran pmTrsp (N)) \land (Q = \sum_{SymGrp (N)} r \land s = {(- 1)}^{\|r\|})) \to \exists w \in Word ran pmTrsp (N ∖ \{K\}) {Q ↾}_{(N ∖ \{K\})} = \sum_{SymGrp (N ∖ \{K\})} w$
25		simp-4l	$⊢ ((((((N \in Fin \land K \in N) \land Q \in \{q \in P \| q (K) = K\}) \land r \in Word ran pmTrsp (N)) \land Q = \sum_{SymGrp (N)} r) \land w \in Word ran pmTrsp (N ∖ \{K\})) \land {Q ↾}_{(N ∖ \{K\})} = \sum_{SymGrp (N ∖ \{K\})} w) \to ((N \in Fin \land K \in N) \land Q \in \{q \in P \| q (K) = K\})$
26		simpr	$⊢ (((((N \in Fin \land K \in N) \land Q \in \{q \in P \| q (K) = K\}) \land r \in Word ran pmTrsp (N)) \land Q = \sum_{SymGrp (N)} r) \land w \in Word ran pmTrsp (N ∖ \{K\})) \to w \in Word ran pmTrsp (N ∖ \{K\})$
27	26	adantr	$⊢ ((((((N \in Fin \land K \in N) \land Q \in \{q \in P \| q (K) = K\}) \land r \in Word ran pmTrsp (N)) \land Q = \sum_{SymGrp (N)} r) \land w \in Word ran pmTrsp (N ∖ \{K\})) \land {Q ↾}_{(N ∖ \{K\})} = \sum_{SymGrp (N ∖ \{K\})} w) \to w \in Word ran pmTrsp (N ∖ \{K\})$
28		simpr	$⊢ ((((((N \in Fin \land K \in N) \land Q \in \{q \in P \| q (K) = K\}) \land r \in Word ran pmTrsp (N)) \land Q = \sum_{SymGrp (N)} r) \land w \in Word ran pmTrsp (N ∖ \{K\})) \land {Q ↾}_{(N ∖ \{K\})} = \sum_{SymGrp (N ∖ \{K\})} w) \to {Q ↾}_{(N ∖ \{K\})} = \sum_{SymGrp (N ∖ \{K\})} w$
29		simp-4r	$⊢ ((((((N \in Fin \land K \in N) \land Q \in \{q \in P \| q (K) = K\}) \land r \in Word ran pmTrsp (N)) \land Q = \sum_{SymGrp (N)} r) \land w \in Word ran pmTrsp (N ∖ \{K\})) \land {Q ↾}_{(N ∖ \{K\})} = \sum_{SymGrp (N ∖ \{K\})} w) \to r \in Word ran pmTrsp (N)$
30	27 28 29	3jca	$⊢ ((((((N \in Fin \land K \in N) \land Q \in \{q \in P \| q (K) = K\}) \land r \in Word ran pmTrsp (N)) \land Q = \sum_{SymGrp (N)} r) \land w \in Word ran pmTrsp (N ∖ \{K\})) \land {Q ↾}_{(N ∖ \{K\})} = \sum_{SymGrp (N ∖ \{K\})} w) \to (w \in Word ran pmTrsp (N ∖ \{K\}) \land {Q ↾}_{(N ∖ \{K\})} = \sum_{SymGrp (N ∖ \{K\})} w \land r \in Word ran pmTrsp (N))$
31		simpr	$⊢ ((((N \in Fin \land K \in N) \land Q \in \{q \in P \| q (K) = K\}) \land r \in Word ran pmTrsp (N)) \land Q = \sum_{SymGrp (N)} r) \to Q = \sum_{SymGrp (N)} r$
32	31	ad2antrr	$⊢ ((((((N \in Fin \land K \in N) \land Q \in \{q \in P \| q (K) = K\}) \land r \in Word ran pmTrsp (N)) \land Q = \sum_{SymGrp (N)} r) \land w \in Word ran pmTrsp (N ∖ \{K\})) \land {Q ↾}_{(N ∖ \{K\})} = \sum_{SymGrp (N ∖ \{K\})} w) \to Q = \sum_{SymGrp (N)} r$
33	25 30 32 11	syl3c	$⊢ ((((((N \in Fin \land K \in N) \land Q \in \{q \in P \| q (K) = K\}) \land r \in Word ran pmTrsp (N)) \land Q = \sum_{SymGrp (N)} r) \land w \in Word ran pmTrsp (N ∖ \{K\})) \land {Q ↾}_{(N ∖ \{K\})} = \sum_{SymGrp (N ∖ \{K\})} w) \to {(- 1)}^{\|w\|} = {(- 1)}^{\|r\|}$
34	33	eqcomd	$⊢ ((((((N \in Fin \land K \in N) \land Q \in \{q \in P \| q (K) = K\}) \land r \in Word ran pmTrsp (N)) \land Q = \sum_{SymGrp (N)} r) \land w \in Word ran pmTrsp (N ∖ \{K\})) \land {Q ↾}_{(N ∖ \{K\})} = \sum_{SymGrp (N ∖ \{K\})} w) \to {(- 1)}^{\|r\|} = {(- 1)}^{\|w\|}$
35	34	ex	$⊢ (((((N \in Fin \land K \in N) \land Q \in \{q \in P \| q (K) = K\}) \land r \in Word ran pmTrsp (N)) \land Q = \sum_{SymGrp (N)} r) \land w \in Word ran pmTrsp (N ∖ \{K\})) \to ({Q ↾}_{(N ∖ \{K\})} = \sum_{SymGrp (N ∖ \{K\})} w \to {(- 1)}^{\|r\|} = {(- 1)}^{\|w\|})$
36	35	adantlrr	$⊢ (((((N \in Fin \land K \in N) \land Q \in \{q \in P \| q (K) = K\}) \land r \in Word ran pmTrsp (N)) \land (Q = \sum_{SymGrp (N)} r \land s = {(- 1)}^{\|r\|})) \land w \in Word ran pmTrsp (N ∖ \{K\})) \to ({Q ↾}_{(N ∖ \{K\})} = \sum_{SymGrp (N ∖ \{K\})} w \to {(- 1)}^{\|r\|} = {(- 1)}^{\|w\|})$
37		eqeq1	$⊢ s = {(- 1)}^{\|r\|} \to (s = {(- 1)}^{\|w\|} \leftrightarrow {(- 1)}^{\|r\|} = {(- 1)}^{\|w\|})$
38	37	ad2antll	$⊢ ((((N \in Fin \land K \in N) \land Q \in \{q \in P \| q (K) = K\}) \land r \in Word ran pmTrsp (N)) \land (Q = \sum_{SymGrp (N)} r \land s = {(- 1)}^{\|r\|})) \to (s = {(- 1)}^{\|w\|} \leftrightarrow {(- 1)}^{\|r\|} = {(- 1)}^{\|w\|})$
39	38	adantr	$⊢ (((((N \in Fin \land K \in N) \land Q \in \{q \in P \| q (K) = K\}) \land r \in Word ran pmTrsp (N)) \land (Q = \sum_{SymGrp (N)} r \land s = {(- 1)}^{\|r\|})) \land w \in Word ran pmTrsp (N ∖ \{K\})) \to (s = {(- 1)}^{\|w\|} \leftrightarrow {(- 1)}^{\|r\|} = {(- 1)}^{\|w\|})$
40	36 39	sylibrd	$⊢ (((((N \in Fin \land K \in N) \land Q \in \{q \in P \| q (K) = K\}) \land r \in Word ran pmTrsp (N)) \land (Q = \sum_{SymGrp (N)} r \land s = {(- 1)}^{\|r\|})) \land w \in Word ran pmTrsp (N ∖ \{K\})) \to ({Q ↾}_{(N ∖ \{K\})} = \sum_{SymGrp (N ∖ \{K\})} w \to s = {(- 1)}^{\|w\|})$
41	40	ralrimiva	$⊢ ((((N \in Fin \land K \in N) \land Q \in \{q \in P \| q (K) = K\}) \land r \in Word ran pmTrsp (N)) \land (Q = \sum_{SymGrp (N)} r \land s = {(- 1)}^{\|r\|})) \to \forall w \in Word ran pmTrsp (N ∖ \{K\}) ({Q ↾}_{(N ∖ \{K\})} = \sum_{SymGrp (N ∖ \{K\})} w \to s = {(- 1)}^{\|w\|})$
42	24 41	r19.29imd	$⊢ ((((N \in Fin \land K \in N) \land Q \in \{q \in P \| q (K) = K\}) \land r \in Word ran pmTrsp (N)) \land (Q = \sum_{SymGrp (N)} r \land s = {(- 1)}^{\|r\|})) \to \exists w \in Word ran pmTrsp (N ∖ \{K\}) ({Q ↾}_{(N ∖ \{K\})} = \sum_{SymGrp (N ∖ \{K\})} w \land s = {(- 1)}^{\|w\|})$
43	42	rexlimdva2	$⊢ ((N \in Fin \land K \in N) \land Q \in \{q \in P \| q (K) = K\}) \to (\exists r \in Word ran pmTrsp (N) (Q = \sum_{SymGrp (N)} r \land s = {(- 1)}^{\|r\|}) \to \exists w \in Word ran pmTrsp (N ∖ \{K\}) ({Q ↾}_{(N ∖ \{K\})} = \sum_{SymGrp (N ∖ \{K\})} w \land s = {(- 1)}^{\|w\|}))$
44	21 43	impbid	$⊢ ((N \in Fin \land K \in N) \land Q \in \{q \in P \| q (K) = K\}) \to (\exists w \in Word ran pmTrsp (N ∖ \{K\}) ({Q ↾}_{(N ∖ \{K\})} = \sum_{SymGrp (N ∖ \{K\})} w \land s = {(- 1)}^{\|w\|}) \leftrightarrow \exists r \in Word ran pmTrsp (N) (Q = \sum_{SymGrp (N)} r \land s = {(- 1)}^{\|r\|}))$
45	44	iotabidv	$⊢ ((N \in Fin \land K \in N) \land Q \in \{q \in P \| q (K) = K\}) \to (ι s \| \exists w \in Word ran pmTrsp (N ∖ \{K\}) ({Q ↾}_{(N ∖ \{K\})} = \sum_{SymGrp (N ∖ \{K\})} w \land s = {(- 1)}^{\|w\|})) = (ι s \| \exists r \in Word ran pmTrsp (N) (Q = \sum_{SymGrp (N)} r \land s = {(- 1)}^{\|r\|}))$
46		diffi	$⊢ N \in Fin \to N ∖ \{K\} \in Fin$
47	46	ad2antrr	$⊢ ((N \in Fin \land K \in N) \land Q \in \{q \in P \| q (K) = K\}) \to N ∖ \{K\} \in Fin$
48		eqid	$⊢ \{q \in P \| q (K) = K\} = \{q \in P \| q (K) = K\}$
49		eqid	$⊢ {Base}_{SymGrp (N ∖ \{K\})} = {Base}_{SymGrp (N ∖ \{K\})}$
50		eqid	$⊢ N ∖ \{K\} = N ∖ \{K\}$
51	1 48 49 50	symgfixelsi	$⊢ (K \in N \land Q \in \{q \in P \| q (K) = K\}) \to {Q ↾}_{(N ∖ \{K\})} \in {Base}_{SymGrp (N ∖ \{K\})}$
52	51	adantll	$⊢ ((N \in Fin \land K \in N) \land Q \in \{q \in P \| q (K) = K\}) \to {Q ↾}_{(N ∖ \{K\})} \in {Base}_{SymGrp (N ∖ \{K\})}$
53	5 49 4 3	psgnvalfi	$⊢ (N ∖ \{K\} \in Fin \land {Q ↾}_{(N ∖ \{K\})} \in {Base}_{SymGrp (N ∖ \{K\})}) \to Z ({Q ↾}_{(N ∖ \{K\})}) = (ι s \| \exists w \in Word ran pmTrsp (N ∖ \{K\}) ({Q ↾}_{(N ∖ \{K\})} = \sum_{SymGrp (N ∖ \{K\})} w \land s = {(- 1)}^{\|w\|}))$
54	47 52 53	syl2anc	$⊢ ((N \in Fin \land K \in N) \land Q \in \{q \in P \| q (K) = K\}) \to Z ({Q ↾}_{(N ∖ \{K\})}) = (ι s \| \exists w \in Word ran pmTrsp (N ∖ \{K\}) ({Q ↾}_{(N ∖ \{K\})} = \sum_{SymGrp (N ∖ \{K\})} w \land s = {(- 1)}^{\|w\|}))$
55		simpl	$⊢ (N \in Fin \land K \in N) \to N \in Fin$
56		elrabi	$⊢ Q \in \{q \in P \| q (K) = K\} \to Q \in P$
57	6 1 7 2	psgnvalfi	$⊢ (N \in Fin \land Q \in P) \to S (Q) = (ι s \| \exists r \in Word ran pmTrsp (N) (Q = \sum_{SymGrp (N)} r \land s = {(- 1)}^{\|r\|}))$
58	55 56 57	syl2an	$⊢ ((N \in Fin \land K \in N) \land Q \in \{q \in P \| q (K) = K\}) \to S (Q) = (ι s \| \exists r \in Word ran pmTrsp (N) (Q = \sum_{SymGrp (N)} r \land s = {(- 1)}^{\|r\|}))$
59	45 54 58	3eqtr4d	$⊢ ((N \in Fin \land K \in N) \land Q \in \{q \in P \| q (K) = K\}) \to Z ({Q ↾}_{(N ∖ \{K\})}) = S (Q)$
60	59	ex	$⊢ (N \in Fin \land K \in N) \to (Q \in \{q \in P \| q (K) = K\} \to Z ({Q ↾}_{(N ∖ \{K\})}) = S (Q))$

Metamath Proof Explorer

Theorem psgndif

Proof