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

Theorem prnc 35785
 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 35718 . . . . 5 (𝑅 ∈ CRingOps → 𝑅 ∈ RingOps)
2 ssrab2 3984 . . . . . . 7 {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑋
32a1i 11 . . . . . 6 ((𝑅 ∈ RingOps ∧ 𝐴𝑋) → {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑋)
4 prnc.1 . . . . . . . . 9 𝐺 = (1st𝑅)
5 prnc.3 . . . . . . . . 9 𝑋 = ran 𝐺
6 eqid 2758 . . . . . . . . 9 (GId‘𝐺) = (GId‘𝐺)
74, 5, 6rngo0cl 35637 . . . . . . . 8 (𝑅 ∈ RingOps → (GId‘𝐺) ∈ 𝑋)
87adantr 484 . . . . . . 7 ((𝑅 ∈ RingOps ∧ 𝐴𝑋) → (GId‘𝐺) ∈ 𝑋)
9 prnc.2 . . . . . . . . . 10 𝐻 = (2nd𝑅)
106, 5, 4, 9rngolz 35640 . . . . . . . . 9 ((𝑅 ∈ RingOps ∧ 𝐴𝑋) → ((GId‘𝐺)𝐻𝐴) = (GId‘𝐺))
1110eqcomd 2764 . . . . . . . 8 ((𝑅 ∈ RingOps ∧ 𝐴𝑋) → (GId‘𝐺) = ((GId‘𝐺)𝐻𝐴))
12 oveq1 7157 . . . . . . . . 9 (𝑦 = (GId‘𝐺) → (𝑦𝐻𝐴) = ((GId‘𝐺)𝐻𝐴))
1312rspceeqv 3556 . . . . . . . 8 (((GId‘𝐺) ∈ 𝑋 ∧ (GId‘𝐺) = ((GId‘𝐺)𝐻𝐴)) → ∃𝑦𝑋 (GId‘𝐺) = (𝑦𝐻𝐴))
148, 11, 13syl2anc 587 . . . . . . 7 ((𝑅 ∈ RingOps ∧ 𝐴𝑋) → ∃𝑦𝑋 (GId‘𝐺) = (𝑦𝐻𝐴))
15 eqeq1 2762 . . . . . . . . 9 (𝑥 = (GId‘𝐺) → (𝑥 = (𝑦𝐻𝐴) ↔ (GId‘𝐺) = (𝑦𝐻𝐴)))
1615rexbidv 3221 . . . . . . . 8 (𝑥 = (GId‘𝐺) → (∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴) ↔ ∃𝑦𝑋 (GId‘𝐺) = (𝑦𝐻𝐴)))
1716elrab 3602 . . . . . . 7 ((GId‘𝐺) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ↔ ((GId‘𝐺) ∈ 𝑋 ∧ ∃𝑦𝑋 (GId‘𝐺) = (𝑦𝐻𝐴)))
188, 14, 17sylanbrc 586 . . . . . 6 ((𝑅 ∈ RingOps ∧ 𝐴𝑋) → (GId‘𝐺) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)})
19 eqeq1 2762 . . . . . . . . . . 11 (𝑥 = 𝑢 → (𝑥 = (𝑦𝐻𝐴) ↔ 𝑢 = (𝑦𝐻𝐴)))
2019rexbidv 3221 . . . . . . . . . 10 (𝑥 = 𝑢 → (∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴) ↔ ∃𝑦𝑋 𝑢 = (𝑦𝐻𝐴)))
21 oveq1 7157 . . . . . . . . . . . 12 (𝑦 = 𝑟 → (𝑦𝐻𝐴) = (𝑟𝐻𝐴))
2221eqeq2d 2769 . . . . . . . . . . 11 (𝑦 = 𝑟 → (𝑢 = (𝑦𝐻𝐴) ↔ 𝑢 = (𝑟𝐻𝐴)))
2322cbvrexvw 3362 . . . . . . . . . 10 (∃𝑦𝑋 𝑢 = (𝑦𝐻𝐴) ↔ ∃𝑟𝑋 𝑢 = (𝑟𝐻𝐴))
2420, 23bitrdi 290 . . . . . . . . 9 (𝑥 = 𝑢 → (∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴) ↔ ∃𝑟𝑋 𝑢 = (𝑟𝐻𝐴)))
2524elrab 3602 . . . . . . . 8 (𝑢 ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ↔ (𝑢𝑋 ∧ ∃𝑟𝑋 𝑢 = (𝑟𝐻𝐴)))
26 eqeq1 2762 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑣 → (𝑥 = (𝑦𝐻𝐴) ↔ 𝑣 = (𝑦𝐻𝐴)))
2726rexbidv 3221 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑣 → (∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴) ↔ ∃𝑦𝑋 𝑣 = (𝑦𝐻𝐴)))
28 oveq1 7157 . . . . . . . . . . . . . . . . . 18 (𝑦 = 𝑠 → (𝑦𝐻𝐴) = (𝑠𝐻𝐴))
2928eqeq2d 2769 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑠 → (𝑣 = (𝑦𝐻𝐴) ↔ 𝑣 = (𝑠𝐻𝐴)))
3029cbvrexvw 3362 . . . . . . . . . . . . . . . 16 (∃𝑦𝑋 𝑣 = (𝑦𝐻𝐴) ↔ ∃𝑠𝑋 𝑣 = (𝑠𝐻𝐴))
3127, 30bitrdi 290 . . . . . . . . . . . . . . 15 (𝑥 = 𝑣 → (∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴) ↔ ∃𝑠𝑋 𝑣 = (𝑠𝐻𝐴)))
3231elrab 3602 . . . . . . . . . . . . . 14 (𝑣 ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ↔ (𝑣𝑋 ∧ ∃𝑠𝑋 𝑣 = (𝑠𝐻𝐴)))
334, 9, 5rngodir 35623 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑅 ∈ RingOps ∧ (𝑟𝑋𝑠𝑋𝐴𝑋)) → ((𝑟𝐺𝑠)𝐻𝐴) = ((𝑟𝐻𝐴)𝐺(𝑠𝐻𝐴)))
34333exp2 1351 . . . . . . . . . . . . . . . . . . . . 21 (𝑅 ∈ RingOps → (𝑟𝑋 → (𝑠𝑋 → (𝐴𝑋 → ((𝑟𝐺𝑠)𝐻𝐴) = ((𝑟𝐻𝐴)𝐺(𝑠𝐻𝐴))))))
3534imp42 430 . . . . . . . . . . . . . . . . . . . 20 (((𝑅 ∈ RingOps ∧ (𝑟𝑋𝑠𝑋)) ∧ 𝐴𝑋) → ((𝑟𝐺𝑠)𝐻𝐴) = ((𝑟𝐻𝐴)𝐺(𝑠𝐻𝐴)))
364, 5rngogcl 35630 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑅 ∈ RingOps ∧ 𝑟𝑋𝑠𝑋) → (𝑟𝐺𝑠) ∈ 𝑋)
37363expib 1119 . . . . . . . . . . . . . . . . . . . . . 22 (𝑅 ∈ RingOps → ((𝑟𝑋𝑠𝑋) → (𝑟𝐺𝑠) ∈ 𝑋))
3837imdistani 572 . . . . . . . . . . . . . . . . . . . . 21 ((𝑅 ∈ RingOps ∧ (𝑟𝑋𝑠𝑋)) → (𝑅 ∈ RingOps ∧ (𝑟𝐺𝑠) ∈ 𝑋))
394, 9, 5rngocl 35619 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑅 ∈ RingOps ∧ (𝑟𝐺𝑠) ∈ 𝑋𝐴𝑋) → ((𝑟𝐺𝑠)𝐻𝐴) ∈ 𝑋)
40393expa 1115 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑅 ∈ RingOps ∧ (𝑟𝐺𝑠) ∈ 𝑋) ∧ 𝐴𝑋) → ((𝑟𝐺𝑠)𝐻𝐴) ∈ 𝑋)
41 eqid 2758 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑟𝐺𝑠)𝐻𝐴) = ((𝑟𝐺𝑠)𝐻𝐴)
42 oveq1 7157 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 = (𝑟𝐺𝑠) → (𝑦𝐻𝐴) = ((𝑟𝐺𝑠)𝐻𝐴))
4342rspceeqv 3556 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑟𝐺𝑠) ∈ 𝑋 ∧ ((𝑟𝐺𝑠)𝐻𝐴) = ((𝑟𝐺𝑠)𝐻𝐴)) → ∃𝑦𝑋 ((𝑟𝐺𝑠)𝐻𝐴) = (𝑦𝐻𝐴))
4441, 43mpan2 690 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑟𝐺𝑠) ∈ 𝑋 → ∃𝑦𝑋 ((𝑟𝐺𝑠)𝐻𝐴) = (𝑦𝐻𝐴))
4544ad2antlr 726 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑅 ∈ RingOps ∧ (𝑟𝐺𝑠) ∈ 𝑋) ∧ 𝐴𝑋) → ∃𝑦𝑋 ((𝑟𝐺𝑠)𝐻𝐴) = (𝑦𝐻𝐴))
46 eqeq1 2762 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = ((𝑟𝐺𝑠)𝐻𝐴) → (𝑥 = (𝑦𝐻𝐴) ↔ ((𝑟𝐺𝑠)𝐻𝐴) = (𝑦𝐻𝐴)))
4746rexbidv 3221 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = ((𝑟𝐺𝑠)𝐻𝐴) → (∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴) ↔ ∃𝑦𝑋 ((𝑟𝐺𝑠)𝐻𝐴) = (𝑦𝐻𝐴)))
4847elrab 3602 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑟𝐺𝑠)𝐻𝐴) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ↔ (((𝑟𝐺𝑠)𝐻𝐴) ∈ 𝑋 ∧ ∃𝑦𝑋 ((𝑟𝐺𝑠)𝐻𝐴) = (𝑦𝐻𝐴)))
4940, 45, 48sylanbrc 586 . . . . . . . . . . . . . . . . . . . . 21 (((𝑅 ∈ RingOps ∧ (𝑟𝐺𝑠) ∈ 𝑋) ∧ 𝐴𝑋) → ((𝑟𝐺𝑠)𝐻𝐴) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)})
5038, 49sylan 583 . . . . . . . . . . . . . . . . . . . 20 (((𝑅 ∈ RingOps ∧ (𝑟𝑋𝑠𝑋)) ∧ 𝐴𝑋) → ((𝑟𝐺𝑠)𝐻𝐴) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)})
5135, 50eqeltrrd 2853 . . . . . . . . . . . . . . . . . . 19 (((𝑅 ∈ RingOps ∧ (𝑟𝑋𝑠𝑋)) ∧ 𝐴𝑋) → ((𝑟𝐻𝐴)𝐺(𝑠𝐻𝐴)) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)})
5251an32s 651 . . . . . . . . . . . . . . . . . 18 (((𝑅 ∈ RingOps ∧ 𝐴𝑋) ∧ (𝑟𝑋𝑠𝑋)) → ((𝑟𝐻𝐴)𝐺(𝑠𝐻𝐴)) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)})
5352anassrs 471 . . . . . . . . . . . . . . . . 17 ((((𝑅 ∈ RingOps ∧ 𝐴𝑋) ∧ 𝑟𝑋) ∧ 𝑠𝑋) → ((𝑟𝐻𝐴)𝐺(𝑠𝐻𝐴)) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)})
54 oveq2 7158 . . . . . . . . . . . . . . . . . 18 (𝑣 = (𝑠𝐻𝐴) → ((𝑟𝐻𝐴)𝐺𝑣) = ((𝑟𝐻𝐴)𝐺(𝑠𝐻𝐴)))
5554eleq1d 2836 . . . . . . . . . . . . . . . . 17 (𝑣 = (𝑠𝐻𝐴) → (((𝑟𝐻𝐴)𝐺𝑣) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ↔ ((𝑟𝐻𝐴)𝐺(𝑠𝐻𝐴)) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)}))
5653, 55syl5ibrcom 250 . . . . . . . . . . . . . . . 16 ((((𝑅 ∈ RingOps ∧ 𝐴𝑋) ∧ 𝑟𝑋) ∧ 𝑠𝑋) → (𝑣 = (𝑠𝐻𝐴) → ((𝑟𝐻𝐴)𝐺𝑣) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)}))
5756rexlimdva 3208 . . . . . . . . . . . . . . 15 (((𝑅 ∈ RingOps ∧ 𝐴𝑋) ∧ 𝑟𝑋) → (∃𝑠𝑋 𝑣 = (𝑠𝐻𝐴) → ((𝑟𝐻𝐴)𝐺𝑣) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)}))
5857adantld 494 . . . . . . . . . . . . . 14 (((𝑅 ∈ RingOps ∧ 𝐴𝑋) ∧ 𝑟𝑋) → ((𝑣𝑋 ∧ ∃𝑠𝑋 𝑣 = (𝑠𝐻𝐴)) → ((𝑟𝐻𝐴)𝐺𝑣) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)}))
5932, 58syl5bi 245 . . . . . . . . . . . . 13 (((𝑅 ∈ RingOps ∧ 𝐴𝑋) ∧ 𝑟𝑋) → (𝑣 ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} → ((𝑟𝐻𝐴)𝐺𝑣) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)}))
6059ralrimiv 3112 . . . . . . . . . . . 12 (((𝑅 ∈ RingOps ∧ 𝐴𝑋) ∧ 𝑟𝑋) → ∀𝑣 ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ((𝑟𝐻𝐴)𝐺𝑣) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)})
614, 9, 5rngoass 35624 . . . . . . . . . . . . . . . . . 18 ((𝑅 ∈ RingOps ∧ (𝑤𝑋𝑟𝑋𝐴𝑋)) → ((𝑤𝐻𝑟)𝐻𝐴) = (𝑤𝐻(𝑟𝐻𝐴)))
62613exp2 1351 . . . . . . . . . . . . . . . . 17 (𝑅 ∈ RingOps → (𝑤𝑋 → (𝑟𝑋 → (𝐴𝑋 → ((𝑤𝐻𝑟)𝐻𝐴) = (𝑤𝐻(𝑟𝐻𝐴))))))
6362imp42 430 . . . . . . . . . . . . . . . 16 (((𝑅 ∈ RingOps ∧ (𝑤𝑋𝑟𝑋)) ∧ 𝐴𝑋) → ((𝑤𝐻𝑟)𝐻𝐴) = (𝑤𝐻(𝑟𝐻𝐴)))
6463an32s 651 . . . . . . . . . . . . . . 15 (((𝑅 ∈ RingOps ∧ 𝐴𝑋) ∧ (𝑤𝑋𝑟𝑋)) → ((𝑤𝐻𝑟)𝐻𝐴) = (𝑤𝐻(𝑟𝐻𝐴)))
654, 9, 5rngocl 35619 . . . . . . . . . . . . . . . . . . 19 ((𝑅 ∈ RingOps ∧ 𝑤𝑋𝑟𝑋) → (𝑤𝐻𝑟) ∈ 𝑋)
66653expib 1119 . . . . . . . . . . . . . . . . . 18 (𝑅 ∈ RingOps → ((𝑤𝑋𝑟𝑋) → (𝑤𝐻𝑟) ∈ 𝑋))
6766imdistani 572 . . . . . . . . . . . . . . . . 17 ((𝑅 ∈ RingOps ∧ (𝑤𝑋𝑟𝑋)) → (𝑅 ∈ RingOps ∧ (𝑤𝐻𝑟) ∈ 𝑋))
684, 9, 5rngocl 35619 . . . . . . . . . . . . . . . . . . 19 ((𝑅 ∈ RingOps ∧ (𝑤𝐻𝑟) ∈ 𝑋𝐴𝑋) → ((𝑤𝐻𝑟)𝐻𝐴) ∈ 𝑋)
69683expa 1115 . . . . . . . . . . . . . . . . . 18 (((𝑅 ∈ RingOps ∧ (𝑤𝐻𝑟) ∈ 𝑋) ∧ 𝐴𝑋) → ((𝑤𝐻𝑟)𝐻𝐴) ∈ 𝑋)
70 eqid 2758 . . . . . . . . . . . . . . . . . . . 20 ((𝑤𝐻𝑟)𝐻𝐴) = ((𝑤𝐻𝑟)𝐻𝐴)
71 oveq1 7157 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 = (𝑤𝐻𝑟) → (𝑦𝐻𝐴) = ((𝑤𝐻𝑟)𝐻𝐴))
7271rspceeqv 3556 . . . . . . . . . . . . . . . . . . . 20 (((𝑤𝐻𝑟) ∈ 𝑋 ∧ ((𝑤𝐻𝑟)𝐻𝐴) = ((𝑤𝐻𝑟)𝐻𝐴)) → ∃𝑦𝑋 ((𝑤𝐻𝑟)𝐻𝐴) = (𝑦𝐻𝐴))
7370, 72mpan2 690 . . . . . . . . . . . . . . . . . . 19 ((𝑤𝐻𝑟) ∈ 𝑋 → ∃𝑦𝑋 ((𝑤𝐻𝑟)𝐻𝐴) = (𝑦𝐻𝐴))
7473ad2antlr 726 . . . . . . . . . . . . . . . . . 18 (((𝑅 ∈ RingOps ∧ (𝑤𝐻𝑟) ∈ 𝑋) ∧ 𝐴𝑋) → ∃𝑦𝑋 ((𝑤𝐻𝑟)𝐻𝐴) = (𝑦𝐻𝐴))
75 eqeq1 2762 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = ((𝑤𝐻𝑟)𝐻𝐴) → (𝑥 = (𝑦𝐻𝐴) ↔ ((𝑤𝐻𝑟)𝐻𝐴) = (𝑦𝐻𝐴)))
7675rexbidv 3221 . . . . . . . . . . . . . . . . . . 19 (𝑥 = ((𝑤𝐻𝑟)𝐻𝐴) → (∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴) ↔ ∃𝑦𝑋 ((𝑤𝐻𝑟)𝐻𝐴) = (𝑦𝐻𝐴)))
7776elrab 3602 . . . . . . . . . . . . . . . . . 18 (((𝑤𝐻𝑟)𝐻𝐴) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ↔ (((𝑤𝐻𝑟)𝐻𝐴) ∈ 𝑋 ∧ ∃𝑦𝑋 ((𝑤𝐻𝑟)𝐻𝐴) = (𝑦𝐻𝐴)))
7869, 74, 77sylanbrc 586 . . . . . . . . . . . . . . . . 17 (((𝑅 ∈ RingOps ∧ (𝑤𝐻𝑟) ∈ 𝑋) ∧ 𝐴𝑋) → ((𝑤𝐻𝑟)𝐻𝐴) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)})
7967, 78sylan 583 . . . . . . . . . . . . . . . 16 (((𝑅 ∈ RingOps ∧ (𝑤𝑋𝑟𝑋)) ∧ 𝐴𝑋) → ((𝑤𝐻𝑟)𝐻𝐴) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)})
8079an32s 651 . . . . . . . . . . . . . . 15 (((𝑅 ∈ RingOps ∧ 𝐴𝑋) ∧ (𝑤𝑋𝑟𝑋)) → ((𝑤𝐻𝑟)𝐻𝐴) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)})
8164, 80eqeltrrd 2853 . . . . . . . . . . . . . 14 (((𝑅 ∈ RingOps ∧ 𝐴𝑋) ∧ (𝑤𝑋𝑟𝑋)) → (𝑤𝐻(𝑟𝐻𝐴)) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)})
8281anass1rs 654 . . . . . . . . . . . . 13 ((((𝑅 ∈ RingOps ∧ 𝐴𝑋) ∧ 𝑟𝑋) ∧ 𝑤𝑋) → (𝑤𝐻(𝑟𝐻𝐴)) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)})
8382ralrimiva 3113 . . . . . . . . . . . 12 (((𝑅 ∈ RingOps ∧ 𝐴𝑋) ∧ 𝑟𝑋) → ∀𝑤𝑋 (𝑤𝐻(𝑟𝐻𝐴)) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)})
8460, 83jca 515 . . . . . . . . . . 11 (((𝑅 ∈ RingOps ∧ 𝐴𝑋) ∧ 𝑟𝑋) → (∀𝑣 ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ((𝑟𝐻𝐴)𝐺𝑣) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑤𝑋 (𝑤𝐻(𝑟𝐻𝐴)) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)}))
85 oveq1 7157 . . . . . . . . . . . . . 14 (𝑢 = (𝑟𝐻𝐴) → (𝑢𝐺𝑣) = ((𝑟𝐻𝐴)𝐺𝑣))
8685eleq1d 2836 . . . . . . . . . . . . 13 (𝑢 = (𝑟𝐻𝐴) → ((𝑢𝐺𝑣) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ↔ ((𝑟𝐻𝐴)𝐺𝑣) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)}))
8786ralbidv 3126 . . . . . . . . . . . 12 (𝑢 = (𝑟𝐻𝐴) → (∀𝑣 ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} (𝑢𝐺𝑣) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ↔ ∀𝑣 ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ((𝑟𝐻𝐴)𝐺𝑣) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)}))
88 oveq2 7158 . . . . . . . . . . . . . 14 (𝑢 = (𝑟𝐻𝐴) → (𝑤𝐻𝑢) = (𝑤𝐻(𝑟𝐻𝐴)))
8988eleq1d 2836 . . . . . . . . . . . . 13 (𝑢 = (𝑟𝐻𝐴) → ((𝑤𝐻𝑢) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ↔ (𝑤𝐻(𝑟𝐻𝐴)) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)}))
9089ralbidv 3126 . . . . . . . . . . . 12 (𝑢 = (𝑟𝐻𝐴) → (∀𝑤𝑋 (𝑤𝐻𝑢) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ↔ ∀𝑤𝑋 (𝑤𝐻(𝑟𝐻𝐴)) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)}))
9187, 90anbi12d 633 . . . . . . . . . . 11 (𝑢 = (𝑟𝐻𝐴) → ((∀𝑣 ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} (𝑢𝐺𝑣) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑤𝑋 (𝑤𝐻𝑢) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)}) ↔ (∀𝑣 ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ((𝑟𝐻𝐴)𝐺𝑣) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑤𝑋 (𝑤𝐻(𝑟𝐻𝐴)) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)})))
9284, 91syl5ibrcom 250 . . . . . . . . . 10 (((𝑅 ∈ RingOps ∧ 𝐴𝑋) ∧ 𝑟𝑋) → (𝑢 = (𝑟𝐻𝐴) → (∀𝑣 ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} (𝑢𝐺𝑣) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑤𝑋 (𝑤𝐻𝑢) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)})))
9392rexlimdva 3208 . . . . . . . . 9 ((𝑅 ∈ RingOps ∧ 𝐴𝑋) → (∃𝑟𝑋 𝑢 = (𝑟𝐻𝐴) → (∀𝑣 ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} (𝑢𝐺𝑣) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑤𝑋 (𝑤𝐻𝑢) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)})))
9493adantld 494 . . . . . . . 8 ((𝑅 ∈ RingOps ∧ 𝐴𝑋) → ((𝑢𝑋 ∧ ∃𝑟𝑋 𝑢 = (𝑟𝐻𝐴)) → (∀𝑣 ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} (𝑢𝐺𝑣) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑤𝑋 (𝑤𝐻𝑢) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)})))
9525, 94syl5bi 245 . . . . . . 7 ((𝑅 ∈ RingOps ∧ 𝐴𝑋) → (𝑢 ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} → (∀𝑣 ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} (𝑢𝐺𝑣) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑤𝑋 (𝑤𝐻𝑢) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)})))
9695ralrimiv 3112 . . . . . 6 ((𝑅 ∈ RingOps ∧ 𝐴𝑋) → ∀𝑢 ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} (∀𝑣 ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} (𝑢𝐺𝑣) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑤𝑋 (𝑤𝐻𝑢) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)}))
973, 18, 963jca 1125 . . . . 5 ((𝑅 ∈ RingOps ∧ 𝐴𝑋) → ({𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑋 ∧ (GId‘𝐺) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑢 ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} (∀𝑣 ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} (𝑢𝐺𝑣) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑤𝑋 (𝑤𝐻𝑢) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)})))
981, 97sylan 583 . . . 4 ((𝑅 ∈ CRingOps ∧ 𝐴𝑋) → ({𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑋 ∧ (GId‘𝐺) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑢 ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} (∀𝑣 ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} (𝑢𝐺𝑣) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑤𝑋 (𝑤𝐻𝑢) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)})))
994, 9, 5, 6isidlc 35733 . . . . 5 (𝑅 ∈ CRingOps → ({𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ∈ (Idl‘𝑅) ↔ ({𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑋 ∧ (GId‘𝐺) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑢 ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} (∀𝑣 ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} (𝑢𝐺𝑣) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑤𝑋 (𝑤𝐻𝑢) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)}))))
10099adantr 484 . . . 4 ((𝑅 ∈ CRingOps ∧ 𝐴𝑋) → ({𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ∈ (Idl‘𝑅) ↔ ({𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑋 ∧ (GId‘𝐺) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑢 ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} (∀𝑣 ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} (𝑢𝐺𝑣) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑤𝑋 (𝑤𝐻𝑢) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)}))))
10198, 100mpbird 260 . . 3 ((𝑅 ∈ CRingOps ∧ 𝐴𝑋) → {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ∈ (Idl‘𝑅))
102 simpr 488 . . . . 5 ((𝑅 ∈ CRingOps ∧ 𝐴𝑋) → 𝐴𝑋)
1034rneqi 5778 . . . . . . . . . 10 ran 𝐺 = ran (1st𝑅)
1045, 103eqtri 2781 . . . . . . . . 9 𝑋 = ran (1st𝑅)
105 eqid 2758 . . . . . . . . 9 (GId‘𝐻) = (GId‘𝐻)
106104, 9, 105rngo1cl 35657 . . . . . . . 8 (𝑅 ∈ RingOps → (GId‘𝐻) ∈ 𝑋)
107106adantr 484 . . . . . . 7 ((𝑅 ∈ RingOps ∧ 𝐴𝑋) → (GId‘𝐻) ∈ 𝑋)
1089, 104, 105rngolidm 35655 . . . . . . . 8 ((𝑅 ∈ RingOps ∧ 𝐴𝑋) → ((GId‘𝐻)𝐻𝐴) = 𝐴)
109108eqcomd 2764 . . . . . . 7 ((𝑅 ∈ RingOps ∧ 𝐴𝑋) → 𝐴 = ((GId‘𝐻)𝐻𝐴))
110 oveq1 7157 . . . . . . . 8 (𝑦 = (GId‘𝐻) → (𝑦𝐻𝐴) = ((GId‘𝐻)𝐻𝐴))
111110rspceeqv 3556 . . . . . . 7 (((GId‘𝐻) ∈ 𝑋𝐴 = ((GId‘𝐻)𝐻𝐴)) → ∃𝑦𝑋 𝐴 = (𝑦𝐻𝐴))
112107, 109, 111syl2anc 587 . . . . . 6 ((𝑅 ∈ RingOps ∧ 𝐴𝑋) → ∃𝑦𝑋 𝐴 = (𝑦𝐻𝐴))
1131, 112sylan 583 . . . . 5 ((𝑅 ∈ CRingOps ∧ 𝐴𝑋) → ∃𝑦𝑋 𝐴 = (𝑦𝐻𝐴))
114 eqeq1 2762 . . . . . . 7 (𝑥 = 𝐴 → (𝑥 = (𝑦𝐻𝐴) ↔ 𝐴 = (𝑦𝐻𝐴)))
115114rexbidv 3221 . . . . . 6 (𝑥 = 𝐴 → (∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴) ↔ ∃𝑦𝑋 𝐴 = (𝑦𝐻𝐴)))
116115elrab 3602 . . . . 5 (𝐴 ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ↔ (𝐴𝑋 ∧ ∃𝑦𝑋 𝐴 = (𝑦𝐻𝐴)))
117102, 113, 116sylanbrc 586 . . . 4 ((𝑅 ∈ CRingOps ∧ 𝐴𝑋) → 𝐴 ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)})
118117snssd 4699 . . 3 ((𝑅 ∈ CRingOps ∧ 𝐴𝑋) → {𝐴} ⊆ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)})
119 snssg 4675 . . . . . . . . 9 (𝐴𝑋 → (𝐴𝑗 ↔ {𝐴} ⊆ 𝑗))
120119biimpar 481 . . . . . . . 8 ((𝐴𝑋 ∧ {𝐴} ⊆ 𝑗) → 𝐴𝑗)
1214, 9, 5idllmulcl 35738 . . . . . . . . . . . . . . 15 (((𝑅 ∈ RingOps ∧ 𝑗 ∈ (Idl‘𝑅)) ∧ (𝐴𝑗𝑦𝑋)) → (𝑦𝐻𝐴) ∈ 𝑗)
122121anassrs 471 . . . . . . . . . . . . . 14 ((((𝑅 ∈ RingOps ∧ 𝑗 ∈ (Idl‘𝑅)) ∧ 𝐴𝑗) ∧ 𝑦𝑋) → (𝑦𝐻𝐴) ∈ 𝑗)
123 eleq1 2839 . . . . . . . . . . . . . 14 (𝑥 = (𝑦𝐻𝐴) → (𝑥𝑗 ↔ (𝑦𝐻𝐴) ∈ 𝑗))
124122, 123syl5ibrcom 250 . . . . . . . . . . . . 13 ((((𝑅 ∈ RingOps ∧ 𝑗 ∈ (Idl‘𝑅)) ∧ 𝐴𝑗) ∧ 𝑦𝑋) → (𝑥 = (𝑦𝐻𝐴) → 𝑥𝑗))
125124rexlimdva 3208 . . . . . . . . . . . 12 (((𝑅 ∈ RingOps ∧ 𝑗 ∈ (Idl‘𝑅)) ∧ 𝐴𝑗) → (∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴) → 𝑥𝑗))
126125adantr 484 . . . . . . . . . . 11 ((((𝑅 ∈ RingOps ∧ 𝑗 ∈ (Idl‘𝑅)) ∧ 𝐴𝑗) ∧ 𝑥𝑋) → (∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴) → 𝑥𝑗))
127126ralrimiva 3113 . . . . . . . . . 10 (((𝑅 ∈ RingOps ∧ 𝑗 ∈ (Idl‘𝑅)) ∧ 𝐴𝑗) → ∀𝑥𝑋 (∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴) → 𝑥𝑗))
128 rabss 3976 . . . . . . . . . 10 ({𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑗 ↔ ∀𝑥𝑋 (∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴) → 𝑥𝑗))
129127, 128sylibr 237 . . . . . . . . 9 (((𝑅 ∈ RingOps ∧ 𝑗 ∈ (Idl‘𝑅)) ∧ 𝐴𝑗) → {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑗)
130129ex 416 . . . . . . . 8 ((𝑅 ∈ RingOps ∧ 𝑗 ∈ (Idl‘𝑅)) → (𝐴𝑗 → {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑗))
131120, 130syl5 34 . . . . . . 7 ((𝑅 ∈ RingOps ∧ 𝑗 ∈ (Idl‘𝑅)) → ((𝐴𝑋 ∧ {𝐴} ⊆ 𝑗) → {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑗))
132131expdimp 456 . . . . . 6 (((𝑅 ∈ RingOps ∧ 𝑗 ∈ (Idl‘𝑅)) ∧ 𝐴𝑋) → ({𝐴} ⊆ 𝑗 → {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑗))
133132an32s 651 . . . . 5 (((𝑅 ∈ RingOps ∧ 𝐴𝑋) ∧ 𝑗 ∈ (Idl‘𝑅)) → ({𝐴} ⊆ 𝑗 → {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑗))
134133ralrimiva 3113 . . . 4 ((𝑅 ∈ RingOps ∧ 𝐴𝑋) → ∀𝑗 ∈ (Idl‘𝑅)({𝐴} ⊆ 𝑗 → {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑗))
1351, 134sylan 583 . . 3 ((𝑅 ∈ CRingOps ∧ 𝐴𝑋) → ∀𝑗 ∈ (Idl‘𝑅)({𝐴} ⊆ 𝑗 → {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑗))
136101, 118, 1353jca 1125 . 2 ((𝑅 ∈ CRingOps ∧ 𝐴𝑋) → ({𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ∈ (Idl‘𝑅) ∧ {𝐴} ⊆ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑗 ∈ (Idl‘𝑅)({𝐴} ⊆ 𝑗 → {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑗)))
137 snssi 4698 . . 3 (𝐴𝑋 → {𝐴} ⊆ 𝑋)
1384, 5igenval2 35784 . . 3 ((𝑅 ∈ RingOps ∧ {𝐴} ⊆ 𝑋) → ((𝑅 IdlGen {𝐴}) = {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ↔ ({𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ∈ (Idl‘𝑅) ∧ {𝐴} ⊆ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑗 ∈ (Idl‘𝑅)({𝐴} ⊆ 𝑗 → {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑗))))
1391, 137, 138syl2an 598 . 2 ((𝑅 ∈ CRingOps ∧ 𝐴𝑋) → ((𝑅 IdlGen {𝐴}) = {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ↔ ({𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ∈ (Idl‘𝑅) ∧ {𝐴} ⊆ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑗 ∈ (Idl‘𝑅)({𝐴} ⊆ 𝑗 → {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑗))))
140136, 139mpbird 260 1 ((𝑅 ∈ CRingOps ∧ 𝐴𝑋) → (𝑅 IdlGen {𝐴}) = {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)})
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   ∧ w3a 1084   = wceq 1538   ∈ wcel 2111  ∀wral 3070  ∃wrex 3071  {crab 3074   ⊆ wss 3858  {csn 4522  ran crn 5525  ‘cfv 6335  (class class class)co 7150  1st c1st 7691  2nd c2nd 7692  GIdcgi 28372  RingOpscrngo 35612  CRingOpsccring 35711  Idlcidl 35725   IdlGen cigen 35777 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729  ax-rep 5156  ax-sep 5169  ax-nul 5176  ax-pow 5234  ax-pr 5298  ax-un 7459 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2557  df-eu 2588  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ne 2952  df-ral 3075  df-rex 3076  df-reu 3077  df-rmo 3078  df-rab 3079  df-v 3411  df-sbc 3697  df-csb 3806  df-dif 3861  df-un 3863  df-in 3865  df-ss 3875  df-nul 4226  df-if 4421  df-pw 4496  df-sn 4523  df-pr 4525  df-op 4529  df-uni 4799  df-int 4839  df-iun 4885  df-br 5033  df-opab 5095  df-mpt 5113  df-id 5430  df-xp 5530  df-rel 5531  df-cnv 5532  df-co 5533  df-dm 5534  df-rn 5535  df-res 5536  df-ima 5537  df-iota 6294  df-fun 6337  df-fn 6338  df-f 6339  df-f1 6340  df-fo 6341  df-f1o 6342  df-fv 6343  df-riota 7108  df-ov 7153  df-oprab 7154  df-mpo 7155  df-1st 7693  df-2nd 7694  df-grpo 28375  df-gid 28376  df-ginv 28377  df-ablo 28427  df-ass 35561  df-exid 35563  df-mgmOLD 35567  df-sgrOLD 35579  df-mndo 35585  df-rngo 35613  df-com2 35708  df-crngo 35712  df-idl 35728  df-igen 35778 This theorem is referenced by:  isfldidl  35786  ispridlc  35788
 Copyright terms: Public domain W3C validator