| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | dmatid.a | . . . . 5
⊢ 𝐴 = (𝑁 Mat 𝑅) | 
| 2 | 1 | matgrp 22436 | . . . 4
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐴 ∈ Grp) | 
| 3 | 2 | adantr 480 | . . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷)) → 𝐴 ∈ Grp) | 
| 4 |  | dmatid.b | . . . . . 6
⊢ 𝐵 = (Base‘𝐴) | 
| 5 |  | dmatid.0 | . . . . . 6
⊢  0 =
(0g‘𝑅) | 
| 6 |  | dmatid.d | . . . . . 6
⊢ 𝐷 = (𝑁 DMat 𝑅) | 
| 7 | 1, 4, 5, 6 | dmatmat 22500 | . . . . 5
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝑋 ∈ 𝐷 → 𝑋 ∈ 𝐵)) | 
| 8 | 7 | imp 406 | . . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑋 ∈ 𝐷) → 𝑋 ∈ 𝐵) | 
| 9 | 8 | adantrr 717 | . . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷)) → 𝑋 ∈ 𝐵) | 
| 10 | 1, 4, 5, 6 | dmatmat 22500 | . . . . 5
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝑌 ∈ 𝐷 → 𝑌 ∈ 𝐵)) | 
| 11 | 10 | imp 406 | . . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑌 ∈ 𝐷) → 𝑌 ∈ 𝐵) | 
| 12 | 11 | adantrl 716 | . . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷)) → 𝑌 ∈ 𝐵) | 
| 13 |  | eqid 2737 | . . . 4
⊢
(-g‘𝐴) = (-g‘𝐴) | 
| 14 | 4, 13 | grpsubcl 19038 | . . 3
⊢ ((𝐴 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋(-g‘𝐴)𝑌) ∈ 𝐵) | 
| 15 | 3, 9, 12, 14 | syl3anc 1373 | . 2
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷)) → (𝑋(-g‘𝐴)𝑌) ∈ 𝐵) | 
| 16 |  | simpr 484 | . . . . . . . . 9
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑅 ∈ Ring) | 
| 17 | 16 | adantr 480 | . . . . . . . 8
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷)) → 𝑅 ∈ Ring) | 
| 18 | 17 | adantr 480 | . . . . . . 7
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷)) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → 𝑅 ∈ Ring) | 
| 19 | 7, 10 | anim12d 609 | . . . . . . . . 9
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → ((𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷) → (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵))) | 
| 20 | 19 | imp 406 | . . . . . . . 8
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷)) → (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) | 
| 21 | 20 | adantr 480 | . . . . . . 7
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷)) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) | 
| 22 |  | simpr 484 | . . . . . . 7
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷)) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) | 
| 23 |  | eqid 2737 | . . . . . . . 8
⊢
(-g‘𝑅) = (-g‘𝑅) | 
| 24 | 1, 4, 13, 23 | matsubgcell 22440 | . . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (𝑖(𝑋(-g‘𝐴)𝑌)𝑗) = ((𝑖𝑋𝑗)(-g‘𝑅)(𝑖𝑌𝑗))) | 
| 25 | 18, 21, 22, 24 | syl3anc 1373 | . . . . . 6
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷)) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (𝑖(𝑋(-g‘𝐴)𝑌)𝑗) = ((𝑖𝑋𝑗)(-g‘𝑅)(𝑖𝑌𝑗))) | 
| 26 | 25 | adantr 480 | . . . . 5
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷)) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑖 ≠ 𝑗) → (𝑖(𝑋(-g‘𝐴)𝑌)𝑗) = ((𝑖𝑋𝑗)(-g‘𝑅)(𝑖𝑌𝑗))) | 
| 27 |  | simpll 767 | . . . . . . . . . 10
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷)) → 𝑁 ∈ Fin) | 
| 28 |  | simprl 771 | . . . . . . . . . 10
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷)) → 𝑋 ∈ 𝐷) | 
| 29 | 27, 17, 28 | 3jca 1129 | . . . . . . . . 9
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷)) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐷)) | 
| 30 | 29 | adantr 480 | . . . . . . . 8
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷)) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐷)) | 
| 31 | 30 | adantr 480 | . . . . . . 7
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷)) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑖 ≠ 𝑗) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐷)) | 
| 32 |  | simplrl 777 | . . . . . . 7
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷)) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑖 ≠ 𝑗) → 𝑖 ∈ 𝑁) | 
| 33 |  | simplrr 778 | . . . . . . 7
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷)) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑖 ≠ 𝑗) → 𝑗 ∈ 𝑁) | 
| 34 |  | simpr 484 | . . . . . . 7
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷)) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑖 ≠ 𝑗) → 𝑖 ≠ 𝑗) | 
| 35 | 1, 4, 5, 6 | dmatelnd 22502 | . . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐷) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ∧ 𝑖 ≠ 𝑗)) → (𝑖𝑋𝑗) = 0 ) | 
| 36 | 31, 32, 33, 34, 35 | syl13anc 1374 | . . . . . 6
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷)) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑖 ≠ 𝑗) → (𝑖𝑋𝑗) = 0 ) | 
| 37 |  | simprr 773 | . . . . . . . . . 10
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷)) → 𝑌 ∈ 𝐷) | 
| 38 | 27, 17, 37 | 3jca 1129 | . . . . . . . . 9
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷)) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑌 ∈ 𝐷)) | 
| 39 | 38 | adantr 480 | . . . . . . . 8
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷)) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑌 ∈ 𝐷)) | 
| 40 | 39 | adantr 480 | . . . . . . 7
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷)) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑖 ≠ 𝑗) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑌 ∈ 𝐷)) | 
| 41 | 1, 4, 5, 6 | dmatelnd 22502 | . . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑌 ∈ 𝐷) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ∧ 𝑖 ≠ 𝑗)) → (𝑖𝑌𝑗) = 0 ) | 
| 42 | 40, 32, 33, 34, 41 | syl13anc 1374 | . . . . . 6
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷)) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑖 ≠ 𝑗) → (𝑖𝑌𝑗) = 0 ) | 
| 43 | 36, 42 | oveq12d 7449 | . . . . 5
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷)) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑖 ≠ 𝑗) → ((𝑖𝑋𝑗)(-g‘𝑅)(𝑖𝑌𝑗)) = ( 0 (-g‘𝑅) 0 )) | 
| 44 |  | ringgrp 20235 | . . . . . . . . 9
⊢ (𝑅 ∈ Ring → 𝑅 ∈ Grp) | 
| 45 |  | eqid 2737 | . . . . . . . . . 10
⊢
(Base‘𝑅) =
(Base‘𝑅) | 
| 46 | 45, 5 | ring0cl 20264 | . . . . . . . . 9
⊢ (𝑅 ∈ Ring → 0 ∈
(Base‘𝑅)) | 
| 47 | 44, 46 | jca 511 | . . . . . . . 8
⊢ (𝑅 ∈ Ring → (𝑅 ∈ Grp ∧ 0 ∈
(Base‘𝑅))) | 
| 48 | 47 | adantl 481 | . . . . . . 7
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝑅 ∈ Grp ∧ 0 ∈
(Base‘𝑅))) | 
| 49 | 45, 5, 23 | grpsubid 19042 | . . . . . . 7
⊢ ((𝑅 ∈ Grp ∧ 0 ∈
(Base‘𝑅)) → (
0
(-g‘𝑅)
0 ) =
0
) | 
| 50 | 48, 49 | syl 17 | . . . . . 6
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → ( 0
(-g‘𝑅)
0 ) =
0
) | 
| 51 | 50 | ad3antrrr 730 | . . . . 5
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷)) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑖 ≠ 𝑗) → ( 0 (-g‘𝑅) 0 ) = 0 ) | 
| 52 | 26, 43, 51 | 3eqtrd 2781 | . . . 4
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷)) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑖 ≠ 𝑗) → (𝑖(𝑋(-g‘𝐴)𝑌)𝑗) = 0 ) | 
| 53 | 52 | ex 412 | . . 3
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷)) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (𝑖 ≠ 𝑗 → (𝑖(𝑋(-g‘𝐴)𝑌)𝑗) = 0 )) | 
| 54 | 53 | ralrimivva 3202 | . 2
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷)) → ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖(𝑋(-g‘𝐴)𝑌)𝑗) = 0 )) | 
| 55 | 1, 4, 5, 6 | dmatel 22499 | . . 3
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → ((𝑋(-g‘𝐴)𝑌) ∈ 𝐷 ↔ ((𝑋(-g‘𝐴)𝑌) ∈ 𝐵 ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖(𝑋(-g‘𝐴)𝑌)𝑗) = 0 )))) | 
| 56 | 55 | adantr 480 | . 2
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷)) → ((𝑋(-g‘𝐴)𝑌) ∈ 𝐷 ↔ ((𝑋(-g‘𝐴)𝑌) ∈ 𝐵 ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖(𝑋(-g‘𝐴)𝑌)𝑗) = 0 )))) | 
| 57 | 15, 54, 56 | mpbir2and 713 | 1
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷)) → (𝑋(-g‘𝐴)𝑌) ∈ 𝐷) |