Step | Hyp | Ref
| Expression |
1 | | dmatval.d |
. 2
⊢ 𝐷 = (𝑁 DMat 𝑅) |
2 | | df-dmat 20115 |
. . . 4
⊢ DMat =
(𝑛 ∈ Fin, 𝑟 ∈ V ↦ {𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ∣ ∀𝑖 ∈ 𝑛 ∀𝑗 ∈ 𝑛 (𝑖 ≠ 𝑗 → (𝑖𝑚𝑗) = (0g‘𝑟))}) |
3 | 2 | a1i 11 |
. . 3
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) → DMat = (𝑛 ∈ Fin, 𝑟 ∈ V ↦ {𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ∣ ∀𝑖 ∈ 𝑛 ∀𝑗 ∈ 𝑛 (𝑖 ≠ 𝑗 → (𝑖𝑚𝑗) = (0g‘𝑟))})) |
4 | | oveq12 6558 |
. . . . . . 7
⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → (𝑛 Mat 𝑟) = (𝑁 Mat 𝑅)) |
5 | 4 | fveq2d 6107 |
. . . . . 6
⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → (Base‘(𝑛 Mat 𝑟)) = (Base‘(𝑁 Mat 𝑅))) |
6 | | dmatval.b |
. . . . . . 7
⊢ 𝐵 = (Base‘𝐴) |
7 | | dmatval.a |
. . . . . . . 8
⊢ 𝐴 = (𝑁 Mat 𝑅) |
8 | 7 | fveq2i 6106 |
. . . . . . 7
⊢
(Base‘𝐴) =
(Base‘(𝑁 Mat 𝑅)) |
9 | 6, 8 | eqtri 2632 |
. . . . . 6
⊢ 𝐵 = (Base‘(𝑁 Mat 𝑅)) |
10 | 5, 9 | syl6eqr 2662 |
. . . . 5
⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → (Base‘(𝑛 Mat 𝑟)) = 𝐵) |
11 | | simpl 472 |
. . . . . 6
⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → 𝑛 = 𝑁) |
12 | | fveq2 6103 |
. . . . . . . . . . 11
⊢ (𝑟 = 𝑅 → (0g‘𝑟) = (0g‘𝑅)) |
13 | | dmatval.0 |
. . . . . . . . . . 11
⊢ 0 =
(0g‘𝑅) |
14 | 12, 13 | syl6eqr 2662 |
. . . . . . . . . 10
⊢ (𝑟 = 𝑅 → (0g‘𝑟) = 0 ) |
15 | 14 | adantl 481 |
. . . . . . . . 9
⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → (0g‘𝑟) = 0 ) |
16 | 15 | eqeq2d 2620 |
. . . . . . . 8
⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → ((𝑖𝑚𝑗) = (0g‘𝑟) ↔ (𝑖𝑚𝑗) = 0 )) |
17 | 16 | imbi2d 329 |
. . . . . . 7
⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → ((𝑖 ≠ 𝑗 → (𝑖𝑚𝑗) = (0g‘𝑟)) ↔ (𝑖 ≠ 𝑗 → (𝑖𝑚𝑗) = 0 ))) |
18 | 11, 17 | raleqbidv 3129 |
. . . . . 6
⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → (∀𝑗 ∈ 𝑛 (𝑖 ≠ 𝑗 → (𝑖𝑚𝑗) = (0g‘𝑟)) ↔ ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑚𝑗) = 0 ))) |
19 | 11, 18 | raleqbidv 3129 |
. . . . 5
⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → (∀𝑖 ∈ 𝑛 ∀𝑗 ∈ 𝑛 (𝑖 ≠ 𝑗 → (𝑖𝑚𝑗) = (0g‘𝑟)) ↔ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑚𝑗) = 0 ))) |
20 | 10, 19 | rabeqbidv 3168 |
. . . 4
⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → {𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ∣ ∀𝑖 ∈ 𝑛 ∀𝑗 ∈ 𝑛 (𝑖 ≠ 𝑗 → (𝑖𝑚𝑗) = (0g‘𝑟))} = {𝑚 ∈ 𝐵 ∣ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑚𝑗) = 0 )}) |
21 | 20 | adantl 481 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) ∧ (𝑛 = 𝑁 ∧ 𝑟 = 𝑅)) → {𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ∣ ∀𝑖 ∈ 𝑛 ∀𝑗 ∈ 𝑛 (𝑖 ≠ 𝑗 → (𝑖𝑚𝑗) = (0g‘𝑟))} = {𝑚 ∈ 𝐵 ∣ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑚𝑗) = 0 )}) |
22 | | simpl 472 |
. . 3
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) → 𝑁 ∈ Fin) |
23 | | elex 3185 |
. . . 4
⊢ (𝑅 ∈ 𝑉 → 𝑅 ∈ V) |
24 | 23 | adantl 481 |
. . 3
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) → 𝑅 ∈ V) |
25 | | fvex 6113 |
. . . . 5
⊢
(Base‘𝐴)
∈ V |
26 | 6, 25 | eqeltri 2684 |
. . . 4
⊢ 𝐵 ∈ V |
27 | | rabexg 4739 |
. . . 4
⊢ (𝐵 ∈ V → {𝑚 ∈ 𝐵 ∣ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑚𝑗) = 0 )} ∈
V) |
28 | 26, 27 | mp1i 13 |
. . 3
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) → {𝑚 ∈ 𝐵 ∣ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑚𝑗) = 0 )} ∈
V) |
29 | 3, 21, 22, 24, 28 | ovmpt2d 6686 |
. 2
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) → (𝑁 DMat 𝑅) = {𝑚 ∈ 𝐵 ∣ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑚𝑗) = 0 )}) |
30 | 1, 29 | syl5eq 2656 |
1
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) → 𝐷 = {𝑚 ∈ 𝐵 ∣ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑚𝑗) = 0 )}) |