isirred

Description: An irreducible element of a ring is a non-unit that is not the product of two non-units. (Contributed by Mario Carneiro, 4-Dec-2014)

	Ref	Expression
Hypotheses	irred.1	$⊢ B = {Base}_{R}$
	irred.2	$⊢ U = Unit (R)$
	irred.3	$⊢ I = Irred (R)$
	irred.4	$⊢ N = B ∖ U$
	irred.5	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
Assertion	isirred	$⊢ X \in I \leftrightarrow (X \in N \land \forall x \in N \forall y \in N x \underset{˙}{\cdot} y \neq X)$

Proof

Step	Hyp	Ref	Expression
1		irred.1	$⊢ B = {Base}_{R}$
2		irred.2	$⊢ U = Unit (R)$
3		irred.3	$⊢ I = Irred (R)$
4		irred.4	$⊢ N = B ∖ U$
5		irred.5	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
6		elfvdm	$⊢ X \in Irred (R) \to R \in dom Irred$
7	6 3	eleq2s	$⊢ X \in I \to R \in dom Irred$
8	7	elexd	$⊢ X \in I \to R \in V$
9		eldifi	$⊢ X \in (B ∖ U) \to X \in B$
10	9 4	eleq2s	$⊢ X \in N \to X \in B$
11	10 1	eleqtrdi	$⊢ X \in N \to X \in {Base}_{R}$
12	11	elfvexd	$⊢ X \in N \to R \in V$
13	12	adantr	$⊢ (X \in N \land \forall x \in N \forall y \in N x \underset{˙}{\cdot} y \neq X) \to R \in V$
14		fvex	$⊢ {Base}_{r} \in V$
15		difexg	$⊢ {Base}_{r} \in V \to {Base}_{r} ∖ Unit (r) \in V$
16	14 15	mp1i	$⊢ r = R \to {Base}_{r} ∖ Unit (r) \in V$
17		simpr	$⊢ (r = R \land b = {Base}_{r} ∖ Unit (r)) \to b = {Base}_{r} ∖ Unit (r)$
18		simpl	$⊢ (r = R \land b = {Base}_{r} ∖ Unit (r)) \to r = R$
19	18	fveq2d	$⊢ (r = R \land b = {Base}_{r} ∖ Unit (r)) \to {Base}_{r} = {Base}_{R}$
20	19 1	eqtr4di	$⊢ (r = R \land b = {Base}_{r} ∖ Unit (r)) \to {Base}_{r} = B$
21	18	fveq2d	$⊢ (r = R \land b = {Base}_{r} ∖ Unit (r)) \to Unit (r) = Unit (R)$
22	21 2	eqtr4di	$⊢ (r = R \land b = {Base}_{r} ∖ Unit (r)) \to Unit (r) = U$
23	20 22	difeq12d	$⊢ (r = R \land b = {Base}_{r} ∖ Unit (r)) \to {Base}_{r} ∖ Unit (r) = B ∖ U$
24	23 4	eqtr4di	$⊢ (r = R \land b = {Base}_{r} ∖ Unit (r)) \to {Base}_{r} ∖ Unit (r) = N$
25	17 24	eqtrd	$⊢ (r = R \land b = {Base}_{r} ∖ Unit (r)) \to b = N$
26	18	fveq2d	$⊢ (r = R \land b = {Base}_{r} ∖ Unit (r)) \to \cdot_{r} = \cdot_{R}$
27	26 5	eqtr4di	$⊢ (r = R \land b = {Base}_{r} ∖ Unit (r)) \to \cdot_{r} = \underset{˙}{\cdot}$
28	27	oveqd	$⊢ (r = R \land b = {Base}_{r} ∖ Unit (r)) \to x \cdot_{r} y = x \underset{˙}{\cdot} y$
29	28	neeq1d	$⊢ (r = R \land b = {Base}_{r} ∖ Unit (r)) \to (x \cdot_{r} y \neq z \leftrightarrow x \underset{˙}{\cdot} y \neq z)$
30	25 29	raleqbidv	$⊢ (r = R \land b = {Base}_{r} ∖ Unit (r)) \to (\forall y \in b x \cdot_{r} y \neq z \leftrightarrow \forall y \in N x \underset{˙}{\cdot} y \neq z)$
31	25 30	raleqbidv	$⊢ (r = R \land b = {Base}_{r} ∖ Unit (r)) \to (\forall x \in b \forall y \in b x \cdot_{r} y \neq z \leftrightarrow \forall x \in N \forall y \in N x \underset{˙}{\cdot} y \neq z)$
32	25 31	rabeqbidv	$⊢ (r = R \land b = {Base}_{r} ∖ Unit (r)) \to \{z \in b \| \forall x \in b \forall y \in b x \cdot_{r} y \neq z\} = \{z \in N \| \forall x \in N \forall y \in N x \underset{˙}{\cdot} y \neq z\}$
33	16 32	csbied	$⊢ r = R \to ⦋ ({Base}_{r} ∖ Unit (r)) / b ⦌ \{z \in b \| \forall x \in b \forall y \in b x \cdot_{r} y \neq z\} = \{z \in N \| \forall x \in N \forall y \in N x \underset{˙}{\cdot} y \neq z\}$
34		df-irred	$⊢ Irred = (r \in V ⟼ ⦋ ({Base}_{r} ∖ Unit (r)) / b ⦌ \{z \in b \| \forall x \in b \forall y \in b x \cdot_{r} y \neq z\})$
35		fvex	$⊢ {Base}_{R} \in V$
36	1 35	eqeltri	$⊢ B \in V$
37	36	difexi	$⊢ B ∖ U \in V$
38	4 37	eqeltri	$⊢ N \in V$
39	38	rabex	$⊢ \{z \in N \| \forall x \in N \forall y \in N x \underset{˙}{\cdot} y \neq z\} \in V$
40	33 34 39	fvmpt	$⊢ R \in V \to Irred (R) = \{z \in N \| \forall x \in N \forall y \in N x \underset{˙}{\cdot} y \neq z\}$
41	3 40	eqtrid	$⊢ R \in V \to I = \{z \in N \| \forall x \in N \forall y \in N x \underset{˙}{\cdot} y \neq z\}$
42	41	eleq2d	$⊢ R \in V \to (X \in I \leftrightarrow X \in \{z \in N \| \forall x \in N \forall y \in N x \underset{˙}{\cdot} y \neq z\})$
43		neeq2	$⊢ z = X \to (x \underset{˙}{\cdot} y \neq z \leftrightarrow x \underset{˙}{\cdot} y \neq X)$
44	43	2ralbidv	$⊢ z = X \to (\forall x \in N \forall y \in N x \underset{˙}{\cdot} y \neq z \leftrightarrow \forall x \in N \forall y \in N x \underset{˙}{\cdot} y \neq X)$
45	44	elrab	$⊢ X \in \{z \in N \| \forall x \in N \forall y \in N x \underset{˙}{\cdot} y \neq z\} \leftrightarrow (X \in N \land \forall x \in N \forall y \in N x \underset{˙}{\cdot} y \neq X)$
46	42 45	bitrdi	$⊢ R \in V \to (X \in I \leftrightarrow (X \in N \land \forall x \in N \forall y \in N x \underset{˙}{\cdot} y \neq X))$
47	8 13 46	pm5.21nii	$⊢ X \in I \leftrightarrow (X \in N \land \forall x \in N \forall y \in N x \underset{˙}{\cdot} y \neq X)$

Metamath Proof Explorer

Theorem isirred

Proof