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 ⊢ 𝐺 = ( 1st ‘ 𝑅 )
igenval.2 ⊢ 𝑋 = ran 𝐺
Assertion igenval ( ( 𝑅 ∈ RingOps ∧ 𝑆 ⊆ 𝑋 ) → ( 𝑅 IdlGen 𝑆 ) = ∩ { 𝑗 ∈ ( Idl ‘ 𝑅 ) ∣ 𝑆 ⊆ 𝑗 } )

Proof

Step Hyp Ref Expression
1 igenval.1 ⊢ 𝐺 = ( 1st ‘ 𝑅 )
2 igenval.2 ⊢ 𝑋 = ran 𝐺
3 1 2 rngoidl ⊢ ( 𝑅 ∈ RingOps → 𝑋 ∈ ( Idl ‘ 𝑅 ) )
4 sseq2 ⊢ ( 𝑗 = 𝑋 → ( 𝑆 ⊆ 𝑗 ↔ 𝑆 ⊆ 𝑋 ) )
5 4 rspcev ⊢ ( ( 𝑋 ∈ ( Idl ‘ 𝑅 ) ∧ 𝑆 ⊆ 𝑋 ) → ∃ 𝑗 ∈ ( Idl ‘ 𝑅 ) 𝑆 ⊆ 𝑗 )
6 3 5 sylan ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑆 ⊆ 𝑋 ) → ∃ 𝑗 ∈ ( Idl ‘ 𝑅 ) 𝑆 ⊆ 𝑗 )
7 rabn0 ⊢ ( { 𝑗 ∈ ( Idl ‘ 𝑅 ) ∣ 𝑆 ⊆ 𝑗 } ≠ ∅ ↔ ∃ 𝑗 ∈ ( Idl ‘ 𝑅 ) 𝑆 ⊆ 𝑗 )
8 6 7 sylibr ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑆 ⊆ 𝑋 ) → { 𝑗 ∈ ( Idl ‘ 𝑅 ) ∣ 𝑆 ⊆ 𝑗 } ≠ ∅ )
9 intex ⊢ ( { 𝑗 ∈ ( Idl ‘ 𝑅 ) ∣ 𝑆 ⊆ 𝑗 } ≠ ∅ ↔ ∩ { 𝑗 ∈ ( Idl ‘ 𝑅 ) ∣ 𝑆 ⊆ 𝑗 } ∈ V )
10 8 9 sylib ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑆 ⊆ 𝑋 ) → ∩ { 𝑗 ∈ ( Idl ‘ 𝑅 ) ∣ 𝑆 ⊆ 𝑗 } ∈ V )
11 1 fvexi ⊢ 𝐺 ∈ V
12 11 rnex ⊢ ran 𝐺 ∈ V
13 2 12 eqeltri ⊢ 𝑋 ∈ V
14 13 elpw2 ⊢ ( 𝑆 ∈ 𝒫 𝑋 ↔ 𝑆 ⊆ 𝑋 )
15 simpl ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) → 𝑟 = 𝑅 )
16 15 fveq2d ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) → ( Idl ‘ 𝑟 ) = ( Idl ‘ 𝑅 ) )
17 sseq1 ⊢ ( 𝑠 = 𝑆 → ( 𝑠 ⊆ 𝑗 ↔ 𝑆 ⊆ 𝑗 ) )
18 17 adantl ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) → ( 𝑠 ⊆ 𝑗 ↔ 𝑆 ⊆ 𝑗 ) )
19 16 18 rabeqbidv ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) → { 𝑗 ∈ ( Idl ‘ 𝑟 ) ∣ 𝑠 ⊆ 𝑗 } = { 𝑗 ∈ ( Idl ‘ 𝑅 ) ∣ 𝑆 ⊆ 𝑗 } )
20 19 inteqd ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) → ∩ { 𝑗 ∈ ( Idl ‘ 𝑟 ) ∣ 𝑠 ⊆ 𝑗 } = ∩ { 𝑗 ∈ ( Idl ‘ 𝑅 ) ∣ 𝑆 ⊆ 𝑗 } )
21 fveq2 ⊢ ( 𝑟 = 𝑅 → ( 1st ‘ 𝑟 ) = ( 1st ‘ 𝑅 ) )
22 21 1 eqtr4di ⊢ ( 𝑟 = 𝑅 → ( 1st ‘ 𝑟 ) = 𝐺 )
23 22 rneqd ⊢ ( 𝑟 = 𝑅 → ran ( 1st ‘ 𝑟 ) = ran 𝐺 )
24 23 2 eqtr4di ⊢ ( 𝑟 = 𝑅 → ran ( 1st ‘ 𝑟 ) = 𝑋 )
25 24 pweqd ⊢ ( 𝑟 = 𝑅 → 𝒫 ran ( 1st ‘ 𝑟 ) = 𝒫 𝑋 )
26 df-igen ⊢ IdlGen = ( 𝑟 ∈ RingOps , 𝑠 ∈ 𝒫 ran ( 1st ‘ 𝑟 ) ↦ ∩ { 𝑗 ∈ ( Idl ‘ 𝑟 ) ∣ 𝑠 ⊆ 𝑗 } )
27 20 25 26 ovmpox ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ 𝒫 𝑋 ∧ ∩ { 𝑗 ∈ ( Idl ‘ 𝑅 ) ∣ 𝑆 ⊆ 𝑗 } ∈ V ) → ( 𝑅 IdlGen 𝑆 ) = ∩ { 𝑗 ∈ ( Idl ‘ 𝑅 ) ∣ 𝑆 ⊆ 𝑗 } )
28 14 27 syl3an2br ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑆 ⊆ 𝑋 ∧ ∩ { 𝑗 ∈ ( Idl ‘ 𝑅 ) ∣ 𝑆 ⊆ 𝑗 } ∈ V ) → ( 𝑅 IdlGen 𝑆 ) = ∩ { 𝑗 ∈ ( Idl ‘ 𝑅 ) ∣ 𝑆 ⊆ 𝑗 } )
29 10 28 mpd3an3 ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑆 ⊆ 𝑋 ) → ( 𝑅 IdlGen 𝑆 ) = ∩ { 𝑗 ∈ ( Idl ‘ 𝑅 ) ∣ 𝑆 ⊆ 𝑗 } )