Step | Hyp | Ref
| Expression |
1 | | mpodifsnif 7254 |
. . . . 5
⊢ (𝑖 ∈ (𝑁 ∖ {𝐾}), 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐾, if(𝑗 = 𝐾, 𝑆, (0g‘𝑅)), (𝑖𝑀𝑗))) = (𝑖 ∈ (𝑁 ∖ {𝐾}), 𝑗 ∈ 𝑁 ↦ (𝑖𝑀𝑗)) |
2 | | mpodifsnif 7254 |
. . . . 5
⊢ (𝑖 ∈ (𝑁 ∖ {𝐾}), 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐾, if(𝑗 = 𝐾, (1r‘𝑅), (0g‘𝑅)), (𝑖𝑀𝑗))) = (𝑖 ∈ (𝑁 ∖ {𝐾}), 𝑗 ∈ 𝑁 ↦ (𝑖𝑀𝑗)) |
3 | 1, 2 | eqtr4i 2785 |
. . . 4
⊢ (𝑖 ∈ (𝑁 ∖ {𝐾}), 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐾, if(𝑗 = 𝐾, 𝑆, (0g‘𝑅)), (𝑖𝑀𝑗))) = (𝑖 ∈ (𝑁 ∖ {𝐾}), 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐾, if(𝑗 = 𝐾, (1r‘𝑅), (0g‘𝑅)), (𝑖𝑀𝑗))) |
4 | | difss 4033 |
. . . . . 6
⊢ (𝑁 ∖ {𝐾}) ⊆ 𝑁 |
5 | | ssid 3910 |
. . . . . 6
⊢ 𝑁 ⊆ 𝑁 |
6 | 4, 5 | pm3.2i 475 |
. . . . 5
⊢ ((𝑁 ∖ {𝐾}) ⊆ 𝑁 ∧ 𝑁 ⊆ 𝑁) |
7 | | resmpo 7259 |
. . . . 5
⊢ (((𝑁 ∖ {𝐾}) ⊆ 𝑁 ∧ 𝑁 ⊆ 𝑁) → ((𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐾, if(𝑗 = 𝐾, 𝑆, (0g‘𝑅)), (𝑖𝑀𝑗))) ↾ ((𝑁 ∖ {𝐾}) × 𝑁)) = (𝑖 ∈ (𝑁 ∖ {𝐾}), 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐾, if(𝑗 = 𝐾, 𝑆, (0g‘𝑅)), (𝑖𝑀𝑗)))) |
8 | 6, 7 | mp1i 13 |
. . . 4
⊢ ((𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝑆 ∈ (Base‘𝑅)) → ((𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐾, if(𝑗 = 𝐾, 𝑆, (0g‘𝑅)), (𝑖𝑀𝑗))) ↾ ((𝑁 ∖ {𝐾}) × 𝑁)) = (𝑖 ∈ (𝑁 ∖ {𝐾}), 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐾, if(𝑗 = 𝐾, 𝑆, (0g‘𝑅)), (𝑖𝑀𝑗)))) |
9 | | resmpo 7259 |
. . . . 5
⊢ (((𝑁 ∖ {𝐾}) ⊆ 𝑁 ∧ 𝑁 ⊆ 𝑁) → ((𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐾, if(𝑗 = 𝐾, (1r‘𝑅), (0g‘𝑅)), (𝑖𝑀𝑗))) ↾ ((𝑁 ∖ {𝐾}) × 𝑁)) = (𝑖 ∈ (𝑁 ∖ {𝐾}), 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐾, if(𝑗 = 𝐾, (1r‘𝑅), (0g‘𝑅)), (𝑖𝑀𝑗)))) |
10 | 6, 9 | mp1i 13 |
. . . 4
⊢ ((𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝑆 ∈ (Base‘𝑅)) → ((𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐾, if(𝑗 = 𝐾, (1r‘𝑅), (0g‘𝑅)), (𝑖𝑀𝑗))) ↾ ((𝑁 ∖ {𝐾}) × 𝑁)) = (𝑖 ∈ (𝑁 ∖ {𝐾}), 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐾, if(𝑗 = 𝐾, (1r‘𝑅), (0g‘𝑅)), (𝑖𝑀𝑗)))) |
11 | 3, 8, 10 | 3eqtr4a 2820 |
. . 3
⊢ ((𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝑆 ∈ (Base‘𝑅)) → ((𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐾, if(𝑗 = 𝐾, 𝑆, (0g‘𝑅)), (𝑖𝑀𝑗))) ↾ ((𝑁 ∖ {𝐾}) × 𝑁)) = ((𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐾, if(𝑗 = 𝐾, (1r‘𝑅), (0g‘𝑅)), (𝑖𝑀𝑗))) ↾ ((𝑁 ∖ {𝐾}) × 𝑁))) |
12 | | simp1 1134 |
. . . . 5
⊢ ((𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝑆 ∈ (Base‘𝑅)) → 𝑀 ∈ 𝐵) |
13 | | simp3 1136 |
. . . . 5
⊢ ((𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝑆 ∈ (Base‘𝑅)) → 𝑆 ∈ (Base‘𝑅)) |
14 | | simp2 1135 |
. . . . 5
⊢ ((𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝑆 ∈ (Base‘𝑅)) → 𝐾 ∈ 𝑁) |
15 | | smadiadet.a |
. . . . . 6
⊢ 𝐴 = (𝑁 Mat 𝑅) |
16 | | smadiadet.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝐴) |
17 | | eqid 2759 |
. . . . . 6
⊢ (𝑁 matRRep 𝑅) = (𝑁 matRRep 𝑅) |
18 | | eqid 2759 |
. . . . . 6
⊢
(0g‘𝑅) = (0g‘𝑅) |
19 | 15, 16, 17, 18 | marrepval 21247 |
. . . . 5
⊢ (((𝑀 ∈ 𝐵 ∧ 𝑆 ∈ (Base‘𝑅)) ∧ (𝐾 ∈ 𝑁 ∧ 𝐾 ∈ 𝑁)) → (𝐾(𝑀(𝑁 matRRep 𝑅)𝑆)𝐾) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐾, if(𝑗 = 𝐾, 𝑆, (0g‘𝑅)), (𝑖𝑀𝑗)))) |
20 | 12, 13, 14, 14, 19 | syl22anc 838 |
. . . 4
⊢ ((𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝑆 ∈ (Base‘𝑅)) → (𝐾(𝑀(𝑁 matRRep 𝑅)𝑆)𝐾) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐾, if(𝑗 = 𝐾, 𝑆, (0g‘𝑅)), (𝑖𝑀𝑗)))) |
21 | 20 | reseq1d 5815 |
. . 3
⊢ ((𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝑆 ∈ (Base‘𝑅)) → ((𝐾(𝑀(𝑁 matRRep 𝑅)𝑆)𝐾) ↾ ((𝑁 ∖ {𝐾}) × 𝑁)) = ((𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐾, if(𝑗 = 𝐾, 𝑆, (0g‘𝑅)), (𝑖𝑀𝑗))) ↾ ((𝑁 ∖ {𝐾}) × 𝑁))) |
22 | | smadiadet.r |
. . . . . 6
⊢ 𝑅 ∈ CRing |
23 | | crngring 19362 |
. . . . . . 7
⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring) |
24 | | eqid 2759 |
. . . . . . . 8
⊢
(Base‘𝑅) =
(Base‘𝑅) |
25 | | eqid 2759 |
. . . . . . . 8
⊢
(1r‘𝑅) = (1r‘𝑅) |
26 | 24, 25 | ringidcl 19374 |
. . . . . . 7
⊢ (𝑅 ∈ Ring →
(1r‘𝑅)
∈ (Base‘𝑅)) |
27 | 23, 26 | syl 17 |
. . . . . 6
⊢ (𝑅 ∈ CRing →
(1r‘𝑅)
∈ (Base‘𝑅)) |
28 | 22, 27 | mp1i 13 |
. . . . 5
⊢ ((𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝑆 ∈ (Base‘𝑅)) → (1r‘𝑅) ∈ (Base‘𝑅)) |
29 | 15, 16, 17, 18 | marrepval 21247 |
. . . . 5
⊢ (((𝑀 ∈ 𝐵 ∧ (1r‘𝑅) ∈ (Base‘𝑅)) ∧ (𝐾 ∈ 𝑁 ∧ 𝐾 ∈ 𝑁)) → (𝐾(𝑀(𝑁 matRRep 𝑅)(1r‘𝑅))𝐾) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐾, if(𝑗 = 𝐾, (1r‘𝑅), (0g‘𝑅)), (𝑖𝑀𝑗)))) |
30 | 12, 28, 14, 14, 29 | syl22anc 838 |
. . . 4
⊢ ((𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝑆 ∈ (Base‘𝑅)) → (𝐾(𝑀(𝑁 matRRep 𝑅)(1r‘𝑅))𝐾) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐾, if(𝑗 = 𝐾, (1r‘𝑅), (0g‘𝑅)), (𝑖𝑀𝑗)))) |
31 | 30 | reseq1d 5815 |
. . 3
⊢ ((𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝑆 ∈ (Base‘𝑅)) → ((𝐾(𝑀(𝑁 matRRep 𝑅)(1r‘𝑅))𝐾) ↾ ((𝑁 ∖ {𝐾}) × 𝑁)) = ((𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐾, if(𝑗 = 𝐾, (1r‘𝑅), (0g‘𝑅)), (𝑖𝑀𝑗))) ↾ ((𝑁 ∖ {𝐾}) × 𝑁))) |
32 | 11, 21, 31 | 3eqtr4d 2804 |
. 2
⊢ ((𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝑆 ∈ (Base‘𝑅)) → ((𝐾(𝑀(𝑁 matRRep 𝑅)𝑆)𝐾) ↾ ((𝑁 ∖ {𝐾}) × 𝑁)) = ((𝐾(𝑀(𝑁 matRRep 𝑅)(1r‘𝑅))𝐾) ↾ ((𝑁 ∖ {𝐾}) × 𝑁))) |
33 | 22, 23 | ax-mp 5 |
. . . . . 6
⊢ 𝑅 ∈ Ring |
34 | 15, 16, 25 | minmar1marrep 21335 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → ((𝑁 minMatR1 𝑅)‘𝑀) = (𝑀(𝑁 matRRep 𝑅)(1r‘𝑅))) |
35 | 33, 12, 34 | sylancr 591 |
. . . . 5
⊢ ((𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝑆 ∈ (Base‘𝑅)) → ((𝑁 minMatR1 𝑅)‘𝑀) = (𝑀(𝑁 matRRep 𝑅)(1r‘𝑅))) |
36 | 35 | eqcomd 2765 |
. . . 4
⊢ ((𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝑆 ∈ (Base‘𝑅)) → (𝑀(𝑁 matRRep 𝑅)(1r‘𝑅)) = ((𝑁 minMatR1 𝑅)‘𝑀)) |
37 | 36 | oveqd 7160 |
. . 3
⊢ ((𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝑆 ∈ (Base‘𝑅)) → (𝐾(𝑀(𝑁 matRRep 𝑅)(1r‘𝑅))𝐾) = (𝐾((𝑁 minMatR1 𝑅)‘𝑀)𝐾)) |
38 | 37 | reseq1d 5815 |
. 2
⊢ ((𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝑆 ∈ (Base‘𝑅)) → ((𝐾(𝑀(𝑁 matRRep 𝑅)(1r‘𝑅))𝐾) ↾ ((𝑁 ∖ {𝐾}) × 𝑁)) = ((𝐾((𝑁 minMatR1 𝑅)‘𝑀)𝐾) ↾ ((𝑁 ∖ {𝐾}) × 𝑁))) |
39 | 32, 38 | eqtrd 2794 |
1
⊢ ((𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝑆 ∈ (Base‘𝑅)) → ((𝐾(𝑀(𝑁 matRRep 𝑅)𝑆)𝐾) ↾ ((𝑁 ∖ {𝐾}) × 𝑁)) = ((𝐾((𝑁 minMatR1 𝑅)‘𝑀)𝐾) ↾ ((𝑁 ∖ {𝐾}) × 𝑁))) |