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