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	Could not format assertion : No typesetting found for |- ( mulGrp |` Rng ) : Rng --> Smgrp with typecode |-

Proof

Step	Hyp	Ref	Expression
1		fnmgp	$$⊢\mathrm{mulGrp}Fn\mathrm{V}$$
2		ssv	$$⊢\mathrm{Rng}\subseteq \mathrm{V}$$
3		fnssres	$$⊢\left(\mathrm{mulGrp}Fn\mathrm{V}\wedge \mathrm{Rng}\subseteq \mathrm{V}\right)\to \left({\mathrm{mulGrp}\upharpoonright }_{\mathrm{Rng}}\right)Fn\mathrm{Rng}$$
4	1 2 3	mp2an	$$⊢\left({\mathrm{mulGrp}\upharpoonright }_{\mathrm{Rng}}\right)Fn\mathrm{Rng}$$
5		fvres	$$⊢a\in \mathrm{Rng}\to \left({\mathrm{mulGrp}\upharpoonright }_{\mathrm{Rng}}\right)\left(a\right)={\mathrm{mulGrp}}_a$$
6		eqid	$$⊢{\mathrm{mulGrp}}_a={\mathrm{mulGrp}}_a$$
7	6	rngmgp	Could not format ( a e. Rng -> ( mulGrp ` a ) e. Smgrp ) : No typesetting found for |- ( a e. Rng -> ( mulGrp ` a ) e. Smgrp ) with typecode |-
8	5 7	eqeltrd	Could not format ( a e. Rng -> ( ( mulGrp |` Rng ) ` a ) e. Smgrp ) : No typesetting found for |- ( a e. Rng -> ( ( mulGrp |` Rng ) ` a ) e. Smgrp ) with typecode |-
9	8	rgen	Could not format A. a e. Rng ( ( mulGrp |` Rng ) ` a ) e. Smgrp : No typesetting found for |- A. a e. Rng ( ( mulGrp |` Rng ) ` a ) e. Smgrp with typecode |-
10		ffnfv	Could not format ( ( mulGrp |` Rng ) : Rng --> Smgrp <-> ( ( mulGrp |` Rng ) Fn Rng /\ A. a e. Rng ( ( mulGrp |` Rng ) ` a ) e. Smgrp ) ) : No typesetting found for |- ( ( mulGrp |` Rng ) : Rng --> Smgrp <-> ( ( mulGrp |` Rng ) Fn Rng /\ A. a e. Rng ( ( mulGrp |` Rng ) ` a ) e. Smgrp ) ) with typecode |-
11	4 9 10	mpbir2an	Could not format ( mulGrp |` Rng ) : Rng --> Smgrp : No typesetting found for |- ( mulGrp |` Rng ) : Rng --> Smgrp with typecode |-