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