madjusmdetlem1

	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$
	madjusmdetlem1.g	$⊢ G = {Base}_{SymGrp ((1 \dots N))}$
	madjusmdetlem1.s	$⊢ S = pmSgn ((1 \dots N))$
	madjusmdetlem1.u	$⊢ U = I ((1 \dots N) minMatR1 R) (M) J$
	madjusmdetlem1.w	$⊢ W = (i \in (1 \dots N), j \in (1 \dots N) ⟼ P (i) U Q (j))$
	madjusmdetlem1.p	$⊢ φ \to P \in G$
	madjusmdetlem1.q	$⊢ φ \to Q \in G$
	madjusmdetlem1.1	$⊢ φ \to P (N) = I$
	madjusmdetlem1.2	$⊢ φ \to Q (N) = J$
	madjusmdetlem1.3	$⊢ φ \to I {subMat}_{1} (U) J = N {subMat}_{1} (W) N$
Assertion	madjusmdetlem1	$⊢ φ \to J K (M) I = Z (S (P) S (Q)) \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		madjusmdetlem1.g	$⊢ G = {Base}_{SymGrp ((1 \dots N))}$
14		madjusmdetlem1.s	$⊢ S = pmSgn ((1 \dots N))$
15		madjusmdetlem1.u	$⊢ U = I ((1 \dots N) minMatR1 R) (M) J$
16		madjusmdetlem1.w	$⊢ W = (i \in (1 \dots N), j \in (1 \dots N) ⟼ P (i) U Q (j))$
17		madjusmdetlem1.p	$⊢ φ \to P \in G$
18		madjusmdetlem1.q	$⊢ φ \to Q \in G$
19		madjusmdetlem1.1	$⊢ φ \to P (N) = I$
20		madjusmdetlem1.2	$⊢ φ \to Q (N) = J$
21		madjusmdetlem1.3	$⊢ φ \to I {subMat}_{1} (U) J = N {subMat}_{1} (W) N$
22	2 1 3 4	maducoevalmin1	$⊢ (M \in B \land J \in (1 \dots N) \land I \in (1 \dots N)) \to J K (M) I = D (I ((1 \dots N) minMatR1 R) (M) J)$
23	12 11 10 22	syl3anc	$⊢ φ \to J K (M) I = D (I ((1 \dots N) minMatR1 R) (M) J)$
24	15	fveq2i	$⊢ D (U) = D (I ((1 \dots N) minMatR1 R) (M) J)$
25	23 24	eqtr4di	$⊢ φ \to J K (M) I = D (U)$
26		fzfid	$⊢ φ \to (1 \dots N) \in Fin$
27		crngring	$⊢ R \in CRing \to R \in Ring$
28	9 27	syl	$⊢ φ \to R \in Ring$
29	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$
30	28 12 10 11 29	syl22anc	$⊢ φ \to I ((1 \dots N) minMatR1 R) (M) J \in B$
31	15 30	eqeltrid	$⊢ φ \to U \in B$
32	2 1 3 13 14 6 5 16 9 26 31 17 18	mdetpmtr12	$⊢ φ \to D (U) = Z (S (P) S (Q)) \underset{˙}{\cdot} D (W)$
33		simplr	$⊢ (((φ \land i \in (1 \dots N) \land j \in (1 \dots N)) \land i = N) \land j = N) \to i = N$
34	33	fveq2d	$⊢ (((φ \land i \in (1 \dots N) \land j \in (1 \dots N)) \land i = N) \land j = N) \to P (i) = P (N)$
35	19	3ad2ant1	$⊢ (φ \land i \in (1 \dots N) \land j \in (1 \dots N)) \to P (N) = I$
36	35	ad2antrr	$⊢ (((φ \land i \in (1 \dots N) \land j \in (1 \dots N)) \land i = N) \land j = N) \to P (N) = I$
37	34 36	eqtrd	$⊢ (((φ \land i \in (1 \dots N) \land j \in (1 \dots N)) \land i = N) \land j = N) \to P (i) = I$
38		simpr	$⊢ (((φ \land i \in (1 \dots N) \land j \in (1 \dots N)) \land i = N) \land j = N) \to j = N$
39	38	fveq2d	$⊢ (((φ \land i \in (1 \dots N) \land j \in (1 \dots N)) \land i = N) \land j = N) \to Q (j) = Q (N)$
40	20	3ad2ant1	$⊢ (φ \land i \in (1 \dots N) \land j \in (1 \dots N)) \to Q (N) = J$
41	40	ad2antrr	$⊢ (((φ \land i \in (1 \dots N) \land j \in (1 \dots N)) \land i = N) \land j = N) \to Q (N) = J$
42	39 41	eqtrd	$⊢ (((φ \land i \in (1 \dots N) \land j \in (1 \dots N)) \land i = N) \land j = N) \to Q (j) = J$
43	37 42	oveq12d	$⊢ (((φ \land i \in (1 \dots N) \land j \in (1 \dots N)) \land i = N) \land j = N) \to P (i) (I ((1 \dots N) minMatR1 R) (M) J) Q (j) = I (I ((1 \dots N) minMatR1 R) (M) J) J$
44	12	3ad2ant1	$⊢ (φ \land i \in (1 \dots N) \land j \in (1 \dots N)) \to M \in B$
45	44	ad2antrr	$⊢ (((φ \land i \in (1 \dots N) \land j \in (1 \dots N)) \land i = N) \land j = N) \to M \in B$
46	10	3ad2ant1	$⊢ (φ \land i \in (1 \dots N) \land j \in (1 \dots N)) \to I \in (1 \dots N)$
47	46	ad2antrr	$⊢ (((φ \land i \in (1 \dots N) \land j \in (1 \dots N)) \land i = N) \land j = N) \to I \in (1 \dots N)$
48	11	3ad2ant1	$⊢ (φ \land i \in (1 \dots N) \land j \in (1 \dots N)) \to J \in (1 \dots N)$
49	48	ad2antrr	$⊢ (((φ \land i \in (1 \dots N) \land j \in (1 \dots N)) \land i = N) \land j = N) \to J \in (1 \dots N)$
50		eqid	$⊢ (1 \dots N) minMatR1 R = (1 \dots N) minMatR1 R$
51		eqid	$⊢ 1_{R} = 1_{R}$
52		eqid	$⊢ 0_{R} = 0_{R}$
53	2 1 50 51 52	minmar1eval	$⊢ (M \in B \land (I \in (1 \dots N) \land J \in (1 \dots N)) \land (I \in (1 \dots N) \land J \in (1 \dots N))) \to I (I ((1 \dots N) minMatR1 R) (M) J) J = if (I = I, if (J = J, 1_{R}, 0_{R}), I M J)$
54	45 47 49 47 49 53	syl122anc	$⊢ (((φ \land i \in (1 \dots N) \land j \in (1 \dots N)) \land i = N) \land j = N) \to I (I ((1 \dots N) minMatR1 R) (M) J) J = if (I = I, if (J = J, 1_{R}, 0_{R}), I M J)$
55		eqid	$⊢ I = I$
56	55	iftruei	$⊢ if (I = I, if (J = J, 1_{R}, 0_{R}), I M J) = if (J = J, 1_{R}, 0_{R})$
57		eqid	$⊢ J = J$
58	57	iftruei	$⊢ if (J = J, 1_{R}, 0_{R}) = 1_{R}$
59	56 58	eqtri	$⊢ if (I = I, if (J = J, 1_{R}, 0_{R}), I M J) = 1_{R}$
60	59	a1i	$⊢ (((φ \land i \in (1 \dots N) \land j \in (1 \dots N)) \land i = N) \land j = N) \to if (I = I, if (J = J, 1_{R}, 0_{R}), I M J) = 1_{R}$
61	43 54 60	3eqtrrd	$⊢ (((φ \land i \in (1 \dots N) \land j \in (1 \dots N)) \land i = N) \land j = N) \to 1_{R} = P (i) (I ((1 \dots N) minMatR1 R) (M) J) Q (j)$
62		simplr	$⊢ (((φ \land i \in (1 \dots N) \land j \in (1 \dots N)) \land i = N) \land \neg j = N) \to i = N$
63	62	fveq2d	$⊢ (((φ \land i \in (1 \dots N) \land j \in (1 \dots N)) \land i = N) \land \neg j = N) \to P (i) = P (N)$
64	35	ad2antrr	$⊢ (((φ \land i \in (1 \dots N) \land j \in (1 \dots N)) \land i = N) \land \neg j = N) \to P (N) = I$
65	63 64	eqtrd	$⊢ (((φ \land i \in (1 \dots N) \land j \in (1 \dots N)) \land i = N) \land \neg j = N) \to P (i) = I$
66	65	oveq1d	$⊢ (((φ \land i \in (1 \dots N) \land j \in (1 \dots N)) \land i = N) \land \neg j = N) \to P (i) (I ((1 \dots N) minMatR1 R) (M) J) Q (j) = I (I ((1 \dots N) minMatR1 R) (M) J) Q (j)$
67	44	ad2antrr	$⊢ (((φ \land i \in (1 \dots N) \land j \in (1 \dots N)) \land i = N) \land \neg j = N) \to M \in B$
68	46	ad2antrr	$⊢ (((φ \land i \in (1 \dots N) \land j \in (1 \dots N)) \land i = N) \land \neg j = N) \to I \in (1 \dots N)$
69	48	ad2antrr	$⊢ (((φ \land i \in (1 \dots N) \land j \in (1 \dots N)) \land i = N) \land \neg j = N) \to J \in (1 \dots N)$
70	18	3ad2ant1	$⊢ (φ \land i \in (1 \dots N) \land j \in (1 \dots N)) \to Q \in G$
71		simp3	$⊢ (φ \land i \in (1 \dots N) \land j \in (1 \dots N)) \to j \in (1 \dots N)$
72		eqid	$⊢ SymGrp ((1 \dots N)) = SymGrp ((1 \dots N))$
73	72 13	symgfv	$⊢ (Q \in G \land j \in (1 \dots N)) \to Q (j) \in (1 \dots N)$
74	70 71 73	syl2anc	$⊢ (φ \land i \in (1 \dots N) \land j \in (1 \dots N)) \to Q (j) \in (1 \dots N)$
75	74	ad2antrr	$⊢ (((φ \land i \in (1 \dots N) \land j \in (1 \dots N)) \land i = N) \land \neg j = N) \to Q (j) \in (1 \dots N)$
76	2 1 50 51 52	minmar1eval	$⊢ (M \in B \land (I \in (1 \dots N) \land J \in (1 \dots N)) \land (I \in (1 \dots N) \land Q (j) \in (1 \dots N))) \to I (I ((1 \dots N) minMatR1 R) (M) J) Q (j) = if (I = I, if (Q (j) = J, 1_{R}, 0_{R}), I M Q (j))$
77	67 68 69 68 75 76	syl122anc	$⊢ (((φ \land i \in (1 \dots N) \land j \in (1 \dots N)) \land i = N) \land \neg j = N) \to I (I ((1 \dots N) minMatR1 R) (M) J) Q (j) = if (I = I, if (Q (j) = J, 1_{R}, 0_{R}), I M Q (j))$
78	55	a1i	$⊢ (((φ \land i \in (1 \dots N) \land j \in (1 \dots N)) \land i = N) \land \neg j = N) \to I = I$
79	78	iftrued	$⊢ (((φ \land i \in (1 \dots N) \land j \in (1 \dots N)) \land i = N) \land \neg j = N) \to if (I = I, if (Q (j) = J, 1_{R}, 0_{R}), I M Q (j)) = if (Q (j) = J, 1_{R}, 0_{R})$
80		simpr	$⊢ (((φ \land i \in (1 \dots N) \land j \in (1 \dots N)) \land i = N) \land Q (j) = J) \to Q (j) = J$
81	80	fveq2d	$⊢ (((φ \land i \in (1 \dots N) \land j \in (1 \dots N)) \land i = N) \land Q (j) = J) \to Q^{-1} (Q (j)) = Q^{-1} (J)$
82	72 13	symgbasf1o	$⊢ Q \in G \to Q : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)$
83	70 82	syl	$⊢ (φ \land i \in (1 \dots N) \land j \in (1 \dots N)) \to Q : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)$
84	83	ad2antrr	$⊢ (((φ \land i \in (1 \dots N) \land j \in (1 \dots N)) \land i = N) \land Q (j) = J) \to Q : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)$
85	71	ad2antrr	$⊢ (((φ \land i \in (1 \dots N) \land j \in (1 \dots N)) \land i = N) \land Q (j) = J) \to j \in (1 \dots N)$
86		f1ocnvfv1	$⊢ (Q : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \land j \in (1 \dots N)) \to Q^{-1} (Q (j)) = j$
87	84 85 86	syl2anc	$⊢ (((φ \land i \in (1 \dots N) \land j \in (1 \dots N)) \land i = N) \land Q (j) = J) \to Q^{-1} (Q (j)) = j$
88	20	fveq2d	$⊢ φ \to Q^{-1} (Q (N)) = Q^{-1} (J)$
89	18 82	syl	$⊢ φ \to Q : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)$
90		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
91	8 90	eleqtrdi	$⊢ φ \to N \in ℤ_{\geq 1}$
92		eluzfz2	$⊢ N \in ℤ_{\geq 1} \to N \in (1 \dots N)$
93	91 92	syl	$⊢ φ \to N \in (1 \dots N)$
94		f1ocnvfv1	$⊢ (Q : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \land N \in (1 \dots N)) \to Q^{-1} (Q (N)) = N$
95	89 93 94	syl2anc	$⊢ φ \to Q^{-1} (Q (N)) = N$
96	88 95	eqtr3d	$⊢ φ \to Q^{-1} (J) = N$
97	96	3ad2ant1	$⊢ (φ \land i \in (1 \dots N) \land j \in (1 \dots N)) \to Q^{-1} (J) = N$
98	97	ad2antrr	$⊢ (((φ \land i \in (1 \dots N) \land j \in (1 \dots N)) \land i = N) \land Q (j) = J) \to Q^{-1} (J) = N$
99	81 87 98	3eqtr3d	$⊢ (((φ \land i \in (1 \dots N) \land j \in (1 \dots N)) \land i = N) \land Q (j) = J) \to j = N$
100	99	ex	$⊢ ((φ \land i \in (1 \dots N) \land j \in (1 \dots N)) \land i = N) \to (Q (j) = J \to j = N)$
101	100	con3d	$⊢ ((φ \land i \in (1 \dots N) \land j \in (1 \dots N)) \land i = N) \to (\neg j = N \to \neg Q (j) = J)$
102	101	imp	$⊢ (((φ \land i \in (1 \dots N) \land j \in (1 \dots N)) \land i = N) \land \neg j = N) \to \neg Q (j) = J$
103	102	iffalsed	$⊢ (((φ \land i \in (1 \dots N) \land j \in (1 \dots N)) \land i = N) \land \neg j = N) \to if (Q (j) = J, 1_{R}, 0_{R}) = 0_{R}$
104	79 103	eqtrd	$⊢ (((φ \land i \in (1 \dots N) \land j \in (1 \dots N)) \land i = N) \land \neg j = N) \to if (I = I, if (Q (j) = J, 1_{R}, 0_{R}), I M Q (j)) = 0_{R}$
105	66 77 104	3eqtrrd	$⊢ (((φ \land i \in (1 \dots N) \land j \in (1 \dots N)) \land i = N) \land \neg j = N) \to 0_{R} = P (i) (I ((1 \dots N) minMatR1 R) (M) J) Q (j)$
106	61 105	ifeqda	$⊢ ((φ \land i \in (1 \dots N) \land j \in (1 \dots N)) \land i = N) \to if (j = N, 1_{R}, 0_{R}) = P (i) (I ((1 \dots N) minMatR1 R) (M) J) Q (j)$
107		simp2	$⊢ (φ \land i \in (1 \dots N) \land j \in (1 \dots N)) \to i \in (1 \dots N)$
108	107	adantr	$⊢ ((φ \land i \in (1 \dots N) \land j \in (1 \dots N)) \land \neg i = N) \to i \in (1 \dots N)$
109	71	adantr	$⊢ ((φ \land i \in (1 \dots N) \land j \in (1 \dots N)) \land \neg i = N) \to j \in (1 \dots N)$
110		ovexd	$⊢ ((φ \land i \in (1 \dots N) \land j \in (1 \dots N)) \land \neg i = N) \to P (i) (I ((1 \dots N) minMatR1 R) (M) J) Q (j) \in V$
111	15	oveqi	$⊢ P (i) U Q (j) = P (i) (I ((1 \dots N) minMatR1 R) (M) J) Q (j)$
112	111	a1i	$⊢ (i \in (1 \dots N) \land j \in (1 \dots N)) \to P (i) U Q (j) = P (i) (I ((1 \dots N) minMatR1 R) (M) J) Q (j)$
113	112	mpoeq3ia	$⊢ (i \in (1 \dots N), j \in (1 \dots N) ⟼ P (i) U Q (j)) = (i \in (1 \dots N), j \in (1 \dots N) ⟼ P (i) (I ((1 \dots N) minMatR1 R) (M) J) Q (j))$
114	16 113	eqtri	$⊢ W = (i \in (1 \dots N), j \in (1 \dots N) ⟼ P (i) (I ((1 \dots N) minMatR1 R) (M) J) Q (j))$
115	114	ovmpt4g	$⊢ (i \in (1 \dots N) \land j \in (1 \dots N) \land P (i) (I ((1 \dots N) minMatR1 R) (M) J) Q (j) \in V) \to i W j = P (i) (I ((1 \dots N) minMatR1 R) (M) J) Q (j)$
116	108 109 110 115	syl3anc	$⊢ ((φ \land i \in (1 \dots N) \land j \in (1 \dots N)) \land \neg i = N) \to i W j = P (i) (I ((1 \dots N) minMatR1 R) (M) J) Q (j)$
117	106 116	ifeqda	$⊢ (φ \land i \in (1 \dots N) \land j \in (1 \dots N)) \to if (i = N, if (j = N, 1_{R}, 0_{R}), i W j) = P (i) (I ((1 \dots N) minMatR1 R) (M) J) Q (j)$
118	117	mpoeq3dva	$⊢ φ \to (i \in (1 \dots N), j \in (1 \dots N) ⟼ if (i = N, if (j = N, 1_{R}, 0_{R}), i W j)) = (i \in (1 \dots N), j \in (1 \dots N) ⟼ P (i) (I ((1 \dots N) minMatR1 R) (M) J) Q (j))$
119		eqid	$⊢ {Base}_{R} = {Base}_{R}$
120	17	3ad2ant1	$⊢ (φ \land i \in (1 \dots N) \land j \in (1 \dots N)) \to P \in G$
121	72 13	symgfv	$⊢ (P \in G \land i \in (1 \dots N)) \to P (i) \in (1 \dots N)$
122	120 107 121	syl2anc	$⊢ (φ \land i \in (1 \dots N) \land j \in (1 \dots N)) \to P (i) \in (1 \dots N)$
123	31	3ad2ant1	$⊢ (φ \land i \in (1 \dots N) \land j \in (1 \dots N)) \to U \in B$
124	2 119 1 122 74 123	matecld	$⊢ (φ \land i \in (1 \dots N) \land j \in (1 \dots N)) \to P (i) U Q (j) \in {Base}_{R}$
125	2 119 1 26 9 124	matbas2d	$⊢ φ \to (i \in (1 \dots N), j \in (1 \dots N) ⟼ P (i) U Q (j)) \in B$
126	16 125	eqeltrid	$⊢ φ \to W \in B$
127	119 51	ringidcl	$⊢ R \in Ring \to 1_{R} \in {Base}_{R}$
128	28 127	syl	$⊢ φ \to 1_{R} \in {Base}_{R}$
129		eqid	$⊢ (1 \dots N) matRRep R = (1 \dots N) matRRep R$
130	2 1 129 52	marrepval	$⊢ ((W \in B \land 1_{R} \in {Base}_{R}) \land (N \in (1 \dots N) \land N \in (1 \dots N))) \to N (W ((1 \dots N) matRRep R) 1_{R}) N = (i \in (1 \dots N), j \in (1 \dots N) ⟼ if (i = N, if (j = N, 1_{R}, 0_{R}), i W j))$
131	126 128 93 93 130	syl22anc	$⊢ φ \to N (W ((1 \dots N) matRRep R) 1_{R}) N = (i \in (1 \dots N), j \in (1 \dots N) ⟼ if (i = N, if (j = N, 1_{R}, 0_{R}), i W j))$
132	114	a1i	$⊢ φ \to W = (i \in (1 \dots N), j \in (1 \dots N) ⟼ P (i) (I ((1 \dots N) minMatR1 R) (M) J) Q (j))$
133	118 131 132	3eqtr4d	$⊢ φ \to N (W ((1 \dots N) matRRep R) 1_{R}) N = W$
134	133	fveq2d	$⊢ φ \to D (N (W ((1 \dots N) matRRep R) 1_{R}) N) = D (W)$
135		eqid	$⊢ (1 \dots N) subMat R = (1 \dots N) subMat R$
136	2 135 1	submaval	$⊢ (W \in B \land N \in (1 \dots N) \land N \in (1 \dots N)) \to N ((1 \dots N) subMat R) (W) N = (i \in ((1 \dots N) ∖ \{N\}), j \in ((1 \dots N) ∖ \{N\}) ⟼ i W j)$
137	126 93 93 136	syl3anc	$⊢ φ \to N ((1 \dots N) subMat R) (W) N = (i \in ((1 \dots N) ∖ \{N\}), j \in ((1 \dots N) ∖ \{N\}) ⟼ i W j)$
138		fzdif2	$⊢ N \in ℤ_{\geq 1} \to (1 \dots N) ∖ \{N\} = (1 \dots N - 1)$
139	91 138	syl	$⊢ φ \to (1 \dots N) ∖ \{N\} = (1 \dots N - 1)$
140		mpoeq12	$⊢ ((1 \dots N) ∖ \{N\} = (1 \dots N - 1) \land (1 \dots N) ∖ \{N\} = (1 \dots N - 1)) \to (i \in ((1 \dots N) ∖ \{N\}), j \in ((1 \dots N) ∖ \{N\}) ⟼ i W j) = (i \in (1 \dots N - 1), j \in (1 \dots N - 1) ⟼ i W j)$
141	139 139 140	syl2anc	$⊢ φ \to (i \in ((1 \dots N) ∖ \{N\}), j \in ((1 \dots N) ∖ \{N\}) ⟼ i W j) = (i \in (1 \dots N - 1), j \in (1 \dots N - 1) ⟼ i W j)$
142	137 141	eqtrd	$⊢ φ \to N ((1 \dots N) subMat R) (W) N = (i \in (1 \dots N - 1), j \in (1 \dots N - 1) ⟼ i W j)$
143		difssd	$⊢ φ \to (1 \dots N) ∖ \{N\} \subseteq (1 \dots N)$
144	139 143	eqsstrrd	$⊢ φ \to (1 \dots N - 1) \subseteq (1 \dots N)$
145	2 1	submabas	$⊢ (W \in B \land (1 \dots N - 1) \subseteq (1 \dots N)) \to (i \in (1 \dots N - 1), j \in (1 \dots N - 1) ⟼ i W j) \in {Base}_{((1 \dots N - 1) Mat R)}$
146	126 144 145	syl2anc	$⊢ φ \to (i \in (1 \dots N - 1), j \in (1 \dots N - 1) ⟼ i W j) \in {Base}_{((1 \dots N - 1) Mat R)}$
147	142 146	eqeltrd	$⊢ φ \to N ((1 \dots N) subMat R) (W) N \in {Base}_{((1 \dots N - 1) Mat R)}$
148		eqid	$⊢ (1 \dots N - 1) Mat R = (1 \dots N - 1) Mat R$
149		eqid	$⊢ {Base}_{((1 \dots N - 1) Mat R)} = {Base}_{((1 \dots N - 1) Mat R)}$
150	7 148 149 119	mdetcl	$⊢ (R \in CRing \land N ((1 \dots N) subMat R) (W) N \in {Base}_{((1 \dots N - 1) Mat R)}) \to E (N ((1 \dots N) subMat R) (W) N) \in {Base}_{R}$
151	9 147 150	syl2anc	$⊢ φ \to E (N ((1 \dots N) subMat R) (W) N) \in {Base}_{R}$
152	119 5 51	ringlidm	$⊢ (R \in Ring \land E (N ((1 \dots N) subMat R) (W) N) \in {Base}_{R}) \to 1_{R} \underset{˙}{\cdot} E (N ((1 \dots N) subMat R) (W) N) = E (N ((1 \dots N) subMat R) (W) N)$
153	28 151 152	syl2anc	$⊢ φ \to 1_{R} \underset{˙}{\cdot} E (N ((1 \dots N) subMat R) (W) N) = E (N ((1 \dots N) subMat R) (W) N)$
154	2	fveq2i	$⊢ {Base}_{A} = {Base}_{((1 \dots N) Mat R)}$
155	1 154	eqtri	$⊢ B = {Base}_{((1 \dots N) Mat R)}$
156	126 155	eleqtrdi	$⊢ φ \to W \in {Base}_{((1 \dots N) Mat R)}$
157		smadiadetr	$⊢ ((R \in CRing \land W \in {Base}_{((1 \dots N) Mat R)}) \land (N \in (1 \dots N) \land 1_{R} \in {Base}_{R})) \to ((1 \dots N) maDet R) (N (W ((1 \dots N) matRRep R) 1_{R}) N) = 1_{R} \cdot_{R} (((1 \dots N) ∖ \{N\}) maDet R) (N ((1 \dots N) subMat R) (W) N)$
158	9 156 93 128 157	syl22anc	$⊢ φ \to ((1 \dots N) maDet R) (N (W ((1 \dots N) matRRep R) 1_{R}) N) = 1_{R} \cdot_{R} (((1 \dots N) ∖ \{N\}) maDet R) (N ((1 \dots N) subMat R) (W) N)$
159	3	fveq1i	$⊢ D (N (W ((1 \dots N) matRRep R) 1_{R}) N) = ((1 \dots N) maDet R) (N (W ((1 \dots N) matRRep R) 1_{R}) N)$
160	5	oveqi	$⊢ 1_{R} \underset{˙}{\cdot} (((1 \dots N) ∖ \{N\}) maDet R) (N ((1 \dots N) subMat R) (W) N) = 1_{R} \cdot_{R} (((1 \dots N) ∖ \{N\}) maDet R) (N ((1 \dots N) subMat R) (W) N)$
161	159 160	eqeq12i	$⊢ D (N (W ((1 \dots N) matRRep R) 1_{R}) N) = 1_{R} \underset{˙}{\cdot} (((1 \dots N) ∖ \{N\}) maDet R) (N ((1 \dots N) subMat R) (W) N) \leftrightarrow ((1 \dots N) maDet R) (N (W ((1 \dots N) matRRep R) 1_{R}) N) = 1_{R} \cdot_{R} (((1 \dots N) ∖ \{N\}) maDet R) (N ((1 \dots N) subMat R) (W) N)$
162	158 161	sylibr	$⊢ φ \to D (N (W ((1 \dots N) matRRep R) 1_{R}) N) = 1_{R} \underset{˙}{\cdot} (((1 \dots N) ∖ \{N\}) maDet R) (N ((1 \dots N) subMat R) (W) N)$
163	139	oveq1d	$⊢ φ \to ((1 \dots N) ∖ \{N\}) maDet R = (1 \dots N - 1) maDet R$
164	163 7	eqtr4di	$⊢ φ \to ((1 \dots N) ∖ \{N\}) maDet R = E$
165	164	fveq1d	$⊢ φ \to (((1 \dots N) ∖ \{N\}) maDet R) (N ((1 \dots N) subMat R) (W) N) = E (N ((1 \dots N) subMat R) (W) N)$
166	165	oveq2d	$⊢ φ \to 1_{R} \underset{˙}{\cdot} (((1 \dots N) ∖ \{N\}) maDet R) (N ((1 \dots N) subMat R) (W) N) = 1_{R} \underset{˙}{\cdot} E (N ((1 \dots N) subMat R) (W) N)$
167	162 166	eqtrd	$⊢ φ \to D (N (W ((1 \dots N) matRRep R) 1_{R}) N) = 1_{R} \underset{˙}{\cdot} E (N ((1 \dots N) subMat R) (W) N)$
168	2 1	submat1n	$⊢ (N \in ℕ \land W \in B) \to N {subMat}_{1} (W) N = N ((1 \dots N) subMat R) (W) N$
169	8 126 168	syl2anc	$⊢ φ \to N {subMat}_{1} (W) N = N ((1 \dots N) subMat R) (W) N$
170	169	fveq2d	$⊢ φ \to E (N {subMat}_{1} (W) N) = E (N ((1 \dots N) subMat R) (W) N)$
171	153 167 170	3eqtr4d	$⊢ φ \to D (N (W ((1 \dots N) matRRep R) 1_{R}) N) = E (N {subMat}_{1} (W) N)$
172	134 171	eqtr3d	$⊢ φ \to D (W) = E (N {subMat}_{1} (W) N)$
173	2 1 8 10 11 28 12 15	submatminr1	$⊢ φ \to I {subMat}_{1} (M) J = I {subMat}_{1} (U) J$
174	173 21	eqtrd	$⊢ φ \to I {subMat}_{1} (M) J = N {subMat}_{1} (W) N$
175	174	fveq2d	$⊢ φ \to E (I {subMat}_{1} (M) J) = E (N {subMat}_{1} (W) N)$
176	172 175	eqtr4d	$⊢ φ \to D (W) = E (I {subMat}_{1} (M) J)$
177	176	oveq2d	$⊢ φ \to Z (S (P) S (Q)) \underset{˙}{\cdot} D (W) = Z (S (P) S (Q)) \underset{˙}{\cdot} E (I {subMat}_{1} (M) J)$
178	25 32 177	3eqtrd	$⊢ φ \to J K (M) I = Z (S (P) S (Q)) \underset{˙}{\cdot} E (I {subMat}_{1} (M) J)$

Metamath Proof Explorer

Theorem madjusmdetlem1

Proof