Theorem igenval 34810

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.)

Hypotheses

Ref	Expression
igenval.1	⊢ 𝐺 = (1st ‘𝑅)
igenval.2	⊢ 𝑋 = ran 𝐺

Assertion

Ref	Expression
igenval	⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ⊆ 𝑋) → (𝑅 IdlGen 𝑆) = ∩ {𝑗 ∈ (Idl‘𝑅) ∣ 𝑆 ⊆ 𝑗})

Distinct variable groups:   𝑅,𝑗   𝑆,𝑗   𝑗,𝑋

Allowed substitution hint:   𝐺(𝑗)

Proof of Theorem igenval

Dummy variables 𝑟 𝑠 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		igenval.1	. . . . . 6 ⊢ 𝐺 = (1st ‘𝑅)
2		igenval.2	. . . . . 6 ⊢ 𝑋 = ran 𝐺
3	1, 2	rngoidl 34773	. . . . 5 ⊢ (𝑅 ∈ RingOps → 𝑋 ∈ (Idl‘𝑅))
4		sseq2 3877	. . . . . 6 ⊢ (𝑗 = 𝑋 → (𝑆 ⊆ 𝑗 ↔ 𝑆 ⊆ 𝑋))
5	4	rspcev 3529	. . . . 5 ⊢ ((𝑋 ∈ (Idl‘𝑅) ∧ 𝑆 ⊆ 𝑋) → ∃𝑗 ∈ (Idl‘𝑅)𝑆 ⊆ 𝑗)
6	3, 5	sylan 572	. . . 4 ⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ⊆ 𝑋) → ∃𝑗 ∈ (Idl‘𝑅)𝑆 ⊆ 𝑗)
7		rabn0 4219	. . . 4 ⊢ ({𝑗 ∈ (Idl‘𝑅) ∣ 𝑆 ⊆ 𝑗} ≠ ∅ ↔ ∃𝑗 ∈ (Idl‘𝑅)𝑆 ⊆ 𝑗)
8	6, 7	sylibr 226	. . 3 ⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ⊆ 𝑋) → {𝑗 ∈ (Idl‘𝑅) ∣ 𝑆 ⊆ 𝑗} ≠ ∅)
9		intex 5092	. . 3 ⊢ ({𝑗 ∈ (Idl‘𝑅) ∣ 𝑆 ⊆ 𝑗} ≠ ∅ ↔ ∩ {𝑗 ∈ (Idl‘𝑅) ∣ 𝑆 ⊆ 𝑗} ∈ V)
10	8, 9	sylib 210	. 2 ⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ⊆ 𝑋) → ∩ {𝑗 ∈ (Idl‘𝑅) ∣ 𝑆 ⊆ 𝑗} ∈ V)
11	1	fvexi 6510	. . . . . 6 ⊢ 𝐺 ∈ V
12	11	rnex 7430	. . . . 5 ⊢ ran 𝐺 ∈ V
13	2, 12	eqeltri 2856	. . . 4 ⊢ 𝑋 ∈ V
14	13	elpw2 5100	. . 3 ⊢ (𝑆 ∈ 𝒫 𝑋 ↔ 𝑆 ⊆ 𝑋)
15		simpl 475	. . . . . . 7 ⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → 𝑟 = 𝑅)
16	15	fveq2d 6500	. . . . . 6 ⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → (Idl‘𝑟) = (Idl‘𝑅))
17		sseq1 3876	. . . . . . 7 ⊢ (𝑠 = 𝑆 → (𝑠 ⊆ 𝑗 ↔ 𝑆 ⊆ 𝑗))
18	17	adantl 474	. . . . . 6 ⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → (𝑠 ⊆ 𝑗 ↔ 𝑆 ⊆ 𝑗))
19	16, 18	rabeqbidv 3402	. . . . 5 ⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → {𝑗 ∈ (Idl‘𝑟) ∣ 𝑠 ⊆ 𝑗} = {𝑗 ∈ (Idl‘𝑅) ∣ 𝑆 ⊆ 𝑗})
20	19	inteqd 4750	. . . 4 ⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → ∩ {𝑗 ∈ (Idl‘𝑟) ∣ 𝑠 ⊆ 𝑗} = ∩ {𝑗 ∈ (Idl‘𝑅) ∣ 𝑆 ⊆ 𝑗})
21		fveq2 6496	. . . . . . . 8 ⊢ (𝑟 = 𝑅 → (1st ‘𝑟) = (1st ‘𝑅))
22	21, 1	syl6eqr 2826	. . . . . . 7 ⊢ (𝑟 = 𝑅 → (1st ‘𝑟) = 𝐺)
23	22	rneqd 5648	. . . . . 6 ⊢ (𝑟 = 𝑅 → ran (1st ‘𝑟) = ran 𝐺)
24	23, 2	syl6eqr 2826	. . . . 5 ⊢ (𝑟 = 𝑅 → ran (1st ‘𝑟) = 𝑋)
25	24	pweqd 4421	. . . 4 ⊢ (𝑟 = 𝑅 → 𝒫 ran (1st ‘𝑟) = 𝒫 𝑋)
26		df-igen 34809	. . . 4 ⊢ IdlGen = (𝑟 ∈ RingOps, 𝑠 ∈ 𝒫 ran (1st ‘𝑟) ↦ ∩ {𝑗 ∈ (Idl‘𝑟) ∣ 𝑠 ⊆ 𝑗})
27	20, 25, 26	ovmpox 7117	. . 3 ⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ 𝒫 𝑋 ∧ ∩ {𝑗 ∈ (Idl‘𝑅) ∣ 𝑆 ⊆ 𝑗} ∈ V) → (𝑅 IdlGen 𝑆) = ∩ {𝑗 ∈ (Idl‘𝑅) ∣ 𝑆 ⊆ 𝑗})
28	14, 27	syl3an2br 1387	. 2 ⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ⊆ 𝑋 ∧ ∩ {𝑗 ∈ (Idl‘𝑅) ∣ 𝑆 ⊆ 𝑗} ∈ V) → (𝑅 IdlGen 𝑆) = ∩ {𝑗 ∈ (Idl‘𝑅) ∣ 𝑆 ⊆ 𝑗})
29	10, 28	mpd3an3 1441	1 ⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ⊆ 𝑋) → (𝑅 IdlGen 𝑆) = ∩ {𝑗 ∈ (Idl‘𝑅) ∣ 𝑆 ⊆ 𝑗})

Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 387   = wceq 1507   ∈ wcel 2050   ≠ wne 2961  ∃wrex 3083  {crab 3086  Vcvv 3409   ⊆ wss 3823  ∅c0 4172  𝒫 cpw 4416  ∩ cint 4745  ran crn 5404  ‘cfv 6185  (class class class)co 6974  1^st c1st 7497  RingOpscrngo 34643  Idlcidl 34756   IdlGen cigen 34808

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-13 2301  ax-ext 2744  ax-sep 5056  ax-nul 5063  ax-pow 5115  ax-pr 5182  ax-un 7277

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-mo 2547  df-eu 2584  df-clab 2753  df-cleq 2765  df-clel 2840  df-nfc 2912  df-ne 2962  df-ral 3087  df-rex 3088  df-reu 3089  df-rab 3091  df-v 3411  df-sbc 3676  df-csb 3781  df-dif 3826  df-un 3828  df-in 3830  df-ss 3837  df-nul 4173  df-if 4345  df-pw 4418  df-sn 4436  df-pr 4438  df-op 4442  df-uni 4709  df-int 4746  df-iun 4790  df-br 4926  df-opab 4988  df-mpt 5005  df-id 5308  df-xp 5409  df-rel 5410  df-cnv 5411  df-co 5412  df-dm 5413  df-rn 5414  df-iota 6149  df-fun 6187  df-fn 6188  df-f 6189  df-fo 6191  df-fv 6193  df-riota 6935  df-ov 6977  df-oprab 6978  df-mpo 6979  df-1st 7499  df-2nd 7500  df-grpo 28059  df-gid 28060  df-ablo 28111  df-rngo 34644  df-idl 34759  df-igen 34809

This theorem is referenced by:  igenss  34811  igenidl  34812  igenmin  34813  igenidl2  34814  igenval2  34815