Theorem isidl

Description: Obsolete theorem, use df2idl2 instead. The predicate "is an ideal of the ring R ". (Contributed by Jeff Madsen, 10-Jun-2010) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypotheses	idlval.1	⊢ 𝐺 = ( 1st ‘ 𝑅 )
	idlval.2	⊢ 𝐻 = ( 2nd ‘ 𝑅 )
	idlval.3	⊢ 𝑋 = ran 𝐺
	idlval.4	⊢ 𝑍 = ( GId ‘ 𝐺 )
Assertion	isidl	⊢ ( 𝑅 ∈ RingOps → ( 𝐼 ∈ ( Idl ‘ 𝑅 ) ↔ ( 𝐼 ⊆ 𝑋 ∧ 𝑍 ∈ 𝐼 ∧ ∀ 𝑥 ∈ 𝐼 ( ∀ 𝑦 ∈ 𝐼 ( 𝑥 𝐺 𝑦 ) ∈ 𝐼 ∧ ∀ 𝑧 ∈ 𝑋 ( ( 𝑧 𝐻 𝑥 ) ∈ 𝐼 ∧ ( 𝑥 𝐻 𝑧 ) ∈ 𝐼 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		idlval.1	⊢ 𝐺 = ( 1st ‘ 𝑅 )
2		idlval.2	⊢ 𝐻 = ( 2nd ‘ 𝑅 )
3		idlval.3	⊢ 𝑋 = ran 𝐺
4		idlval.4	⊢ 𝑍 = ( GId ‘ 𝐺 )
5	1 2 3 4	idlval	⊢ ( 𝑅 ∈ RingOps → ( Idl ‘ 𝑅 ) = { 𝑖 ∈ 𝒫 𝑋 ∣ ( 𝑍 ∈ 𝑖 ∧ ∀ 𝑥 ∈ 𝑖 ( ∀ 𝑦 ∈ 𝑖 ( 𝑥 𝐺 𝑦 ) ∈ 𝑖 ∧ ∀ 𝑧 ∈ 𝑋 ( ( 𝑧 𝐻 𝑥 ) ∈ 𝑖 ∧ ( 𝑥 𝐻 𝑧 ) ∈ 𝑖 ) ) ) } )
6	5	eleq2d	⊢ ( 𝑅 ∈ RingOps → ( 𝐼 ∈ ( Idl ‘ 𝑅 ) ↔ 𝐼 ∈ { 𝑖 ∈ 𝒫 𝑋 ∣ ( 𝑍 ∈ 𝑖 ∧ ∀ 𝑥 ∈ 𝑖 ( ∀ 𝑦 ∈ 𝑖 ( 𝑥 𝐺 𝑦 ) ∈ 𝑖 ∧ ∀ 𝑧 ∈ 𝑋 ( ( 𝑧 𝐻 𝑥 ) ∈ 𝑖 ∧ ( 𝑥 𝐻 𝑧 ) ∈ 𝑖 ) ) ) } ) )
7	1	fvexi	⊢ 𝐺 ∈ V
8	7	rnex	⊢ ran 𝐺 ∈ V
9	3 8	eqeltri	⊢ 𝑋 ∈ V
10	9	elpw2	⊢ ( 𝐼 ∈ 𝒫 𝑋 ↔ 𝐼 ⊆ 𝑋 )
11	10	anbi1i	⊢ ( ( 𝐼 ∈ 𝒫 𝑋 ∧ ( 𝑍 ∈ 𝐼 ∧ ∀ 𝑥 ∈ 𝐼 ( ∀ 𝑦 ∈ 𝐼 ( 𝑥 𝐺 𝑦 ) ∈ 𝐼 ∧ ∀ 𝑧 ∈ 𝑋 ( ( 𝑧 𝐻 𝑥 ) ∈ 𝐼 ∧ ( 𝑥 𝐻 𝑧 ) ∈ 𝐼 ) ) ) ) ↔ ( 𝐼 ⊆ 𝑋 ∧ ( 𝑍 ∈ 𝐼 ∧ ∀ 𝑥 ∈ 𝐼 ( ∀ 𝑦 ∈ 𝐼 ( 𝑥 𝐺 𝑦 ) ∈ 𝐼 ∧ ∀ 𝑧 ∈ 𝑋 ( ( 𝑧 𝐻 𝑥 ) ∈ 𝐼 ∧ ( 𝑥 𝐻 𝑧 ) ∈ 𝐼 ) ) ) ) )
12		eleq2	⊢ ( 𝑖 = 𝐼 → ( 𝑍 ∈ 𝑖 ↔ 𝑍 ∈ 𝐼 ) )
13		eleq2	⊢ ( 𝑖 = 𝐼 → ( ( 𝑥 𝐺 𝑦 ) ∈ 𝑖 ↔ ( 𝑥 𝐺 𝑦 ) ∈ 𝐼 ) )
14	13	raleqbi1dv	⊢ ( 𝑖 = 𝐼 → ( ∀ 𝑦 ∈ 𝑖 ( 𝑥 𝐺 𝑦 ) ∈ 𝑖 ↔ ∀ 𝑦 ∈ 𝐼 ( 𝑥 𝐺 𝑦 ) ∈ 𝐼 ) )
15		eleq2	⊢ ( 𝑖 = 𝐼 → ( ( 𝑧 𝐻 𝑥 ) ∈ 𝑖 ↔ ( 𝑧 𝐻 𝑥 ) ∈ 𝐼 ) )
16		eleq2	⊢ ( 𝑖 = 𝐼 → ( ( 𝑥 𝐻 𝑧 ) ∈ 𝑖 ↔ ( 𝑥 𝐻 𝑧 ) ∈ 𝐼 ) )
17	15 16	anbi12d	⊢ ( 𝑖 = 𝐼 → ( ( ( 𝑧 𝐻 𝑥 ) ∈ 𝑖 ∧ ( 𝑥 𝐻 𝑧 ) ∈ 𝑖 ) ↔ ( ( 𝑧 𝐻 𝑥 ) ∈ 𝐼 ∧ ( 𝑥 𝐻 𝑧 ) ∈ 𝐼 ) ) )
18	17	ralbidv	⊢ ( 𝑖 = 𝐼 → ( ∀ 𝑧 ∈ 𝑋 ( ( 𝑧 𝐻 𝑥 ) ∈ 𝑖 ∧ ( 𝑥 𝐻 𝑧 ) ∈ 𝑖 ) ↔ ∀ 𝑧 ∈ 𝑋 ( ( 𝑧 𝐻 𝑥 ) ∈ 𝐼 ∧ ( 𝑥 𝐻 𝑧 ) ∈ 𝐼 ) ) )
19	14 18	anbi12d	⊢ ( 𝑖 = 𝐼 → ( ( ∀ 𝑦 ∈ 𝑖 ( 𝑥 𝐺 𝑦 ) ∈ 𝑖 ∧ ∀ 𝑧 ∈ 𝑋 ( ( 𝑧 𝐻 𝑥 ) ∈ 𝑖 ∧ ( 𝑥 𝐻 𝑧 ) ∈ 𝑖 ) ) ↔ ( ∀ 𝑦 ∈ 𝐼 ( 𝑥 𝐺 𝑦 ) ∈ 𝐼 ∧ ∀ 𝑧 ∈ 𝑋 ( ( 𝑧 𝐻 𝑥 ) ∈ 𝐼 ∧ ( 𝑥 𝐻 𝑧 ) ∈ 𝐼 ) ) ) )
20	19	raleqbi1dv	⊢ ( 𝑖 = 𝐼 → ( ∀ 𝑥 ∈ 𝑖 ( ∀ 𝑦 ∈ 𝑖 ( 𝑥 𝐺 𝑦 ) ∈ 𝑖 ∧ ∀ 𝑧 ∈ 𝑋 ( ( 𝑧 𝐻 𝑥 ) ∈ 𝑖 ∧ ( 𝑥 𝐻 𝑧 ) ∈ 𝑖 ) ) ↔ ∀ 𝑥 ∈ 𝐼 ( ∀ 𝑦 ∈ 𝐼 ( 𝑥 𝐺 𝑦 ) ∈ 𝐼 ∧ ∀ 𝑧 ∈ 𝑋 ( ( 𝑧 𝐻 𝑥 ) ∈ 𝐼 ∧ ( 𝑥 𝐻 𝑧 ) ∈ 𝐼 ) ) ) )
21	12 20	anbi12d	⊢ ( 𝑖 = 𝐼 → ( ( 𝑍 ∈ 𝑖 ∧ ∀ 𝑥 ∈ 𝑖 ( ∀ 𝑦 ∈ 𝑖 ( 𝑥 𝐺 𝑦 ) ∈ 𝑖 ∧ ∀ 𝑧 ∈ 𝑋 ( ( 𝑧 𝐻 𝑥 ) ∈ 𝑖 ∧ ( 𝑥 𝐻 𝑧 ) ∈ 𝑖 ) ) ) ↔ ( 𝑍 ∈ 𝐼 ∧ ∀ 𝑥 ∈ 𝐼 ( ∀ 𝑦 ∈ 𝐼 ( 𝑥 𝐺 𝑦 ) ∈ 𝐼 ∧ ∀ 𝑧 ∈ 𝑋 ( ( 𝑧 𝐻 𝑥 ) ∈ 𝐼 ∧ ( 𝑥 𝐻 𝑧 ) ∈ 𝐼 ) ) ) ) )
22	21	elrab	⊢ ( 𝐼 ∈ { 𝑖 ∈ 𝒫 𝑋 ∣ ( 𝑍 ∈ 𝑖 ∧ ∀ 𝑥 ∈ 𝑖 ( ∀ 𝑦 ∈ 𝑖 ( 𝑥 𝐺 𝑦 ) ∈ 𝑖 ∧ ∀ 𝑧 ∈ 𝑋 ( ( 𝑧 𝐻 𝑥 ) ∈ 𝑖 ∧ ( 𝑥 𝐻 𝑧 ) ∈ 𝑖 ) ) ) } ↔ ( 𝐼 ∈ 𝒫 𝑋 ∧ ( 𝑍 ∈ 𝐼 ∧ ∀ 𝑥 ∈ 𝐼 ( ∀ 𝑦 ∈ 𝐼 ( 𝑥 𝐺 𝑦 ) ∈ 𝐼 ∧ ∀ 𝑧 ∈ 𝑋 ( ( 𝑧 𝐻 𝑥 ) ∈ 𝐼 ∧ ( 𝑥 𝐻 𝑧 ) ∈ 𝐼 ) ) ) ) )
23		3anass	⊢ ( ( 𝐼 ⊆ 𝑋 ∧ 𝑍 ∈ 𝐼 ∧ ∀ 𝑥 ∈ 𝐼 ( ∀ 𝑦 ∈ 𝐼 ( 𝑥 𝐺 𝑦 ) ∈ 𝐼 ∧ ∀ 𝑧 ∈ 𝑋 ( ( 𝑧 𝐻 𝑥 ) ∈ 𝐼 ∧ ( 𝑥 𝐻 𝑧 ) ∈ 𝐼 ) ) ) ↔ ( 𝐼 ⊆ 𝑋 ∧ ( 𝑍 ∈ 𝐼 ∧ ∀ 𝑥 ∈ 𝐼 ( ∀ 𝑦 ∈ 𝐼 ( 𝑥 𝐺 𝑦 ) ∈ 𝐼 ∧ ∀ 𝑧 ∈ 𝑋 ( ( 𝑧 𝐻 𝑥 ) ∈ 𝐼 ∧ ( 𝑥 𝐻 𝑧 ) ∈ 𝐼 ) ) ) ) )
24	11 22 23	3bitr4i	⊢ ( 𝐼 ∈ { 𝑖 ∈ 𝒫 𝑋 ∣ ( 𝑍 ∈ 𝑖 ∧ ∀ 𝑥 ∈ 𝑖 ( ∀ 𝑦 ∈ 𝑖 ( 𝑥 𝐺 𝑦 ) ∈ 𝑖 ∧ ∀ 𝑧 ∈ 𝑋 ( ( 𝑧 𝐻 𝑥 ) ∈ 𝑖 ∧ ( 𝑥 𝐻 𝑧 ) ∈ 𝑖 ) ) ) } ↔ ( 𝐼 ⊆ 𝑋 ∧ 𝑍 ∈ 𝐼 ∧ ∀ 𝑥 ∈ 𝐼 ( ∀ 𝑦 ∈ 𝐼 ( 𝑥 𝐺 𝑦 ) ∈ 𝐼 ∧ ∀ 𝑧 ∈ 𝑋 ( ( 𝑧 𝐻 𝑥 ) ∈ 𝐼 ∧ ( 𝑥 𝐻 𝑧 ) ∈ 𝐼 ) ) ) )
25	6 24	bitrdi	⊢ ( 𝑅 ∈ RingOps → ( 𝐼 ∈ ( Idl ‘ 𝑅 ) ↔ ( 𝐼 ⊆ 𝑋 ∧ 𝑍 ∈ 𝐼 ∧ ∀ 𝑥 ∈ 𝐼 ( ∀ 𝑦 ∈ 𝐼 ( 𝑥 𝐺 𝑦 ) ∈ 𝐼 ∧ ∀ 𝑧 ∈ 𝑋 ( ( 𝑧 𝐻 𝑥 ) ∈ 𝐼 ∧ ( 𝑥 𝐻 𝑧 ) ∈ 𝐼 ) ) ) ) )