Theorem ringinvval

Description: The ring inverse expressed in terms of multiplication. (Contributed by Thierry Arnoux, 23-Oct-2017)

	Ref	Expression
Hypotheses	ringinvval.b	$$⊢B={\mathrm{Base}}_R$$
	ringinvval.p	$$⊢\underset{\dot{}}{\ast }={\cdot }_R$$
	ringinvval.o	$$⊢\underset{\dot{}}{1}=1_R$$
	ringinvval.n	$$⊢N={inv}_r\left(R\right)$$
	ringinvval.u	$$⊢U=\mathrm{Unit}\left(R\right)$$
Assertion	ringinvval	$$⊢\left(R\in \mathrm{Ring}\wedge X\in U\right)\to N\left(X\right)=\left(\iota y\in U|y\underset{\dot{}}{\ast }X=\underset{\dot{}}{1}\right)$$

Proof

Step	Hyp	Ref	Expression
1		ringinvval.b	$$⊢B={\mathrm{Base}}_R$$
2		ringinvval.p	$$⊢\underset{\dot{}}{\ast }={\cdot }_R$$
3		ringinvval.o	$$⊢\underset{\dot{}}{1}=1_R$$
4		ringinvval.n	$$⊢N={inv}_r\left(R\right)$$
5		ringinvval.u	$$⊢U=\mathrm{Unit}\left(R\right)$$
6		eqid	$$⊢{\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}U={\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}U$$
7	5 6	unitgrpbas	$$⊢U={\mathrm{Base}}_{\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}U\right)}$$
8	5	fvexi	$$⊢U\in \mathrm{V}$$
9		eqid	$$⊢{\mathrm{mulGrp}}_R={\mathrm{mulGrp}}_R$$
10	9 2	mgpplusg	$$⊢\underset{\dot{}}{\ast }={+}_{{\mathrm{mulGrp}}_R}$$
11	6 10	ressplusg	$$⊢U\in \mathrm{V}\to \underset{\dot{}}{\ast }={+}_{\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}U\right)}$$
12	8 11	ax-mp	$$⊢\underset{\dot{}}{\ast }={+}_{\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}U\right)}$$
13		eqid	$$⊢0_{\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}U\right)}=0_{\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}U\right)}$$
14	5 6 4	invrfval	$$⊢N={inv}_g\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}U\right)$$
15	7 12 13 14	grpinvval	$$⊢X\in U\to N\left(X\right)=\left(\iota y\in U|y\underset{\dot{}}{\ast }X=0_{\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}U\right)}\right)$$
16	15	adantl	$$⊢\left(R\in \mathrm{Ring}\wedge X\in U\right)\to N\left(X\right)=\left(\iota y\in U|y\underset{\dot{}}{\ast }X=0_{\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}U\right)}\right)$$
17	5 6 3	unitgrpid	$$⊢R\in \mathrm{Ring}\to \underset{\dot{}}{1}=0_{\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}U\right)}$$
18	17	adantr	$$⊢\left(R\in \mathrm{Ring}\wedge y\in U\right)\to \underset{\dot{}}{1}=0_{\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}U\right)}$$
19	18	eqeq2d	$$⊢\left(R\in \mathrm{Ring}\wedge y\in U\right)\to \left(y\underset{\dot{}}{\ast }X=\underset{\dot{}}{1}\leftrightarrow y\underset{\dot{}}{\ast }X=0_{\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}U\right)}\right)$$
20	19	riotabidva	$$⊢R\in \mathrm{Ring}\to \left(\iota y\in U|y\underset{\dot{}}{\ast }X=\underset{\dot{}}{1}\right)=\left(\iota y\in U|y\underset{\dot{}}{\ast }X=0_{\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}U\right)}\right)$$
21	20	adantr	$$⊢\left(R\in \mathrm{Ring}\wedge X\in U\right)\to \left(\iota y\in U|y\underset{\dot{}}{\ast }X=\underset{\dot{}}{1}\right)=\left(\iota y\in U|y\underset{\dot{}}{\ast }X=0_{\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}U\right)}\right)$$
22	16 21	eqtr4d	$$⊢\left(R\in \mathrm{Ring}\wedge X\in U\right)\to N\left(X\right)=\left(\iota y\in U|y\underset{\dot{}}{\ast }X=\underset{\dot{}}{1}\right)$$