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

Metamath Proof Explorer

Theorem divrngidl

Description: The only ideals in a division ring are the zero ideal and the unit ideal. (Contributed by Jeff Madsen, 10-Jun-2010)

Ref Expression
Hypotheses divrngidl.1 
|- G = ( 1st ` R )
divrngidl.2 
|- H = ( 2nd ` R )
divrngidl.3 
|- X = ran G
divrngidl.4 
|- Z = ( GId ` G )
Assertion divrngidl 
|- ( R e. DivRingOps -> ( Idl ` R ) = { { Z } , X } )

Proof

Step Hyp Ref Expression
1 divrngidl.1 
 |-  G = ( 1st ` R )
2 divrngidl.2 
 |-  H = ( 2nd ` R )
3 divrngidl.3 
 |-  X = ran G
4 divrngidl.4 
 |-  Z = ( GId ` G )
5 eqid 
 |-  ( GId ` H ) = ( GId ` H )
6 1 2 4 3 5 isdrngo2 
 |-  ( R e. DivRingOps <-> ( R e. RingOps /\ ( ( GId ` H ) =/= Z /\ A. x e. ( X \ { Z } ) E. y e. ( X \ { Z } ) ( y H x ) = ( GId ` H ) ) ) )
7 1 4 idl0cl 
 |-  ( ( R e. RingOps /\ i e. ( Idl ` R ) ) -> Z e. i )
8 7 adantr 
 |-  ( ( ( R e. RingOps /\ i e. ( Idl ` R ) ) /\ A. x e. ( X \ { Z } ) E. y e. ( X \ { Z } ) ( y H x ) = ( GId ` H ) ) -> Z e. i )
9 4 fvexi 
 |-  Z e. _V
10 9 snss 
 |-  ( Z e. i <-> { Z } C_ i )
11 necom 
 |-  ( i =/= { Z } <-> { Z } =/= i )
12 pssdifn0 
 |-  ( ( { Z } C_ i /\ { Z } =/= i ) -> ( i \ { Z } ) =/= (/) )
13 n0 
 |-  ( ( i \ { Z } ) =/= (/) <-> E. z z e. ( i \ { Z } ) )
14 12 13 sylib 
 |-  ( ( { Z } C_ i /\ { Z } =/= i ) -> E. z z e. ( i \ { Z } ) )
15 10 11 14 syl2anb 
 |-  ( ( Z e. i /\ i =/= { Z } ) -> E. z z e. ( i \ { Z } ) )
16 1 3 idlss 
 |-  ( ( R e. RingOps /\ i e. ( Idl ` R ) ) -> i C_ X )
17 ssdif 
 |-  ( i C_ X -> ( i \ { Z } ) C_ ( X \ { Z } ) )
18 17 sselda 
 |-  ( ( i C_ X /\ z e. ( i \ { Z } ) ) -> z e. ( X \ { Z } ) )
19 16 18 sylan 
 |-  ( ( ( R e. RingOps /\ i e. ( Idl ` R ) ) /\ z e. ( i \ { Z } ) ) -> z e. ( X \ { Z } ) )
20 oveq2 
 |-  ( x = z -> ( y H x ) = ( y H z ) )
21 20 eqeq1d 
 |-  ( x = z -> ( ( y H x ) = ( GId ` H ) <-> ( y H z ) = ( GId ` H ) ) )
22 21 rexbidv 
 |-  ( x = z -> ( E. y e. ( X \ { Z } ) ( y H x ) = ( GId ` H ) <-> E. y e. ( X \ { Z } ) ( y H z ) = ( GId ` H ) ) )
