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

Metamath Proof Explorer

Theorem isfldidl

Description: Determine if a ring is a field based on its ideals. (Contributed by Jeff Madsen, 10-Jun-2010)

Ref Expression
Hypotheses isfldidl.1 ⊢ 𝐺 = ( 1st ‘ 𝐾 )
isfldidl.2 ⊢ 𝐻 = ( 2nd ‘ 𝐾 )
isfldidl.3 ⊢ 𝑋 = ran 𝐺
isfldidl.4 ⊢ 𝑍 = ( GId ‘ 𝐺 )
isfldidl.5 ⊢ 𝑈 = ( GId ‘ 𝐻 )
Assertion isfldidl ( 𝐾 ∈ Fld ↔ ( 𝐾 ∈ CRingOps ∧ 𝑈 ≠ 𝑍 ∧ ( Idl ‘ 𝐾 ) = { { 𝑍 } , 𝑋 } ) )

Proof

Step Hyp Ref Expression
1 isfldidl.1 ⊢ 𝐺 = ( 1st ‘ 𝐾 )
2 isfldidl.2 ⊢ 𝐻 = ( 2nd ‘ 𝐾 )
3 isfldidl.3 ⊢ 𝑋 = ran 𝐺
4 isfldidl.4 ⊢ 𝑍 = ( GId ‘ 𝐺 )
5 isfldidl.5 ⊢ 𝑈 = ( GId ‘ 𝐻 )
6 fldcrngo ⊢ ( 𝐾 ∈ Fld → 𝐾 ∈ CRingOps )
7 flddivrng ⊢ ( 𝐾 ∈ Fld → 𝐾 ∈ DivRingOps )
8 1 2 3 4 5 dvrunz ⊢ ( 𝐾 ∈ DivRingOps → 𝑈 ≠ 𝑍 )
9 7 8 syl ⊢ ( 𝐾 ∈ Fld → 𝑈 ≠ 𝑍 )
10 1 2 3 4 divrngidl ⊢ ( 𝐾 ∈ DivRingOps → ( Idl ‘ 𝐾 ) = { { 𝑍 } , 𝑋 } )
11 7 10 syl ⊢ ( 𝐾 ∈ Fld → ( Idl ‘ 𝐾 ) = { { 𝑍 } , 𝑋 } )
12 6 9 11 3jca ⊢ ( 𝐾 ∈ Fld → ( 𝐾 ∈ CRingOps ∧ 𝑈 ≠ 𝑍 ∧ ( Idl ‘ 𝐾 ) = { { 𝑍 } , 𝑋 } ) )
13 crngorngo ⊢ ( 𝐾 ∈ CRingOps → 𝐾 ∈ RingOps )
14 13 3ad2ant1 ⊢ ( ( 𝐾 ∈ CRingOps ∧ 𝑈 ≠ 𝑍 ∧ ( Idl ‘ 𝐾 ) = { { 𝑍 } , 𝑋 } ) → 𝐾 ∈ RingOps )
15 simp2 ⊢ ( ( 𝐾 ∈ CRingOps ∧ 𝑈 ≠ 𝑍 ∧ ( Idl ‘ 𝐾 ) = { { 𝑍 } , 𝑋 } ) → 𝑈 ≠ 𝑍 )
16 1 rneqi ⊢ ran 𝐺 = ran ( 1st ‘ 𝐾 )
17 3 16 eqtri ⊢ 𝑋 = ran ( 1st ‘ 𝐾 )
18 17 2 5 rngo1cl ⊢ ( 𝐾 ∈ RingOps → 𝑈 ∈ 𝑋 )
19 13 18 syl ⊢ ( 𝐾 ∈ CRingOps → 𝑈 ∈ 𝑋 )
20 19 ad2antrr ⊢ ( ( ( 𝐾 ∈ CRingOps ∧ ( Idl ‘ 𝐾 ) = { { 𝑍 } , 𝑋 } ) ∧ 𝑥 ∈ ( 𝑋 ∖ { 𝑍 } ) ) → 𝑈 ∈ 𝑋 )
21 eldif ⊢ ( 𝑥 ∈ ( 𝑋 ∖ { 𝑍 } ) ↔ ( 𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ { 𝑍 } ) )
22 snssi ⊢ ( 𝑥 ∈ 𝑋 → { 𝑥 } ⊆ 𝑋 )
23 1 3 igenss ⊢ ( ( 𝐾 ∈ RingOps ∧ { 𝑥 } ⊆ 𝑋 ) → { 𝑥 } ⊆ ( 𝐾 IdlGen { 𝑥 } ) )
24 22 23 sylan2 ⊢ ( ( 𝐾 ∈ RingOps ∧ 𝑥 ∈ 𝑋 ) → { 𝑥 } ⊆ ( 𝐾 IdlGen { 𝑥 } ) )
25 vex ⊢ 𝑥 ∈ V
26 25 snss ⊢ ( 𝑥 ∈ ( 𝐾 IdlGen { 𝑥 } ) ↔ { 𝑥 } ⊆ ( 𝐾 IdlGen { 𝑥 } ) )
27 26 biimpri ⊢ ( { 𝑥 } ⊆ ( 𝐾 IdlGen { 𝑥 } ) → 𝑥 ∈ ( 𝐾 IdlGen { 𝑥 } ) )
28 eleq2 ⊢ ( ( 𝐾 IdlGen { 𝑥 } ) = { 𝑍 } → ( 𝑥 ∈ ( 𝐾 IdlGen { 𝑥 } ) ↔ 𝑥 ∈ { 𝑍 } ) )
29 27 28 syl5ibcom ⊢ ( { 𝑥 } ⊆ ( 𝐾 IdlGen { 𝑥 } ) → ( ( 𝐾 IdlGen { 𝑥 } ) = { 𝑍 } → 𝑥 ∈ { 𝑍 } ) )
30 29 con3dimp ⊢ ( ( { 𝑥 } ⊆ ( 𝐾 IdlGen { 𝑥 } ) ∧ ¬ 𝑥 ∈ { 𝑍 } ) → ¬ ( 𝐾 IdlGen { 𝑥 } ) = { 𝑍 } )
31 24 30 sylan ⊢ ( ( ( 𝐾 ∈ RingOps ∧ 𝑥 ∈ 𝑋 ) ∧ ¬ 𝑥 ∈ { 𝑍 } ) → ¬ ( 𝐾 IdlGen { 𝑥 } ) = { 𝑍 } )
32 31 anasss ⊢ ( ( 𝐾 ∈ RingOps ∧ ( 𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ { 𝑍 } ) ) → ¬ ( 𝐾 IdlGen { 𝑥 } ) = { 𝑍 } )
33 21 32 sylan2b ⊢ ( ( 𝐾 ∈ RingOps ∧ 𝑥 ∈ ( 𝑋 ∖ { 𝑍 } ) ) → ¬ ( 𝐾 IdlGen { 𝑥 } ) = { 𝑍 } )
34 33 adantlr ⊢ ( ( ( 𝐾 ∈ RingOps ∧ ( Idl ‘ 𝐾 ) = { { 𝑍 } , 𝑋 } ) ∧ 𝑥 ∈ ( 𝑋 ∖ { 𝑍 } ) ) → ¬ ( 𝐾 IdlGen { 𝑥 } ) = { 𝑍 } )
35 eldifi ⊢ ( 𝑥 ∈ ( 𝑋 ∖ { 𝑍 } ) → 𝑥 ∈ 𝑋 )
36 35 snssd ⊢ ( 𝑥 ∈ ( 𝑋 ∖ { 𝑍 } ) → { 𝑥 } ⊆ 𝑋 )
37 1 3 igenidl ⊢ ( ( 𝐾 ∈ RingOps ∧ { 𝑥 } ⊆ 𝑋 ) → ( 𝐾 IdlGen { 𝑥 } ) ∈ ( Idl ‘ 𝐾 ) )
38 36 37 sylan2 ⊢ ( ( 𝐾 ∈ RingOps ∧ 𝑥 ∈ ( 𝑋 ∖ { 𝑍 } ) ) → ( 𝐾 IdlGen { 𝑥 } ) ∈ ( Idl ‘ 𝐾 ) )
39 eleq2 ⊢ ( ( Idl ‘ 𝐾 ) = { { 𝑍 } , 𝑋 } → ( ( 𝐾 IdlGen { 𝑥 } ) ∈ ( Idl ‘ 𝐾 ) ↔ ( 𝐾 IdlGen { 𝑥 } ) ∈ { { 𝑍 } , 𝑋 } ) )
40 38 39 syl5ibcom ⊢ ( ( 𝐾 ∈ RingOps ∧ 𝑥 ∈ ( 𝑋 ∖ { 𝑍 } ) ) → ( ( Idl ‘ 𝐾 ) = { { 𝑍 } , 𝑋 } → ( 𝐾 IdlGen { 𝑥 } ) ∈ { { 𝑍 } , 𝑋 } ) )
41 40 imp ⊢ ( ( ( 𝐾 ∈ RingOps ∧ 𝑥 ∈ ( 𝑋 ∖ { 𝑍 } ) ) ∧ ( Idl ‘ 𝐾 ) = { { 𝑍 } , 𝑋 } ) → ( 𝐾 IdlGen { 𝑥 } ) ∈ { { 𝑍 } , 𝑋 } )
42 41 an32s ⊢ ( ( ( 𝐾 ∈ RingOps ∧ ( Idl ‘ 𝐾 ) = { { 𝑍 } , 𝑋 } ) ∧ 𝑥 ∈ ( 𝑋 ∖ { 𝑍 } ) ) → ( 𝐾 IdlGen { 𝑥 } ) ∈ { { 𝑍 } , 𝑋 } )
43 ovex ⊢ ( 𝐾 IdlGen { 𝑥 } ) ∈ V
44 43 elpr ⊢ ( ( 𝐾 IdlGen { 𝑥 } ) ∈ { { 𝑍 } , 𝑋 } ↔ ( ( 𝐾 IdlGen { 𝑥 } ) = { 𝑍 } ∨ ( 𝐾 IdlGen { 𝑥 } ) = 𝑋 ) )
45 42 44 sylib ⊢ ( ( ( 𝐾 ∈ RingOps ∧ ( Idl ‘ 𝐾 ) = { { 𝑍 } , 𝑋 } ) ∧ 𝑥 ∈ ( 𝑋 ∖ { 𝑍 } ) ) → ( ( 𝐾 IdlGen { 𝑥 } ) = { 𝑍 } ∨ ( 𝐾 IdlGen { 𝑥 } ) = 𝑋 ) )
46 45 ord ⊢ ( ( ( 𝐾 ∈ RingOps ∧ ( Idl ‘ 𝐾 ) = { { 𝑍 } , 𝑋 } ) ∧ 𝑥 ∈ ( 𝑋 ∖ { 𝑍 } ) ) → ( ¬ ( 𝐾 IdlGen { 𝑥 } ) = { 𝑍 } → ( 𝐾 IdlGen { 𝑥 } ) = 𝑋 ) )
47 34 46 mpd ⊢ ( ( ( 𝐾 ∈ RingOps ∧ ( Idl ‘ 𝐾 ) = { { 𝑍 } , 𝑋 } ) ∧ 𝑥 ∈ ( 𝑋 ∖ { 𝑍 } ) ) → ( 𝐾 IdlGen { 𝑥 } ) = 𝑋 )
48 13 47 sylanl1 ⊢ ( ( ( 𝐾 ∈ CRingOps ∧ ( Idl ‘ 𝐾 ) = { { 𝑍 } , 𝑋 } ) ∧ 𝑥 ∈ ( 𝑋 ∖ { 𝑍 } ) ) → ( 𝐾 IdlGen { 𝑥 } ) = 𝑋 )
49 1 2 3 prnc ⊢ ( ( 𝐾 ∈ CRingOps ∧ 𝑥 ∈ 𝑋 ) → ( 𝐾 IdlGen { 𝑥 } ) = { 𝑧 ∈ 𝑋 ∣ ∃ 𝑦 ∈ 𝑋 𝑧 = ( 𝑦 𝐻 𝑥 ) } )
50 35 49 sylan2 ⊢ ( ( 𝐾 ∈ CRingOps ∧ 𝑥 ∈ ( 𝑋 ∖ { 𝑍 } ) ) → ( 𝐾 IdlGen { 𝑥 } ) = { 𝑧 ∈ 𝑋 ∣ ∃ 𝑦 ∈ 𝑋 𝑧 = ( 𝑦 𝐻 𝑥 ) } )
51 50 adantlr ⊢ ( ( ( 𝐾 ∈ CRingOps ∧ ( Idl ‘ 𝐾 ) = { { 𝑍 } , 𝑋 } ) ∧ 𝑥 ∈ ( 𝑋 ∖ { 𝑍 } ) ) → ( 𝐾 IdlGen { 𝑥 } ) = { 𝑧 ∈ 𝑋 ∣ ∃ 𝑦 ∈ 𝑋 𝑧 = ( 𝑦 𝐻 𝑥 ) } )
52 48 51 eqtr3d ⊢ ( ( ( 𝐾 ∈ CRingOps ∧ ( Idl ‘ 𝐾 ) = { { 𝑍 } , 𝑋 } ) ∧ 𝑥 ∈ ( 𝑋 ∖ { 𝑍 } ) ) → 𝑋 = { 𝑧 ∈ 𝑋 ∣ ∃ 𝑦 ∈ 𝑋 𝑧 = ( 𝑦 𝐻 𝑥 ) } )
53 20 52 eleqtrd ⊢ ( ( ( 𝐾 ∈ CRingOps ∧ ( Idl ‘ 𝐾 ) = { { 𝑍 } , 𝑋 } ) ∧ 𝑥 ∈ ( 𝑋 ∖ { 𝑍 } ) ) → 𝑈 ∈ { 𝑧 ∈ 𝑋 ∣ ∃ 𝑦 ∈ 𝑋 𝑧 = ( 𝑦 𝐻 𝑥 ) } )
54 eqeq1 ⊢ ( 𝑧 = 𝑈 → ( 𝑧 = ( 𝑦 𝐻 𝑥 ) ↔ 𝑈 = ( 𝑦 𝐻 𝑥 ) ) )
55 54 rexbidv ⊢ ( 𝑧 = 𝑈 → ( ∃ 𝑦 ∈ 𝑋 𝑧 = ( 𝑦 𝐻 𝑥 ) ↔ ∃ 𝑦 ∈ 𝑋 𝑈 = ( 𝑦 𝐻 𝑥 ) ) )
56 55 elrab ⊢ ( 𝑈 ∈ { 𝑧 ∈ 𝑋 ∣ ∃ 𝑦 ∈ 𝑋 𝑧 = ( 𝑦 𝐻 𝑥 ) } ↔ ( 𝑈 ∈ 𝑋 ∧ ∃ 𝑦 ∈ 𝑋 𝑈 = ( 𝑦 𝐻 𝑥 ) ) )
57 53 56 sylib ⊢ ( ( ( 𝐾 ∈ CRingOps ∧ ( Idl ‘ 𝐾 ) = { { 𝑍 } , 𝑋 } ) ∧ 𝑥 ∈ ( 𝑋 ∖ { 𝑍 } ) ) → ( 𝑈 ∈ 𝑋 ∧ ∃ 𝑦 ∈ 𝑋 𝑈 = ( 𝑦 𝐻 𝑥 ) ) )
58 57 simprd ⊢ ( ( ( 𝐾 ∈ CRingOps ∧ ( Idl ‘ 𝐾 ) = { { 𝑍 } , 𝑋 } ) ∧ 𝑥 ∈ ( 𝑋 ∖ { 𝑍 } ) ) → ∃ 𝑦 ∈ 𝑋 𝑈 = ( 𝑦 𝐻 𝑥 ) )
59 eqcom ⊢ ( ( 𝑦 𝐻 𝑥 ) = 𝑈 ↔ 𝑈 = ( 𝑦 𝐻 𝑥 ) )
60 59 rexbii ⊢ ( ∃ 𝑦 ∈ 𝑋 ( 𝑦 𝐻 𝑥 ) = 𝑈 ↔ ∃ 𝑦 ∈ 𝑋 𝑈 = ( 𝑦 𝐻 𝑥 ) )
61 58 60 sylibr ⊢ ( ( ( 𝐾 ∈ CRingOps ∧ ( Idl ‘ 𝐾 ) = { { 𝑍 } , 𝑋 } ) ∧ 𝑥 ∈ ( 𝑋 ∖ { 𝑍 } ) ) → ∃ 𝑦 ∈ 𝑋 ( 𝑦 𝐻 𝑥 ) = 𝑈 )
62 61 ralrimiva ⊢ ( ( 𝐾 ∈ CRingOps ∧ ( Idl ‘ 𝐾 ) = { { 𝑍 } , 𝑋 } ) → ∀ 𝑥 ∈ ( 𝑋 ∖ { 𝑍 } ) ∃ 𝑦 ∈ 𝑋 ( 𝑦 𝐻 𝑥 ) = 𝑈 )
63 62 3adant2 ⊢ ( ( 𝐾 ∈ CRingOps ∧ 𝑈 ≠ 𝑍 ∧ ( Idl ‘ 𝐾 ) = { { 𝑍 } , 𝑋 } ) → ∀ 𝑥 ∈ ( 𝑋 ∖ { 𝑍 } ) ∃ 𝑦 ∈ 𝑋 ( 𝑦 𝐻 𝑥 ) = 𝑈 )
64 14 15 63 jca32 ⊢ ( ( 𝐾 ∈ CRingOps ∧ 𝑈 ≠ 𝑍 ∧ ( Idl ‘ 𝐾 ) = { { 𝑍 } , 𝑋 } ) → ( 𝐾 ∈ RingOps ∧ ( 𝑈 ≠ 𝑍 ∧ ∀ 𝑥 ∈ ( 𝑋 ∖ { 𝑍 } ) ∃ 𝑦 ∈ 𝑋 ( 𝑦 𝐻 𝑥 ) = 𝑈 ) ) )
65 1 2 4 3 5 isdrngo3 ⊢ ( 𝐾 ∈ DivRingOps ↔ ( 𝐾 ∈ RingOps ∧ ( 𝑈 ≠ 𝑍 ∧ ∀ 𝑥 ∈ ( 𝑋 ∖ { 𝑍 } ) ∃ 𝑦 ∈ 𝑋 ( 𝑦 𝐻 𝑥 ) = 𝑈 ) ) )
66 64 65 sylibr ⊢ ( ( 𝐾 ∈ CRingOps ∧ 𝑈 ≠ 𝑍 ∧ ( Idl ‘ 𝐾 ) = { { 𝑍 } , 𝑋 } ) → 𝐾 ∈ DivRingOps )
67 simp1 ⊢ ( ( 𝐾 ∈ CRingOps ∧ 𝑈 ≠ 𝑍 ∧ ( Idl ‘ 𝐾 ) = { { 𝑍 } , 𝑋 } ) → 𝐾 ∈ CRingOps )
68 isfld2 ⊢ ( 𝐾 ∈ Fld ↔ ( 𝐾 ∈ DivRingOps ∧ 𝐾 ∈ CRingOps ) )
69 66 67 68 sylanbrc ⊢ ( ( 𝐾 ∈ CRingOps ∧ 𝑈 ≠ 𝑍 ∧ ( Idl ‘ 𝐾 ) = { { 𝑍 } , 𝑋 } ) → 𝐾 ∈ Fld )
70 12 69 impbii ⊢ ( 𝐾 ∈ Fld ↔ ( 𝐾 ∈ CRingOps ∧ 𝑈 ≠ 𝑍 ∧ ( Idl ‘ 𝐾 ) = { { 𝑍 } , 𝑋 } ) )