![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > mgpf | Structured version Visualization version GIF version |
Description: Restricted functionality of the multiplicative group on rings. (Contributed by Mario Carneiro, 11-Mar-2015.) |
Ref | Expression |
---|---|
mgpf | ⊢ (mulGrp ↾ Ring):Ring⟶Mnd |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fnmgp 18687 | . . 3 ⊢ mulGrp Fn V | |
2 | ssv 3762 | . . 3 ⊢ Ring ⊆ V | |
3 | fnssres 6161 | . . 3 ⊢ ((mulGrp Fn V ∧ Ring ⊆ V) → (mulGrp ↾ Ring) Fn Ring) | |
4 | 1, 2, 3 | mp2an 710 | . 2 ⊢ (mulGrp ↾ Ring) Fn Ring |
5 | fvres 6364 | . . . 4 ⊢ (𝑎 ∈ Ring → ((mulGrp ↾ Ring)‘𝑎) = (mulGrp‘𝑎)) | |
6 | eqid 2756 | . . . . 5 ⊢ (mulGrp‘𝑎) = (mulGrp‘𝑎) | |
7 | 6 | ringmgp 18749 | . . . 4 ⊢ (𝑎 ∈ Ring → (mulGrp‘𝑎) ∈ Mnd) |
8 | 5, 7 | eqeltrd 2835 | . . 3 ⊢ (𝑎 ∈ Ring → ((mulGrp ↾ Ring)‘𝑎) ∈ Mnd) |
9 | 8 | rgen 3056 | . 2 ⊢ ∀𝑎 ∈ Ring ((mulGrp ↾ Ring)‘𝑎) ∈ Mnd |
10 | ffnfv 6547 | . 2 ⊢ ((mulGrp ↾ Ring):Ring⟶Mnd ↔ ((mulGrp ↾ Ring) Fn Ring ∧ ∀𝑎 ∈ Ring ((mulGrp ↾ Ring)‘𝑎) ∈ Mnd)) | |
11 | 4, 9, 10 | mpbir2an 993 | 1 ⊢ (mulGrp ↾ Ring):Ring⟶Mnd |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2135 ∀wral 3046 Vcvv 3336 ⊆ wss 3711 ↾ cres 5264 Fn wfn 6040 ⟶wf 6041 ‘cfv 6045 Mndcmnd 17491 mulGrpcmgp 18685 Ringcrg 18743 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1867 ax-4 1882 ax-5 1984 ax-6 2050 ax-7 2086 ax-9 2144 ax-10 2164 ax-11 2179 ax-12 2192 ax-13 2387 ax-ext 2736 ax-sep 4929 ax-nul 4937 ax-pr 5051 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3an 1074 df-tru 1631 df-ex 1850 df-nf 1855 df-sb 2043 df-eu 2607 df-mo 2608 df-clab 2743 df-cleq 2749 df-clel 2752 df-nfc 2887 df-ral 3051 df-rex 3052 df-rab 3055 df-v 3338 df-sbc 3573 df-dif 3714 df-un 3716 df-in 3718 df-ss 3725 df-nul 4055 df-if 4227 df-sn 4318 df-pr 4320 df-op 4324 df-uni 4585 df-br 4801 df-opab 4861 df-mpt 4878 df-id 5170 df-xp 5268 df-rel 5269 df-cnv 5270 df-co 5271 df-dm 5272 df-rn 5273 df-res 5274 df-iota 6008 df-fun 6047 df-fn 6048 df-f 6049 df-fv 6053 df-ov 6812 df-mgp 18686 df-ring 18745 |
This theorem is referenced by: prdsringd 18808 prds1 18810 |
Copyright terms: Public domain | W3C validator |