Metamath Proof Explorer

Theorem rngoidl

Description: Obsolete theorem, use 2idl1 instead. A ring R is an R ideal. (Contributed by Jeff Madsen, 10-Jun-2010) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses rngidl.1 ⊢ G = 1 st ⁡ R
rngidl.2 ⊢ X = ran ⁡ G
Assertion rngoidl ⊢ R ∈ RingOps → X ∈ Idl ⁡ R

Proof

Step Hyp Ref Expression
1 rngidl.1 ⊢ G = 1 st ⁡ R
2 rngidl.2 ⊢ X = ran ⁡ G
3 ssidd ⊢ R ∈ RingOps → X ⊆ X
4 eqid ⊢ GId ⁡ G = GId ⁡ G
5 1 2 4 rngo0cl ⊢ R ∈ RingOps → GId ⁡ G ∈ X
6 1 2 rngogcl ⊢ R ∈ RingOps ∧ x ∈ X ∧ y ∈ X → x G y ∈ X
7 6 3expa ⊢ R ∈ RingOps ∧ x ∈ X ∧ y ∈ X → x G y ∈ X
8 7 ralrimiva ⊢ R ∈ RingOps ∧ x ∈ X → ∀ y ∈ X x G y ∈ X
9 eqid ⊢ 2 nd ⁡ R = 2 nd ⁡ R
10 1 9 2 rngocl ⊢ R ∈ RingOps ∧ z ∈ X ∧ x ∈ X → z 2 nd ⁡ R x ∈ X
11 10 3com23 ⊢ R ∈ RingOps ∧ x ∈ X ∧ z ∈ X → z 2 nd ⁡ R x ∈ X
12 1 9 2 rngocl ⊢ R ∈ RingOps ∧ x ∈ X ∧ z ∈ X → x 2 nd ⁡ R z ∈ X
13 11 12 jca ⊢ R ∈ RingOps ∧ x ∈ X ∧ z ∈ X → z 2 nd ⁡ R x ∈ X ∧ x 2 nd ⁡ R z ∈ X
14 13 3expa ⊢ R ∈ RingOps ∧ x ∈ X ∧ z ∈ X → z 2 nd ⁡ R x ∈ X ∧ x 2 nd ⁡ R z ∈ X
15 14 ralrimiva ⊢ R ∈ RingOps ∧ x ∈ X → ∀ z ∈ X z 2 nd ⁡ R x ∈ X ∧ x 2 nd ⁡ R z ∈ X
16 8 15 jca ⊢ R ∈ RingOps ∧ x ∈ X → ∀ y ∈ X x G y ∈ X ∧ ∀ z ∈ X z 2 nd ⁡ R x ∈ X ∧ x 2 nd ⁡ R z ∈ X
17 16 ralrimiva ⊢ R ∈ RingOps → ∀ x ∈ X ∀ y ∈ X x G y ∈ X ∧ ∀ z ∈ X z 2 nd ⁡ R x ∈ X ∧ x 2 nd ⁡ R z ∈ X
18 1 9 2 4 isidl ⊢ R ∈ RingOps → X ∈ Idl ⁡ R ↔ X ⊆ X ∧ GId ⁡ G ∈ X ∧ ∀ x ∈ X ∀ y ∈ X x G y ∈ X ∧ ∀ z ∈ X z 2 nd ⁡ R x ∈ X ∧ x 2 nd ⁡ R z ∈ X
19 3 5 17 18 mpbir3and ⊢ R ∈ RingOps → X ∈ Idl ⁡ R