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

Metamath Proof Explorer

Theorem igenval2

Description: The ideal generated by a subset of a ring. (Contributed by Jeff Madsen, 10-Jun-2010)

Ref Expression
Hypotheses igenval2.1 
|- G = ( 1st ` R )
igenval2.2 
|- X = ran G
Assertion igenval2 
|- ( ( R e. RingOps /\ S C_ X ) -> ( ( R IdlGen S ) = I <-> ( I e. ( Idl ` R ) /\ S C_ I /\ A. j e. ( Idl ` R ) ( S C_ j -> I C_ j ) ) ) )

Proof

Step Hyp Ref Expression
1 igenval2.1 
 |-  G = ( 1st ` R )
2 igenval2.2 
 |-  X = ran G
3 1 2 igenidl 
 |-  ( ( R e. RingOps /\ S C_ X ) -> ( R IdlGen S ) e. ( Idl ` R ) )
4 1 2 igenss 
 |-  ( ( R e. RingOps /\ S C_ X ) -> S C_ ( R IdlGen S ) )
5 igenmin 
 |-  ( ( R e. RingOps /\ j e. ( Idl ` R ) /\ S C_ j ) -> ( R IdlGen S ) C_ j )
6 5 3expia 
 |-  ( ( R e. RingOps /\ j e. ( Idl ` R ) ) -> ( S C_ j -> ( R IdlGen S ) C_ j ) )
7 6 ralrimiva 
 |-  ( R e. RingOps -> A. j e. ( Idl ` R ) ( S C_ j -> ( R IdlGen S ) C_ j ) )
8 7 adantr 
 |-  ( ( R e. RingOps /\ S C_ X ) -> A. j e. ( Idl ` R ) ( S C_ j -> ( R IdlGen S ) C_ j ) )
9 3 4 8 3jca 
 |-  ( ( R e. RingOps /\ S C_ X ) -> ( ( R IdlGen S ) e. ( Idl ` R ) /\ S C_ ( R IdlGen S ) /\ A. j e. ( Idl ` R ) ( S C_ j -> ( R IdlGen S ) C_ j ) ) )
10 eleq1 
 |-  ( ( R IdlGen S ) = I -> ( ( R IdlGen S ) e. ( Idl ` R ) <-> I e. ( Idl ` R ) ) )
11 sseq2 
 |-  ( ( R IdlGen S ) = I -> ( S C_ ( R IdlGen S ) <-> S C_ I ) )
12 sseq1 
 |-  ( ( R IdlGen S ) = I -> ( ( R IdlGen S ) C_ j <-> I C_ j ) )
13 12 imbi2d 
 |-  ( ( R IdlGen S ) = I -> ( ( S C_ j -> ( R IdlGen S ) C_ j ) <-> ( S C_ j -> I C_ j ) ) )
14 13 ralbidv 
 |-  ( ( R IdlGen S ) = I -> ( A. j e. ( Idl ` R ) ( S C_ j -> ( R IdlGen S ) C_ j ) <-> A. j e. ( Idl ` R ) ( S C_ j -> I C_ j ) ) )
15 10 11 14 3anbi123d 
 |-  ( ( R IdlGen S ) = I -> ( ( ( R IdlGen S ) e. ( Idl ` R ) /\ S C_ ( R IdlGen S ) /\ A. j e. ( Idl ` R ) ( S C_ j -> ( R IdlGen S ) C_ j ) ) <-> ( I e. ( Idl ` R ) /\ S C_ I /\ A. j e. ( Idl ` R ) ( S C_ j -> I C_ j ) ) ) )
16 9 15 syl5ibcom 
 |-  ( ( R e. RingOps /\ S C_ X ) -> ( ( R IdlGen S ) = I -> ( I e. ( Idl ` R ) /\ S C_ I /\ A. j e. ( Idl ` R ) ( S C_ j -> I C_ j ) ) ) )
17 igenmin 
 |-  ( ( R e. RingOps /\ I e. ( Idl ` R ) /\ S C_ I ) -> ( R IdlGen S ) C_ I )
18 17 3adant3r3 
 |-  ( ( R e. RingOps /\ ( I e. ( Idl ` R ) /\ S C_ I /\ A. j e. ( Idl ` R ) ( S C_ j -> I C_ j ) ) ) -> ( R IdlGen S ) C_ I )
19 18 adantlr 
 |-  ( ( ( R e. RingOps /\ S C_ X ) /\ ( I e. ( Idl ` R ) /\ S C_ I /\ A. j e. ( Idl ` R ) ( S C_ j -> I C_ j ) ) ) -> ( R IdlGen S ) C_ I )
20 ssint 
 |-  ( I C_ |^| { i e. ( Idl ` R ) | S C_ i } <-> A. j e. { i e. ( Idl ` R ) | S C_ i } I C_ j )
21 sseq2 
 |-  ( i = j -> ( S C_ i <-> S C_ j ) )
22 21 ralrab 
 |-  ( A. j e. { i e. ( Idl ` R ) | S C_ i } I C_ j <-> A. j e. ( Idl ` R ) ( S C_ j -> I C_ j ) )
23 20 22 sylbbr 
 |-  ( A. j e. ( Idl ` R ) ( S C_ j -> I C_ j ) -> I C_ |^| { i e. ( Idl ` R ) | S C_ i } )
24 23 3ad2ant3 
 |-  ( ( I e. ( Idl ` R ) /\ S C_ I /\ A. j e. ( Idl ` R ) ( S C_ j -> I C_ j ) ) -> I C_ |^| { i e. ( Idl ` R ) | S C_ i } )
25 24 adantl 
 |-  ( ( ( R e. RingOps /\ S C_ X ) /\ ( I e. ( Idl ` R ) /\ S C_ I /\ A. j e. ( Idl ` R ) ( S C_ j -> I C_ j ) ) ) -> I C_ |^| { i e. ( Idl ` R ) | S C_ i } )
26 1 2 igenval 
 |-  ( ( R e. RingOps /\ S C_ X ) -> ( R IdlGen S ) = |^| { i e. ( Idl ` R ) | S C_ i } )
27 26 adantr 
 |-  ( ( ( R e. RingOps /\ S C_ X ) /\ ( I e. ( Idl ` R ) /\ S C_ I /\ A. j e. ( Idl ` R ) ( S C_ j -> I C_ j ) ) ) -> ( R IdlGen S ) = |^| { i e. ( Idl ` R ) | S C_ i } )
28 25 27 sseqtrrd 
 |-  ( ( ( R e. RingOps /\ S C_ X ) /\ ( I e. ( Idl ` R ) /\ S C_ I /\ A. j e. ( Idl ` R ) ( S C_ j -> I C_ j ) ) ) -> I C_ ( R IdlGen S ) )
29 19 28 eqssd 
 |-  ( ( ( R e. RingOps /\ S C_ X ) /\ ( I e. ( Idl ` R ) /\ S C_ I /\ A. j e. ( Idl ` R ) ( S C_ j -> I C_ j ) ) ) -> ( R IdlGen S ) = I )
30 29 ex 
 |-  ( ( R e. RingOps /\ S C_ X ) -> ( ( I e. ( Idl ` R ) /\ S C_ I /\ A. j e. ( Idl ` R ) ( S C_ j -> I C_ j ) ) -> ( R IdlGen S ) = I ) )
31 16 30 impbid 
 |-  ( ( R e. RingOps /\ S C_ X ) -> ( ( R IdlGen S ) = I <-> ( I e. ( Idl ` R ) /\ S C_ I /\ A. j e. ( Idl ` R ) ( S C_ j -> I C_ j ) ) ) )