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 \in RingOps \land S \subseteq X) \to R IdlGen S = ⋂ \{j \in Idl (R) \| S \subseteq j\}$

Proof

Step	Hyp	Ref	Expression
1		igenval.1	$⊢ G = 1^{st} (R)$
2		igenval.2	$⊢ X = ran G$
3	1 2	rngoidl	$⊢ R \in RingOps \to X \in Idl (R)$
4		sseq2	$⊢ j = X \to (S \subseteq j \leftrightarrow S \subseteq X)$
5	4	rspcev	$⊢ (X \in Idl (R) \land S \subseteq X) \to \exists j \in Idl (R) S \subseteq j$
6	3 5	sylan	$⊢ (R \in RingOps \land S \subseteq X) \to \exists j \in Idl (R) S \subseteq j$
7		rabn0	$⊢ \{j \in Idl (R) \| S \subseteq j\} \neq \emptyset \leftrightarrow \exists j \in Idl (R) S \subseteq j$
8	6 7	sylibr	$⊢ (R \in RingOps \land S \subseteq X) \to \{j \in Idl (R) \| S \subseteq j\} \neq \emptyset$
9		intex	$⊢ \{j \in Idl (R) \| S \subseteq j\} \neq \emptyset \leftrightarrow ⋂ \{j \in Idl (R) \| S \subseteq j\} \in V$
10	8 9	sylib	$⊢ (R \in RingOps \land S \subseteq X) \to ⋂ \{j \in Idl (R) \| S \subseteq j\} \in V$
11	1	fvexi	$⊢ G \in V$
12	11	rnex	$⊢ ran G \in V$
13	2 12	eqeltri	$⊢ X \in V$
14	13	elpw2	$⊢ S \in 𝒫 X \leftrightarrow S \subseteq X$
15		simpl	$⊢ (r = R \land s = S) \to r = R$
16	15	fveq2d	$⊢ (r = R \land s = S) \to Idl (r) = Idl (R)$
17		sseq1	$⊢ s = S \to (s \subseteq j \leftrightarrow S \subseteq j)$
18	17	adantl	$⊢ (r = R \land s = S) \to (s \subseteq j \leftrightarrow S \subseteq j)$
19	16 18	rabeqbidv	$⊢ (r = R \land s = S) \to \{j \in Idl (r) \| s \subseteq j\} = \{j \in Idl (R) \| S \subseteq j\}$
20	19	inteqd	$⊢ (r = R \land s = S) \to ⋂ \{j \in Idl (r) \| s \subseteq j\} = ⋂ \{j \in Idl (R) \| S \subseteq j\}$
21		fveq2	$⊢ r = R \to 1^{st} (r) = 1^{st} (R)$
22	21 1	syl6eqr	$⊢ r = R \to 1^{st} (r) = G$
23	22	rneqd	$⊢ r = R \to ran 1^{st} (r) = ran G$
24	23 2	syl6eqr	$⊢ r = R \to ran 1^{st} (r) = X$
25	24	pweqd	$⊢ r = R \to 𝒫 ran 1^{st} (r) = 𝒫 X$
26		df-igen	$⊢ IdlGen = (r \in RingOps, s \in 𝒫 ran 1^{st} (r) ⟼ ⋂ \{j \in Idl (r) \| s \subseteq j\})$
27	20 25 26	ovmpox	$⊢ (R \in RingOps \land S \in 𝒫 X \land ⋂ \{j \in Idl (R) \| S \subseteq j\} \in V) \to R IdlGen S = ⋂ \{j \in Idl (R) \| S \subseteq j\}$
28	14 27	syl3an2br	$⊢ (R \in RingOps \land S \subseteq X \land ⋂ \{j \in Idl (R) \| S \subseteq j\} \in V) \to R IdlGen S = ⋂ \{j \in Idl (R) \| S \subseteq j\}$
29	10 28	mpd3an3	$⊢ (R \in RingOps \land S \subseteq X) \to R IdlGen S = ⋂ \{j \in Idl (R) \| S \subseteq j\}$

Metamath Proof Explorer

Theorem igenval

Proof