Theorem 1idl

Description: Two ways of expressing the unit ideal. (Contributed by Jeff Madsen, 10-Jun-2010)

	Ref	Expression
Hypotheses	1idl.1	|- G = ( 1st ` R )
	1idl.2	|- H = ( 2nd ` R )
	1idl.3	|- X = ran G
	1idl.4	|- U = ( GId ` H )
Assertion	1idl	|- ( ( R e. RingOps /\ I e. ( Idl ` R ) ) -> ( U e. I <-> I = X ) )

Proof

Step	Hyp	Ref	Expression
1		1idl.1	|- G = ( 1st ` R )
2		1idl.2	|- H = ( 2nd ` R )
3		1idl.3	|- X = ran G
4		1idl.4	|- U = ( GId ` H )
5	1 3	idlss	|- ( ( R e. RingOps /\ I e. ( Idl ` R ) ) -> I C_ X )
6	5	adantr	|- ( ( ( R e. RingOps /\ I e. ( Idl ` R ) ) /\ U e. I ) -> I C_ X )
7	1	rneqi	|- ran G = ran ( 1st ` R )
8	3 7	eqtri	|- X = ran ( 1st ` R )
9	2 8 4	rngolidm	|- ( ( R e. RingOps /\ x e. X ) -> ( U H x ) = x )
10	9	ad2ant2rl	|- ( ( ( R e. RingOps /\ I e. ( Idl ` R ) ) /\ ( U e. I /\ x e. X ) ) -> ( U H x ) = x )
11	1 2 3	idlrmulcl	|- ( ( ( R e. RingOps /\ I e. ( Idl ` R ) ) /\ ( U e. I /\ x e. X ) ) -> ( U H x ) e. I )
12	10 11	eqeltrrd	|- ( ( ( R e. RingOps /\ I e. ( Idl ` R ) ) /\ ( U e. I /\ x e. X ) ) -> x e. I )
13	12	expr	|- ( ( ( R e. RingOps /\ I e. ( Idl ` R ) ) /\ U e. I ) -> ( x e. X -> x e. I ) )
14	13	ssrdv	|- ( ( ( R e. RingOps /\ I e. ( Idl ` R ) ) /\ U e. I ) -> X C_ I )
15	6 14	eqssd	|- ( ( ( R e. RingOps /\ I e. ( Idl ` R ) ) /\ U e. I ) -> I = X )
16	15	ex	|- ( ( R e. RingOps /\ I e. ( Idl ` R ) ) -> ( U e. I -> I = X ) )
17	8 2 4	rngo1cl	|- ( R e. RingOps -> U e. X )
18	17	adantr	|- ( ( R e. RingOps /\ I e. ( Idl ` R ) ) -> U e. X )
19		eleq2	|- ( I = X -> ( U e. I <-> U e. X ) )
20	18 19	syl5ibrcom	|- ( ( R e. RingOps /\ I e. ( Idl ` R ) ) -> ( I = X -> U e. I ) )
21	16 20	impbid	|- ( ( R e. RingOps /\ I e. ( Idl ` R ) ) -> ( U e. I <-> I = X ) )