madjusmdetlem4

	Ref	Expression
Hypotheses	madjusmdet.b	$⊢ B = {Base}_{A}$
	madjusmdet.a	$⊢ A = (1 \dots N) Mat R$
	madjusmdet.d	$⊢ D = (1 \dots N) maDet R$
	madjusmdet.k	$⊢ K = (1 \dots N) maAdju R$
	madjusmdet.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	madjusmdet.z	$⊢ Z = ℤRHom (R)$
	madjusmdet.e	$⊢ E = (1 \dots N - 1) maDet R$
	madjusmdet.n	$⊢ φ \to N \in ℕ$
	madjusmdet.r	$⊢ φ \to R \in CRing$
	madjusmdet.i	$⊢ φ \to I \in (1 \dots N)$
	madjusmdet.j	$⊢ φ \to J \in (1 \dots N)$
	madjusmdet.m	$⊢ φ \to M \in B$
	madjusmdetlem2.p	$⊢ P = (i \in (1 \dots N) ⟼ if (i = 1, I, if (i \leq I, i - 1, i)))$
	madjusmdetlem2.s	$⊢ S = (i \in (1 \dots N) ⟼ if (i = 1, N, if (i \leq N, i - 1, i)))$
	madjusmdetlem4.q	$⊢ Q = (j \in (1 \dots N) ⟼ if (j = 1, J, if (j \leq J, j - 1, j)))$
	madjusmdetlem4.t	$⊢ T = (j \in (1 \dots N) ⟼ if (j = 1, N, if (j \leq N, j - 1, j)))$
Assertion	madjusmdetlem4	$⊢ φ \to J K (M) I = Z ({(- 1)}^{I + J}) \underset{˙}{\cdot} E (I {subMat}_{1} (M) J)$

Proof

