lidldvgen

Description: An element generates an ideal iff it is contained in the ideal and all elements are right-divided by it. (Contributed by Stefan O'Rear, 3-Jan-2015)

	Ref	Expression
Hypotheses	lidldvgen.b	$⊢ B = {Base}_{R}$
	lidldvgen.u	$⊢ U = LIdeal (R)$
	lidldvgen.k	$⊢ K = RSpan (R)$
	lidldvgen.d	$⊢ \underset{˙}{∥} = ∥_{r} (R)$
Assertion	lidldvgen	$⊢ (R \in Ring \land I \in U \land G \in B) \to (I = K (\{G\}) \leftrightarrow (G \in I \land \forall x \in I G \underset{˙}{∥} x))$

Proof

Step	Hyp	Ref	Expression
1		lidldvgen.b	$⊢ B = {Base}_{R}$
2		lidldvgen.u	$⊢ U = LIdeal (R)$
3		lidldvgen.k	$⊢ K = RSpan (R)$
4		lidldvgen.d	$⊢ \underset{˙}{∥} = ∥_{r} (R)$
5		simp1	$⊢ (R \in Ring \land I \in U \land G \in B) \to R \in Ring$
6		simp3	$⊢ (R \in Ring \land I \in U \land G \in B) \to G \in B$
7	6	snssd	$⊢ (R \in Ring \land I \in U \land G \in B) \to \{G\} \subseteq B$
8	3 1	rspssid	$⊢ (R \in Ring \land \{G\} \subseteq B) \to \{G\} \subseteq K (\{G\})$
9	5 7 8	syl2anc	$⊢ (R \in Ring \land I \in U \land G \in B) \to \{G\} \subseteq K (\{G\})$
10		snssg	$⊢ G \in B \to (G \in K (\{G\}) \leftrightarrow \{G\} \subseteq K (\{G\}))$
11	10	3ad2ant3	$⊢ (R \in Ring \land I \in U \land G \in B) \to (G \in K (\{G\}) \leftrightarrow \{G\} \subseteq K (\{G\}))$
12	9 11	mpbird	$⊢ (R \in Ring \land I \in U \land G \in B) \to G \in K (\{G\})$
13	1 3 4	rspsn	$⊢ (R \in Ring \land G \in B) \to K (\{G\}) = \{y \| G \underset{˙}{∥} y\}$
14	13	3adant2	$⊢ (R \in Ring \land I \in U \land G \in B) \to K (\{G\}) = \{y \| G \underset{˙}{∥} y\}$
15	14	eleq2d	$⊢ (R \in Ring \land I \in U \land G \in B) \to (x \in K (\{G\}) \leftrightarrow x \in \{y \| G \underset{˙}{∥} y\})$
16		vex	$⊢ x \in V$
17		breq2	$⊢ y = x \to (G \underset{˙}{∥} y \leftrightarrow G \underset{˙}{∥} x)$
18	16 17	elab	$⊢ x \in \{y \| G \underset{˙}{∥} y\} \leftrightarrow G \underset{˙}{∥} x$
19	15 18	bitrdi	$⊢ (R \in Ring \land I \in U \land G \in B) \to (x \in K (\{G\}) \leftrightarrow G \underset{˙}{∥} x)$
20	19	biimpd	$⊢ (R \in Ring \land I \in U \land G \in B) \to (x \in K (\{G\}) \to G \underset{˙}{∥} x)$
21	20	ralrimiv	$⊢ (R \in Ring \land I \in U \land G \in B) \to \forall x \in K (\{G\}) G \underset{˙}{∥} x$
22	12 21	jca	$⊢ (R \in Ring \land I \in U \land G \in B) \to (G \in K (\{G\}) \land \forall x \in K (\{G\}) G \underset{˙}{∥} x)$
23		eleq2	$⊢ I = K (\{G\}) \to (G \in I \leftrightarrow G \in K (\{G\}))$
24		raleq	$⊢ I = K (\{G\}) \to (\forall x \in I G \underset{˙}{∥} x \leftrightarrow \forall x \in K (\{G\}) G \underset{˙}{∥} x)$
25	23 24	anbi12d	$⊢ I = K (\{G\}) \to ((G \in I \land \forall x \in I G \underset{˙}{∥} x) \leftrightarrow (G \in K (\{G\}) \land \forall x \in K (\{G\}) G \underset{˙}{∥} x))$
26	22 25	syl5ibrcom	$⊢ (R \in Ring \land I \in U \land G \in B) \to (I = K (\{G\}) \to (G \in I \land \forall x \in I G \underset{˙}{∥} x))$
27		df-ral	$⊢ \forall x \in I G \underset{˙}{∥} x \leftrightarrow \forall x (x \in I \to G \underset{˙}{∥} x)$
28		ssab	$⊢ I \subseteq \{x \| G \underset{˙}{∥} x\} \leftrightarrow \forall x (x \in I \to G \underset{˙}{∥} x)$
29	27 28	sylbb2	$⊢ \forall x \in I G \underset{˙}{∥} x \to I \subseteq \{x \| G \underset{˙}{∥} x\}$
30	29	ad2antll	$⊢ ((R \in Ring \land I \in U \land G \in B) \land (G \in I \land \forall x \in I G \underset{˙}{∥} x)) \to I \subseteq \{x \| G \underset{˙}{∥} x\}$
31	1 3 4	rspsn	$⊢ (R \in Ring \land G \in B) \to K (\{G\}) = \{x \| G \underset{˙}{∥} x\}$
32	31	3adant2	$⊢ (R \in Ring \land I \in U \land G \in B) \to K (\{G\}) = \{x \| G \underset{˙}{∥} x\}$
33	32	adantr	$⊢ ((R \in Ring \land I \in U \land G \in B) \land (G \in I \land \forall x \in I G \underset{˙}{∥} x)) \to K (\{G\}) = \{x \| G \underset{˙}{∥} x\}$
34	30 33	sseqtrrd	$⊢ ((R \in Ring \land I \in U \land G \in B) \land (G \in I \land \forall x \in I G \underset{˙}{∥} x)) \to I \subseteq K (\{G\})$
35		simpl1	$⊢ ((R \in Ring \land I \in U \land G \in B) \land G \in I) \to R \in Ring$
36		simpl2	$⊢ ((R \in Ring \land I \in U \land G \in B) \land G \in I) \to I \in U$
37		snssi	$⊢ G \in I \to \{G\} \subseteq I$
38	37	adantl	$⊢ ((R \in Ring \land I \in U \land G \in B) \land G \in I) \to \{G\} \subseteq I$
39	3 2	rspssp	$⊢ (R \in Ring \land I \in U \land \{G\} \subseteq I) \to K (\{G\}) \subseteq I$
40	35 36 38 39	syl3anc	$⊢ ((R \in Ring \land I \in U \land G \in B) \land G \in I) \to K (\{G\}) \subseteq I$
41	40	adantrr	$⊢ ((R \in Ring \land I \in U \land G \in B) \land (G \in I \land \forall x \in I G \underset{˙}{∥} x)) \to K (\{G\}) \subseteq I$
42	34 41	eqssd	$⊢ ((R \in Ring \land I \in U \land G \in B) \land (G \in I \land \forall x \in I G \underset{˙}{∥} x)) \to I = K (\{G\})$
43	42	ex	$⊢ (R \in Ring \land I \in U \land G \in B) \to ((G \in I \land \forall x \in I G \underset{˙}{∥} x) \to I = K (\{G\}))$
44	26 43	impbid	$⊢ (R \in Ring \land I \in U \land G \in B) \to (I = K (\{G\}) \leftrightarrow (G \in I \land \forall x \in I G \underset{˙}{∥} x))$

Metamath Proof Explorer

Theorem lidldvgen

Proof