Metamath Proof Explorer

Theorem mat1mhm

Description: There is a monoid homomorphism from the multiplicative group of a ring to the multiplicative 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 >. } )
mat1mhm.m 
|- M = ( mulGrp ` R )
mat1mhm.n 
|- N = ( mulGrp ` A )
Assertion mat1mhm 
|- ( ( R e. Ring /\ E e. V ) -> F e. ( M MndHom N ) )

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 mat1mhm.m 
 |-  M = ( mulGrp ` R )
7 mat1mhm.n 
 |-  N = ( mulGrp ` A )
8 6 ringmgp 
 |-  ( R e. Ring -> M e. Mnd )
9 8 adantr 
 |-  ( ( R e. Ring /\ E e. V ) -> M e. Mnd )
10 snfi 
 |-  { E } e. Fin
11 simpl 
 |-  ( ( R e. Ring /\ E e. V ) -> R e. Ring )
12 2 matring 
 |-  ( ( { E } e. Fin /\ R e. Ring ) -> A e. Ring )
13 10 11 12 sylancr 
 |-  ( ( R e. Ring /\ E e. V ) -> A e. Ring )
14 7 ringmgp 
 |-  ( A e. Ring -> N e. Mnd )
15 13 14 syl 
 |-  ( ( R e. Ring /\ E e. V ) -> N e. Mnd )
16 1 2 3 4 5 mat1f 
 |-  ( ( R e. Ring /\ E e. V ) -> F : K --> B )
17 ringmnd 
 |-  ( R e. Ring -> R e. Mnd )
18 17 adantr 
 |-  ( ( R e. Ring /\ E e. V ) -> R e. Mnd )
19 18 adantr 
 |-  ( ( ( R e. Ring /\ E e. V ) /\ ( w e. K /\ y e. K ) ) -> R e. Mnd )
20 simpr 
 |-  ( ( R e. Ring /\ E e. V ) -> E e. V )
21 20 adantr 
 |-  ( ( ( R e. Ring /\ E e. V ) /\ ( w e. K /\ y e. K ) ) -> E e. V )
22 simpll 
 |-  ( ( ( R e. Ring /\ E e. V ) /\ ( w e. K /\ y e. K ) ) -> R e. Ring )
23 eqid 
 |-  ( Base ` A ) = ( Base ` A )
24 snidg 
 |-  ( E e. V -> E e. { E } )
25 24 ad2antlr 
 |-  ( ( ( R e. Ring /\ E e. V ) /\ ( w e. K /\ y e. K ) ) -> E e. { E } )
26 simprl 
 |-  ( ( ( R e. Ring /\ E e. V ) /\ ( w e. K /\ y e. K ) ) -> w e. K )
27 1 2 23 4 5 mat1rhmcl 
 |-  ( ( R e. Ring /\ E e. V /\ w e. K ) -> ( F ` w ) e. ( Base ` A ) )
28 22 21 26 27 syl3anc 
 |-  ( ( ( R e. Ring /\ E e. V ) /\ ( w e. K /\ y e. K ) ) -> ( F ` w ) e. ( Base ` A ) )
29 2 1 23 25 25 28 matecld 
 |-  ( ( ( R e. Ring /\ E e. V ) /\ ( w e. K /\ y e. K ) ) -> ( E ( F ` w ) E ) e. K )
30 simprr 
 |-  ( ( ( R e. Ring /\ E e. V ) /\ ( w e. K /\ y e. K ) ) -> y e. K )
31 1 2 23 4 5 mat1rhmcl 
 |-  ( ( R e. Ring /\ E e. V /\ y e. K ) -> ( F ` y ) e. ( Base ` A ) )
32 22 21 30 31 syl3anc 
 |-  ( ( ( R e. Ring /\ E e. V ) /\ ( w e. K /\ y e. K ) ) -> ( F ` y ) e. ( Base ` A ) )
33 2 1 23 25 25 32 matecld 
 |-  ( ( ( R e. Ring /\ E e. V ) /\ ( w e. K /\ y e. K ) ) -> ( E ( F ` y ) E ) e. K )
