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 = ( Base ` R )
Assertion	isdrng3lem0	|- ( Base ` ( ( mulGrp ` R ) |`s ( B \ X ) ) ) = ( B \ X )

Proof

Step	Hyp	Ref	Expression
1		isdrng3.b	|- B = ( Base ` R )
2		difss	|- ( B \ X ) C_ B
3		eqid	|- ( ( mulGrp ` R ) |`s ( B \ X ) ) = ( ( mulGrp ` R ) |`s ( B \ X ) )
4		eqid	|- ( mulGrp ` R ) = ( mulGrp ` R )
5	4 1	mgpbas	|- B = ( Base ` ( mulGrp ` R ) )
6	3 5	ressbas2	|- ( ( B \ X ) C_ B -> ( B \ X ) = ( Base ` ( ( mulGrp ` R ) |`s ( B \ X ) ) ) )
7	6	eqcomd	|- ( ( B \ X ) C_ B -> ( Base ` ( ( mulGrp ` R ) |`s ( B \ X ) ) ) = ( B \ X ) )
8	2 7	ax-mp	|- ( Base ` ( ( mulGrp ` R ) |`s ( B \ X ) ) ) = ( B \ X )