irredrmul

Description: The product of an irreducible element and a unit is irreducible. (Contributed by Mario Carneiro, 4-Dec-2014)

	Ref	Expression
Hypotheses	irredn0.i	$⊢ I = Irred (R)$
	irredrmul.u	$⊢ U = Unit (R)$
	irredrmul.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
Assertion	irredrmul	$⊢ (R \in Ring \land X \in I \land Y \in U) \to X \underset{˙}{\cdot} Y \in I$

Proof

Step	Hyp	Ref	Expression
1		irredn0.i	$⊢ I = Irred (R)$
2		irredrmul.u	$⊢ U = Unit (R)$
3		irredrmul.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
4		simp2	$⊢ (R \in Ring \land X \in I \land Y \in U) \to X \in I$
5		simp1	$⊢ (R \in Ring \land X \in I \land Y \in U) \to R \in Ring$
6		simp3	$⊢ (R \in Ring \land X \in I \land Y \in U) \to Y \in U$
7		eqid	$⊢ /_{r} (R) = /_{r} (R)$
8	2 7	unitdvcl	$⊢ (R \in Ring \land X \underset{˙}{\cdot} Y \in U \land Y \in U) \to (X \underset{˙}{\cdot} Y) /_{r} (R) Y \in U$
9	8	3com23	$⊢ (R \in Ring \land Y \in U \land X \underset{˙}{\cdot} Y \in U) \to (X \underset{˙}{\cdot} Y) /_{r} (R) Y \in U$
10	9	3expia	$⊢ (R \in Ring \land Y \in U) \to (X \underset{˙}{\cdot} Y \in U \to (X \underset{˙}{\cdot} Y) /_{r} (R) Y \in U)$
11	5 6 10	syl2anc	$⊢ (R \in Ring \land X \in I \land Y \in U) \to (X \underset{˙}{\cdot} Y \in U \to (X \underset{˙}{\cdot} Y) /_{r} (R) Y \in U)$
12		eqid	$⊢ {Base}_{R} = {Base}_{R}$
13	1 12	irredcl	$⊢ X \in I \to X \in {Base}_{R}$
14	13	3ad2ant2	$⊢ (R \in Ring \land X \in I \land Y \in U) \to X \in {Base}_{R}$
15	12 2 7 3	dvrcan3	$⊢ (R \in Ring \land X \in {Base}_{R} \land Y \in U) \to (X \underset{˙}{\cdot} Y) /_{r} (R) Y = X$
16	5 14 6 15	syl3anc	$⊢ (R \in Ring \land X \in I \land Y \in U) \to (X \underset{˙}{\cdot} Y) /_{r} (R) Y = X$
17	16	eleq1d	$⊢ (R \in Ring \land X \in I \land Y \in U) \to ((X \underset{˙}{\cdot} Y) /_{r} (R) Y \in U \leftrightarrow X \in U)$
18	11 17	sylibd	$⊢ (R \in Ring \land X \in I \land Y \in U) \to (X \underset{˙}{\cdot} Y \in U \to X \in U)$
19	5	ad2antrr	$⊢ (((R \in Ring \land X \in I \land Y \in U) \land x \in ({Base}_{R} ∖ U)) \land (y \in ({Base}_{R} ∖ U) \land x \underset{˙}{\cdot} y = X \underset{˙}{\cdot} Y)) \to R \in Ring$
20		eldifi	$⊢ y \in ({Base}_{R} ∖ U) \to y \in {Base}_{R}$
21	20	ad2antrl	$⊢ (((R \in Ring \land X \in I \land Y \in U) \land x \in ({Base}_{R} ∖ U)) \land (y \in ({Base}_{R} ∖ U) \land x \underset{˙}{\cdot} y = X \underset{˙}{\cdot} Y)) \to y \in {Base}_{R}$
22	6	ad2antrr	$⊢ (((R \in Ring \land X \in I \land Y \in U) \land x \in ({Base}_{R} ∖ U)) \land (y \in ({Base}_{R} ∖ U) \land x \underset{˙}{\cdot} y = X \underset{˙}{\cdot} Y)) \to Y \in U$
23	12 2 7	dvrcl	$⊢ (R \in Ring \land y \in {Base}_{R} \land Y \in U) \to y /_{r} (R) Y \in {Base}_{R}$
24	19 21 22 23	syl3anc	$⊢ (((R \in Ring \land X \in I \land Y \in U) \land x \in ({Base}_{R} ∖ U)) \land (y \in ({Base}_{R} ∖ U) \land x \underset{˙}{\cdot} y = X \underset{˙}{\cdot} Y)) \to y /_{r} (R) Y \in {Base}_{R}$
25		eldifn	$⊢ y \in ({Base}_{R} ∖ U) \to \neg y \in U$
26	25	ad2antrl	$⊢ (((R \in Ring \land X \in I \land Y \in U) \land x \in ({Base}_{R} ∖ U)) \land (y \in ({Base}_{R} ∖ U) \land x \underset{˙}{\cdot} y = X \underset{˙}{\cdot} Y)) \to \neg y \in U$
27	2 3	unitmulcl	$⊢ (R \in Ring \land y /_{r} (R) Y \in U \land Y \in U) \to (y /_{r} (R) Y) \underset{˙}{\cdot} Y \in U$
28	27	3com23	$⊢ (R \in Ring \land Y \in U \land y /_{r} (R) Y \in U) \to (y /_{r} (R) Y) \underset{˙}{\cdot} Y \in U$
29	28	3expia	$⊢ (R \in Ring \land Y \in U) \to (y /_{r} (R) Y \in U \to (y /_{r} (R) Y) \underset{˙}{\cdot} Y \in U)$
30	19 22 29	syl2anc	$⊢ (((R \in Ring \land X \in I \land Y \in U) \land x \in ({Base}_{R} ∖ U)) \land (y \in ({Base}_{R} ∖ U) \land x \underset{˙}{\cdot} y = X \underset{˙}{\cdot} Y)) \to (y /_{r} (R) Y \in U \to (y /_{r} (R) Y) \underset{˙}{\cdot} Y \in U)$
31	12 2 7 3	dvrcan1	$⊢ (R \in Ring \land y \in {Base}_{R} \land Y \in U) \to (y /_{r} (R) Y) \underset{˙}{\cdot} Y = y$
32	19 21 22 31	syl3anc	$⊢ (((R \in Ring \land X \in I \land Y \in U) \land x \in ({Base}_{R} ∖ U)) \land (y \in ({Base}_{R} ∖ U) \land x \underset{˙}{\cdot} y = X \underset{˙}{\cdot} Y)) \to (y /_{r} (R) Y) \underset{˙}{\cdot} Y = y$
33	32	eleq1d	$⊢ (((R \in Ring \land X \in I \land Y \in U) \land x \in ({Base}_{R} ∖ U)) \land (y \in ({Base}_{R} ∖ U) \land x \underset{˙}{\cdot} y = X \underset{˙}{\cdot} Y)) \to ((y /_{r} (R) Y) \underset{˙}{\cdot} Y \in U \leftrightarrow y \in U)$
34	30 33	sylibd	$⊢ (((R \in Ring \land X \in I \land Y \in U) \land x \in ({Base}_{R} ∖ U)) \land (y \in ({Base}_{R} ∖ U) \land x \underset{˙}{\cdot} y = X \underset{˙}{\cdot} Y)) \to (y /_{r} (R) Y \in U \to y \in U)$
35	26 34	mtod	$⊢ (((R \in Ring \land X \in I \land Y \in U) \land x \in ({Base}_{R} ∖ U)) \land (y \in ({Base}_{R} ∖ U) \land x \underset{˙}{\cdot} y = X \underset{˙}{\cdot} Y)) \to \neg y /_{r} (R) Y \in U$
36	24 35	eldifd	$⊢ (((R \in Ring \land X \in I \land Y \in U) \land x \in ({Base}_{R} ∖ U)) \land (y \in ({Base}_{R} ∖ U) \land x \underset{˙}{\cdot} y = X \underset{˙}{\cdot} Y)) \to y /_{r} (R) Y \in ({Base}_{R} ∖ U)$
37		simprr	$⊢ (((R \in Ring \land X \in I \land Y \in U) \land x \in ({Base}_{R} ∖ U)) \land (y \in ({Base}_{R} ∖ U) \land x \underset{˙}{\cdot} y = X \underset{˙}{\cdot} Y)) \to x \underset{˙}{\cdot} y = X \underset{˙}{\cdot} Y$
38	37	oveq1d	$⊢ (((R \in Ring \land X \in I \land Y \in U) \land x \in ({Base}_{R} ∖ U)) \land (y \in ({Base}_{R} ∖ U) \land x \underset{˙}{\cdot} y = X \underset{˙}{\cdot} Y)) \to (x \underset{˙}{\cdot} y) /_{r} (R) Y = (X \underset{˙}{\cdot} Y) /_{r} (R) Y$
39		eldifi	$⊢ x \in ({Base}_{R} ∖ U) \to x \in {Base}_{R}$
40	39	ad2antlr	$⊢ (((R \in Ring \land X \in I \land Y \in U) \land x \in ({Base}_{R} ∖ U)) \land (y \in ({Base}_{R} ∖ U) \land x \underset{˙}{\cdot} y = X \underset{˙}{\cdot} Y)) \to x \in {Base}_{R}$
41	12 2 7 3	dvrass	$⊢ (R \in Ring \land (x \in {Base}_{R} \land y \in {Base}_{R} \land Y \in U)) \to (x \underset{˙}{\cdot} y) /_{r} (R) Y = x \underset{˙}{\cdot} (y /_{r} (R) Y)$
42	19 40 21 22 41	syl13anc	$⊢ (((R \in Ring \land X \in I \land Y \in U) \land x \in ({Base}_{R} ∖ U)) \land (y \in ({Base}_{R} ∖ U) \land x \underset{˙}{\cdot} y = X \underset{˙}{\cdot} Y)) \to (x \underset{˙}{\cdot} y) /_{r} (R) Y = x \underset{˙}{\cdot} (y /_{r} (R) Y)$
43	16	ad2antrr	$⊢ (((R \in Ring \land X \in I \land Y \in U) \land x \in ({Base}_{R} ∖ U)) \land (y \in ({Base}_{R} ∖ U) \land x \underset{˙}{\cdot} y = X \underset{˙}{\cdot} Y)) \to (X \underset{˙}{\cdot} Y) /_{r} (R) Y = X$
44	38 42 43	3eqtr3d	$⊢ (((R \in Ring \land X \in I \land Y \in U) \land x \in ({Base}_{R} ∖ U)) \land (y \in ({Base}_{R} ∖ U) \land x \underset{˙}{\cdot} y = X \underset{˙}{\cdot} Y)) \to x \underset{˙}{\cdot} (y /_{r} (R) Y) = X$
45		oveq2	$⊢ z = y /_{r} (R) Y \to x \underset{˙}{\cdot} z = x \underset{˙}{\cdot} (y /_{r} (R) Y)$
46	45	eqeq1d	$⊢ z = y /_{r} (R) Y \to (x \underset{˙}{\cdot} z = X \leftrightarrow x \underset{˙}{\cdot} (y /_{r} (R) Y) = X)$
47	46	rspcev	$⊢ (y /_{r} (R) Y \in ({Base}_{R} ∖ U) \land x \underset{˙}{\cdot} (y /_{r} (R) Y) = X) \to \exists z \in ({Base}_{R} ∖ U) x \underset{˙}{\cdot} z = X$
48	36 44 47	syl2anc	$⊢ (((R \in Ring \land X \in I \land Y \in U) \land x \in ({Base}_{R} ∖ U)) \land (y \in ({Base}_{R} ∖ U) \land x \underset{˙}{\cdot} y = X \underset{˙}{\cdot} Y)) \to \exists z \in ({Base}_{R} ∖ U) x \underset{˙}{\cdot} z = X$
49	48	rexlimdvaa	$⊢ ((R \in Ring \land X \in I \land Y \in U) \land x \in ({Base}_{R} ∖ U)) \to (\exists y \in ({Base}_{R} ∖ U) x \underset{˙}{\cdot} y = X \underset{˙}{\cdot} Y \to \exists z \in ({Base}_{R} ∖ U) x \underset{˙}{\cdot} z = X)$
50	49	reximdva	$⊢ (R \in Ring \land X \in I \land Y \in U) \to (\exists x \in ({Base}_{R} ∖ U) \exists y \in ({Base}_{R} ∖ U) x \underset{˙}{\cdot} y = X \underset{˙}{\cdot} Y \to \exists x \in ({Base}_{R} ∖ U) \exists z \in ({Base}_{R} ∖ U) x \underset{˙}{\cdot} z = X)$
51	18 50	orim12d	$⊢ (R \in Ring \land X \in I \land Y \in U) \to ((X \underset{˙}{\cdot} Y \in U \lor \exists x \in ({Base}_{R} ∖ U) \exists y \in ({Base}_{R} ∖ U) x \underset{˙}{\cdot} y = X \underset{˙}{\cdot} Y) \to (X \in U \lor \exists x \in ({Base}_{R} ∖ U) \exists z \in ({Base}_{R} ∖ U) x \underset{˙}{\cdot} z = X))$
52	12 2	unitcl	$⊢ Y \in U \to Y \in {Base}_{R}$
53	52	3ad2ant3	$⊢ (R \in Ring \land X \in I \land Y \in U) \to Y \in {Base}_{R}$
54	12 3	ringcl	$⊢ (R \in Ring \land X \in {Base}_{R} \land Y \in {Base}_{R}) \to X \underset{˙}{\cdot} Y \in {Base}_{R}$
55	5 14 53 54	syl3anc	$⊢ (R \in Ring \land X \in I \land Y \in U) \to X \underset{˙}{\cdot} Y \in {Base}_{R}$
56		eqid	$⊢ {Base}_{R} ∖ U = {Base}_{R} ∖ U$
57	12 2 1 56 3	isnirred	$⊢ X \underset{˙}{\cdot} Y \in {Base}_{R} \to (\neg X \underset{˙}{\cdot} Y \in I \leftrightarrow (X \underset{˙}{\cdot} Y \in U \lor \exists x \in ({Base}_{R} ∖ U) \exists y \in ({Base}_{R} ∖ U) x \underset{˙}{\cdot} y = X \underset{˙}{\cdot} Y))$
58	55 57	syl	$⊢ (R \in Ring \land X \in I \land Y \in U) \to (\neg X \underset{˙}{\cdot} Y \in I \leftrightarrow (X \underset{˙}{\cdot} Y \in U \lor \exists x \in ({Base}_{R} ∖ U) \exists y \in ({Base}_{R} ∖ U) x \underset{˙}{\cdot} y = X \underset{˙}{\cdot} Y))$
59	12 2 1 56 3	isnirred	$⊢ X \in {Base}_{R} \to (\neg X \in I \leftrightarrow (X \in U \lor \exists x \in ({Base}_{R} ∖ U) \exists z \in ({Base}_{R} ∖ U) x \underset{˙}{\cdot} z = X))$
60	14 59	syl	$⊢ (R \in Ring \land X \in I \land Y \in U) \to (\neg X \in I \leftrightarrow (X \in U \lor \exists x \in ({Base}_{R} ∖ U) \exists z \in ({Base}_{R} ∖ U) x \underset{˙}{\cdot} z = X))$
61	51 58 60	3imtr4d	$⊢ (R \in Ring \land X \in I \land Y \in U) \to (\neg X \underset{˙}{\cdot} Y \in I \to \neg X \in I)$
62	4 61	mt4d	$⊢ (R \in Ring \land X \in I \land Y \in U) \to X \underset{˙}{\cdot} Y \in I$

Metamath Proof Explorer

Theorem irredrmul

Proof