mdetdiaglem

Description: Lemma for mdetdiag . Previously part of proof for mdet1 . (Contributed by SO, 10-Jul-2018) (Revised by AV, 17-Aug-2019)

	Ref	Expression
Hypotheses	mdetdiag.d	$⊢ D = N maDet R$
	mdetdiag.a	$⊢ A = N Mat R$
	mdetdiag.b	$⊢ B = {Base}_{A}$
	mdetdiag.g	$⊢ G = {mulGrp}_{R}$
	mdetdiag.0	$⊢ \underset{˙}{0} = 0_{R}$
	mdetdiaglem.g	$⊢ H = {Base}_{SymGrp (N)}$
	mdetdiaglem.z	$⊢ Z = ℤRHom (R)$
	mdetdiaglem.s	$⊢ S = pmSgn (N)$
	mdetdiaglem.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
Assertion	mdetdiaglem	$⊢ ((R \in CRing \land N \in Fin \land M \in B) \land \forall i \in N \forall j \in N (i \neq j \to i M j = \underset{˙}{0}) \land (P \in H \land P \neq {I ↾}_{N})) \to (Z \circ S) (P) \underset{˙}{\cdot} (\underset{k \in N}{\sum_{G}}, (P (k) M k)) = \underset{˙}{0}$

Proof

