Metamath Proof Explorer

Theorem mat1dimcrng

Description: The algebra of matrices with dimension 1 over a commutative ring is a commutative ring. (Contributed by AV, 16-Aug-2019)

Ref Expression
Hypotheses mat1dim.a 
|- A = ( { E } Mat R )
mat1dim.b 
|- B = ( Base ` R )
mat1dim.o 
|- O = <. E , E >.
Assertion mat1dimcrng 
|- ( ( R e. CRing /\ E e. V ) -> A e. CRing )

Proof

Step Hyp Ref Expression
1 mat1dim.a 
 |-  A = ( { E } Mat R )
2 mat1dim.b 
 |-  B = ( Base ` R )
3 mat1dim.o 
 |-  O = <. E , E >.
4 snfi 
 |-  { E } e. Fin
5 crngring 
 |-  ( R e. CRing -> R e. Ring )
6 5 adantr 
 |-  ( ( R e. CRing /\ E e. V ) -> R e. Ring )
7 1 matring 
 |-  ( ( { E } e. Fin /\ R e. Ring ) -> A e. Ring )
8 4 6 7 sylancr 
 |-  ( ( R e. CRing /\ E e. V ) -> A e. Ring )
9 1 2 3 mat1dimelbas 
 |-  ( ( R e. Ring /\ E e. V ) -> ( x e. ( Base ` A ) <-> E. a e. B x = { <. O , a >. } ) )
10 1 2 3 mat1dimelbas 
 |-  ( ( R e. Ring /\ E e. V ) -> ( y e. ( Base ` A ) <-> E. b e. B y = { <. O , b >. } ) )
11 9 10 anbi12d 
 |-  ( ( R e. Ring /\ E e. V ) -> ( ( x e. ( Base ` A ) /\ y e. ( Base ` A ) ) <-> ( E. a e. B x = { <. O , a >. } /\ E. b e. B y = { <. O , b >. } ) ) )
12 5 11 sylan 
 |-  ( ( R e. CRing /\ E e. V ) -> ( ( x e. ( Base ` A ) /\ y e. ( Base ` A ) ) <-> ( E. a e. B x = { <. O , a >. } /\ E. b e. B y = { <. O , b >. } ) ) )
13 simpll 
 |-  ( ( ( R e. CRing /\ E e. V ) /\ ( a e. B /\ b e. B ) ) -> R e. CRing )
14 simprl 
 |-  ( ( ( R e. CRing /\ E e. V ) /\ ( a e. B /\ b e. B ) ) -> a e. B )
15 simprr 
 |-  ( ( ( R e. CRing /\ E e. V ) /\ ( a e. B /\ b e. B ) ) -> b e. B )
16 eqid 
 |-  ( .r ` R ) = ( .r ` R )
17 2 16 crngcom 
 |-  ( ( R e. CRing /\ a e. B /\ b e. B ) -> ( a ( .r ` R ) b ) = ( b ( .r ` R ) a ) )
18 13 14 15 17 syl3anc 
 |-  ( ( ( R e. CRing /\ E e. V ) /\ ( a e. B /\ b e. B ) ) -> ( a ( .r ` R ) b ) = ( b ( .r ` R ) a ) )
19 18 opeq2d 
 |-  ( ( ( R e. CRing /\ E e. V ) /\ ( a e. B /\ b e. B ) ) -> <. O , ( a ( .r ` R ) b ) >. = <. O , ( b ( .r ` R ) a ) >. )
20 19 sneqd 
 |-  ( ( ( R e. CRing /\ E e. V ) /\ ( a e. B /\ b e. B ) ) -> { <. O , ( a ( .r ` R ) b ) >. } = { <. O , ( b ( .r ` R ) a ) >. } )
21 5 anim1i 
 |-  ( ( R e. CRing /\ E e. V ) -> ( R e. Ring /\ E e. V ) )
22 1 2 3 mat1dimmul 
 |-  ( ( ( R e. Ring /\ E e. V ) /\ ( a e. B /\ b e. B ) ) -> ( { <. O , a >. } ( .r ` A ) { <. O , b >. } ) = { <. O , ( a ( .r ` R ) b ) >. } )
23 21 22 sylan 
 |-  ( ( ( R e. CRing /\ E e. V ) /\ ( a e. B /\ b e. B ) ) -> ( { <. O , a >. } ( .r ` A ) { <. O , b >. } ) = { <. O , ( a ( .r ` R ) b ) >. } )
24 pm3.22 
 |-  ( ( a e. B /\ b e. B ) -> ( b e. B /\ a e. B ) )
25 1 2 3 mat1dimmul 
 |-  ( ( ( R e. Ring /\ E e. V ) /\ ( b e. B /\ a e. B ) ) -> ( { <. O , b >. } ( .r ` A ) { <. O , a >. } ) = { <. O , ( b ( .r ` R ) a ) >. } )
26 21 24 25 syl2an 
 |-  ( ( ( R e. CRing /\ E e. V ) /\ ( a e. B /\ b e. B ) ) -> ( { <. O , b >. } ( .r ` A ) { <. O , a >. } ) = { <. O , ( b ( .r ` R ) a ) >. } )
27 20 23 26 3eqtr4d 
 |-  ( ( ( R e. CRing /\ E e. V ) /\ ( a e. B /\ b e. B ) ) -> ( { <. O , a >. } ( .r ` A ) { <. O , b >. } ) = ( { <. O , b >. } ( .r ` A ) { <. O , a >. } ) )
