Metamath Proof Explorer

Theorem mat1ghm

Description: There is a group homomorphism from the additive group of a ring to the additive group of the ring of matrices with dimension 1 over this ring. (Contributed by AV, 22-Dec-2019)

Ref Expression
Hypotheses mat1rhmval.k 
|- K = ( Base ` R )
mat1rhmval.a 
|- A = ( { E } Mat R )
mat1rhmval.b 
|- B = ( Base ` A )
mat1rhmval.o 
|- O = <. E , E >.
mat1rhmval.f 
|- F = ( x e. K |-> { <. O , x >. } )
Assertion mat1ghm 
|- ( ( R e. Ring /\ E e. V ) -> F e. ( R GrpHom A ) )

Proof

Step Hyp Ref Expression
1 mat1rhmval.k 
 |-  K = ( Base ` R )
2 mat1rhmval.a 
 |-  A = ( { E } Mat R )
3 mat1rhmval.b 
 |-  B = ( Base ` A )
4 mat1rhmval.o 
 |-  O = <. E , E >.
5 mat1rhmval.f 
 |-  F = ( x e. K |-> { <. O , x >. } )
6 eqid 
 |-  ( +g ` R ) = ( +g ` R )
7 eqid 
 |-  ( +g ` A ) = ( +g ` A )
8 ringgrp 
 |-  ( R e. Ring -> R e. Grp )
9 8 adantr 
 |-  ( ( R e. Ring /\ E e. V ) -> R e. Grp )
10 snfi 
 |-  { E } e. Fin
11 simpl 
 |-  ( ( R e. Ring /\ E e. V ) -> R e. Ring )
12 2 matgrp 
 |-  ( ( { E } e. Fin /\ R e. Ring ) -> A e. Grp )
13 10 11 12 sylancr 
 |-  ( ( R e. Ring /\ E e. V ) -> A e. Grp )
14 1 2 3 4 5 mat1f 
 |-  ( ( R e. Ring /\ E e. V ) -> F : K --> B )
15 11 adantr 
 |-  ( ( ( R e. Ring /\ E e. V ) /\ ( w e. K /\ y e. K ) ) -> R e. Ring )
16 simpr 
 |-  ( ( R e. Ring /\ E e. V ) -> E e. V )
17 16 adantr 
 |-  ( ( ( R e. Ring /\ E e. V ) /\ ( w e. K /\ y e. K ) ) -> E e. V )
18 simpl 
 |-  ( ( w e. K /\ y e. K ) -> w e. K )
19 18 adantl 
 |-  ( ( ( R e. Ring /\ E e. V ) /\ ( w e. K /\ y e. K ) ) -> w e. K )
20 1 2 3 4 5 mat1rhmelval 
 |-  ( ( R e. Ring /\ E e. V /\ w e. K ) -> ( E ( F ` w ) E ) = w )
21 15 17 19 20 syl3anc 
 |-  ( ( ( R e. Ring /\ E e. V ) /\ ( w e. K /\ y e. K ) ) -> ( E ( F ` w ) E ) = w )
22 simpr 
 |-  ( ( w e. K /\ y e. K ) -> y e. K )
23 22 adantl 
 |-  ( ( ( R e. Ring /\ E e. V ) /\ ( w e. K /\ y e. K ) ) -> y e. K )
24 1 2 3 4 5 mat1rhmelval 
 |-  ( ( R e. Ring /\ E e. V /\ y e. K ) -> ( E ( F ` y ) E ) = y )
25 15 17 23 24 syl3anc 
 |-  ( ( ( R e. Ring /\ E e. V ) /\ ( w e. K /\ y e. K ) ) -> ( E ( F ` y ) E ) = y )
