igenval2

Description: The ideal generated by a subset of a ring. (Contributed by Jeff Madsen, 10-Jun-2010)

	Ref	Expression
Hypotheses	igenval2.1	$⊢ G = 1^{st} (R)$
	igenval2.2	$⊢ X = ran G$
Assertion	igenval2	$⊢ (R \in RingOps \land S \subseteq X) \to (R IdlGen S = I \leftrightarrow (I \in Idl (R) \land S \subseteq I \land \forall j \in Idl (R) (S \subseteq j \to I \subseteq j)))$

Proof

Step	Hyp	Ref	Expression
1		igenval2.1	$⊢ G = 1^{st} (R)$
2		igenval2.2	$⊢ X = ran G$
3	1 2	igenidl	$⊢ (R \in RingOps \land S \subseteq X) \to R IdlGen S \in Idl (R)$
4	1 2	igenss	$⊢ (R \in RingOps \land S \subseteq X) \to S \subseteq R IdlGen S$
5		igenmin	$⊢ (R \in RingOps \land j \in Idl (R) \land S \subseteq j) \to R IdlGen S \subseteq j$
6	5	3expia	$⊢ (R \in RingOps \land j \in Idl (R)) \to (S \subseteq j \to R IdlGen S \subseteq j)$
7	6	ralrimiva	$⊢ R \in RingOps \to \forall j \in Idl (R) (S \subseteq j \to R IdlGen S \subseteq j)$
8	7	adantr	$⊢ (R \in RingOps \land S \subseteq X) \to \forall j \in Idl (R) (S \subseteq j \to R IdlGen S \subseteq j)$
9	3 4 8	3jca	$⊢ (R \in RingOps \land S \subseteq X) \to (R IdlGen S \in Idl (R) \land S \subseteq R IdlGen S \land \forall j \in Idl (R) (S \subseteq j \to R IdlGen S \subseteq j))$
10		eleq1	$⊢ R IdlGen S = I \to (R IdlGen S \in Idl (R) \leftrightarrow I \in Idl (R))$
11		sseq2	$⊢ R IdlGen S = I \to (S \subseteq R IdlGen S \leftrightarrow S \subseteq I)$
12		sseq1	$⊢ R IdlGen S = I \to (R IdlGen S \subseteq j \leftrightarrow I \subseteq j)$
13	12	imbi2d	$⊢ R IdlGen S = I \to ((S \subseteq j \to R IdlGen S \subseteq j) \leftrightarrow (S \subseteq j \to I \subseteq j))$
14	13	ralbidv	$⊢ R IdlGen S = I \to (\forall j \in Idl (R) (S \subseteq j \to R IdlGen S \subseteq j) \leftrightarrow \forall j \in Idl (R) (S \subseteq j \to I \subseteq j))$
15	10 11 14	3anbi123d	$⊢ R IdlGen S = I \to ((R IdlGen S \in Idl (R) \land S \subseteq R IdlGen S \land \forall j \in Idl (R) (S \subseteq j \to R IdlGen S \subseteq j)) \leftrightarrow (I \in Idl (R) \land S \subseteq I \land \forall j \in Idl (R) (S \subseteq j \to I \subseteq j)))$
16	9 15	syl5ibcom	$⊢ (R \in RingOps \land S \subseteq X) \to (R IdlGen S = I \to (I \in Idl (R) \land S \subseteq I \land \forall j \in Idl (R) (S \subseteq j \to I \subseteq j)))$
17		igenmin	$⊢ (R \in RingOps \land I \in Idl (R) \land S \subseteq I) \to R IdlGen S \subseteq I$
18	17	3adant3r3	$⊢ (R \in RingOps \land (I \in Idl (R) \land S \subseteq I \land \forall j \in Idl (R) (S \subseteq j \to I \subseteq j))) \to R IdlGen S \subseteq I$
19	18	adantlr	$⊢ ((R \in RingOps \land S \subseteq X) \land (I \in Idl (R) \land S \subseteq I \land \forall j \in Idl (R) (S \subseteq j \to I \subseteq j))) \to R IdlGen S \subseteq I$
20		ssint	$⊢ I \subseteq ⋂ \{i \in Idl (R) \| S \subseteq i\} \leftrightarrow \forall j \in \{i \in Idl (R) \| S \subseteq i\} I \subseteq j$
21		sseq2	$⊢ i = j \to (S \subseteq i \leftrightarrow S \subseteq j)$
22	21	ralrab	$⊢ \forall j \in \{i \in Idl (R) \| S \subseteq i\} I \subseteq j \leftrightarrow \forall j \in Idl (R) (S \subseteq j \to I \subseteq j)$
23	20 22	sylbbr	$⊢ \forall j \in Idl (R) (S \subseteq j \to I \subseteq j) \to I \subseteq ⋂ \{i \in Idl (R) \| S \subseteq i\}$
24	23	3ad2ant3	$⊢ (I \in Idl (R) \land S \subseteq I \land \forall j \in Idl (R) (S \subseteq j \to I \subseteq j)) \to I \subseteq ⋂ \{i \in Idl (R) \| S \subseteq i\}$
25	24	adantl	$⊢ ((R \in RingOps \land S \subseteq X) \land (I \in Idl (R) \land S \subseteq I \land \forall j \in Idl (R) (S \subseteq j \to I \subseteq j))) \to I \subseteq ⋂ \{i \in Idl (R) \| S \subseteq i\}$
26	1 2	igenval	$⊢ (R \in RingOps \land S \subseteq X) \to R IdlGen S = ⋂ \{i \in Idl (R) \| S \subseteq i\}$
27	26	adantr	$⊢ ((R \in RingOps \land S \subseteq X) \land (I \in Idl (R) \land S \subseteq I \land \forall j \in Idl (R) (S \subseteq j \to I \subseteq j))) \to R IdlGen S = ⋂ \{i \in Idl (R) \| S \subseteq i\}$
28	25 27	sseqtrrd	$⊢ ((R \in RingOps \land S \subseteq X) \land (I \in Idl (R) \land S \subseteq I \land \forall j \in Idl (R) (S \subseteq j \to I \subseteq j))) \to I \subseteq R IdlGen S$
29	19 28	eqssd	$⊢ ((R \in RingOps \land S \subseteq X) \land (I \in Idl (R) \land S \subseteq I \land \forall j \in Idl (R) (S \subseteq j \to I \subseteq j))) \to R IdlGen S = I$
30	29	ex	$⊢ (R \in RingOps \land S \subseteq X) \to ((I \in Idl (R) \land S \subseteq I \land \forall j \in Idl (R) (S \subseteq j \to I \subseteq j)) \to R IdlGen S = I)$
31	16 30	impbid	$⊢ (R \in RingOps \land S \subseteq X) \to (R IdlGen S = I \leftrightarrow (I \in Idl (R) \land S \subseteq I \land \forall j \in Idl (R) (S \subseteq j \to I \subseteq j)))$

Metamath Proof Explorer

Theorem igenval2

Proof