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	syl5bb	⊢ ( 𝐾 ∈ 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 ‘ 𝐾 ) = { { 𝑍 } , 𝑋 } ) )