This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝑅 ∈ Ring ∧ 𝐴 ∈ Fin ) → ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝐴 ) ) ∈ ( ( SymGrp ‘ 𝐴 ) MndHom ( mulGrp ‘ 𝑅 ) ) )

Proof

Step Hyp Ref Expression
1 eqid ⊢ ( ℤRHom ‘ 𝑅 ) = ( ℤRHom ‘ 𝑅 )
2 1 zrhrhm ⊢ ( 𝑅 ∈ Ring → ( ℤRHom ‘ 𝑅 ) ∈ ( ℤring RingHom 𝑅 ) )
3 eqid ⊢ ( mulGrp ‘ ℤring ) = ( mulGrp ‘ ℤring )
4 eqid ⊢ ( mulGrp ‘ 𝑅 ) = ( mulGrp ‘ 𝑅 )
5 3 4 rhmmhm ⊢ ( ( ℤRHom ‘ 𝑅 ) ∈ ( ℤring RingHom 𝑅 ) → ( ℤRHom ‘ 𝑅 ) ∈ ( ( mulGrp ‘ ℤring ) MndHom ( mulGrp ‘ 𝑅 ) ) )
6 2 5 syl ⊢ ( 𝑅 ∈ Ring → ( ℤRHom ‘ 𝑅 ) ∈ ( ( mulGrp ‘ ℤring ) MndHom ( mulGrp ‘ 𝑅 ) ) )
7 eqid ⊢ ( SymGrp ‘ 𝐴 ) = ( SymGrp ‘ 𝐴 )
8 eqid ⊢ ( pmSgn ‘ 𝐴 ) = ( pmSgn ‘ 𝐴 )
9 eqid ⊢ ( ( mulGrp ‘ ℂfld ) ↾s { 1 , - 1 } ) = ( ( mulGrp ‘ ℂfld ) ↾s { 1 , - 1 } )
10 7 8 9 psgnghm2 ⊢ ( 𝐴 ∈ Fin → ( pmSgn ‘ 𝐴 ) ∈ ( ( SymGrp ‘ 𝐴 ) GrpHom ( ( mulGrp ‘ ℂfld ) ↾s { 1 , - 1 } ) ) )
11 ghmmhm ⊢ ( ( pmSgn ‘ 𝐴 ) ∈ ( ( SymGrp ‘ 𝐴 ) GrpHom ( ( mulGrp ‘ ℂfld ) ↾s { 1 , - 1 } ) ) → ( pmSgn ‘ 𝐴 ) ∈ ( ( SymGrp ‘ 𝐴 ) MndHom ( ( mulGrp ‘ ℂfld ) ↾s { 1 , - 1 } ) ) )
12 10 11 syl ⊢ ( 𝐴 ∈ Fin → ( pmSgn ‘ 𝐴 ) ∈ ( ( SymGrp ‘ 𝐴 ) MndHom ( ( mulGrp ‘ ℂfld ) ↾s { 1 , - 1 } ) ) )
13 eqid ⊢ ( ( mulGrp ‘ ℂfld ) ↾s ( ℂ ∖ { 0 } ) ) = ( ( mulGrp ‘ ℂfld ) ↾s ( ℂ ∖ { 0 } ) )
14 13 cnmsgnsubg ⊢ { 1 , - 1 } ∈ ( SubGrp ‘ ( ( mulGrp ‘ ℂfld ) ↾s ( ℂ ∖ { 0 } ) ) )
15 subgsubm ⊢ ( { 1 , - 1 } ∈ ( SubGrp ‘ ( ( mulGrp ‘ ℂfld ) ↾s ( ℂ ∖ { 0 } ) ) ) → { 1 , - 1 } ∈ ( SubMnd ‘ ( ( mulGrp ‘ ℂfld ) ↾s ( ℂ ∖ { 0 } ) ) ) )
16 14 15 ax-mp ⊢ { 1 , - 1 } ∈ ( SubMnd ‘ ( ( mulGrp ‘ ℂfld ) ↾s ( ℂ ∖ { 0 } ) ) )
17 cnring ⊢ ℂfld ∈ Ring
18 cnfldbas ⊢ ℂ = ( Base ‘ ℂfld )
19 cnfld0 ⊢ 0 = ( 0g ‘ ℂfld )
20 cndrng ⊢ ℂfld ∈ DivRing
21 18 19 20 drngui ⊢ ( ℂ ∖ { 0 } ) = ( Unit ‘ ℂfld )
22 eqid ⊢ ( mulGrp ‘ ℂfld ) = ( mulGrp ‘ ℂfld )
23 21 22 unitsubm ⊢ ( ℂfld ∈ Ring → ( ℂ ∖ { 0 } ) ∈ ( SubMnd ‘ ( mulGrp ‘ ℂfld ) ) )
24 13 subsubm ⊢ ( ( ℂ ∖ { 0 } ) ∈ ( SubMnd ‘ ( mulGrp ‘ ℂfld ) ) → ( { 1 , - 1 } ∈ ( SubMnd ‘ ( ( mulGrp ‘ ℂfld ) ↾s ( ℂ ∖ { 0 } ) ) ) ↔ ( { 1 , - 1 } ∈ ( SubMnd ‘ ( mulGrp ‘ ℂfld ) ) ∧ { 1 , - 1 } ⊆ ( ℂ ∖ { 0 } ) ) ) )
25 17 23 24 mp2b ⊢ ( { 1 , - 1 } ∈ ( SubMnd ‘ ( ( mulGrp ‘ ℂfld ) ↾s ( ℂ ∖ { 0 } ) ) ) ↔ ( { 1 , - 1 } ∈ ( SubMnd ‘ ( mulGrp ‘ ℂfld ) ) ∧ { 1 , - 1 } ⊆ ( ℂ ∖ { 0 } ) ) )
26 16 25 mpbi ⊢ ( { 1 , - 1 } ∈ ( SubMnd ‘ ( mulGrp ‘ ℂfld ) ) ∧ { 1 , - 1 } ⊆ ( ℂ ∖ { 0 } ) )
27 26 simpli ⊢ { 1 , - 1 } ∈ ( SubMnd ‘ ( mulGrp ‘ ℂfld ) )
28 1z ⊢ 1 ∈ ℤ
29 neg1z ⊢ - 1 ∈ ℤ
30 prssi ⊢ ( ( 1 ∈ ℤ ∧ - 1 ∈ ℤ ) → { 1 , - 1 } ⊆ ℤ )
31 28 29 30 mp2an ⊢ { 1 , - 1 } ⊆ ℤ
32 zsubrg ⊢ ℤ ∈ ( SubRing ‘ ℂfld )
33 22 subrgsubm ⊢ ( ℤ ∈ ( SubRing ‘ ℂfld ) → ℤ ∈ ( SubMnd ‘ ( mulGrp ‘ ℂfld ) ) )
34 zringmpg ⊢ ( ( mulGrp ‘ ℂfld ) ↾s ℤ ) = ( mulGrp ‘ ℤring )
35 34 eqcomi ⊢ ( mulGrp ‘ ℤring ) = ( ( mulGrp ‘ ℂfld ) ↾s ℤ )
36 35 subsubm ⊢ ( ℤ ∈ ( SubMnd ‘ ( mulGrp ‘ ℂfld ) ) → ( { 1 , - 1 } ∈ ( SubMnd ‘ ( mulGrp ‘ ℤring ) ) ↔ ( { 1 , - 1 } ∈ ( SubMnd ‘ ( mulGrp ‘ ℂfld ) ) ∧ { 1 , - 1 } ⊆ ℤ ) ) )
37 32 33 36 mp2b ⊢ ( { 1 , - 1 } ∈ ( SubMnd ‘ ( mulGrp ‘ ℤring ) ) ↔ ( { 1 , - 1 } ∈ ( SubMnd ‘ ( mulGrp ‘ ℂfld ) ) ∧ { 1 , - 1 } ⊆ ℤ ) )
38 27 31 37 mpbir2an ⊢ { 1 , - 1 } ∈ ( SubMnd ‘ ( mulGrp ‘ ℤring ) )
39 zex ⊢ ℤ ∈ V
40 ressabs ⊢ ( ( ℤ ∈ V ∧ { 1 , - 1 } ⊆ ℤ ) → ( ( ( mulGrp ‘ ℂfld ) ↾s ℤ ) ↾s { 1 , - 1 } ) = ( ( mulGrp ‘ ℂfld ) ↾s { 1 , - 1 } ) )
41 39 31 40 mp2an ⊢ ( ( ( mulGrp ‘ ℂfld ) ↾s ℤ ) ↾s { 1 , - 1 } ) = ( ( mulGrp ‘ ℂfld ) ↾s { 1 , - 1 } )
42 34 oveq1i ⊢ ( ( ( mulGrp ‘ ℂfld ) ↾s ℤ ) ↾s { 1 , - 1 } ) = ( ( mulGrp ‘ ℤring ) ↾s { 1 , - 1 } )
43 41 42 eqtr3i ⊢ ( ( mulGrp ‘ ℂfld ) ↾s { 1 , - 1 } ) = ( ( mulGrp ‘ ℤring ) ↾s { 1 , - 1 } )
44 43 resmhm2 ⊢ ( ( ( pmSgn ‘ 𝐴 ) ∈ ( ( SymGrp ‘ 𝐴 ) MndHom ( ( mulGrp ‘ ℂfld ) ↾s { 1 , - 1 } ) ) ∧ { 1 , - 1 } ∈ ( SubMnd ‘ ( mulGrp ‘ ℤring ) ) ) → ( pmSgn ‘ 𝐴 ) ∈ ( ( SymGrp ‘ 𝐴 ) MndHom ( mulGrp ‘ ℤring ) ) )
45 12 38 44 sylancl ⊢ ( 𝐴 ∈ Fin → ( pmSgn ‘ 𝐴 ) ∈ ( ( SymGrp ‘ 𝐴 ) MndHom ( mulGrp ‘ ℤring ) ) )
46 mhmco ⊢ ( ( ( ℤRHom ‘ 𝑅 ) ∈ ( ( mulGrp ‘ ℤring ) MndHom ( mulGrp ‘ 𝑅 ) ) ∧ ( pmSgn ‘ 𝐴 ) ∈ ( ( SymGrp ‘ 𝐴 ) MndHom ( mulGrp ‘ ℤring ) ) ) → ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝐴 ) ) ∈ ( ( SymGrp ‘ 𝐴 ) MndHom ( mulGrp ‘ 𝑅 ) ) )
47 6 45 46 syl2an ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐴 ∈ Fin ) → ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝐴 ) ) ∈ ( ( SymGrp ‘ 𝐴 ) MndHom ( mulGrp ‘ 𝑅 ) ) )