Step	Hyp	Ref	Expression
1		madjusmdet.b	$⊢ B = {Base}_{A}$
2		madjusmdet.a	$⊢ A = (1 \dots N) Mat R$
3		madjusmdet.d	$⊢ D = (1 \dots N) maDet R$
4		madjusmdet.k	$⊢ K = (1 \dots N) maAdju R$
5		madjusmdet.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
6		madjusmdet.z	$⊢ Z = ℤRHom (R)$
7		madjusmdet.e	$⊢ E = (1 \dots N - 1) maDet R$
8		madjusmdet.n	$⊢ φ \to N \in ℕ$
9		madjusmdet.r	$⊢ φ \to R \in CRing$
10		madjusmdet.i	$⊢ φ \to I \in (1 \dots N)$
11		madjusmdet.j	$⊢ φ \to J \in (1 \dots N)$
12		madjusmdet.m	$⊢ φ \to M \in B$
13		madjusmdetlem2.p	$⊢ P = (i \in (1 \dots N) ⟼ if (i = 1, I, if (i \leq I, i - 1, i)))$
14		madjusmdetlem2.s	$⊢ S = (i \in (1 \dots N) ⟼ if (i = 1, N, if (i \leq N, i - 1, i)))$
15		madjusmdetlem4.q	$⊢ Q = (j \in (1 \dots N) ⟼ if (j = 1, J, if (j \leq J, j - 1, j)))$
16		madjusmdetlem4.t	$⊢ T = (j \in (1 \dots N) ⟼ if (j = 1, N, if (j \leq N, j - 1, j)))$
17		eqid	$⊢ {Base}_{SymGrp ((1 \dots N))} = {Base}_{SymGrp ((1 \dots N))}$
18		eqid	$⊢ pmSgn ((1 \dots N)) = pmSgn ((1 \dots N))$
19		eqid	$⊢ I ((1 \dots N) minMatR1 R) (M) J = I ((1 \dots N) minMatR1 R) (M) J$
20		fveq2	$⊢ k = i \to (P \circ S^{-1}) (k) = (P \circ S^{-1}) (i)$
21	20	oveq1d	$⊢ k = i \to (P \circ S^{-1}) (k) (I ((1 \dots N) minMatR1 R) (M) J) (Q \circ T^{-1}) (l) = (P \circ S^{-1}) (i) (I ((1 \dots N) minMatR1 R) (M) J) (Q \circ T^{-1}) (l)$
22		fveq2	$⊢ l = j \to (Q \circ T^{-1}) (l) = (Q \circ T^{-1}) (j)$
23	22	oveq2d	$⊢ l = j \to (P \circ S^{-1}) (i) (I ((1 \dots N) minMatR1 R) (M) J) (Q \circ T^{-1}) (l) = (P \circ S^{-1}) (i) (I ((1 \dots N) minMatR1 R) (M) J) (Q \circ T^{-1}) (j)$
24	21 23	cbvmpov	$⊢ (k \in (1 \dots N), l \in (1 \dots N) ⟼ (P \circ S^{-1}) (k) (I ((1 \dots N) minMatR1 R) (M) J) (Q \circ T^{-1}) (l)) = (i \in (1 \dots N), j \in (1 \dots N) ⟼ (P \circ S^{-1}) (i) (I ((1 \dots N) minMatR1 R) (M) J) (Q \circ T^{-1}) (j))$
25		eqid	$⊢ (1 \dots N) = (1 \dots N)$
26		eqid	$⊢ SymGrp ((1 \dots N)) = SymGrp ((1 \dots N))$
27	25 13 26 17	fzto1st	$⊢ I \in (1 \dots N) \to P \in {Base}_{SymGrp ((1 \dots N))}$
28	10 27	syl	$⊢ φ \to P \in {Base}_{SymGrp ((1 \dots N))}$
29		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
30	8 29	eleqtrdi	$⊢ φ \to N \in ℤ_{\geq 1}$
31		eluzfz2	$⊢ N \in ℤ_{\geq 1} \to N \in (1 \dots N)$
32	30 31	syl	$⊢ φ \to N \in (1 \dots N)$
33	25 14 26 17	fzto1st	$⊢ N \in (1 \dots N) \to S \in {Base}_{SymGrp ((1 \dots N))}$
34	32 33	syl	$⊢ φ \to S \in {Base}_{SymGrp ((1 \dots N))}$
35		eqid	$⊢ {inv}_{g} (SymGrp ((1 \dots N))) = {inv}_{g} (SymGrp ((1 \dots N)))$
36	26 17 35	symginv	$⊢ S \in {Base}_{SymGrp ((1 \dots N))} \to {inv}_{g} (SymGrp ((1 \dots N))) (S) = S^{-1}$
37	34 36	syl	$⊢ φ \to {inv}_{g} (SymGrp ((1 \dots N))) (S) = S^{-1}$
38		fzfid	$⊢ φ \to (1 \dots N) \in Fin$
39	26	symggrp	$⊢ (1 \dots N) \in Fin \to SymGrp ((1 \dots N)) \in Grp$
40	38 39	syl	$⊢ φ \to SymGrp ((1 \dots N)) \in Grp$
41	17 35	grpinvcl	$⊢ (SymGrp ((1 \dots N)) \in Grp \land S \in {Base}_{SymGrp ((1 \dots N))}) \to {inv}_{g} (SymGrp ((1 \dots N))) (S) \in {Base}_{SymGrp ((1 \dots N))}$
42	40 34 41	syl2anc	$⊢ φ \to {inv}_{g} (SymGrp ((1 \dots N))) (S) \in {Base}_{SymGrp ((1 \dots N))}$
43	37 42	eqeltrrd	$⊢ φ \to S^{-1} \in {Base}_{SymGrp ((1 \dots N))}$
44		eqid	$⊢ +_{SymGrp ((1 \dots N))} = +_{SymGrp ((1 \dots N))}$
45	26 17 44	symgov	$⊢ (P \in {Base}_{SymGrp ((1 \dots N))} \land S^{-1} \in {Base}_{SymGrp ((1 \dots N))}) \to P +_{SymGrp ((1 \dots N))} S^{-1} = P \circ S^{-1}$
46	26 17 44	symgcl	$⊢ (P \in {Base}_{SymGrp ((1 \dots N))} \land S^{-1} \in {Base}_{SymGrp ((1 \dots N))}) \to P +_{SymGrp ((1 \dots N))} S^{-1} \in {Base}_{SymGrp ((1 \dots N))}$
47	45 46	eqeltrrd	$⊢ (P \in {Base}_{SymGrp ((1 \dots N))} \land S^{-1} \in {Base}_{SymGrp ((1 \dots N))}) \to P \circ S^{-1} \in {Base}_{SymGrp ((1 \dots N))}$
48	28 43 47	syl2anc	$⊢ φ \to P \circ S^{-1} \in {Base}_{SymGrp ((1 \dots N))}$
49	25 15 26 17	fzto1st	$⊢ J \in (1 \dots N) \to Q \in {Base}_{SymGrp ((1 \dots N))}$
50	11 49	syl	$⊢ φ \to Q \in {Base}_{SymGrp ((1 \dots N))}$
51	25 16 26 17	fzto1st	$⊢ N \in (1 \dots N) \to T \in {Base}_{SymGrp ((1 \dots N))}$
52	32 51	syl	$⊢ φ \to T \in {Base}_{SymGrp ((1 \dots N))}$
53	26 17 35	symginv	$⊢ T \in {Base}_{SymGrp ((1 \dots N))} \to {inv}_{g} (SymGrp ((1 \dots N))) (T) = T^{-1}$
54	52 53	syl	$⊢ φ \to {inv}_{g} (SymGrp ((1 \dots N))) (T) = T^{-1}$
55	17 35	grpinvcl	$⊢ (SymGrp ((1 \dots N)) \in Grp \land T \in {Base}_{SymGrp ((1 \dots N))}) \to {inv}_{g} (SymGrp ((1 \dots N))) (T) \in {Base}_{SymGrp ((1 \dots N))}$
56	40 52 55	syl2anc	$⊢ φ \to {inv}_{g} (SymGrp ((1 \dots N))) (T) \in {Base}_{SymGrp ((1 \dots N))}$
57	54 56	eqeltrrd	$⊢ φ \to T^{-1} \in {Base}_{SymGrp ((1 \dots N))}$
58	26 17 44	symgov	$⊢ (Q \in {Base}_{SymGrp ((1 \dots N))} \land T^{-1} \in {Base}_{SymGrp ((1 \dots N))}) \to Q +_{SymGrp ((1 \dots N))} T^{-1} = Q \circ T^{-1}$
59	26 17 44	symgcl	$⊢ (Q \in {Base}_{SymGrp ((1 \dots N))} \land T^{-1} \in {Base}_{SymGrp ((1 \dots N))}) \to Q +_{SymGrp ((1 \dots N))} T^{-1} \in {Base}_{SymGrp ((1 \dots N))}$
60	58 59	eqeltrrd	$⊢ (Q \in {Base}_{SymGrp ((1 \dots N))} \land T^{-1} \in {Base}_{SymGrp ((1 \dots N))}) \to Q \circ T^{-1} \in {Base}_{SymGrp ((1 \dots N))}$
61	50 57 60	syl2anc	$⊢ φ \to Q \circ T^{-1} \in {Base}_{SymGrp ((1 \dots N))}$
62	26 17	symgbasf1o	$⊢ S \in {Base}_{SymGrp ((1 \dots N))} \to S : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)$
63	34 62	syl	$⊢ φ \to S : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)$
64		f1of1	$⊢ S : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \to S : (1 \dots N) \underset{1-1}{⟶} (1 \dots N)$
65		df-f1	$⊢ S : (1 \dots N) \underset{1-1}{⟶} (1 \dots N) \leftrightarrow (S : (1 \dots N) ⟶ (1 \dots N) \land Fun S^{-1})$
66	65	simprbi	$⊢ S : (1 \dots N) \underset{1-1}{⟶} (1 \dots N) \to Fun S^{-1}$
67	63 64 66	3syl	$⊢ φ \to Fun S^{-1}$
68		f1ocnv	$⊢ S : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \to S^{-1} : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)$
69		f1odm	$⊢ S^{-1} : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \to dom S^{-1} = (1 \dots N)$
70	63 68 69	3syl	$⊢ φ \to dom S^{-1} = (1 \dots N)$
71	32 70	eleqtrrd	$⊢ φ \to N \in dom S^{-1}$
72		fvco	$⊢ (Fun S^{-1} \land N \in dom S^{-1}) \to (P \circ S^{-1}) (N) = P (S^{-1} (N))$
73	67 71 72	syl2anc	$⊢ φ \to (P \circ S^{-1}) (N) = P (S^{-1} (N))$
74	25 14 26 17	fzto1stinvn	$⊢ N \in (1 \dots N) \to S^{-1} (N) = 1$
75	32 74	syl	$⊢ φ \to S^{-1} (N) = 1$
76	75	fveq2d	$⊢ φ \to P (S^{-1} (N)) = P (1)$
77	25 13	fzto1stfv1	$⊢ I \in (1 \dots N) \to P (1) = I$
78	10 77	syl	$⊢ φ \to P (1) = I$
79	73 76 78	3eqtrd	$⊢ φ \to (P \circ S^{-1}) (N) = I$
80	26 17	symgbasf1o	$⊢ T \in {Base}_{SymGrp ((1 \dots N))} \to T : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)$
81	52 80	syl	$⊢ φ \to T : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)$
82		f1of1	$⊢ T : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \to T : (1 \dots N) \underset{1-1}{⟶} (1 \dots N)$
83		df-f1	$⊢ T : (1 \dots N) \underset{1-1}{⟶} (1 \dots N) \leftrightarrow (T : (1 \dots N) ⟶ (1 \dots N) \land Fun T^{-1})$
84	83	simprbi	$⊢ T : (1 \dots N) \underset{1-1}{⟶} (1 \dots N) \to Fun T^{-1}$
85	81 82 84	3syl	$⊢ φ \to Fun T^{-1}$
86		f1ocnv	$⊢ T : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \to T^{-1} : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)$
87		f1odm	$⊢ T^{-1} : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \to dom T^{-1} = (1 \dots N)$
88	81 86 87	3syl	$⊢ φ \to dom T^{-1} = (1 \dots N)$
89	32 88	eleqtrrd	$⊢ φ \to N \in dom T^{-1}$
90		fvco	$⊢ (Fun T^{-1} \land N \in dom T^{-1}) \to (Q \circ T^{-1}) (N) = Q (T^{-1} (N))$
91	85 89 90	syl2anc	$⊢ φ \to (Q \circ T^{-1}) (N) = Q (T^{-1} (N))$
92	25 16 26 17	fzto1stinvn	$⊢ N \in (1 \dots N) \to T^{-1} (N) = 1$
93	32 92	syl	$⊢ φ \to T^{-1} (N) = 1$
94	93	fveq2d	$⊢ φ \to Q (T^{-1} (N)) = Q (1)$
95	25 15	fzto1stfv1	$⊢ J \in (1 \dots N) \to Q (1) = J$
96	11 95	syl	$⊢ φ \to Q (1) = J$
97	91 94 96	3eqtrd	$⊢ φ \to (Q \circ T^{-1}) (N) = J$
98		crngring	$⊢ R \in CRing \to R \in Ring$
99	9 98	syl	$⊢ φ \to R \in Ring$
100	2 1	minmar1cl	$⊢ ((R \in Ring \land M \in B) \land (I \in (1 \dots N) \land J \in (1 \dots N))) \to I ((1 \dots N) minMatR1 R) (M) J \in B$
101	99 12 10 11 100	syl22anc	$⊢ φ \to I ((1 \dots N) minMatR1 R) (M) J \in B$
102	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 24 101	madjusmdetlem3	$⊢ φ \to I {subMat}_{1} (I ((1 \dots N) minMatR1 R) (M) J) J = N {subMat}_{1} ((k \in (1 \dots N), l \in (1 \dots N) ⟼ (P \circ S^{-1}) (k) (I ((1 \dots N) minMatR1 R) (M) J) (Q \circ T^{-1}) (l))) N$
103	1 2 3 4 5 6 7 8 9 10 11 12 17 18 19 24 48 61 79 97 102	madjusmdetlem1	$⊢ φ \to J K (M) I = Z (pmSgn ((1 \dots N)) (P \circ S^{-1}) pmSgn ((1 \dots N)) (Q \circ T^{-1})) \underset{˙}{\cdot} E (I {subMat}_{1} (M) J)$
104	26 18 17	psgnco	$⊢ ((1 \dots N) \in Fin \land P \in {Base}_{SymGrp ((1 \dots N))} \land S^{-1} \in {Base}_{SymGrp ((1 \dots N))}) \to pmSgn ((1 \dots N)) (P \circ S^{-1}) = pmSgn ((1 \dots N)) (P) pmSgn ((1 \dots N)) (S^{-1})$
105	38 28 43 104	syl3anc	$⊢ φ \to pmSgn ((1 \dots N)) (P \circ S^{-1}) = pmSgn ((1 \dots N)) (P) pmSgn ((1 \dots N)) (S^{-1})$
106	25 13 26 17 18	psgnfzto1st	$⊢ I \in (1 \dots N) \to pmSgn ((1 \dots N)) (P) = {(- 1)}^{I + 1}$
107	10 106	syl	$⊢ φ \to pmSgn ((1 \dots N)) (P) = {(- 1)}^{I + 1}$
108	26 18 17	psgninv	$⊢ ((1 \dots N) \in Fin \land S \in {Base}_{SymGrp ((1 \dots N))}) \to pmSgn ((1 \dots N)) (S^{-1}) = pmSgn ((1 \dots N)) (S)$
109	38 34 108	syl2anc	$⊢ φ \to pmSgn ((1 \dots N)) (S^{-1}) = pmSgn ((1 \dots N)) (S)$
110	25 14 26 17 18	psgnfzto1st	$⊢ N \in (1 \dots N) \to pmSgn ((1 \dots N)) (S) = {(- 1)}^{N + 1}$
111	32 110	syl	$⊢ φ \to pmSgn ((1 \dots N)) (S) = {(- 1)}^{N + 1}$
112	109 111	eqtrd	$⊢ φ \to pmSgn ((1 \dots N)) (S^{-1}) = {(- 1)}^{N + 1}$
113	107 112	oveq12d	$⊢ φ \to pmSgn ((1 \dots N)) (P) pmSgn ((1 \dots N)) (S^{-1}) = {(- 1)}^{I + 1} {(- 1)}^{N + 1}$
114	105 113	eqtrd	$⊢ φ \to pmSgn ((1 \dots N)) (P \circ S^{-1}) = {(- 1)}^{I + 1} {(- 1)}^{N + 1}$
115	26 18 17	psgnco	$⊢ ((1 \dots N) \in Fin \land Q \in {Base}_{SymGrp ((1 \dots N))} \land T^{-1} \in {Base}_{SymGrp ((1 \dots N))}) \to pmSgn ((1 \dots N)) (Q \circ T^{-1}) = pmSgn ((1 \dots N)) (Q) pmSgn ((1 \dots N)) (T^{-1})$
116	38 50 57 115	syl3anc	$⊢ φ \to pmSgn ((1 \dots N)) (Q \circ T^{-1}) = pmSgn ((1 \dots N)) (Q) pmSgn ((1 \dots N)) (T^{-1})$
117	25 15 26 17 18	psgnfzto1st	$⊢ J \in (1 \dots N) \to pmSgn ((1 \dots N)) (Q) = {(- 1)}^{J + 1}$
118	11 117	syl	$⊢ φ \to pmSgn ((1 \dots N)) (Q) = {(- 1)}^{J + 1}$
119	26 18 17	psgninv	$⊢ ((1 \dots N) \in Fin \land T \in {Base}_{SymGrp ((1 \dots N))}) \to pmSgn ((1 \dots N)) (T^{-1}) = pmSgn ((1 \dots N)) (T)$
120	38 52 119	syl2anc	$⊢ φ \to pmSgn ((1 \dots N)) (T^{-1}) = pmSgn ((1 \dots N)) (T)$
121	25 16 26 17 18	psgnfzto1st	$⊢ N \in (1 \dots N) \to pmSgn ((1 \dots N)) (T) = {(- 1)}^{N + 1}$
122	32 121	syl	$⊢ φ \to pmSgn ((1 \dots N)) (T) = {(- 1)}^{N + 1}$
123	120 122	eqtrd	$⊢ φ \to pmSgn ((1 \dots N)) (T^{-1}) = {(- 1)}^{N + 1}$
124	118 123	oveq12d	$⊢ φ \to pmSgn ((1 \dots N)) (Q) pmSgn ((1 \dots N)) (T^{-1}) = {(- 1)}^{J + 1} {(- 1)}^{N + 1}$
125	116 124	eqtrd	$⊢ φ \to pmSgn ((1 \dots N)) (Q \circ T^{-1}) = {(- 1)}^{J + 1} {(- 1)}^{N + 1}$
126	114 125	oveq12d	$⊢ φ \to pmSgn ((1 \dots N)) (P \circ S^{-1}) pmSgn ((1 \dots N)) (Q \circ T^{-1}) = {(- 1)}^{I + 1} {(- 1)}^{N + 1} {(- 1)}^{J + 1} {(- 1)}^{N + 1}$
127		1cnd	$⊢ φ \to 1 \in ℂ$
128	127	negcld	$⊢ φ \to - 1 \in ℂ$
129		fz1ssnn	$⊢ (1 \dots N) \subseteq ℕ$
130	129 10	sselid	$⊢ φ \to I \in ℕ$
131	130	nnnn0d	$⊢ φ \to I \in ℕ_{0}$
132		1nn0	$⊢ 1 \in ℕ_{0}$
133	132	a1i	$⊢ φ \to 1 \in ℕ_{0}$
134	131 133	nn0addcld	$⊢ φ \to I + 1 \in ℕ_{0}$
135	128 134	expcld	$⊢ φ \to {(- 1)}^{I + 1} \in ℂ$
136	8	nnnn0d	$⊢ φ \to N \in ℕ_{0}$
137	136 133	nn0addcld	$⊢ φ \to N + 1 \in ℕ_{0}$
138	128 137	expcld	$⊢ φ \to {(- 1)}^{N + 1} \in ℂ$
139	129 11	sselid	$⊢ φ \to J \in ℕ$
140	139	nnnn0d	$⊢ φ \to J \in ℕ_{0}$
141	140 133	nn0addcld	$⊢ φ \to J + 1 \in ℕ_{0}$
142	128 141	expcld	$⊢ φ \to {(- 1)}^{J + 1} \in ℂ$
143	135 138 142 138	mul4d	$⊢ φ \to {(- 1)}^{I + 1} {(- 1)}^{N + 1} {(- 1)}^{J + 1} {(- 1)}^{N + 1} = {(- 1)}^{I + 1} {(- 1)}^{J + 1} {(- 1)}^{N + 1} {(- 1)}^{N + 1}$
144	128 141 134	expaddd	$⊢ φ \to {(- 1)}^{I + 1 + J + 1} = {(- 1)}^{I + 1} {(- 1)}^{J + 1}$
145	130	nncnd	$⊢ φ \to I \in ℂ$
146	139	nncnd	$⊢ φ \to J \in ℂ$
147	145 127 146 127	add4d	$⊢ φ \to I + 1 + J + 1 = I + J + 1 + 1$
148		1p1e2	$⊢ 1 + 1 = 2$
149	148	oveq2i	$⊢ I + J + 1 + 1 = I + J + 2$
150	147 149	eqtrdi	$⊢ φ \to I + 1 + J + 1 = I + J + 2$
151	150	oveq2d	$⊢ φ \to {(- 1)}^{I + 1 + J + 1} = {(- 1)}^{I + J + 2}$
152		2nn0	$⊢ 2 \in ℕ_{0}$
153	152	a1i	$⊢ φ \to 2 \in ℕ_{0}$
154	131 140	nn0addcld	$⊢ φ \to I + J \in ℕ_{0}$
155	128 153 154	expaddd	$⊢ φ \to {(- 1)}^{I + J + 2} = {(- 1)}^{I + J} {(- 1)}^{2}$
156		neg1sqe1	$⊢ {(- 1)}^{2} = 1$
157	156	oveq2i	$⊢ {(- 1)}^{I + J} {(- 1)}^{2} = {(- 1)}^{I + J} \cdot 1$
158	155 157	eqtrdi	$⊢ φ \to {(- 1)}^{I + J + 2} = {(- 1)}^{I + J} \cdot 1$
159	128 154	expcld	$⊢ φ \to {(- 1)}^{I + J} \in ℂ$
160	159	mulridd	$⊢ φ \to {(- 1)}^{I + J} \cdot 1 = {(- 1)}^{I + J}$
161	151 158 160	3eqtrd	$⊢ φ \to {(- 1)}^{I + 1 + J + 1} = {(- 1)}^{I + J}$
162	144 161	eqtr3d	$⊢ φ \to {(- 1)}^{I + 1} {(- 1)}^{J + 1} = {(- 1)}^{I + J}$
163	137	nn0zd	$⊢ φ \to N + 1 \in ℤ$
164		m1expcl2	$⊢ N + 1 \in ℤ \to {(- 1)}^{N + 1} \in \{- 1, 1\}$
165		1neg1t1neg1	$⊢ {(- 1)}^{N + 1} \in \{- 1, 1\} \to {(- 1)}^{N + 1} {(- 1)}^{N + 1} = 1$
166	163 164 165	3syl	$⊢ φ \to {(- 1)}^{N + 1} {(- 1)}^{N + 1} = 1$
167	162 166	oveq12d	$⊢ φ \to {(- 1)}^{I + 1} {(- 1)}^{J + 1} {(- 1)}^{N + 1} {(- 1)}^{N + 1} = {(- 1)}^{I + J} \cdot 1$
168	143 167 160	3eqtrd	$⊢ φ \to {(- 1)}^{I + 1} {(- 1)}^{N + 1} {(- 1)}^{J + 1} {(- 1)}^{N + 1} = {(- 1)}^{I + J}$
169	126 168	eqtrd	$⊢ φ \to pmSgn ((1 \dots N)) (P \circ S^{-1}) pmSgn ((1 \dots N)) (Q \circ T^{-1}) = {(- 1)}^{I + J}$
170	169	fveq2d	$⊢ φ \to Z (pmSgn ((1 \dots N)) (P \circ S^{-1}) pmSgn ((1 \dots N)) (Q \circ T^{-1})) = Z ({(- 1)}^{I + J})$
171	170	oveq1d	$⊢ φ \to Z (pmSgn ((1 \dots N)) (P \circ S^{-1}) pmSgn ((1 \dots N)) (Q \circ T^{-1})) \underset{˙}{\cdot} E (I {subMat}_{1} (M) J) = Z ({(- 1)}^{I + J}) \underset{˙}{\cdot} E (I {subMat}_{1} (M) J)$
172	103 171	eqtrd	$⊢ φ \to J K (M) I = Z ({(- 1)}^{I + J}) \underset{˙}{\cdot} E (I {subMat}_{1} (M) J)$

Metamath Proof Explorer

Theorem madjusmdetlem4

Proof