Users' Mathboxes Mathbox for Jeff Madsen < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  prnc Structured version   Visualization version   GIF version

Theorem prnc 36935
Description: A principal ideal (an ideal generated by one element) in a commutative ring. (Contributed by Jeff Madsen, 10-Jun-2010.)
Hypotheses
Ref Expression
prnc.1 𝐺 = (1st𝑅)
prnc.2 𝐻 = (2nd𝑅)
prnc.3 𝑋 = ran 𝐺
Assertion
Ref Expression
prnc ((𝑅 ∈ CRingOps ∧ 𝐴𝑋) → (𝑅 IdlGen {𝐴}) = {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)})
Distinct variable groups:   𝑥,𝑅,𝑦   𝑥,𝑋,𝑦   𝑥,𝐺,𝑦   𝑥,𝐻,𝑦   𝑥,𝐴,𝑦

Proof of Theorem prnc
Dummy variables 𝑗 𝑢 𝑣 𝑤 𝑟 𝑠 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 crngorngo 36868 . . . . 5 (𝑅 ∈ CRingOps → 𝑅 ∈ RingOps)
2 ssrab2 4078 . . . . . . 7 {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑋
32a1i 11 . . . . . 6 ((𝑅 ∈ RingOps ∧ 𝐴𝑋) → {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑋)
4 prnc.1 . . . . . . . . 9 𝐺 = (1st𝑅)
5 prnc.3 . . . . . . . . 9 𝑋 = ran 𝐺
6 eqid 2733 . . . . . . . . 9 (GId‘𝐺) = (GId‘𝐺)
74, 5, 6rngo0cl 36787 . . . . . . . 8 (𝑅 ∈ RingOps → (GId‘𝐺) ∈ 𝑋)
87adantr 482 . . . . . . 7 ((𝑅 ∈ RingOps ∧ 𝐴𝑋) → (GId‘𝐺) ∈ 𝑋)
9 prnc.2 . . . . . . . . . 10 𝐻 = (2nd𝑅)
106, 5, 4, 9rngolz 36790 . . . . . . . . 9 ((𝑅 ∈ RingOps ∧ 𝐴𝑋) → ((GId‘𝐺)𝐻𝐴) = (GId‘𝐺))
1110eqcomd 2739 . . . . . . . 8 ((𝑅 ∈ RingOps ∧ 𝐴𝑋) → (GId‘𝐺) = ((GId‘𝐺)𝐻𝐴))
12 oveq1 7416 . . . . . . . . 9 (𝑦 = (GId‘𝐺) → (𝑦𝐻𝐴) = ((GId‘𝐺)𝐻𝐴))
1312rspceeqv 3634 . . . . . . . 8 (((GId‘𝐺) ∈ 𝑋 ∧ (GId‘𝐺) = ((GId‘𝐺)𝐻𝐴)) → ∃𝑦𝑋 (GId‘𝐺) = (𝑦𝐻𝐴))
148, 11, 13syl2anc 585 . . . . . . 7 ((𝑅 ∈ RingOps ∧ 𝐴𝑋) → ∃𝑦𝑋 (GId‘𝐺) = (𝑦𝐻𝐴))
15 eqeq1 2737 . . . . . . . . 9 (𝑥 = (GId‘𝐺) → (𝑥 = (𝑦𝐻𝐴) ↔ (GId‘𝐺) = (𝑦𝐻𝐴)))
1615rexbidv 3179 . . . . . . . 8 (𝑥 = (GId‘𝐺) → (∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴) ↔ ∃𝑦𝑋 (GId‘𝐺) = (𝑦𝐻𝐴)))
1716elrab 3684 . . . . . . 7 ((GId‘𝐺) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ↔ ((GId‘𝐺) ∈ 𝑋 ∧ ∃𝑦𝑋 (GId‘𝐺) = (𝑦𝐻𝐴)))
188, 14, 17sylanbrc 584 . . . . . 6 ((𝑅 ∈ RingOps ∧ 𝐴𝑋) → (GId‘𝐺) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)})
19 eqeq1 2737 . . . . . . . . . . 11 (𝑥 = 𝑢 → (𝑥 = (𝑦𝐻𝐴) ↔ 𝑢 = (𝑦𝐻𝐴)))
2019rexbidv 3179 . . . . . . . . . 10 (𝑥 = 𝑢 → (∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴) ↔ ∃𝑦𝑋 𝑢 = (𝑦𝐻𝐴)))
21 oveq1 7416 . . . . . . . . . . . 12 (𝑦 = 𝑟 → (𝑦𝐻𝐴) = (𝑟𝐻𝐴))
2221eqeq2d 2744 . . . . . . . . . . 11 (𝑦 = 𝑟 → (𝑢 = (𝑦𝐻𝐴) ↔ 𝑢 = (𝑟𝐻𝐴)))
2322cbvrexvw 3236 . . . . . . . . . 10 (∃𝑦𝑋 𝑢 = (𝑦𝐻𝐴) ↔ ∃𝑟𝑋 𝑢 = (𝑟𝐻𝐴))
2420, 23bitrdi 287 . . . . . . . . 9 (𝑥 = 𝑢 → (∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴) ↔ ∃𝑟𝑋 𝑢 = (𝑟𝐻𝐴)))
2524elrab 3684 . . . . . . . 8 (𝑢 ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ↔ (𝑢𝑋 ∧ ∃𝑟𝑋 𝑢 = (𝑟𝐻𝐴)))
26 eqeq1 2737 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑣 → (𝑥 = (𝑦𝐻𝐴) ↔ 𝑣 = (𝑦𝐻𝐴)))
2726rexbidv 3179 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑣 → (∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴) ↔ ∃𝑦𝑋 𝑣 = (𝑦𝐻𝐴)))
28 oveq1 7416 . . . . . . . . . . . . . . . . . 18 (𝑦 = 𝑠 → (𝑦𝐻𝐴) = (𝑠𝐻𝐴))
2928eqeq2d 2744 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑠 → (𝑣 = (𝑦𝐻𝐴) ↔ 𝑣 = (𝑠𝐻𝐴)))
3029cbvrexvw 3236 . . . . . . . . . . . . . . . 16 (∃𝑦𝑋 𝑣 = (𝑦𝐻𝐴) ↔ ∃𝑠𝑋 𝑣 = (𝑠𝐻𝐴))
3127, 30bitrdi 287 . . . . . . . . . . . . . . 15 (𝑥 = 𝑣 → (∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴) ↔ ∃𝑠𝑋 𝑣 = (𝑠𝐻𝐴)))
3231elrab 3684 . . . . . . . . . . . . . 14 (𝑣 ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ↔ (𝑣𝑋 ∧ ∃𝑠𝑋 𝑣 = (𝑠𝐻𝐴)))
334, 9, 5rngodir 36773 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑅 ∈ RingOps ∧ (𝑟𝑋𝑠𝑋𝐴𝑋)) → ((𝑟𝐺𝑠)𝐻𝐴) = ((𝑟𝐻𝐴)𝐺(𝑠𝐻𝐴)))
34333exp2 1355 . . . . . . . . . . . . . . . . . . . . 21 (𝑅 ∈ RingOps → (𝑟𝑋 → (𝑠𝑋 → (𝐴𝑋 → ((𝑟𝐺𝑠)𝐻𝐴) = ((𝑟𝐻𝐴)𝐺(𝑠𝐻𝐴))))))
3534imp42 428 . . . . . . . . . . . . . . . . . . . 20 (((𝑅 ∈ RingOps ∧ (𝑟𝑋𝑠𝑋)) ∧ 𝐴𝑋) → ((𝑟𝐺𝑠)𝐻𝐴) = ((𝑟𝐻𝐴)𝐺(𝑠𝐻𝐴)))
364, 5rngogcl 36780 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑅 ∈ RingOps ∧ 𝑟𝑋𝑠𝑋) → (𝑟𝐺𝑠) ∈ 𝑋)
37363expib 1123 . . . . . . . . . . . . . . . . . . . . . 22 (𝑅 ∈ RingOps → ((𝑟𝑋𝑠𝑋) → (𝑟𝐺𝑠) ∈ 𝑋))
3837imdistani 570 . . . . . . . . . . . . . . . . . . . . 21 ((𝑅 ∈ RingOps ∧ (𝑟𝑋𝑠𝑋)) → (𝑅 ∈ RingOps ∧ (𝑟𝐺𝑠) ∈ 𝑋))
394, 9, 5rngocl 36769 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑅 ∈ RingOps ∧ (𝑟𝐺𝑠) ∈ 𝑋𝐴𝑋) → ((𝑟𝐺𝑠)𝐻𝐴) ∈ 𝑋)
40393expa 1119 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑅 ∈ RingOps ∧ (𝑟𝐺𝑠) ∈ 𝑋) ∧ 𝐴𝑋) → ((𝑟𝐺𝑠)𝐻𝐴) ∈ 𝑋)
41 eqid 2733 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑟𝐺𝑠)𝐻𝐴) = ((𝑟𝐺𝑠)𝐻𝐴)
42 oveq1 7416 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 = (𝑟𝐺𝑠) → (𝑦𝐻𝐴) = ((𝑟𝐺𝑠)𝐻𝐴))
4342rspceeqv 3634 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑟𝐺𝑠) ∈ 𝑋 ∧ ((𝑟𝐺𝑠)𝐻𝐴) = ((𝑟𝐺𝑠)𝐻𝐴)) → ∃𝑦𝑋 ((𝑟𝐺𝑠)𝐻𝐴) = (𝑦𝐻𝐴))
4441, 43mpan2 690 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑟𝐺𝑠) ∈ 𝑋 → ∃𝑦𝑋 ((𝑟𝐺𝑠)𝐻𝐴) = (𝑦𝐻𝐴))
4544ad2antlr 726 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑅 ∈ RingOps ∧ (𝑟𝐺𝑠) ∈ 𝑋) ∧ 𝐴𝑋) → ∃𝑦𝑋 ((𝑟𝐺𝑠)𝐻𝐴) = (𝑦𝐻𝐴))
46 eqeq1 2737 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = ((𝑟𝐺𝑠)𝐻𝐴) → (𝑥 = (𝑦𝐻𝐴) ↔ ((𝑟𝐺𝑠)𝐻𝐴) = (𝑦𝐻𝐴)))
4746rexbidv 3179 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = ((𝑟𝐺𝑠)𝐻𝐴) → (∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴) ↔ ∃𝑦𝑋 ((𝑟𝐺𝑠)𝐻𝐴) = (𝑦𝐻𝐴)))
4847elrab 3684 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑟𝐺𝑠)𝐻𝐴) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ↔ (((𝑟𝐺𝑠)𝐻𝐴) ∈ 𝑋 ∧ ∃𝑦𝑋 ((𝑟𝐺𝑠)𝐻𝐴) = (𝑦𝐻𝐴)))
4940, 45, 48sylanbrc 584 . . . . . . . . . . . . . . . . . . . . 21 (((𝑅 ∈ RingOps ∧ (𝑟𝐺𝑠) ∈ 𝑋) ∧ 𝐴𝑋) → ((𝑟𝐺𝑠)𝐻𝐴) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)})
5038, 49sylan 581 . . . . . . . . . . . . . . . . . . . 20 (((𝑅 ∈ RingOps ∧ (𝑟𝑋𝑠𝑋)) ∧ 𝐴𝑋) → ((𝑟𝐺𝑠)𝐻𝐴) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)})
5135, 50eqeltrrd 2835 . . . . . . . . . . . . . . . . . . 19 (((𝑅 ∈ RingOps ∧ (𝑟𝑋𝑠𝑋)) ∧ 𝐴𝑋) → ((𝑟𝐻𝐴)𝐺(𝑠𝐻𝐴)) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)})
5251an32s 651 . . . . . . . . . . . . . . . . . 18 (((𝑅 ∈ RingOps ∧ 𝐴𝑋) ∧ (𝑟𝑋𝑠𝑋)) → ((𝑟𝐻𝐴)𝐺(𝑠𝐻𝐴)) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)})
5352anassrs 469 . . . . . . . . . . . . . . . . 17 ((((𝑅 ∈ RingOps ∧ 𝐴𝑋) ∧ 𝑟𝑋) ∧ 𝑠𝑋) → ((𝑟𝐻𝐴)𝐺(𝑠𝐻𝐴)) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)})
54 oveq2 7417 . . . . . . . . . . . . . . . . . 18 (𝑣 = (𝑠𝐻𝐴) → ((𝑟𝐻𝐴)𝐺𝑣) = ((𝑟𝐻𝐴)𝐺(𝑠𝐻𝐴)))
5554eleq1d 2819 . . . . . . . . . . . . . . . . 17 (𝑣 = (𝑠𝐻𝐴) → (((𝑟𝐻𝐴)𝐺𝑣) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ↔ ((𝑟𝐻𝐴)𝐺(𝑠𝐻𝐴)) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)}))
5653, 55syl5ibrcom 246 . . . . . . . . . . . . . . . 16 ((((𝑅 ∈ RingOps ∧ 𝐴𝑋) ∧ 𝑟𝑋) ∧ 𝑠𝑋) → (𝑣 = (𝑠𝐻𝐴) → ((𝑟𝐻𝐴)𝐺𝑣) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)}))
5756rexlimdva 3156 . . . . . . . . . . . . . . 15 (((𝑅 ∈ RingOps ∧ 𝐴𝑋) ∧ 𝑟𝑋) → (∃𝑠𝑋 𝑣 = (𝑠𝐻𝐴) → ((𝑟𝐻𝐴)𝐺𝑣) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)}))
5857adantld 492 . . . . . . . . . . . . . 14 (((𝑅 ∈ RingOps ∧ 𝐴𝑋) ∧ 𝑟𝑋) → ((𝑣𝑋 ∧ ∃𝑠𝑋 𝑣 = (𝑠𝐻𝐴)) → ((𝑟𝐻𝐴)𝐺𝑣) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)}))
5932, 58biimtrid 241 . . . . . . . . . . . . 13 (((𝑅 ∈ RingOps ∧ 𝐴𝑋) ∧ 𝑟𝑋) → (𝑣 ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} → ((𝑟𝐻𝐴)𝐺𝑣) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)}))
6059ralrimiv 3146 . . . . . . . . . . . 12 (((𝑅 ∈ RingOps ∧ 𝐴𝑋) ∧ 𝑟𝑋) → ∀𝑣 ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ((𝑟𝐻𝐴)𝐺𝑣) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)})
614, 9, 5rngoass 36774 . . . . . . . . . . . . . . . . . 18 ((𝑅 ∈ RingOps ∧ (𝑤𝑋𝑟𝑋𝐴𝑋)) → ((𝑤𝐻𝑟)𝐻𝐴) = (𝑤𝐻(𝑟𝐻𝐴)))
62613exp2 1355 . . . . . . . . . . . . . . . . 17 (𝑅 ∈ RingOps → (𝑤𝑋 → (𝑟𝑋 → (𝐴𝑋 → ((𝑤𝐻𝑟)𝐻𝐴) = (𝑤𝐻(𝑟𝐻𝐴))))))
6362imp42 428 . . . . . . . . . . . . . . . 16 (((𝑅 ∈ RingOps ∧ (𝑤𝑋𝑟𝑋)) ∧ 𝐴𝑋) → ((𝑤𝐻𝑟)𝐻𝐴) = (𝑤𝐻(𝑟𝐻𝐴)))
6463an32s 651 . . . . . . . . . . . . . . 15 (((𝑅 ∈ RingOps ∧ 𝐴𝑋) ∧ (𝑤𝑋𝑟𝑋)) → ((𝑤𝐻𝑟)𝐻𝐴) = (𝑤𝐻(𝑟𝐻𝐴)))
654, 9, 5rngocl 36769 . . . . . . . . . . . . . . . . . . 19 ((𝑅 ∈ RingOps ∧ 𝑤𝑋𝑟𝑋) → (𝑤𝐻𝑟) ∈ 𝑋)
66653expib 1123 . . . . . . . . . . . . . . . . . 18 (𝑅 ∈ RingOps → ((𝑤𝑋𝑟𝑋) → (𝑤𝐻𝑟) ∈ 𝑋))
6766imdistani 570 . . . . . . . . . . . . . . . . 17 ((𝑅 ∈ RingOps ∧ (𝑤𝑋𝑟𝑋)) → (𝑅 ∈ RingOps ∧ (𝑤𝐻𝑟) ∈ 𝑋))
684, 9, 5rngocl 36769 . . . . . . . . . . . . . . . . . . 19 ((𝑅 ∈ RingOps ∧ (𝑤𝐻𝑟) ∈ 𝑋𝐴𝑋) → ((𝑤𝐻𝑟)𝐻𝐴) ∈ 𝑋)
69683expa 1119 . . . . . . . . . . . . . . . . . 18 (((𝑅 ∈ RingOps ∧ (𝑤𝐻𝑟) ∈ 𝑋) ∧ 𝐴𝑋) → ((𝑤𝐻𝑟)𝐻𝐴) ∈ 𝑋)
70 eqid 2733 . . . . . . . . . . . . . . . . . . . 20 ((𝑤𝐻𝑟)𝐻𝐴) = ((𝑤𝐻𝑟)𝐻𝐴)
71 oveq1 7416 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 = (𝑤𝐻𝑟) → (𝑦𝐻𝐴) = ((𝑤𝐻𝑟)𝐻𝐴))
7271rspceeqv 3634 . . . . . . . . . . . . . . . . . . . 20 (((𝑤𝐻𝑟) ∈ 𝑋 ∧ ((𝑤𝐻𝑟)𝐻𝐴) = ((𝑤𝐻𝑟)𝐻𝐴)) → ∃𝑦𝑋 ((𝑤𝐻𝑟)𝐻𝐴) = (𝑦𝐻𝐴))
7370, 72mpan2 690 . . . . . . . . . . . . . . . . . . 19 ((𝑤𝐻𝑟) ∈ 𝑋 → ∃𝑦𝑋 ((𝑤𝐻𝑟)𝐻𝐴) = (𝑦𝐻𝐴))
7473ad2antlr 726 . . . . . . . . . . . . . . . . . 18 (((𝑅 ∈ RingOps ∧ (𝑤𝐻𝑟) ∈ 𝑋) ∧ 𝐴𝑋) → ∃𝑦𝑋 ((𝑤𝐻𝑟)𝐻𝐴) = (𝑦𝐻𝐴))
75 eqeq1 2737 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = ((𝑤𝐻𝑟)𝐻𝐴) → (𝑥 = (𝑦𝐻𝐴) ↔ ((𝑤𝐻𝑟)𝐻𝐴) = (𝑦𝐻𝐴)))
7675rexbidv 3179 . . . . . . . . . . . . . . . . . . 19 (𝑥 = ((𝑤𝐻𝑟)𝐻𝐴) → (∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴) ↔ ∃𝑦𝑋 ((𝑤𝐻𝑟)𝐻𝐴) = (𝑦𝐻𝐴)))
7776elrab 3684 . . . . . . . . . . . . . . . . . 18 (((𝑤𝐻𝑟)𝐻𝐴) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ↔ (((𝑤𝐻𝑟)𝐻𝐴) ∈ 𝑋 ∧ ∃𝑦𝑋 ((𝑤𝐻𝑟)𝐻𝐴) = (𝑦𝐻𝐴)))
7869, 74, 77sylanbrc 584 . . . . . . . . . . . . . . . . 17 (((𝑅 ∈ RingOps ∧ (𝑤𝐻𝑟) ∈ 𝑋) ∧ 𝐴𝑋) → ((𝑤𝐻𝑟)𝐻𝐴) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)})
7967, 78sylan 581 . . . . . . . . . . . . . . . 16 (((𝑅 ∈ RingOps ∧ (𝑤𝑋𝑟𝑋)) ∧ 𝐴𝑋) → ((𝑤𝐻𝑟)𝐻𝐴) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)})
8079an32s 651 . . . . . . . . . . . . . . 15 (((𝑅 ∈ RingOps ∧ 𝐴𝑋) ∧ (𝑤𝑋𝑟𝑋)) → ((𝑤𝐻𝑟)𝐻𝐴) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)})
8164, 80eqeltrrd 2835 . . . . . . . . . . . . . 14 (((𝑅 ∈ RingOps ∧ 𝐴𝑋) ∧ (𝑤𝑋𝑟𝑋)) → (𝑤𝐻(𝑟𝐻𝐴)) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)})
8281anass1rs 654 . . . . . . . . . . . . 13 ((((𝑅 ∈ RingOps ∧ 𝐴𝑋) ∧ 𝑟𝑋) ∧ 𝑤𝑋) → (𝑤𝐻(𝑟𝐻𝐴)) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)})
8382ralrimiva 3147 . . . . . . . . . . . 12 (((𝑅 ∈ RingOps ∧ 𝐴𝑋) ∧ 𝑟𝑋) → ∀𝑤𝑋 (𝑤𝐻(𝑟𝐻𝐴)) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)})
8460, 83jca 513 . . . . . . . . . . 11 (((𝑅 ∈ RingOps ∧ 𝐴𝑋) ∧ 𝑟𝑋) → (∀𝑣 ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ((𝑟𝐻𝐴)𝐺𝑣) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑤𝑋 (𝑤𝐻(𝑟𝐻𝐴)) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)}))
85 oveq1 7416 . . . . . . . . . . . . . 14 (𝑢 = (𝑟𝐻𝐴) → (𝑢𝐺𝑣) = ((𝑟𝐻𝐴)𝐺𝑣))
8685eleq1d 2819 . . . . . . . . . . . . 13 (𝑢 = (𝑟𝐻𝐴) → ((𝑢𝐺𝑣) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ↔ ((𝑟𝐻𝐴)𝐺𝑣) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)}))
8786ralbidv 3178 . . . . . . . . . . . 12 (𝑢 = (𝑟𝐻𝐴) → (∀𝑣 ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} (𝑢𝐺𝑣) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ↔ ∀𝑣 ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ((𝑟𝐻𝐴)𝐺𝑣) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)}))
88 oveq2 7417 . . . . . . . . . . . . . 14 (𝑢 = (𝑟𝐻𝐴) → (𝑤𝐻𝑢) = (𝑤𝐻(𝑟𝐻𝐴)))
8988eleq1d 2819 . . . . . . . . . . . . 13 (𝑢 = (𝑟𝐻𝐴) → ((𝑤𝐻𝑢) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ↔ (𝑤𝐻(𝑟𝐻𝐴)) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)}))
9089ralbidv 3178 . . . . . . . . . . . 12 (𝑢 = (𝑟𝐻𝐴) → (∀𝑤𝑋 (𝑤𝐻𝑢) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ↔ ∀𝑤𝑋 (𝑤𝐻(𝑟𝐻𝐴)) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)}))
9187, 90anbi12d 632 . . . . . . . . . . 11 (𝑢 = (𝑟𝐻𝐴) → ((∀𝑣 ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} (𝑢𝐺𝑣) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑤𝑋 (𝑤𝐻𝑢) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)}) ↔ (∀𝑣 ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ((𝑟𝐻𝐴)𝐺𝑣) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑤𝑋 (𝑤𝐻(𝑟𝐻𝐴)) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)})))
9284, 91syl5ibrcom 246 . . . . . . . . . 10 (((𝑅 ∈ RingOps ∧ 𝐴𝑋) ∧ 𝑟𝑋) → (𝑢 = (𝑟𝐻𝐴) → (∀𝑣 ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} (𝑢𝐺𝑣) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑤𝑋 (𝑤𝐻𝑢) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)})))
9392rexlimdva 3156 . . . . . . . . 9 ((𝑅 ∈ RingOps ∧ 𝐴𝑋) → (∃𝑟𝑋 𝑢 = (𝑟𝐻𝐴) → (∀𝑣 ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} (𝑢𝐺𝑣) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑤𝑋 (𝑤𝐻𝑢) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)})))
9493adantld 492 . . . . . . . 8 ((𝑅 ∈ RingOps ∧ 𝐴𝑋) → ((𝑢𝑋 ∧ ∃𝑟𝑋 𝑢 = (𝑟𝐻𝐴)) → (∀𝑣 ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} (𝑢𝐺𝑣) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑤𝑋 (𝑤𝐻𝑢) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)})))
9525, 94biimtrid 241 . . . . . . 7 ((𝑅 ∈ RingOps ∧ 𝐴𝑋) → (𝑢 ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} → (∀𝑣 ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} (𝑢𝐺𝑣) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑤𝑋 (𝑤𝐻𝑢) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)})))
9695ralrimiv 3146 . . . . . 6 ((𝑅 ∈ RingOps ∧ 𝐴𝑋) → ∀𝑢 ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} (∀𝑣 ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} (𝑢𝐺𝑣) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑤𝑋 (𝑤𝐻𝑢) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)}))
973, 18, 963jca 1129 . . . . 5 ((𝑅 ∈ RingOps ∧ 𝐴𝑋) → ({𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑋 ∧ (GId‘𝐺) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑢 ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} (∀𝑣 ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} (𝑢𝐺𝑣) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑤𝑋 (𝑤𝐻𝑢) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)})))
981, 97sylan 581 . . . 4 ((𝑅 ∈ CRingOps ∧ 𝐴𝑋) → ({𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑋 ∧ (GId‘𝐺) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑢 ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} (∀𝑣 ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} (𝑢𝐺𝑣) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑤𝑋 (𝑤𝐻𝑢) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)})))
994, 9, 5, 6isidlc 36883 . . . . 5 (𝑅 ∈ CRingOps → ({𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ∈ (Idl‘𝑅) ↔ ({𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑋 ∧ (GId‘𝐺) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑢 ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} (∀𝑣 ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} (𝑢𝐺𝑣) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑤𝑋 (𝑤𝐻𝑢) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)}))))
10099adantr 482 . . . 4 ((𝑅 ∈ CRingOps ∧ 𝐴𝑋) → ({𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ∈ (Idl‘𝑅) ↔ ({𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑋 ∧ (GId‘𝐺) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑢 ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} (∀𝑣 ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} (𝑢𝐺𝑣) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑤𝑋 (𝑤𝐻𝑢) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)}))))
10198, 100mpbird 257 . . 3 ((𝑅 ∈ CRingOps ∧ 𝐴𝑋) → {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ∈ (Idl‘𝑅))
102 simpr 486 . . . . 5 ((𝑅 ∈ CRingOps ∧ 𝐴𝑋) → 𝐴𝑋)
1034rneqi 5937 . . . . . . . . . 10 ran 𝐺 = ran (1st𝑅)
1045, 103eqtri 2761 . . . . . . . . 9 𝑋 = ran (1st𝑅)
105 eqid 2733 . . . . . . . . 9 (GId‘𝐻) = (GId‘𝐻)
106104, 9, 105rngo1cl 36807 . . . . . . . 8 (𝑅 ∈ RingOps → (GId‘𝐻) ∈ 𝑋)
107106adantr 482 . . . . . . 7 ((𝑅 ∈ RingOps ∧ 𝐴𝑋) → (GId‘𝐻) ∈ 𝑋)
1089, 104, 105rngolidm 36805 . . . . . . . 8 ((𝑅 ∈ RingOps ∧ 𝐴𝑋) → ((GId‘𝐻)𝐻𝐴) = 𝐴)
109108eqcomd 2739 . . . . . . 7 ((𝑅 ∈ RingOps ∧ 𝐴𝑋) → 𝐴 = ((GId‘𝐻)𝐻𝐴))
110 oveq1 7416 . . . . . . . 8 (𝑦 = (GId‘𝐻) → (𝑦𝐻𝐴) = ((GId‘𝐻)𝐻𝐴))
111110rspceeqv 3634 . . . . . . 7 (((GId‘𝐻) ∈ 𝑋𝐴 = ((GId‘𝐻)𝐻𝐴)) → ∃𝑦𝑋 𝐴 = (𝑦𝐻𝐴))
112107, 109, 111syl2anc 585 . . . . . 6 ((𝑅 ∈ RingOps ∧ 𝐴𝑋) → ∃𝑦𝑋 𝐴 = (𝑦𝐻𝐴))
1131, 112sylan 581 . . . . 5 ((𝑅 ∈ CRingOps ∧ 𝐴𝑋) → ∃𝑦𝑋 𝐴 = (𝑦𝐻𝐴))
114 eqeq1 2737 . . . . . . 7 (𝑥 = 𝐴 → (𝑥 = (𝑦𝐻𝐴) ↔ 𝐴 = (𝑦𝐻𝐴)))
115114rexbidv 3179 . . . . . 6 (𝑥 = 𝐴 → (∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴) ↔ ∃𝑦𝑋 𝐴 = (𝑦𝐻𝐴)))
116115elrab 3684 . . . . 5 (𝐴 ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ↔ (𝐴𝑋 ∧ ∃𝑦𝑋 𝐴 = (𝑦𝐻𝐴)))
117102, 113, 116sylanbrc 584 . . . 4 ((𝑅 ∈ CRingOps ∧ 𝐴𝑋) → 𝐴 ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)})
118117snssd 4813 . . 3 ((𝑅 ∈ CRingOps ∧ 𝐴𝑋) → {𝐴} ⊆ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)})
119 snssg 4788 . . . . . . . . 9 (𝐴𝑋 → (𝐴𝑗 ↔ {𝐴} ⊆ 𝑗))
120119biimpar 479 . . . . . . . 8 ((𝐴𝑋 ∧ {𝐴} ⊆ 𝑗) → 𝐴𝑗)
1214, 9, 5idllmulcl 36888 . . . . . . . . . . . . . . 15 (((𝑅 ∈ RingOps ∧ 𝑗 ∈ (Idl‘𝑅)) ∧ (𝐴𝑗𝑦𝑋)) → (𝑦𝐻𝐴) ∈ 𝑗)
122121anassrs 469 . . . . . . . . . . . . . 14 ((((𝑅 ∈ RingOps ∧ 𝑗 ∈ (Idl‘𝑅)) ∧ 𝐴𝑗) ∧ 𝑦𝑋) → (𝑦𝐻𝐴) ∈ 𝑗)
123 eleq1 2822 . . . . . . . . . . . . . 14 (𝑥 = (𝑦𝐻𝐴) → (𝑥𝑗 ↔ (𝑦𝐻𝐴) ∈ 𝑗))
124122, 123syl5ibrcom 246 . . . . . . . . . . . . 13 ((((𝑅 ∈ RingOps ∧ 𝑗 ∈ (Idl‘𝑅)) ∧ 𝐴𝑗) ∧ 𝑦𝑋) → (𝑥 = (𝑦𝐻𝐴) → 𝑥𝑗))
125124rexlimdva 3156 . . . . . . . . . . . 12 (((𝑅 ∈ RingOps ∧ 𝑗 ∈ (Idl‘𝑅)) ∧ 𝐴𝑗) → (∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴) → 𝑥𝑗))
126125adantr 482 . . . . . . . . . . 11 ((((𝑅 ∈ RingOps ∧ 𝑗 ∈ (Idl‘𝑅)) ∧ 𝐴𝑗) ∧ 𝑥𝑋) → (∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴) → 𝑥𝑗))
127126ralrimiva 3147 . . . . . . . . . 10 (((𝑅 ∈ RingOps ∧ 𝑗 ∈ (Idl‘𝑅)) ∧ 𝐴𝑗) → ∀𝑥𝑋 (∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴) → 𝑥𝑗))
128 rabss 4070 . . . . . . . . . 10 ({𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑗 ↔ ∀𝑥𝑋 (∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴) → 𝑥𝑗))
129127, 128sylibr 233 . . . . . . . . 9 (((𝑅 ∈ RingOps ∧ 𝑗 ∈ (Idl‘𝑅)) ∧ 𝐴𝑗) → {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑗)
130129ex 414 . . . . . . . 8 ((𝑅 ∈ RingOps ∧ 𝑗 ∈ (Idl‘𝑅)) → (𝐴𝑗 → {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑗))
131120, 130syl5 34 . . . . . . 7 ((𝑅 ∈ RingOps ∧ 𝑗 ∈ (Idl‘𝑅)) → ((𝐴𝑋 ∧ {𝐴} ⊆ 𝑗) → {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑗))
132131expdimp 454 . . . . . 6 (((𝑅 ∈ RingOps ∧ 𝑗 ∈ (Idl‘𝑅)) ∧ 𝐴𝑋) → ({𝐴} ⊆ 𝑗 → {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑗))
133132an32s 651 . . . . 5 (((𝑅 ∈ RingOps ∧ 𝐴𝑋) ∧ 𝑗 ∈ (Idl‘𝑅)) → ({𝐴} ⊆ 𝑗 → {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑗))
134133ralrimiva 3147 . . . 4 ((𝑅 ∈ RingOps ∧ 𝐴𝑋) → ∀𝑗 ∈ (Idl‘𝑅)({𝐴} ⊆ 𝑗 → {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑗))
1351, 134sylan 581 . . 3 ((𝑅 ∈ CRingOps ∧ 𝐴𝑋) → ∀𝑗 ∈ (Idl‘𝑅)({𝐴} ⊆ 𝑗 → {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑗))
136101, 118, 1353jca 1129 . 2 ((𝑅 ∈ CRingOps ∧ 𝐴𝑋) → ({𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ∈ (Idl‘𝑅) ∧ {𝐴} ⊆ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑗 ∈ (Idl‘𝑅)({𝐴} ⊆ 𝑗 → {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑗)))
137 snssi 4812 . . 3 (𝐴𝑋 → {𝐴} ⊆ 𝑋)
1384, 5igenval2 36934 . . 3 ((𝑅 ∈ RingOps ∧ {𝐴} ⊆ 𝑋) → ((𝑅 IdlGen {𝐴}) = {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ↔ ({𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ∈ (Idl‘𝑅) ∧ {𝐴} ⊆ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑗 ∈ (Idl‘𝑅)({𝐴} ⊆ 𝑗 → {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑗))))
1391, 137, 138syl2an 597 . 2 ((𝑅 ∈ CRingOps ∧ 𝐴𝑋) → ((𝑅 IdlGen {𝐴}) = {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ↔ ({𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ∈ (Idl‘𝑅) ∧ {𝐴} ⊆ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑗 ∈ (Idl‘𝑅)({𝐴} ⊆ 𝑗 → {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑗))))
140136, 139mpbird 257 1 ((𝑅 ∈ CRingOps ∧ 𝐴𝑋) → (𝑅 IdlGen {𝐴}) = {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)})
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 397  w3a 1088   = wceq 1542  wcel 2107  wral 3062  wrex 3071  {crab 3433  wss 3949  {csn 4629  ran crn 5678  cfv 6544  (class class class)co 7409  1st c1st 7973  2nd c2nd 7974  GIdcgi 29743  RingOpscrngo 36762  CRingOpsccring 36861  Idlcidl 36875   IdlGen cigen 36927
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5286  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7725
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-int 4952  df-iun 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-id 5575  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-riota 7365  df-ov 7412  df-oprab 7413  df-mpo 7414  df-1st 7975  df-2nd 7976  df-grpo 29746  df-gid 29747  df-ginv 29748  df-ablo 29798  df-ass 36711  df-exid 36713  df-mgmOLD 36717  df-sgrOLD 36729  df-mndo 36735  df-rngo 36763  df-com2 36858  df-crngo 36862  df-idl 36878  df-igen 36928
This theorem is referenced by:  isfldidl  36936  ispridlc  36938
  Copyright terms: Public domain W3C validator