psgndiflemB

	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	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 ((U \in Word R \land \|W\| = \|U\| \land \forall i \in (0 ..^\|W\|) (U (i) (K) = K \land \forall n \in (N ∖ \{K\}) W (i) (n) = U (i) (n))) \to Q = \sum_{Z} 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		elrabi	$⊢ Q \in \{q \in P \| q (K) = K\} \to Q \in P$
7		eqid	$⊢ SymGrp (N) = SymGrp (N)$
8	7 1	symgbasf	$⊢ Q \in P \to Q : N ⟶ N$
9		ffn	$⊢ Q : N ⟶ N \to Q Fn N$
10	6 8 9	3syl	$⊢ Q \in \{q \in P \| q (K) = K\} \to Q Fn N$
11	10	ad3antlr	$⊢ ((((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 \|W\| = \|U\| \land \forall i \in (0 ..^\|W\|) (U (i) (K) = K \land \forall n \in (N ∖ \{K\}) W (i) (n) = U (i) (n)))) \to Q Fn N$
12		simpl	$⊢ (N \in Fin \land K \in N) \to N \in Fin$
13	12	adantr	$⊢ ((N \in Fin \land K \in N) \land Q \in \{q \in P \| q (K) = K\}) \to N \in Fin$
14	13	adantr	$⊢ (((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)) \to N \in Fin$
15		simp1	$⊢ (U \in Word R \land \|W\| = \|U\| \land \forall i \in (0 ..^\|W\|) (U (i) (K) = K \land \forall n \in (N ∖ \{K\}) W (i) (n) = U (i) (n))) \to U \in Word R$
16	4	eqcomi	$⊢ SymGrp (N) = Z$
17	16	fveq2i	$⊢ {Base}_{SymGrp (N)} = {Base}_{Z}$
18	1 17	eqtri	$⊢ P = {Base}_{Z}$
19	4 18 5	gsmtrcl	$⊢ (N \in Fin \land U \in Word R) \to \sum_{Z} U \in P$
20	14 15 19	syl2an	$⊢ ((((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 \|W\| = \|U\| \land \forall i \in (0 ..^\|W\|) (U (i) (K) = K \land \forall n \in (N ∖ \{K\}) W (i) (n) = U (i) (n)))) \to \sum_{Z} U \in P$
21	7 1	symgbasf	$⊢ \sum_{Z} U \in P \to (\sum_{Z}, U) : N ⟶ N$
22		ffn	$⊢ (\sum_{Z}, U) : N ⟶ N \to (\sum_{Z}, U) Fn N$
23	20 21 22	3syl	$⊢ ((((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 \|W\| = \|U\| \land \forall i \in (0 ..^\|W\|) (U (i) (K) = K \land \forall n \in (N ∖ \{K\}) W (i) (n) = U (i) (n)))) \to (\sum_{Z}, U) Fn N$
24	12	ad3antrrr	$⊢ ((((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 \|W\| = \|U\| \land \forall i \in (0 ..^\|W\|) (U (i) (K) = K \land \forall n \in (N ∖ \{K\}) W (i) (n) = U (i) (n)))) \to N \in Fin$
25		simpr	$⊢ (N \in Fin \land K \in N) \to K \in N$
26	25	ad3antrrr	$⊢ ((((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 \|W\| = \|U\| \land \forall i \in (0 ..^\|W\|) (U (i) (K) = K \land \forall n \in (N ∖ \{K\}) W (i) (n) = U (i) (n)))) \to K \in N$
27		eqid	$⊢ {Base}_{Z} = {Base}_{Z}$
28	5 4 27	symgtrf	$⊢ R \subseteq {Base}_{Z}$
29		sswrd	$⊢ R \subseteq {Base}_{Z} \to Word R \subseteq Word {Base}_{Z}$
30	29	sseld	$⊢ R \subseteq {Base}_{Z} \to (U \in Word R \to U \in Word {Base}_{Z})$
31	28 30	ax-mp	$⊢ U \in Word R \to U \in Word {Base}_{Z}$
32	31	3ad2ant1	$⊢ (U \in Word R \land \|W\| = \|U\| \land \forall i \in (0 ..^\|W\|) (U (i) (K) = K \land \forall n \in (N ∖ \{K\}) W (i) (n) = U (i) (n))) \to U \in Word {Base}_{Z}$
33	32	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 \land \|W\| = \|U\| \land \forall i \in (0 ..^\|W\|) (U (i) (K) = K \land \forall n \in (N ∖ \{K\}) W (i) (n) = U (i) (n)))) \to U \in Word {Base}_{Z}$
34	24 26 33	3jca	$⊢ ((((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 \|W\| = \|U\| \land \forall i \in (0 ..^\|W\|) (U (i) (K) = K \land \forall n \in (N ∖ \{K\}) W (i) (n) = U (i) (n)))) \to (N \in Fin \land K \in N \land U \in Word {Base}_{Z})$
35		simpl	$⊢ (U (i) (K) = K \land \forall n \in (N ∖ \{K\}) W (i) (n) = U (i) (n)) \to U (i) (K) = K$
36	35	ralimi	$⊢ \forall i \in (0 ..^\|W\|) (U (i) (K) = K \land \forall n \in (N ∖ \{K\}) W (i) (n) = U (i) (n)) \to \forall i \in (0 ..^\|W\|) U (i) (K) = K$
37	36	3ad2ant3	$⊢ (U \in Word R \land \|W\| = \|U\| \land \forall i \in (0 ..^\|W\|) (U (i) (K) = K \land \forall n \in (N ∖ \{K\}) W (i) (n) = U (i) (n))) \to \forall i \in (0 ..^\|W\|) U (i) (K) = K$
38	37	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 \land \|W\| = \|U\| \land \forall i \in (0 ..^\|W\|) (U (i) (K) = K \land \forall n \in (N ∖ \{K\}) W (i) (n) = U (i) (n)))) \to \forall i \in (0 ..^\|W\|) U (i) (K) = K$
39		oveq2	$⊢ \|U\| = \|W\| \to (0 ..^\|U\|) = (0 ..^\|W\|)$
40	39	eqcoms	$⊢ \|W\| = \|U\| \to (0 ..^\|U\|) = (0 ..^\|W\|)$
41	40	raleqdv	$⊢ \|W\| = \|U\| \to (\forall i \in (0 ..^\|U\|) U (i) (K) = K \leftrightarrow \forall i \in (0 ..^\|W\|) U (i) (K) = K)$
42	41	3ad2ant2	$⊢ (U \in Word R \land \|W\| = \|U\| \land \forall i \in (0 ..^\|W\|) (U (i) (K) = K \land \forall n \in (N ∖ \{K\}) W (i) (n) = U (i) (n))) \to (\forall i \in (0 ..^\|U\|) U (i) (K) = K \leftrightarrow \forall i \in (0 ..^\|W\|) U (i) (K) = K)$
43	42	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 \land \|W\| = \|U\| \land \forall i \in (0 ..^\|W\|) (U (i) (K) = K \land \forall n \in (N ∖ \{K\}) W (i) (n) = U (i) (n)))) \to (\forall i \in (0 ..^\|U\|) U (i) (K) = K \leftrightarrow \forall i \in (0 ..^\|W\|) U (i) (K) = K)$
44	38 43	mpbird	$⊢ ((((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 \|W\| = \|U\| \land \forall i \in (0 ..^\|W\|) (U (i) (K) = K \land \forall n \in (N ∖ \{K\}) W (i) (n) = U (i) (n)))) \to \forall i \in (0 ..^\|U\|) U (i) (K) = K$
45	4 27	gsmsymgrfix	$⊢ (N \in Fin \land K \in N \land U \in Word {Base}_{Z}) \to (\forall i \in (0 ..^\|U\|) U (i) (K) = K \to (\sum_{Z}, U) (K) = K)$
46	34 44 45	sylc	$⊢ ((((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 \|W\| = \|U\| \land \forall i \in (0 ..^\|W\|) (U (i) (K) = K \land \forall n \in (N ∖ \{K\}) W (i) (n) = U (i) (n)))) \to (\sum_{Z}, U) (K) = K$
47	46	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 (U \in Word R \land \|W\| = \|U\| \land \forall i \in (0 ..^\|W\|) (U (i) (K) = K \land \forall n \in (N ∖ \{K\}) W (i) (n) = U (i) (n)))) \to K = (\sum_{Z}, U) (K)$
48	47	adantr	$⊢ (((((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 \|W\| = \|U\| \land \forall i \in (0 ..^\|W\|) (U (i) (K) = K \land \forall n \in (N ∖ \{K\}) W (i) (n) = U (i) (n)))) \land k = K) \to K = (\sum_{Z}, U) (K)$
49		fveq2	$⊢ k = K \to Q (k) = Q (K)$
50		fveq1	$⊢ q = Q \to q (K) = Q (K)$
51	50	eqeq1d	$⊢ q = Q \to (q (K) = K \leftrightarrow Q (K) = K)$
52	51	elrab	$⊢ Q \in \{q \in P \| q (K) = K\} \leftrightarrow (Q \in P \land Q (K) = K)$
53	52	simprbi	$⊢ Q \in \{q \in P \| q (K) = K\} \to Q (K) = K$
54	53	ad3antlr	$⊢ ((((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 \|W\| = \|U\| \land \forall i \in (0 ..^\|W\|) (U (i) (K) = K \land \forall n \in (N ∖ \{K\}) W (i) (n) = U (i) (n)))) \to Q (K) = K$
55	49 54	sylan9eqr	$⊢ (((((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 \|W\| = \|U\| \land \forall i \in (0 ..^\|W\|) (U (i) (K) = K \land \forall n \in (N ∖ \{K\}) W (i) (n) = U (i) (n)))) \land k = K) \to Q (k) = K$
56		fveq2	$⊢ k = K \to (\sum_{Z}, U) (k) = (\sum_{Z}, U) (K)$
57	56	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 \land \|W\| = \|U\| \land \forall i \in (0 ..^\|W\|) (U (i) (K) = K \land \forall n \in (N ∖ \{K\}) W (i) (n) = U (i) (n)))) \land k = K) \to (\sum_{Z}, U) (k) = (\sum_{Z}, U) (K)$
58	48 55 57	3eqtr4d	$⊢ (((((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 \|W\| = \|U\| \land \forall i \in (0 ..^\|W\|) (U (i) (K) = K \land \forall n \in (N ∖ \{K\}) W (i) (n) = U (i) (n)))) \land k = K) \to Q (k) = (\sum_{Z}, U) (k)$
59	58	ex	$⊢ ((((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 \|W\| = \|U\| \land \forall i \in (0 ..^\|W\|) (U (i) (K) = K \land \forall n \in (N ∖ \{K\}) W (i) (n) = U (i) (n)))) \to (k = K \to Q (k) = (\sum_{Z}, U) (k))$
60	59	adantr	$⊢ (((((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 \|W\| = \|U\| \land \forall i \in (0 ..^\|W\|) (U (i) (K) = K \land \forall n \in (N ∖ \{K\}) W (i) (n) = U (i) (n)))) \land k \in N) \to (k = K \to Q (k) = (\sum_{Z}, U) (k))$
61	60	com12	$⊢ k = K \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 \land \|W\| = \|U\| \land \forall i \in (0 ..^\|W\|) (U (i) (K) = K \land \forall n \in (N ∖ \{K\}) W (i) (n) = U (i) (n)))) \land k \in N) \to Q (k) = (\sum_{Z}, U) (k))$
62		fveq1	$⊢ {Q ↾}_{(N ∖ \{K\})} = \sum_{S} W \to ({Q ↾}_{(N ∖ \{K\})}) (k) = (\sum_{S}, W) (k)$
63	62	adantl	$⊢ (W \in Word T \land {Q ↾}_{(N ∖ \{K\})} = \sum_{S} W) \to ({Q ↾}_{(N ∖ \{K\})}) (k) = (\sum_{S}, W) (k)$
64	63	ad3antlr	$⊢ (((((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 \|W\| = \|U\| \land \forall i \in (0 ..^\|W\|) (U (i) (K) = K \land \forall n \in (N ∖ \{K\}) W (i) (n) = U (i) (n)))) \land k \in N) \to ({Q ↾}_{(N ∖ \{K\})}) (k) = (\sum_{S}, W) (k)$
65	64	adantl	$⊢ (\neg k = K \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 \|W\| = \|U\| \land \forall i \in (0 ..^\|W\|) (U (i) (K) = K \land \forall n \in (N ∖ \{K\}) W (i) (n) = U (i) (n)))) \land k \in N)) \to ({Q ↾}_{(N ∖ \{K\})}) (k) = (\sum_{S}, W) (k)$
66		simpr	$⊢ ((N \in Fin \land K \in N) \land k \in N) \to k \in N$
67		neqne	$⊢ \neg k = K \to k \neq K$
68	66 67	anim12i	$⊢ (((N \in Fin \land K \in N) \land k \in N) \land \neg k = K) \to (k \in N \land k \neq K)$
69		eldifsn	$⊢ k \in (N ∖ \{K\}) \leftrightarrow (k \in N \land k \neq K)$
70	68 69	sylibr	$⊢ (((N \in Fin \land K \in N) \land k \in N) \land \neg k = K) \to k \in (N ∖ \{K\})$
71	70	fvresd	$⊢ (((N \in Fin \land K \in N) \land k \in N) \land \neg k = K) \to ({Q ↾}_{(N ∖ \{K\})}) (k) = Q (k)$
72	71	exp31	$⊢ (N \in Fin \land K \in N) \to (k \in N \to (\neg k = K \to ({Q ↾}_{(N ∖ \{K\})}) (k) = Q (k)))$
73	72	ad3antrrr	$⊢ ((((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 \|W\| = \|U\| \land \forall i \in (0 ..^\|W\|) (U (i) (K) = K \land \forall n \in (N ∖ \{K\}) W (i) (n) = U (i) (n)))) \to (k \in N \to (\neg k = K \to ({Q ↾}_{(N ∖ \{K\})}) (k) = Q (k)))$
74	73	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 \land \|W\| = \|U\| \land \forall i \in (0 ..^\|W\|) (U (i) (K) = K \land \forall n \in (N ∖ \{K\}) W (i) (n) = U (i) (n)))) \land k \in N) \to (\neg k = K \to ({Q ↾}_{(N ∖ \{K\})}) (k) = Q (k))$
75	74	impcom	$⊢ (\neg k = K \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 \|W\| = \|U\| \land \forall i \in (0 ..^\|W\|) (U (i) (K) = K \land \forall n \in (N ∖ \{K\}) W (i) (n) = U (i) (n)))) \land k \in N)) \to ({Q ↾}_{(N ∖ \{K\})}) (k) = Q (k)$
76		fveq2	$⊢ n = k \to (\sum_{S}, W) (n) = (\sum_{S}, W) (k)$
77		fveq2	$⊢ n = k \to (\sum_{Z}, U) (n) = (\sum_{Z}, U) (k)$
78	76 77	eqeq12d	$⊢ n = k \to ((\sum_{S}, W) (n) = (\sum_{Z}, U) (n) \leftrightarrow (\sum_{S}, W) (k) = (\sum_{Z}, U) (k))$
79		diffi	$⊢ N \in Fin \to N ∖ \{K\} \in Fin$
80	79	ancri	$⊢ N \in Fin \to (N ∖ \{K\} \in Fin \land N \in Fin)$
81	80	adantr	$⊢ (N \in Fin \land K \in N) \to (N ∖ \{K\} \in Fin \land N \in Fin)$
82	81	ad3antrrr	$⊢ ((((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 \|W\| = \|U\| \land \forall i \in (0 ..^\|W\|) (U (i) (K) = K \land \forall n \in (N ∖ \{K\}) W (i) (n) = U (i) (n)))) \to (N ∖ \{K\} \in Fin \land N \in Fin)$
83		eqid	$⊢ {Base}_{S} = {Base}_{S}$
84	2 3 83	symgtrf	$⊢ T \subseteq {Base}_{S}$
85		sswrd	$⊢ T \subseteq {Base}_{S} \to Word T \subseteq Word {Base}_{S}$
86	85	sseld	$⊢ T \subseteq {Base}_{S} \to (W \in Word T \to W \in Word {Base}_{S})$
87	84 86	ax-mp	$⊢ W \in Word T \to W \in Word {Base}_{S}$
88	87	ad2antrl	$⊢ (((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)) \to W \in Word {Base}_{S}$
89	88	adantr	$⊢ ((((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 \|W\| = \|U\| \land \forall i \in (0 ..^\|W\|) (U (i) (K) = K \land \forall n \in (N ∖ \{K\}) W (i) (n) = U (i) (n)))) \to W \in Word {Base}_{S}$
90		simpr2	$⊢ ((((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 \|W\| = \|U\| \land \forall i \in (0 ..^\|W\|) (U (i) (K) = K \land \forall n \in (N ∖ \{K\}) W (i) (n) = U (i) (n)))) \to \|W\| = \|U\|$
91	89 33 90	3jca	$⊢ ((((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 \|W\| = \|U\| \land \forall i \in (0 ..^\|W\|) (U (i) (K) = K \land \forall n \in (N ∖ \{K\}) W (i) (n) = U (i) (n)))) \to (W \in Word {Base}_{S} \land U \in Word {Base}_{Z} \land \|W\| = \|U\|)$
92	82 91	jca	$⊢ ((((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 \|W\| = \|U\| \land \forall i \in (0 ..^\|W\|) (U (i) (K) = K \land \forall n \in (N ∖ \{K\}) W (i) (n) = U (i) (n)))) \to ((N ∖ \{K\} \in Fin \land N \in Fin) \land (W \in Word {Base}_{S} \land U \in Word {Base}_{Z} \land \|W\| = \|U\|))$
93	92	ad2antrl	$⊢ (\neg k = K \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 \|W\| = \|U\| \land \forall i \in (0 ..^\|W\|) (U (i) (K) = K \land \forall n \in (N ∖ \{K\}) W (i) (n) = U (i) (n)))) \land k \in N)) \to ((N ∖ \{K\} \in Fin \land N \in Fin) \land (W \in Word {Base}_{S} \land U \in Word {Base}_{Z} \land \|W\| = \|U\|))$
94		simpr	$⊢ (U (i) (K) = K \land \forall n \in (N ∖ \{K\}) W (i) (n) = U (i) (n)) \to \forall n \in (N ∖ \{K\}) W (i) (n) = U (i) (n)$
95	94	ralimi	$⊢ \forall i \in (0 ..^\|W\|) (U (i) (K) = K \land \forall n \in (N ∖ \{K\}) W (i) (n) = U (i) (n)) \to \forall i \in (0 ..^\|W\|) \forall n \in (N ∖ \{K\}) W (i) (n) = U (i) (n)$
96	95	3ad2ant3	$⊢ (U \in Word R \land \|W\| = \|U\| \land \forall i \in (0 ..^\|W\|) (U (i) (K) = K \land \forall n \in (N ∖ \{K\}) W (i) (n) = U (i) (n))) \to \forall i \in (0 ..^\|W\|) \forall n \in (N ∖ \{K\}) W (i) (n) = U (i) (n)$
97	96	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 \land \|W\| = \|U\| \land \forall i \in (0 ..^\|W\|) (U (i) (K) = K \land \forall n \in (N ∖ \{K\}) W (i) (n) = U (i) (n)))) \to \forall i \in (0 ..^\|W\|) \forall n \in (N ∖ \{K\}) W (i) (n) = U (i) (n)$
98	97	ad2antrl	$⊢ (\neg k = K \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 \|W\| = \|U\| \land \forall i \in (0 ..^\|W\|) (U (i) (K) = K \land \forall n \in (N ∖ \{K\}) W (i) (n) = U (i) (n)))) \land k \in N)) \to \forall i \in (0 ..^\|W\|) \forall n \in (N ∖ \{K\}) W (i) (n) = U (i) (n)$
99		incom	$⊢ (N ∖ \{K\}) \cap N = N \cap (N ∖ \{K\})$
100		indif	$⊢ N \cap (N ∖ \{K\}) = N ∖ \{K\}$
101	99 100	eqtri	$⊢ (N ∖ \{K\}) \cap N = N ∖ \{K\}$
102	101	eqcomi	$⊢ N ∖ \{K\} = (N ∖ \{K\}) \cap N$
103	3 83 4 27 102	gsmsymgreq	$⊢ ((N ∖ \{K\} \in Fin \land N \in Fin) \land (W \in Word {Base}_{S} \land U \in Word {Base}_{Z} \land \|W\| = \|U\|)) \to (\forall i \in (0 ..^\|W\|) \forall n \in (N ∖ \{K\}) W (i) (n) = U (i) (n) \to \forall n \in (N ∖ \{K\}) (\sum_{S}, W) (n) = (\sum_{Z}, U) (n))$
104	93 98 103	sylc	$⊢ (\neg k = K \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 \|W\| = \|U\| \land \forall i \in (0 ..^\|W\|) (U (i) (K) = K \land \forall n \in (N ∖ \{K\}) W (i) (n) = U (i) (n)))) \land k \in N)) \to \forall n \in (N ∖ \{K\}) (\sum_{S}, W) (n) = (\sum_{Z}, U) (n)$
105	67	anim2i	$⊢ (k \in N \land \neg k = K) \to (k \in N \land k \neq K)$
106	105 69	sylibr	$⊢ (k \in N \land \neg k = K) \to k \in (N ∖ \{K\})$
107	106	ex	$⊢ k \in N \to (\neg k = K \to k \in (N ∖ \{K\}))$
108	107	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 \land \|W\| = \|U\| \land \forall i \in (0 ..^\|W\|) (U (i) (K) = K \land \forall n \in (N ∖ \{K\}) W (i) (n) = U (i) (n)))) \land k \in N) \to (\neg k = K \to k \in (N ∖ \{K\}))$
109	108	impcom	$⊢ (\neg k = K \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 \|W\| = \|U\| \land \forall i \in (0 ..^\|W\|) (U (i) (K) = K \land \forall n \in (N ∖ \{K\}) W (i) (n) = U (i) (n)))) \land k \in N)) \to k \in (N ∖ \{K\})$
110	78 104 109	rspcdva	$⊢ (\neg k = K \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 \|W\| = \|U\| \land \forall i \in (0 ..^\|W\|) (U (i) (K) = K \land \forall n \in (N ∖ \{K\}) W (i) (n) = U (i) (n)))) \land k \in N)) \to (\sum_{S}, W) (k) = (\sum_{Z}, U) (k)$
111	65 75 110	3eqtr3d	$⊢ (\neg k = K \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 \|W\| = \|U\| \land \forall i \in (0 ..^\|W\|) (U (i) (K) = K \land \forall n \in (N ∖ \{K\}) W (i) (n) = U (i) (n)))) \land k \in N)) \to Q (k) = (\sum_{Z}, U) (k)$
112	111	ex	$⊢ \neg k = K \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 \land \|W\| = \|U\| \land \forall i \in (0 ..^\|W\|) (U (i) (K) = K \land \forall n \in (N ∖ \{K\}) W (i) (n) = U (i) (n)))) \land k \in N) \to Q (k) = (\sum_{Z}, U) (k))$
113	61 112	pm2.61i	$⊢ (((((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 \|W\| = \|U\| \land \forall i \in (0 ..^\|W\|) (U (i) (K) = K \land \forall n \in (N ∖ \{K\}) W (i) (n) = U (i) (n)))) \land k \in N) \to Q (k) = (\sum_{Z}, U) (k)$
114	11 23 113	eqfnfvd	$⊢ ((((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 \|W\| = \|U\| \land \forall i \in (0 ..^\|W\|) (U (i) (K) = K \land \forall n \in (N ∖ \{K\}) W (i) (n) = U (i) (n)))) \to Q = \sum_{Z} U$
115	114	exp31	$⊢ ((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 ((U \in Word R \land \|W\| = \|U\| \land \forall i \in (0 ..^\|W\|) (U (i) (K) = K \land \forall n \in (N ∖ \{K\}) W (i) (n) = U (i) (n))) \to Q = \sum_{Z} U))$

Metamath Proof Explorer

Theorem psgndiflemB

Proof