Metamath Proof Explorer

Theorem lidldvgen

Description: An element generates an ideal iff it is contained in the ideal and all elements are right-divided by it. (Contributed by Stefan O'Rear, 3-Jan-2015)

Ref Expression
Hypotheses lidldvgen.b 
|- B = ( Base ` R )
lidldvgen.u 
|- U = ( LIdeal ` R )
lidldvgen.k 
|- K = ( RSpan ` R )
lidldvgen.d 
|- .|| = ( ||r ` R )
Assertion lidldvgen 
|- ( ( R e. Ring /\ I e. U /\ G e. B ) -> ( I = ( K ` { G } ) <-> ( G e. I /\ A. x e. I G .|| x ) ) )

Proof

Step Hyp Ref Expression
1 lidldvgen.b 
 |-  B = ( Base ` R )
2 lidldvgen.u 
 |-  U = ( LIdeal ` R )
3 lidldvgen.k 
 |-  K = ( RSpan ` R )
4 lidldvgen.d 
 |-  .|| = ( ||r ` R )
5 simp1 
 |-  ( ( R e. Ring /\ I e. U /\ G e. B ) -> R e. Ring )
6 simp3 
 |-  ( ( R e. Ring /\ I e. U /\ G e. B ) -> G e. B )
7 6 snssd 
 |-  ( ( R e. Ring /\ I e. U /\ G e. B ) -> { G } C_ B )
8 3 1 rspssid 
 |-  ( ( R e. Ring /\ { G } C_ B ) -> { G } C_ ( K ` { G } ) )
9 5 7 8 syl2anc 
 |-  ( ( R e. Ring /\ I e. U /\ G e. B ) -> { G } C_ ( K ` { G } ) )
10 snssg 
 |-  ( G e. B -> ( G e. ( K ` { G } ) <-> { G } C_ ( K ` { G } ) ) )
11 10 3ad2ant3 
 |-  ( ( R e. Ring /\ I e. U /\ G e. B ) -> ( G e. ( K ` { G } ) <-> { G } C_ ( K ` { G } ) ) )
12 9 11 mpbird 
 |-  ( ( R e. Ring /\ I e. U /\ G e. B ) -> G e. ( K ` { G } ) )
13 1 3 4 rspsn 
 |-  ( ( R e. Ring /\ G e. B ) -> ( K ` { G } ) = { y | G .|| y } )
14 13 3adant2 
 |-  ( ( R e. Ring /\ I e. U /\ G e. B ) -> ( K ` { G } ) = { y | G .|| y } )
15 14 eleq2d 
 |-  ( ( R e. Ring /\ I e. U /\ G e. B ) -> ( x e. ( K ` { G } ) <-> x e. { y | G .|| y } ) )
16 vex 
 |-  x e. _V
17 breq2 
 |-  ( y = x -> ( G .|| y <-> G .|| x ) )
18 16 17 elab 
 |-  ( x e. { y | G .|| y } <-> G .|| x )
19 15 18 bitrdi 
 |-  ( ( R e. Ring /\ I e. U /\ G e. B ) -> ( x e. ( K ` { G } ) <-> G .|| x ) )
20 19 biimpd 
 |-  ( ( R e. Ring /\ I e. U /\ G e. B ) -> ( x e. ( K ` { G } ) -> G .|| x ) )
21 20 ralrimiv 
 |-  ( ( R e. Ring /\ I e. U /\ G e. B ) -> A. x e. ( K ` { G } ) G .|| x )
22 12 21 jca 
 |-  ( ( R e. Ring /\ I e. U /\ G e. B ) -> ( G e. ( K ` { G } ) /\ A. x e. ( K ` { G } ) G .|| x ) )
23 eleq2 
 |-  ( I = ( K ` { G } ) -> ( G e. I <-> G e. ( K ` { G } ) ) )
24 raleq 
 |-  ( I = ( K ` { G } ) -> ( A. x e. I G .|| x <-> A. x e. ( K ` { G } ) G .|| x ) )
25 23 24 anbi12d 
 |-  ( I = ( K ` { G } ) -> ( ( G e. I /\ A. x e. I G .|| x ) <-> ( G e. ( K ` { G } ) /\ A. x e. ( K ` { G } ) G .|| x ) ) )
26 22 25 syl5ibrcom 
 |-  ( ( R e. Ring /\ I e. U /\ G e. B ) -> ( I = ( K ` { G } ) -> ( G e. I /\ A. x e. I G .|| x ) ) )
27 df-ral 
 |-  ( A. x e. I G .|| x <-> A. x ( x e. I -> G .|| x ) )
28 ssab 
 |-  ( I C_ { x | G .|| x } <-> A. x ( x e. I -> G .|| x ) )
29 27 28 sylbb2 
 |-  ( A. x e. I G .|| x -> I C_ { x | G .|| x } )
30 29 ad2antll 
 |-  ( ( ( R e. Ring /\ I e. U /\ G e. B ) /\ ( G e. I /\ A. x e. I G .|| x ) ) -> I C_ { x | G .|| x } )
31 1 3 4 rspsn 
 |-  ( ( R e. Ring /\ G e. B ) -> ( K ` { G } ) = { x | G .|| x } )
32 31 3adant2 
 |-  ( ( R e. Ring /\ I e. U /\ G e. B ) -> ( K ` { G } ) = { x | G .|| x } )
33 32 adantr 
 |-  ( ( ( R e. Ring /\ I e. U /\ G e. B ) /\ ( G e. I /\ A. x e. I G .|| x ) ) -> ( K ` { G } ) = { x | G .|| x } )
34 30 33 sseqtrrd 
 |-  ( ( ( R e. Ring /\ I e. U /\ G e. B ) /\ ( G e. I /\ A. x e. I G .|| x ) ) -> I C_ ( K ` { G } ) )
35 simpl1 
 |-  ( ( ( R e. Ring /\ I e. U /\ G e. B ) /\ G e. I ) -> R e. Ring )
36 simpl2 
 |-  ( ( ( R e. Ring /\ I e. U /\ G e. B ) /\ G e. I ) -> I e. U )
37 snssi 
 |-  ( G e. I -> { G } C_ I )
38 37 adantl 
 |-  ( ( ( R e. Ring /\ I e. U /\ G e. B ) /\ G e. I ) -> { G } C_ I )
39 3 2 rspssp 
 |-  ( ( R e. Ring /\ I e. U /\ { G } C_ I ) -> ( K ` { G } ) C_ I )
40 35 36 38 39 syl3anc 
 |-  ( ( ( R e. Ring /\ I e. U /\ G e. B ) /\ G e. I ) -> ( K ` { G } ) C_ I )
41 40 adantrr 
 |-  ( ( ( R e. Ring /\ I e. U /\ G e. B ) /\ ( G e. I /\ A. x e. I G .|| x ) ) -> ( K ` { G } ) C_ I )
42 34 41 eqssd 
 |-  ( ( ( R e. Ring /\ I e. U /\ G e. B ) /\ ( G e. I /\ A. x e. I G .|| x ) ) -> I = ( K ` { G } ) )
43 42 ex 
 |-  ( ( R e. Ring /\ I e. U /\ G e. B ) -> ( ( G e. I /\ A. x e. I G .|| x ) -> I = ( K ` { G } ) ) )
44 26 43 impbid 
 |-  ( ( R e. Ring /\ I e. U /\ G e. B ) -> ( I = ( K ` { G } ) <-> ( G e. I /\ A. x e. I G .|| x ) ) )