23 22 rspcva 
 |-  ( ( z e. ( X \ { Z } ) /\ A. x e. ( X \ { Z } ) E. y e. ( X \ { Z } ) ( y H x ) = ( GId ` H ) ) -> E. y e. ( X \ { Z } ) ( y H z ) = ( GId ` H ) )
24 19 23 sylan 
 |-  ( ( ( ( R e. RingOps /\ i e. ( Idl ` R ) ) /\ z e. ( i \ { Z } ) ) /\ A. x e. ( X \ { Z } ) E. y e. ( X \ { Z } ) ( y H x ) = ( GId ` H ) ) -> E. y e. ( X \ { Z } ) ( y H z ) = ( GId ` H ) )
25 eldifi 
 |-  ( z e. ( i \ { Z } ) -> z e. i )
26 eldifi 
 |-  ( y e. ( X \ { Z } ) -> y e. X )
27 25 26 anim12i 
 |-  ( ( z e. ( i \ { Z } ) /\ y e. ( X \ { Z } ) ) -> ( z e. i /\ y e. X ) )
28 1 2 3 idllmulcl 
 |-  ( ( ( R e. RingOps /\ i e. ( Idl ` R ) ) /\ ( z e. i /\ y e. X ) ) -> ( y H z ) e. i )
29 1 2 3 5 1idl 
 |-  ( ( R e. RingOps /\ i e. ( Idl ` R ) ) -> ( ( GId ` H ) e. i <-> i = X ) )
30 29 biimpd 
 |-  ( ( R e. RingOps /\ i e. ( Idl ` R ) ) -> ( ( GId ` H ) e. i -> i = X ) )
31 30 adantr 
 |-  ( ( ( R e. RingOps /\ i e. ( Idl ` R ) ) /\ ( z e. i /\ y e. X ) ) -> ( ( GId ` H ) e. i -> i = X ) )
32 eleq1 
 |-  ( ( y H z ) = ( GId ` H ) -> ( ( y H z ) e. i <-> ( GId ` H ) e. i ) )
33 32 imbi1d 
 |-  ( ( y H z ) = ( GId ` H ) -> ( ( ( y H z ) e. i -> i = X ) <-> ( ( GId ` H ) e. i -> i = X ) ) )
