Theorem isdrng3lem0

Description: Lemma for isdrng3 : The base set of a multipication group restricted to a subset of the original base set. (Contributed by AV, 22-Jul-2026)

	Ref	Expression
Hypothesis	isdrng3.b	$$⊢B={\mathrm{Base}}_R$$
Assertion	isdrng3lem0	$$⊢{\mathrm{Base}}_{\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left(B\setminus X\right)\right)}=B\setminus X$$

Proof

Step	Hyp	Ref	Expression
1		isdrng3.b	$$⊢B={\mathrm{Base}}_R$$
2		difss	$$⊢B\setminus X\subseteq B$$
3		eqid	$$⊢{\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left(B\setminus X\right)={\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left(B\setminus X\right)$$
4		eqid	$$⊢{\mathrm{mulGrp}}_R={\mathrm{mulGrp}}_R$$
5	4 1	mgpbas	$$⊢B={\mathrm{Base}}_{{\mathrm{mulGrp}}_R}$$
6	3 5	ressbas2	$$⊢B\setminus X\subseteq B\to B\setminus X={\mathrm{Base}}_{\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left(B\setminus X\right)\right)}$$
7	6	eqcomd	$$⊢B\setminus X\subseteq B\to {\mathrm{Base}}_{\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left(B\setminus X\right)\right)}=B\setminus X$$
8	2 7	ax-mp	$$⊢{\mathrm{Base}}_{\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left(B\setminus X\right)\right)}=B\setminus X$$