Metamath Proof Explorer

Theorem prnc

Description: A principal ideal (an ideal generated by one element) in a commutative ring. (Contributed by Jeff Madsen, 10-Jun-2010)

Ref Expression
Hypotheses prnc.1 ⊢ G = 1 st ⁡ R
prnc.2 ⊢ H = 2 nd ⁡ R
prnc.3 ⊢ X = ran ⁡ G
Assertion prnc ⊢ R ∈ CRingOps ∧ A ∈ X → R IdlGen A = x ∈ X | ∃ y ∈ X x = y H A

Proof

Step Hyp Ref Expression
1 prnc.1 ⊢ G = 1 st ⁡ R
2 prnc.2 ⊢ H = 2 nd ⁡ R
3 prnc.3 ⊢ X = ran ⁡ G
4 crngorngo ⊢ R ∈ CRingOps → R ∈ RingOps
5 ssrab2 ⊢ x ∈ X | ∃ y ∈ X x = y H A ⊆ X
6 5 a1i ⊢ R ∈ RingOps ∧ A ∈ X → x ∈ X | ∃ y ∈ X x = y H A ⊆ X
7 eqid ⊢ GId ⁡ G = GId ⁡ G
8 1 3 7 rngo0cl ⊢ R ∈ RingOps → GId ⁡ G ∈ X
9 8 adantr ⊢ R ∈ RingOps ∧ A ∈ X → GId ⁡ G ∈ X
10 7 3 1 2 rngolz ⊢ R ∈ RingOps ∧ A ∈ X → GId ⁡ G H A = GId ⁡ G
11 10 eqcomd ⊢ R ∈ RingOps ∧ A ∈ X → GId ⁡ G = GId ⁡ G H A
12 oveq1 ⊢ y = GId ⁡ G → y H A = GId ⁡ G H A
13 12 rspceeqv ⊢ GId ⁡ G ∈ X ∧ GId ⁡ G = GId ⁡ G H A → ∃ y ∈ X GId ⁡ G = y H A
14 9 11 13 syl2anc ⊢ R ∈ RingOps ∧ A ∈ X → ∃ y ∈ X GId ⁡ G = y H A
15 eqeq1 ⊢ x = GId ⁡ G → x = y H A ↔ GId ⁡ G = y H A
16 15 rexbidv ⊢ x = GId ⁡ G → ∃ y ∈ X x = y H A ↔ ∃ y ∈ X GId ⁡ G = y H A
17 16 elrab ⊢ GId ⁡ G ∈ x ∈ X | ∃ y ∈ X x = y H A ↔ GId ⁡ G ∈ X ∧ ∃ y ∈ X GId ⁡ G = y H A
18 9 14 17 sylanbrc ⊢ R ∈ RingOps ∧ A ∈ X → GId ⁡ G ∈ x ∈ X | ∃ y ∈ X x = y H A
19 eqeq1 ⊢ x = u → x = y H A ↔ u = y H A
20 19 rexbidv ⊢ x = u → ∃ y ∈ X x = y H A ↔ ∃ y ∈ X u = y H A
21 oveq1 ⊢ y = r → y H A = r H A
22 21 eqeq2d ⊢ y = r → u = y H A ↔ u = r H A
23 22 cbvrexvw ⊢ ∃ y ∈ X u = y H A ↔ ∃ r ∈ X u = r H A
24 20 23 bitrdi ⊢ x = u → ∃ y ∈ X x = y H A ↔ ∃ r ∈ X u = r H A
25 24 elrab ⊢ u ∈ x ∈ X | ∃ y ∈ X x = y H A ↔ u ∈ X ∧ ∃ r ∈ X u = r H A
26 eqeq1 ⊢ x = v → x = y H A ↔ v = y H A
27 26 rexbidv ⊢ x = v → ∃ y ∈ X x = y H A ↔ ∃ y ∈ X v = y H A
28 oveq1 ⊢ y = s → y H A = s H A
29 28 eqeq2d ⊢ y = s → v = y H A ↔ v = s H A
30 29 cbvrexvw ⊢ ∃ y ∈ X v = y H A ↔ ∃ s ∈ X v = s H A
31 27 30 bitrdi ⊢ x = v → ∃ y ∈ X x = y H A ↔ ∃ s ∈ X v = s H A
32 31 elrab ⊢ v ∈ x ∈ X | ∃ y ∈ X x = y H A ↔ v ∈ X ∧ ∃ s ∈ X v = s H A
33 1 2 3 rngodir ⊢ R ∈ RingOps ∧ r ∈ X ∧ s ∈ X ∧ A ∈ X → r G s H A = r H A G s H A
34 33 3exp2 ⊢ R ∈ RingOps → r ∈ X → s ∈ X → A ∈ X → r G s H A = r H A G s H A
35 34 imp42 ⊢ R ∈ RingOps ∧ r ∈ X ∧ s ∈ X ∧ A ∈ X → r G s H A = r H A G s H A
36 1 3 rngogcl ⊢ R ∈ RingOps ∧ r ∈ X ∧ s ∈ X → r G s ∈ X
37 36 3expib ⊢ R ∈ RingOps → r ∈ X ∧ s ∈ X → r G s ∈ X
38 37 imdistani ⊢ R ∈ RingOps ∧ r ∈ X ∧ s ∈ X → R ∈ RingOps ∧ r G s ∈ X
39 1 2 3 rngocl ⊢ R ∈ RingOps ∧ r G s ∈ X ∧ A ∈ X → r G s H A ∈ X
40 39 3expa ⊢ R ∈ RingOps ∧ r G s ∈ X ∧ A ∈ X → r G s H A ∈ X
41 eqid ⊢ r G s H A = r G s H A
42 oveq1 ⊢ y = r G s → y H A = r G s H A
43 42 rspceeqv ⊢ r G s ∈ X ∧ r G s H A = r G s H A → ∃ y ∈ X r G s H A = y H A
44 41 43 mpan2 ⊢ r G s ∈ X → ∃ y ∈ X r G s H A = y H A
45 44 ad2antlr ⊢ R ∈ RingOps ∧ r G s ∈ X ∧ A ∈ X → ∃ y ∈ X r G s H A = y H A
46 eqeq1 ⊢ x = r G s H A → x = y H A ↔ r G s H A = y H A
47 46 rexbidv ⊢ x = r G s H A → ∃ y ∈ X x = y H A ↔ ∃ y ∈ X r G s H A = y H A
48 47 elrab ⊢ r G s H A ∈ x ∈ X | ∃ y ∈ X x = y H A ↔ r G s H A ∈ X ∧ ∃ y ∈ X r G s H A = y H A
49 40 45 48 sylanbrc ⊢ R ∈ RingOps ∧ r G s ∈ X ∧ A ∈ X → r G s H A ∈ x ∈ X | ∃ y ∈ X x = y H A
50 38 49 sylan ⊢ R ∈ RingOps ∧ r ∈ X ∧ s ∈ X ∧ A ∈ X → r G s H A ∈ x ∈ X | ∃ y ∈ X x = y H A
51 35 50 eqeltrrd ⊢ R ∈ RingOps ∧ r ∈ X ∧ s ∈ X ∧ A ∈ X → r H A G s H A ∈ x ∈ X | ∃ y ∈ X x = y H A
52 51 an32s ⊢ R ∈ RingOps ∧ A ∈ X ∧ r ∈ X ∧ s ∈ X → r H A G s H A ∈ x ∈ X | ∃ y ∈ X x = y H A
53 52 anassrs ⊢ R ∈ RingOps ∧ A ∈ X ∧ r ∈ X ∧ s ∈ X → r H A G s H A ∈ x ∈ X | ∃ y ∈ X x = y H A
54 oveq2 ⊢ v = s H A → r H A G v = r H A G s H A
55 54 eleq1d ⊢ v = s H A → r H A G v ∈ x ∈ X | ∃ y ∈ X x = y H A ↔ r H A G s H A ∈ x ∈ X | ∃ y ∈ X x = y H A
56 53 55 syl5ibrcom ⊢ R ∈ RingOps ∧ A ∈ X ∧ r ∈ X ∧ s ∈ X → v = s H A → r H A G v ∈ x ∈ X | ∃ y ∈ X x = y H A
57 56 rexlimdva ⊢ R ∈ RingOps ∧ A ∈ X ∧ r ∈ X → ∃ s ∈ X v = s H A → r H A G v ∈ x ∈ X | ∃ y ∈ X x = y H A
58 57 adantld ⊢ R ∈ RingOps ∧ A ∈ X ∧ r ∈ X → v ∈ X ∧ ∃ s ∈ X v = s H A → r H A G v ∈ x ∈ X | ∃ y ∈ X x = y H A
59 32 58 biimtrid ⊢ R ∈ RingOps ∧ A ∈ X ∧ r ∈ X → v ∈ x ∈ X | ∃ y ∈ X x = y H A → r H A G v ∈ x ∈ X | ∃ y ∈ X x = y H A
60 59 ralrimiv ⊢ R ∈ RingOps ∧ A ∈ X ∧ r ∈ X → ∀ v ∈ x ∈ X | ∃ y ∈ X x = y H A r H A G v ∈ x ∈ X | ∃ y ∈ X x = y H A
61 1 2 3 rngoass ⊢ R ∈ RingOps ∧ w ∈ X ∧ r ∈ X ∧ A ∈ X → w H r H A = w H r H A
62 61 3exp2 ⊢ R ∈ RingOps → w ∈ X → r ∈ X → A ∈ X → w H r H A = w H r H A
63 62 imp42 ⊢ R ∈ RingOps ∧ w ∈ X ∧ r ∈ X ∧ A ∈ X → w H r H A = w H r H A
64 63 an32s ⊢ R ∈ RingOps ∧ A ∈ X ∧ w ∈ X ∧ r ∈ X → w H r H A = w H r H A
65 1 2 3 rngocl ⊢ R ∈ RingOps ∧ w ∈ X ∧ r ∈ X → w H r ∈ X
66 65 3expib ⊢ R ∈ RingOps → w ∈ X ∧ r ∈ X → w H r ∈ X
67 66 imdistani ⊢ R ∈ RingOps ∧ w ∈ X ∧ r ∈ X → R ∈ RingOps ∧ w H r ∈ X
68 1 2 3 rngocl ⊢ R ∈ RingOps ∧ w H r ∈ X ∧ A ∈ X → w H r H A ∈ X
69 68 3expa ⊢ R ∈ RingOps ∧ w H r ∈ X ∧ A ∈ X → w H r H A ∈ X
70 eqid ⊢ w H r H A = w H r H A
71 oveq1 ⊢ y = w H r → y H A = w H r H A
72 71 rspceeqv ⊢ w H r ∈ X ∧ w H r H A = w H r H A → ∃ y ∈ X w H r H A = y H A
73 70 72 mpan2 ⊢ w H r ∈ X → ∃ y ∈ X w H r H A = y H A
74 73 ad2antlr ⊢ R ∈ RingOps ∧ w H r ∈ X ∧ A ∈ X → ∃ y ∈ X w H r H A = y H A
75 eqeq1 ⊢ x = w H r H A → x = y H A ↔ w H r H A = y H A
76 75 rexbidv ⊢ x = w H r H A → ∃ y ∈ X x = y H A ↔ ∃ y ∈ X w H r H A = y H A
77 76 elrab ⊢ w H r H A ∈ x ∈ X | ∃ y ∈ X x = y H A ↔ w H r H A ∈ X ∧ ∃ y ∈ X w H r H A = y H A
78 69 74 77 sylanbrc ⊢ R ∈ RingOps ∧ w H r ∈ X ∧ A ∈ X → w H r H A ∈ x ∈ X | ∃ y ∈ X x = y H A
79 67 78 sylan ⊢ R ∈ RingOps ∧ w ∈ X ∧ r ∈ X ∧ A ∈ X → w H r H A ∈ x ∈ X | ∃ y ∈ X x = y H A
80 79 an32s ⊢ R ∈ RingOps ∧ A ∈ X ∧ w ∈ X ∧ r ∈ X → w H r H A ∈ x ∈ X | ∃ y ∈ X x = y H A
81 64 80 eqeltrrd ⊢ R ∈ RingOps ∧ A ∈ X ∧ w ∈ X ∧ r ∈ X → w H r H A ∈ x ∈ X | ∃ y ∈ X x = y H A
82 81 anass1rs ⊢ R ∈ RingOps ∧ A ∈ X ∧ r ∈ X ∧ w ∈ X → w H r H A ∈ x ∈ X | ∃ y ∈ X x = y H A
83 82 ralrimiva ⊢ R ∈ RingOps ∧ A ∈ X ∧ r ∈ X → ∀ w ∈ X w H r H A ∈ x ∈ X | ∃ y ∈ X x = y H A
84 60 83 jca ⊢ R ∈ RingOps ∧ A ∈ X ∧ r ∈ X → ∀ v ∈ x ∈ X | ∃ y ∈ X x = y H A r H A G v ∈ x ∈ X | ∃ y ∈ X x = y H A ∧ ∀ w ∈ X w H r H A ∈ x ∈ X | ∃ y ∈ X x = y H A
85 oveq1 ⊢ u = r H A → u G v = r H A G v
86 85 eleq1d ⊢ u = r H A → u G v ∈ x ∈ X | ∃ y ∈ X x = y H A ↔ r H A G v ∈ x ∈ X | ∃ y ∈ X x = y H A
87 86 ralbidv ⊢ u = r H A → ∀ v ∈ x ∈ X | ∃ y ∈ X x = y H A u G v ∈ x ∈ X | ∃ y ∈ X x = y H A ↔ ∀ v ∈ x ∈ X | ∃ y ∈ X x = y H A r H A G v ∈ x ∈ X | ∃ y ∈ X x = y H A
88 oveq2 ⊢ u = r H A → w H u = w H r H A
89 88 eleq1d ⊢ u = r H A → w H u ∈ x ∈ X | ∃ y ∈ X x = y H A ↔ w H r H A ∈ x ∈ X | ∃ y ∈ X x = y H A
90 89 ralbidv ⊢ u = r H A → ∀ w ∈ X w H u ∈ x ∈ X | ∃ y ∈ X x = y H A ↔ ∀ w ∈ X w H r H A ∈ x ∈ X | ∃ y ∈ X x = y H A
91 87 90 anbi12d ⊢ u = r H A → ∀ v ∈ x ∈ X | ∃ y ∈ X x = y H A u G v ∈ x ∈ X | ∃ y ∈ X x = y H A ∧ ∀ w ∈ X w H u ∈ x ∈ X | ∃ y ∈ X x = y H A ↔ ∀ v ∈ x ∈ X | ∃ y ∈ X x = y H A r H A G v ∈ x ∈ X | ∃ y ∈ X x = y H A ∧ ∀ w ∈ X w H r H A ∈ x ∈ X | ∃ y ∈ X x = y H A
92 84 91 syl5ibrcom ⊢ R ∈ RingOps ∧ A ∈ X ∧ r ∈ X → u = r H A → ∀ v ∈ x ∈ X | ∃ y ∈ X x = y H A u G v ∈ x ∈ X | ∃ y ∈ X x = y H A ∧ ∀ w ∈ X w H u ∈ x ∈ X | ∃ y ∈ X x = y H A
93 92 rexlimdva ⊢ R ∈ RingOps ∧ A ∈ X → ∃ r ∈ X u = r H A → ∀ v ∈ x ∈ X | ∃ y ∈ X x = y H A u G v ∈ x ∈ X | ∃ y ∈ X x = y H A ∧ ∀ w ∈ X w H u ∈ x ∈ X | ∃ y ∈ X x = y H A
94 93 adantld ⊢ R ∈ RingOps ∧ A ∈ X → u ∈ X ∧ ∃ r ∈ X u = r H A → ∀ v ∈ x ∈ X | ∃ y ∈ X x = y H A u G v ∈ x ∈ X | ∃ y ∈ X x = y H A ∧ ∀ w ∈ X w H u ∈ x ∈ X | ∃ y ∈ X x = y H A
95 25 94 biimtrid ⊢ R ∈ RingOps ∧ A ∈ X → u ∈ x ∈ X | ∃ y ∈ X x = y H A → ∀ v ∈ x ∈ X | ∃ y ∈ X x = y H A u G v ∈ x ∈ X | ∃ y ∈ X x = y H A ∧ ∀ w ∈ X w H u ∈ x ∈ X | ∃ y ∈ X x = y H A
96 95 ralrimiv ⊢ R ∈ RingOps ∧ A ∈ X → ∀ u ∈ x ∈ X | ∃ y ∈ X x = y H A ∀ v ∈ x ∈ X | ∃ y ∈ X x = y H A u G v ∈ x ∈ X | ∃ y ∈ X x = y H A ∧ ∀ w ∈ X w H u ∈ x ∈ X | ∃ y ∈ X x = y H A
97 6 18 96 3jca ⊢ R ∈ RingOps ∧ A ∈ X → x ∈ X | ∃ y ∈ X x = y H A ⊆ X ∧ GId ⁡ G ∈ x ∈ X | ∃ y ∈ X x = y H A ∧ ∀ u ∈ x ∈ X | ∃ y ∈ X x = y H A ∀ v ∈ x ∈ X | ∃ y ∈ X x = y H A u G v ∈ x ∈ X | ∃ y ∈ X x = y H A ∧ ∀ w ∈ X w H u ∈ x ∈ X | ∃ y ∈ X x = y H A
98 4 97 sylan ⊢ R ∈ CRingOps ∧ A ∈ X → x ∈ X | ∃ y ∈ X x = y H A ⊆ X ∧ GId ⁡ G ∈ x ∈ X | ∃ y ∈ X x = y H A ∧ ∀ u ∈ x ∈ X | ∃ y ∈ X x = y H A ∀ v ∈ x ∈ X | ∃ y ∈ X x = y H A u G v ∈ x ∈ X | ∃ y ∈ X x = y H A ∧ ∀ w ∈ X w H u ∈ x ∈ X | ∃ y ∈ X x = y H A
99 1 2 3 7 isidlc ⊢ R ∈ CRingOps → x ∈ X | ∃ y ∈ X x = y H A ∈ Idl ⁡ R ↔ x ∈ X | ∃ y ∈ X x = y H A ⊆ X ∧ GId ⁡ G ∈ x ∈ X | ∃ y ∈ X x = y H A ∧ ∀ u ∈ x ∈ X | ∃ y ∈ X x = y H A ∀ v ∈ x ∈ X | ∃ y ∈ X x = y H A u G v ∈ x ∈ X | ∃ y ∈ X x = y H A ∧ ∀ w ∈ X w H u ∈ x ∈ X | ∃ y ∈ X x = y H A
100 99 adantr ⊢ R ∈ CRingOps ∧ A ∈ X → x ∈ X | ∃ y ∈ X x = y H A ∈ Idl ⁡ R ↔ x ∈ X | ∃ y ∈ X x = y H A ⊆ X ∧ GId ⁡ G ∈ x ∈ X | ∃ y ∈ X x = y H A ∧ ∀ u ∈ x ∈ X | ∃ y ∈ X x = y H A ∀ v ∈ x ∈ X | ∃ y ∈ X x = y H A u G v ∈ x ∈ X | ∃ y ∈ X x = y H A ∧ ∀ w ∈ X w H u ∈ x ∈ X | ∃ y ∈ X x = y H A
101 98 100 mpbird ⊢ R ∈ CRingOps ∧ A ∈ X → x ∈ X | ∃ y ∈ X x = y H A ∈ Idl ⁡ R
102 simpr ⊢ R ∈ CRingOps ∧ A ∈ X → A ∈ X
103 1 rneqi ⊢ ran ⁡ G = ran ⁡ 1 st ⁡ R
104 3 103 eqtri ⊢ X = ran ⁡ 1 st ⁡ R
105 eqid ⊢ GId ⁡ H = GId ⁡ H
106 104 2 105 rngo1cl ⊢ R ∈ RingOps → GId ⁡ H ∈ X
107 106 adantr ⊢ R ∈ RingOps ∧ A ∈ X → GId ⁡ H ∈ X
108 2 104 105 rngolidm ⊢ R ∈ RingOps ∧ A ∈ X → GId ⁡ H H A = A
109 108 eqcomd ⊢ R ∈ RingOps ∧ A ∈ X → A = GId ⁡ H H A
110 oveq1 ⊢ y = GId ⁡ H → y H A = GId ⁡ H H A
111 110 rspceeqv ⊢ GId ⁡ H ∈ X ∧ A = GId ⁡ H H A → ∃ y ∈ X A = y H A
112 107 109 111 syl2anc ⊢ R ∈ RingOps ∧ A ∈ X → ∃ y ∈ X A = y H A
113 4 112 sylan ⊢ R ∈ CRingOps ∧ A ∈ X → ∃ y ∈ X A = y H A
114 eqeq1 ⊢ x = A → x = y H A ↔ A = y H A
115 114 rexbidv ⊢ x = A → ∃ y ∈ X x = y H A ↔ ∃ y ∈ X A = y H A
116 115 elrab ⊢ A ∈ x ∈ X | ∃ y ∈ X x = y H A ↔ A ∈ X ∧ ∃ y ∈ X A = y H A
117 102 113 116 sylanbrc ⊢ R ∈ CRingOps ∧ A ∈ X → A ∈ x ∈ X | ∃ y ∈ X x = y H A
118 117 snssd ⊢ R ∈ CRingOps ∧ A ∈ X → A ⊆ x ∈ X | ∃ y ∈ X x = y H A
119 snssg ⊢ A ∈ X → A ∈ j ↔ A ⊆ j
120 119 biimpar ⊢ A ∈ X ∧ A ⊆ j → A ∈ j
121 1 2 3 idllmulcl ⊢ R ∈ RingOps ∧ j ∈ Idl ⁡ R ∧ A ∈ j ∧ y ∈ X → y H A ∈ j
122 121 anassrs ⊢ R ∈ RingOps ∧ j ∈ Idl ⁡ R ∧ A ∈ j ∧ y ∈ X → y H A ∈ j
123 eleq1 ⊢ x = y H A → x ∈ j ↔ y H A ∈ j
124 122 123 syl5ibrcom ⊢ R ∈ RingOps ∧ j ∈ Idl ⁡ R ∧ A ∈ j ∧ y ∈ X → x = y H A → x ∈ j
125 124 rexlimdva ⊢ R ∈ RingOps ∧ j ∈ Idl ⁡ R ∧ A ∈ j → ∃ y ∈ X x = y H A → x ∈ j
126 125 adantr ⊢ R ∈ RingOps ∧ j ∈ Idl ⁡ R ∧ A ∈ j ∧ x ∈ X → ∃ y ∈ X x = y H A → x ∈ j
127 126 ralrimiva ⊢ R ∈ RingOps ∧ j ∈ Idl ⁡ R ∧ A ∈ j → ∀ x ∈ X ∃ y ∈ X x = y H A → x ∈ j
128 rabss ⊢ x ∈ X | ∃ y ∈ X x = y H A ⊆ j ↔ ∀ x ∈ X ∃ y ∈ X x = y H A → x ∈ j
129 127 128 sylibr ⊢ R ∈ RingOps ∧ j ∈ Idl ⁡ R ∧ A ∈ j → x ∈ X | ∃ y ∈ X x = y H A ⊆ j
130 129 ex ⊢ R ∈ RingOps ∧ j ∈ Idl ⁡ R → A ∈ j → x ∈ X | ∃ y ∈ X x = y H A ⊆ j
131 120 130 syl5 ⊢ R ∈ RingOps ∧ j ∈ Idl ⁡ R → A ∈ X ∧ A ⊆ j → x ∈ X | ∃ y ∈ X x = y H A ⊆ j
132 131 expdimp ⊢ R ∈ RingOps ∧ j ∈ Idl ⁡ R ∧ A ∈ X → A ⊆ j → x ∈ X | ∃ y ∈ X x = y H A ⊆ j
133 132 an32s ⊢ R ∈ RingOps ∧ A ∈ X ∧ j ∈ Idl ⁡ R → A ⊆ j → x ∈ X | ∃ y ∈ X x = y H A ⊆ j
134 133 ralrimiva ⊢ R ∈ RingOps ∧ A ∈ X → ∀ j ∈ Idl ⁡ R A ⊆ j → x ∈ X | ∃ y ∈ X x = y H A ⊆ j
135 4 134 sylan ⊢ R ∈ CRingOps ∧ A ∈ X → ∀ j ∈ Idl ⁡ R A ⊆ j → x ∈ X | ∃ y ∈ X x = y H A ⊆ j
136 101 118 135 3jca ⊢ R ∈ CRingOps ∧ A ∈ X → x ∈ X | ∃ y ∈ X x = y H A ∈ Idl ⁡ R ∧ A ⊆ x ∈ X | ∃ y ∈ X x = y H A ∧ ∀ j ∈ Idl ⁡ R A ⊆ j → x ∈ X | ∃ y ∈ X x = y H A ⊆ j
137 snssi ⊢ A ∈ X → A ⊆ X
138 1 3 igenval2 ⊢ R ∈ RingOps ∧ A ⊆ X → R IdlGen A = x ∈ X | ∃ y ∈ X x = y H A ↔ x ∈ X | ∃ y ∈ X x = y H A ∈ Idl ⁡ R ∧ A ⊆ x ∈ X | ∃ y ∈ X x = y H A ∧ ∀ j ∈ Idl ⁡ R A ⊆ j → x ∈ X | ∃ y ∈ X x = y H A ⊆ j
139 4 137 138 syl2an ⊢ R ∈ CRingOps ∧ A ∈ X → R IdlGen A = x ∈ X | ∃ y ∈ X x = y H A ↔ x ∈ X | ∃ y ∈ X x = y H A ∈ Idl ⁡ R ∧ A ⊆ x ∈ X | ∃ y ∈ X x = y H A ∧ ∀ j ∈ Idl ⁡ R A ⊆ j → x ∈ X | ∃ y ∈ X x = y H A ⊆ j
140 136 139 mpbird ⊢ R ∈ CRingOps ∧ A ∈ X → R IdlGen A = x ∈ X | ∃ y ∈ X x = y H A