Theorem irredmul

Description: If product of two elements is irreducible, then one of the elements must be a unit. (Contributed by Mario Carneiro, 4-Dec-2014)

	Ref	Expression
Hypotheses	irredn0.i	$$⊢I=\mathrm{Irred}\left(R\right)$$
	irredmul.b	$$⊢B={\mathrm{Base}}_R$$
	irredmul.u	$$⊢U=\mathrm{Unit}\left(R\right)$$
	irredmul.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
Assertion	irredmul	$$⊢\left(X\in B\wedge Y\in B\wedge X\underset{\dot{}}{·}Y\in I\right)\to \left(X\in U\vee Y\in U\right)$$

Proof

Step	Hyp	Ref	Expression
1		irredn0.i	$$⊢I=\mathrm{Irred}\left(R\right)$$
2		irredmul.b	$$⊢B={\mathrm{Base}}_R$$
3		irredmul.u	$$⊢U=\mathrm{Unit}\left(R\right)$$
4		irredmul.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
5	2 3 1 4	isirred2	$$⊢X\underset{\dot{}}{·}Y\in I\leftrightarrow \left(X\underset{\dot{}}{·}Y\in B\wedge \neg X\underset{\dot{}}{·}Y\in U\wedge \forall x\in B\forall y\in B\left(x\underset{\dot{}}{·}y=X\underset{\dot{}}{·}Y\to \left(x\in U\vee y\in U\right)\right)\right)$$
6	5	simp3bi	$$⊢X\underset{\dot{}}{·}Y\in I\to \forall x\in B\forall y\in B\left(x\underset{\dot{}}{·}y=X\underset{\dot{}}{·}Y\to \left(x\in U\vee y\in U\right)\right)$$
7		eqid	$$⊢X\underset{\dot{}}{·}Y=X\underset{\dot{}}{·}Y$$
8		oveq1	$$⊢x=X\to x\underset{\dot{}}{·}y=X\underset{\dot{}}{·}y$$
9	8	eqeq1d	$$⊢x=X\to \left(x\underset{\dot{}}{·}y=X\underset{\dot{}}{·}Y\leftrightarrow X\underset{\dot{}}{·}y=X\underset{\dot{}}{·}Y\right)$$
10		eleq1	$$⊢x=X\to \left(x\in U\leftrightarrow X\in U\right)$$
11	10	orbi1d	$$⊢x=X\to \left(\left(x\in U\vee y\in U\right)\leftrightarrow \left(X\in U\vee y\in U\right)\right)$$
12	9 11	imbi12d	$$⊢x=X\to \left(\left(x\underset{\dot{}}{·}y=X\underset{\dot{}}{·}Y\to \left(x\in U\vee y\in U\right)\right)\leftrightarrow \left(X\underset{\dot{}}{·}y=X\underset{\dot{}}{·}Y\to \left(X\in U\vee y\in U\right)\right)\right)$$
13		oveq2	$$⊢y=Y\to X\underset{\dot{}}{·}y=X\underset{\dot{}}{·}Y$$
14	13	eqeq1d	$$⊢y=Y\to \left(X\underset{\dot{}}{·}y=X\underset{\dot{}}{·}Y\leftrightarrow X\underset{\dot{}}{·}Y=X\underset{\dot{}}{·}Y\right)$$
15		eleq1	$$⊢y=Y\to \left(y\in U\leftrightarrow Y\in U\right)$$
16	15	orbi2d	$$⊢y=Y\to \left(\left(X\in U\vee y\in U\right)\leftrightarrow \left(X\in U\vee Y\in U\right)\right)$$
17	14 16	imbi12d	$$⊢y=Y\to \left(\left(X\underset{\dot{}}{·}y=X\underset{\dot{}}{·}Y\to \left(X\in U\vee y\in U\right)\right)\leftrightarrow \left(X\underset{\dot{}}{·}Y=X\underset{\dot{}}{·}Y\to \left(X\in U\vee Y\in U\right)\right)\right)$$
18	12 17	rspc2v	$$⊢\left(X\in B\wedge Y\in B\right)\to \left(\forall x\in B\forall y\in B\left(x\underset{\dot{}}{·}y=X\underset{\dot{}}{·}Y\to \left(x\in U\vee y\in U\right)\right)\to \left(X\underset{\dot{}}{·}Y=X\underset{\dot{}}{·}Y\to \left(X\in U\vee Y\in U\right)\right)\right)$$
19	7 18	mpii	$$⊢\left(X\in B\wedge Y\in B\right)\to \left(\forall x\in B\forall y\in B\left(x\underset{\dot{}}{·}y=X\underset{\dot{}}{·}Y\to \left(x\in U\vee y\in U\right)\right)\to \left(X\in U\vee Y\in U\right)\right)$$
20	6 19	syl5	$$⊢\left(X\in B\wedge Y\in B\right)\to \left(X\underset{\dot{}}{·}Y\in I\to \left(X\in U\vee Y\in U\right)\right)$$
21	20	3impia	$$⊢\left(X\in B\wedge Y\in B\wedge X\underset{\dot{}}{·}Y\in I\right)\to \left(X\in U\vee Y\in U\right)$$