Theorem irredcl

Description: An irreducible element is in the ring. (Contributed by Mario Carneiro, 4-Dec-2014)

	Ref	Expression
Hypotheses	irredn0.i	|- I = ( Irred ` R )
	irredcl.b	|- B = ( Base ` R )
Assertion	irredcl	|- ( X e. I -> X e. B )

Proof

Step	Hyp	Ref	Expression
1		irredn0.i	|- I = ( Irred ` R )
2		irredcl.b	|- B = ( Base ` R )
3		eqid	|- ( Unit ` R ) = ( Unit ` R )
4		eqid	|- ( .r ` R ) = ( .r ` R )
5	2 3 1 4	isirred2	|- ( X e. I <-> ( X e. B /\ -. X e. ( Unit ` R ) /\ A. x e. B A. y e. B ( ( x ( .r ` R ) y ) = X -> ( x e. ( Unit ` R ) \/ y e. ( Unit ` R ) ) ) ) )
6	5	simp1bi	|- ( X e. I -> X e. B )