psgndiflemA

	Ref	Expression
Hypotheses	psgnfix.p	$⊢ P = {Base}_{SymGrp (N)}$
	psgnfix.t	$⊢ T = ran pmTrsp (N ∖ \{K\})$
	psgnfix.s	$⊢ S = SymGrp (N ∖ \{K\})$
	psgnfix.z	$⊢ Z = SymGrp (N)$
	psgnfix.r	$⊢ R = ran pmTrsp (N)$
Assertion	psgndiflemA	$⊢ ((N \in Fin \land K \in N) \land Q \in \{q \in P \| q (K) = K\}) \to ((W \in Word T \land {Q ↾}_{(N ∖ \{K\})} = \sum_{S} W \land U \in Word R) \to (Q = \sum_{SymGrp (N)} U \to {(- 1)}^{\|W\|} = {(- 1)}^{\|U\|}))$

Proof

Step	Hyp	Ref	Expression
1		psgnfix.p	$⊢ P = {Base}_{SymGrp (N)}$
2		psgnfix.t	$⊢ T = ran pmTrsp (N ∖ \{K\})$
3		psgnfix.s	$⊢ S = SymGrp (N ∖ \{K\})$
4		psgnfix.z	$⊢ Z = SymGrp (N)$
5		psgnfix.r	$⊢ R = ran pmTrsp (N)$
6		fveq2	$⊢ w = W \to \|w\| = \|W\|$
7	6	eqeq1d	$⊢ w = W \to (\|w\| = \|r\| \leftrightarrow \|W\| = \|r\|)$
8	6	oveq2d	$⊢ w = W \to (0 ..^\|w\|) = (0 ..^\|W\|)$
9		fveq1	$⊢ w = W \to w (i) = W (i)$
10	9	fveq1d	$⊢ w = W \to w (i) (n) = W (i) (n)$
11	10	eqeq1d	$⊢ w = W \to (w (i) (n) = r (i) (n) \leftrightarrow W (i) (n) = r (i) (n))$
12	11	ralbidv	$⊢ w = W \to (\forall n \in (N ∖ \{K\}) w (i) (n) = r (i) (n) \leftrightarrow \forall n \in (N ∖ \{K\}) W (i) (n) = r (i) (n))$
13	12	anbi2d	$⊢ w = W \to ((r (i) (K) = K \land \forall n \in (N ∖ \{K\}) w (i) (n) = r (i) (n)) \leftrightarrow (r (i) (K) = K \land \forall n \in (N ∖ \{K\}) W (i) (n) = r (i) (n)))$
14	8 13	raleqbidv	$⊢ w = W \to (\forall i \in (0 ..^\|w\|) (r (i) (K) = K \land \forall n \in (N ∖ \{K\}) w (i) (n) = r (i) (n)) \leftrightarrow \forall i \in (0 ..^\|W\|) (r (i) (K) = K \land \forall n \in (N ∖ \{K\}) W (i) (n) = r (i) (n)))$
15	7 14	anbi12d	$⊢ w = W \to ((\|w\| = \|r\| \land \forall i \in (0 ..^\|w\|) (r (i) (K) = K \land \forall n \in (N ∖ \{K\}) w (i) (n) = r (i) (n))) \leftrightarrow (\|W\| = \|r\| \land \forall i \in (0 ..^\|W\|) (r (i) (K) = K \land \forall n \in (N ∖ \{K\}) W (i) (n) = r (i) (n))))$
16	15	rexbidv	$⊢ w = W \to (\exists r \in Word R (\|w\| = \|r\| \land \forall i \in (0 ..^\|w\|) (r (i) (K) = K \land \forall n \in (N ∖ \{K\}) w (i) (n) = r (i) (n))) \leftrightarrow \exists r \in Word R (\|W\| = \|r\| \land \forall i \in (0 ..^\|W\|) (r (i) (K) = K \land \forall n \in (N ∖ \{K\}) W (i) (n) = r (i) (n))))$
17	16	rspccv	$⊢ \forall w \in Word T \exists r \in Word R (\|w\| = \|r\| \land \forall i \in (0 ..^\|w\|) (r (i) (K) = K \land \forall n \in (N ∖ \{K\}) w (i) (n) = r (i) (n))) \to (W \in Word T \to \exists r \in Word R (\|W\| = \|r\| \land \forall i \in (0 ..^\|W\|) (r (i) (K) = K \land \forall n \in (N ∖ \{K\}) W (i) (n) = r (i) (n))))$
18	2 5	pmtrdifwrdel2	$⊢ K \in N \to \forall w \in Word T \exists r \in Word R (\|w\| = \|r\| \land \forall i \in (0 ..^\|w\|) (r (i) (K) = K \land \forall n \in (N ∖ \{K\}) w (i) (n) = r (i) (n)))$
19	17 18	syl11	$⊢ W \in Word T \to (K \in N \to \exists r \in Word R (\|W\| = \|r\| \land \forall i \in (0 ..^\|W\|) (r (i) (K) = K \land \forall n \in (N ∖ \{K\}) W (i) (n) = r (i) (n))))$
20	19	3ad2ant1	$⊢ (W \in Word T \land {Q ↾}_{(N ∖ \{K\})} = \sum_{S} W \land U \in Word R) \to (K \in N \to \exists r \in Word R (\|W\| = \|r\| \land \forall i \in (0 ..^\|W\|) (r (i) (K) = K \land \forall n \in (N ∖ \{K\}) W (i) (n) = r (i) (n))))$
21	20	com12	$⊢ K \in N \to ((W \in Word T \land {Q ↾}_{(N ∖ \{K\})} = \sum_{S} W \land U \in Word R) \to \exists r \in Word R (\|W\| = \|r\| \land \forall i \in (0 ..^\|W\|) (r (i) (K) = K \land \forall n \in (N ∖ \{K\}) W (i) (n) = r (i) (n))))$
22	21	ad2antlr	$⊢ ((N \in Fin \land K \in N) \land Q \in \{q \in P \| q (K) = K\}) \to ((W \in Word T \land {Q ↾}_{(N ∖ \{K\})} = \sum_{S} W \land U \in Word R) \to \exists r \in Word R (\|W\| = \|r\| \land \forall i \in (0 ..^\|W\|) (r (i) (K) = K \land \forall n \in (N ∖ \{K\}) W (i) (n) = r (i) (n))))$
23	22	imp	$⊢ (((N \in Fin \land K \in N) \land Q \in \{q \in P \| q (K) = K\}) \land (W \in Word T \land {Q ↾}_{(N ∖ \{K\})} = \sum_{S} W \land U \in Word R)) \to \exists r \in Word R (\|W\| = \|r\| \land \forall i \in (0 ..^\|W\|) (r (i) (K) = K \land \forall n \in (N ∖ \{K\}) W (i) (n) = r (i) (n)))$
24		oveq2	$⊢ \|W\| = \|r\| \to {(- 1)}^{\|W\|} = {(- 1)}^{\|r\|}$
25	24	adantr	$⊢ (\|W\| = \|r\| \land \forall i \in (0 ..^\|W\|) (r (i) (K) = K \land \forall n \in (N ∖ \{K\}) W (i) (n) = r (i) (n))) \to {(- 1)}^{\|W\|} = {(- 1)}^{\|r\|}$
26	25	ad3antlr	$⊢ (((r \in Word R \land (\|W\| = \|r\| \land \forall i \in (0 ..^\|W\|) (r (i) (K) = K \land \forall n \in (N ∖ \{K\}) W (i) (n) = r (i) (n)))) \land (((N \in Fin \land K \in N) \land Q \in \{q \in P \| q (K) = K\}) \land (W \in Word T \land {Q ↾}_{(N ∖ \{K\})} = \sum_{S} W \land U \in Word R))) \land Q = \sum_{SymGrp (N)} U) \to {(- 1)}^{\|W\|} = {(- 1)}^{\|r\|}$
27		simplll	$⊢ (((N \in Fin \land K \in N) \land Q \in \{q \in P \| q (K) = K\}) \land (W \in Word T \land {Q ↾}_{(N ∖ \{K\})} = \sum_{S} W \land U \in Word R)) \to N \in Fin$
28	27	ad2antlr	$⊢ (((r \in Word R \land (\|W\| = \|r\| \land \forall i \in (0 ..^\|W\|) (r (i) (K) = K \land \forall n \in (N ∖ \{K\}) W (i) (n) = r (i) (n)))) \land (((N \in Fin \land K \in N) \land Q \in \{q \in P \| q (K) = K\}) \land (W \in Word T \land {Q ↾}_{(N ∖ \{K\})} = \sum_{S} W \land U \in Word R))) \land Q = \sum_{SymGrp (N)} U) \to N \in Fin$
29		simplll	$⊢ (((r \in Word R \land (\|W\| = \|r\| \land \forall i \in (0 ..^\|W\|) (r (i) (K) = K \land \forall n \in (N ∖ \{K\}) W (i) (n) = r (i) (n)))) \land (((N \in Fin \land K \in N) \land Q \in \{q \in P \| q (K) = K\}) \land (W \in Word T \land {Q ↾}_{(N ∖ \{K\})} = \sum_{S} W \land U \in Word R))) \land Q = \sum_{SymGrp (N)} U) \to r \in Word R$
30		simprr3	$⊢ ((r \in Word R \land (\|W\| = \|r\| \land \forall i \in (0 ..^\|W\|) (r (i) (K) = K \land \forall n \in (N ∖ \{K\}) W (i) (n) = r (i) (n)))) \land (((N \in Fin \land K \in N) \land Q \in \{q \in P \| q (K) = K\}) \land (W \in Word T \land {Q ↾}_{(N ∖ \{K\})} = \sum_{S} W \land U \in Word R))) \to U \in Word R$
31	30	adantr	$⊢ (((r \in Word R \land (\|W\| = \|r\| \land \forall i \in (0 ..^\|W\|) (r (i) (K) = K \land \forall n \in (N ∖ \{K\}) W (i) (n) = r (i) (n)))) \land (((N \in Fin \land K \in N) \land Q \in \{q \in P \| q (K) = K\}) \land (W \in Word T \land {Q ↾}_{(N ∖ \{K\})} = \sum_{S} W \land U \in Word R))) \land Q = \sum_{SymGrp (N)} U) \to U \in Word R$
32		simplrl	$⊢ (((r \in Word R \land (\|W\| = \|r\| \land \forall i \in (0 ..^\|W\|) (r (i) (K) = K \land \forall n \in (N ∖ \{K\}) W (i) (n) = r (i) (n)))) \land (((N \in Fin \land K \in N) \land Q \in \{q \in P \| q (K) = K\}) \land (W \in Word T \land {Q ↾}_{(N ∖ \{K\})} = \sum_{S} W \land U \in Word R))) \land Q = \sum_{SymGrp (N)} U) \to ((N \in Fin \land K \in N) \land Q \in \{q \in P \| q (K) = K\})$
33		3simpa	$⊢ (W \in Word T \land {Q ↾}_{(N ∖ \{K\})} = \sum_{S} W \land U \in Word R) \to (W \in Word T \land {Q ↾}_{(N ∖ \{K\})} = \sum_{S} W)$
34	33	adantl	$⊢ (((N \in Fin \land K \in N) \land Q \in \{q \in P \| q (K) = K\}) \land (W \in Word T \land {Q ↾}_{(N ∖ \{K\})} = \sum_{S} W \land U \in Word R)) \to (W \in Word T \land {Q ↾}_{(N ∖ \{K\})} = \sum_{S} W)$
35	34	ad2antlr	$⊢ (((r \in Word R \land (\|W\| = \|r\| \land \forall i \in (0 ..^\|W\|) (r (i) (K) = K \land \forall n \in (N ∖ \{K\}) W (i) (n) = r (i) (n)))) \land (((N \in Fin \land K \in N) \land Q \in \{q \in P \| q (K) = K\}) \land (W \in Word T \land {Q ↾}_{(N ∖ \{K\})} = \sum_{S} W \land U \in Word R))) \land Q = \sum_{SymGrp (N)} U) \to (W \in Word T \land {Q ↾}_{(N ∖ \{K\})} = \sum_{S} W)$
36		simplrl	$⊢ ((r \in Word R \land (\|W\| = \|r\| \land \forall i \in (0 ..^\|W\|) (r (i) (K) = K \land \forall n \in (N ∖ \{K\}) W (i) (n) = r (i) (n)))) \land (((N \in Fin \land K \in N) \land Q \in \{q \in P \| q (K) = K\}) \land (W \in Word T \land {Q ↾}_{(N ∖ \{K\})} = \sum_{S} W \land U \in Word R))) \to \|W\| = \|r\|$
37	36	adantr	$⊢ (((r \in Word R \land (\|W\| = \|r\| \land \forall i \in (0 ..^\|W\|) (r (i) (K) = K \land \forall n \in (N ∖ \{K\}) W (i) (n) = r (i) (n)))) \land (((N \in Fin \land K \in N) \land Q \in \{q \in P \| q (K) = K\}) \land (W \in Word T \land {Q ↾}_{(N ∖ \{K\})} = \sum_{S} W \land U \in Word R))) \land Q = \sum_{SymGrp (N)} U) \to \|W\| = \|r\|$
38		simplrr	$⊢ ((r \in Word R \land (\|W\| = \|r\| \land \forall i \in (0 ..^\|W\|) (r (i) (K) = K \land \forall n \in (N ∖ \{K\}) W (i) (n) = r (i) (n)))) \land (((N \in Fin \land K \in N) \land Q \in \{q \in P \| q (K) = K\}) \land (W \in Word T \land {Q ↾}_{(N ∖ \{K\})} = \sum_{S} W \land U \in Word R))) \to \forall i \in (0 ..^\|W\|) (r (i) (K) = K \land \forall n \in (N ∖ \{K\}) W (i) (n) = r (i) (n))$
39	38	adantr	$⊢ (((r \in Word R \land (\|W\| = \|r\| \land \forall i \in (0 ..^\|W\|) (r (i) (K) = K \land \forall n \in (N ∖ \{K\}) W (i) (n) = r (i) (n)))) \land (((N \in Fin \land K \in N) \land Q \in \{q \in P \| q (K) = K\}) \land (W \in Word T \land {Q ↾}_{(N ∖ \{K\})} = \sum_{S} W \land U \in Word R))) \land Q = \sum_{SymGrp (N)} U) \to \forall i \in (0 ..^\|W\|) (r (i) (K) = K \land \forall n \in (N ∖ \{K\}) W (i) (n) = r (i) (n))$
40	1 2 3 4 5	psgndiflemB	$⊢ ((N \in Fin \land K \in N) \land Q \in \{q \in P \| q (K) = K\}) \to ((W \in Word T \land {Q ↾}_{(N ∖ \{K\})} = \sum_{S} W) \to ((r \in Word R \land \|W\| = \|r\| \land \forall i \in (0 ..^\|W\|) (r (i) (K) = K \land \forall n \in (N ∖ \{K\}) W (i) (n) = r (i) (n))) \to Q = \sum_{Z} r))$
41	40	imp31	$⊢ ((((N \in Fin \land K \in N) \land Q \in \{q \in P \| q (K) = K\}) \land (W \in Word T \land {Q ↾}_{(N ∖ \{K\})} = \sum_{S} W)) \land (r \in Word R \land \|W\| = \|r\| \land \forall i \in (0 ..^\|W\|) (r (i) (K) = K \land \forall n \in (N ∖ \{K\}) W (i) (n) = r (i) (n)))) \to Q = \sum_{Z} r$
42	41	eqcomd	$⊢ ((((N \in Fin \land K \in N) \land Q \in \{q \in P \| q (K) = K\}) \land (W \in Word T \land {Q ↾}_{(N ∖ \{K\})} = \sum_{S} W)) \land (r \in Word R \land \|W\| = \|r\| \land \forall i \in (0 ..^\|W\|) (r (i) (K) = K \land \forall n \in (N ∖ \{K\}) W (i) (n) = r (i) (n)))) \to \sum_{Z} r = Q$
43	32 35 29 37 39 42	syl23anc	$⊢ (((r \in Word R \land (\|W\| = \|r\| \land \forall i \in (0 ..^\|W\|) (r (i) (K) = K \land \forall n \in (N ∖ \{K\}) W (i) (n) = r (i) (n)))) \land (((N \in Fin \land K \in N) \land Q \in \{q \in P \| q (K) = K\}) \land (W \in Word T \land {Q ↾}_{(N ∖ \{K\})} = \sum_{S} W \land U \in Word R))) \land Q = \sum_{SymGrp (N)} U) \to \sum_{Z} r = Q$
44		id	$⊢ Q = \sum_{SymGrp (N)} U \to Q = \sum_{SymGrp (N)} U$
45	4	eqcomi	$⊢ SymGrp (N) = Z$
46	45	oveq1i	$⊢ \sum_{SymGrp (N)} U = \sum_{Z} U$
47	44 46	eqtrdi	$⊢ Q = \sum_{SymGrp (N)} U \to Q = \sum_{Z} U$
48	47	adantl	$⊢ (((r \in Word R \land (\|W\| = \|r\| \land \forall i \in (0 ..^\|W\|) (r (i) (K) = K \land \forall n \in (N ∖ \{K\}) W (i) (n) = r (i) (n)))) \land (((N \in Fin \land K \in N) \land Q \in \{q \in P \| q (K) = K\}) \land (W \in Word T \land {Q ↾}_{(N ∖ \{K\})} = \sum_{S} W \land U \in Word R))) \land Q = \sum_{SymGrp (N)} U) \to Q = \sum_{Z} U$
49	43 48	eqtrd	$⊢ (((r \in Word R \land (\|W\| = \|r\| \land \forall i \in (0 ..^\|W\|) (r (i) (K) = K \land \forall n \in (N ∖ \{K\}) W (i) (n) = r (i) (n)))) \land (((N \in Fin \land K \in N) \land Q \in \{q \in P \| q (K) = K\}) \land (W \in Word T \land {Q ↾}_{(N ∖ \{K\})} = \sum_{S} W \land U \in Word R))) \land Q = \sum_{SymGrp (N)} U) \to \sum_{Z} r = \sum_{Z} U$
50	4 5 28 29 31 49	psgnuni	$⊢ (((r \in Word R \land (\|W\| = \|r\| \land \forall i \in (0 ..^\|W\|) (r (i) (K) = K \land \forall n \in (N ∖ \{K\}) W (i) (n) = r (i) (n)))) \land (((N \in Fin \land K \in N) \land Q \in \{q \in P \| q (K) = K\}) \land (W \in Word T \land {Q ↾}_{(N ∖ \{K\})} = \sum_{S} W \land U \in Word R))) \land Q = \sum_{SymGrp (N)} U) \to {(- 1)}^{\|r\|} = {(- 1)}^{\|U\|}$
51	26 50	eqtrd	$⊢ (((r \in Word R \land (\|W\| = \|r\| \land \forall i \in (0 ..^\|W\|) (r (i) (K) = K \land \forall n \in (N ∖ \{K\}) W (i) (n) = r (i) (n)))) \land (((N \in Fin \land K \in N) \land Q \in \{q \in P \| q (K) = K\}) \land (W \in Word T \land {Q ↾}_{(N ∖ \{K\})} = \sum_{S} W \land U \in Word R))) \land Q = \sum_{SymGrp (N)} U) \to {(- 1)}^{\|W\|} = {(- 1)}^{\|U\|}$
52	51	ex	$⊢ ((r \in Word R \land (\|W\| = \|r\| \land \forall i \in (0 ..^\|W\|) (r (i) (K) = K \land \forall n \in (N ∖ \{K\}) W (i) (n) = r (i) (n)))) \land (((N \in Fin \land K \in N) \land Q \in \{q \in P \| q (K) = K\}) \land (W \in Word T \land {Q ↾}_{(N ∖ \{K\})} = \sum_{S} W \land U \in Word R))) \to (Q = \sum_{SymGrp (N)} U \to {(- 1)}^{\|W\|} = {(- 1)}^{\|U\|})$
53	52	ex	$⊢ (r \in Word R \land (\|W\| = \|r\| \land \forall i \in (0 ..^\|W\|) (r (i) (K) = K \land \forall n \in (N ∖ \{K\}) W (i) (n) = r (i) (n)))) \to ((((N \in Fin \land K \in N) \land Q \in \{q \in P \| q (K) = K\}) \land (W \in Word T \land {Q ↾}_{(N ∖ \{K\})} = \sum_{S} W \land U \in Word R)) \to (Q = \sum_{SymGrp (N)} U \to {(- 1)}^{\|W\|} = {(- 1)}^{\|U\|}))$
54	53	rexlimiva	$⊢ \exists r \in Word R (\|W\| = \|r\| \land \forall i \in (0 ..^\|W\|) (r (i) (K) = K \land \forall n \in (N ∖ \{K\}) W (i) (n) = r (i) (n))) \to ((((N \in Fin \land K \in N) \land Q \in \{q \in P \| q (K) = K\}) \land (W \in Word T \land {Q ↾}_{(N ∖ \{K\})} = \sum_{S} W \land U \in Word R)) \to (Q = \sum_{SymGrp (N)} U \to {(- 1)}^{\|W\|} = {(- 1)}^{\|U\|}))$
55	23 54	mpcom	$⊢ (((N \in Fin \land K \in N) \land Q \in \{q \in P \| q (K) = K\}) \land (W \in Word T \land {Q ↾}_{(N ∖ \{K\})} = \sum_{S} W \land U \in Word R)) \to (Q = \sum_{SymGrp (N)} U \to {(- 1)}^{\|W\|} = {(- 1)}^{\|U\|})$
56	55	ex	$⊢ ((N \in Fin \land K \in N) \land Q \in \{q \in P \| q (K) = K\}) \to ((W \in Word T \land {Q ↾}_{(N ∖ \{K\})} = \sum_{S} W \land U \in Word R) \to (Q = \sum_{SymGrp (N)} U \to {(- 1)}^{\|W\|} = {(- 1)}^{\|U\|}))$

Metamath Proof Explorer

Theorem psgndiflemA

Proof