Step	Hyp	Ref	Expression
1		mdetdiag.d	$⊢ D = N maDet R$
2		mdetdiag.a	$⊢ A = N Mat R$
3		mdetdiag.b	$⊢ B = {Base}_{A}$
4		mdetdiag.g	$⊢ G = {mulGrp}_{R}$
5		mdetdiag.0	$⊢ \underset{˙}{0} = 0_{R}$
6		mdetdiaglem.g	$⊢ H = {Base}_{SymGrp (N)}$
7		mdetdiaglem.z	$⊢ Z = ℤRHom (R)$
8		mdetdiaglem.s	$⊢ S = pmSgn (N)$
9		mdetdiaglem.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
10	7	a1i	$⊢ ((R \in CRing \land N \in Fin \land M \in B) \land \forall i \in N \forall j \in N (i \neq j \to i M j = \underset{˙}{0}) \land (P \in H \land P \neq {I ↾}_{N})) \to Z = ℤRHom (R)$
11	8	a1i	$⊢ ((R \in CRing \land N \in Fin \land M \in B) \land \forall i \in N \forall j \in N (i \neq j \to i M j = \underset{˙}{0}) \land (P \in H \land P \neq {I ↾}_{N})) \to S = pmSgn (N)$
12	10 11	coeq12d	$⊢ ((R \in CRing \land N \in Fin \land M \in B) \land \forall i \in N \forall j \in N (i \neq j \to i M j = \underset{˙}{0}) \land (P \in H \land P \neq {I ↾}_{N})) \to Z \circ S = ℤRHom (R) \circ pmSgn (N)$
13	12	fveq1d	$⊢ ((R \in CRing \land N \in Fin \land M \in B) \land \forall i \in N \forall j \in N (i \neq j \to i M j = \underset{˙}{0}) \land (P \in H \land P \neq {I ↾}_{N})) \to (Z \circ S) (P) = (ℤRHom (R) \circ pmSgn (N)) (P)$
14		eqid	$⊢ SymGrp (N) = SymGrp (N)$
15	14 6	symgbasf1o	$⊢ P \in H \to P : N \underset{1-1 onto}{⟶} N$
16		f1ofn	$⊢ P : N \underset{1-1 onto}{⟶} N \to P Fn N$
17	15 16	syl	$⊢ P \in H \to P Fn N$
18		fnnfpeq0	$⊢ P Fn N \to (dom (P ∖ I) = \emptyset \leftrightarrow P = {I ↾}_{N})$
19	17 18	syl	$⊢ P \in H \to (dom (P ∖ I) = \emptyset \leftrightarrow P = {I ↾}_{N})$
20	19	adantl	$⊢ (((R \in CRing \land N \in Fin \land M \in B) \land \forall i \in N \forall j \in N (i \neq j \to i M j = \underset{˙}{0})) \land P \in H) \to (dom (P ∖ I) = \emptyset \leftrightarrow P = {I ↾}_{N})$
21	20	bicomd	$⊢ (((R \in CRing \land N \in Fin \land M \in B) \land \forall i \in N \forall j \in N (i \neq j \to i M j = \underset{˙}{0})) \land P \in H) \to (P = {I ↾}_{N} \leftrightarrow dom (P ∖ I) = \emptyset)$
22	21	necon3bid	$⊢ (((R \in CRing \land N \in Fin \land M \in B) \land \forall i \in N \forall j \in N (i \neq j \to i M j = \underset{˙}{0})) \land P \in H) \to (P \neq {I ↾}_{N} \leftrightarrow dom (P ∖ I) \neq \emptyset)$
23		n0	$⊢ dom (P ∖ I) \neq \emptyset \leftrightarrow \exists s s \in dom (P ∖ I)$
24		eqid	$⊢ {Base}_{G} = {Base}_{G}$
25		eqid	$⊢ \cdot_{R} = \cdot_{R}$
26	4 25	mgpplusg	$⊢ \cdot_{R} = +_{G}$
27	4	crngmgp	$⊢ R \in CRing \to G \in CMnd$
28	27	3ad2ant1	$⊢ (R \in CRing \land N \in Fin \land M \in B) \to G \in CMnd$
29	28	ad2antrr	$⊢ (((R \in CRing \land N \in Fin \land M \in B) \land \forall i \in N \forall j \in N (i \neq j \to i M j = \underset{˙}{0})) \land (P \in H \land s \in dom (P ∖ I))) \to G \in CMnd$
30		simpll2	$⊢ (((R \in CRing \land N \in Fin \land M \in B) \land \forall i \in N \forall j \in N (i \neq j \to i M j = \underset{˙}{0})) \land (P \in H \land s \in dom (P ∖ I))) \to N \in Fin$
31		eqid	$⊢ {Base}_{R} = {Base}_{R}$
32	2 31 3	matbas2i	$⊢ M \in B \to M \in ({Base}_{R}^{(N \times N)})$
33	32	3ad2ant3	$⊢ (R \in CRing \land N \in Fin \land M \in B) \to M \in ({Base}_{R}^{(N \times N)})$
34		elmapi	$⊢ M \in ({Base}_{R}^{(N \times N)}) \to M : N \times N ⟶ {Base}_{R}$
35	33 34	syl	$⊢ (R \in CRing \land N \in Fin \land M \in B) \to M : N \times N ⟶ {Base}_{R}$
36	4 31	mgpbas	$⊢ {Base}_{R} = {Base}_{G}$
37	36	eqcomi	$⊢ {Base}_{G} = {Base}_{R}$
38	37	a1i	$⊢ (R \in CRing \land N \in Fin \land M \in B) \to {Base}_{G} = {Base}_{R}$
39	38	feq3d	$⊢ (R \in CRing \land N \in Fin \land M \in B) \to (M : N \times N ⟶ {Base}_{G} \leftrightarrow M : N \times N ⟶ {Base}_{R})$
40	35 39	mpbird	$⊢ (R \in CRing \land N \in Fin \land M \in B) \to M : N \times N ⟶ {Base}_{G}$
41	40	ad3antrrr	$⊢ ((((R \in CRing \land N \in Fin \land M \in B) \land \forall i \in N \forall j \in N (i \neq j \to i M j = \underset{˙}{0})) \land (P \in H \land s \in dom (P ∖ I))) \land k \in N) \to M : N \times N ⟶ {Base}_{G}$
42	14 6	symgbasf	$⊢ P \in H \to P : N ⟶ N$
43	42	ad2antrl	$⊢ (((R \in CRing \land N \in Fin \land M \in B) \land \forall i \in N \forall j \in N (i \neq j \to i M j = \underset{˙}{0})) \land (P \in H \land s \in dom (P ∖ I))) \to P : N ⟶ N$
44	43	ffvelcdmda	$⊢ ((((R \in CRing \land N \in Fin \land M \in B) \land \forall i \in N \forall j \in N (i \neq j \to i M j = \underset{˙}{0})) \land (P \in H \land s \in dom (P ∖ I))) \land k \in N) \to P (k) \in N$
45		simpr	$⊢ ((((R \in CRing \land N \in Fin \land M \in B) \land \forall i \in N \forall j \in N (i \neq j \to i M j = \underset{˙}{0})) \land (P \in H \land s \in dom (P ∖ I))) \land k \in N) \to k \in N$
46	41 44 45	fovcdmd	$⊢ ((((R \in CRing \land N \in Fin \land M \in B) \land \forall i \in N \forall j \in N (i \neq j \to i M j = \underset{˙}{0})) \land (P \in H \land s \in dom (P ∖ I))) \land k \in N) \to P (k) M k \in {Base}_{G}$
47		disjdif	$⊢ \{s\} \cap (N ∖ \{s\}) = \emptyset$
48	47	a1i	$⊢ (((R \in CRing \land N \in Fin \land M \in B) \land \forall i \in N \forall j \in N (i \neq j \to i M j = \underset{˙}{0})) \land (P \in H \land s \in dom (P ∖ I))) \to \{s\} \cap (N ∖ \{s\}) = \emptyset$
49		difss	$⊢ P ∖ I \subseteq P$
50		dmss	$⊢ P ∖ I \subseteq P \to dom (P ∖ I) \subseteq dom P$
51	49 50	ax-mp	$⊢ dom (P ∖ I) \subseteq dom P$
52	42	adantl	$⊢ (((R \in CRing \land N \in Fin \land M \in B) \land \forall i \in N \forall j \in N (i \neq j \to i M j = \underset{˙}{0})) \land P \in H) \to P : N ⟶ N$
53	51 52	fssdm	$⊢ (((R \in CRing \land N \in Fin \land M \in B) \land \forall i \in N \forall j \in N (i \neq j \to i M j = \underset{˙}{0})) \land P \in H) \to dom (P ∖ I) \subseteq N$
54	53	sseld	$⊢ (((R \in CRing \land N \in Fin \land M \in B) \land \forall i \in N \forall j \in N (i \neq j \to i M j = \underset{˙}{0})) \land P \in H) \to (s \in dom (P ∖ I) \to s \in N)$
55	54	impr	$⊢ (((R \in CRing \land N \in Fin \land M \in B) \land \forall i \in N \forall j \in N (i \neq j \to i M j = \underset{˙}{0})) \land (P \in H \land s \in dom (P ∖ I))) \to s \in N$
56	55	snssd	$⊢ (((R \in CRing \land N \in Fin \land M \in B) \land \forall i \in N \forall j \in N (i \neq j \to i M j = \underset{˙}{0})) \land (P \in H \land s \in dom (P ∖ I))) \to \{s\} \subseteq N$
57		undif	$⊢ \{s\} \subseteq N \leftrightarrow \{s\} \cup (N ∖ \{s\}) = N$
58	56 57	sylib	$⊢ (((R \in CRing \land N \in Fin \land M \in B) \land \forall i \in N \forall j \in N (i \neq j \to i M j = \underset{˙}{0})) \land (P \in H \land s \in dom (P ∖ I))) \to \{s\} \cup (N ∖ \{s\}) = N$
59	58	eqcomd	$⊢ (((R \in CRing \land N \in Fin \land M \in B) \land \forall i \in N \forall j \in N (i \neq j \to i M j = \underset{˙}{0})) \land (P \in H \land s \in dom (P ∖ I))) \to N = \{s\} \cup (N ∖ \{s\})$
60	24 26 29 30 46 48 59	gsummptfidmsplit	$⊢ (((R \in CRing \land N \in Fin \land M \in B) \land \forall i \in N \forall j \in N (i \neq j \to i M j = \underset{˙}{0})) \land (P \in H \land s \in dom (P ∖ I))) \to \underset{k \in N}{\sum_{G}} (P (k) M k) = (\underset{k \in \{s\}}{\sum_{G}}, (P (k) M k)) \cdot_{R} (\underset{k \in N ∖ \{s\}}{\sum_{G}}, (P (k) M k))$
61		crngring	$⊢ R \in CRing \to R \in Ring$
62	61	adantr	$⊢ (R \in CRing \land N \in Fin) \to R \in Ring$
63	4	ringmgp	$⊢ R \in Ring \to G \in Mnd$
64	62 63	syl	$⊢ (R \in CRing \land N \in Fin) \to G \in Mnd$
65	64	3adant3	$⊢ (R \in CRing \land N \in Fin \land M \in B) \to G \in Mnd$
66	65	ad2antrr	$⊢ (((R \in CRing \land N \in Fin \land M \in B) \land \forall i \in N \forall j \in N (i \neq j \to i M j = \underset{˙}{0})) \land (P \in H \land s \in dom (P ∖ I))) \to G \in Mnd$
67		vex	$⊢ s \in V$
68	67	a1i	$⊢ (((R \in CRing \land N \in Fin \land M \in B) \land \forall i \in N \forall j \in N (i \neq j \to i M j = \underset{˙}{0})) \land (P \in H \land s \in dom (P ∖ I))) \to s \in V$
69	35	ad2antrr	$⊢ (((R \in CRing \land N \in Fin \land M \in B) \land \forall i \in N \forall j \in N (i \neq j \to i M j = \underset{˙}{0})) \land (P \in H \land s \in dom (P ∖ I))) \to M : N \times N ⟶ {Base}_{R}$
70	43 55	ffvelcdmd	$⊢ (((R \in CRing \land N \in Fin \land M \in B) \land \forall i \in N \forall j \in N (i \neq j \to i M j = \underset{˙}{0})) \land (P \in H \land s \in dom (P ∖ I))) \to P (s) \in N$
71	69 70 55	fovcdmd	$⊢ (((R \in CRing \land N \in Fin \land M \in B) \land \forall i \in N \forall j \in N (i \neq j \to i M j = \underset{˙}{0})) \land (P \in H \land s \in dom (P ∖ I))) \to P (s) M s \in {Base}_{R}$
72		fveq2	$⊢ k = s \to P (k) = P (s)$
73		id	$⊢ k = s \to k = s$
74	72 73	oveq12d	$⊢ k = s \to P (k) M k = P (s) M s$
75	36 74	gsumsn	$⊢ (G \in Mnd \land s \in V \land P (s) M s \in {Base}_{R}) \to \underset{k \in \{s\}}{\sum_{G}} (P (k) M k) = P (s) M s$
76	66 68 71 75	syl3anc	$⊢ (((R \in CRing \land N \in Fin \land M \in B) \land \forall i \in N \forall j \in N (i \neq j \to i M j = \underset{˙}{0})) \land (P \in H \land s \in dom (P ∖ I))) \to \underset{k \in \{s\}}{\sum_{G}} (P (k) M k) = P (s) M s$
77		simprr	$⊢ (((R \in CRing \land N \in Fin \land M \in B) \land \forall i \in N \forall j \in N (i \neq j \to i M j = \underset{˙}{0})) \land (P \in H \land s \in dom (P ∖ I))) \to s \in dom (P ∖ I)$
78	17	ad2antrl	$⊢ (((R \in CRing \land N \in Fin \land M \in B) \land \forall i \in N \forall j \in N (i \neq j \to i M j = \underset{˙}{0})) \land (P \in H \land s \in dom (P ∖ I))) \to P Fn N$
79		fnelnfp	$⊢ (P Fn N \land s \in N) \to (s \in dom (P ∖ I) \leftrightarrow P (s) \neq s)$
80	78 55 79	syl2anc	$⊢ (((R \in CRing \land N \in Fin \land M \in B) \land \forall i \in N \forall j \in N (i \neq j \to i M j = \underset{˙}{0})) \land (P \in H \land s \in dom (P ∖ I))) \to (s \in dom (P ∖ I) \leftrightarrow P (s) \neq s)$
81	77 80	mpbid	$⊢ (((R \in CRing \land N \in Fin \land M \in B) \land \forall i \in N \forall j \in N (i \neq j \to i M j = \underset{˙}{0})) \land (P \in H \land s \in dom (P ∖ I))) \to P (s) \neq s$
82	42	ad2antrl	$⊢ ((R \in CRing \land N \in Fin \land M \in B) \land (P \in H \land s \in dom (P ∖ I))) \to P : N ⟶ N$
83	42	adantl	$⊢ ((R \in CRing \land N \in Fin \land M \in B) \land P \in H) \to P : N ⟶ N$
84	51 83	fssdm	$⊢ ((R \in CRing \land N \in Fin \land M \in B) \land P \in H) \to dom (P ∖ I) \subseteq N$
85	84	sseld	$⊢ ((R \in CRing \land N \in Fin \land M \in B) \land P \in H) \to (s \in dom (P ∖ I) \to s \in N)$
86	85	impr	$⊢ ((R \in CRing \land N \in Fin \land M \in B) \land (P \in H \land s \in dom (P ∖ I))) \to s \in N$
87	82 86	ffvelcdmd	$⊢ ((R \in CRing \land N \in Fin \land M \in B) \land (P \in H \land s \in dom (P ∖ I))) \to P (s) \in N$
88		neeq1	$⊢ i = P (s) \to (i \neq j \leftrightarrow P (s) \neq j)$
89		oveq1	$⊢ i = P (s) \to i M j = P (s) M j$
90	89	eqeq1d	$⊢ i = P (s) \to (i M j = \underset{˙}{0} \leftrightarrow P (s) M j = \underset{˙}{0})$
91	88 90	imbi12d	$⊢ i = P (s) \to ((i \neq j \to i M j = \underset{˙}{0}) \leftrightarrow (P (s) \neq j \to P (s) M j = \underset{˙}{0}))$
92		neeq2	$⊢ j = s \to (P (s) \neq j \leftrightarrow P (s) \neq s)$
93		oveq2	$⊢ j = s \to P (s) M j = P (s) M s$
94	93	eqeq1d	$⊢ j = s \to (P (s) M j = \underset{˙}{0} \leftrightarrow P (s) M s = \underset{˙}{0})$
95	92 94	imbi12d	$⊢ j = s \to ((P (s) \neq j \to P (s) M j = \underset{˙}{0}) \leftrightarrow (P (s) \neq s \to P (s) M s = \underset{˙}{0}))$
96	91 95	rspc2v	$⊢ (P (s) \in N \land s \in N) \to (\forall i \in N \forall j \in N (i \neq j \to i M j = \underset{˙}{0}) \to (P (s) \neq s \to P (s) M s = \underset{˙}{0}))$
97	87 86 96	syl2anc	$⊢ ((R \in CRing \land N \in Fin \land M \in B) \land (P \in H \land s \in dom (P ∖ I))) \to (\forall i \in N \forall j \in N (i \neq j \to i M j = \underset{˙}{0}) \to (P (s) \neq s \to P (s) M s = \underset{˙}{0}))$
98	97	impancom	$⊢ ((R \in CRing \land N \in Fin \land M \in B) \land \forall i \in N \forall j \in N (i \neq j \to i M j = \underset{˙}{0})) \to ((P \in H \land s \in dom (P ∖ I)) \to (P (s) \neq s \to P (s) M s = \underset{˙}{0}))$
99	98	imp	$⊢ (((R \in CRing \land N \in Fin \land M \in B) \land \forall i \in N \forall j \in N (i \neq j \to i M j = \underset{˙}{0})) \land (P \in H \land s \in dom (P ∖ I))) \to (P (s) \neq s \to P (s) M s = \underset{˙}{0})$
100	81 99	mpd	$⊢ (((R \in CRing \land N \in Fin \land M \in B) \land \forall i \in N \forall j \in N (i \neq j \to i M j = \underset{˙}{0})) \land (P \in H \land s \in dom (P ∖ I))) \to P (s) M s = \underset{˙}{0}$
101	76 100	eqtrd	$⊢ (((R \in CRing \land N \in Fin \land M \in B) \land \forall i \in N \forall j \in N (i \neq j \to i M j = \underset{˙}{0})) \land (P \in H \land s \in dom (P ∖ I))) \to \underset{k \in \{s\}}{\sum_{G}} (P (k) M k) = \underset{˙}{0}$
102	101	oveq1d	$⊢ (((R \in CRing \land N \in Fin \land M \in B) \land \forall i \in N \forall j \in N (i \neq j \to i M j = \underset{˙}{0})) \land (P \in H \land s \in dom (P ∖ I))) \to (\underset{k \in \{s\}}{\sum_{G}}, (P (k) M k)) \cdot_{R} (\underset{k \in N ∖ \{s\}}{\sum_{G}}, (P (k) M k)) = \underset{˙}{0} \cdot_{R} (\underset{k \in N ∖ \{s\}}{\sum_{G}}, (P (k) M k))$
103	61	3ad2ant1	$⊢ (R \in CRing \land N \in Fin \land M \in B) \to R \in Ring$
104	103	ad2antrr	$⊢ (((R \in CRing \land N \in Fin \land M \in B) \land \forall i \in N \forall j \in N (i \neq j \to i M j = \underset{˙}{0})) \land (P \in H \land s \in dom (P ∖ I))) \to R \in Ring$
105	28	adantr	$⊢ ((R \in CRing \land N \in Fin \land M \in B) \land P \in H) \to G \in CMnd$
106		simpl2	$⊢ ((R \in CRing \land N \in Fin \land M \in B) \land P \in H) \to N \in Fin$
107		difss	$⊢ N ∖ \{s\} \subseteq N$
108		ssfi	$⊢ (N \in Fin \land N ∖ \{s\} \subseteq N) \to N ∖ \{s\} \in Fin$
109	106 107 108	sylancl	$⊢ ((R \in CRing \land N \in Fin \land M \in B) \land P \in H) \to N ∖ \{s\} \in Fin$
110	35	ad2antrr	$⊢ (((R \in CRing \land N \in Fin \land M \in B) \land P \in H) \land k \in (N ∖ \{s\})) \to M : N \times N ⟶ {Base}_{R}$
111	83	adantr	$⊢ (((R \in CRing \land N \in Fin \land M \in B) \land P \in H) \land k \in (N ∖ \{s\})) \to P : N ⟶ N$
112		eldifi	$⊢ k \in (N ∖ \{s\}) \to k \in N$
113	112	adantl	$⊢ (((R \in CRing \land N \in Fin \land M \in B) \land P \in H) \land k \in (N ∖ \{s\})) \to k \in N$
114	111 113	ffvelcdmd	$⊢ (((R \in CRing \land N \in Fin \land M \in B) \land P \in H) \land k \in (N ∖ \{s\})) \to P (k) \in N$
115	110 114 113	fovcdmd	$⊢ (((R \in CRing \land N \in Fin \land M \in B) \land P \in H) \land k \in (N ∖ \{s\})) \to P (k) M k \in {Base}_{R}$
116	115	ralrimiva	$⊢ ((R \in CRing \land N \in Fin \land M \in B) \land P \in H) \to \forall k \in (N ∖ \{s\}) P (k) M k \in {Base}_{R}$
117	36 105 109 116	gsummptcl	$⊢ ((R \in CRing \land N \in Fin \land M \in B) \land P \in H) \to \underset{k \in N ∖ \{s\}}{\sum_{G}} (P (k) M k) \in {Base}_{R}$
118	117	ad2ant2r	$⊢ (((R \in CRing \land N \in Fin \land M \in B) \land \forall i \in N \forall j \in N (i \neq j \to i M j = \underset{˙}{0})) \land (P \in H \land s \in dom (P ∖ I))) \to \underset{k \in N ∖ \{s\}}{\sum_{G}} (P (k) M k) \in {Base}_{R}$
119	31 25 5	ringlz	$⊢ (R \in Ring \land \underset{k \in N ∖ \{s\}}{\sum_{G}} (P (k) M k) \in {Base}_{R}) \to \underset{˙}{0} \cdot_{R} (\underset{k \in N ∖ \{s\}}{\sum_{G}}, (P (k) M k)) = \underset{˙}{0}$
120	104 118 119	syl2anc	$⊢ (((R \in CRing \land N \in Fin \land M \in B) \land \forall i \in N \forall j \in N (i \neq j \to i M j = \underset{˙}{0})) \land (P \in H \land s \in dom (P ∖ I))) \to \underset{˙}{0} \cdot_{R} (\underset{k \in N ∖ \{s\}}{\sum_{G}}, (P (k) M k)) = \underset{˙}{0}$
121	60 102 120	3eqtrd	$⊢ (((R \in CRing \land N \in Fin \land M \in B) \land \forall i \in N \forall j \in N (i \neq j \to i M j = \underset{˙}{0})) \land (P \in H \land s \in dom (P ∖ I))) \to \underset{k \in N}{\sum_{G}} (P (k) M k) = \underset{˙}{0}$
122	121	expr	$⊢ (((R \in CRing \land N \in Fin \land M \in B) \land \forall i \in N \forall j \in N (i \neq j \to i M j = \underset{˙}{0})) \land P \in H) \to (s \in dom (P ∖ I) \to \underset{k \in N}{\sum_{G}} (P (k) M k) = \underset{˙}{0})$
123	122	exlimdv	$⊢ (((R \in CRing \land N \in Fin \land M \in B) \land \forall i \in N \forall j \in N (i \neq j \to i M j = \underset{˙}{0})) \land P \in H) \to (\exists s s \in dom (P ∖ I) \to \underset{k \in N}{\sum_{G}} (P (k) M k) = \underset{˙}{0})$
124	23 123	biimtrid	$⊢ (((R \in CRing \land N \in Fin \land M \in B) \land \forall i \in N \forall j \in N (i \neq j \to i M j = \underset{˙}{0})) \land P \in H) \to (dom (P ∖ I) \neq \emptyset \to \underset{k \in N}{\sum_{G}} (P (k) M k) = \underset{˙}{0})$
125	22 124	sylbid	$⊢ (((R \in CRing \land N \in Fin \land M \in B) \land \forall i \in N \forall j \in N (i \neq j \to i M j = \underset{˙}{0})) \land P \in H) \to (P \neq {I ↾}_{N} \to \underset{k \in N}{\sum_{G}} (P (k) M k) = \underset{˙}{0})$
126	125	expimpd	$⊢ ((R \in CRing \land N \in Fin \land M \in B) \land \forall i \in N \forall j \in N (i \neq j \to i M j = \underset{˙}{0})) \to ((P \in H \land P \neq {I ↾}_{N}) \to \underset{k \in N}{\sum_{G}} (P (k) M k) = \underset{˙}{0})$
127	126	3impia	$⊢ ((R \in CRing \land N \in Fin \land M \in B) \land \forall i \in N \forall j \in N (i \neq j \to i M j = \underset{˙}{0}) \land (P \in H \land P \neq {I ↾}_{N})) \to \underset{k \in N}{\sum_{G}} (P (k) M k) = \underset{˙}{0}$
128	13 127	oveq12d	$⊢ ((R \in CRing \land N \in Fin \land M \in B) \land \forall i \in N \forall j \in N (i \neq j \to i M j = \underset{˙}{0}) \land (P \in H \land P \neq {I ↾}_{N})) \to (Z \circ S) (P) \underset{˙}{\cdot} (\underset{k \in N}{\sum_{G}}, (P (k) M k)) = (ℤRHom (R) \circ pmSgn (N)) (P) \underset{˙}{\cdot} \underset{˙}{0}$
129		3simpa	$⊢ (R \in CRing \land N \in Fin \land M \in B) \to (R \in CRing \land N \in Fin)$
130		simpl	$⊢ (P \in H \land P \neq {I ↾}_{N}) \to P \in H$
131	61	ad2antrr	$⊢ ((R \in CRing \land N \in Fin) \land P \in H) \to R \in Ring$
132		zrhpsgnmhm	$⊢ (R \in Ring \land N \in Fin) \to ℤRHom (R) \circ pmSgn (N) \in (SymGrp (N) MndHom {mulGrp}_{R})$
133	61 132	sylan	$⊢ (R \in CRing \land N \in Fin) \to ℤRHom (R) \circ pmSgn (N) \in (SymGrp (N) MndHom {mulGrp}_{R})$
134		eqid	$⊢ {Base}_{{mulGrp}_{R}} = {Base}_{{mulGrp}_{R}}$
135	6 134	mhmf	$⊢ ℤRHom (R) \circ pmSgn (N) \in (SymGrp (N) MndHom {mulGrp}_{R}) \to (ℤRHom (R) \circ pmSgn (N)) : H ⟶ {Base}_{{mulGrp}_{R}}$
136	133 135	syl	$⊢ (R \in CRing \land N \in Fin) \to (ℤRHom (R) \circ pmSgn (N)) : H ⟶ {Base}_{{mulGrp}_{R}}$
137	136	ffvelcdmda	$⊢ ((R \in CRing \land N \in Fin) \land P \in H) \to (ℤRHom (R) \circ pmSgn (N)) (P) \in {Base}_{{mulGrp}_{R}}$
138		eqid	$⊢ {mulGrp}_{R} = {mulGrp}_{R}$
139	138 31	mgpbas	$⊢ {Base}_{R} = {Base}_{{mulGrp}_{R}}$
140	139	eqcomi	$⊢ {Base}_{{mulGrp}_{R}} = {Base}_{R}$
141	140 9 5	ringrz	$⊢ (R \in Ring \land (ℤRHom (R) \circ pmSgn (N)) (P) \in {Base}_{{mulGrp}_{R}}) \to (ℤRHom (R) \circ pmSgn (N)) (P) \underset{˙}{\cdot} \underset{˙}{0} = \underset{˙}{0}$
142	131 137 141	syl2anc	$⊢ ((R \in CRing \land N \in Fin) \land P \in H) \to (ℤRHom (R) \circ pmSgn (N)) (P) \underset{˙}{\cdot} \underset{˙}{0} = \underset{˙}{0}$
143	129 130 142	syl2an	$⊢ ((R \in CRing \land N \in Fin \land M \in B) \land (P \in H \land P \neq {I ↾}_{N})) \to (ℤRHom (R) \circ pmSgn (N)) (P) \underset{˙}{\cdot} \underset{˙}{0} = \underset{˙}{0}$
144	143	3adant2	$⊢ ((R \in CRing \land N \in Fin \land M \in B) \land \forall i \in N \forall j \in N (i \neq j \to i M j = \underset{˙}{0}) \land (P \in H \land P \neq {I ↾}_{N})) \to (ℤRHom (R) \circ pmSgn (N)) (P) \underset{˙}{\cdot} \underset{˙}{0} = \underset{˙}{0}$
145	128 144	eqtrd	$⊢ ((R \in CRing \land N \in Fin \land M \in B) \land \forall i \in N \forall j \in N (i \neq j \to i M j = \underset{˙}{0}) \land (P \in H \land P \neq {I ↾}_{N})) \to (Z \circ S) (P) \underset{˙}{\cdot} (\underset{k \in N}{\sum_{G}}, (P (k) M k)) = \underset{˙}{0}$

Metamath Proof Explorer

Theorem mdetdiaglem

Proof