Theorem rngqipbas

Description: The base set of the product of the quotient with a two-sided ideal and the two-sided ideal is the cartesian product of the base set of the quotient and the base set of the two-sided ideal. (Contributed by AV, 21-Feb-2025)

	Ref	Expression
Hypotheses	rng2idlring.r	|- ( ph -> R e. Rng )
	rng2idlring.i	|- ( ph -> I e. ( 2Ideal ` R ) )
	rng2idlring.j	|- J = ( R |`s I )
	rng2idlring.u	|- ( ph -> J e. Ring )
	rng2idlring.b	|- B = ( Base ` R )
	rng2idlring.t	|- .x. = ( .r ` R )
	rng2idlring.1	|- .1. = ( 1r ` J )
	rngqiprngim.g	|- .~ = ( R ~QG I )
	rngqiprngim.q	|- Q = ( R /s .~ )
	rngqiprngim.c	|- C = ( Base ` Q )
	rngqiprngim.p	|- P = ( Q Xs. J )
Assertion	rngqipbas	|- ( ph -> ( Base ` P ) = ( C X. I ) )

Proof

Step	Hyp	Ref	Expression
1		rng2idlring.r	|- ( ph -> R e. Rng )
2		rng2idlring.i	|- ( ph -> I e. ( 2Ideal ` R ) )
3		rng2idlring.j	|- J = ( R |`s I )
4		rng2idlring.u	|- ( ph -> J e. Ring )
5		rng2idlring.b	|- B = ( Base ` R )
6		rng2idlring.t	|- .x. = ( .r ` R )
7		rng2idlring.1	|- .1. = ( 1r ` J )
8		rngqiprngim.g	|- .~ = ( R ~QG I )
9		rngqiprngim.q	|- Q = ( R /s .~ )
10		rngqiprngim.c	|- C = ( Base ` Q )
11		rngqiprngim.p	|- P = ( Q Xs. J )
12		eqid	|- ( Base ` J ) = ( Base ` J )
13	9	ovexi	|- Q e. _V
14	13	a1i	|- ( ph -> Q e. _V )
15	11 10 12 14 4	xpsbas	|- ( ph -> ( C X. ( Base ` J ) ) = ( Base ` P ) )
16	2 3 12	2idlbas	|- ( ph -> ( Base ` J ) = I )
17	16	xpeq2d	|- ( ph -> ( C X. ( Base ` J ) ) = ( C X. I ) )
18	15 17	eqtr3d	|- ( ph -> ( Base ` P ) = ( C X. I ) )