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

Metamath Proof Explorer

Theorem isfldidl2

Description: Determine if a ring is a field based on its ideals. (Contributed by Jeff Madsen, 6-Jan-2011)

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

Proof

Step Hyp Ref Expression
1 isfldidl2.1 ⊢ 𝐺 = ( 1st ‘ 𝐾 )
2 isfldidl2.2 ⊢ 𝐻 = ( 2nd ‘ 𝐾 )
3 isfldidl2.3 ⊢ 𝑋 = ran 𝐺
4 isfldidl2.4 ⊢ 𝑍 = ( GId ‘ 𝐺 )
5 eqid ⊢ ( GId ‘ 𝐻 ) = ( GId ‘ 𝐻 )
6 1 2 3 4 5 isfldidl ⊢ ( 𝐾 ∈ Fld ↔ ( 𝐾 ∈ CRingOps ∧ ( GId ‘ 𝐻 ) ≠ 𝑍 ∧ ( Idl ‘ 𝐾 ) = { { 𝑍 } , 𝑋 } ) )
7 crngorngo ⊢ ( 𝐾 ∈ CRingOps → 𝐾 ∈ RingOps )
8 eqcom ⊢ ( ( GId ‘ 𝐻 ) = 𝑍 ↔ 𝑍 = ( GId ‘ 𝐻 ) )
9 1 2 3 4 5 0rngo ⊢ ( 𝐾 ∈ RingOps → ( 𝑍 = ( GId ‘ 𝐻 ) ↔ 𝑋 = { 𝑍 } ) )
10 8 9 bitrid ⊢ ( 𝐾 ∈ RingOps → ( ( GId ‘ 𝐻 ) = 𝑍 ↔ 𝑋 = { 𝑍 } ) )
11 7 10 syl ⊢ ( 𝐾 ∈ CRingOps → ( ( GId ‘ 𝐻 ) = 𝑍 ↔ 𝑋 = { 𝑍 } ) )
12 11 necon3bid ⊢ ( 𝐾 ∈ CRingOps → ( ( GId ‘ 𝐻 ) ≠ 𝑍 ↔ 𝑋 ≠ { 𝑍 } ) )
13 12 anbi1d ⊢ ( 𝐾 ∈ CRingOps → ( ( ( GId ‘ 𝐻 ) ≠ 𝑍 ∧ ( Idl ‘ 𝐾 ) = { { 𝑍 } , 𝑋 } ) ↔ ( 𝑋 ≠ { 𝑍 } ∧ ( Idl ‘ 𝐾 ) = { { 𝑍 } , 𝑋 } ) ) )
14 13 pm5.32i ⊢ ( ( 𝐾 ∈ CRingOps ∧ ( ( GId ‘ 𝐻 ) ≠ 𝑍 ∧ ( Idl ‘ 𝐾 ) = { { 𝑍 } , 𝑋 } ) ) ↔ ( 𝐾 ∈ CRingOps ∧ ( 𝑋 ≠ { 𝑍 } ∧ ( Idl ‘ 𝐾 ) = { { 𝑍 } , 𝑋 } ) ) )
15 3anass ⊢ ( ( 𝐾 ∈ CRingOps ∧ ( GId ‘ 𝐻 ) ≠ 𝑍 ∧ ( Idl ‘ 𝐾 ) = { { 𝑍 } , 𝑋 } ) ↔ ( 𝐾 ∈ CRingOps ∧ ( ( GId ‘ 𝐻 ) ≠ 𝑍 ∧ ( Idl ‘ 𝐾 ) = { { 𝑍 } , 𝑋 } ) ) )
16 3anass ⊢ ( ( 𝐾 ∈ CRingOps ∧ 𝑋 ≠ { 𝑍 } ∧ ( Idl ‘ 𝐾 ) = { { 𝑍 } , 𝑋 } ) ↔ ( 𝐾 ∈ CRingOps ∧ ( 𝑋 ≠ { 𝑍 } ∧ ( Idl ‘ 𝐾 ) = { { 𝑍 } , 𝑋 } ) ) )
17 14 15 16 3bitr4i ⊢ ( ( 𝐾 ∈ CRingOps ∧ ( GId ‘ 𝐻 ) ≠ 𝑍 ∧ ( Idl ‘ 𝐾 ) = { { 𝑍 } , 𝑋 } ) ↔ ( 𝐾 ∈ CRingOps ∧ 𝑋 ≠ { 𝑍 } ∧ ( Idl ‘ 𝐾 ) = { { 𝑍 } , 𝑋 } ) )
18 6 17 bitri ⊢ ( 𝐾 ∈ Fld ↔ ( 𝐾 ∈ CRingOps ∧ 𝑋 ≠ { 𝑍 } ∧ ( Idl ‘ 𝐾 ) = { { 𝑍 } , 𝑋 } ) )