26 21 25 oveq12d 
 |-  ( ( ( R e. Ring /\ E e. V ) /\ ( w e. K /\ y e. K ) ) -> ( ( E ( F ` w ) E ) ( +g ` R ) ( E ( F ` y ) E ) ) = ( w ( +g ` R ) y ) )
27 1 2 3 4 5 mat1rhmcl 
 |-  ( ( R e. Ring /\ E e. V /\ w e. K ) -> ( F ` w ) e. B )
28 15 17 19 27 syl3anc 
 |-  ( ( ( R e. Ring /\ E e. V ) /\ ( w e. K /\ y e. K ) ) -> ( F ` w ) e. B )
29 1 2 3 4 5 mat1rhmcl 
 |-  ( ( R e. Ring /\ E e. V /\ y e. K ) -> ( F ` y ) e. B )
30 15 17 23 29 syl3anc 
 |-  ( ( ( R e. Ring /\ E e. V ) /\ ( w e. K /\ y e. K ) ) -> ( F ` y ) e. B )
31 snidg 
 |-  ( E e. V -> E e. { E } )
32 31 31 jca 
 |-  ( E e. V -> ( E e. { E } /\ E e. { E } ) )
33 32 adantl 
 |-  ( ( R e. Ring /\ E e. V ) -> ( E e. { E } /\ E e. { E } ) )
34 33 adantr 
 |-  ( ( ( R e. Ring /\ E e. V ) /\ ( w e. K /\ y e. K ) ) -> ( E e. { E } /\ E e. { E } ) )
35 2 3 7 6 matplusgcell 
 |-  ( ( ( ( F ` w ) e. B /\ ( F ` y ) e. B ) /\ ( E e. { E } /\ E e. { E } ) ) -> ( E ( ( F ` w ) ( +g ` A ) ( F ` y ) ) E ) = ( ( E ( F ` w ) E ) ( +g ` R ) ( E ( F ` y ) E ) ) )
36 28 30 34 35 syl21anc 
 |-  ( ( ( R e. Ring /\ E e. V ) /\ ( w e. K /\ y e. K ) ) -> ( E ( ( F ` w ) ( +g ` A ) ( F ` y ) ) E ) = ( ( E ( F ` w ) E ) ( +g ` R ) ( E ( F ` y ) E ) ) )
37 1 6 ringacl 
 |-  ( ( R e. Ring /\ w e. K /\ y e. K ) -> ( w ( +g ` R ) y ) e. K )
38 15 19 23 37 syl3anc 
 |-  ( ( ( R e. Ring /\ E e. V ) /\ ( w e. K /\ y e. K ) ) -> ( w ( +g ` R ) y ) e. K )
39 1 2 3 4 5 mat1rhmelval 
 |-  ( ( R e. Ring /\ E e. V /\ ( w ( +g ` R ) y ) e. K ) -> ( E ( F ` ( w ( +g ` R ) y ) ) E ) = ( w ( +g ` R ) y ) )
40 15 17 38 39 syl3anc 
 |-  ( ( ( R e. Ring /\ E e. V ) /\ ( w e. K /\ y e. K ) ) -> ( E ( F ` ( w ( +g ` R ) y ) ) E ) = ( w ( +g ` R ) y ) )
41 26 36 40 3eqtr4rd 
 |-  ( ( ( R e. Ring /\ E e. V ) /\ ( w e. K /\ y e. K ) ) -> ( E ( F ` ( w ( +g ` R ) y ) ) E ) = ( E ( ( F ` w ) ( +g ` A ) ( F ` y ) ) E ) )
42 oveq1 
 |-  ( i = E -> ( i ( F ` ( w ( +g ` R ) y ) ) j ) = ( E ( F ` ( w ( +g ` R ) y ) ) j ) )
43 oveq1 
 |-  ( i = E -> ( i ( ( F ` w ) ( +g ` A ) ( F ` y ) ) j ) = ( E ( ( F ` w ) ( +g ` A ) ( F ` y ) ) j ) )
44 42 43 eqeq12d 
 |-  ( i = E -> ( ( i ( F ` ( w ( +g ` R ) y ) ) j ) = ( i ( ( F ` w ) ( +g ` A ) ( F ` y ) ) j ) <-> ( E ( F ` ( w ( +g ` R ) y ) ) j ) = ( E ( ( F ` w ) ( +g ` A ) ( F ` y ) ) j ) ) )
45 oveq2 
 |-  ( j = E -> ( E ( F ` ( w ( +g ` R ) y ) ) j ) = ( E ( F ` ( w ( +g ` R ) y ) ) E ) )
46 oveq2 
 |-  ( j = E -> ( E ( ( F ` w ) ( +g ` A ) ( F ` y ) ) j ) = ( E ( ( F ` w ) ( +g ` A ) ( F ` y ) ) E ) )
47 45 46 eqeq12d 
 |-  ( j = E -> ( ( E ( F ` ( w ( +g ` R ) y ) ) j ) = ( E ( ( F ` w ) ( +g ` A ) ( F ` y ) ) j ) <-> ( E ( F ` ( w ( +g ` R ) y ) ) E ) = ( E ( ( F ` w ) ( +g ` A ) ( F ` y ) ) E ) ) )
