smadiadetlem3

	Ref	Expression
Hypotheses	marep01ma.a	$⊢ A = N Mat R$
	marep01ma.b	$⊢ B = {Base}_{A}$
	marep01ma.r	$⊢ R \in CRing$
	marep01ma.0	$⊢ \underset{˙}{0} = 0_{R}$
	marep01ma.1	$⊢ \underset{˙}{1} = 1_{R}$
	smadiadetlem.p	$⊢ P = {Base}_{SymGrp (N)}$
	smadiadetlem.g	$⊢ G = {mulGrp}_{R}$
	madetminlem.y	$⊢ Y = ℤRHom (R)$
	madetminlem.s	$⊢ S = pmSgn (N)$
	madetminlem.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	smadiadetlem.w	$⊢ W = {Base}_{SymGrp (N ∖ \{K\})}$
	smadiadetlem.z	$⊢ Z = pmSgn (N ∖ \{K\})$
Assertion	smadiadetlem3	$⊢ (M \in B \land K \in N) \to \underset{p \in \{q \in P \| q (K) = K\}}{\sum_{R}} ((Y \circ S) (p) \cdot_{R} (\underset{n \in N ∖ \{K\}}{\sum_{G}}, (n (i \in (N ∖ \{K\}), j \in (N ∖ \{K\}) ⟼ i M j) p (n)))) = \underset{p \in W}{\sum_{R}} ((Y \circ Z) (p) \cdot_{R} (\underset{n \in N ∖ \{K\}}{\sum_{G}}, (n (i \in (N ∖ \{K\}), j \in (N ∖ \{K\}) ⟼ i M j) p (n))))$

Proof

Step	Hyp	Ref	Expression
1		marep01ma.a	$⊢ A = N Mat R$
2		marep01ma.b	$⊢ B = {Base}_{A}$
3		marep01ma.r	$⊢ R \in CRing$
4		marep01ma.0	$⊢ \underset{˙}{0} = 0_{R}$
5		marep01ma.1	$⊢ \underset{˙}{1} = 1_{R}$
6		smadiadetlem.p	$⊢ P = {Base}_{SymGrp (N)}$
7		smadiadetlem.g	$⊢ G = {mulGrp}_{R}$
8		madetminlem.y	$⊢ Y = ℤRHom (R)$
9		madetminlem.s	$⊢ S = pmSgn (N)$
10		madetminlem.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
11		smadiadetlem.w	$⊢ W = {Base}_{SymGrp (N ∖ \{K\})}$
12		smadiadetlem.z	$⊢ Z = pmSgn (N ∖ \{K\})$
13		eqid	$⊢ {Base}_{R} = {Base}_{R}$
14		eqid	$⊢ Cntz (R) = Cntz (R)$
15		crngring	$⊢ R \in CRing \to R \in Ring$
16		ringmnd	$⊢ R \in Ring \to R \in Mnd$
17	3 15 16	mp2b	$⊢ R \in Mnd$
18	17	a1i	$⊢ (M \in B \land K \in N) \to R \in Mnd$
19		fvexd	$⊢ (M \in B \land K \in N) \to {Base}_{SymGrp (N ∖ \{K\})} \in V$
20	11 19	eqeltrid	$⊢ (M \in B \land K \in N) \to W \in V$
21	1 2 3 4 5 6 7 8 9 10 11 12	smadiadetlem3lem1	$⊢ (M \in B \land K \in N) \to (p \in W ⟼ (Y \circ Z) (p) \cdot_{R} (\underset{n \in N ∖ \{K\}}{\sum_{G}}, (n (i \in (N ∖ \{K\}), j \in (N ∖ \{K\}) ⟼ i M j) p (n)))) : W ⟶ {Base}_{R}$
22	1 2 3 4 5 6 7 8 9 10 11 12	smadiadetlem3lem2	$⊢ (M \in B \land K \in N) \to ran (p \in W ⟼ (Y \circ Z) (p) \cdot_{R} (\underset{n \in N ∖ \{K\}}{\sum_{G}}, (n (i \in (N ∖ \{K\}), j \in (N ∖ \{K\}) ⟼ i M j) p (n)))) \subseteq Cntz (R) (ran (p \in W ⟼ (Y \circ Z) (p) \cdot_{R} (\underset{n \in N ∖ \{K\}}{\sum_{G}}, (n (i \in (N ∖ \{K\}), j \in (N ∖ \{K\}) ⟼ i M j) p (n)))))$
23		eqid	$⊢ (p \in W ⟼ (Y \circ Z) (p) \cdot_{R} (\underset{n \in N ∖ \{K\}}{\sum_{G}}, (n (i \in (N ∖ \{K\}), j \in (N ∖ \{K\}) ⟼ i M j) p (n)))) = (p \in W ⟼ (Y \circ Z) (p) \cdot_{R} (\underset{n \in N ∖ \{K\}}{\sum_{G}}, (n (i \in (N ∖ \{K\}), j \in (N ∖ \{K\}) ⟼ i M j) p (n))))$
24	1 2	matrcl	$⊢ M \in B \to (N \in Fin \land R \in V)$
25	24	simpld	$⊢ M \in B \to N \in Fin$
26	25	adantr	$⊢ (M \in B \land K \in N) \to N \in Fin$
27		diffi	$⊢ N \in Fin \to N ∖ \{K\} \in Fin$
28		eqid	$⊢ SymGrp (N ∖ \{K\}) = SymGrp (N ∖ \{K\})$
29		eqid	$⊢ {Base}_{SymGrp (N ∖ \{K\})} = {Base}_{SymGrp (N ∖ \{K\})}$
30	28 29	symgbasfi	$⊢ N ∖ \{K\} \in Fin \to {Base}_{SymGrp (N ∖ \{K\})} \in Fin$
31	26 27 30	3syl	$⊢ (M \in B \land K \in N) \to {Base}_{SymGrp (N ∖ \{K\})} \in Fin$
32	11 31	eqeltrid	$⊢ (M \in B \land K \in N) \to W \in Fin$
33		ovexd	$⊢ ((M \in B \land K \in N) \land p \in W) \to (Y \circ Z) (p) \cdot_{R} (\underset{n \in N ∖ \{K\}}{\sum_{G}}, (n (i \in (N ∖ \{K\}), j \in (N ∖ \{K\}) ⟼ i M j) p (n))) \in V$
34	4	fvexi	$⊢ \underset{˙}{0} \in V$
35	34	a1i	$⊢ (M \in B \land K \in N) \to \underset{˙}{0} \in V$
36	23 32 33 35	fsuppmptdm	$⊢ (M \in B \land K \in N) \to {finSupp}_{\underset{˙}{0}} ((p \in W ⟼ (Y \circ Z) (p) \cdot_{R} (\underset{n \in N ∖ \{K\}}{\sum_{G}}, (n (i \in (N ∖ \{K\}), j \in (N ∖ \{K\}) ⟼ i M j) p (n)))))$
37		fveq1	$⊢ q = p \to q (K) = p (K)$
38	37	eqeq1d	$⊢ q = p \to (q (K) = K \leftrightarrow p (K) = K)$
39	38	cbvrabv	$⊢ \{q \in P \| q (K) = K\} = \{p \in P \| p (K) = K\}$
40		eqid	$⊢ (p \in \{q \in P \| q (K) = K\} ⟼ {p ↾}_{(N ∖ \{K\})}) = (p \in \{q \in P \| q (K) = K\} ⟼ {p ↾}_{(N ∖ \{K\})})$
41	6 39 11 40	symgfixf1o	$⊢ (N \in Fin \land K \in N) \to (p \in \{q \in P \| q (K) = K\} ⟼ {p ↾}_{(N ∖ \{K\})}) : \{q \in P \| q (K) = K\} \underset{1-1 onto}{⟶} W$
42	25 41	sylan	$⊢ (M \in B \land K \in N) \to (p \in \{q \in P \| q (K) = K\} ⟼ {p ↾}_{(N ∖ \{K\})}) : \{q \in P \| q (K) = K\} \underset{1-1 onto}{⟶} W$
43	13 4 14 18 20 21 22 36 42	gsumzf1o	$⊢ (M \in B \land K \in N) \to \underset{p \in W}{\sum_{R}} ((Y \circ Z) (p) \cdot_{R} (\underset{n \in N ∖ \{K\}}{\sum_{G}}, (n (i \in (N ∖ \{K\}), j \in (N ∖ \{K\}) ⟼ i M j) p (n)))) = \sum_{R} ((p \in W ⟼ (Y \circ Z) (p) \cdot_{R} (\underset{n \in N ∖ \{K\}}{\sum_{G}}, (n (i \in (N ∖ \{K\}), j \in (N ∖ \{K\}) ⟼ i M j) p (n)))) \circ (p \in \{q \in P \| q (K) = K\} ⟼ {p ↾}_{(N ∖ \{K\})}))$
44		eqid	$⊢ \{q \in P \| q (K) = K\} = \{q \in P \| q (K) = K\}$
45		eqid	$⊢ N ∖ \{K\} = N ∖ \{K\}$
46	6 44 11 45	symgfixelsi	$⊢ (K \in N \land p \in \{q \in P \| q (K) = K\}) \to {p ↾}_{(N ∖ \{K\})} \in W$
47	46	adantll	$⊢ ((M \in B \land K \in N) \land p \in \{q \in P \| q (K) = K\}) \to {p ↾}_{(N ∖ \{K\})} \in W$
48		eqidd	$⊢ (M \in B \land K \in N) \to (p \in \{q \in P \| q (K) = K\} ⟼ {p ↾}_{(N ∖ \{K\})}) = (p \in \{q \in P \| q (K) = K\} ⟼ {p ↾}_{(N ∖ \{K\})})$
49		fveq2	$⊢ p = y \to (Y \circ Z) (p) = (Y \circ Z) (y)$
50		fveq1	$⊢ p = y \to p (n) = y (n)$
51	50	oveq2d	$⊢ p = y \to n (i \in (N ∖ \{K\}), j \in (N ∖ \{K\}) ⟼ i M j) p (n) = n (i \in (N ∖ \{K\}), j \in (N ∖ \{K\}) ⟼ i M j) y (n)$
52	51	mpteq2dv	$⊢ p = y \to (n \in (N ∖ \{K\}) ⟼ n (i \in (N ∖ \{K\}), j \in (N ∖ \{K\}) ⟼ i M j) p (n)) = (n \in (N ∖ \{K\}) ⟼ n (i \in (N ∖ \{K\}), j \in (N ∖ \{K\}) ⟼ i M j) y (n))$
53	52	oveq2d	$⊢ p = y \to \underset{n \in N ∖ \{K\}}{\sum_{G}} (n (i \in (N ∖ \{K\}), j \in (N ∖ \{K\}) ⟼ i M j) p (n)) = \underset{n \in N ∖ \{K\}}{\sum_{G}} (n (i \in (N ∖ \{K\}), j \in (N ∖ \{K\}) ⟼ i M j) y (n))$
54	49 53	oveq12d	$⊢ p = y \to (Y \circ Z) (p) \cdot_{R} (\underset{n \in N ∖ \{K\}}{\sum_{G}}, (n (i \in (N ∖ \{K\}), j \in (N ∖ \{K\}) ⟼ i M j) p (n))) = (Y \circ Z) (y) \cdot_{R} (\underset{n \in N ∖ \{K\}}{\sum_{G}}, (n (i \in (N ∖ \{K\}), j \in (N ∖ \{K\}) ⟼ i M j) y (n)))$
55	54	cbvmptv	$⊢ (p \in W ⟼ (Y \circ Z) (p) \cdot_{R} (\underset{n \in N ∖ \{K\}}{\sum_{G}}, (n (i \in (N ∖ \{K\}), j \in (N ∖ \{K\}) ⟼ i M j) p (n)))) = (y \in W ⟼ (Y \circ Z) (y) \cdot_{R} (\underset{n \in N ∖ \{K\}}{\sum_{G}}, (n (i \in (N ∖ \{K\}), j \in (N ∖ \{K\}) ⟼ i M j) y (n))))$
56	55	a1i	$⊢ (M \in B \land K \in N) \to (p \in W ⟼ (Y \circ Z) (p) \cdot_{R} (\underset{n \in N ∖ \{K\}}{\sum_{G}}, (n (i \in (N ∖ \{K\}), j \in (N ∖ \{K\}) ⟼ i M j) p (n)))) = (y \in W ⟼ (Y \circ Z) (y) \cdot_{R} (\underset{n \in N ∖ \{K\}}{\sum_{G}}, (n (i \in (N ∖ \{K\}), j \in (N ∖ \{K\}) ⟼ i M j) y (n))))$
57		fveq2	$⊢ y = {p ↾}_{(N ∖ \{K\})} \to (Y \circ Z) (y) = (Y \circ Z) ({p ↾}_{(N ∖ \{K\})})$
58		fveq1	$⊢ y = {p ↾}_{(N ∖ \{K\})} \to y (n) = ({p ↾}_{(N ∖ \{K\})}) (n)$
59		fvres	$⊢ n \in (N ∖ \{K\}) \to ({p ↾}_{(N ∖ \{K\})}) (n) = p (n)$
60	58 59	sylan9eq	$⊢ (y = {p ↾}_{(N ∖ \{K\})} \land n \in (N ∖ \{K\})) \to y (n) = p (n)$
61	60	oveq2d	$⊢ (y = {p ↾}_{(N ∖ \{K\})} \land n \in (N ∖ \{K\})) \to n (i \in (N ∖ \{K\}), j \in (N ∖ \{K\}) ⟼ i M j) y (n) = n (i \in (N ∖ \{K\}), j \in (N ∖ \{K\}) ⟼ i M j) p (n)$
62	61	mpteq2dva	$⊢ y = {p ↾}_{(N ∖ \{K\})} \to (n \in (N ∖ \{K\}) ⟼ n (i \in (N ∖ \{K\}), j \in (N ∖ \{K\}) ⟼ i M j) y (n)) = (n \in (N ∖ \{K\}) ⟼ n (i \in (N ∖ \{K\}), j \in (N ∖ \{K\}) ⟼ i M j) p (n))$
63	62	oveq2d	$⊢ y = {p ↾}_{(N ∖ \{K\})} \to \underset{n \in N ∖ \{K\}}{\sum_{G}} (n (i \in (N ∖ \{K\}), j \in (N ∖ \{K\}) ⟼ i M j) y (n)) = \underset{n \in N ∖ \{K\}}{\sum_{G}} (n (i \in (N ∖ \{K\}), j \in (N ∖ \{K\}) ⟼ i M j) p (n))$
64	57 63	oveq12d	$⊢ y = {p ↾}_{(N ∖ \{K\})} \to (Y \circ Z) (y) \cdot_{R} (\underset{n \in N ∖ \{K\}}{\sum_{G}}, (n (i \in (N ∖ \{K\}), j \in (N ∖ \{K\}) ⟼ i M j) y (n))) = (Y \circ Z) ({p ↾}_{(N ∖ \{K\})}) \cdot_{R} (\underset{n \in N ∖ \{K\}}{\sum_{G}}, (n (i \in (N ∖ \{K\}), j \in (N ∖ \{K\}) ⟼ i M j) p (n)))$
65	47 48 56 64	fmptco	$⊢ (M \in B \land K \in N) \to (p \in W ⟼ (Y \circ Z) (p) \cdot_{R} (\underset{n \in N ∖ \{K\}}{\sum_{G}}, (n (i \in (N ∖ \{K\}), j \in (N ∖ \{K\}) ⟼ i M j) p (n)))) \circ (p \in \{q \in P \| q (K) = K\} ⟼ {p ↾}_{(N ∖ \{K\})}) = (p \in \{q \in P \| q (K) = K\} ⟼ (Y \circ Z) ({p ↾}_{(N ∖ \{K\})}) \cdot_{R} (\underset{n \in N ∖ \{K\}}{\sum_{G}}, (n (i \in (N ∖ \{K\}), j \in (N ∖ \{K\}) ⟼ i M j) p (n))))$
66	6 9 12	copsgndif	$⊢ (N \in Fin \land K \in N) \to (p \in \{q \in P \| q (K) = K\} \to (Y \circ Z) ({p ↾}_{(N ∖ \{K\})}) = (Y \circ S) (p))$
67	25 66	sylan	$⊢ (M \in B \land K \in N) \to (p \in \{q \in P \| q (K) = K\} \to (Y \circ Z) ({p ↾}_{(N ∖ \{K\})}) = (Y \circ S) (p))$
68	67	imp	$⊢ ((M \in B \land K \in N) \land p \in \{q \in P \| q (K) = K\}) \to (Y \circ Z) ({p ↾}_{(N ∖ \{K\})}) = (Y \circ S) (p)$
69	68	oveq1d	$⊢ ((M \in B \land K \in N) \land p \in \{q \in P \| q (K) = K\}) \to (Y \circ Z) ({p ↾}_{(N ∖ \{K\})}) \cdot_{R} (\underset{n \in N ∖ \{K\}}{\sum_{G}}, (n (i \in (N ∖ \{K\}), j \in (N ∖ \{K\}) ⟼ i M j) p (n))) = (Y \circ S) (p) \cdot_{R} (\underset{n \in N ∖ \{K\}}{\sum_{G}}, (n (i \in (N ∖ \{K\}), j \in (N ∖ \{K\}) ⟼ i M j) p (n)))$
70	69	mpteq2dva	$⊢ (M \in B \land K \in N) \to (p \in \{q \in P \| q (K) = K\} ⟼ (Y \circ Z) ({p ↾}_{(N ∖ \{K\})}) \cdot_{R} (\underset{n \in N ∖ \{K\}}{\sum_{G}}, (n (i \in (N ∖ \{K\}), j \in (N ∖ \{K\}) ⟼ i M j) p (n)))) = (p \in \{q \in P \| q (K) = K\} ⟼ (Y \circ S) (p) \cdot_{R} (\underset{n \in N ∖ \{K\}}{\sum_{G}}, (n (i \in (N ∖ \{K\}), j \in (N ∖ \{K\}) ⟼ i M j) p (n))))$
71	65 70	eqtrd	$⊢ (M \in B \land K \in N) \to (p \in W ⟼ (Y \circ Z) (p) \cdot_{R} (\underset{n \in N ∖ \{K\}}{\sum_{G}}, (n (i \in (N ∖ \{K\}), j \in (N ∖ \{K\}) ⟼ i M j) p (n)))) \circ (p \in \{q \in P \| q (K) = K\} ⟼ {p ↾}_{(N ∖ \{K\})}) = (p \in \{q \in P \| q (K) = K\} ⟼ (Y \circ S) (p) \cdot_{R} (\underset{n \in N ∖ \{K\}}{\sum_{G}}, (n (i \in (N ∖ \{K\}), j \in (N ∖ \{K\}) ⟼ i M j) p (n))))$
72	71	oveq2d	$⊢ (M \in B \land K \in N) \to \sum_{R} ((p \in W ⟼ (Y \circ Z) (p) \cdot_{R} (\underset{n \in N ∖ \{K\}}{\sum_{G}}, (n (i \in (N ∖ \{K\}), j \in (N ∖ \{K\}) ⟼ i M j) p (n)))) \circ (p \in \{q \in P \| q (K) = K\} ⟼ {p ↾}_{(N ∖ \{K\})})) = \underset{p \in \{q \in P \| q (K) = K\}}{\sum_{R}} ((Y \circ S) (p) \cdot_{R} (\underset{n \in N ∖ \{K\}}{\sum_{G}}, (n (i \in (N ∖ \{K\}), j \in (N ∖ \{K\}) ⟼ i M j) p (n))))$
73	43 72	eqtr2d	$⊢ (M \in B \land K \in N) \to \underset{p \in \{q \in P \| q (K) = K\}}{\sum_{R}} ((Y \circ S) (p) \cdot_{R} (\underset{n \in N ∖ \{K\}}{\sum_{G}}, (n (i \in (N ∖ \{K\}), j \in (N ∖ \{K\}) ⟼ i M j) p (n)))) = \underset{p \in W}{\sum_{R}} ((Y \circ Z) (p) \cdot_{R} (\underset{n \in N ∖ \{K\}}{\sum_{G}}, (n (i \in (N ∖ \{K\}), j \in (N ∖ \{K\}) ⟼ i M j) p (n))))$

Metamath Proof Explorer

Theorem smadiadetlem3

Proof