smadiadetlem4

	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	smadiadetlem4	$⊢ (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}{\sum_{G}}, (n (i \in N, j \in N ⟼ if (i = K, if (j = K, \underset{˙}{1}, \underset{˙}{0}), 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	7	crngmgp	$⊢ R \in CRing \to G \in CMnd$
14	3 13	mp1i	$⊢ (M \in B \land K \in N) \to G \in CMnd$
15	1 2	matrcl	$⊢ M \in B \to (N \in Fin \land R \in V)$
16	15	simpld	$⊢ M \in B \to N \in Fin$
17	16	adantr	$⊢ (M \in B \land K \in N) \to N \in Fin$
18	14 17	jca	$⊢ (M \in B \land K \in N) \to (G \in CMnd \land N \in Fin)$
19	18	adantr	$⊢ ((M \in B \land K \in N) \land p \in \{q \in P \| q (K) = K\}) \to (G \in CMnd \land N \in Fin)$
20		simprl	$⊢ ((M \in B \land K \in N) \land (i \in N \land j \in N)) \to i \in N$
21		simprr	$⊢ ((M \in B \land K \in N) \land (i \in N \land j \in N)) \to j \in N$
22	2	eleq2i	$⊢ M \in B \leftrightarrow M \in {Base}_{A}$
23	22	biimpi	$⊢ M \in B \to M \in {Base}_{A}$
24	23	adantr	$⊢ (M \in B \land K \in N) \to M \in {Base}_{A}$
25	24	adantr	$⊢ ((M \in B \land K \in N) \land (i \in N \land j \in N)) \to M \in {Base}_{A}$
26		eqid	$⊢ {Base}_{R} = {Base}_{R}$
27	1 26	matecl	$⊢ (i \in N \land j \in N \land M \in {Base}_{A}) \to i M j \in {Base}_{R}$
28	20 21 25 27	syl3anc	$⊢ ((M \in B \land K \in N) \land (i \in N \land j \in N)) \to i M j \in {Base}_{R}$
29	7 26	mgpbas	$⊢ {Base}_{R} = {Base}_{G}$
30	28 29	eleqtrdi	$⊢ ((M \in B \land K \in N) \land (i \in N \land j \in N)) \to i M j \in {Base}_{G}$
31	30	ralrimivva	$⊢ (M \in B \land K \in N) \to \forall i \in N \forall j \in N i M j \in {Base}_{G}$
32	31	adantr	$⊢ ((M \in B \land K \in N) \land p \in \{q \in P \| q (K) = K\}) \to \forall i \in N \forall j \in N i M j \in {Base}_{G}$
33		crngring	$⊢ R \in CRing \to R \in Ring$
34	26 4	ring0cl	$⊢ R \in Ring \to \underset{˙}{0} \in {Base}_{R}$
35	3 33 34	mp2b	$⊢ \underset{˙}{0} \in {Base}_{R}$
36	35 29	eleqtri	$⊢ \underset{˙}{0} \in {Base}_{G}$
37	32 36	jctir	$⊢ ((M \in B \land K \in N) \land p \in \{q \in P \| q (K) = K\}) \to (\forall i \in N \forall j \in N i M j \in {Base}_{G} \land \underset{˙}{0} \in {Base}_{G})$
38		simpr	$⊢ (M \in B \land K \in N) \to K \in N$
39	38	adantr	$⊢ ((M \in B \land K \in N) \land p \in \{q \in P \| q (K) = K\}) \to K \in N$
40		simpr	$⊢ ((M \in B \land K \in N) \land p \in \{q \in P \| q (K) = K\}) \to p \in \{q \in P \| q (K) = K\}$
41		eqid	$⊢ \{q \in P \| q (K) = K\} = \{q \in P \| q (K) = K\}$
42	7 5	ringidval	$⊢ \underset{˙}{1} = 0_{G}$
43		eqid	$⊢ {Base}_{G} = {Base}_{G}$
44	6 41 42 43	gsummatr01	$⊢ ((G \in CMnd \land N \in Fin) \land (\forall i \in N \forall j \in N i M j \in {Base}_{G} \land \underset{˙}{0} \in {Base}_{G}) \land (K \in N \land K \in N \land p \in \{q \in P \| q (K) = K\})) \to \underset{n \in N}{\sum_{G}} (n (i \in N, j \in N ⟼ if (i = K, if (j = K, \underset{˙}{1}, \underset{˙}{0}), i M j)) p (n)) = \underset{n \in N ∖ \{K\}}{\sum_{G}} (n (i \in (N ∖ \{K\}), j \in (N ∖ \{K\}) ⟼ i M j) p (n))$
45	19 37 39 39 40 44	syl113anc	$⊢ ((M \in B \land K \in N) \land p \in \{q \in P \| q (K) = K\}) \to \underset{n \in N}{\sum_{G}} (n (i \in N, j \in N ⟼ if (i = K, if (j = K, \underset{˙}{1}, \underset{˙}{0}), i M j)) p (n)) = \underset{n \in N ∖ \{K\}}{\sum_{G}} (n (i \in (N ∖ \{K\}), j \in (N ∖ \{K\}) ⟼ i M j) p (n))$
46	45	oveq2d	$⊢ ((M \in B \land K \in N) \land p \in \{q \in P \| q (K) = K\}) \to (Y \circ S) (p) \cdot_{R} (\underset{n \in N}{\sum_{G}}, (n (i \in N, j \in N ⟼ if (i = K, if (j = K, \underset{˙}{1}, \underset{˙}{0}), 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)))$
47	46	mpteq2dva	$⊢ (M \in B \land K \in N) \to (p \in \{q \in P \| q (K) = K\} ⟼ (Y \circ S) (p) \cdot_{R} (\underset{n \in N}{\sum_{G}}, (n (i \in N, j \in N ⟼ if (i = K, if (j = K, \underset{˙}{1}, \underset{˙}{0}), 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))))$
48	47	oveq2d	$⊢ (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}{\sum_{G}}, (n (i \in N, j \in N ⟼ if (i = K, if (j = K, \underset{˙}{1}, \underset{˙}{0}), i M j)) p (n)))) = \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))))$
49	1 2 3 4 5 6 7 8 9 10 11 12	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))))$
50	48 49	eqtrd	$⊢ (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}{\sum_{G}}, (n (i \in N, j \in N ⟼ if (i = K, if (j = K, \underset{˙}{1}, \underset{˙}{0}), 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 smadiadetlem4

Proof