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 ⊆ V
3 fnssres ( ( mulGrp Fn V ∧ Ring ⊆ V ) → ( mulGrp ↾ Ring ) Fn Ring )
4 1 2 3 mp2an ( mulGrp ↾ Ring ) Fn Ring
5 fvres ( 𝑎 ∈ Ring → ( ( mulGrp ↾ Ring ) ‘ 𝑎 ) = ( mulGrp ‘ 𝑎 ) )
6 eqid ( mulGrp ‘ 𝑎 ) = ( mulGrp ‘ 𝑎 )
7 6 ringmgp ( 𝑎 ∈ Ring → ( mulGrp ‘ 𝑎 ) ∈ Mnd )
8 5 7 eqeltrd ( 𝑎 ∈ Ring → ( ( mulGrp ↾ Ring ) ‘ 𝑎 ) ∈ Mnd )
9 8 rgen 𝑎 ∈ Ring ( ( mulGrp ↾ Ring ) ‘ 𝑎 ) ∈ Mnd
10 ffnfv ( ( mulGrp ↾ Ring ) : Ring ⟶ Mnd ↔ ( ( mulGrp ↾ Ring ) Fn Ring ∧ ∀ 𝑎 ∈ Ring ( ( mulGrp ↾ Ring ) ‘ 𝑎 ) ∈ Mnd ) )
11 4 9 10 mpbir2an ( mulGrp ↾ Ring ) : Ring ⟶ Mnd