This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )