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	$$⊢\phi \to R\in \mathrm{Rng}$$
	rng2idlring.i	$$⊢\phi \to I\in \mathrm{2Ideal}\left(R\right)$$
	rng2idlring.j	$$⊢J=R{\upharpoonright }_{𝑠}I$$
	rng2idlring.u	$$⊢\phi \to J\in \mathrm{Ring}$$
	rng2idlring.b	$$⊢B={\mathrm{Base}}_R$$
	rng2idlring.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	rng2idlring.1	$$⊢\underset{\dot{}}{1}=1_J$$
	rngqiprngim.g	$$⊢\underset{\dot{}}{\sim }=R{~}_{\mathit{QG}}I$$
	rngqiprngim.q	$$⊢Q=R{/}_{𝑠}\underset{\dot{}}{\sim }$$
	rngqiprngim.c	$$⊢C={\mathrm{Base}}_Q$$
	rngqiprngim.p	$$⊢P=Q{\times }_{𝑠}J$$
Assertion	rngqipbas	$$⊢\phi \to {\mathrm{Base}}_P=C\times I$$

Proof

Step	Hyp	Ref	Expression
1		rng2idlring.r	$$⊢\phi \to R\in \mathrm{Rng}$$
2		rng2idlring.i	$$⊢\phi \to I\in \mathrm{2Ideal}\left(R\right)$$
3		rng2idlring.j	$$⊢J=R{\upharpoonright }_{𝑠}I$$
4		rng2idlring.u	$$⊢\phi \to J\in \mathrm{Ring}$$
5		rng2idlring.b	$$⊢B={\mathrm{Base}}_R$$
6		rng2idlring.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
7		rng2idlring.1	$$⊢\underset{\dot{}}{1}=1_J$$
8		rngqiprngim.g	$$⊢\underset{\dot{}}{\sim }=R{~}_{\mathit{QG}}I$$
9		rngqiprngim.q	$$⊢Q=R{/}_{𝑠}\underset{\dot{}}{\sim }$$
10		rngqiprngim.c	$$⊢C={\mathrm{Base}}_Q$$
11		rngqiprngim.p	$$⊢P=Q{\times }_{𝑠}J$$
12		eqid	$$⊢{\mathrm{Base}}_J={\mathrm{Base}}_J$$
13	9	ovexi	$$⊢Q\in \mathrm{V}$$
14	13	a1i	$$⊢\phi \to Q\in \mathrm{V}$$
15	11 10 12 14 4	xpsbas	$$⊢\phi \to C\times {\mathrm{Base}}_J={\mathrm{Base}}_P$$
16	2 3 12	2idlbas	$$⊢\phi \to {\mathrm{Base}}_J=I$$
17	16	xpeq2d	$$⊢\phi \to C\times {\mathrm{Base}}_J=C\times I$$
18	15 17	eqtr3d	$$⊢\phi \to {\mathrm{Base}}_P=C\times I$$