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 36555
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 36488 . . . . 5 (𝑅 ∈ CRingOps → 𝑅 ∈ RingOps)
2 ssrab2 4042 . . . . . . 7 {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑋
32a1i 11 . . . . . 6 ((𝑅 ∈ RingOps ∧ 𝐴𝑋) → {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑋)
4 prnc.1 . . . . . . . . 9 𝐺 = (1st𝑅)
5 prnc.3 . . . . . . . . 9 𝑋 = ran 𝐺
6 eqid 2737 . . . . . . . . 9 (GId‘𝐺) = (GId‘𝐺)
74, 5, 6rngo0cl 36407 . . . . . . . 8 (𝑅 ∈ RingOps → (GId‘𝐺) ∈ 𝑋)
87adantr 482 . . . . . . 7 ((𝑅 ∈ RingOps ∧ 𝐴𝑋) → (GId‘𝐺) ∈ 𝑋)
9 prnc.2 . . . . . . . . . 10 𝐻 = (2nd𝑅)
106, 5, 4, 9rngolz 36410 . . . . . . . . 9 ((𝑅 ∈ RingOps ∧ 𝐴𝑋) → ((GId‘𝐺)𝐻𝐴) = (GId‘𝐺))
1110eqcomd 2743 . . . . . . . 8 ((𝑅 ∈ RingOps ∧ 𝐴𝑋) → (GId‘𝐺) = ((GId‘𝐺)𝐻𝐴))
12 oveq1 7369 . . . . . . . . 9 (𝑦 = (GId‘𝐺) → (𝑦𝐻𝐴) = ((GId‘𝐺)𝐻𝐴))
1312rspceeqv 3600 . . . . . . . 8 (((GId‘𝐺) ∈ 𝑋 ∧ (GId‘𝐺) = ((GId‘𝐺)𝐻𝐴)) → ∃𝑦𝑋 (GId‘𝐺) = (𝑦𝐻𝐴))
148, 11, 13syl2anc 585 . . . . . . 7 ((𝑅 ∈ RingOps ∧ 𝐴𝑋) → ∃𝑦𝑋 (GId‘𝐺) = (𝑦𝐻𝐴))
15 eqeq1 2741 . . . . . . . . 9 (𝑥 = (GId‘𝐺) → (𝑥 = (𝑦𝐻𝐴) ↔ (GId‘𝐺) = (𝑦𝐻𝐴)))
1615rexbidv 3176 . . . . . . . 8 (𝑥 = (GId‘𝐺) → (∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴) ↔ ∃𝑦𝑋 (GId‘𝐺) = (𝑦𝐻𝐴)))
1716elrab 3650 . . . . . . 7 ((GId‘𝐺) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ↔ ((GId‘𝐺) ∈ 𝑋 ∧ ∃𝑦𝑋 (GId‘𝐺) = (𝑦𝐻𝐴)))
188, 14, 17sylanbrc 584 . . . . . 6 ((𝑅 ∈ RingOps ∧ 𝐴𝑋) → (GId‘𝐺) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)})
19 eqeq1 2741 . . . . . . . . . . 11 (𝑥 = 𝑢 → (𝑥 = (𝑦𝐻𝐴) ↔ 𝑢 = (𝑦𝐻𝐴)))
2019rexbidv 3176 . . . . . . . . . 10 (𝑥 = 𝑢 → (∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴) ↔ ∃𝑦𝑋 𝑢 = (𝑦𝐻𝐴)))
21 oveq1 7369 . . . . . . . . . . . 12 (𝑦 = 𝑟 → (𝑦𝐻𝐴) = (𝑟𝐻𝐴))
2221eqeq2d 2748 . . . . . . . . . . 11 (𝑦 = 𝑟 → (𝑢 = (𝑦𝐻𝐴) ↔ 𝑢 = (𝑟𝐻𝐴)))
2322cbvrexvw 3229 . . . . . . . . . 10 (∃𝑦𝑋 𝑢 = (𝑦𝐻𝐴) ↔ ∃𝑟𝑋 𝑢 = (𝑟𝐻𝐴))
2420, 23bitrdi 287 . . . . . . . . 9 (𝑥 = 𝑢 → (∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴) ↔ ∃𝑟𝑋 𝑢 = (𝑟𝐻𝐴)))
2524elrab 3650 . . . . . . . 8 (𝑢 ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ↔ (𝑢𝑋 ∧ ∃𝑟𝑋 𝑢 = (𝑟𝐻𝐴)))
26 eqeq1 2741 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑣 → (𝑥 = (𝑦𝐻𝐴) ↔ 𝑣 = (𝑦𝐻𝐴)))
2726rexbidv 3176 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑣 → (∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴) ↔ ∃𝑦𝑋 𝑣 = (𝑦𝐻𝐴)))
28 oveq1 7369 . . . . . . . . . . . . . . . . . 18 (𝑦 = 𝑠 → (𝑦𝐻𝐴) = (𝑠𝐻𝐴))
2928eqeq2d 2748 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑠 → (𝑣 = (𝑦𝐻𝐴) ↔ 𝑣 = (𝑠𝐻𝐴)))
3029cbvrexvw 3229 . . . . . . . . . . . . . . . 16 (∃𝑦𝑋 𝑣 = (𝑦𝐻𝐴) ↔ ∃𝑠𝑋 𝑣 = (𝑠𝐻𝐴))
3127, 30bitrdi 287 . . . . . . . . . . . . . . 15 (𝑥 = 𝑣 → (∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴) ↔ ∃𝑠𝑋 𝑣 = (𝑠𝐻𝐴)))
3231elrab 3650 . . . . . . . . . . . . . 14 (𝑣 ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ↔ (𝑣𝑋 ∧ ∃𝑠𝑋 𝑣 = (𝑠𝐻𝐴)))
334, 9, 5rngodir 36393 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑅 ∈ RingOps ∧ (𝑟𝑋𝑠𝑋𝐴𝑋)) → ((𝑟𝐺𝑠)𝐻𝐴) = ((𝑟𝐻𝐴)𝐺(𝑠𝐻𝐴)))
34333exp2 1355 . . . . . . . . . . . . . . . . . . . . 21 (𝑅 ∈ RingOps → (𝑟𝑋 → (𝑠𝑋 → (𝐴𝑋 → ((𝑟𝐺𝑠)𝐻𝐴) = ((𝑟𝐻𝐴)𝐺(𝑠𝐻𝐴))))))
3534imp42 428 . . . . . . . . . . . . . . . . . . . 20 (((𝑅 ∈ RingOps ∧ (𝑟𝑋𝑠𝑋)) ∧ 𝐴𝑋) → ((𝑟𝐺𝑠)𝐻𝐴) = ((𝑟𝐻𝐴)𝐺(𝑠𝐻𝐴)))
364, 5rngogcl 36400 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑅 ∈ RingOps ∧ 𝑟𝑋𝑠𝑋) → (𝑟𝐺𝑠) ∈ 𝑋)
37363expib 1123 . . . . . . . . . . . . . . . . . . . . . 22 (𝑅 ∈ RingOps → ((𝑟𝑋𝑠𝑋) → (𝑟𝐺𝑠) ∈ 𝑋))
3837imdistani 570 . . . . . . . . . . . . . . . . . . . . 21 ((𝑅 ∈ RingOps ∧ (𝑟𝑋𝑠𝑋)) → (𝑅 ∈ RingOps ∧ (𝑟𝐺𝑠) ∈ 𝑋))
394, 9, 5rngocl 36389 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑅 ∈ RingOps ∧ (𝑟𝐺𝑠) ∈ 𝑋𝐴𝑋) → ((𝑟𝐺𝑠)𝐻𝐴) ∈ 𝑋)
40393expa 1119 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑅 ∈ RingOps ∧ (𝑟𝐺𝑠) ∈ 𝑋) ∧ 𝐴𝑋) → ((𝑟𝐺𝑠)𝐻𝐴) ∈ 𝑋)
41 eqid 2737 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑟𝐺𝑠)𝐻𝐴) = ((𝑟𝐺𝑠)𝐻𝐴)
42 oveq1 7369 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 = (𝑟𝐺𝑠) → (𝑦𝐻𝐴) = ((𝑟𝐺𝑠)𝐻𝐴))
4342rspceeqv 3600 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑟𝐺𝑠) ∈ 𝑋 ∧ ((𝑟𝐺𝑠)𝐻𝐴) = ((𝑟𝐺𝑠)𝐻𝐴)) → ∃𝑦𝑋 ((𝑟𝐺𝑠)𝐻𝐴) = (𝑦𝐻𝐴))
4441, 43mpan2 690 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑟𝐺𝑠) ∈ 𝑋 → ∃𝑦𝑋 ((𝑟𝐺𝑠)𝐻𝐴) = (𝑦𝐻𝐴))
4544ad2antlr 726 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑅 ∈ RingOps ∧ (𝑟𝐺𝑠) ∈ 𝑋) ∧ 𝐴𝑋) → ∃𝑦𝑋 ((𝑟𝐺𝑠)𝐻𝐴) = (𝑦𝐻𝐴))
46 eqeq1 2741 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = ((𝑟𝐺𝑠)𝐻𝐴) → (𝑥 = (𝑦𝐻𝐴) ↔ ((𝑟𝐺𝑠)𝐻𝐴) = (𝑦𝐻𝐴)))
4746rexbidv 3176 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = ((𝑟𝐺𝑠)𝐻𝐴) → (∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴) ↔ ∃𝑦𝑋 ((𝑟𝐺𝑠)𝐻𝐴) = (𝑦𝐻𝐴)))
4847elrab 3650 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑟𝐺𝑠)𝐻𝐴) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ↔ (((𝑟𝐺𝑠)𝐻𝐴) ∈ 𝑋 ∧ ∃𝑦𝑋 ((𝑟𝐺𝑠)𝐻𝐴) = (𝑦𝐻𝐴)))
4940, 45, 48sylanbrc 584 . . . . . . . . . . . . . . . . . . . . 21 (((𝑅 ∈ RingOps ∧ (𝑟𝐺𝑠) ∈ 𝑋) ∧ 𝐴𝑋) → ((𝑟𝐺𝑠)𝐻𝐴) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)})
5038, 49sylan 581 . . . . . . . . . . . . . . . . . . . 20 (((𝑅 ∈ RingOps ∧ (𝑟𝑋𝑠𝑋)) ∧ 𝐴𝑋) → ((𝑟𝐺𝑠)𝐻𝐴) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)})
5135, 50eqeltrrd 2839 . . . . . . . . . . . . . . . . . . 19 (((𝑅 ∈ RingOps ∧ (𝑟𝑋𝑠𝑋)) ∧ 𝐴𝑋) → ((𝑟𝐻𝐴)𝐺(𝑠𝐻𝐴)) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)})
5251an32s 651 . . . . . . . . . . . . . . . . . 18 (((𝑅 ∈ RingOps ∧ 𝐴𝑋) ∧ (𝑟𝑋𝑠𝑋)) → ((𝑟𝐻𝐴)𝐺(𝑠𝐻𝐴)) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)})
5352anassrs 469 . . . . . . . . . . . . . . . . 17 ((((𝑅 ∈ RingOps ∧ 𝐴𝑋) ∧ 𝑟𝑋) ∧ 𝑠𝑋) → ((𝑟𝐻𝐴)𝐺(𝑠𝐻𝐴)) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)})
54 oveq2 7370 . . . . . . . . . . . . . . . . . 18 (𝑣 = (𝑠𝐻𝐴) → ((𝑟𝐻𝐴)𝐺𝑣) = ((𝑟𝐻𝐴)𝐺(𝑠𝐻𝐴)))
5554eleq1d 2823 . . . . . . . . . . . . . . . . 17 (𝑣 = (𝑠𝐻𝐴) → (((𝑟𝐻𝐴)𝐺𝑣) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ↔ ((𝑟𝐻𝐴)𝐺(𝑠𝐻𝐴)) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)}))
5653, 55syl5ibrcom 247 . . . . . . . . . . . . . . . 16 ((((𝑅 ∈ RingOps ∧ 𝐴𝑋) ∧ 𝑟𝑋) ∧ 𝑠𝑋) → (𝑣 = (𝑠𝐻𝐴) → ((𝑟𝐻𝐴)𝐺𝑣) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)}))
5756rexlimdva 3153 . . . . . . . . . . . . . . 15 (((𝑅 ∈ RingOps ∧ 𝐴𝑋) ∧ 𝑟𝑋) → (∃𝑠𝑋 𝑣 = (𝑠𝐻𝐴) → ((𝑟𝐻𝐴)𝐺𝑣) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)}))
5857adantld 492 . . . . . . . . . . . . . 14 (((𝑅 ∈ RingOps ∧ 𝐴𝑋) ∧ 𝑟𝑋) → ((𝑣𝑋 ∧ ∃𝑠𝑋 𝑣 = (𝑠𝐻𝐴)) → ((𝑟𝐻𝐴)𝐺𝑣) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)}))
5932, 58biimtrid 241 . . . . . . . . . . . . 13 (((𝑅 ∈ RingOps ∧ 𝐴𝑋) ∧ 𝑟𝑋) → (𝑣 ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} → ((𝑟𝐻𝐴)𝐺𝑣) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)}))
6059ralrimiv 3143 . . . . . . . . . . . 12 (((𝑅 ∈ RingOps ∧ 𝐴𝑋) ∧ 𝑟𝑋) → ∀𝑣 ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ((𝑟𝐻𝐴)𝐺𝑣) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)})
614, 9, 5rngoass 36394 . . . . . . . . . . . . . . . . . 18 ((𝑅 ∈ RingOps ∧ (𝑤𝑋𝑟𝑋𝐴𝑋)) → ((𝑤𝐻𝑟)𝐻𝐴) = (𝑤𝐻(𝑟𝐻𝐴)))
62613exp2 1355 . . . . . . . . . . . . . . . . 17 (𝑅 ∈ RingOps → (𝑤𝑋 → (𝑟𝑋 → (𝐴𝑋 → ((𝑤𝐻𝑟)𝐻𝐴) = (𝑤𝐻(𝑟𝐻𝐴))))))
6362imp42 428 . . . . . . . . . . . . . . . 16 (((𝑅 ∈ RingOps ∧ (𝑤𝑋𝑟𝑋)) ∧ 𝐴𝑋) → ((𝑤𝐻𝑟)𝐻𝐴) = (𝑤𝐻(𝑟𝐻𝐴)))
6463an32s 651 . . . . . . . . . . . . . . 15 (((𝑅 ∈ RingOps ∧ 𝐴𝑋) ∧ (𝑤𝑋𝑟𝑋)) → ((𝑤𝐻𝑟)𝐻𝐴) = (𝑤𝐻(𝑟𝐻𝐴)))
654, 9, 5rngocl 36389 . . . . . . . . . . . . . . . . . . 19 ((𝑅 ∈ RingOps ∧ 𝑤𝑋𝑟𝑋) → (𝑤𝐻𝑟) ∈ 𝑋)
66653expib 1123 . . . . . . . . . . . . . . . . . 18 (𝑅 ∈ RingOps → ((𝑤𝑋𝑟𝑋) → (𝑤𝐻𝑟) ∈ 𝑋))
6766imdistani 570 . . . . . . . . . . . . . . . . 17 ((𝑅 ∈ RingOps ∧ (𝑤𝑋𝑟𝑋)) → (𝑅 ∈ RingOps ∧ (𝑤𝐻𝑟) ∈ 𝑋))
684, 9, 5rngocl 36389 . . . . . . . . . . . . . . . . . . 19 ((𝑅 ∈ RingOps ∧ (𝑤𝐻𝑟) ∈ 𝑋𝐴𝑋) → ((𝑤𝐻𝑟)𝐻𝐴) ∈ 𝑋)
69683expa 1119 . . . . . . . . . . . . . . . . . 18 (((𝑅 ∈ RingOps ∧ (𝑤𝐻𝑟) ∈ 𝑋) ∧ 𝐴𝑋) → ((𝑤𝐻𝑟)𝐻𝐴) ∈ 𝑋)
70 eqid 2737 . . . . . . . . . . . . . . . . . . . 20 ((𝑤𝐻𝑟)𝐻𝐴) = ((𝑤𝐻𝑟)𝐻𝐴)
71 oveq1 7369 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 = (𝑤𝐻𝑟) → (𝑦𝐻𝐴) = ((𝑤𝐻𝑟)𝐻𝐴))
7271rspceeqv 3600 . . . . . . . . . . . . . . . . . . . 20 (((𝑤𝐻𝑟) ∈ 𝑋 ∧ ((𝑤𝐻𝑟)𝐻𝐴) = ((𝑤𝐻𝑟)𝐻𝐴)) → ∃𝑦𝑋 ((𝑤𝐻𝑟)𝐻𝐴) = (𝑦𝐻𝐴))
7370, 72mpan2 690 . . . . . . . . . . . . . . . . . . 19 ((𝑤𝐻𝑟) ∈ 𝑋 → ∃𝑦𝑋 ((𝑤𝐻𝑟)𝐻𝐴) = (𝑦𝐻𝐴))
7473ad2antlr 726 . . . . . . . . . . . . . . . . . 18 (((𝑅 ∈ RingOps ∧ (𝑤𝐻𝑟) ∈ 𝑋) ∧ 𝐴𝑋) → ∃𝑦𝑋 ((𝑤𝐻𝑟)𝐻𝐴) = (𝑦𝐻𝐴))
75 eqeq1 2741 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = ((𝑤𝐻𝑟)𝐻𝐴) → (𝑥 = (𝑦𝐻𝐴) ↔ ((𝑤𝐻𝑟)𝐻𝐴) = (𝑦𝐻𝐴)))
7675rexbidv 3176 . . . . . . . . . . . . . . . . . . 19 (𝑥 = ((𝑤𝐻𝑟)𝐻𝐴) → (∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴) ↔ ∃𝑦𝑋 ((𝑤𝐻𝑟)𝐻𝐴) = (𝑦𝐻𝐴)))
7776elrab 3650 . . . . . . . . . . . . . . . . . 18 (((𝑤𝐻𝑟)𝐻𝐴) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ↔ (((𝑤𝐻𝑟)𝐻𝐴) ∈ 𝑋 ∧ ∃𝑦𝑋 ((𝑤𝐻𝑟)𝐻𝐴) = (𝑦𝐻𝐴)))
7869, 74, 77sylanbrc 584 . . . . . . . . . . . . . . . . 17 (((𝑅 ∈ RingOps ∧ (𝑤𝐻𝑟) ∈ 𝑋) ∧ 𝐴𝑋) → ((𝑤𝐻𝑟)𝐻𝐴) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)})
7967, 78sylan 581 . . . . . . . . . . . . . . . 16 (((𝑅 ∈ RingOps ∧ (𝑤𝑋𝑟𝑋)) ∧ 𝐴𝑋) → ((𝑤𝐻𝑟)𝐻𝐴) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)})
8079an32s 651 . . . . . . . . . . . . . . 15 (((𝑅 ∈ RingOps ∧ 𝐴𝑋) ∧ (𝑤𝑋𝑟𝑋)) → ((𝑤𝐻𝑟)𝐻𝐴) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)})
8164, 80eqeltrrd 2839 . . . . . . . . . . . . . 14 (((𝑅 ∈ RingOps ∧ 𝐴𝑋) ∧ (𝑤𝑋𝑟𝑋)) → (𝑤𝐻(𝑟𝐻𝐴)) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)})
8281anass1rs 654 . . . . . . . . . . . . 13 ((((𝑅 ∈ RingOps ∧ 𝐴𝑋) ∧ 𝑟𝑋) ∧ 𝑤𝑋) → (𝑤𝐻(𝑟𝐻𝐴)) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)})
8382ralrimiva 3144 . . . . . . . . . . . 12 (((𝑅 ∈ RingOps ∧ 𝐴𝑋) ∧ 𝑟𝑋) → ∀𝑤𝑋 (𝑤𝐻(𝑟𝐻𝐴)) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)})
8460, 83jca 513 . . . . . . . . . . 11 (((𝑅 ∈ RingOps ∧ 𝐴𝑋) ∧ 𝑟𝑋) → (∀𝑣 ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ((𝑟𝐻𝐴)𝐺𝑣) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑤𝑋 (𝑤𝐻(𝑟𝐻𝐴)) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)}))
85 oveq1 7369 . . . . . . . . . . . . . 14 (𝑢 = (𝑟𝐻𝐴) → (𝑢𝐺𝑣) = ((𝑟𝐻𝐴)𝐺𝑣))
8685eleq1d 2823 . . . . . . . . . . . . 13 (𝑢 = (𝑟𝐻𝐴) → ((𝑢𝐺𝑣) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ↔ ((𝑟𝐻𝐴)𝐺𝑣) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)}))
8786ralbidv 3175 . . . . . . . . . . . 12 (𝑢 = (𝑟𝐻𝐴) → (∀𝑣 ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} (𝑢𝐺𝑣) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ↔ ∀𝑣 ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ((𝑟𝐻𝐴)𝐺𝑣) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)}))
88 oveq2 7370 . . . . . . . . . . . . . 14 (𝑢 = (𝑟𝐻𝐴) → (𝑤𝐻𝑢) = (𝑤𝐻(𝑟𝐻𝐴)))
8988eleq1d 2823 . . . . . . . . . . . . 13 (𝑢 = (𝑟𝐻𝐴) → ((𝑤𝐻𝑢) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ↔ (𝑤𝐻(𝑟𝐻𝐴)) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)}))
9089ralbidv 3175 . . . . . . . . . . . 12 (𝑢 = (𝑟𝐻𝐴) → (∀𝑤𝑋 (𝑤𝐻𝑢) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ↔ ∀𝑤𝑋 (𝑤𝐻(𝑟𝐻𝐴)) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)}))
9187, 90anbi12d 632 . . . . . . . . . . 11 (𝑢 = (𝑟𝐻𝐴) → ((∀𝑣 ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} (𝑢𝐺𝑣) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑤𝑋 (𝑤𝐻𝑢) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)}) ↔ (∀𝑣 ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ((𝑟𝐻𝐴)𝐺𝑣) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑤𝑋 (𝑤𝐻(𝑟𝐻𝐴)) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)})))
9284, 91syl5ibrcom 247 . . . . . . . . . 10 (((𝑅 ∈ RingOps ∧ 𝐴𝑋) ∧ 𝑟𝑋) → (𝑢 = (𝑟𝐻𝐴) → (∀𝑣 ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} (𝑢𝐺𝑣) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑤𝑋 (𝑤𝐻𝑢) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)})))
9392rexlimdva 3153 . . . . . . . . 9 ((𝑅 ∈ RingOps ∧ 𝐴𝑋) → (∃𝑟𝑋 𝑢 = (𝑟𝐻𝐴) → (∀𝑣 ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} (𝑢𝐺𝑣) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑤𝑋 (𝑤𝐻𝑢) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)})))
9493adantld 492 . . . . . . . 8 ((𝑅 ∈ RingOps ∧ 𝐴𝑋) → ((𝑢𝑋 ∧ ∃𝑟𝑋 𝑢 = (𝑟𝐻𝐴)) → (∀𝑣 ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} (𝑢𝐺𝑣) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑤𝑋 (𝑤𝐻𝑢) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)})))
9525, 94biimtrid 241 . . . . . . 7 ((𝑅 ∈ RingOps ∧ 𝐴𝑋) → (𝑢 ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} → (∀𝑣 ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} (𝑢𝐺𝑣) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑤𝑋 (𝑤𝐻𝑢) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)})))
9695ralrimiv 3143 . . . . . 6 ((𝑅 ∈ RingOps ∧ 𝐴𝑋) → ∀𝑢 ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} (∀𝑣 ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} (𝑢𝐺𝑣) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑤𝑋 (𝑤𝐻𝑢) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)}))
973, 18, 963jca 1129 . . . . 5 ((𝑅 ∈ RingOps ∧ 𝐴𝑋) → ({𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑋 ∧ (GId‘𝐺) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑢 ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} (∀𝑣 ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} (𝑢𝐺𝑣) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑤𝑋 (𝑤𝐻𝑢) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)})))
981, 97sylan 581 . . . 4 ((𝑅 ∈ CRingOps ∧ 𝐴𝑋) → ({𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑋 ∧ (GId‘𝐺) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑢 ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} (∀𝑣 ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} (𝑢𝐺𝑣) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑤𝑋 (𝑤𝐻𝑢) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)})))
994, 9, 5, 6isidlc 36503 . . . . 5 (𝑅 ∈ CRingOps → ({𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ∈ (Idl‘𝑅) ↔ ({𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑋 ∧ (GId‘𝐺) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑢 ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} (∀𝑣 ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} (𝑢𝐺𝑣) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑤𝑋 (𝑤𝐻𝑢) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)}))))
10099adantr 482 . . . 4 ((𝑅 ∈ CRingOps ∧ 𝐴𝑋) → ({𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ∈ (Idl‘𝑅) ↔ ({𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑋 ∧ (GId‘𝐺) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑢 ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} (∀𝑣 ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} (𝑢𝐺𝑣) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑤𝑋 (𝑤𝐻𝑢) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)}))))
10198, 100mpbird 257 . . 3 ((𝑅 ∈ CRingOps ∧ 𝐴𝑋) → {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ∈ (Idl‘𝑅))
102 simpr 486 . . . . 5 ((𝑅 ∈ CRingOps ∧ 𝐴𝑋) → 𝐴𝑋)
1034rneqi 5897 . . . . . . . . . 10 ran 𝐺 = ran (1st𝑅)
1045, 103eqtri 2765 . . . . . . . . 9 𝑋 = ran (1st𝑅)
105 eqid 2737 . . . . . . . . 9 (GId‘𝐻) = (GId‘𝐻)
106104, 9, 105rngo1cl 36427 . . . . . . . 8 (𝑅 ∈ RingOps → (GId‘𝐻) ∈ 𝑋)
107106adantr 482 . . . . . . 7 ((𝑅 ∈ RingOps ∧ 𝐴𝑋) → (GId‘𝐻) ∈ 𝑋)
1089, 104, 105rngolidm 36425 . . . . . . . 8 ((𝑅 ∈ RingOps ∧ 𝐴𝑋) → ((GId‘𝐻)𝐻𝐴) = 𝐴)
109108eqcomd 2743 . . . . . . 7 ((𝑅 ∈ RingOps ∧ 𝐴𝑋) → 𝐴 = ((GId‘𝐻)𝐻𝐴))
110 oveq1 7369 . . . . . . . 8 (𝑦 = (GId‘𝐻) → (𝑦𝐻𝐴) = ((GId‘𝐻)𝐻𝐴))
111110rspceeqv 3600 . . . . . . 7 (((GId‘𝐻) ∈ 𝑋𝐴 = ((GId‘𝐻)𝐻𝐴)) → ∃𝑦𝑋 𝐴 = (𝑦𝐻𝐴))
112107, 109, 111syl2anc 585 . . . . . 6 ((𝑅 ∈ RingOps ∧ 𝐴𝑋) → ∃𝑦𝑋 𝐴 = (𝑦𝐻𝐴))
1131, 112sylan 581 . . . . 5 ((𝑅 ∈ CRingOps ∧ 𝐴𝑋) → ∃𝑦𝑋 𝐴 = (𝑦𝐻𝐴))
114 eqeq1 2741 . . . . . . 7 (𝑥 = 𝐴 → (𝑥 = (𝑦𝐻𝐴) ↔ 𝐴 = (𝑦𝐻𝐴)))
115114rexbidv 3176 . . . . . 6 (𝑥 = 𝐴 → (∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴) ↔ ∃𝑦𝑋 𝐴 = (𝑦𝐻𝐴)))
116115elrab 3650 . . . . 5 (𝐴 ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ↔ (𝐴𝑋 ∧ ∃𝑦𝑋 𝐴 = (𝑦𝐻𝐴)))
117102, 113, 116sylanbrc 584 . . . 4 ((𝑅 ∈ CRingOps ∧ 𝐴𝑋) → 𝐴 ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)})
118117snssd 4774 . . 3 ((𝑅 ∈ CRingOps ∧ 𝐴𝑋) → {𝐴} ⊆ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)})
119 snssg 4749 . . . . . . . . 9 (𝐴𝑋 → (𝐴𝑗 ↔ {𝐴} ⊆ 𝑗))
120119biimpar 479 . . . . . . . 8 ((𝐴𝑋 ∧ {𝐴} ⊆ 𝑗) → 𝐴𝑗)
1214, 9, 5idllmulcl 36508 . . . . . . . . . . . . . . 15 (((𝑅 ∈ RingOps ∧ 𝑗 ∈ (Idl‘𝑅)) ∧ (𝐴𝑗𝑦𝑋)) → (𝑦𝐻𝐴) ∈ 𝑗)
122121anassrs 469 . . . . . . . . . . . . . 14 ((((𝑅 ∈ RingOps ∧ 𝑗 ∈ (Idl‘𝑅)) ∧ 𝐴𝑗) ∧ 𝑦𝑋) → (𝑦𝐻𝐴) ∈ 𝑗)
123 eleq1 2826 . . . . . . . . . . . . . 14 (𝑥 = (𝑦𝐻𝐴) → (𝑥𝑗 ↔ (𝑦𝐻𝐴) ∈ 𝑗))
124122, 123syl5ibrcom 247 . . . . . . . . . . . . 13 ((((𝑅 ∈ RingOps ∧ 𝑗 ∈ (Idl‘𝑅)) ∧ 𝐴𝑗) ∧ 𝑦𝑋) → (𝑥 = (𝑦𝐻𝐴) → 𝑥𝑗))
125124rexlimdva 3153 . . . . . . . . . . . 12 (((𝑅 ∈ RingOps ∧ 𝑗 ∈ (Idl‘𝑅)) ∧ 𝐴𝑗) → (∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴) → 𝑥𝑗))
126125adantr 482 . . . . . . . . . . 11 ((((𝑅 ∈ RingOps ∧ 𝑗 ∈ (Idl‘𝑅)) ∧ 𝐴𝑗) ∧ 𝑥𝑋) → (∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴) → 𝑥𝑗))
127126ralrimiva 3144 . . . . . . . . . 10 (((𝑅 ∈ RingOps ∧ 𝑗 ∈ (Idl‘𝑅)) ∧ 𝐴𝑗) → ∀𝑥𝑋 (∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴) → 𝑥𝑗))
128 rabss 4034 . . . . . . . . . 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 3144 . . . 4 ((𝑅 ∈ RingOps ∧ 𝐴𝑋) → ∀𝑗 ∈ (Idl‘𝑅)({𝐴} ⊆ 𝑗 → {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑗))
1351, 134sylan 581 . . 3 ((𝑅 ∈ CRingOps ∧ 𝐴𝑋) → ∀𝑗 ∈ (Idl‘𝑅)({𝐴} ⊆ 𝑗 → {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑗))
136101, 118, 1353jca 1129 . 2 ((𝑅 ∈ CRingOps ∧ 𝐴𝑋) → ({𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ∈ (Idl‘𝑅) ∧ {𝐴} ⊆ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑗 ∈ (Idl‘𝑅)({𝐴} ⊆ 𝑗 → {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑗)))
137 snssi 4773 . . 3 (𝐴𝑋 → {𝐴} ⊆ 𝑋)
1384, 5igenval2 36554 . . 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 3065  wrex 3074  {crab 3410  wss 3915  {csn 4591  ran crn 5639  cfv 6501  (class class class)co 7362  1st c1st 7924  2nd c2nd 7925  GIdcgi 29474  RingOpscrngo 36382  CRingOpsccring 36481  Idlcidl 36495   IdlGen cigen 36547
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 2708  ax-rep 5247  ax-sep 5261  ax-nul 5268  ax-pow 5325  ax-pr 5389  ax-un 7677
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 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-ral 3066  df-rex 3075  df-rmo 3356  df-reu 3357  df-rab 3411  df-v 3450  df-sbc 3745  df-csb 3861  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-int 4913  df-iun 4961  df-br 5111  df-opab 5173  df-mpt 5194  df-id 5536  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-fv 6509  df-riota 7318  df-ov 7365  df-oprab 7366  df-mpo 7367  df-1st 7926  df-2nd 7927  df-grpo 29477  df-gid 29478  df-ginv 29479  df-ablo 29529  df-ass 36331  df-exid 36333  df-mgmOLD 36337  df-sgrOLD 36349  df-mndo 36355  df-rngo 36383  df-com2 36478  df-crngo 36482  df-idl 36498  df-igen 36548
This theorem is referenced by:  isfldidl  36556  ispridlc  36558
  Copyright terms: Public domain W3C validator