Theorem invrpropd

Description: The ring inverse function depends only on the ring's base set and multiplication operation. (Contributed by Mario Carneiro, 26-Dec-2014) (Revised by Mario Carneiro, 5-Oct-2015)

	Ref	Expression
Hypotheses	rngidpropd.1	$$⊢\phi \to B={\mathrm{Base}}_K$$
	rngidpropd.2	$$⊢\phi \to B={\mathrm{Base}}_L$$
	rngidpropd.3	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to x{\cdot }_{K}y=x{\cdot }_{L}y$$
Assertion	invrpropd	$$⊢\phi \to {inv}_r\left(K\right)={inv}_r\left(L\right)$$

Proof

Step	Hyp	Ref	Expression
1		rngidpropd.1	$$⊢\phi \to B={\mathrm{Base}}_K$$
2		rngidpropd.2	$$⊢\phi \to B={\mathrm{Base}}_L$$
3		rngidpropd.3	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to x{\cdot }_{K}y=x{\cdot }_{L}y$$
4		eqid	$$⊢\mathrm{Unit}\left(K\right)=\mathrm{Unit}\left(K\right)$$
5		eqid	$$⊢{\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}\mathrm{Unit}\left(K\right)={\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}\mathrm{Unit}\left(K\right)$$
6	4 5	unitgrpbas	$$⊢\mathrm{Unit}\left(K\right)={\mathrm{Base}}_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}\mathrm{Unit}\left(K\right)\right)}$$
7	6	a1i	$$⊢\phi \to \mathrm{Unit}\left(K\right)={\mathrm{Base}}_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}\mathrm{Unit}\left(K\right)\right)}$$
8	1 2 3	unitpropd	$$⊢\phi \to \mathrm{Unit}\left(K\right)=\mathrm{Unit}\left(L\right)$$
9		eqid	$$⊢\mathrm{Unit}\left(L\right)=\mathrm{Unit}\left(L\right)$$
10		eqid	$$⊢{\mathrm{mulGrp}}_L{\upharpoonright }_{𝑠}\mathrm{Unit}\left(L\right)={\mathrm{mulGrp}}_L{\upharpoonright }_{𝑠}\mathrm{Unit}\left(L\right)$$
11	9 10	unitgrpbas	$$⊢\mathrm{Unit}\left(L\right)={\mathrm{Base}}_{\left({\mathrm{mulGrp}}_L{\upharpoonright }_{𝑠}\mathrm{Unit}\left(L\right)\right)}$$
12	8 11	eqtrdi	$$⊢\phi \to \mathrm{Unit}\left(K\right)={\mathrm{Base}}_{\left({\mathrm{mulGrp}}_L{\upharpoonright }_{𝑠}\mathrm{Unit}\left(L\right)\right)}$$
13		eqid	$$⊢{\mathrm{Base}}_K={\mathrm{Base}}_K$$
14	13 4	unitss	$$⊢\mathrm{Unit}\left(K\right)\subseteq {\mathrm{Base}}_K$$
15	14 1	sseqtrrid	$$⊢\phi \to \mathrm{Unit}\left(K\right)\subseteq B$$
16	15	sselda	$$⊢\left(\phi \wedge x\in \mathrm{Unit}\left(K\right)\right)\to x\in B$$
17	15	sselda	$$⊢\left(\phi \wedge y\in \mathrm{Unit}\left(K\right)\right)\to y\in B$$
18	16 17	anim12dan	$$⊢\left(\phi \wedge \left(x\in \mathrm{Unit}\left(K\right)\wedge y\in \mathrm{Unit}\left(K\right)\right)\right)\to \left(x\in B\wedge y\in B\right)$$
19	18 3	syldan	$$⊢\left(\phi \wedge \left(x\in \mathrm{Unit}\left(K\right)\wedge y\in \mathrm{Unit}\left(K\right)\right)\right)\to x{\cdot }_{K}y=x{\cdot }_{L}y$$
20		fvex	$$⊢\mathrm{Unit}\left(K\right)\in \mathrm{V}$$
21		eqid	$$⊢{\mathrm{mulGrp}}_K={\mathrm{mulGrp}}_K$$
22		eqid	$$⊢{\cdot }_K={\cdot }_K$$
23	21 22	mgpplusg	$$⊢{\cdot }_K={+}_{{\mathrm{mulGrp}}_K}$$
24	5 23	ressplusg	$$⊢\mathrm{Unit}\left(K\right)\in \mathrm{V}\to {\cdot }_K={+}_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}\mathrm{Unit}\left(K\right)\right)}$$
25	20 24	ax-mp	$$⊢{\cdot }_K={+}_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}\mathrm{Unit}\left(K\right)\right)}$$
26	25	oveqi	$$⊢x{\cdot }_{K}y=x{+}_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}\mathrm{Unit}\left(K\right)\right)}y$$
27		fvex	$$⊢\mathrm{Unit}\left(L\right)\in \mathrm{V}$$
28		eqid	$$⊢{\mathrm{mulGrp}}_L={\mathrm{mulGrp}}_L$$
29		eqid	$$⊢{\cdot }_L={\cdot }_L$$
30	28 29	mgpplusg	$$⊢{\cdot }_L={+}_{{\mathrm{mulGrp}}_L}$$
31	10 30	ressplusg	$$⊢\mathrm{Unit}\left(L\right)\in \mathrm{V}\to {\cdot }_L={+}_{\left({\mathrm{mulGrp}}_L{\upharpoonright }_{𝑠}\mathrm{Unit}\left(L\right)\right)}$$
32	27 31	ax-mp	$$⊢{\cdot }_L={+}_{\left({\mathrm{mulGrp}}_L{\upharpoonright }_{𝑠}\mathrm{Unit}\left(L\right)\right)}$$
33	32	oveqi	$$⊢x{\cdot }_{L}y=x{+}_{\left({\mathrm{mulGrp}}_L{\upharpoonright }_{𝑠}\mathrm{Unit}\left(L\right)\right)}y$$
34	19 26 33	3eqtr3g	$$⊢\left(\phi \wedge \left(x\in \mathrm{Unit}\left(K\right)\wedge y\in \mathrm{Unit}\left(K\right)\right)\right)\to x{+}_{\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}\mathrm{Unit}\left(K\right)\right)}y=x{+}_{\left({\mathrm{mulGrp}}_L{\upharpoonright }_{𝑠}\mathrm{Unit}\left(L\right)\right)}y$$
35	7 12 34	grpinvpropd	$$⊢\phi \to {inv}_g\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}\mathrm{Unit}\left(K\right)\right)={inv}_g\left({\mathrm{mulGrp}}_L{\upharpoonright }_{𝑠}\mathrm{Unit}\left(L\right)\right)$$
36		eqid	$$⊢{inv}_r\left(K\right)={inv}_r\left(K\right)$$
37	4 5 36	invrfval	$$⊢{inv}_r\left(K\right)={inv}_g\left({\mathrm{mulGrp}}_K{\upharpoonright }_{𝑠}\mathrm{Unit}\left(K\right)\right)$$
38		eqid	$$⊢{inv}_r\left(L\right)={inv}_r\left(L\right)$$
39	9 10 38	invrfval	$$⊢{inv}_r\left(L\right)={inv}_g\left({\mathrm{mulGrp}}_L{\upharpoonright }_{𝑠}\mathrm{Unit}\left(L\right)\right)$$
40	35 37 39	3eqtr4g	$$⊢\phi \to {inv}_r\left(K\right)={inv}_r\left(L\right)$$