Theorem mgpf

Description: Restricted functionality of the multiplicative group on rings. (Contributed by Mario Carneiro, 11-Mar-2015)

	Ref	Expression
Assertion	mgpf	$$⊢\left({\mathrm{mulGrp}\upharpoonright }_{\mathrm{Ring}}\right):\mathrm{Ring}⟶\mathrm{Mnd}$$

Proof

Step	Hyp	Ref	Expression
1		fnmgp	$$⊢\mathrm{mulGrp}Fn\mathrm{V}$$
2		ssv	$$⊢\mathrm{Ring}\subseteq \mathrm{V}$$
3		fnssres	$$⊢\left(\mathrm{mulGrp}Fn\mathrm{V}\wedge \mathrm{Ring}\subseteq \mathrm{V}\right)\to \left({\mathrm{mulGrp}\upharpoonright }_{\mathrm{Ring}}\right)Fn\mathrm{Ring}$$
4	1 2 3	mp2an	$$⊢\left({\mathrm{mulGrp}\upharpoonright }_{\mathrm{Ring}}\right)Fn\mathrm{Ring}$$
5		fvres	$$⊢a\in \mathrm{Ring}\to \left({\mathrm{mulGrp}\upharpoonright }_{\mathrm{Ring}}\right)\left(a\right)={\mathrm{mulGrp}}_a$$
6		eqid	$$⊢{\mathrm{mulGrp}}_a={\mathrm{mulGrp}}_a$$
7	6	ringmgp	$$⊢a\in \mathrm{Ring}\to {\mathrm{mulGrp}}_a\in \mathrm{Mnd}$$
8	5 7	eqeltrd	$$⊢a\in \mathrm{Ring}\to \left({\mathrm{mulGrp}\upharpoonright }_{\mathrm{Ring}}\right)\left(a\right)\in \mathrm{Mnd}$$
9	8	rgen	$$⊢\forall a\in \mathrm{Ring}\left({\mathrm{mulGrp}\upharpoonright }_{\mathrm{Ring}}\right)\left(a\right)\in \mathrm{Mnd}$$
10		ffnfv	$$⊢\left({\mathrm{mulGrp}\upharpoonright }_{\mathrm{Ring}}\right):\mathrm{Ring}⟶\mathrm{Mnd}\leftrightarrow \left(\left({\mathrm{mulGrp}\upharpoonright }_{\mathrm{Ring}}\right)Fn\mathrm{Ring}\wedge \forall a\in \mathrm{Ring}\left({\mathrm{mulGrp}\upharpoonright }_{\mathrm{Ring}}\right)\left(a\right)\in \mathrm{Mnd}\right)$$
11	4 9 10	mpbir2an	$$⊢\left({\mathrm{mulGrp}\upharpoonright }_{\mathrm{Ring}}\right):\mathrm{Ring}⟶\mathrm{Mnd}$$