28 27 expr 
 |-  ( ( ( R e. CRing /\ E e. V ) /\ a e. B ) -> ( b e. B -> ( { <. O , a >. } ( .r ` A ) { <. O , b >. } ) = ( { <. O , b >. } ( .r ` A ) { <. O , a >. } ) ) )
29 28 adantr 
 |-  ( ( ( ( R e. CRing /\ E e. V ) /\ a e. B ) /\ x = { <. O , a >. } ) -> ( b e. B -> ( { <. O , a >. } ( .r ` A ) { <. O , b >. } ) = ( { <. O , b >. } ( .r ` A ) { <. O , a >. } ) ) )
30 29 imp 
 |-  ( ( ( ( ( R e. CRing /\ E e. V ) /\ a e. B ) /\ x = { <. O , a >. } ) /\ b e. B ) -> ( { <. O , a >. } ( .r ` A ) { <. O , b >. } ) = ( { <. O , b >. } ( .r ` A ) { <. O , a >. } ) )
31 30 adantr 
 |-  ( ( ( ( ( ( R e. CRing /\ E e. V ) /\ a e. B ) /\ x = { <. O , a >. } ) /\ b e. B ) /\ y = { <. O , b >. } ) -> ( { <. O , a >. } ( .r ` A ) { <. O , b >. } ) = ( { <. O , b >. } ( .r ` A ) { <. O , a >. } ) )
32 oveq12 
 |-  ( ( x = { <. O , a >. } /\ y = { <. O , b >. } ) -> ( x ( .r ` A ) y ) = ( { <. O , a >. } ( .r ` A ) { <. O , b >. } ) )
33 32 ad4ant24 
 |-  ( ( ( ( ( ( R e. CRing /\ E e. V ) /\ a e. B ) /\ x = { <. O , a >. } ) /\ b e. B ) /\ y = { <. O , b >. } ) -> ( x ( .r ` A ) y ) = ( { <. O , a >. } ( .r ` A ) { <. O , b >. } ) )
34 oveq12 
 |-  ( ( y = { <. O , b >. } /\ x = { <. O , a >. } ) -> ( y ( .r ` A ) x ) = ( { <. O , b >. } ( .r ` A ) { <. O , a >. } ) )
35 34 expcom 
 |-  ( x = { <. O , a >. } -> ( y = { <. O , b >. } -> ( y ( .r ` A ) x ) = ( { <. O , b >. } ( .r ` A ) { <. O , a >. } ) ) )
36 35 ad2antlr 
 |-  ( ( ( ( ( R e. CRing /\ E e. V ) /\ a e. B ) /\ x = { <. O , a >. } ) /\ b e. B ) -> ( y = { <. O , b >. } -> ( y ( .r ` A ) x ) = ( { <. O , b >. } ( .r ` A ) { <. O , a >. } ) ) )
37 36 imp 
 |-  ( ( ( ( ( ( R e. CRing /\ E e. V ) /\ a e. B ) /\ x = { <. O , a >. } ) /\ b e. B ) /\ y = { <. O , b >. } ) -> ( y ( .r ` A ) x ) = ( { <. O , b >. } ( .r ` A ) { <. O , a >. } ) )
38 31 33 37 3eqtr4d 
 |-  ( ( ( ( ( ( R e. CRing /\ E e. V ) /\ a e. B ) /\ x = { <. O , a >. } ) /\ b e. B ) /\ y = { <. O , b >. } ) -> ( x ( .r ` A ) y ) = ( y ( .r ` A ) x ) )
39 38 rexlimdva2 
 |-  ( ( ( ( R e. CRing /\ E e. V ) /\ a e. B ) /\ x = { <. O , a >. } ) -> ( E. b e. B y = { <. O , b >. } -> ( x ( .r ` A ) y ) = ( y ( .r ` A ) x ) ) )
40 39 rexlimdva2 
 |-  ( ( R e. CRing /\ E e. V ) -> ( E. a e. B x = { <. O , a >. } -> ( E. b e. B y = { <. O , b >. } -> ( x ( .r ` A ) y ) = ( y ( .r ` A ) x ) ) ) )
41 40 impd 
 |-  ( ( R e. CRing /\ E e. V ) -> ( ( E. a e. B x = { <. O , a >. } /\ E. b e. B y = { <. O , b >. } ) -> ( x ( .r ` A ) y ) = ( y ( .r ` A ) x ) ) )
42 12 41 sylbid 
 |-  ( ( R e. CRing /\ E e. V ) -> ( ( x e. ( Base ` A ) /\ y e. ( Base ` A ) ) -> ( x ( .r ` A ) y ) = ( y ( .r ` A ) x ) ) )
43 42 ralrimivv 
 |-  ( ( R e. CRing /\ E e. V ) -> A. x e. ( Base ` A ) A. y e. ( Base ` A ) ( x ( .r ` A ) y ) = ( y ( .r ` A ) x ) )
44 eqid 
 |-  ( Base ` A ) = ( Base ` A )
45 eqid 
 |-  ( .r ` A ) = ( .r ` A )
46 44 45 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 ) ) )
47 8 43 46 sylanbrc 
 |-  ( ( R e. CRing /\ E e. V ) -> A e. CRing )