1idl

Description: Obsolete theorem, use 2idl1el instead. Two ways of expressing the unit ideal. (Contributed by Jeff Madsen, 10-Jun-2010) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypotheses	1idl.1	$⊢ G = 1^{st} (R)$
	1idl.2	$⊢ H = 2^{nd} (R)$
	1idl.3	$⊢ X = ran G$
	1idl.4	$⊢ U = GId (H)$
Assertion	1idl	$⊢ (R \in RingOps \land I \in Idl (R)) \to (U \in I \leftrightarrow I = X)$

Proof

Step	Hyp	Ref	Expression
1		1idl.1	$⊢ G = 1^{st} (R)$
2		1idl.2	$⊢ H = 2^{nd} (R)$
3		1idl.3	$⊢ X = ran G$
4		1idl.4	$⊢ U = GId (H)$
5	1 3	idlss	$⊢ (R \in RingOps \land I \in Idl (R)) \to I \subseteq X$
6	5	adantr	$⊢ ((R \in RingOps \land I \in Idl (R)) \land U \in I) \to I \subseteq X$
7	1	rneqi	$⊢ ran G = ran 1^{st} (R)$
8	3 7	eqtri	$⊢ X = ran 1^{st} (R)$
9	2 8 4	rngolidm	$⊢ (R \in RingOps \land x \in X) \to U H x = x$
10	9	ad2ant2rl	$⊢ ((R \in RingOps \land I \in Idl (R)) \land (U \in I \land x \in X)) \to U H x = x$
11	1 2 3	idlrmulcl	$⊢ ((R \in RingOps \land I \in Idl (R)) \land (U \in I \land x \in X)) \to U H x \in I$
12	10 11	eqeltrrd	$⊢ ((R \in RingOps \land I \in Idl (R)) \land (U \in I \land x \in X)) \to x \in I$
13	12	expr	$⊢ ((R \in RingOps \land I \in Idl (R)) \land U \in I) \to (x \in X \to x \in I)$
14	13	ssrdv	$⊢ ((R \in RingOps \land I \in Idl (R)) \land U \in I) \to X \subseteq I$
15	6 14	eqssd	$⊢ ((R \in RingOps \land I \in Idl (R)) \land U \in I) \to I = X$
16	15	ex	$⊢ (R \in RingOps \land I \in Idl (R)) \to (U \in I \to I = X)$
17	8 2 4	rngo1cl	$⊢ R \in RingOps \to U \in X$
18	17	adantr	$⊢ (R \in RingOps \land I \in Idl (R)) \to U \in X$
19		eleq2	$⊢ I = X \to (U \in I \leftrightarrow U \in X)$
20	18 19	syl5ibrcom	$⊢ (R \in RingOps \land I \in Idl (R)) \to (I = X \to U \in I)$
21	16 20	impbid	$⊢ (R \in RingOps \land I \in Idl (R)) \to (U \in I \leftrightarrow I = X)$

Metamath Proof Explorer

Theorem 1idl

Proof