Metamath Proof Explorer

Theorem igenval

Description: The ideal generated by a subset of a ring. (Contributed by Jeff Madsen, 10-Jun-2010) (Proof shortened by Mario Carneiro, 20-Dec-2013)

Ref Expression
Hypotheses igenval.1 
|- G = ( 1st ` R )
igenval.2 
|- X = ran G
Assertion igenval 
|- ( ( R e. RingOps /\ S C_ X ) -> ( R IdlGen S ) = |^| { j e. ( Idl ` R ) | S C_ j } )

Proof

Step Hyp Ref Expression
1 igenval.1 
 |-  G = ( 1st ` R )
2 igenval.2 
 |-  X = ran G
3 1 2 rngoidl 
 |-  ( R e. RingOps -> X e. ( Idl ` R ) )
4 sseq2 
 |-  ( j = X -> ( S C_ j <-> S C_ X ) )
5 4 rspcev 
 |-  ( ( X e. ( Idl ` R ) /\ S C_ X ) -> E. j e. ( Idl ` R ) S C_ j )
6 3 5 sylan 
 |-  ( ( R e. RingOps /\ S C_ X ) -> E. j e. ( Idl ` R ) S C_ j )
7 rabn0 
 |-  ( { j e. ( Idl ` R ) | S C_ j } =/= (/) <-> E. j e. ( Idl ` R ) S C_ j )
8 6 7 sylibr 
 |-  ( ( R e. RingOps /\ S C_ X ) -> { j e. ( Idl ` R ) | S C_ j } =/= (/) )
9 intex 
 |-  ( { j e. ( Idl ` R ) | S C_ j } =/= (/) <-> |^| { j e. ( Idl ` R ) | S C_ j } e. _V )
10 8 9 sylib 
 |-  ( ( R e. RingOps /\ S C_ X ) -> |^| { j e. ( Idl ` R ) | S C_ j } e. _V )
11 1 fvexi 
 |-  G e. _V
12 11 rnex 
 |-  ran G e. _V
13 2 12 eqeltri 
 |-  X e. _V
14 13 elpw2 
 |-  ( S e. ~P X <-> S C_ X )
15 simpl 
 |-  ( ( r = R /\ s = S ) -> r = R )
16 15 fveq2d 
 |-  ( ( r = R /\ s = S ) -> ( Idl ` r ) = ( Idl ` R ) )
17 sseq1 
 |-  ( s = S -> ( s C_ j <-> S C_ j ) )
18 17 adantl 
 |-  ( ( r = R /\ s = S ) -> ( s C_ j <-> S C_ j ) )
19 16 18 rabeqbidv 
 |-  ( ( r = R /\ s = S ) -> { j e. ( Idl ` r ) | s C_ j } = { j e. ( Idl ` R ) | S C_ j } )
20 19 inteqd 
 |-  ( ( r = R /\ s = S ) -> |^| { j e. ( Idl ` r ) | s C_ j } = |^| { j e. ( Idl ` R ) | S C_ j } )
21 fveq2 
 |-  ( r = R -> ( 1st ` r ) = ( 1st ` R ) )
22 21 1 eqtr4di 
 |-  ( r = R -> ( 1st ` r ) = G )
23 22 rneqd 
 |-  ( r = R -> ran ( 1st ` r ) = ran G )
24 23 2 eqtr4di 
 |-  ( r = R -> ran ( 1st ` r ) = X )
25 24 pweqd 
 |-  ( r = R -> ~P ran ( 1st ` r ) = ~P X )
26 df-igen 
 |-  IdlGen = ( r e. RingOps , s e. ~P ran ( 1st ` r ) |-> |^| { j e. ( Idl ` r ) | s C_ j } )
27 20 25 26 ovmpox 
 |-  ( ( R e. RingOps /\ S e. ~P X /\ |^| { j e. ( Idl ` R ) | S C_ j } e. _V ) -> ( R IdlGen S ) = |^| { j e. ( Idl ` R ) | S C_ j } )
28 14 27 syl3an2br 
 |-  ( ( R e. RingOps /\ S C_ X /\ |^| { j e. ( Idl ` R ) | S C_ j } e. _V ) -> ( R IdlGen S ) = |^| { j e. ( Idl ` R ) | S C_ j } )
29 10 28 mpd3an3 
 |-  ( ( R e. RingOps /\ S C_ X ) -> ( R IdlGen S ) = |^| { j e. ( Idl ` R ) | S C_ j } )