Metamath Proof Explorer

Theorem zrhpsgnmhm

Description: Embedding of permutation signs into an arbitrary ring is a homomorphism. (Contributed by SO, 9-Jul-2018)

Ref Expression
Assertion zrhpsgnmhm 
|- ( ( R e. Ring /\ A e. Fin ) -> ( ( ZRHom ` R ) o. ( pmSgn ` A ) ) e. ( ( SymGrp ` A ) MndHom ( mulGrp ` R ) ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( ZRHom ` R ) = ( ZRHom ` R )
2 1 zrhrhm 
 |-  ( R e. Ring -> ( ZRHom ` R ) e. ( ZZring RingHom R ) )
3 eqid 
 |-  ( mulGrp ` ZZring ) = ( mulGrp ` ZZring )
4 eqid 
 |-  ( mulGrp ` R ) = ( mulGrp ` R )
5 3 4 rhmmhm 
 |-  ( ( ZRHom ` R ) e. ( ZZring RingHom R ) -> ( ZRHom ` R ) e. ( ( mulGrp ` ZZring ) MndHom ( mulGrp ` R ) ) )
6 2 5 syl 
 |-  ( R e. Ring -> ( ZRHom ` R ) e. ( ( mulGrp ` ZZring ) MndHom ( mulGrp ` R ) ) )
7 eqid 
 |-  ( SymGrp ` A ) = ( SymGrp ` A )
8 eqid 
 |-  ( pmSgn ` A ) = ( pmSgn ` A )
9 eqid 
 |-  ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } ) = ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } )
10 7 8 9 psgnghm2 
 |-  ( A e. Fin -> ( pmSgn ` A ) e. ( ( SymGrp ` A ) GrpHom ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } ) ) )
11 ghmmhm 
 |-  ( ( pmSgn ` A ) e. ( ( SymGrp ` A ) GrpHom ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } ) ) -> ( pmSgn ` A ) e. ( ( SymGrp ` A ) MndHom ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } ) ) )
12 10 11 syl 
 |-  ( A e. Fin -> ( pmSgn ` A ) e. ( ( SymGrp ` A ) MndHom ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } ) ) )
