Metamath Proof Explorer

Theorem df2idl2crng

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

Ref Expression
Hypotheses df2idl2crng.u ⊢ 𝑈 = ( 2Ideal ‘ 𝑅 )
df2idl2crng.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
df2idl2crng.t ⊢ · = ( .r ‘ 𝑅 )
Assertion df2idl2crng ( 𝑅 ∈ CRing → ( 𝐼 ∈ 𝑈 ↔ ( 𝐼 ∈ ( SubGrp ‘ 𝑅 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐼 ( 𝑥 · 𝑦 ) ∈ 𝐼 ) ) )

Proof

Step Hyp Ref Expression
1 df2idl2crng.u ⊢ 𝑈 = ( 2Ideal ‘ 𝑅 )
2 df2idl2crng.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
3 df2idl2crng.t ⊢ · = ( .r ‘ 𝑅 )
4 crngring ⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
5 1 2 3 df2idl2 ⊢ ( 𝑅 ∈ Ring → ( 𝐼 ∈ 𝑈 ↔ ( 𝐼 ∈ ( SubGrp ‘ 𝑅 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐼 ( ( 𝑥 · 𝑦 ) ∈ 𝐼 ∧ ( 𝑦 · 𝑥 ) ∈ 𝐼 ) ) ) )
6 4 5 syl ⊢ ( 𝑅 ∈ CRing → ( 𝐼 ∈ 𝑈 ↔ ( 𝐼 ∈ ( SubGrp ‘ 𝑅 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐼 ( ( 𝑥 · 𝑦 ) ∈ 𝐼 ∧ ( 𝑦 · 𝑥 ) ∈ 𝐼 ) ) ) )
7 simpll ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( SubGrp ‘ 𝑅 ) ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐼 ) ) → 𝑅 ∈ CRing )
8 simpl ⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐼 ) → 𝑥 ∈ 𝐵 )
9 8 adantl ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( SubGrp ‘ 𝑅 ) ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐼 ) ) → 𝑥 ∈ 𝐵 )
10 2 subgss ⊢ ( 𝐼 ∈ ( SubGrp ‘ 𝑅 ) → 𝐼 ⊆ 𝐵 )
11 10 adantl ⊢ ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( SubGrp ‘ 𝑅 ) ) → 𝐼 ⊆ 𝐵 )
12 11 sseld ⊢ ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( SubGrp ‘ 𝑅 ) ) → ( 𝑦 ∈ 𝐼 → 𝑦 ∈ 𝐵 ) )
13 12 adantld ⊢ ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( SubGrp ‘ 𝑅 ) ) → ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐼 ) → 𝑦 ∈ 𝐵 ) )
14 13 imp ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( SubGrp ‘ 𝑅 ) ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐼 ) ) → 𝑦 ∈ 𝐵 )
15 2 3 7 9 14 crngcomd ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( SubGrp ‘ 𝑅 ) ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐼 ) ) → ( 𝑥 · 𝑦 ) = ( 𝑦 · 𝑥 ) )
16 15 eleq1d ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( SubGrp ‘ 𝑅 ) ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐼 ) ) → ( ( 𝑥 · 𝑦 ) ∈ 𝐼 ↔ ( 𝑦 · 𝑥 ) ∈ 𝐼 ) )
17 16 pm4.71da ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( SubGrp ‘ 𝑅 ) ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐼 ) ) → ( ( 𝑥 · 𝑦 ) ∈ 𝐼 ↔ ( ( 𝑥 · 𝑦 ) ∈ 𝐼 ∧ ( 𝑦 · 𝑥 ) ∈ 𝐼 ) ) )
18 17 bicomd ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( SubGrp ‘ 𝑅 ) ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐼 ) ) → ( ( ( 𝑥 · 𝑦 ) ∈ 𝐼 ∧ ( 𝑦 · 𝑥 ) ∈ 𝐼 ) ↔ ( 𝑥 · 𝑦 ) ∈ 𝐼 ) )
19 18 2ralbidva ⊢ ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( SubGrp ‘ 𝑅 ) ) → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐼 ( ( 𝑥 · 𝑦 ) ∈ 𝐼 ∧ ( 𝑦 · 𝑥 ) ∈ 𝐼 ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐼 ( 𝑥 · 𝑦 ) ∈ 𝐼 ) )
20 19 pm5.32da ⊢ ( 𝑅 ∈ CRing → ( ( 𝐼 ∈ ( SubGrp ‘ 𝑅 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐼 ( ( 𝑥 · 𝑦 ) ∈ 𝐼 ∧ ( 𝑦 · 𝑥 ) ∈ 𝐼 ) ) ↔ ( 𝐼 ∈ ( SubGrp ‘ 𝑅 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐼 ( 𝑥 · 𝑦 ) ∈ 𝐼 ) ) )
21 6 20 bitrd ⊢ ( 𝑅 ∈ CRing → ( 𝐼 ∈ 𝑈 ↔ ( 𝐼 ∈ ( SubGrp ‘ 𝑅 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐼 ( 𝑥 · 𝑦 ) ∈ 𝐼 ) ) )