48 44 47 2ralsng 
 |-  ( ( E e. V /\ E e. V ) -> ( A. i e. { E } A. j e. { E } ( i ( F ` ( w ( +g ` R ) y ) ) j ) = ( i ( ( F ` w ) ( +g ` A ) ( F ` y ) ) j ) <-> ( E ( F ` ( w ( +g ` R ) y ) ) E ) = ( E ( ( F ` w ) ( +g ` A ) ( F ` y ) ) E ) ) )
49 16 16 48 syl2anc 
 |-  ( ( R e. Ring /\ E e. V ) -> ( A. i e. { E } A. j e. { E } ( i ( F ` ( w ( +g ` R ) y ) ) j ) = ( i ( ( F ` w ) ( +g ` A ) ( F ` y ) ) j ) <-> ( E ( F ` ( w ( +g ` R ) y ) ) E ) = ( E ( ( F ` w ) ( +g ` A ) ( F ` y ) ) E ) ) )
50 49 adantr 
 |-  ( ( ( R e. Ring /\ E e. V ) /\ ( w e. K /\ y e. K ) ) -> ( A. i e. { E } A. j e. { E } ( i ( F ` ( w ( +g ` R ) y ) ) j ) = ( i ( ( F ` w ) ( +g ` A ) ( F ` y ) ) j ) <-> ( E ( F ` ( w ( +g ` R ) y ) ) E ) = ( E ( ( F ` w ) ( +g ` A ) ( F ` y ) ) E ) ) )
51 41 50 mpbird 
 |-  ( ( ( R e. Ring /\ E e. V ) /\ ( w e. K /\ y e. K ) ) -> A. i e. { E } A. j e. { E } ( i ( F ` ( w ( +g ` R ) y ) ) j ) = ( i ( ( F ` w ) ( +g ` A ) ( F ` y ) ) j ) )
52 1 2 3 4 5 mat1rhmcl 
 |-  ( ( R e. Ring /\ E e. V /\ ( w ( +g ` R ) y ) e. K ) -> ( F ` ( w ( +g ` R ) y ) ) e. B )
53 15 17 38 52 syl3anc 
 |-  ( ( ( R e. Ring /\ E e. V ) /\ ( w e. K /\ y e. K ) ) -> ( F ` ( w ( +g ` R ) y ) ) e. B )
54 2 matring 
 |-  ( ( { E } e. Fin /\ R e. Ring ) -> A e. Ring )
55 10 11 54 sylancr 
 |-  ( ( R e. Ring /\ E e. V ) -> A e. Ring )
56 55 adantr 
 |-  ( ( ( R e. Ring /\ E e. V ) /\ ( w e. K /\ y e. K ) ) -> A e. Ring )
57 3 7 ringacl 
 |-  ( ( A e. Ring /\ ( F ` w ) e. B /\ ( F ` y ) e. B ) -> ( ( F ` w ) ( +g ` A ) ( F ` y ) ) e. B )
58 56 28 30 57 syl3anc 
 |-  ( ( ( R e. Ring /\ E e. V ) /\ ( w e. K /\ y e. K ) ) -> ( ( F ` w ) ( +g ` A ) ( F ` y ) ) e. B )
59 2 3 eqmat 
 |-  ( ( ( F ` ( w ( +g ` R ) y ) ) e. B /\ ( ( F ` w ) ( +g ` A ) ( F ` y ) ) e. B ) -> ( ( F ` ( w ( +g ` R ) y ) ) = ( ( F ` w ) ( +g ` A ) ( F ` y ) ) <-> A. i e. { E } A. j e. { E } ( i ( F ` ( w ( +g ` R ) y ) ) j ) = ( i ( ( F ` w ) ( +g ` A ) ( F ` y ) ) j ) ) )
60 53 58 59 syl2anc 
 |-  ( ( ( R e. Ring /\ E e. V ) /\ ( w e. K /\ y e. K ) ) -> ( ( F ` ( w ( +g ` R ) y ) ) = ( ( F ` w ) ( +g ` A ) ( F ` y ) ) <-> A. i e. { E } A. j e. { E } ( i ( F ` ( w ( +g ` R ) y ) ) j ) = ( i ( ( F ` w ) ( +g ` A ) ( F ` y ) ) j ) ) )
61 51 60 mpbird 
 |-  ( ( ( R e. Ring /\ E e. V ) /\ ( w e. K /\ y e. K ) ) -> ( F ` ( w ( +g ` R ) y ) ) = ( ( F ` w ) ( +g ` A ) ( F ` y ) ) )
62 1 3 6 7 9 13 14 61 isghmd 
 |-  ( ( R e. Ring /\ E e. V ) -> F e. ( R GrpHom A ) )