Theorem igenval

Description: Obsolete theorem, use rspvalint instead. The ideal generated by a subset of a ring. (Contributed by Jeff Madsen, 10-Jun-2010) (Proof shortened by Mario Carneiro, 20-Dec-2013) (New usage is discouraged.) (Proof modification is discouraged.)

	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 ‘ 𝑅 ) ∣ 𝑆 ⊆ 𝑗 } )