Metamath Proof Explorer

Theorem smadiadetglem1

Description: Lemma 1 for smadiadetg . (Contributed by AV, 13-Feb-2019)

Ref Expression
Hypotheses smadiadet.a ⊢ A = N Mat R
smadiadet.b ⊢ B = Base A
smadiadet.r ⊢ R ∈ CRing
smadiadet.d ⊢ D = N maDet R
smadiadet.h ⊢ E = N ∖ K maDet R
Assertion smadiadetglem1 ⊢ M ∈ B ∧ K ∈ N ∧ S ∈ Base R → K M N matRRep R S K ↾ N ∖ K × N = K N minMatR1 R ⁡ M K ↾ N ∖ K × N

Proof

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