Step |
Hyp |
Ref |
Expression |
1 |
|
dmatid.a |
|- A = ( N Mat R ) |
2 |
|
dmatid.b |
|- B = ( Base ` A ) |
3 |
|
dmatid.0 |
|- .0. = ( 0g ` R ) |
4 |
|
dmatid.d |
|- D = ( N DMat R ) |
5 |
1 2 3 4
|
dmatsgrp |
|- ( ( R e. Ring /\ N e. Fin ) -> D e. ( SubGrp ` A ) ) |
6 |
1 2 3 4
|
dmatid |
|- ( ( N e. Fin /\ R e. Ring ) -> ( 1r ` A ) e. D ) |
7 |
6
|
ancoms |
|- ( ( R e. Ring /\ N e. Fin ) -> ( 1r ` A ) e. D ) |
8 |
1 2 3 4
|
dmatmulcl |
|- ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. D /\ y e. D ) ) -> ( x ( .r ` A ) y ) e. D ) |
9 |
8
|
ralrimivva |
|- ( ( N e. Fin /\ R e. Ring ) -> A. x e. D A. y e. D ( x ( .r ` A ) y ) e. D ) |
10 |
9
|
ancoms |
|- ( ( R e. Ring /\ N e. Fin ) -> A. x e. D A. y e. D ( x ( .r ` A ) y ) e. D ) |
11 |
1
|
matring |
|- ( ( N e. Fin /\ R e. Ring ) -> A e. Ring ) |
12 |
11
|
ancoms |
|- ( ( R e. Ring /\ N e. Fin ) -> A e. Ring ) |
13 |
|
eqid |
|- ( 1r ` A ) = ( 1r ` A ) |
14 |
|
eqid |
|- ( .r ` A ) = ( .r ` A ) |
15 |
2 13 14
|
issubrg2 |
|- ( A e. Ring -> ( D e. ( SubRing ` A ) <-> ( D e. ( SubGrp ` A ) /\ ( 1r ` A ) e. D /\ A. x e. D A. y e. D ( x ( .r ` A ) y ) e. D ) ) ) |
16 |
12 15
|
syl |
|- ( ( R e. Ring /\ N e. Fin ) -> ( D e. ( SubRing ` A ) <-> ( D e. ( SubGrp ` A ) /\ ( 1r ` A ) e. D /\ A. x e. D A. y e. D ( x ( .r ` A ) y ) e. D ) ) ) |
17 |
5 7 10 16
|
mpbir3and |
|- ( ( R e. Ring /\ N e. Fin ) -> D e. ( SubRing ` A ) ) |