irredn0

Description: The additive identity is not irreducible. (Contributed by Mario Carneiro, 4-Dec-2014)

	Ref	Expression
Hypotheses	irredn0.i	$⊢ I = Irred (R)$
	irredn0.z	$⊢ \underset{˙}{0} = 0_{R}$
Assertion	irredn0	$⊢ (R \in Ring \land X \in I) \to X \neq \underset{˙}{0}$

Proof

Step	Hyp	Ref	Expression
1		irredn0.i	$⊢ I = Irred (R)$
2		irredn0.z	$⊢ \underset{˙}{0} = 0_{R}$
3		eqid	$⊢ {Base}_{R} = {Base}_{R}$
4	3 2	ring0cl	$⊢ R \in Ring \to \underset{˙}{0} \in {Base}_{R}$
5	4	anim1i	$⊢ (R \in Ring \land \neg \underset{˙}{0} \in Unit (R)) \to (\underset{˙}{0} \in {Base}_{R} \land \neg \underset{˙}{0} \in Unit (R))$
6		eldif	$⊢ \underset{˙}{0} \in ({Base}_{R} ∖ Unit (R)) \leftrightarrow (\underset{˙}{0} \in {Base}_{R} \land \neg \underset{˙}{0} \in Unit (R))$
7	5 6	sylibr	$⊢ (R \in Ring \land \neg \underset{˙}{0} \in Unit (R)) \to \underset{˙}{0} \in ({Base}_{R} ∖ Unit (R))$
8		eqid	$⊢ \cdot_{R} = \cdot_{R}$
9	3 8 2	ringlz	$⊢ (R \in Ring \land \underset{˙}{0} \in {Base}_{R}) \to \underset{˙}{0} \cdot_{R} \underset{˙}{0} = \underset{˙}{0}$
10	4 9	mpdan	$⊢ R \in Ring \to \underset{˙}{0} \cdot_{R} \underset{˙}{0} = \underset{˙}{0}$
11	10	adantr	$⊢ (R \in Ring \land \neg \underset{˙}{0} \in Unit (R)) \to \underset{˙}{0} \cdot_{R} \underset{˙}{0} = \underset{˙}{0}$
12		oveq1	$⊢ x = \underset{˙}{0} \to x \cdot_{R} y = \underset{˙}{0} \cdot_{R} y$
13	12	eqeq1d	$⊢ x = \underset{˙}{0} \to (x \cdot_{R} y = \underset{˙}{0} \leftrightarrow \underset{˙}{0} \cdot_{R} y = \underset{˙}{0})$
14		oveq2	$⊢ y = \underset{˙}{0} \to \underset{˙}{0} \cdot_{R} y = \underset{˙}{0} \cdot_{R} \underset{˙}{0}$
15	14	eqeq1d	$⊢ y = \underset{˙}{0} \to (\underset{˙}{0} \cdot_{R} y = \underset{˙}{0} \leftrightarrow \underset{˙}{0} \cdot_{R} \underset{˙}{0} = \underset{˙}{0})$
16	13 15	rspc2ev	$⊢ (\underset{˙}{0} \in ({Base}_{R} ∖ Unit (R)) \land \underset{˙}{0} \in ({Base}_{R} ∖ Unit (R)) \land \underset{˙}{0} \cdot_{R} \underset{˙}{0} = \underset{˙}{0}) \to \exists x \in ({Base}_{R} ∖ Unit (R)) \exists y \in ({Base}_{R} ∖ Unit (R)) x \cdot_{R} y = \underset{˙}{0}$
17	7 7 11 16	syl3anc	$⊢ (R \in Ring \land \neg \underset{˙}{0} \in Unit (R)) \to \exists x \in ({Base}_{R} ∖ Unit (R)) \exists y \in ({Base}_{R} ∖ Unit (R)) x \cdot_{R} y = \underset{˙}{0}$
18	17	ex	$⊢ R \in Ring \to (\neg \underset{˙}{0} \in Unit (R) \to \exists x \in ({Base}_{R} ∖ Unit (R)) \exists y \in ({Base}_{R} ∖ Unit (R)) x \cdot_{R} y = \underset{˙}{0})$
19	18	orrd	$⊢ R \in Ring \to (\underset{˙}{0} \in Unit (R) \lor \exists x \in ({Base}_{R} ∖ Unit (R)) \exists y \in ({Base}_{R} ∖ Unit (R)) x \cdot_{R} y = \underset{˙}{0})$
20		eqid	$⊢ Unit (R) = Unit (R)$
21		eqid	$⊢ {Base}_{R} ∖ Unit (R) = {Base}_{R} ∖ Unit (R)$
22	3 20 1 21 8	isnirred	$⊢ \underset{˙}{0} \in {Base}_{R} \to (\neg \underset{˙}{0} \in I \leftrightarrow (\underset{˙}{0} \in Unit (R) \lor \exists x \in ({Base}_{R} ∖ Unit (R)) \exists y \in ({Base}_{R} ∖ Unit (R)) x \cdot_{R} y = \underset{˙}{0}))$
23	4 22	syl	$⊢ R \in Ring \to (\neg \underset{˙}{0} \in I \leftrightarrow (\underset{˙}{0} \in Unit (R) \lor \exists x \in ({Base}_{R} ∖ Unit (R)) \exists y \in ({Base}_{R} ∖ Unit (R)) x \cdot_{R} y = \underset{˙}{0}))$
24	19 23	mpbird	$⊢ R \in Ring \to \neg \underset{˙}{0} \in I$
25	24	adantr	$⊢ (R \in Ring \land X \in I) \to \neg \underset{˙}{0} \in I$
26		simpr	$⊢ (R \in Ring \land X \in I) \to X \in I$
27		eleq1	$⊢ X = \underset{˙}{0} \to (X \in I \leftrightarrow \underset{˙}{0} \in I)$
28	26 27	syl5ibcom	$⊢ (R \in Ring \land X \in I) \to (X = \underset{˙}{0} \to \underset{˙}{0} \in I)$
29	28	necon3bd	$⊢ (R \in Ring \land X \in I) \to (\neg \underset{˙}{0} \in I \to X \neq \underset{˙}{0})$
30	25 29	mpd	$⊢ (R \in Ring \land X \in I) \to X \neq \underset{˙}{0}$

Metamath Proof Explorer

Theorem irredn0

Proof