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 = 1 st R
igenval.2 X = ran G
Assertion igenval R RingOps S X R IdlGen S = j Idl R | S j

Proof

Step Hyp Ref Expression
1 igenval.1 G = 1 st R
2 igenval.2 X = ran G
3 1 2 rngoidl R RingOps X Idl R
4 sseq2 j = X S j S X
5 4 rspcev X Idl R S X j Idl R S j
6 3 5 sylan R RingOps S X j Idl R S j
7 rabn0 j Idl R | S j j Idl R S j
8 6 7 sylibr R RingOps S X j Idl R | S j
9 intex j Idl R | S j j Idl R | S j V
10 8 9 sylib R RingOps S X j Idl R | S j V
11 1 fvexi G V
12 11 rnex ran G V
13 2 12 eqeltri X V
14 13 elpw2 S 𝒫 X S 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 j S j
18 17 adantl r = R s = S s j S j
19 16 18 rabeqbidv r = R s = S j Idl r | s j = j Idl R | S j
20 19 inteqd r = R s = S j Idl r | s j = j Idl R | S j
21 fveq2 r = R 1 st r = 1 st R
22 21 1 eqtr4di r = R 1 st r = G
23 22 rneqd r = R ran 1 st r = ran G
24 23 2 eqtr4di r = R ran 1 st r = X
25 24 pweqd r = R 𝒫 ran 1 st r = 𝒫 X
26 df-igen IdlGen = r RingOps , s 𝒫 ran 1 st r j Idl r | s j
27 20 25 26 ovmpox R RingOps S 𝒫 X j Idl R | S j V R IdlGen S = j Idl R | S j
28 14 27 syl3an2br R RingOps S X j Idl R | S j V R IdlGen S = j Idl R | S j
29 10 28 mpd3an3 R RingOps S X R IdlGen S = j Idl R | S j