Theorem lpigen

Description: An ideal is principal iff it contains an element which right-divides all elements. (Contributed by Stefan O'Rear, 3-Jan-2015) (Revised by Wolf Lammen, 6-Sep-2020)

	Ref	Expression
Hypotheses	lpigen.u	|- U = ( LIdeal ` R )
	lpigen.p	|- P = ( LPIdeal ` R )
	lpigen.d	|- .|| = ( ||r ` R )
Assertion	lpigen	|- ( ( R e. Ring /\ I e. U ) -> ( I e. P <-> E. x e. I A. y e. I x .|| y ) )

Proof

Step	Hyp	Ref	Expression
1		lpigen.u	|- U = ( LIdeal ` R )
2		lpigen.p	|- P = ( LPIdeal ` R )
3		lpigen.d	|- .|| = ( ||r ` R )
4		eqid	|- ( RSpan ` R ) = ( RSpan ` R )
5		eqid	|- ( Base ` R ) = ( Base ` R )
6	2 4 5	islpidl	|- ( R e. Ring -> ( I e. P <-> E. x e. ( Base ` R ) I = ( ( RSpan ` R ) ` { x } ) ) )
7	6	adantr	|- ( ( R e. Ring /\ I e. U ) -> ( I e. P <-> E. x e. ( Base ` R ) I = ( ( RSpan ` R ) ` { x } ) ) )
8	5 1 4 3	lidldvgen	|- ( ( R e. Ring /\ I e. U /\ x e. ( Base ` R ) ) -> ( I = ( ( RSpan ` R ) ` { x } ) <-> ( x e. I /\ A. y e. I x .|| y ) ) )
9	8	3expa	|- ( ( ( R e. Ring /\ I e. U ) /\ x e. ( Base ` R ) ) -> ( I = ( ( RSpan ` R ) ` { x } ) <-> ( x e. I /\ A. y e. I x .|| y ) ) )
10	9	rexbidva	|- ( ( R e. Ring /\ I e. U ) -> ( E. x e. ( Base ` R ) I = ( ( RSpan ` R ) ` { x } ) <-> E. x e. ( Base ` R ) ( x e. I /\ A. y e. I x .|| y ) ) )
11		simpr	|- ( ( x e. ( Base ` R ) /\ ( x e. I /\ A. y e. I x .|| y ) ) -> ( x e. I /\ A. y e. I x .|| y ) )
12	5 1	lidlss	|- ( I e. U -> I C_ ( Base ` R ) )
13	12	adantl	|- ( ( R e. Ring /\ I e. U ) -> I C_ ( Base ` R ) )
14	13	sseld	|- ( ( R e. Ring /\ I e. U ) -> ( x e. I -> x e. ( Base ` R ) ) )
15	14	adantrd	|- ( ( R e. Ring /\ I e. U ) -> ( ( x e. I /\ A. y e. I x .|| y ) -> x e. ( Base ` R ) ) )
16	15	ancrd	|- ( ( R e. Ring /\ I e. U ) -> ( ( x e. I /\ A. y e. I x .|| y ) -> ( x e. ( Base ` R ) /\ ( x e. I /\ A. y e. I x .|| y ) ) ) )
17	11 16	impbid2	|- ( ( R e. Ring /\ I e. U ) -> ( ( x e. ( Base ` R ) /\ ( x e. I /\ A. y e. I x .|| y ) ) <-> ( x e. I /\ A. y e. I x .|| y ) ) )
18	17	rexbidv2	|- ( ( R e. Ring /\ I e. U ) -> ( E. x e. ( Base ` R ) ( x e. I /\ A. y e. I x .|| y ) <-> E. x e. I A. y e. I x .|| y ) )
19	7 10 18	3bitrd	|- ( ( R e. Ring /\ I e. U ) -> ( I e. P <-> E. x e. I A. y e. I x .|| y ) )