Step | Hyp | Ref
| Expression |
1 | | fzdif2 30856 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘1) → ((1...𝑁) ∖ {𝑁}) = (1...(𝑁 − 1))) |
2 | | nnuz 12501 |
. . . . 5
⊢ ℕ =
(ℤ≥‘1) |
3 | 1, 2 | eleq2s 2857 |
. . . 4
⊢ (𝑁 ∈ ℕ →
((1...𝑁) ∖ {𝑁}) = (1...(𝑁 − 1))) |
4 | 3 | adantr 484 |
. . 3
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ 𝐵) → ((1...𝑁) ∖ {𝑁}) = (1...(𝑁 − 1))) |
5 | 4 | adantr 484 |
. . 3
⊢ (((𝑁 ∈ ℕ ∧ 𝑀 ∈ 𝐵) ∧ 𝑖 ∈ ((1...𝑁) ∖ {𝑁})) → ((1...𝑁) ∖ {𝑁}) = (1...(𝑁 − 1))) |
6 | | eqid 2738 |
. . . . 5
⊢ (𝑁(subMat1‘𝑀)𝑁) = (𝑁(subMat1‘𝑀)𝑁) |
7 | | elfz1end 13166 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ ↔ 𝑁 ∈ (1...𝑁)) |
8 | 7 | biimpi 219 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → 𝑁 ∈ (1...𝑁)) |
9 | 8 | adantr 484 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ 𝐵) → 𝑁 ∈ (1...𝑁)) |
10 | 9, 7 | sylibr 237 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ 𝐵) → 𝑁 ∈ ℕ) |
11 | 10 | adantr 484 |
. . . . 5
⊢ (((𝑁 ∈ ℕ ∧ 𝑀 ∈ 𝐵) ∧ (𝑖 ∈ ((1...𝑁) ∖ {𝑁}) ∧ 𝑗 ∈ ((1...𝑁) ∖ {𝑁}))) → 𝑁 ∈ ℕ) |
12 | 11, 8 | syl 17 |
. . . . 5
⊢ (((𝑁 ∈ ℕ ∧ 𝑀 ∈ 𝐵) ∧ (𝑖 ∈ ((1...𝑁) ∖ {𝑁}) ∧ 𝑗 ∈ ((1...𝑁) ∖ {𝑁}))) → 𝑁 ∈ (1...𝑁)) |
13 | | submat1n.a |
. . . . . . 7
⊢ 𝐴 = ((1...𝑁) Mat 𝑅) |
14 | | eqid 2738 |
. . . . . . 7
⊢
(Base‘𝑅) =
(Base‘𝑅) |
15 | | submat1n.b |
. . . . . . 7
⊢ 𝐵 = (Base‘𝐴) |
16 | 13, 14, 15 | matbas2i 21343 |
. . . . . 6
⊢ (𝑀 ∈ 𝐵 → 𝑀 ∈ ((Base‘𝑅) ↑m ((1...𝑁) × (1...𝑁)))) |
17 | 16 | ad2antlr 727 |
. . . . 5
⊢ (((𝑁 ∈ ℕ ∧ 𝑀 ∈ 𝐵) ∧ (𝑖 ∈ ((1...𝑁) ∖ {𝑁}) ∧ 𝑗 ∈ ((1...𝑁) ∖ {𝑁}))) → 𝑀 ∈ ((Base‘𝑅) ↑m ((1...𝑁) × (1...𝑁)))) |
18 | | simprl 771 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ 𝑀 ∈ 𝐵) ∧ (𝑖 ∈ ((1...𝑁) ∖ {𝑁}) ∧ 𝑗 ∈ ((1...𝑁) ∖ {𝑁}))) → 𝑖 ∈ ((1...𝑁) ∖ {𝑁})) |
19 | | nnz 12223 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℤ) |
20 | | fzoval 13268 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℤ →
(1..^𝑁) = (1...(𝑁 − 1))) |
21 | 19, 20 | syl 17 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ →
(1..^𝑁) = (1...(𝑁 − 1))) |
22 | 21, 3 | eqtr4d 2781 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ →
(1..^𝑁) = ((1...𝑁) ∖ {𝑁})) |
23 | 11, 22 | syl 17 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ 𝑀 ∈ 𝐵) ∧ (𝑖 ∈ ((1...𝑁) ∖ {𝑁}) ∧ 𝑗 ∈ ((1...𝑁) ∖ {𝑁}))) → (1..^𝑁) = ((1...𝑁) ∖ {𝑁})) |
24 | 18, 23 | eleqtrrd 2842 |
. . . . 5
⊢ (((𝑁 ∈ ℕ ∧ 𝑀 ∈ 𝐵) ∧ (𝑖 ∈ ((1...𝑁) ∖ {𝑁}) ∧ 𝑗 ∈ ((1...𝑁) ∖ {𝑁}))) → 𝑖 ∈ (1..^𝑁)) |
25 | | simprr 773 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ 𝑀 ∈ 𝐵) ∧ (𝑖 ∈ ((1...𝑁) ∖ {𝑁}) ∧ 𝑗 ∈ ((1...𝑁) ∖ {𝑁}))) → 𝑗 ∈ ((1...𝑁) ∖ {𝑁})) |
26 | 25, 23 | eleqtrrd 2842 |
. . . . 5
⊢ (((𝑁 ∈ ℕ ∧ 𝑀 ∈ 𝐵) ∧ (𝑖 ∈ ((1...𝑁) ∖ {𝑁}) ∧ 𝑗 ∈ ((1...𝑁) ∖ {𝑁}))) → 𝑗 ∈ (1..^𝑁)) |
27 | 6, 11, 11, 12, 12, 17, 24, 26 | smattl 31486 |
. . . 4
⊢ (((𝑁 ∈ ℕ ∧ 𝑀 ∈ 𝐵) ∧ (𝑖 ∈ ((1...𝑁) ∖ {𝑁}) ∧ 𝑗 ∈ ((1...𝑁) ∖ {𝑁}))) → (𝑖(𝑁(subMat1‘𝑀)𝑁)𝑗) = (𝑖𝑀𝑗)) |
28 | 27 | eqcomd 2744 |
. . 3
⊢ (((𝑁 ∈ ℕ ∧ 𝑀 ∈ 𝐵) ∧ (𝑖 ∈ ((1...𝑁) ∖ {𝑁}) ∧ 𝑗 ∈ ((1...𝑁) ∖ {𝑁}))) → (𝑖𝑀𝑗) = (𝑖(𝑁(subMat1‘𝑀)𝑁)𝑗)) |
29 | 4, 5, 28 | mpoeq123dva 7303 |
. 2
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ 𝐵) → (𝑖 ∈ ((1...𝑁) ∖ {𝑁}), 𝑗 ∈ ((1...𝑁) ∖ {𝑁}) ↦ (𝑖𝑀𝑗)) = (𝑖 ∈ (1...(𝑁 − 1)), 𝑗 ∈ (1...(𝑁 − 1)) ↦ (𝑖(𝑁(subMat1‘𝑀)𝑁)𝑗))) |
30 | | simpr 488 |
. . 3
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ 𝐵) → 𝑀 ∈ 𝐵) |
31 | | eqid 2738 |
. . . 4
⊢
((1...𝑁) subMat
𝑅) = ((1...𝑁) subMat 𝑅) |
32 | 13, 31, 15 | submaval 21502 |
. . 3
⊢ ((𝑀 ∈ 𝐵 ∧ 𝑁 ∈ (1...𝑁) ∧ 𝑁 ∈ (1...𝑁)) → (𝑁(((1...𝑁) subMat 𝑅)‘𝑀)𝑁) = (𝑖 ∈ ((1...𝑁) ∖ {𝑁}), 𝑗 ∈ ((1...𝑁) ∖ {𝑁}) ↦ (𝑖𝑀𝑗))) |
33 | 30, 9, 9, 32 | syl3anc 1373 |
. 2
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ 𝐵) → (𝑁(((1...𝑁) subMat 𝑅)‘𝑀)𝑁) = (𝑖 ∈ ((1...𝑁) ∖ {𝑁}), 𝑗 ∈ ((1...𝑁) ∖ {𝑁}) ↦ (𝑖𝑀𝑗))) |
34 | | eqid 2738 |
. . . 4
⊢
(Base‘((1...(𝑁
− 1)) Mat 𝑅)) =
(Base‘((1...(𝑁
− 1)) Mat 𝑅)) |
35 | 13, 15, 34, 6, 10, 9, 9, 30 | smatcl 31490 |
. . 3
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ 𝐵) → (𝑁(subMat1‘𝑀)𝑁) ∈ (Base‘((1...(𝑁 − 1)) Mat 𝑅))) |
36 | | eqid 2738 |
. . . 4
⊢
((1...(𝑁 − 1))
Mat 𝑅) = ((1...(𝑁 − 1)) Mat 𝑅) |
37 | 36, 34 | matmpo 31491 |
. . 3
⊢ ((𝑁(subMat1‘𝑀)𝑁) ∈ (Base‘((1...(𝑁 − 1)) Mat 𝑅)) → (𝑁(subMat1‘𝑀)𝑁) = (𝑖 ∈ (1...(𝑁 − 1)), 𝑗 ∈ (1...(𝑁 − 1)) ↦ (𝑖(𝑁(subMat1‘𝑀)𝑁)𝑗))) |
38 | 35, 37 | syl 17 |
. 2
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ 𝐵) → (𝑁(subMat1‘𝑀)𝑁) = (𝑖 ∈ (1...(𝑁 − 1)), 𝑗 ∈ (1...(𝑁 − 1)) ↦ (𝑖(𝑁(subMat1‘𝑀)𝑁)𝑗))) |
39 | 29, 33, 38 | 3eqtr4rd 2789 |
1
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ 𝐵) → (𝑁(subMat1‘𝑀)𝑁) = (𝑁(((1...𝑁) subMat 𝑅)‘𝑀)𝑁)) |