Metamath Proof Explorer

Theorem mat0dimcrng

Description: The algebra of matrices with dimension 0 (over an arbitrary ring!) is a commutative ring. (Contributed by AV, 10-Aug-2019)

Ref Expression
Hypothesis mat0dim.a 
|- A = ( (/) Mat R )
Assertion mat0dimcrng 
|- ( R e. Ring -> A e. CRing )

Proof

Step Hyp Ref Expression
1 mat0dim.a 
 |-  A = ( (/) Mat R )
2 0fi 
 |-  (/) e. Fin
3 1 matring 
 |-  ( ( (/) e. Fin /\ R e. Ring ) -> A e. Ring )
4 2 3 mpan 
 |-  ( R e. Ring -> A e. Ring )
5 mat0dimbas0 
 |-  ( R e. Ring -> ( Base ` ( (/) Mat R ) ) = { (/) } )
6 1 eqcomi 
 |-  ( (/) Mat R ) = A
7 6 fveq2i 
 |-  ( Base ` ( (/) Mat R ) ) = ( Base ` A )
8 7 eqeq1i 
 |-  ( ( Base ` ( (/) Mat R ) ) = { (/) } <-> ( Base ` A ) = { (/) } )
9 eqidd 
 |-  ( ( ( Base ` A ) = { (/) } /\ R e. Ring ) -> ( (/) ( .r ` A ) (/) ) = ( (/) ( .r ` A ) (/) ) )
10 0ex 
 |-  (/) e. _V
11 oveq1 
 |-  ( x = (/) -> ( x ( .r ` A ) y ) = ( (/) ( .r ` A ) y ) )
12 oveq2 
 |-  ( x = (/) -> ( y ( .r ` A ) x ) = ( y ( .r ` A ) (/) ) )
13 11 12 eqeq12d 
 |-  ( x = (/) -> ( ( x ( .r ` A ) y ) = ( y ( .r ` A ) x ) <-> ( (/) ( .r ` A ) y ) = ( y ( .r ` A ) (/) ) ) )
14 13 ralbidv 
 |-  ( x = (/) -> ( A. y e. { (/) } ( x ( .r ` A ) y ) = ( y ( .r ` A ) x ) <-> A. y e. { (/) } ( (/) ( .r ` A ) y ) = ( y ( .r ` A ) (/) ) ) )
15 10 14 ralsn 
 |-  ( A. x e. { (/) } A. y e. { (/) } ( x ( .r ` A ) y ) = ( y ( .r ` A ) x ) <-> A. y e. { (/) } ( (/) ( .r ` A ) y ) = ( y ( .r ` A ) (/) ) )
16 oveq2 
 |-  ( y = (/) -> ( (/) ( .r ` A ) y ) = ( (/) ( .r ` A ) (/) ) )
17 oveq1 
 |-  ( y = (/) -> ( y ( .r ` A ) (/) ) = ( (/) ( .r ` A ) (/) ) )
18 16 17 eqeq12d 
 |-  ( y = (/) -> ( ( (/) ( .r ` A ) y ) = ( y ( .r ` A ) (/) ) <-> ( (/) ( .r ` A ) (/) ) = ( (/) ( .r ` A ) (/) ) ) )
19 10 18 ralsn 
 |-  ( A. y e. { (/) } ( (/) ( .r ` A ) y ) = ( y ( .r ` A ) (/) ) <-> ( (/) ( .r ` A ) (/) ) = ( (/) ( .r ` A ) (/) ) )
20 15 19 bitri 
 |-  ( A. x e. { (/) } A. y e. { (/) } ( x ( .r ` A ) y ) = ( y ( .r ` A ) x ) <-> ( (/) ( .r ` A ) (/) ) = ( (/) ( .r ` A ) (/) ) )
21 9 20 sylibr 
 |-  ( ( ( Base ` A ) = { (/) } /\ R e. Ring ) -> A. x e. { (/) } A. y e. { (/) } ( x ( .r ` A ) y ) = ( y ( .r ` A ) x ) )
22 raleq 
 |-  ( ( Base ` A ) = { (/) } -> ( A. y e. ( Base ` A ) ( x ( .r ` A ) y ) = ( y ( .r ` A ) x ) <-> A. y e. { (/) } ( x ( .r ` A ) y ) = ( y ( .r ` A ) x ) ) )
23 22 raleqbi1dv 
 |-  ( ( Base ` A ) = { (/) } -> ( A. x e. ( Base ` A ) A. y e. ( Base ` A ) ( x ( .r ` A ) y ) = ( y ( .r ` A ) x ) <-> A. x e. { (/) } A. y e. { (/) } ( x ( .r ` A ) y ) = ( y ( .r ` A ) x ) ) )
24 23 adantr 
 |-  ( ( ( Base ` A ) = { (/) } /\ R e. Ring ) -> ( A. x e. ( Base ` A ) A. y e. ( Base ` A ) ( x ( .r ` A ) y ) = ( y ( .r ` A ) x ) <-> A. x e. { (/) } A. y e. { (/) } ( x ( .r ` A ) y ) = ( y ( .r ` A ) x ) ) )
25 21 24 mpbird 
 |-  ( ( ( Base ` A ) = { (/) } /\ R e. Ring ) -> A. x e. ( Base ` A ) A. y e. ( Base ` A ) ( x ( .r ` A ) y ) = ( y ( .r ` A ) x ) )
26 25 ex 
 |-  ( ( Base ` A ) = { (/) } -> ( R e. Ring -> A. x e. ( Base ` A ) A. y e. ( Base ` A ) ( x ( .r ` A ) y ) = ( y ( .r ` A ) x ) ) )
27 8 26 sylbi 
 |-  ( ( Base ` ( (/) Mat R ) ) = { (/) } -> ( R e. Ring -> A. x e. ( Base ` A ) A. y e. ( Base ` A ) ( x ( .r ` A ) y ) = ( y ( .r ` A ) x ) ) )
28 5 27 mpcom 
 |-  ( R e. Ring -> A. x e. ( Base ` A ) A. y e. ( Base ` A ) ( x ( .r ` A ) y ) = ( y ( .r ` A ) x ) )
29 eqid 
 |-  ( Base ` A ) = ( Base ` A )
30 eqid 
 |-  ( .r ` A ) = ( .r ` A )
31 29 30 iscrng2 
 |-  ( A e. CRing <-> ( A e. Ring /\ A. x e. ( Base ` A ) A. y e. ( Base ` A ) ( x ( .r ` A ) y ) = ( y ( .r ` A ) x ) ) )
32 4 28 31 sylanbrc 
 |-  ( R e. Ring -> A e. CRing )