smadiadetglem2

	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$
	smadiadetg.x	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
Assertion	smadiadetglem2	$⊢ (M \in B \land K \in N \land S \in {Base}_{R}) \to {(K (M (N matRRep R) S) K) ↾}_{(\{K\} \times N)} = ((\{K\} \times N) \times \{S\}) {\underset{˙}{\cdot}}_{f} ({(K (N minMatR1 R) (M) K) ↾}_{(\{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		smadiadetg.x	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
7		snex	$⊢ \{K\} \in V$
8	7	a1i	$⊢ (M \in B \land K \in N \land S \in {Base}_{R}) \to \{K\} \in V$
9	1 2	matrcl	$⊢ M \in B \to (N \in Fin \land R \in V)$
10		elex	$⊢ N \in Fin \to N \in V$
11	10	adantr	$⊢ (N \in Fin \land R \in V) \to N \in V$
12	9 11	syl	$⊢ M \in B \to N \in V$
13	12	3ad2ant1	$⊢ (M \in B \land K \in N \land S \in {Base}_{R}) \to N \in V$
14		simp13	$⊢ ((M \in B \land K \in N \land S \in {Base}_{R}) \land i \in \{K\} \land j \in N) \to S \in {Base}_{R}$
15		crngring	$⊢ R \in CRing \to R \in Ring$
16	3 15	mp1i	$⊢ ((M \in B \land K \in N \land S \in {Base}_{R}) \land i \in \{K\} \land j \in N) \to R \in Ring$
17		eqid	$⊢ {Base}_{R} = {Base}_{R}$
18		eqid	$⊢ 1_{R} = 1_{R}$
19	17 18	ringidcl	$⊢ R \in Ring \to 1_{R} \in {Base}_{R}$
20		eqid	$⊢ 0_{R} = 0_{R}$
21	17 20	ring0cl	$⊢ R \in Ring \to 0_{R} \in {Base}_{R}$
22	19 21	ifcld	$⊢ R \in Ring \to if (j = K, 1_{R}, 0_{R}) \in {Base}_{R}$
23	16 22	syl	$⊢ ((M \in B \land K \in N \land S \in {Base}_{R}) \land i \in \{K\} \land j \in N) \to if (j = K, 1_{R}, 0_{R}) \in {Base}_{R}$
24		fconstmpo	$⊢ (\{K\} \times N) \times \{S\} = (i \in \{K\}, j \in N ⟼ S)$
25	24	a1i	$⊢ (M \in B \land K \in N \land S \in {Base}_{R}) \to (\{K\} \times N) \times \{S\} = (i \in \{K\}, j \in N ⟼ S)$
26		eqidd	$⊢ (M \in B \land K \in N \land S \in {Base}_{R}) \to (i \in \{K\}, j \in N ⟼ if (j = K, 1_{R}, 0_{R})) = (i \in \{K\}, j \in N ⟼ if (j = K, 1_{R}, 0_{R}))$
27	8 13 14 23 25 26	offval22	$⊢ (M \in B \land K \in N \land S \in {Base}_{R}) \to ((\{K\} \times N) \times \{S\}) {\underset{˙}{\cdot}}_{f} (i \in \{K\}, j \in N ⟼ if (j = K, 1_{R}, 0_{R})) = (i \in \{K\}, j \in N ⟼ S \underset{˙}{\cdot} if (j = K, 1_{R}, 0_{R}))$
28	3 15	mp1i	$⊢ S \in {Base}_{R} \to R \in Ring$
29	17 6 18	ringridm	$⊢ (R \in Ring \land S \in {Base}_{R}) \to S \underset{˙}{\cdot} 1_{R} = S$
30	28 29	mpancom	$⊢ S \in {Base}_{R} \to S \underset{˙}{\cdot} 1_{R} = S$
31	30	3ad2ant3	$⊢ (M \in B \land K \in N \land S \in {Base}_{R}) \to S \underset{˙}{\cdot} 1_{R} = S$
32	31	ad2antrl	$⊢ (j = K \land ((M \in B \land K \in N \land S \in {Base}_{R}) \land j \in N)) \to S \underset{˙}{\cdot} 1_{R} = S$
33		iftrue	$⊢ j = K \to if (j = K, 1_{R}, 0_{R}) = 1_{R}$
34	33	adantr	$⊢ (j = K \land ((M \in B \land K \in N \land S \in {Base}_{R}) \land j \in N)) \to if (j = K, 1_{R}, 0_{R}) = 1_{R}$
35	34	oveq2d	$⊢ (j = K \land ((M \in B \land K \in N \land S \in {Base}_{R}) \land j \in N)) \to S \underset{˙}{\cdot} if (j = K, 1_{R}, 0_{R}) = S \underset{˙}{\cdot} 1_{R}$
36		iftrue	$⊢ j = K \to if (j = K, S, 0_{R}) = S$
37	36	adantr	$⊢ (j = K \land ((M \in B \land K \in N \land S \in {Base}_{R}) \land j \in N)) \to if (j = K, S, 0_{R}) = S$
38	32 35 37	3eqtr4d	$⊢ (j = K \land ((M \in B \land K \in N \land S \in {Base}_{R}) \land j \in N)) \to S \underset{˙}{\cdot} if (j = K, 1_{R}, 0_{R}) = if (j = K, S, 0_{R})$
39	17 6 20	ringrz	$⊢ (R \in Ring \land S \in {Base}_{R}) \to S \underset{˙}{\cdot} 0_{R} = 0_{R}$
40	28 39	mpancom	$⊢ S \in {Base}_{R} \to S \underset{˙}{\cdot} 0_{R} = 0_{R}$
41	40	3ad2ant3	$⊢ (M \in B \land K \in N \land S \in {Base}_{R}) \to S \underset{˙}{\cdot} 0_{R} = 0_{R}$
42	41	ad2antrl	$⊢ (\neg j = K \land ((M \in B \land K \in N \land S \in {Base}_{R}) \land j \in N)) \to S \underset{˙}{\cdot} 0_{R} = 0_{R}$
43		iffalse	$⊢ \neg j = K \to if (j = K, 1_{R}, 0_{R}) = 0_{R}$
44	43	oveq2d	$⊢ \neg j = K \to S \underset{˙}{\cdot} if (j = K, 1_{R}, 0_{R}) = S \underset{˙}{\cdot} 0_{R}$
45	44	adantr	$⊢ (\neg j = K \land ((M \in B \land K \in N \land S \in {Base}_{R}) \land j \in N)) \to S \underset{˙}{\cdot} if (j = K, 1_{R}, 0_{R}) = S \underset{˙}{\cdot} 0_{R}$
46		iffalse	$⊢ \neg j = K \to if (j = K, S, 0_{R}) = 0_{R}$
47	46	adantr	$⊢ (\neg j = K \land ((M \in B \land K \in N \land S \in {Base}_{R}) \land j \in N)) \to if (j = K, S, 0_{R}) = 0_{R}$
48	42 45 47	3eqtr4d	$⊢ (\neg j = K \land ((M \in B \land K \in N \land S \in {Base}_{R}) \land j \in N)) \to S \underset{˙}{\cdot} if (j = K, 1_{R}, 0_{R}) = if (j = K, S, 0_{R})$
49	38 48	pm2.61ian	$⊢ ((M \in B \land K \in N \land S \in {Base}_{R}) \land j \in N) \to S \underset{˙}{\cdot} if (j = K, 1_{R}, 0_{R}) = if (j = K, S, 0_{R})$
50	49	3adant2	$⊢ ((M \in B \land K \in N \land S \in {Base}_{R}) \land i \in \{K\} \land j \in N) \to S \underset{˙}{\cdot} if (j = K, 1_{R}, 0_{R}) = if (j = K, S, 0_{R})$
51	50	mpoeq3dva	$⊢ (M \in B \land K \in N \land S \in {Base}_{R}) \to (i \in \{K\}, j \in N ⟼ S \underset{˙}{\cdot} if (j = K, 1_{R}, 0_{R})) = (i \in \{K\}, j \in N ⟼ if (j = K, S, 0_{R}))$
52	27 51	eqtrd	$⊢ (M \in B \land K \in N \land S \in {Base}_{R}) \to ((\{K\} \times N) \times \{S\}) {\underset{˙}{\cdot}}_{f} (i \in \{K\}, j \in N ⟼ if (j = K, 1_{R}, 0_{R})) = (i \in \{K\}, j \in N ⟼ if (j = K, S, 0_{R}))$
53		simp2	$⊢ (M \in B \land K \in N \land S \in {Base}_{R}) \to K \in N$
54		eqid	$⊢ N minMatR1 R = N minMatR1 R$
55	1 2 54 18 20	minmar1val	$⊢ (M \in B \land K \in N \land K \in N) \to K (N minMatR1 R) (M) K = (i \in N, j \in N ⟼ if (i = K, if (j = K, 1_{R}, 0_{R}), i M j))$
56	53 55	syld3an3	$⊢ (M \in B \land K \in N \land S \in {Base}_{R}) \to K (N minMatR1 R) (M) K = (i \in N, j \in N ⟼ if (i = K, if (j = K, 1_{R}, 0_{R}), i M j))$
57	56	reseq1d	$⊢ (M \in B \land K \in N \land S \in {Base}_{R}) \to {(K (N minMatR1 R) (M) K) ↾}_{(\{K\} \times N)} = {(i \in N, j \in N ⟼ if (i = K, if (j = K, 1_{R}, 0_{R}), i M j)) ↾}_{(\{K\} \times N)}$
58		snssi	$⊢ K \in N \to \{K\} \subseteq N$
59	58	3ad2ant2	$⊢ (M \in B \land K \in N \land S \in {Base}_{R}) \to \{K\} \subseteq N$
60		ssid	$⊢ N \subseteq N$
61		resmpo	$⊢ (\{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)) ↾}_{(\{K\} \times N)} = (i \in \{K\}, j \in N ⟼ if (i = K, if (j = K, 1_{R}, 0_{R}), i M j))$
62	59 60 61	sylancl	$⊢ (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)) ↾}_{(\{K\} \times N)} = (i \in \{K\}, j \in N ⟼ if (i = K, if (j = K, 1_{R}, 0_{R}), i M j))$
63		mposnif	$⊢ (i \in \{K\}, j \in N ⟼ if (i = K, if (j = K, 1_{R}, 0_{R}), i M j)) = (i \in \{K\}, j \in N ⟼ if (j = K, 1_{R}, 0_{R}))$
64	63	a1i	$⊢ (M \in B \land K \in N \land S \in {Base}_{R}) \to (i \in \{K\}, j \in N ⟼ if (i = K, if (j = K, 1_{R}, 0_{R}), i M j)) = (i \in \{K\}, j \in N ⟼ if (j = K, 1_{R}, 0_{R}))$
65	57 62 64	3eqtrd	$⊢ (M \in B \land K \in N \land S \in {Base}_{R}) \to {(K (N minMatR1 R) (M) K) ↾}_{(\{K\} \times N)} = (i \in \{K\}, j \in N ⟼ if (j = K, 1_{R}, 0_{R}))$
66	65	oveq2d	$⊢ (M \in B \land K \in N \land S \in {Base}_{R}) \to ((\{K\} \times N) \times \{S\}) {\underset{˙}{\cdot}}_{f} ({(K (N minMatR1 R) (M) K) ↾}_{(\{K\} \times N)}) = ((\{K\} \times N) \times \{S\}) {\underset{˙}{\cdot}}_{f} (i \in \{K\}, j \in N ⟼ if (j = K, 1_{R}, 0_{R}))$
67		3simpb	$⊢ (M \in B \land K \in N \land S \in {Base}_{R}) \to (M \in B \land S \in {Base}_{R})$
68		eqid	$⊢ N matRRep R = N matRRep R$
69	1 2 68 20	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))$
70	67 53 53 69	syl12anc	$⊢ (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))$
71	70	reseq1d	$⊢ (M \in B \land K \in N \land S \in {Base}_{R}) \to {(K (M (N matRRep R) S) K) ↾}_{(\{K\} \times N)} = {(i \in N, j \in N ⟼ if (i = K, if (j = K, S, 0_{R}), i M j)) ↾}_{(\{K\} \times N)}$
72		resmpo	$⊢ (\{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)) ↾}_{(\{K\} \times N)} = (i \in \{K\}, j \in N ⟼ if (i = K, if (j = K, S, 0_{R}), i M j))$
73	59 60 72	sylancl	$⊢ (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)) ↾}_{(\{K\} \times N)} = (i \in \{K\}, j \in N ⟼ if (i = K, if (j = K, S, 0_{R}), i M j))$
74		mposnif	$⊢ (i \in \{K\}, j \in N ⟼ if (i = K, if (j = K, S, 0_{R}), i M j)) = (i \in \{K\}, j \in N ⟼ if (j = K, S, 0_{R}))$
75	74	a1i	$⊢ (M \in B \land K \in N \land S \in {Base}_{R}) \to (i \in \{K\}, j \in N ⟼ if (i = K, if (j = K, S, 0_{R}), i M j)) = (i \in \{K\}, j \in N ⟼ if (j = K, S, 0_{R}))$
76	71 73 75	3eqtrd	$⊢ (M \in B \land K \in N \land S \in {Base}_{R}) \to {(K (M (N matRRep R) S) K) ↾}_{(\{K\} \times N)} = (i \in \{K\}, j \in N ⟼ if (j = K, S, 0_{R}))$
77	52 66 76	3eqtr4rd	$⊢ (M \in B \land K \in N \land S \in {Base}_{R}) \to {(K (M (N matRRep R) S) K) ↾}_{(\{K\} \times N)} = ((\{K\} \times N) \times \{S\}) {\underset{˙}{\cdot}}_{f} ({(K (N minMatR1 R) (M) K) ↾}_{(\{K\} \times N)})$

Metamath Proof Explorer

Theorem smadiadetglem2

Proof