This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )