opprirred

Description: Irreducibility is symmetric, so the irreducible elements of the opposite ring are the same as the original ring. (Contributed by Mario Carneiro, 4-Dec-2014)

	Ref	Expression
Hypotheses	opprirred.1	$⊢ S = {opp}_{r} (R)$
	opprirred.2	$⊢ I = Irred (R)$
Assertion	opprirred	$⊢ I = Irred (S)$

Proof

Step	Hyp	Ref	Expression
1		opprirred.1	$⊢ S = {opp}_{r} (R)$
2		opprirred.2	$⊢ I = Irred (R)$
3		ralcom	$⊢ \forall z \in ({Base}_{R} ∖ Unit (R)) \forall y \in ({Base}_{R} ∖ Unit (R)) z \cdot_{R} y \neq x \leftrightarrow \forall y \in ({Base}_{R} ∖ Unit (R)) \forall z \in ({Base}_{R} ∖ Unit (R)) z \cdot_{R} y \neq x$
4		eqid	$⊢ {Base}_{R} = {Base}_{R}$
5		eqid	$⊢ \cdot_{R} = \cdot_{R}$
6		eqid	$⊢ \cdot_{S} = \cdot_{S}$
7	4 5 1 6	opprmul	$⊢ y \cdot_{S} z = z \cdot_{R} y$
8	7	neeq1i	$⊢ y \cdot_{S} z \neq x \leftrightarrow z \cdot_{R} y \neq x$
9	8	2ralbii	$⊢ \forall y \in ({Base}_{R} ∖ Unit (R)) \forall z \in ({Base}_{R} ∖ Unit (R)) y \cdot_{S} z \neq x \leftrightarrow \forall y \in ({Base}_{R} ∖ Unit (R)) \forall z \in ({Base}_{R} ∖ Unit (R)) z \cdot_{R} y \neq x$
10	3 9	bitr4i	$⊢ \forall z \in ({Base}_{R} ∖ Unit (R)) \forall y \in ({Base}_{R} ∖ Unit (R)) z \cdot_{R} y \neq x \leftrightarrow \forall y \in ({Base}_{R} ∖ Unit (R)) \forall z \in ({Base}_{R} ∖ Unit (R)) y \cdot_{S} z \neq x$
11	10	anbi2i	$⊢ (x \in ({Base}_{R} ∖ Unit (R)) \land \forall z \in ({Base}_{R} ∖ Unit (R)) \forall y \in ({Base}_{R} ∖ Unit (R)) z \cdot_{R} y \neq x) \leftrightarrow (x \in ({Base}_{R} ∖ Unit (R)) \land \forall y \in ({Base}_{R} ∖ Unit (R)) \forall z \in ({Base}_{R} ∖ Unit (R)) y \cdot_{S} z \neq x)$
12		eqid	$⊢ Unit (R) = Unit (R)$
13		eqid	$⊢ {Base}_{R} ∖ Unit (R) = {Base}_{R} ∖ Unit (R)$
14	4 12 2 13 5	isirred	$⊢ x \in I \leftrightarrow (x \in ({Base}_{R} ∖ Unit (R)) \land \forall z \in ({Base}_{R} ∖ Unit (R)) \forall y \in ({Base}_{R} ∖ Unit (R)) z \cdot_{R} y \neq x)$
15	1 4	opprbas	$⊢ {Base}_{R} = {Base}_{S}$
16	12 1	opprunit	$⊢ Unit (R) = Unit (S)$
17		eqid	$⊢ Irred (S) = Irred (S)$
18	15 16 17 13 6	isirred	$⊢ x \in Irred (S) \leftrightarrow (x \in ({Base}_{R} ∖ Unit (R)) \land \forall y \in ({Base}_{R} ∖ Unit (R)) \forall z \in ({Base}_{R} ∖ Unit (R)) y \cdot_{S} z \neq x)$
19	11 14 18	3bitr4i	$⊢ x \in I \leftrightarrow x \in Irred (S)$
20	19	eqriv	$⊢ I = Irred (S)$

Metamath Proof Explorer

Theorem opprirred

Proof