| 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 ‘ 𝑅 ) ) ) |