34 eqid 
 |-  ( .r ` R ) = ( .r ` R )
35 1 34 ringcl 
 |-  ( ( R e. Ring /\ ( E ( F ` w ) E ) e. K /\ ( E ( F ` y ) E ) e. K ) -> ( ( E ( F ` w ) E ) ( .r ` R ) ( E ( F ` y ) E ) ) e. K )
36 22 29 33 35 syl3anc 
 |-  ( ( ( R e. Ring /\ E e. V ) /\ ( w e. K /\ y e. K ) ) -> ( ( E ( F ` w ) E ) ( .r ` R ) ( E ( F ` y ) E ) ) e. K )
37 oveq2 
 |-  ( e = E -> ( E ( F ` w ) e ) = ( E ( F ` w ) E ) )
38 oveq1 
 |-  ( e = E -> ( e ( F ` y ) E ) = ( E ( F ` y ) E ) )
39 37 38 oveq12d 
 |-  ( e = E -> ( ( E ( F ` w ) e ) ( .r ` R ) ( e ( F ` y ) E ) ) = ( ( E ( F ` w ) E ) ( .r ` R ) ( E ( F ` y ) E ) ) )
40 39 adantl 
 |-  ( ( ( ( R e. Ring /\ E e. V ) /\ ( w e. K /\ y e. K ) ) /\ e = E ) -> ( ( E ( F ` w ) e ) ( .r ` R ) ( e ( F ` y ) E ) ) = ( ( E ( F ` w ) E ) ( .r ` R ) ( E ( F ` y ) E ) ) )
