Metamath Proof Explorer

Theorem isidl

Description: The predicate "is an ideal of the ring R ". (Contributed by Jeff Madsen, 10-Jun-2010)

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 ‘ 𝑅 ) ↔ ( 𝐼 ⊆ 𝑋 ∧ 𝑍 ∈ 𝐼 ∧ ∀ 𝑥 ∈ 𝐼 ( ∀ 𝑦 ∈ 𝐼 ( 𝑥 𝐺 𝑦 ) ∈ 𝐼 ∧ ∀ 𝑧 ∈ 𝑋 ( ( 𝑧 𝐻 𝑥 ) ∈ 𝐼 ∧ ( 𝑥 𝐻 𝑧 ) ∈ 𝐼 ) ) ) ) )