13 eqid 
 |-  ( ( mulGrp ` CCfld ) |`s ( CC \ { 0 } ) ) = ( ( mulGrp ` CCfld ) |`s ( CC \ { 0 } ) )
14 13 cnmsgnsubg 
 |-  { 1 , -u 1 } e. ( SubGrp ` ( ( mulGrp ` CCfld ) |`s ( CC \ { 0 } ) ) )
15 subgsubm 
 |-  ( { 1 , -u 1 } e. ( SubGrp ` ( ( mulGrp ` CCfld ) |`s ( CC \ { 0 } ) ) ) -> { 1 , -u 1 } e. ( SubMnd ` ( ( mulGrp ` CCfld ) |`s ( CC \ { 0 } ) ) ) )
16 14 15 ax-mp 
 |-  { 1 , -u 1 } e. ( SubMnd ` ( ( mulGrp ` CCfld ) |`s ( CC \ { 0 } ) ) )
17 cnring 
 |-  CCfld e. Ring
18 cnfldbas 
 |-  CC = ( Base ` CCfld )
19 cnfld0 
 |-  0 = ( 0g ` CCfld )
20 cndrng 
 |-  CCfld e. DivRing
21 18 19 20 drngui 
 |-  ( CC \ { 0 } ) = ( Unit ` CCfld )
22 eqid 
 |-  ( mulGrp ` CCfld ) = ( mulGrp ` CCfld )
23 21 22 unitsubm 
 |-  ( CCfld e. Ring -> ( CC \ { 0 } ) e. ( SubMnd ` ( mulGrp ` CCfld ) ) )
24 13 subsubm 
 |-  ( ( CC \ { 0 } ) e. ( SubMnd ` ( mulGrp ` CCfld ) ) -> ( { 1 , -u 1 } e. ( SubMnd ` ( ( mulGrp ` CCfld ) |`s ( CC \ { 0 } ) ) ) <-> ( { 1 , -u 1 } e. ( SubMnd ` ( mulGrp ` CCfld ) ) /\ { 1 , -u 1 } C_ ( CC \ { 0 } ) ) ) )
25 17 23 24 mp2b 
 |-  ( { 1 , -u 1 } e. ( SubMnd ` ( ( mulGrp ` CCfld ) |`s ( CC \ { 0 } ) ) ) <-> ( { 1 , -u 1 } e. ( SubMnd ` ( mulGrp ` CCfld ) ) /\ { 1 , -u 1 } C_ ( CC \ { 0 } ) ) )
26 16 25 mpbi 
 |-  ( { 1 , -u 1 } e. ( SubMnd ` ( mulGrp ` CCfld ) ) /\ { 1 , -u 1 } C_ ( CC \ { 0 } ) )
27 26 simpli 
 |-  { 1 , -u 1 } e. ( SubMnd ` ( mulGrp ` CCfld ) )
28 1z 
 |-  1 e. ZZ
29 neg1z 
 |-  -u 1 e. ZZ
30 prssi 
 |-  ( ( 1 e. ZZ /\ -u 1 e. ZZ ) -> { 1 , -u 1 } C_ ZZ )
31 28 29 30 mp2an 
 |-  { 1 , -u 1 } C_ ZZ
32 zsubrg 
 |-  ZZ e. ( SubRing ` CCfld )
33 22 subrgsubm 
 |-  ( ZZ e. ( SubRing ` CCfld ) -> ZZ e. ( SubMnd ` ( mulGrp ` CCfld ) ) )
34 zringmpg 
 |-  ( ( mulGrp ` CCfld ) |`s ZZ ) = ( mulGrp ` ZZring )
35 34 eqcomi 
 |-  ( mulGrp ` ZZring ) = ( ( mulGrp ` CCfld ) |`s ZZ )
36 35 subsubm 
 |-  ( ZZ e. ( SubMnd ` ( mulGrp ` CCfld ) ) -> ( { 1 , -u 1 } e. ( SubMnd ` ( mulGrp ` ZZring ) ) <-> ( { 1 , -u 1 } e. ( SubMnd ` ( mulGrp ` CCfld ) ) /\ { 1 , -u 1 } C_ ZZ ) ) )
37 32 33 36 mp2b 
 |-  ( { 1 , -u 1 } e. ( SubMnd ` ( mulGrp ` ZZring ) ) <-> ( { 1 , -u 1 } e. ( SubMnd ` ( mulGrp ` CCfld ) ) /\ { 1 , -u 1 } C_ ZZ ) )
38 27 31 37 mpbir2an 
 |-  { 1 , -u 1 } e. ( SubMnd ` ( mulGrp ` ZZring ) )
39 zex 
 |-  ZZ e. _V
40 ressabs 
 |-  ( ( ZZ e. _V /\ { 1 , -u 1 } C_ ZZ ) -> ( ( ( mulGrp ` CCfld ) |`s ZZ ) |`s { 1 , -u 1 } ) = ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } ) )
41 39 31 40 mp2an 
 |-  ( ( ( mulGrp ` CCfld ) |`s ZZ ) |`s { 1 , -u 1 } ) = ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } )
42 34 oveq1i 
 |-  ( ( ( mulGrp ` CCfld ) |`s ZZ ) |`s { 1 , -u 1 } ) = ( ( mulGrp ` ZZring ) |`s { 1 , -u 1 } )
43 41 42 eqtr3i 
 |-  ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } ) = ( ( mulGrp ` ZZring ) |`s { 1 , -u 1 } )
44 43 resmhm2 
 |-  ( ( ( pmSgn ` A ) e. ( ( SymGrp ` A ) MndHom ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } ) ) /\ { 1 , -u 1 } e. ( SubMnd ` ( mulGrp ` ZZring ) ) ) -> ( pmSgn ` A ) e. ( ( SymGrp ` A ) MndHom ( mulGrp ` ZZring ) ) )
45 12 38 44 sylancl 
 |-  ( A e. Fin -> ( pmSgn ` A ) e. ( ( SymGrp ` A ) MndHom ( mulGrp ` ZZring ) ) )
46 mhmco 
 |-  ( ( ( ZRHom ` R ) e. ( ( mulGrp ` ZZring ) MndHom ( mulGrp ` R ) ) /\ ( pmSgn ` A ) e. ( ( SymGrp ` A ) MndHom ( mulGrp ` ZZring ) ) ) -> ( ( ZRHom ` R ) o. ( pmSgn ` A ) ) e. ( ( SymGrp ` A ) MndHom ( mulGrp ` R ) ) )
47 6 45 46 syl2an 
 |-  ( ( R e. Ring /\ A e. Fin ) -> ( ( ZRHom ` R ) o. ( pmSgn ` A ) ) e. ( ( SymGrp ` A ) MndHom ( mulGrp ` R ) ) )