41 1 19 21 36 40 gsumsnd 
 |-  ( ( ( R e. Ring /\ E e. V ) /\ ( w e. K /\ y e. K ) ) -> ( R gsum ( e e. { E } |-> ( ( E ( F ` w ) e ) ( .r ` R ) ( e ( F ` y ) E ) ) ) ) = ( ( E ( F ` w ) E ) ( .r ` R ) ( E ( F ` y ) E ) ) )
42 1 2 3 4 5 mat1rhmelval 
 |-  ( ( R e. Ring /\ E e. V /\ w e. K ) -> ( E ( F ` w ) E ) = w )
43 22 21 26 42 syl3anc 
 |-  ( ( ( R e. Ring /\ E e. V ) /\ ( w e. K /\ y e. K ) ) -> ( E ( F ` w ) E ) = w )
44 1 2 3 4 5 mat1rhmelval 
 |-  ( ( R e. Ring /\ E e. V /\ y e. K ) -> ( E ( F ` y ) E ) = y )
45 22 21 30 44 syl3anc 
 |-  ( ( ( R e. Ring /\ E e. V ) /\ ( w e. K /\ y e. K ) ) -> ( E ( F ` y ) E ) = y )
46 43 45 oveq12d 
 |-  ( ( ( R e. Ring /\ E e. V ) /\ ( w e. K /\ y e. K ) ) -> ( ( E ( F ` w ) E ) ( .r ` R ) ( E ( F ` y ) E ) ) = ( w ( .r ` R ) y ) )
47 41 46 eqtrd 
 |-  ( ( ( R e. Ring /\ E e. V ) /\ ( w e. K /\ y e. K ) ) -> ( R gsum ( e e. { E } |-> ( ( E ( F ` w ) e ) ( .r ` R ) ( e ( F ` y ) E ) ) ) ) = ( w ( .r ` R ) y ) )
48 1 2 3 4 5 mat1rhmcl 
 |-  ( ( R e. Ring /\ E e. V /\ w e. K ) -> ( F ` w ) e. B )
49 22 21 26 48 syl3anc 
 |-  ( ( ( R e. Ring /\ E e. V ) /\ ( w e. K /\ y e. K ) ) -> ( F ` w ) e. B )
50 1 2 3 4 5 mat1rhmcl 
 |-  ( ( R e. Ring /\ E e. V /\ y e. K ) -> ( F ` y ) e. B )
51 22 21 30 50 syl3anc 
 |-  ( ( ( R e. Ring /\ E e. V ) /\ ( w e. K /\ y e. K ) ) -> ( F ` y ) e. B )
52 49 51 jca 
 |-  ( ( ( R e. Ring /\ E e. V ) /\ ( w e. K /\ y e. K ) ) -> ( ( F ` w ) e. B /\ ( F ` y ) e. B ) )
53 24 24 jca 
 |-  ( E e. V -> ( E e. { E } /\ E e. { E } ) )
54 53 ad2antlr 
 |-  ( ( ( R e. Ring /\ E e. V ) /\ ( w e. K /\ y e. K ) ) -> ( E e. { E } /\ E e. { E } ) )
55 eqid 
 |-  ( .r ` A ) = ( .r ` A )
56 2 3 55 matmulcell 
 |-  ( ( R e. Ring /\ ( ( F ` w ) e. B /\ ( F ` y ) e. B ) /\ ( E e. { E } /\ E e. { E } ) ) -> ( E ( ( F ` w ) ( .r ` A ) ( F ` y ) ) E ) = ( R gsum ( e e. { E } |-> ( ( E ( F ` w ) e ) ( .r ` R ) ( e ( F ` y ) E ) ) ) ) )
57 22 52 54 56 syl3anc 
 |-  ( ( ( R e. Ring /\ E e. V ) /\ ( w e. K /\ y e. K ) ) -> ( E ( ( F ` w ) ( .r ` A ) ( F ` y ) ) E ) = ( R gsum ( e e. { E } |-> ( ( E ( F ` w ) e ) ( .r ` R ) ( e ( F ` y ) E ) ) ) ) )
58 1 34 ringcl 
 |-  ( ( R e. Ring /\ w e. K /\ y e. K ) -> ( w ( .r ` R ) y ) e. K )
59 22 26 30 58 syl3anc 
 |-  ( ( ( R e. Ring /\ E e. V ) /\ ( w e. K /\ y e. K ) ) -> ( w ( .r ` R ) y ) e. K )
60 1 2 3 4 5 mat1rhmelval 
 |-  ( ( R e. Ring /\ E e. V /\ ( w ( .r ` R ) y ) e. K ) -> ( E ( F ` ( w ( .r ` R ) y ) ) E ) = ( w ( .r ` R ) y ) )
61 22 21 59 60 syl3anc 
 |-  ( ( ( R e. Ring /\ E e. V ) /\ ( w e. K /\ y e. K ) ) -> ( E ( F ` ( w ( .r ` R ) y ) ) E ) = ( w ( .r ` R ) y ) )
62 47 57 61 3eqtr4rd 
 |-  ( ( ( R e. Ring /\ E e. V ) /\ ( w e. K /\ y e. K ) ) -> ( E ( F ` ( w ( .r ` R ) y ) ) E ) = ( E ( ( F ` w ) ( .r ` A ) ( F ` y ) ) E ) )
63 oveq1 
 |-  ( i = E -> ( i ( F ` ( w ( .r ` R ) y ) ) j ) = ( E ( F ` ( w ( .r ` R ) y ) ) j ) )
64 oveq1 
 |-  ( i = E -> ( i ( ( F ` w ) ( .r ` A ) ( F ` y ) ) j ) = ( E ( ( F ` w ) ( .r ` A ) ( F ` y ) ) j ) )
65 63 64 eqeq12d 
 |-  ( i = E -> ( ( i ( F ` ( w ( .r ` R ) y ) ) j ) = ( i ( ( F ` w ) ( .r ` A ) ( F ` y ) ) j ) <-> ( E ( F ` ( w ( .r ` R ) y ) ) j ) = ( E ( ( F ` w ) ( .r ` A ) ( F ` y ) ) j ) ) )
