smadiadetglem1

	Ref	Expression
Hypotheses	smadiadet.a	$⊢ A = N Mat R$
	smadiadet.b	$⊢ B = {Base}_{A}$
	smadiadet.r	$⊢ R \in CRing$
	smadiadet.d	$⊢ D = N maDet R$
	smadiadet.h	$⊢ E = (N ∖ \{K\}) maDet R$
Assertion	smadiadetglem1	$⊢ (M \in B \land K \in N \land S \in {Base}_{R}) \to {(K (M (N matRRep R) S) K) ↾}_{((N ∖ \{K\}) \times N)} = {(K (N minMatR1 R) (M) K) ↾}_{((N ∖ \{K\}) \times N)}$

Proof

Step	Hyp	Ref	Expression
1		smadiadet.a	$⊢ A = N Mat R$
2		smadiadet.b	$⊢ B = {Base}_{A}$
3		smadiadet.r	$⊢ R \in CRing$
4		smadiadet.d	$⊢ D = N maDet R$
5		smadiadet.h	$⊢ E = (N ∖ \{K\}) maDet R$
6		mpodifsnif	$⊢ (i \in (N ∖ \{K\}), j \in N ⟼ if (i = K, if (j = K, S, 0_{R}), i M j)) = (i \in (N ∖ \{K\}), j \in N ⟼ i M j)$
7		mpodifsnif	$⊢ (i \in (N ∖ \{K\}), j \in N ⟼ if (i = K, if (j = K, 1_{R}, 0_{R}), i M j)) = (i \in (N ∖ \{K\}), j \in N ⟼ i M j)$
8	6 7	eqtr4i	$⊢ (i \in (N ∖ \{K\}), j \in N ⟼ if (i = K, if (j = K, S, 0_{R}), i M j)) = (i \in (N ∖ \{K\}), j \in N ⟼ if (i = K, if (j = K, 1_{R}, 0_{R}), i M j))$
9		difss	$⊢ N ∖ \{K\} \subseteq N$
10		ssid	$⊢ N \subseteq N$
11	9 10	pm3.2i	$⊢ (N ∖ \{K\} \subseteq N \land N \subseteq N)$
12		resmpo	$⊢ (N ∖ \{K\} \subseteq N \land N \subseteq N) \to {(i \in N, j \in N ⟼ if (i = K, if (j = K, S, 0_{R}), i M j)) ↾}_{((N ∖ \{K\}) \times N)} = (i \in (N ∖ \{K\}), j \in N ⟼ if (i = K, if (j = K, S, 0_{R}), i M j))$
13	11 12	mp1i	$⊢ (M \in B \land K \in N \land S \in {Base}_{R}) \to {(i \in N, j \in N ⟼ if (i = K, if (j = K, S, 0_{R}), i M j)) ↾}_{((N ∖ \{K\}) \times N)} = (i \in (N ∖ \{K\}), j \in N ⟼ if (i = K, if (j = K, S, 0_{R}), i M j))$
14		resmpo	$⊢ (N ∖ \{K\} \subseteq N \land N \subseteq N) \to {(i \in N, j \in N ⟼ if (i = K, if (j = K, 1_{R}, 0_{R}), i M j)) ↾}_{((N ∖ \{K\}) \times N)} = (i \in (N ∖ \{K\}), j \in N ⟼ if (i = K, if (j = K, 1_{R}, 0_{R}), i M j))$
15	11 14	mp1i	$⊢ (M \in B \land K \in N \land S \in {Base}_{R}) \to {(i \in N, j \in N ⟼ if (i = K, if (j = K, 1_{R}, 0_{R}), i M j)) ↾}_{((N ∖ \{K\}) \times N)} = (i \in (N ∖ \{K\}), j \in N ⟼ if (i = K, if (j = K, 1_{R}, 0_{R}), i M j))$
16	8 13 15	3eqtr4a	$⊢ (M \in B \land K \in N \land S \in {Base}_{R}) \to {(i \in N, j \in N ⟼ if (i = K, if (j = K, S, 0_{R}), i M j)) ↾}_{((N ∖ \{K\}) \times N)} = {(i \in N, j \in N ⟼ if (i = K, if (j = K, 1_{R}, 0_{R}), i M j)) ↾}_{((N ∖ \{K\}) \times N)}$
17		simp1	$⊢ (M \in B \land K \in N \land S \in {Base}_{R}) \to M \in B$
18		simp3	$⊢ (M \in B \land K \in N \land S \in {Base}_{R}) \to S \in {Base}_{R}$
19		simp2	$⊢ (M \in B \land K \in N \land S \in {Base}_{R}) \to K \in N$
20		eqid	$⊢ N matRRep R = N matRRep R$
21		eqid	$⊢ 0_{R} = 0_{R}$
22	1 2 20 21	marrepval	$⊢ ((M \in B \land S \in {Base}_{R}) \land (K \in N \land K \in N)) \to K (M (N matRRep R) S) K = (i \in N, j \in N ⟼ if (i = K, if (j = K, S, 0_{R}), i M j))$
23	17 18 19 19 22	syl22anc	$⊢ (M \in B \land K \in N \land S \in {Base}_{R}) \to K (M (N matRRep R) S) K = (i \in N, j \in N ⟼ if (i = K, if (j = K, S, 0_{R}), i M j))$
24	23	reseq1d	$⊢ (M \in B \land K \in N \land S \in {Base}_{R}) \to {(K (M (N matRRep R) S) K) ↾}_{((N ∖ \{K\}) \times N)} = {(i \in N, j \in N ⟼ if (i = K, if (j = K, S, 0_{R}), i M j)) ↾}_{((N ∖ \{K\}) \times N)}$
25		crngring	$⊢ R \in CRing \to R \in Ring$
26		eqid	$⊢ {Base}_{R} = {Base}_{R}$
27		eqid	$⊢ 1_{R} = 1_{R}$
28	26 27	ringidcl	$⊢ R \in Ring \to 1_{R} \in {Base}_{R}$
29	25 28	syl	$⊢ R \in CRing \to 1_{R} \in {Base}_{R}$
30	3 29	mp1i	$⊢ (M \in B \land K \in N \land S \in {Base}_{R}) \to 1_{R} \in {Base}_{R}$
31	1 2 20 21	marrepval	$⊢ ((M \in B \land 1_{R} \in {Base}_{R}) \land (K \in N \land K \in N)) \to K (M (N matRRep R) 1_{R}) K = (i \in N, j \in N ⟼ if (i = K, if (j = K, 1_{R}, 0_{R}), i M j))$
32	17 30 19 19 31	syl22anc	$⊢ (M \in B \land K \in N \land S \in {Base}_{R}) \to K (M (N matRRep R) 1_{R}) K = (i \in N, j \in N ⟼ if (i = K, if (j = K, 1_{R}, 0_{R}), i M j))$
33	32	reseq1d	$⊢ (M \in B \land K \in N \land S \in {Base}_{R}) \to {(K (M (N matRRep R) 1_{R}) K) ↾}_{((N ∖ \{K\}) \times N)} = {(i \in N, j \in N ⟼ if (i = K, if (j = K, 1_{R}, 0_{R}), i M j)) ↾}_{((N ∖ \{K\}) \times N)}$
34	16 24 33	3eqtr4d	$⊢ (M \in B \land K \in N \land S \in {Base}_{R}) \to {(K (M (N matRRep R) S) K) ↾}_{((N ∖ \{K\}) \times N)} = {(K (M (N matRRep R) 1_{R}) K) ↾}_{((N ∖ \{K\}) \times N)}$
35	3 25	ax-mp	$⊢ R \in Ring$
36	1 2 27	minmar1marrep	$⊢ (R \in Ring \land M \in B) \to (N minMatR1 R) (M) = M (N matRRep R) 1_{R}$
37	35 17 36	sylancr	$⊢ (M \in B \land K \in N \land S \in {Base}_{R}) \to (N minMatR1 R) (M) = M (N matRRep R) 1_{R}$
38	37	eqcomd	$⊢ (M \in B \land K \in N \land S \in {Base}_{R}) \to M (N matRRep R) 1_{R} = (N minMatR1 R) (M)$
39	38	oveqd	$⊢ (M \in B \land K \in N \land S \in {Base}_{R}) \to K (M (N matRRep R) 1_{R}) K = K (N minMatR1 R) (M) K$
40	39	reseq1d	$⊢ (M \in B \land K \in N \land S \in {Base}_{R}) \to {(K (M (N matRRep R) 1_{R}) K) ↾}_{((N ∖ \{K\}) \times N)} = {(K (N minMatR1 R) (M) K) ↾}_{((N ∖ \{K\}) \times N)}$
41	34 40	eqtrd	$⊢ (M \in B \land K \in N \land S \in {Base}_{R}) \to {(K (M (N matRRep R) S) K) ↾}_{((N ∖ \{K\}) \times N)} = {(K (N minMatR1 R) (M) K) ↾}_{((N ∖ \{K\}) \times N)}$

Metamath Proof Explorer

Theorem smadiadetglem1

Proof