Metamath Proof Explorer

Theorem rngmgpf

Description: Restricted functionality of the multiplicative group on non-unital rings ( mgpf analog). (Contributed by AV, 22-Feb-2025)

Ref Expression
Assertion rngmgpf 
|- ( mulGrp |` Rng ) : Rng --> Smgrp

Proof

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