Theorem rprmdvds

Description: If a ring prime Q divides a product X .x. Y , then it divides either X or Y . (Contributed by Thierry Arnoux, 18-May-2025)

	Ref	Expression
Hypotheses	rprmdvds.b	$$⊢B={\mathrm{Base}}_R$$
	rprmdvds.p	$$⊢P=\mathrm{RPrime}\left(R\right)$$
	rprmdvds.d	$$⊢\underset{\dot{}}{\parallel }={\parallel }_r\left(R\right)$$
	rprmdvds.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	rprmdvds.r	$$⊢\phi \to R\in V$$
	rprmdvds.q	$$⊢\phi \to Q\in P$$
	rprmdvds.x	$$⊢\phi \to X\in B$$
	rprmdvds.y	$$⊢\phi \to Y\in B$$
	rprmdvds.1	$$⊢\phi \to Q\underset{\dot{}}{\parallel }\left(X\underset{\dot{}}{·}Y\right)$$
Assertion	rprmdvds	$$⊢\phi \to \left(Q\underset{\dot{}}{\parallel }X\vee Q\underset{\dot{}}{\parallel }Y\right)$$

Proof

Step	Hyp	Ref	Expression
1		rprmdvds.b	$$⊢B={\mathrm{Base}}_R$$
2		rprmdvds.p	$$⊢P=\mathrm{RPrime}\left(R\right)$$
3		rprmdvds.d	$$⊢\underset{\dot{}}{\parallel }={\parallel }_r\left(R\right)$$
4		rprmdvds.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
5		rprmdvds.r	$$⊢\phi \to R\in V$$
6		rprmdvds.q	$$⊢\phi \to Q\in P$$
7		rprmdvds.x	$$⊢\phi \to X\in B$$
8		rprmdvds.y	$$⊢\phi \to Y\in B$$
9		rprmdvds.1	$$⊢\phi \to Q\underset{\dot{}}{\parallel }\left(X\underset{\dot{}}{·}Y\right)$$
10		oveq1	$$⊢x=X\to x\underset{\dot{}}{·}y=X\underset{\dot{}}{·}y$$
11	10	breq2d	$$⊢x=X\to \left(Q\underset{\dot{}}{\parallel }\left(x\underset{\dot{}}{·}y\right)\leftrightarrow Q\underset{\dot{}}{\parallel }\left(X\underset{\dot{}}{·}y\right)\right)$$
12		breq2	$$⊢x=X\to \left(Q\underset{\dot{}}{\parallel }x\leftrightarrow Q\underset{\dot{}}{\parallel }X\right)$$
13	12	orbi1d	$$⊢x=X\to \left(\left(Q\underset{\dot{}}{\parallel }x\vee Q\underset{\dot{}}{\parallel }y\right)\leftrightarrow \left(Q\underset{\dot{}}{\parallel }X\vee Q\underset{\dot{}}{\parallel }y\right)\right)$$
14	11 13	imbi12d	$$⊢x=X\to \left(\left(Q\underset{\dot{}}{\parallel }\left(x\underset{\dot{}}{·}y\right)\to \left(Q\underset{\dot{}}{\parallel }x\vee Q\underset{\dot{}}{\parallel }y\right)\right)\leftrightarrow \left(Q\underset{\dot{}}{\parallel }\left(X\underset{\dot{}}{·}y\right)\to \left(Q\underset{\dot{}}{\parallel }X\vee Q\underset{\dot{}}{\parallel }y\right)\right)\right)$$
15		oveq2	$$⊢y=Y\to X\underset{\dot{}}{·}y=X\underset{\dot{}}{·}Y$$
16	15	breq2d	$$⊢y=Y\to \left(Q\underset{\dot{}}{\parallel }\left(X\underset{\dot{}}{·}y\right)\leftrightarrow Q\underset{\dot{}}{\parallel }\left(X\underset{\dot{}}{·}Y\right)\right)$$
17		breq2	$$⊢y=Y\to \left(Q\underset{\dot{}}{\parallel }y\leftrightarrow Q\underset{\dot{}}{\parallel }Y\right)$$
18	17	orbi2d	$$⊢y=Y\to \left(\left(Q\underset{\dot{}}{\parallel }X\vee Q\underset{\dot{}}{\parallel }y\right)\leftrightarrow \left(Q\underset{\dot{}}{\parallel }X\vee Q\underset{\dot{}}{\parallel }Y\right)\right)$$
19	16 18	imbi12d	$$⊢y=Y\to \left(\left(Q\underset{\dot{}}{\parallel }\left(X\underset{\dot{}}{·}y\right)\to \left(Q\underset{\dot{}}{\parallel }X\vee Q\underset{\dot{}}{\parallel }y\right)\right)\leftrightarrow \left(Q\underset{\dot{}}{\parallel }\left(X\underset{\dot{}}{·}Y\right)\to \left(Q\underset{\dot{}}{\parallel }X\vee Q\underset{\dot{}}{\parallel }Y\right)\right)\right)$$
20	6 2	eleqtrdi	$$⊢\phi \to Q\in \mathrm{RPrime}\left(R\right)$$
21		eqid	$$⊢\mathrm{Unit}\left(R\right)=\mathrm{Unit}\left(R\right)$$
22		eqid	$$⊢0_R=0_R$$
23	1 21 22 3 4	isrprm	$$⊢R\in V\to \left(Q\in \mathrm{RPrime}\left(R\right)\leftrightarrow \left(Q\in \left(B\setminus \left(\mathrm{Unit}\left(R\right)\cup \left\{0_R\right\}\right)\right)\wedge \forall x\in B\forall y\in B\left(Q\underset{\dot{}}{\parallel }\left(x\underset{\dot{}}{·}y\right)\to \left(Q\underset{\dot{}}{\parallel }x\vee Q\underset{\dot{}}{\parallel }y\right)\right)\right)\right)$$
24	23	simplbda	$$⊢\left(R\in V\wedge Q\in \mathrm{RPrime}\left(R\right)\right)\to \forall x\in B\forall y\in B\left(Q\underset{\dot{}}{\parallel }\left(x\underset{\dot{}}{·}y\right)\to \left(Q\underset{\dot{}}{\parallel }x\vee Q\underset{\dot{}}{\parallel }y\right)\right)$$
25	5 20 24	syl2anc	$$⊢\phi \to \forall x\in B\forall y\in B\left(Q\underset{\dot{}}{\parallel }\left(x\underset{\dot{}}{·}y\right)\to \left(Q\underset{\dot{}}{\parallel }x\vee Q\underset{\dot{}}{\parallel }y\right)\right)$$
26	14 19 25 7 8	rspc2dv	$$⊢\phi \to \left(Q\underset{\dot{}}{\parallel }\left(X\underset{\dot{}}{·}Y\right)\to \left(Q\underset{\dot{}}{\parallel }X\vee Q\underset{\dot{}}{\parallel }Y\right)\right)$$
27	9 26	mpd	$$⊢\phi \to \left(Q\underset{\dot{}}{\parallel }X\vee Q\underset{\dot{}}{\parallel }Y\right)$$