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

Metamath Proof Explorer

Theorem isidlc

Description: The predicate "is an ideal of the commutative 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 isidlc ( 𝑅 ∈ CRingOps → ( 𝐼 ∈ ( Idl ‘ 𝑅 ) ↔ ( 𝐼 ⊆ 𝑋 ∧ 𝑍 ∈ 𝐼 ∧ ∀ 𝑥 ∈ 𝐼 ( ∀ 𝑦 ∈ 𝐼 ( 𝑥 𝐺 𝑦 ) ∈ 𝐼 ∧ ∀ 𝑧 ∈ 𝑋 ( 𝑧 𝐻 𝑥 ) ∈ 𝐼 ) ) ) )

Proof

Step Hyp Ref Expression
1 idlval.1 ⊢ 𝐺 = ( 1st ‘ 𝑅 )
2 idlval.2 ⊢ 𝐻 = ( 2nd ‘ 𝑅 )
3 idlval.3 ⊢ 𝑋 = ran 𝐺
4 idlval.4 ⊢ 𝑍 = ( GId ‘ 𝐺 )
5 crngorngo ⊢ ( 𝑅 ∈ CRingOps → 𝑅 ∈ RingOps )
6 1 2 3 4 isidl ⊢ ( 𝑅 ∈ RingOps → ( 𝐼 ∈ ( Idl ‘ 𝑅 ) ↔ ( 𝐼 ⊆ 𝑋 ∧ 𝑍 ∈ 𝐼 ∧ ∀ 𝑥 ∈ 𝐼 ( ∀ 𝑦 ∈ 𝐼 ( 𝑥 𝐺 𝑦 ) ∈ 𝐼 ∧ ∀ 𝑧 ∈ 𝑋 ( ( 𝑧 𝐻 𝑥 ) ∈ 𝐼 ∧ ( 𝑥 𝐻 𝑧 ) ∈ 𝐼 ) ) ) ) )
7 5 6 syl ⊢ ( 𝑅 ∈ CRingOps → ( 𝐼 ∈ ( Idl ‘ 𝑅 ) ↔ ( 𝐼 ⊆ 𝑋 ∧ 𝑍 ∈ 𝐼 ∧ ∀ 𝑥 ∈ 𝐼 ( ∀ 𝑦 ∈ 𝐼 ( 𝑥 𝐺 𝑦 ) ∈ 𝐼 ∧ ∀ 𝑧 ∈ 𝑋 ( ( 𝑧 𝐻 𝑥 ) ∈ 𝐼 ∧ ( 𝑥 𝐻 𝑧 ) ∈ 𝐼 ) ) ) ) )
8 ssel2 ⊢ ( ( 𝐼 ⊆ 𝑋 ∧ 𝑥 ∈ 𝐼 ) → 𝑥 ∈ 𝑋 )
9 1 2 3 crngocom ⊢ ( ( 𝑅 ∈ CRingOps ∧ 𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) → ( 𝑥 𝐻 𝑧 ) = ( 𝑧 𝐻 𝑥 ) )
10 9 eleq1d ⊢ ( ( 𝑅 ∈ CRingOps ∧ 𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) → ( ( 𝑥 𝐻 𝑧 ) ∈ 𝐼 ↔ ( 𝑧 𝐻 𝑥 ) ∈ 𝐼 ) )
11 10 biimprd ⊢ ( ( 𝑅 ∈ CRingOps ∧ 𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) → ( ( 𝑧 𝐻 𝑥 ) ∈ 𝐼 → ( 𝑥 𝐻 𝑧 ) ∈ 𝐼 ) )
12 11 3expa ⊢ ( ( ( 𝑅 ∈ CRingOps ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑧 ∈ 𝑋 ) → ( ( 𝑧 𝐻 𝑥 ) ∈ 𝐼 → ( 𝑥 𝐻 𝑧 ) ∈ 𝐼 ) )
13 12 pm4.71d ⊢ ( ( ( 𝑅 ∈ CRingOps ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑧 ∈ 𝑋 ) → ( ( 𝑧 𝐻 𝑥 ) ∈ 𝐼 ↔ ( ( 𝑧 𝐻 𝑥 ) ∈ 𝐼 ∧ ( 𝑥 𝐻 𝑧 ) ∈ 𝐼 ) ) )
14 13 bicomd ⊢ ( ( ( 𝑅 ∈ CRingOps ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑧 ∈ 𝑋 ) → ( ( ( 𝑧 𝐻 𝑥 ) ∈ 𝐼 ∧ ( 𝑥 𝐻 𝑧 ) ∈ 𝐼 ) ↔ ( 𝑧 𝐻 𝑥 ) ∈ 𝐼 ) )
15 14 ralbidva ⊢ ( ( 𝑅 ∈ CRingOps ∧ 𝑥 ∈ 𝑋 ) → ( ∀ 𝑧 ∈ 𝑋 ( ( 𝑧 𝐻 𝑥 ) ∈ 𝐼 ∧ ( 𝑥 𝐻 𝑧 ) ∈ 𝐼 ) ↔ ∀ 𝑧 ∈ 𝑋 ( 𝑧 𝐻 𝑥 ) ∈ 𝐼 ) )
16 15 anbi2d ⊢ ( ( 𝑅 ∈ CRingOps ∧ 𝑥 ∈ 𝑋 ) → ( ( ∀ 𝑦 ∈ 𝐼 ( 𝑥 𝐺 𝑦 ) ∈ 𝐼 ∧ ∀ 𝑧 ∈ 𝑋 ( ( 𝑧 𝐻 𝑥 ) ∈ 𝐼 ∧ ( 𝑥 𝐻 𝑧 ) ∈ 𝐼 ) ) ↔ ( ∀ 𝑦 ∈ 𝐼 ( 𝑥 𝐺 𝑦 ) ∈ 𝐼 ∧ ∀ 𝑧 ∈ 𝑋 ( 𝑧 𝐻 𝑥 ) ∈ 𝐼 ) ) )
17 8 16 sylan2 ⊢ ( ( 𝑅 ∈ CRingOps ∧ ( 𝐼 ⊆ 𝑋 ∧ 𝑥 ∈ 𝐼 ) ) → ( ( ∀ 𝑦 ∈ 𝐼 ( 𝑥 𝐺 𝑦 ) ∈ 𝐼 ∧ ∀ 𝑧 ∈ 𝑋 ( ( 𝑧 𝐻 𝑥 ) ∈ 𝐼 ∧ ( 𝑥 𝐻 𝑧 ) ∈ 𝐼 ) ) ↔ ( ∀ 𝑦 ∈ 𝐼 ( 𝑥 𝐺 𝑦 ) ∈ 𝐼 ∧ ∀ 𝑧 ∈ 𝑋 ( 𝑧 𝐻 𝑥 ) ∈ 𝐼 ) ) )
18 17 anassrs ⊢ ( ( ( 𝑅 ∈ CRingOps ∧ 𝐼 ⊆ 𝑋 ) ∧ 𝑥 ∈ 𝐼 ) → ( ( ∀ 𝑦 ∈ 𝐼 ( 𝑥 𝐺 𝑦 ) ∈ 𝐼 ∧ ∀ 𝑧 ∈ 𝑋 ( ( 𝑧 𝐻 𝑥 ) ∈ 𝐼 ∧ ( 𝑥 𝐻 𝑧 ) ∈ 𝐼 ) ) ↔ ( ∀ 𝑦 ∈ 𝐼 ( 𝑥 𝐺 𝑦 ) ∈ 𝐼 ∧ ∀ 𝑧 ∈ 𝑋 ( 𝑧 𝐻 𝑥 ) ∈ 𝐼 ) ) )
19 18 ralbidva ⊢ ( ( 𝑅 ∈ CRingOps ∧ 𝐼 ⊆ 𝑋 ) → ( ∀ 𝑥 ∈ 𝐼 ( ∀ 𝑦 ∈ 𝐼 ( 𝑥 𝐺 𝑦 ) ∈ 𝐼 ∧ ∀ 𝑧 ∈ 𝑋 ( ( 𝑧 𝐻 𝑥 ) ∈ 𝐼 ∧ ( 𝑥 𝐻 𝑧 ) ∈ 𝐼 ) ) ↔ ∀ 𝑥 ∈ 𝐼 ( ∀ 𝑦 ∈ 𝐼 ( 𝑥 𝐺 𝑦 ) ∈ 𝐼 ∧ ∀ 𝑧 ∈ 𝑋 ( 𝑧 𝐻 𝑥 ) ∈ 𝐼 ) ) )
20 19 adantrr ⊢ ( ( 𝑅 ∈ CRingOps ∧ ( 𝐼 ⊆ 𝑋 ∧ 𝑍 ∈ 𝐼 ) ) → ( ∀ 𝑥 ∈ 𝐼 ( ∀ 𝑦 ∈ 𝐼 ( 𝑥 𝐺 𝑦 ) ∈ 𝐼 ∧ ∀ 𝑧 ∈ 𝑋 ( ( 𝑧 𝐻 𝑥 ) ∈ 𝐼 ∧ ( 𝑥 𝐻 𝑧 ) ∈ 𝐼 ) ) ↔ ∀ 𝑥 ∈ 𝐼 ( ∀ 𝑦 ∈ 𝐼 ( 𝑥 𝐺 𝑦 ) ∈ 𝐼 ∧ ∀ 𝑧 ∈ 𝑋 ( 𝑧 𝐻 𝑥 ) ∈ 𝐼 ) ) )
21 20 pm5.32da ⊢ ( 𝑅 ∈ CRingOps → ( ( ( 𝐼 ⊆ 𝑋 ∧ 𝑍 ∈ 𝐼 ) ∧ ∀ 𝑥 ∈ 𝐼 ( ∀ 𝑦 ∈ 𝐼 ( 𝑥 𝐺 𝑦 ) ∈ 𝐼 ∧ ∀ 𝑧 ∈ 𝑋 ( ( 𝑧 𝐻 𝑥 ) ∈ 𝐼 ∧ ( 𝑥 𝐻 𝑧 ) ∈ 𝐼 ) ) ) ↔ ( ( 𝐼 ⊆ 𝑋 ∧ 𝑍 ∈ 𝐼 ) ∧ ∀ 𝑥 ∈ 𝐼 ( ∀ 𝑦 ∈ 𝐼 ( 𝑥 𝐺 𝑦 ) ∈ 𝐼 ∧ ∀ 𝑧 ∈ 𝑋 ( 𝑧 𝐻 𝑥 ) ∈ 𝐼 ) ) ) )
22 df-3an ⊢ ( ( 𝐼 ⊆ 𝑋 ∧ 𝑍 ∈ 𝐼 ∧ ∀ 𝑥 ∈ 𝐼 ( ∀ 𝑦 ∈ 𝐼 ( 𝑥 𝐺 𝑦 ) ∈ 𝐼 ∧ ∀ 𝑧 ∈ 𝑋 ( ( 𝑧 𝐻 𝑥 ) ∈ 𝐼 ∧ ( 𝑥 𝐻 𝑧 ) ∈ 𝐼 ) ) ) ↔ ( ( 𝐼 ⊆ 𝑋 ∧ 𝑍 ∈ 𝐼 ) ∧ ∀ 𝑥 ∈ 𝐼 ( ∀ 𝑦 ∈ 𝐼 ( 𝑥 𝐺 𝑦 ) ∈ 𝐼 ∧ ∀ 𝑧 ∈ 𝑋 ( ( 𝑧 𝐻 𝑥 ) ∈ 𝐼 ∧ ( 𝑥 𝐻 𝑧 ) ∈ 𝐼 ) ) ) )
23 df-3an ⊢ ( ( 𝐼 ⊆ 𝑋 ∧ 𝑍 ∈ 𝐼 ∧ ∀ 𝑥 ∈ 𝐼 ( ∀ 𝑦 ∈ 𝐼 ( 𝑥 𝐺 𝑦 ) ∈ 𝐼 ∧ ∀ 𝑧 ∈ 𝑋 ( 𝑧 𝐻 𝑥 ) ∈ 𝐼 ) ) ↔ ( ( 𝐼 ⊆ 𝑋 ∧ 𝑍 ∈ 𝐼 ) ∧ ∀ 𝑥 ∈ 𝐼 ( ∀ 𝑦 ∈ 𝐼 ( 𝑥 𝐺 𝑦 ) ∈ 𝐼 ∧ ∀ 𝑧 ∈ 𝑋 ( 𝑧 𝐻 𝑥 ) ∈ 𝐼 ) ) )
24 21 22 23 3bitr4g ⊢ ( 𝑅 ∈ CRingOps → ( ( 𝐼 ⊆ 𝑋 ∧ 𝑍 ∈ 𝐼 ∧ ∀ 𝑥 ∈ 𝐼 ( ∀ 𝑦 ∈ 𝐼 ( 𝑥 𝐺 𝑦 ) ∈ 𝐼 ∧ ∀ 𝑧 ∈ 𝑋 ( ( 𝑧 𝐻 𝑥 ) ∈ 𝐼 ∧ ( 𝑥 𝐻 𝑧 ) ∈ 𝐼 ) ) ) ↔ ( 𝐼 ⊆ 𝑋 ∧ 𝑍 ∈ 𝐼 ∧ ∀ 𝑥 ∈ 𝐼 ( ∀ 𝑦 ∈ 𝐼 ( 𝑥 𝐺 𝑦 ) ∈ 𝐼 ∧ ∀ 𝑧 ∈ 𝑋 ( 𝑧 𝐻 𝑥 ) ∈ 𝐼 ) ) ) )
25 7 24 bitrd ⊢ ( 𝑅 ∈ CRingOps → ( 𝐼 ∈ ( Idl ‘ 𝑅 ) ↔ ( 𝐼 ⊆ 𝑋 ∧ 𝑍 ∈ 𝐼 ∧ ∀ 𝑥 ∈ 𝐼 ( ∀ 𝑦 ∈ 𝐼 ( 𝑥 𝐺 𝑦 ) ∈ 𝐼 ∧ ∀ 𝑧 ∈ 𝑋 ( 𝑧 𝐻 𝑥 ) ∈ 𝐼 ) ) ) )