66 oveq2 
 |-  ( j = E -> ( E ( F ` ( w ( .r ` R ) y ) ) j ) = ( E ( F ` ( w ( .r ` R ) y ) ) E ) )
67 oveq2 
 |-  ( j = E -> ( E ( ( F ` w ) ( .r ` A ) ( F ` y ) ) j ) = ( E ( ( F ` w ) ( .r ` A ) ( F ` y ) ) E ) )
68 66 67 eqeq12d 
 |-  ( j = E -> ( ( E ( F ` ( w ( .r ` R ) y ) ) j ) = ( E ( ( F ` w ) ( .r ` A ) ( F ` y ) ) j ) <-> ( E ( F ` ( w ( .r ` R ) y ) ) E ) = ( E ( ( F ` w ) ( .r ` A ) ( F ` y ) ) E ) ) )
69 65 68 2ralsng 
 |-  ( ( E e. V /\ E e. V ) -> ( A. i e. { E } A. j e. { E } ( i ( F ` ( w ( .r ` R ) y ) ) j ) = ( i ( ( F ` w ) ( .r ` A ) ( F ` y ) ) j ) <-> ( E ( F ` ( w ( .r ` R ) y ) ) E ) = ( E ( ( F ` w ) ( .r ` A ) ( F ` y ) ) E ) ) )
70 20 69 sylancom 
 |-  ( ( R e. Ring /\ E e. V ) -> ( A. i e. { E } A. j e. { E } ( i ( F ` ( w ( .r ` R ) y ) ) j ) = ( i ( ( F ` w ) ( .r ` A ) ( F ` y ) ) j ) <-> ( E ( F ` ( w ( .r ` R ) y ) ) E ) = ( E ( ( F ` w ) ( .r ` A ) ( F ` y ) ) E ) ) )
71 70 adantr 
 |-  ( ( ( R e. Ring /\ E e. V ) /\ ( w e. K /\ y e. K ) ) -> ( A. i e. { E } A. j e. { E } ( i ( F ` ( w ( .r ` R ) y ) ) j ) = ( i ( ( F ` w ) ( .r ` A ) ( F ` y ) ) j ) <-> ( E ( F ` ( w ( .r ` R ) y ) ) E ) = ( E ( ( F ` w ) ( .r ` A ) ( F ` y ) ) E ) ) )
72 62 71 mpbird 
 |-  ( ( ( R e. Ring /\ E e. V ) /\ ( w e. K /\ y e. K ) ) -> A. i e. { E } A. j e. { E } ( i ( F ` ( w ( .r ` R ) y ) ) j ) = ( i ( ( F ` w ) ( .r ` A ) ( F ` y ) ) j ) )
73 1 2 3 4 5 mat1rhmcl 
 |-  ( ( R e. Ring /\ E e. V /\ ( w ( .r ` R ) y ) e. K ) -> ( F ` ( w ( .r ` R ) y ) ) e. B )
74 22 21 59 73 syl3anc 
 |-  ( ( ( R e. Ring /\ E e. V ) /\ ( w e. K /\ y e. K ) ) -> ( F ` ( w ( .r ` R ) y ) ) e. B )
75 13 adantr 
 |-  ( ( ( R e. Ring /\ E e. V ) /\ ( w e. K /\ y e. K ) ) -> A e. Ring )
76 3 55 ringcl 
 |-  ( ( A e. Ring /\ ( F ` w ) e. B /\ ( F ` y ) e. B ) -> ( ( F ` w ) ( .r ` A ) ( F ` y ) ) e. B )
77 75 49 51 76 syl3anc 
 |-  ( ( ( R e. Ring /\ E e. V ) /\ ( w e. K /\ y e. K ) ) -> ( ( F ` w ) ( .r ` A ) ( F ` y ) ) e. B )
