Metamath Proof Explorer

Theorem 0idl

Description: The set containing only 0 is an ideal. (Contributed by Jeff Madsen, 10-Jun-2010)

Ref Expression
Hypotheses 0idl.1 ⊢ G = 1 st ⁡ R
0idl.2 ⊢ Z = GId ⁡ G
Assertion 0idl ⊢ R ∈ RingOps → Z ∈ Idl ⁡ R

Proof

Step Hyp Ref Expression
1 0idl.1 ⊢ G = 1 st ⁡ R
2 0idl.2 ⊢ Z = GId ⁡ G
3 eqid ⊢ ran ⁡ G = ran ⁡ G
4 1 3 2 rngo0cl ⊢ R ∈ RingOps → Z ∈ ran ⁡ G
5 4 snssd ⊢ R ∈ RingOps → Z ⊆ ran ⁡ G
6 2 fvexi ⊢ Z ∈ V
7 6 snid ⊢ Z ∈ Z
8 7 a1i ⊢ R ∈ RingOps → Z ∈ Z
9 velsn ⊢ x ∈ Z ↔ x = Z
10 velsn ⊢ y ∈ Z ↔ y = Z
11 1 3 2 rngo0rid ⊢ R ∈ RingOps ∧ Z ∈ ran ⁡ G → Z G Z = Z
12 4 11 mpdan ⊢ R ∈ RingOps → Z G Z = Z
13 ovex ⊢ Z G Z ∈ V
14 13 elsn ⊢ Z G Z ∈ Z ↔ Z G Z = Z
15 12 14 sylibr ⊢ R ∈ RingOps → Z G Z ∈ Z
16 oveq2 ⊢ y = Z → Z G y = Z G Z
17 16 eleq1d ⊢ y = Z → Z G y ∈ Z ↔ Z G Z ∈ Z
18 15 17 syl5ibrcom ⊢ R ∈ RingOps → y = Z → Z G y ∈ Z
19 10 18 biimtrid ⊢ R ∈ RingOps → y ∈ Z → Z G y ∈ Z
20 19 ralrimiv ⊢ R ∈ RingOps → ∀ y ∈ Z Z G y ∈ Z
21 eqid ⊢ 2 nd ⁡ R = 2 nd ⁡ R
22 2 3 1 21 rngorz ⊢ R ∈ RingOps ∧ z ∈ ran ⁡ G → z 2 nd ⁡ R Z = Z
23 ovex ⊢ z 2 nd ⁡ R Z ∈ V
24 23 elsn ⊢ z 2 nd ⁡ R Z ∈ Z ↔ z 2 nd ⁡ R Z = Z
25 22 24 sylibr ⊢ R ∈ RingOps ∧ z ∈ ran ⁡ G → z 2 nd ⁡ R Z ∈ Z
26 2 3 1 21 rngolz ⊢ R ∈ RingOps ∧ z ∈ ran ⁡ G → Z 2 nd ⁡ R z = Z
27 ovex ⊢ Z 2 nd ⁡ R z ∈ V
28 27 elsn ⊢ Z 2 nd ⁡ R z ∈ Z ↔ Z 2 nd ⁡ R z = Z
29 26 28 sylibr ⊢ R ∈ RingOps ∧ z ∈ ran ⁡ G → Z 2 nd ⁡ R z ∈ Z
30 25 29 jca ⊢ R ∈ RingOps ∧ z ∈ ran ⁡ G → z 2 nd ⁡ R Z ∈ Z ∧ Z 2 nd ⁡ R z ∈ Z
31 30 ralrimiva ⊢ R ∈ RingOps → ∀ z ∈ ran ⁡ G z 2 nd ⁡ R Z ∈ Z ∧ Z 2 nd ⁡ R z ∈ Z
32 20 31 jca ⊢ R ∈ RingOps → ∀ y ∈ Z Z G y ∈ Z ∧ ∀ z ∈ ran ⁡ G z 2 nd ⁡ R Z ∈ Z ∧ Z 2 nd ⁡ R z ∈ Z
33 oveq1 ⊢ x = Z → x G y = Z G y
34 33 eleq1d ⊢ x = Z → x G y ∈ Z ↔ Z G y ∈ Z
35 34 ralbidv ⊢ x = Z → ∀ y ∈ Z x G y ∈ Z ↔ ∀ y ∈ Z Z G y ∈ Z
36 oveq2 ⊢ x = Z → z 2 nd ⁡ R x = z 2 nd ⁡ R Z
37 36 eleq1d ⊢ x = Z → z 2 nd ⁡ R x ∈ Z ↔ z 2 nd ⁡ R Z ∈ Z
38 oveq1 ⊢ x = Z → x 2 nd ⁡ R z = Z 2 nd ⁡ R z
39 38 eleq1d ⊢ x = Z → x 2 nd ⁡ R z ∈ Z ↔ Z 2 nd ⁡ R z ∈ Z
40 37 39 anbi12d ⊢ x = Z → z 2 nd ⁡ R x ∈ Z ∧ x 2 nd ⁡ R z ∈ Z ↔ z 2 nd ⁡ R Z ∈ Z ∧ Z 2 nd ⁡ R z ∈ Z
41 40 ralbidv ⊢ x = Z → ∀ z ∈ ran ⁡ G z 2 nd ⁡ R x ∈ Z ∧ x 2 nd ⁡ R z ∈ Z ↔ ∀ z ∈ ran ⁡ G z 2 nd ⁡ R Z ∈ Z ∧ Z 2 nd ⁡ R z ∈ Z
42 35 41 anbi12d ⊢ x = Z → ∀ y ∈ Z x G y ∈ Z ∧ ∀ z ∈ ran ⁡ G z 2 nd ⁡ R x ∈ Z ∧ x 2 nd ⁡ R z ∈ Z ↔ ∀ y ∈ Z Z G y ∈ Z ∧ ∀ z ∈ ran ⁡ G z 2 nd ⁡ R Z ∈ Z ∧ Z 2 nd ⁡ R z ∈ Z
43 32 42 syl5ibrcom ⊢ R ∈ RingOps → x = Z → ∀ y ∈ Z x G y ∈ Z ∧ ∀ z ∈ ran ⁡ G z 2 nd ⁡ R x ∈ Z ∧ x 2 nd ⁡ R z ∈ Z
44 9 43 biimtrid ⊢ R ∈ RingOps → x ∈ Z → ∀ y ∈ Z x G y ∈ Z ∧ ∀ z ∈ ran ⁡ G z 2 nd ⁡ R x ∈ Z ∧ x 2 nd ⁡ R z ∈ Z
45 44 ralrimiv ⊢ R ∈ RingOps → ∀ x ∈ Z ∀ y ∈ Z x G y ∈ Z ∧ ∀ z ∈ ran ⁡ G z 2 nd ⁡ R x ∈ Z ∧ x 2 nd ⁡ R z ∈ Z
46 1 21 3 2 isidl ⊢ R ∈ RingOps → Z ∈ Idl ⁡ R ↔ Z ⊆ ran ⁡ G ∧ Z ∈ Z ∧ ∀ x ∈ Z ∀ y ∈ Z x G y ∈ Z ∧ ∀ z ∈ ran ⁡ G z 2 nd ⁡ R x ∈ Z ∧ x 2 nd ⁡ R z ∈ Z
47 5 8 45 46 mpbir3and ⊢ R ∈ RingOps → Z ∈ Idl ⁡ R