madetsumid

Description: The identity summand in the Leibniz' formula of a determinant for a square matrix over a commutative ring. (Contributed by AV, 29-Dec-2018)

	Ref	Expression
Hypotheses	madetsumid.a	$⊢ A = N Mat R$
	madetsumid.b	$⊢ B = {Base}_{A}$
	madetsumid.u	$⊢ U = {mulGrp}_{R}$
	madetsumid.y	$⊢ Y = ℤRHom (R)$
	madetsumid.s	$⊢ S = pmSgn (N)$
	madetsumid.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
Assertion	madetsumid	$⊢ (R \in CRing \land M \in B \land P = {I ↾}_{N}) \to (Y \circ S) (P) \underset{˙}{\cdot} (\underset{r \in N}{\sum_{U}}, (P (r) M r)) = \underset{r \in N}{\sum_{U}} (r M r)$

Proof

Step	Hyp	Ref	Expression
1		madetsumid.a	$⊢ A = N Mat R$
2		madetsumid.b	$⊢ B = {Base}_{A}$
3		madetsumid.u	$⊢ U = {mulGrp}_{R}$
4		madetsumid.y	$⊢ Y = ℤRHom (R)$
5		madetsumid.s	$⊢ S = pmSgn (N)$
6		madetsumid.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
7		fveq2	$⊢ P = {I ↾}_{N} \to (Y \circ S) (P) = (Y \circ S) ({I ↾}_{N})$
8		fveq1	$⊢ P = {I ↾}_{N} \to P (r) = ({I ↾}_{N}) (r)$
9	8	oveq1d	$⊢ P = {I ↾}_{N} \to P (r) M r = ({I ↾}_{N}) (r) M r$
10	9	mpteq2dv	$⊢ P = {I ↾}_{N} \to (r \in N ⟼ P (r) M r) = (r \in N ⟼ ({I ↾}_{N}) (r) M r)$
11	10	oveq2d	$⊢ P = {I ↾}_{N} \to \underset{r \in N}{\sum_{U}} (P (r) M r) = \underset{r \in N}{\sum_{U}} (({I ↾}_{N}) (r) M r)$
12	7 11	oveq12d	$⊢ P = {I ↾}_{N} \to (Y \circ S) (P) \underset{˙}{\cdot} (\underset{r \in N}{\sum_{U}}, (P (r) M r)) = (Y \circ S) ({I ↾}_{N}) \underset{˙}{\cdot} (\underset{r \in N}{\sum_{U}}, (({I ↾}_{N}) (r) M r))$
13	12	3ad2ant3	$⊢ (R \in CRing \land M \in B \land P = {I ↾}_{N}) \to (Y \circ S) (P) \underset{˙}{\cdot} (\underset{r \in N}{\sum_{U}}, (P (r) M r)) = (Y \circ S) ({I ↾}_{N}) \underset{˙}{\cdot} (\underset{r \in N}{\sum_{U}}, (({I ↾}_{N}) (r) M r))$
14	1 2	matrcl	$⊢ M \in B \to (N \in Fin \land R \in V)$
15	14	simpld	$⊢ M \in B \to N \in Fin$
16	4 5	coeq12i	$⊢ Y \circ S = ℤRHom (R) \circ pmSgn (N)$
17	16	a1i	$⊢ (R \in CRing \land N \in Fin) \to Y \circ S = ℤRHom (R) \circ pmSgn (N)$
18		eqid	$⊢ SymGrp (N) = SymGrp (N)$
19	18	symgid	$⊢ N \in Fin \to {I ↾}_{N} = 0_{SymGrp (N)}$
20	19	adantl	$⊢ (R \in CRing \land N \in Fin) \to {I ↾}_{N} = 0_{SymGrp (N)}$
21	17 20	fveq12d	$⊢ (R \in CRing \land N \in Fin) \to (Y \circ S) ({I ↾}_{N}) = (ℤRHom (R) \circ pmSgn (N)) (0_{SymGrp (N)})$
22		crngring	$⊢ R \in CRing \to R \in Ring$
23		zrhpsgnmhm	$⊢ (R \in Ring \land N \in Fin) \to ℤRHom (R) \circ pmSgn (N) \in (SymGrp (N) MndHom {mulGrp}_{R})$
24	3	oveq2i	$⊢ SymGrp (N) MndHom U = SymGrp (N) MndHom {mulGrp}_{R}$
25	23 24	eleqtrrdi	$⊢ (R \in Ring \land N \in Fin) \to ℤRHom (R) \circ pmSgn (N) \in (SymGrp (N) MndHom U)$
26	22 25	sylan	$⊢ (R \in CRing \land N \in Fin) \to ℤRHom (R) \circ pmSgn (N) \in (SymGrp (N) MndHom U)$
27		eqid	$⊢ 0_{SymGrp (N)} = 0_{SymGrp (N)}$
28		eqid	$⊢ 1_{R} = 1_{R}$
29	3 28	ringidval	$⊢ 1_{R} = 0_{U}$
30	27 29	mhm0	$⊢ ℤRHom (R) \circ pmSgn (N) \in (SymGrp (N) MndHom U) \to (ℤRHom (R) \circ pmSgn (N)) (0_{SymGrp (N)}) = 1_{R}$
31	26 30	syl	$⊢ (R \in CRing \land N \in Fin) \to (ℤRHom (R) \circ pmSgn (N)) (0_{SymGrp (N)}) = 1_{R}$
32	21 31	eqtrd	$⊢ (R \in CRing \land N \in Fin) \to (Y \circ S) ({I ↾}_{N}) = 1_{R}$
33		fvresi	$⊢ r \in N \to ({I ↾}_{N}) (r) = r$
34	33	adantl	$⊢ ((R \in CRing \land N \in Fin) \land r \in N) \to ({I ↾}_{N}) (r) = r$
35	34	oveq1d	$⊢ ((R \in CRing \land N \in Fin) \land r \in N) \to ({I ↾}_{N}) (r) M r = r M r$
36	35	mpteq2dva	$⊢ (R \in CRing \land N \in Fin) \to (r \in N ⟼ ({I ↾}_{N}) (r) M r) = (r \in N ⟼ r M r)$
37	36	oveq2d	$⊢ (R \in CRing \land N \in Fin) \to \underset{r \in N}{\sum_{U}} (({I ↾}_{N}) (r) M r) = \underset{r \in N}{\sum_{U}} (r M r)$
38	32 37	oveq12d	$⊢ (R \in CRing \land N \in Fin) \to (Y \circ S) ({I ↾}_{N}) \underset{˙}{\cdot} (\underset{r \in N}{\sum_{U}}, (({I ↾}_{N}) (r) M r)) = 1_{R} \underset{˙}{\cdot} (\underset{r \in N}{\sum_{U}}, (r M r))$
39	15 38	sylan2	$⊢ (R \in CRing \land M \in B) \to (Y \circ S) ({I ↾}_{N}) \underset{˙}{\cdot} (\underset{r \in N}{\sum_{U}}, (({I ↾}_{N}) (r) M r)) = 1_{R} \underset{˙}{\cdot} (\underset{r \in N}{\sum_{U}}, (r M r))$
40	1 2 3	matgsumcl	$⊢ (R \in CRing \land M \in B) \to \underset{r \in N}{\sum_{U}} (r M r) \in {Base}_{R}$
41		eqid	$⊢ {Base}_{R} = {Base}_{R}$
42	41 6 28	ringlidm	$⊢ (R \in Ring \land \underset{r \in N}{\sum_{U}} (r M r) \in {Base}_{R}) \to 1_{R} \underset{˙}{\cdot} (\underset{r \in N}{\sum_{U}}, (r M r)) = \underset{r \in N}{\sum_{U}} (r M r)$
43	22 40 42	syl2an2r	$⊢ (R \in CRing \land M \in B) \to 1_{R} \underset{˙}{\cdot} (\underset{r \in N}{\sum_{U}}, (r M r)) = \underset{r \in N}{\sum_{U}} (r M r)$
44	39 43	eqtrd	$⊢ (R \in CRing \land M \in B) \to (Y \circ S) ({I ↾}_{N}) \underset{˙}{\cdot} (\underset{r \in N}{\sum_{U}}, (({I ↾}_{N}) (r) M r)) = \underset{r \in N}{\sum_{U}} (r M r)$
45	44	3adant3	$⊢ (R \in CRing \land M \in B \land P = {I ↾}_{N}) \to (Y \circ S) ({I ↾}_{N}) \underset{˙}{\cdot} (\underset{r \in N}{\sum_{U}}, (({I ↾}_{N}) (r) M r)) = \underset{r \in N}{\sum_{U}} (r M r)$
46	13 45	eqtrd	$⊢ (R \in CRing \land M \in B \land P = {I ↾}_{N}) \to (Y \circ S) (P) \underset{˙}{\cdot} (\underset{r \in N}{\sum_{U}}, (P (r) M r)) = \underset{r \in N}{\sum_{U}} (r M r)$

Metamath Proof Explorer

Theorem madetsumid

Proof