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 ⊢ 𝐺 = ( 1st ‘ 𝑅 )
divrngidl.2 ⊢ 𝐻 = ( 2nd ‘ 𝑅 )
divrngidl.3 ⊢ 𝑋 = ran 𝐺
divrngidl.4 ⊢ 𝑍 = ( GId ‘ 𝐺 )
Assertion divrngidl ( 𝑅 ∈ DivRingOps → ( Idl ‘ 𝑅 ) = { { 𝑍 } , 𝑋 } )

Proof

Step Hyp Ref Expression
1 divrngidl.1 ⊢ 𝐺 = ( 1st ‘ 𝑅 )
2 divrngidl.2 ⊢ 𝐻 = ( 2nd ‘ 𝑅 )
3 divrngidl.3 ⊢ 𝑋 = ran 𝐺
4 divrngidl.4 ⊢ 𝑍 = ( GId ‘ 𝐺 )
5 eqid ⊢ ( GId ‘ 𝐻 ) = ( GId ‘ 𝐻 )
6 1 2 4 3 5 isdrngo2 ⊢ ( 𝑅 ∈ DivRingOps ↔ ( 𝑅 ∈ RingOps ∧ ( ( GId ‘ 𝐻 ) ≠ 𝑍 ∧ ∀ 𝑥 ∈ ( 𝑋 ∖ { 𝑍 } ) ∃ 𝑦 ∈ ( 𝑋 ∖ { 𝑍 } ) ( 𝑦 𝐻 𝑥 ) = ( GId ‘ 𝐻 ) ) ) )
7 1 4 idl0cl ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑖 ∈ ( Idl ‘ 𝑅 ) ) → 𝑍 ∈ 𝑖 )
8 7 adantr ⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝑖 ∈ ( Idl ‘ 𝑅 ) ) ∧ ∀ 𝑥 ∈ ( 𝑋 ∖ { 𝑍 } ) ∃ 𝑦 ∈ ( 𝑋 ∖ { 𝑍 } ) ( 𝑦 𝐻 𝑥 ) = ( GId ‘ 𝐻 ) ) → 𝑍 ∈ 𝑖 )
9 4 fvexi ⊢ 𝑍 ∈ V
10 9 snss ⊢ ( 𝑍 ∈ 𝑖 ↔ { 𝑍 } ⊆ 𝑖 )
11 necom ⊢ ( 𝑖 ≠ { 𝑍 } ↔ { 𝑍 } ≠ 𝑖 )
12 pssdifn0 ⊢ ( ( { 𝑍 } ⊆ 𝑖 ∧ { 𝑍 } ≠ 𝑖 ) → ( 𝑖 ∖ { 𝑍 } ) ≠ ∅ )
13 n0 ⊢ ( ( 𝑖 ∖ { 𝑍 } ) ≠ ∅ ↔ ∃ 𝑧 𝑧 ∈ ( 𝑖 ∖ { 𝑍 } ) )
14 12 13 sylib ⊢ ( ( { 𝑍 } ⊆ 𝑖 ∧ { 𝑍 } ≠ 𝑖 ) → ∃ 𝑧 𝑧 ∈ ( 𝑖 ∖ { 𝑍 } ) )
15 10 11 14 syl2anb ⊢ ( ( 𝑍 ∈ 𝑖 ∧ 𝑖 ≠ { 𝑍 } ) → ∃ 𝑧 𝑧 ∈ ( 𝑖 ∖ { 𝑍 } ) )
16 1 3 idlss ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑖 ∈ ( Idl ‘ 𝑅 ) ) → 𝑖 ⊆ 𝑋 )
17 ssdif ⊢ ( 𝑖 ⊆ 𝑋 → ( 𝑖 ∖ { 𝑍 } ) ⊆ ( 𝑋 ∖ { 𝑍 } ) )
18 17 sselda ⊢ ( ( 𝑖 ⊆ 𝑋 ∧ 𝑧 ∈ ( 𝑖 ∖ { 𝑍 } ) ) → 𝑧 ∈ ( 𝑋 ∖ { 𝑍 } ) )
19 16 18 sylan ⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝑖 ∈ ( Idl ‘ 𝑅 ) ) ∧ 𝑧 ∈ ( 𝑖 ∖ { 𝑍 } ) ) → 𝑧 ∈ ( 𝑋 ∖ { 𝑍 } ) )
20 oveq2 ⊢ ( 𝑥 = 𝑧 → ( 𝑦 𝐻 𝑥 ) = ( 𝑦 𝐻 𝑧 ) )
21 20 eqeq1d ⊢ ( 𝑥 = 𝑧 → ( ( 𝑦 𝐻 𝑥 ) = ( GId ‘ 𝐻 ) ↔ ( 𝑦 𝐻 𝑧 ) = ( GId ‘ 𝐻 ) ) )
22 21 rexbidv ⊢ ( 𝑥 = 𝑧 → ( ∃ 𝑦 ∈ ( 𝑋 ∖ { 𝑍 } ) ( 𝑦 𝐻 𝑥 ) = ( GId ‘ 𝐻 ) ↔ ∃ 𝑦 ∈ ( 𝑋 ∖ { 𝑍 } ) ( 𝑦 𝐻 𝑧 ) = ( GId ‘ 𝐻 ) ) )
23 22 rspcva ⊢ ( ( 𝑧 ∈ ( 𝑋 ∖ { 𝑍 } ) ∧ ∀ 𝑥 ∈ ( 𝑋 ∖ { 𝑍 } ) ∃ 𝑦 ∈ ( 𝑋 ∖ { 𝑍 } ) ( 𝑦 𝐻 𝑥 ) = ( GId ‘ 𝐻 ) ) → ∃ 𝑦 ∈ ( 𝑋 ∖ { 𝑍 } ) ( 𝑦 𝐻 𝑧 ) = ( GId ‘ 𝐻 ) )
24 19 23 sylan ⊢ ( ( ( ( 𝑅 ∈ RingOps ∧ 𝑖 ∈ ( Idl ‘ 𝑅 ) ) ∧ 𝑧 ∈ ( 𝑖 ∖ { 𝑍 } ) ) ∧ ∀ 𝑥 ∈ ( 𝑋 ∖ { 𝑍 } ) ∃ 𝑦 ∈ ( 𝑋 ∖ { 𝑍 } ) ( 𝑦 𝐻 𝑥 ) = ( GId ‘ 𝐻 ) ) → ∃ 𝑦 ∈ ( 𝑋 ∖ { 𝑍 } ) ( 𝑦 𝐻 𝑧 ) = ( GId ‘ 𝐻 ) )
25 eldifi ⊢ ( 𝑧 ∈ ( 𝑖 ∖ { 𝑍 } ) → 𝑧 ∈ 𝑖 )
26 eldifi ⊢ ( 𝑦 ∈ ( 𝑋 ∖ { 𝑍 } ) → 𝑦 ∈ 𝑋 )
27 25 26 anim12i ⊢ ( ( 𝑧 ∈ ( 𝑖 ∖ { 𝑍 } ) ∧ 𝑦 ∈ ( 𝑋 ∖ { 𝑍 } ) ) → ( 𝑧 ∈ 𝑖 ∧ 𝑦 ∈ 𝑋 ) )
28 1 2 3 idllmulcl ⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝑖 ∈ ( Idl ‘ 𝑅 ) ) ∧ ( 𝑧 ∈ 𝑖 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑦 𝐻 𝑧 ) ∈ 𝑖 )
29 1 2 3 5 1idl ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑖 ∈ ( Idl ‘ 𝑅 ) ) → ( ( GId ‘ 𝐻 ) ∈ 𝑖 ↔ 𝑖 = 𝑋 ) )
30 29 biimpd ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑖 ∈ ( Idl ‘ 𝑅 ) ) → ( ( GId ‘ 𝐻 ) ∈ 𝑖 → 𝑖 = 𝑋 ) )
31 30 adantr ⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝑖 ∈ ( Idl ‘ 𝑅 ) ) ∧ ( 𝑧 ∈ 𝑖 ∧ 𝑦 ∈ 𝑋 ) ) → ( ( GId ‘ 𝐻 ) ∈ 𝑖 → 𝑖 = 𝑋 ) )
32 eleq1 ⊢ ( ( 𝑦 𝐻 𝑧 ) = ( GId ‘ 𝐻 ) → ( ( 𝑦 𝐻 𝑧 ) ∈ 𝑖 ↔ ( GId ‘ 𝐻 ) ∈ 𝑖 ) )
33 32 imbi1d ⊢ ( ( 𝑦 𝐻 𝑧 ) = ( GId ‘ 𝐻 ) → ( ( ( 𝑦 𝐻 𝑧 ) ∈ 𝑖 → 𝑖 = 𝑋 ) ↔ ( ( GId ‘ 𝐻 ) ∈ 𝑖 → 𝑖 = 𝑋 ) ) )
34 31 33 syl5ibrcom ⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝑖 ∈ ( Idl ‘ 𝑅 ) ) ∧ ( 𝑧 ∈ 𝑖 ∧ 𝑦 ∈ 𝑋 ) ) → ( ( 𝑦 𝐻 𝑧 ) = ( GId ‘ 𝐻 ) → ( ( 𝑦 𝐻 𝑧 ) ∈ 𝑖 → 𝑖 = 𝑋 ) ) )
35 28 34 mpid ⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝑖 ∈ ( Idl ‘ 𝑅 ) ) ∧ ( 𝑧 ∈ 𝑖 ∧ 𝑦 ∈ 𝑋 ) ) → ( ( 𝑦 𝐻 𝑧 ) = ( GId ‘ 𝐻 ) → 𝑖 = 𝑋 ) )
36 27 35 sylan2 ⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝑖 ∈ ( Idl ‘ 𝑅 ) ) ∧ ( 𝑧 ∈ ( 𝑖 ∖ { 𝑍 } ) ∧ 𝑦 ∈ ( 𝑋 ∖ { 𝑍 } ) ) ) → ( ( 𝑦 𝐻 𝑧 ) = ( GId ‘ 𝐻 ) → 𝑖 = 𝑋 ) )
37 36 anassrs ⊢ ( ( ( ( 𝑅 ∈ RingOps ∧ 𝑖 ∈ ( Idl ‘ 𝑅 ) ) ∧ 𝑧 ∈ ( 𝑖 ∖ { 𝑍 } ) ) ∧ 𝑦 ∈ ( 𝑋 ∖ { 𝑍 } ) ) → ( ( 𝑦 𝐻 𝑧 ) = ( GId ‘ 𝐻 ) → 𝑖 = 𝑋 ) )
38 37 rexlimdva ⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝑖 ∈ ( Idl ‘ 𝑅 ) ) ∧ 𝑧 ∈ ( 𝑖 ∖ { 𝑍 } ) ) → ( ∃ 𝑦 ∈ ( 𝑋 ∖ { 𝑍 } ) ( 𝑦 𝐻 𝑧 ) = ( GId ‘ 𝐻 ) → 𝑖 = 𝑋 ) )
39 38 imp ⊢ ( ( ( ( 𝑅 ∈ RingOps ∧ 𝑖 ∈ ( Idl ‘ 𝑅 ) ) ∧ 𝑧 ∈ ( 𝑖 ∖ { 𝑍 } ) ) ∧ ∃ 𝑦 ∈ ( 𝑋 ∖ { 𝑍 } ) ( 𝑦 𝐻 𝑧 ) = ( GId ‘ 𝐻 ) ) → 𝑖 = 𝑋 )
40 24 39 syldan ⊢ ( ( ( ( 𝑅 ∈ RingOps ∧ 𝑖 ∈ ( Idl ‘ 𝑅 ) ) ∧ 𝑧 ∈ ( 𝑖 ∖ { 𝑍 } ) ) ∧ ∀ 𝑥 ∈ ( 𝑋 ∖ { 𝑍 } ) ∃ 𝑦 ∈ ( 𝑋 ∖ { 𝑍 } ) ( 𝑦 𝐻 𝑥 ) = ( GId ‘ 𝐻 ) ) → 𝑖 = 𝑋 )
41 40 an32s ⊢ ( ( ( ( 𝑅 ∈ RingOps ∧ 𝑖 ∈ ( Idl ‘ 𝑅 ) ) ∧ ∀ 𝑥 ∈ ( 𝑋 ∖ { 𝑍 } ) ∃ 𝑦 ∈ ( 𝑋 ∖ { 𝑍 } ) ( 𝑦 𝐻 𝑥 ) = ( GId ‘ 𝐻 ) ) ∧ 𝑧 ∈ ( 𝑖 ∖ { 𝑍 } ) ) → 𝑖 = 𝑋 )
42 41 ex ⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝑖 ∈ ( Idl ‘ 𝑅 ) ) ∧ ∀ 𝑥 ∈ ( 𝑋 ∖ { 𝑍 } ) ∃ 𝑦 ∈ ( 𝑋 ∖ { 𝑍 } ) ( 𝑦 𝐻 𝑥 ) = ( GId ‘ 𝐻 ) ) → ( 𝑧 ∈ ( 𝑖 ∖ { 𝑍 } ) → 𝑖 = 𝑋 ) )
43 42 exlimdv ⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝑖 ∈ ( Idl ‘ 𝑅 ) ) ∧ ∀ 𝑥 ∈ ( 𝑋 ∖ { 𝑍 } ) ∃ 𝑦 ∈ ( 𝑋 ∖ { 𝑍 } ) ( 𝑦 𝐻 𝑥 ) = ( GId ‘ 𝐻 ) ) → ( ∃ 𝑧 𝑧 ∈ ( 𝑖 ∖ { 𝑍 } ) → 𝑖 = 𝑋 ) )
44 15 43 syl5 ⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝑖 ∈ ( Idl ‘ 𝑅 ) ) ∧ ∀ 𝑥 ∈ ( 𝑋 ∖ { 𝑍 } ) ∃ 𝑦 ∈ ( 𝑋 ∖ { 𝑍 } ) ( 𝑦 𝐻 𝑥 ) = ( GId ‘ 𝐻 ) ) → ( ( 𝑍 ∈ 𝑖 ∧ 𝑖 ≠ { 𝑍 } ) → 𝑖 = 𝑋 ) )
45 8 44 mpand ⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝑖 ∈ ( Idl ‘ 𝑅 ) ) ∧ ∀ 𝑥 ∈ ( 𝑋 ∖ { 𝑍 } ) ∃ 𝑦 ∈ ( 𝑋 ∖ { 𝑍 } ) ( 𝑦 𝐻 𝑥 ) = ( GId ‘ 𝐻 ) ) → ( 𝑖 ≠ { 𝑍 } → 𝑖 = 𝑋 ) )
46 45 an32s ⊢ ( ( ( 𝑅 ∈ RingOps ∧ ∀ 𝑥 ∈ ( 𝑋 ∖ { 𝑍 } ) ∃ 𝑦 ∈ ( 𝑋 ∖ { 𝑍 } ) ( 𝑦 𝐻 𝑥 ) = ( GId ‘ 𝐻 ) ) ∧ 𝑖 ∈ ( Idl ‘ 𝑅 ) ) → ( 𝑖 ≠ { 𝑍 } → 𝑖 = 𝑋 ) )
47 neor ⊢ ( ( 𝑖 = { 𝑍 } ∨ 𝑖 = 𝑋 ) ↔ ( 𝑖 ≠ { 𝑍 } → 𝑖 = 𝑋 ) )
48 46 47 sylibr ⊢ ( ( ( 𝑅 ∈ RingOps ∧ ∀ 𝑥 ∈ ( 𝑋 ∖ { 𝑍 } ) ∃ 𝑦 ∈ ( 𝑋 ∖ { 𝑍 } ) ( 𝑦 𝐻 𝑥 ) = ( GId ‘ 𝐻 ) ) ∧ 𝑖 ∈ ( Idl ‘ 𝑅 ) ) → ( 𝑖 = { 𝑍 } ∨ 𝑖 = 𝑋 ) )
49 48 ex ⊢ ( ( 𝑅 ∈ RingOps ∧ ∀ 𝑥 ∈ ( 𝑋 ∖ { 𝑍 } ) ∃ 𝑦 ∈ ( 𝑋 ∖ { 𝑍 } ) ( 𝑦 𝐻 𝑥 ) = ( GId ‘ 𝐻 ) ) → ( 𝑖 ∈ ( Idl ‘ 𝑅 ) → ( 𝑖 = { 𝑍 } ∨ 𝑖 = 𝑋 ) ) )
50 1 4 0idl ⊢ ( 𝑅 ∈ RingOps → { 𝑍 } ∈ ( Idl ‘ 𝑅 ) )
51 eleq1 ⊢ ( 𝑖 = { 𝑍 } → ( 𝑖 ∈ ( Idl ‘ 𝑅 ) ↔ { 𝑍 } ∈ ( Idl ‘ 𝑅 ) ) )
52 50 51 syl5ibrcom ⊢ ( 𝑅 ∈ RingOps → ( 𝑖 = { 𝑍 } → 𝑖 ∈ ( Idl ‘ 𝑅 ) ) )
53 1 3 rngoidl ⊢ ( 𝑅 ∈ RingOps → 𝑋 ∈ ( Idl ‘ 𝑅 ) )
54 eleq1 ⊢ ( 𝑖 = 𝑋 → ( 𝑖 ∈ ( Idl ‘ 𝑅 ) ↔ 𝑋 ∈ ( Idl ‘ 𝑅 ) ) )
55 53 54 syl5ibrcom ⊢ ( 𝑅 ∈ RingOps → ( 𝑖 = 𝑋 → 𝑖 ∈ ( Idl ‘ 𝑅 ) ) )
56 52 55 jaod ⊢ ( 𝑅 ∈ RingOps → ( ( 𝑖 = { 𝑍 } ∨ 𝑖 = 𝑋 ) → 𝑖 ∈ ( Idl ‘ 𝑅 ) ) )
57 56 adantr ⊢ ( ( 𝑅 ∈ RingOps ∧ ∀ 𝑥 ∈ ( 𝑋 ∖ { 𝑍 } ) ∃ 𝑦 ∈ ( 𝑋 ∖ { 𝑍 } ) ( 𝑦 𝐻 𝑥 ) = ( GId ‘ 𝐻 ) ) → ( ( 𝑖 = { 𝑍 } ∨ 𝑖 = 𝑋 ) → 𝑖 ∈ ( Idl ‘ 𝑅 ) ) )
58 49 57 impbid ⊢ ( ( 𝑅 ∈ RingOps ∧ ∀ 𝑥 ∈ ( 𝑋 ∖ { 𝑍 } ) ∃ 𝑦 ∈ ( 𝑋 ∖ { 𝑍 } ) ( 𝑦 𝐻 𝑥 ) = ( GId ‘ 𝐻 ) ) → ( 𝑖 ∈ ( Idl ‘ 𝑅 ) ↔ ( 𝑖 = { 𝑍 } ∨ 𝑖 = 𝑋 ) ) )
59 vex ⊢ 𝑖 ∈ V
60 59 elpr ⊢ ( 𝑖 ∈ { { 𝑍 } , 𝑋 } ↔ ( 𝑖 = { 𝑍 } ∨ 𝑖 = 𝑋 ) )
61 58 60 bitr4di ⊢ ( ( 𝑅 ∈ RingOps ∧ ∀ 𝑥 ∈ ( 𝑋 ∖ { 𝑍 } ) ∃ 𝑦 ∈ ( 𝑋 ∖ { 𝑍 } ) ( 𝑦 𝐻 𝑥 ) = ( GId ‘ 𝐻 ) ) → ( 𝑖 ∈ ( Idl ‘ 𝑅 ) ↔ 𝑖 ∈ { { 𝑍 } , 𝑋 } ) )
62 61 eqrdv ⊢ ( ( 𝑅 ∈ RingOps ∧ ∀ 𝑥 ∈ ( 𝑋 ∖ { 𝑍 } ) ∃ 𝑦 ∈ ( 𝑋 ∖ { 𝑍 } ) ( 𝑦 𝐻 𝑥 ) = ( GId ‘ 𝐻 ) ) → ( Idl ‘ 𝑅 ) = { { 𝑍 } , 𝑋 } )
63 62 adantrl ⊢ ( ( 𝑅 ∈ RingOps ∧ ( ( GId ‘ 𝐻 ) ≠ 𝑍 ∧ ∀ 𝑥 ∈ ( 𝑋 ∖ { 𝑍 } ) ∃ 𝑦 ∈ ( 𝑋 ∖ { 𝑍 } ) ( 𝑦 𝐻 𝑥 ) = ( GId ‘ 𝐻 ) ) ) → ( Idl ‘ 𝑅 ) = { { 𝑍 } , 𝑋 } )
64 6 63 sylbi ⊢ ( 𝑅 ∈ DivRingOps → ( Idl ‘ 𝑅 ) = { { 𝑍 } , 𝑋 } )