Step | Hyp | Ref
| Expression |
1 | | simprl 790 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐶 ∈ 𝐾 ∧ 𝑀 ∈ 𝐷)) → 𝐶 ∈ 𝐾) |
2 | | dmatscmcl.a |
. . . . . . . 8
⊢ 𝐴 = (𝑁 Mat 𝑅) |
3 | | dmatscmcl.b |
. . . . . . . 8
⊢ 𝐵 = (Base‘𝐴) |
4 | | eqid 2610 |
. . . . . . . 8
⊢
(0g‘𝑅) = (0g‘𝑅) |
5 | | dmatscmcl.d |
. . . . . . . 8
⊢ 𝐷 = (𝑁 DMat 𝑅) |
6 | 2, 3, 4, 5 | dmatmat 20119 |
. . . . . . 7
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝑀 ∈ 𝐷 → 𝑀 ∈ 𝐵)) |
7 | 6 | com12 32 |
. . . . . 6
⊢ (𝑀 ∈ 𝐷 → ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑀 ∈ 𝐵)) |
8 | 7 | adantl 481 |
. . . . 5
⊢ ((𝐶 ∈ 𝐾 ∧ 𝑀 ∈ 𝐷) → ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑀 ∈ 𝐵)) |
9 | 8 | impcom 445 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐶 ∈ 𝐾 ∧ 𝑀 ∈ 𝐷)) → 𝑀 ∈ 𝐵) |
10 | 1, 9 | jca 553 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐶 ∈ 𝐾 ∧ 𝑀 ∈ 𝐷)) → (𝐶 ∈ 𝐾 ∧ 𝑀 ∈ 𝐵)) |
11 | | dmatscmcl.k |
. . . 4
⊢ 𝐾 = (Base‘𝑅) |
12 | | dmatscmcl.s |
. . . 4
⊢ ∗ = (
·𝑠 ‘𝐴) |
13 | 11, 2, 3, 12 | matvscl 20056 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐶 ∈ 𝐾 ∧ 𝑀 ∈ 𝐵)) → (𝐶 ∗ 𝑀) ∈ 𝐵) |
14 | 10, 13 | syldan 486 |
. 2
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐶 ∈ 𝐾 ∧ 𝑀 ∈ 𝐷)) → (𝐶 ∗ 𝑀) ∈ 𝐵) |
15 | 2, 3, 4, 5 | dmatel 20118 |
. . . . 5
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝑀 ∈ 𝐷 ↔ (𝑀 ∈ 𝐵 ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = (0g‘𝑅))))) |
16 | 15 | adantr 480 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐶 ∈ 𝐾) → (𝑀 ∈ 𝐷 ↔ (𝑀 ∈ 𝐵 ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = (0g‘𝑅))))) |
17 | | simp-4r 803 |
. . . . . . . . . . . 12
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝐾) ∧ 𝑀 ∈ 𝐵) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → 𝑅 ∈ Ring) |
18 | | simpr 476 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐶 ∈ 𝐾) → 𝐶 ∈ 𝐾) |
19 | 18 | anim1i 590 |
. . . . . . . . . . . . 13
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐶 ∈ 𝐾) ∧ 𝑀 ∈ 𝐵) → (𝐶 ∈ 𝐾 ∧ 𝑀 ∈ 𝐵)) |
20 | 19 | adantr 480 |
. . . . . . . . . . . 12
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝐾) ∧ 𝑀 ∈ 𝐵) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (𝐶 ∈ 𝐾 ∧ 𝑀 ∈ 𝐵)) |
21 | | simpr 476 |
. . . . . . . . . . . 12
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝐾) ∧ 𝑀 ∈ 𝐵) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) |
22 | 17, 20, 21 | 3jca 1235 |
. . . . . . . . . . 11
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝐾) ∧ 𝑀 ∈ 𝐵) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (𝑅 ∈ Ring ∧ (𝐶 ∈ 𝐾 ∧ 𝑀 ∈ 𝐵) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁))) |
23 | 22 | adantr 480 |
. . . . . . . . . 10
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝐾) ∧ 𝑀 ∈ 𝐵) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ (𝑖𝑀𝑗) = (0g‘𝑅)) → (𝑅 ∈ Ring ∧ (𝐶 ∈ 𝐾 ∧ 𝑀 ∈ 𝐵) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁))) |
24 | | eqid 2610 |
. . . . . . . . . . 11
⊢
(.r‘𝑅) = (.r‘𝑅) |
25 | 2, 3, 11, 12, 24 | matvscacell 20061 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Ring ∧ (𝐶 ∈ 𝐾 ∧ 𝑀 ∈ 𝐵) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (𝑖(𝐶 ∗ 𝑀)𝑗) = (𝐶(.r‘𝑅)(𝑖𝑀𝑗))) |
26 | 23, 25 | syl 17 |
. . . . . . . . 9
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝐾) ∧ 𝑀 ∈ 𝐵) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ (𝑖𝑀𝑗) = (0g‘𝑅)) → (𝑖(𝐶 ∗ 𝑀)𝑗) = (𝐶(.r‘𝑅)(𝑖𝑀𝑗))) |
27 | | oveq2 6557 |
. . . . . . . . . 10
⊢ ((𝑖𝑀𝑗) = (0g‘𝑅) → (𝐶(.r‘𝑅)(𝑖𝑀𝑗)) = (𝐶(.r‘𝑅)(0g‘𝑅))) |
28 | 27 | adantl 481 |
. . . . . . . . 9
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝐾) ∧ 𝑀 ∈ 𝐵) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ (𝑖𝑀𝑗) = (0g‘𝑅)) → (𝐶(.r‘𝑅)(𝑖𝑀𝑗)) = (𝐶(.r‘𝑅)(0g‘𝑅))) |
29 | | simpr 476 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑅 ∈ Ring) |
30 | 29 | anim1i 590 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐶 ∈ 𝐾) → (𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾)) |
31 | 30 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐶 ∈ 𝐾) ∧ 𝑀 ∈ 𝐵) → (𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾)) |
32 | 11, 24, 4 | ringrz 18411 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾) → (𝐶(.r‘𝑅)(0g‘𝑅)) = (0g‘𝑅)) |
33 | 31, 32 | syl 17 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐶 ∈ 𝐾) ∧ 𝑀 ∈ 𝐵) → (𝐶(.r‘𝑅)(0g‘𝑅)) = (0g‘𝑅)) |
34 | 33 | adantr 480 |
. . . . . . . . . 10
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝐾) ∧ 𝑀 ∈ 𝐵) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (𝐶(.r‘𝑅)(0g‘𝑅)) = (0g‘𝑅)) |
35 | 34 | adantr 480 |
. . . . . . . . 9
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝐾) ∧ 𝑀 ∈ 𝐵) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ (𝑖𝑀𝑗) = (0g‘𝑅)) → (𝐶(.r‘𝑅)(0g‘𝑅)) = (0g‘𝑅)) |
36 | 26, 28, 35 | 3eqtrd 2648 |
. . . . . . . 8
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝐾) ∧ 𝑀 ∈ 𝐵) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ (𝑖𝑀𝑗) = (0g‘𝑅)) → (𝑖(𝐶 ∗ 𝑀)𝑗) = (0g‘𝑅)) |
37 | 36 | ex 449 |
. . . . . . 7
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝐾) ∧ 𝑀 ∈ 𝐵) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → ((𝑖𝑀𝑗) = (0g‘𝑅) → (𝑖(𝐶 ∗ 𝑀)𝑗) = (0g‘𝑅))) |
38 | 37 | imim2d 55 |
. . . . . 6
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝐶 ∈ 𝐾) ∧ 𝑀 ∈ 𝐵) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → ((𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = (0g‘𝑅)) → (𝑖 ≠ 𝑗 → (𝑖(𝐶 ∗ 𝑀)𝑗) = (0g‘𝑅)))) |
39 | 38 | ralimdvva 2947 |
. . . . 5
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐶 ∈ 𝐾) ∧ 𝑀 ∈ 𝐵) → (∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = (0g‘𝑅)) → ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖(𝐶 ∗ 𝑀)𝑗) = (0g‘𝑅)))) |
40 | 39 | expimpd 627 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐶 ∈ 𝐾) → ((𝑀 ∈ 𝐵 ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = (0g‘𝑅))) → ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖(𝐶 ∗ 𝑀)𝑗) = (0g‘𝑅)))) |
41 | 16, 40 | sylbid 229 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐶 ∈ 𝐾) → (𝑀 ∈ 𝐷 → ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖(𝐶 ∗ 𝑀)𝑗) = (0g‘𝑅)))) |
42 | 41 | impr 647 |
. 2
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐶 ∈ 𝐾 ∧ 𝑀 ∈ 𝐷)) → ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖(𝐶 ∗ 𝑀)𝑗) = (0g‘𝑅))) |
43 | 2, 3, 4, 5 | dmatel 20118 |
. . 3
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → ((𝐶 ∗ 𝑀) ∈ 𝐷 ↔ ((𝐶 ∗ 𝑀) ∈ 𝐵 ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖(𝐶 ∗ 𝑀)𝑗) = (0g‘𝑅))))) |
44 | 43 | adantr 480 |
. 2
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐶 ∈ 𝐾 ∧ 𝑀 ∈ 𝐷)) → ((𝐶 ∗ 𝑀) ∈ 𝐷 ↔ ((𝐶 ∗ 𝑀) ∈ 𝐵 ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖(𝐶 ∗ 𝑀)𝑗) = (0g‘𝑅))))) |
45 | 14, 42, 44 | mpbir2and 959 |
1
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐶 ∈ 𝐾 ∧ 𝑀 ∈ 𝐷)) → (𝐶 ∗ 𝑀) ∈ 𝐷) |