m1detdiag

Description: The determinant of a 1-dimensional matrix equals its (single) entry. (Contributed by AV, 6-Aug-2019)

	Ref	Expression
Hypotheses	mdetdiag.d	$⊢ D = N maDet R$
	mdetdiag.a	$⊢ A = N Mat R$
	mdetdiag.b	$⊢ B = {Base}_{A}$
Assertion	m1detdiag	$⊢ (R \in CRing \land (N = \{I\} \land I \in V) \land M \in B) \to D (M) = I M I$

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		eqid	$⊢ {Base}_{SymGrp (N)} = {Base}_{SymGrp (N)}$
5		eqid	$⊢ ℤRHom (R) = ℤRHom (R)$
6		eqid	$⊢ pmSgn (N) = pmSgn (N)$
7		eqid	$⊢ \cdot_{R} = \cdot_{R}$
8		eqid	$⊢ {mulGrp}_{R} = {mulGrp}_{R}$
9	1 2 3 4 5 6 7 8	mdetleib	$⊢ M \in B \to D (M) = \underset{p \in {Base}_{SymGrp (N)}}{\sum_{R}} ((ℤRHom (R) \circ pmSgn (N)) (p) \cdot_{R} (\underset{x \in N}{\sum_{{mulGrp}_{R}}}, (p (x) M x)))$
10	9	3ad2ant3	$⊢ (R \in CRing \land (N = \{I\} \land I \in V) \land M \in B) \to D (M) = \underset{p \in {Base}_{SymGrp (N)}}{\sum_{R}} ((ℤRHom (R) \circ pmSgn (N)) (p) \cdot_{R} (\underset{x \in N}{\sum_{{mulGrp}_{R}}}, (p (x) M x)))$
11		2fveq3	$⊢ N = \{I\} \to {Base}_{SymGrp (N)} = {Base}_{SymGrp (\{I\})}$
12	11	adantr	$⊢ (N = \{I\} \land I \in V) \to {Base}_{SymGrp (N)} = {Base}_{SymGrp (\{I\})}$
13	12	3ad2ant2	$⊢ (R \in CRing \land (N = \{I\} \land I \in V) \land M \in B) \to {Base}_{SymGrp (N)} = {Base}_{SymGrp (\{I\})}$
14		simp2r	$⊢ (R \in CRing \land (N = \{I\} \land I \in V) \land M \in B) \to I \in V$
15		eqid	$⊢ SymGrp (\{I\}) = SymGrp (\{I\})$
16		eqid	$⊢ {Base}_{SymGrp (\{I\})} = {Base}_{SymGrp (\{I\})}$
17		eqid	$⊢ \{I\} = \{I\}$
18	15 16 17	symg1bas	$⊢ I \in V \to {Base}_{SymGrp (\{I\})} = \{\{⟨I, I⟩\}\}$
19	14 18	syl	$⊢ (R \in CRing \land (N = \{I\} \land I \in V) \land M \in B) \to {Base}_{SymGrp (\{I\})} = \{\{⟨I, I⟩\}\}$
20	13 19	eqtrd	$⊢ (R \in CRing \land (N = \{I\} \land I \in V) \land M \in B) \to {Base}_{SymGrp (N)} = \{\{⟨I, I⟩\}\}$
21	20	mpteq1d	$⊢ (R \in CRing \land (N = \{I\} \land I \in V) \land M \in B) \to (p \in {Base}_{SymGrp (N)} ⟼ (ℤRHom (R) \circ pmSgn (N)) (p) \cdot_{R} (\underset{x \in N}{\sum_{{mulGrp}_{R}}}, (p (x) M x))) = (p \in \{\{⟨I, I⟩\}\} ⟼ (ℤRHom (R) \circ pmSgn (N)) (p) \cdot_{R} (\underset{x \in N}{\sum_{{mulGrp}_{R}}}, (p (x) M x)))$
22		snex	$⊢ \{⟨I, I⟩\} \in V$
23	22	a1i	$⊢ (R \in CRing \land (N = \{I\} \land I \in V) \land M \in B) \to \{⟨I, I⟩\} \in V$
24		ovex	$⊢ (ℤRHom (R) \circ pmSgn (N)) (\{⟨I, I⟩\}) \cdot_{R} (\underset{x \in N}{\sum_{{mulGrp}_{R}}}, (\{⟨I, I⟩\} (x) M x)) \in V$
25		fveq2	$⊢ p = \{⟨I, I⟩\} \to (ℤRHom (R) \circ pmSgn (N)) (p) = (ℤRHom (R) \circ pmSgn (N)) (\{⟨I, I⟩\})$
26		fveq1	$⊢ p = \{⟨I, I⟩\} \to p (x) = \{⟨I, I⟩\} (x)$
27	26	oveq1d	$⊢ p = \{⟨I, I⟩\} \to p (x) M x = \{⟨I, I⟩\} (x) M x$
28	27	mpteq2dv	$⊢ p = \{⟨I, I⟩\} \to (x \in N ⟼ p (x) M x) = (x \in N ⟼ \{⟨I, I⟩\} (x) M x)$
29	28	oveq2d	$⊢ p = \{⟨I, I⟩\} \to \underset{x \in N}{\sum_{{mulGrp}_{R}}} (p (x) M x) = \underset{x \in N}{\sum_{{mulGrp}_{R}}} (\{⟨I, I⟩\} (x) M x)$
30	25 29	oveq12d	$⊢ p = \{⟨I, I⟩\} \to (ℤRHom (R) \circ pmSgn (N)) (p) \cdot_{R} (\underset{x \in N}{\sum_{{mulGrp}_{R}}}, (p (x) M x)) = (ℤRHom (R) \circ pmSgn (N)) (\{⟨I, I⟩\}) \cdot_{R} (\underset{x \in N}{\sum_{{mulGrp}_{R}}}, (\{⟨I, I⟩\} (x) M x))$
31	30	fmptsng	$⊢ (\{⟨I, I⟩\} \in V \land (ℤRHom (R) \circ pmSgn (N)) (\{⟨I, I⟩\}) \cdot_{R} (\underset{x \in N}{\sum_{{mulGrp}_{R}}}, (\{⟨I, I⟩\} (x) M x)) \in V) \to \{⟨\{⟨I, I⟩\}, (ℤRHom (R) \circ pmSgn (N)) (\{⟨I, I⟩\}) \cdot_{R} (\underset{x \in N}{\sum_{{mulGrp}_{R}}}, (\{⟨I, I⟩\} (x) M x))⟩\} = (p \in \{\{⟨I, I⟩\}\} ⟼ (ℤRHom (R) \circ pmSgn (N)) (p) \cdot_{R} (\underset{x \in N}{\sum_{{mulGrp}_{R}}}, (p (x) M x)))$
32	31	eqcomd	$⊢ (\{⟨I, I⟩\} \in V \land (ℤRHom (R) \circ pmSgn (N)) (\{⟨I, I⟩\}) \cdot_{R} (\underset{x \in N}{\sum_{{mulGrp}_{R}}}, (\{⟨I, I⟩\} (x) M x)) \in V) \to (p \in \{\{⟨I, I⟩\}\} ⟼ (ℤRHom (R) \circ pmSgn (N)) (p) \cdot_{R} (\underset{x \in N}{\sum_{{mulGrp}_{R}}}, (p (x) M x))) = \{⟨\{⟨I, I⟩\}, (ℤRHom (R) \circ pmSgn (N)) (\{⟨I, I⟩\}) \cdot_{R} (\underset{x \in N}{\sum_{{mulGrp}_{R}}}, (\{⟨I, I⟩\} (x) M x))⟩\}$
33	23 24 32	sylancl	$⊢ (R \in CRing \land (N = \{I\} \land I \in V) \land M \in B) \to (p \in \{\{⟨I, I⟩\}\} ⟼ (ℤRHom (R) \circ pmSgn (N)) (p) \cdot_{R} (\underset{x \in N}{\sum_{{mulGrp}_{R}}}, (p (x) M x))) = \{⟨\{⟨I, I⟩\}, (ℤRHom (R) \circ pmSgn (N)) (\{⟨I, I⟩\}) \cdot_{R} (\underset{x \in N}{\sum_{{mulGrp}_{R}}}, (\{⟨I, I⟩\} (x) M x))⟩\}$
34		eqid	$⊢ SymGrp (N) = SymGrp (N)$
35		eqid	$⊢ \{b \in {Base}_{SymGrp (N)} \| dom (b ∖ I) \in Fin\} = \{b \in {Base}_{SymGrp (N)} \| dom (b ∖ I) \in Fin\}$
36	34 4 35 6	psgnfn	$⊢ pmSgn (N) Fn \{b \in {Base}_{SymGrp (N)} \| dom (b ∖ I) \in Fin\}$
37	18	adantl	$⊢ (N = \{I\} \land I \in V) \to {Base}_{SymGrp (\{I\})} = \{\{⟨I, I⟩\}\}$
38	12 37	eqtrd	$⊢ (N = \{I\} \land I \in V) \to {Base}_{SymGrp (N)} = \{\{⟨I, I⟩\}\}$
39	38	3ad2ant2	$⊢ (R \in CRing \land (N = \{I\} \land I \in V) \land M \in B) \to {Base}_{SymGrp (N)} = \{\{⟨I, I⟩\}\}$
40		rabeq	$⊢ {Base}_{SymGrp (N)} = \{\{⟨I, I⟩\}\} \to \{b \in {Base}_{SymGrp (N)} \| dom (b ∖ I) \in Fin\} = \{b \in \{\{⟨I, I⟩\}\} \| dom (b ∖ I) \in Fin\}$
41	39 40	syl	$⊢ (R \in CRing \land (N = \{I\} \land I \in V) \land M \in B) \to \{b \in {Base}_{SymGrp (N)} \| dom (b ∖ I) \in Fin\} = \{b \in \{\{⟨I, I⟩\}\} \| dom (b ∖ I) \in Fin\}$
42		difeq1	$⊢ b = \{⟨I, I⟩\} \to b ∖ I = \{⟨I, I⟩\} ∖ I$
43	42	dmeqd	$⊢ b = \{⟨I, I⟩\} \to dom (b ∖ I) = dom (\{⟨I, I⟩\} ∖ I)$
44	43	eleq1d	$⊢ b = \{⟨I, I⟩\} \to (dom (b ∖ I) \in Fin \leftrightarrow dom (\{⟨I, I⟩\} ∖ I) \in Fin)$
45	44	rabsnif	$⊢ \{b \in \{\{⟨I, I⟩\}\} \| dom (b ∖ I) \in Fin\} = if (dom (\{⟨I, I⟩\} ∖ I) \in Fin, \{\{⟨I, I⟩\}\}, \emptyset)$
46	45	a1i	$⊢ (R \in CRing \land (N = \{I\} \land I \in V) \land M \in B) \to \{b \in \{\{⟨I, I⟩\}\} \| dom (b ∖ I) \in Fin\} = if (dom (\{⟨I, I⟩\} ∖ I) \in Fin, \{\{⟨I, I⟩\}\}, \emptyset)$
47		restidsing	$⊢ {I ↾}_{\{I\}} = \{I\} \times \{I\}$
48		xpsng	$⊢ (I \in V \land I \in V) \to \{I\} \times \{I\} = \{⟨I, I⟩\}$
49	48	anidms	$⊢ I \in V \to \{I\} \times \{I\} = \{⟨I, I⟩\}$
50	47 49	eqtr2id	$⊢ I \in V \to \{⟨I, I⟩\} = {I ↾}_{\{I\}}$
51		fnsng	$⊢ (I \in V \land I \in V) \to \{⟨I, I⟩\} Fn \{I\}$
52	51	anidms	$⊢ I \in V \to \{⟨I, I⟩\} Fn \{I\}$
53		fnnfpeq0	$⊢ \{⟨I, I⟩\} Fn \{I\} \to (dom (\{⟨I, I⟩\} ∖ I) = \emptyset \leftrightarrow \{⟨I, I⟩\} = {I ↾}_{\{I\}})$
54	52 53	syl	$⊢ I \in V \to (dom (\{⟨I, I⟩\} ∖ I) = \emptyset \leftrightarrow \{⟨I, I⟩\} = {I ↾}_{\{I\}})$
55	50 54	mpbird	$⊢ I \in V \to dom (\{⟨I, I⟩\} ∖ I) = \emptyset$
56		0fi	$⊢ \emptyset \in Fin$
57	55 56	eqeltrdi	$⊢ I \in V \to dom (\{⟨I, I⟩\} ∖ I) \in Fin$
58	57	adantl	$⊢ (N = \{I\} \land I \in V) \to dom (\{⟨I, I⟩\} ∖ I) \in Fin$
59	58	3ad2ant2	$⊢ (R \in CRing \land (N = \{I\} \land I \in V) \land M \in B) \to dom (\{⟨I, I⟩\} ∖ I) \in Fin$
60	59	iftrued	$⊢ (R \in CRing \land (N = \{I\} \land I \in V) \land M \in B) \to if (dom (\{⟨I, I⟩\} ∖ I) \in Fin, \{\{⟨I, I⟩\}\}, \emptyset) = \{\{⟨I, I⟩\}\}$
61	41 46 60	3eqtrrd	$⊢ (R \in CRing \land (N = \{I\} \land I \in V) \land M \in B) \to \{\{⟨I, I⟩\}\} = \{b \in {Base}_{SymGrp (N)} \| dom (b ∖ I) \in Fin\}$
62	61	fneq2d	$⊢ (R \in CRing \land (N = \{I\} \land I \in V) \land M \in B) \to (pmSgn (N) Fn \{\{⟨I, I⟩\}\} \leftrightarrow pmSgn (N) Fn \{b \in {Base}_{SymGrp (N)} \| dom (b ∖ I) \in Fin\})$
63	36 62	mpbiri	$⊢ (R \in CRing \land (N = \{I\} \land I \in V) \land M \in B) \to pmSgn (N) Fn \{\{⟨I, I⟩\}\}$
64	22	snid	$⊢ \{⟨I, I⟩\} \in \{\{⟨I, I⟩\}\}$
65		fvco2	$⊢ (pmSgn (N) Fn \{\{⟨I, I⟩\}\} \land \{⟨I, I⟩\} \in \{\{⟨I, I⟩\}\}) \to (ℤRHom (R) \circ pmSgn (N)) (\{⟨I, I⟩\}) = ℤRHom (R) (pmSgn (N) (\{⟨I, I⟩\}))$
66	63 64 65	sylancl	$⊢ (R \in CRing \land (N = \{I\} \land I \in V) \land M \in B) \to (ℤRHom (R) \circ pmSgn (N)) (\{⟨I, I⟩\}) = ℤRHom (R) (pmSgn (N) (\{⟨I, I⟩\}))$
67		fveq2	$⊢ N = \{I\} \to pmSgn (N) = pmSgn (\{I\})$
68	67	adantr	$⊢ (N = \{I\} \land I \in V) \to pmSgn (N) = pmSgn (\{I\})$
69	68	3ad2ant2	$⊢ (R \in CRing \land (N = \{I\} \land I \in V) \land M \in B) \to pmSgn (N) = pmSgn (\{I\})$
70	69	fveq1d	$⊢ (R \in CRing \land (N = \{I\} \land I \in V) \land M \in B) \to pmSgn (N) (\{⟨I, I⟩\}) = pmSgn (\{I\}) (\{⟨I, I⟩\})$
71		snidg	$⊢ \{⟨I, I⟩\} \in V \to \{⟨I, I⟩\} \in \{\{⟨I, I⟩\}\}$
72	22 71	mp1i	$⊢ I \in V \to \{⟨I, I⟩\} \in \{\{⟨I, I⟩\}\}$
73	72 18	eleqtrrd	$⊢ I \in V \to \{⟨I, I⟩\} \in {Base}_{SymGrp (\{I\})}$
74	73	ancli	$⊢ I \in V \to (I \in V \land \{⟨I, I⟩\} \in {Base}_{SymGrp (\{I\})})$
75	74	adantl	$⊢ (N = \{I\} \land I \in V) \to (I \in V \land \{⟨I, I⟩\} \in {Base}_{SymGrp (\{I\})})$
76	75	3ad2ant2	$⊢ (R \in CRing \land (N = \{I\} \land I \in V) \land M \in B) \to (I \in V \land \{⟨I, I⟩\} \in {Base}_{SymGrp (\{I\})})$
77		eqid	$⊢ pmSgn (\{I\}) = pmSgn (\{I\})$
78	17 15 16 77	psgnsn	$⊢ (I \in V \land \{⟨I, I⟩\} \in {Base}_{SymGrp (\{I\})}) \to pmSgn (\{I\}) (\{⟨I, I⟩\}) = 1$
79	76 78	syl	$⊢ (R \in CRing \land (N = \{I\} \land I \in V) \land M \in B) \to pmSgn (\{I\}) (\{⟨I, I⟩\}) = 1$
80	70 79	eqtrd	$⊢ (R \in CRing \land (N = \{I\} \land I \in V) \land M \in B) \to pmSgn (N) (\{⟨I, I⟩\}) = 1$
81	80	fveq2d	$⊢ (R \in CRing \land (N = \{I\} \land I \in V) \land M \in B) \to ℤRHom (R) (pmSgn (N) (\{⟨I, I⟩\})) = ℤRHom (R) (1)$
82		crngring	$⊢ R \in CRing \to R \in Ring$
83	82	3ad2ant1	$⊢ (R \in CRing \land (N = \{I\} \land I \in V) \land M \in B) \to R \in Ring$
84		eqid	$⊢ 1_{R} = 1_{R}$
85	5 84	zrh1	$⊢ R \in Ring \to ℤRHom (R) (1) = 1_{R}$
86	83 85	syl	$⊢ (R \in CRing \land (N = \{I\} \land I \in V) \land M \in B) \to ℤRHom (R) (1) = 1_{R}$
87	66 81 86	3eqtrd	$⊢ (R \in CRing \land (N = \{I\} \land I \in V) \land M \in B) \to (ℤRHom (R) \circ pmSgn (N)) (\{⟨I, I⟩\}) = 1_{R}$
88		simp2l	$⊢ (R \in CRing \land (N = \{I\} \land I \in V) \land M \in B) \to N = \{I\}$
89	88	mpteq1d	$⊢ (R \in CRing \land (N = \{I\} \land I \in V) \land M \in B) \to (x \in N ⟼ \{⟨I, I⟩\} (x) M x) = (x \in \{I\} ⟼ \{⟨I, I⟩\} (x) M x)$
90	89	oveq2d	$⊢ (R \in CRing \land (N = \{I\} \land I \in V) \land M \in B) \to \underset{x \in N}{\sum_{{mulGrp}_{R}}} (\{⟨I, I⟩\} (x) M x) = \underset{x \in \{I\}}{\sum_{{mulGrp}_{R}}} (\{⟨I, I⟩\} (x) M x)$
91	8	ringmgp	$⊢ R \in Ring \to {mulGrp}_{R} \in Mnd$
92	82 91	syl	$⊢ R \in CRing \to {mulGrp}_{R} \in Mnd$
93	92	3ad2ant1	$⊢ (R \in CRing \land (N = \{I\} \land I \in V) \land M \in B) \to {mulGrp}_{R} \in Mnd$
94		snidg	$⊢ I \in V \to I \in \{I\}$
95	94	adantl	$⊢ (N = \{I\} \land I \in V) \to I \in \{I\}$
96		eleq2	$⊢ N = \{I\} \to (I \in N \leftrightarrow I \in \{I\})$
97	96	adantr	$⊢ (N = \{I\} \land I \in V) \to (I \in N \leftrightarrow I \in \{I\})$
98	95 97	mpbird	$⊢ (N = \{I\} \land I \in V) \to I \in N$
99	3	eleq2i	$⊢ M \in B \leftrightarrow M \in {Base}_{A}$
100	99	biimpi	$⊢ M \in B \to M \in {Base}_{A}$
101		simpl	$⊢ (I \in N \land M \in {Base}_{A}) \to I \in N$
102		simpr	$⊢ (I \in N \land M \in {Base}_{A}) \to M \in {Base}_{A}$
103	101 101 102	3jca	$⊢ (I \in N \land M \in {Base}_{A}) \to (I \in N \land I \in N \land M \in {Base}_{A})$
104	98 100 103	syl2an	$⊢ ((N = \{I\} \land I \in V) \land M \in B) \to (I \in N \land I \in N \land M \in {Base}_{A})$
105	104	3adant1	$⊢ (R \in CRing \land (N = \{I\} \land I \in V) \land M \in B) \to (I \in N \land I \in N \land M \in {Base}_{A})$
106		eqid	$⊢ {Base}_{R} = {Base}_{R}$
107	2 106	matecl	$⊢ (I \in N \land I \in N \land M \in {Base}_{A}) \to I M I \in {Base}_{R}$
108	105 107	syl	$⊢ (R \in CRing \land (N = \{I\} \land I \in V) \land M \in B) \to I M I \in {Base}_{R}$
109	8 106	mgpbas	$⊢ {Base}_{R} = {Base}_{{mulGrp}_{R}}$
110	108 109	eleqtrdi	$⊢ (R \in CRing \land (N = \{I\} \land I \in V) \land M \in B) \to I M I \in {Base}_{{mulGrp}_{R}}$
111		eqid	$⊢ {Base}_{{mulGrp}_{R}} = {Base}_{{mulGrp}_{R}}$
112		fveq2	$⊢ x = I \to \{⟨I, I⟩\} (x) = \{⟨I, I⟩\} (I)$
113		eqvisset	$⊢ x = I \to I \in V$
114		fvsng	$⊢ (I \in V \land I \in V) \to \{⟨I, I⟩\} (I) = I$
115	113 113 114	syl2anc	$⊢ x = I \to \{⟨I, I⟩\} (I) = I$
116	112 115	eqtrd	$⊢ x = I \to \{⟨I, I⟩\} (x) = I$
117		id	$⊢ x = I \to x = I$
118	116 117	oveq12d	$⊢ x = I \to \{⟨I, I⟩\} (x) M x = I M I$
119	111 118	gsumsn	$⊢ ({mulGrp}_{R} \in Mnd \land I \in V \land I M I \in {Base}_{{mulGrp}_{R}}) \to \underset{x \in \{I\}}{\sum_{{mulGrp}_{R}}} (\{⟨I, I⟩\} (x) M x) = I M I$
120	93 14 110 119	syl3anc	$⊢ (R \in CRing \land (N = \{I\} \land I \in V) \land M \in B) \to \underset{x \in \{I\}}{\sum_{{mulGrp}_{R}}} (\{⟨I, I⟩\} (x) M x) = I M I$
121	90 120	eqtrd	$⊢ (R \in CRing \land (N = \{I\} \land I \in V) \land M \in B) \to \underset{x \in N}{\sum_{{mulGrp}_{R}}} (\{⟨I, I⟩\} (x) M x) = I M I$
122	87 121	oveq12d	$⊢ (R \in CRing \land (N = \{I\} \land I \in V) \land M \in B) \to (ℤRHom (R) \circ pmSgn (N)) (\{⟨I, I⟩\}) \cdot_{R} (\underset{x \in N}{\sum_{{mulGrp}_{R}}}, (\{⟨I, I⟩\} (x) M x)) = 1_{R} \cdot_{R} (I M I)$
123	98	3ad2ant2	$⊢ (R \in CRing \land (N = \{I\} \land I \in V) \land M \in B) \to I \in N$
124	100	3ad2ant3	$⊢ (R \in CRing \land (N = \{I\} \land I \in V) \land M \in B) \to M \in {Base}_{A}$
125	123 123 124 107	syl3anc	$⊢ (R \in CRing \land (N = \{I\} \land I \in V) \land M \in B) \to I M I \in {Base}_{R}$
126	106 7 84	ringlidm	$⊢ (R \in Ring \land I M I \in {Base}_{R}) \to 1_{R} \cdot_{R} (I M I) = I M I$
127	83 125 126	syl2anc	$⊢ (R \in CRing \land (N = \{I\} \land I \in V) \land M \in B) \to 1_{R} \cdot_{R} (I M I) = I M I$
128	122 127	eqtrd	$⊢ (R \in CRing \land (N = \{I\} \land I \in V) \land M \in B) \to (ℤRHom (R) \circ pmSgn (N)) (\{⟨I, I⟩\}) \cdot_{R} (\underset{x \in N}{\sum_{{mulGrp}_{R}}}, (\{⟨I, I⟩\} (x) M x)) = I M I$
129	128	opeq2d	$⊢ (R \in CRing \land (N = \{I\} \land I \in V) \land M \in B) \to ⟨\{⟨I, I⟩\}, (ℤRHom (R) \circ pmSgn (N)) (\{⟨I, I⟩\}) \cdot_{R} (\underset{x \in N}{\sum_{{mulGrp}_{R}}}, (\{⟨I, I⟩\} (x) M x))⟩ = ⟨\{⟨I, I⟩\}, I M I⟩$
130	129	sneqd	$⊢ (R \in CRing \land (N = \{I\} \land I \in V) \land M \in B) \to \{⟨\{⟨I, I⟩\}, (ℤRHom (R) \circ pmSgn (N)) (\{⟨I, I⟩\}) \cdot_{R} (\underset{x \in N}{\sum_{{mulGrp}_{R}}}, (\{⟨I, I⟩\} (x) M x))⟩\} = \{⟨\{⟨I, I⟩\}, I M I⟩\}$
131		ovex	$⊢ I M I \in V$
132		eqidd	$⊢ y = \{⟨I, I⟩\} \to I M I = I M I$
133	132	fmptsng	$⊢ (\{⟨I, I⟩\} \in V \land I M I \in V) \to \{⟨\{⟨I, I⟩\}, I M I⟩\} = (y \in \{\{⟨I, I⟩\}\} ⟼ I M I)$
134	23 131 133	sylancl	$⊢ (R \in CRing \land (N = \{I\} \land I \in V) \land M \in B) \to \{⟨\{⟨I, I⟩\}, I M I⟩\} = (y \in \{\{⟨I, I⟩\}\} ⟼ I M I)$
135	130 134	eqtrd	$⊢ (R \in CRing \land (N = \{I\} \land I \in V) \land M \in B) \to \{⟨\{⟨I, I⟩\}, (ℤRHom (R) \circ pmSgn (N)) (\{⟨I, I⟩\}) \cdot_{R} (\underset{x \in N}{\sum_{{mulGrp}_{R}}}, (\{⟨I, I⟩\} (x) M x))⟩\} = (y \in \{\{⟨I, I⟩\}\} ⟼ I M I)$
136	21 33 135	3eqtrd	$⊢ (R \in CRing \land (N = \{I\} \land I \in V) \land M \in B) \to (p \in {Base}_{SymGrp (N)} ⟼ (ℤRHom (R) \circ pmSgn (N)) (p) \cdot_{R} (\underset{x \in N}{\sum_{{mulGrp}_{R}}}, (p (x) M x))) = (y \in \{\{⟨I, I⟩\}\} ⟼ I M I)$
137	136	oveq2d	$⊢ (R \in CRing \land (N = \{I\} \land I \in V) \land M \in B) \to \underset{p \in {Base}_{SymGrp (N)}}{\sum_{R}} ((ℤRHom (R) \circ pmSgn (N)) (p) \cdot_{R} (\underset{x \in N}{\sum_{{mulGrp}_{R}}}, (p (x) M x))) = \underset{y \in \{\{⟨I, I⟩\}\}}{\sum_{R}} (I M I)$
138		ringmnd	$⊢ R \in Ring \to R \in Mnd$
139	82 138	syl	$⊢ R \in CRing \to R \in Mnd$
140	139	3ad2ant1	$⊢ (R \in CRing \land (N = \{I\} \land I \in V) \land M \in B) \to R \in Mnd$
141	106 132	gsumsn	$⊢ (R \in Mnd \land \{⟨I, I⟩\} \in V \land I M I \in {Base}_{R}) \to \underset{y \in \{\{⟨I, I⟩\}\}}{\sum_{R}} (I M I) = I M I$
142	140 23 125 141	syl3anc	$⊢ (R \in CRing \land (N = \{I\} \land I \in V) \land M \in B) \to \underset{y \in \{\{⟨I, I⟩\}\}}{\sum_{R}} (I M I) = I M I$
143	10 137 142	3eqtrd	$⊢ (R \in CRing \land (N = \{I\} \land I \in V) \land M \in B) \to D (M) = I M I$

Metamath Proof Explorer

Theorem m1detdiag

Proof