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