78 2 3 eqmat 
 |-  ( ( ( F ` ( w ( .r ` R ) y ) ) e. B /\ ( ( F ` w ) ( .r ` A ) ( F ` y ) ) e. B ) -> ( ( F ` ( w ( .r ` R ) y ) ) = ( ( F ` w ) ( .r ` A ) ( F ` y ) ) <-> A. i e. { E } A. j e. { E } ( i ( F ` ( w ( .r ` R ) y ) ) j ) = ( i ( ( F ` w ) ( .r ` A ) ( F ` y ) ) j ) ) )
79 74 77 78 syl2anc 
 |-  ( ( ( R e. Ring /\ E e. V ) /\ ( w e. K /\ y e. K ) ) -> ( ( F ` ( w ( .r ` R ) y ) ) = ( ( F ` w ) ( .r ` A ) ( F ` y ) ) <-> A. i e. { E } A. j e. { E } ( i ( F ` ( w ( .r ` R ) y ) ) j ) = ( i ( ( F ` w ) ( .r ` A ) ( F ` y ) ) j ) ) )
80 72 79 mpbird 
 |-  ( ( ( R e. Ring /\ E e. V ) /\ ( w e. K /\ y e. K ) ) -> ( F ` ( w ( .r ` R ) y ) ) = ( ( F ` w ) ( .r ` A ) ( F ` y ) ) )
81 80 ralrimivva 
 |-  ( ( R e. Ring /\ E e. V ) -> A. w e. K A. y e. K ( F ` ( w ( .r ` R ) y ) ) = ( ( F ` w ) ( .r ` A ) ( F ` y ) ) )
82 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
83 1 82 ringidcl 
 |-  ( R e. Ring -> ( 1r ` R ) e. K )
84 83 adantr 
 |-  ( ( R e. Ring /\ E e. V ) -> ( 1r ` R ) e. K )
85 1 2 3 4 5 mat1rhmval 
 |-  ( ( R e. Ring /\ E e. V /\ ( 1r ` R ) e. K ) -> ( F ` ( 1r ` R ) ) = { <. O , ( 1r ` R ) >. } )
86 84 85 mpd3an3 
 |-  ( ( R e. Ring /\ E e. V ) -> ( F ` ( 1r ` R ) ) = { <. O , ( 1r ` R ) >. } )
87 2 1 4 mat1dimid 
 |-  ( ( R e. Ring /\ E e. V ) -> ( 1r ` A ) = { <. O , ( 1r ` R ) >. } )
88 86 87 eqtr4d 
 |-  ( ( R e. Ring /\ E e. V ) -> ( F ` ( 1r ` R ) ) = ( 1r ` A ) )
89 16 81 88 3jca 
 |-  ( ( R e. Ring /\ E e. V ) -> ( F : K --> B /\ A. w e. K A. y e. K ( F ` ( w ( .r ` R ) y ) ) = ( ( F ` w ) ( .r ` A ) ( F ` y ) ) /\ ( F ` ( 1r ` R ) ) = ( 1r ` A ) ) )
90 6 1 mgpbas 
 |-  K = ( Base ` M )
91 7 3 mgpbas 
 |-  B = ( Base ` N )
92 6 34 mgpplusg 
 |-  ( .r ` R ) = ( +g ` M )
93 7 55 mgpplusg 
 |-  ( .r ` A ) = ( +g ` N )
94 6 82 ringidval 
 |-  ( 1r ` R ) = ( 0g ` M )
95 eqid 
 |-  ( 1r ` A ) = ( 1r ` A )
96 7 95 ringidval 
 |-  ( 1r ` A ) = ( 0g ` N )
97 90 91 92 93 94 96 ismhm 
 |-  ( F e. ( M MndHom N ) <-> ( ( M e. Mnd /\ N e. Mnd ) /\ ( F : K --> B /\ A. w e. K A. y e. K ( F ` ( w ( .r ` R ) y ) ) = ( ( F ` w ) ( .r ` A ) ( F ` y ) ) /\ ( F ` ( 1r ` R ) ) = ( 1r ` A ) ) ) )
98 9 15 89 97 syl21anbrc 
 |-  ( ( R e. Ring /\ E e. V ) -> F e. ( M MndHom N ) )