34 31 33 syl5ibrcom 
 |-  ( ( ( R e. RingOps /\ i e. ( Idl ` R ) ) /\ ( z e. i /\ y e. X ) ) -> ( ( y H z ) = ( GId ` H ) -> ( ( y H z ) e. i -> i = X ) ) )
35 28 34 mpid 
 |-  ( ( ( R e. RingOps /\ i e. ( Idl ` R ) ) /\ ( z e. i /\ y e. X ) ) -> ( ( y H z ) = ( GId ` H ) -> i = X ) )
36 27 35 sylan2 
 |-  ( ( ( R e. RingOps /\ i e. ( Idl ` R ) ) /\ ( z e. ( i \ { Z } ) /\ y e. ( X \ { Z } ) ) ) -> ( ( y H z ) = ( GId ` H ) -> i = X ) )
37 36 anassrs 
 |-  ( ( ( ( R e. RingOps /\ i e. ( Idl ` R ) ) /\ z e. ( i \ { Z } ) ) /\ y e. ( X \ { Z } ) ) -> ( ( y H z ) = ( GId ` H ) -> i = X ) )
38 37 rexlimdva 
 |-  ( ( ( R e. RingOps /\ i e. ( Idl ` R ) ) /\ z e. ( i \ { Z } ) ) -> ( E. y e. ( X \ { Z } ) ( y H z ) = ( GId ` H ) -> i = X ) )
39 38 imp 
 |-  ( ( ( ( R e. RingOps /\ i e. ( Idl ` R ) ) /\ z e. ( i \ { Z } ) ) /\ E. y e. ( X \ { Z } ) ( y H z ) = ( GId ` H ) ) -> i = X )
40 24 39 syldan 
 |-  ( ( ( ( R e. RingOps /\ i e. ( Idl ` R ) ) /\ z e. ( i \ { Z } ) ) /\ A. x e. ( X \ { Z } ) E. y e. ( X \ { Z } ) ( y H x ) = ( GId ` H ) ) -> i = X )
41 40 an32s 
 |-  ( ( ( ( R e. RingOps /\ i e. ( Idl ` R ) ) /\ A. x e. ( X \ { Z } ) E. y e. ( X \ { Z } ) ( y H x ) = ( GId ` H ) ) /\ z e. ( i \ { Z } ) ) -> i = X )
42 41 ex 
 |-  ( ( ( R e. RingOps /\ i e. ( Idl ` R ) ) /\ A. x e. ( X \ { Z } ) E. y e. ( X \ { Z } ) ( y H x ) = ( GId ` H ) ) -> ( z e. ( i \ { Z } ) -> i = X ) )
43 42 exlimdv 
 |-  ( ( ( R e. RingOps /\ i e. ( Idl ` R ) ) /\ A. x e. ( X \ { Z } ) E. y e. ( X \ { Z } ) ( y H x ) = ( GId ` H ) ) -> ( E. z z e. ( i \ { Z } ) -> i = X ) )
44 15 43 syl5 
 |-  ( ( ( R e. RingOps /\ i e. ( Idl ` R ) ) /\ A. x e. ( X \ { Z } ) E. y e. ( X \ { Z } ) ( y H x ) = ( GId ` H ) ) -> ( ( Z e. i /\ i =/= { Z } ) -> i = X ) )
45 8 44 mpand 
 |-  ( ( ( R e. RingOps /\ i e. ( Idl ` R ) ) /\ A. x e. ( X \ { Z } ) E. y e. ( X \ { Z } ) ( y H x ) = ( GId ` H ) ) -> ( i =/= { Z } -> i = X ) )
46 45 an32s 
 |-  ( ( ( R e. RingOps /\ A. x e. ( X \ { Z } ) E. y e. ( X \ { Z } ) ( y H x ) = ( GId ` H ) ) /\ i e. ( Idl ` R ) ) -> ( i =/= { Z } -> i = X ) )
47 neor 
 |-  ( ( i = { Z } \/ i = X ) <-> ( i =/= { Z } -> i = X ) )
48 46 47 sylibr 
 |-  ( ( ( R e. RingOps /\ A. x e. ( X \ { Z } ) E. y e. ( X \ { Z } ) ( y H x ) = ( GId ` H ) ) /\ i e. ( Idl ` R ) ) -> ( i = { Z } \/ i = X ) )
49 48 ex 
 |-  ( ( R e. RingOps /\ A. x e. ( X \ { Z } ) E. y e. ( X \ { Z } ) ( y H x ) = ( GId ` H ) ) -> ( i e. ( Idl ` R ) -> ( i = { Z } \/ i = X ) ) )
50 1 4 0idl 
 |-  ( R e. RingOps -> { Z } e. ( Idl ` R ) )
51 eleq1 
 |-  ( i = { Z } -> ( i e. ( Idl ` R ) <-> { Z } e. ( Idl ` R ) ) )
52 50 51 syl5ibrcom 
 |-  ( R e. RingOps -> ( i = { Z } -> i e. ( Idl ` R ) ) )
53 1 3 rngoidl 
 |-  ( R e. RingOps -> X e. ( Idl ` R ) )
54 eleq1 
 |-  ( i = X -> ( i e. ( Idl ` R ) <-> X e. ( Idl ` R ) ) )
55 53 54 syl5ibrcom 
 |-  ( R e. RingOps -> ( i = X -> i e. ( Idl ` R ) ) )
56 52 55 jaod 
 |-  ( R e. RingOps -> ( ( i = { Z } \/ i = X ) -> i e. ( Idl ` R ) ) )
57 56 adantr 
 |-  ( ( R e. RingOps /\ A. x e. ( X \ { Z } ) E. y e. ( X \ { Z } ) ( y H x ) = ( GId ` H ) ) -> ( ( i = { Z } \/ i = X ) -> i e. ( Idl ` R ) ) )
58 49 57 impbid 
 |-  ( ( R e. RingOps /\ A. x e. ( X \ { Z } ) E. y e. ( X \ { Z } ) ( y H x ) = ( GId ` H ) ) -> ( i e. ( Idl ` R ) <-> ( i = { Z } \/ i = X ) ) )
59 vex 
 |-  i e. _V
60 59 elpr 
 |-  ( i e. { { Z } , X } <-> ( i = { Z } \/ i = X ) )
61 58 60 bitr4di 
 |-  ( ( R e. RingOps /\ A. x e. ( X \ { Z } ) E. y e. ( X \ { Z } ) ( y H x ) = ( GId ` H ) ) -> ( i e. ( Idl ` R ) <-> i e. { { Z } , X } ) )
62 61 eqrdv 
 |-  ( ( R e. RingOps /\ A. x e. ( X \ { Z } ) E. y e. ( X \ { Z } ) ( y H x ) = ( GId ` H ) ) -> ( Idl ` R ) = { { Z } , X } )
63 62 adantrl 
 |-  ( ( R e. RingOps /\ ( ( GId ` H ) =/= Z /\ A. x e. ( X \ { Z } ) E. y e. ( X \ { Z } ) ( y H x ) = ( GId ` H ) ) ) -> ( Idl ` R ) = { { Z } , X } )
64 6 63 sylbi 
 |-  ( R e. DivRingOps -> ( Idl ` R ) = { { Z } , X } )