Metamath Proof Explorer

Theorem mgpf

Description: Restricted functionality of the multiplicative group on rings. (Contributed by Mario Carneiro, 11-Mar-2015)

Ref Expression
Assertion mgpf 
|- ( mulGrp |` Ring ) : Ring --> Mnd

Proof

Step Hyp Ref Expression
1 fnmgp 
 |-  mulGrp Fn _V
2 ssv 
 |-  Ring C_ _V
3 fnssres 
 |-  ( ( mulGrp Fn _V /\ Ring C_ _V ) -> ( mulGrp |` Ring ) Fn Ring )
4 1 2 3 mp2an 
 |-  ( mulGrp |` Ring ) Fn Ring
5 fvres 
 |-  ( a e. Ring -> ( ( mulGrp |` Ring ) ` a ) = ( mulGrp ` a ) )
6 eqid 
 |-  ( mulGrp ` a ) = ( mulGrp ` a )
7 6 ringmgp 
 |-  ( a e. Ring -> ( mulGrp ` a ) e. Mnd )
8 5 7 eqeltrd 
 |-  ( a e. Ring -> ( ( mulGrp |` Ring ) ` a ) e. Mnd )
9 8 rgen 
 |-  A. a e. Ring ( ( mulGrp |` Ring ) ` a ) e. Mnd
10 ffnfv 
 |-  ( ( mulGrp |` Ring ) : Ring --> Mnd <-> ( ( mulGrp |` Ring ) Fn Ring /\ A. a e. Ring ( ( mulGrp |` Ring ) ` a ) e. Mnd ) )
11 4 9 10 mpbir2an 
 |-  ( mulGrp |` Ring ) : Ring --> Mnd