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 35214
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 35147 . . . . 5 (𝑅 ∈ CRingOps → 𝑅 ∈ RingOps)
2 ssrab2 4059 . . . . . . 7 {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑋
32a1i 11 . . . . . 6 ((𝑅 ∈ RingOps ∧ 𝐴𝑋) → {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑋)
4 prnc.1 . . . . . . . . 9 𝐺 = (1st𝑅)
5 prnc.3 . . . . . . . . 9 𝑋 = ran 𝐺
6 eqid 2824 . . . . . . . . 9 (GId‘𝐺) = (GId‘𝐺)
74, 5, 6rngo0cl 35066 . . . . . . . 8 (𝑅 ∈ RingOps → (GId‘𝐺) ∈ 𝑋)
87adantr 481 . . . . . . 7 ((𝑅 ∈ RingOps ∧ 𝐴𝑋) → (GId‘𝐺) ∈ 𝑋)
9 prnc.2 . . . . . . . . . 10 𝐻 = (2nd𝑅)
106, 5, 4, 9rngolz 35069 . . . . . . . . 9 ((𝑅 ∈ RingOps ∧ 𝐴𝑋) → ((GId‘𝐺)𝐻𝐴) = (GId‘𝐺))
1110eqcomd 2830 . . . . . . . 8 ((𝑅 ∈ RingOps ∧ 𝐴𝑋) → (GId‘𝐺) = ((GId‘𝐺)𝐻𝐴))
12 oveq1 7158 . . . . . . . . 9 (𝑦 = (GId‘𝐺) → (𝑦𝐻𝐴) = ((GId‘𝐺)𝐻𝐴))
1312rspceeqv 3641 . . . . . . . 8 (((GId‘𝐺) ∈ 𝑋 ∧ (GId‘𝐺) = ((GId‘𝐺)𝐻𝐴)) → ∃𝑦𝑋 (GId‘𝐺) = (𝑦𝐻𝐴))
148, 11, 13syl2anc 584 . . . . . . 7 ((𝑅 ∈ RingOps ∧ 𝐴𝑋) → ∃𝑦𝑋 (GId‘𝐺) = (𝑦𝐻𝐴))
15 eqeq1 2828 . . . . . . . . 9 (𝑥 = (GId‘𝐺) → (𝑥 = (𝑦𝐻𝐴) ↔ (GId‘𝐺) = (𝑦𝐻𝐴)))
1615rexbidv 3301 . . . . . . . 8 (𝑥 = (GId‘𝐺) → (∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴) ↔ ∃𝑦𝑋 (GId‘𝐺) = (𝑦𝐻𝐴)))
1716elrab 3683 . . . . . . 7 ((GId‘𝐺) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ↔ ((GId‘𝐺) ∈ 𝑋 ∧ ∃𝑦𝑋 (GId‘𝐺) = (𝑦𝐻𝐴)))
188, 14, 17sylanbrc 583 . . . . . 6 ((𝑅 ∈ RingOps ∧ 𝐴𝑋) → (GId‘𝐺) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)})
19 eqeq1 2828 . . . . . . . . . . 11 (𝑥 = 𝑢 → (𝑥 = (𝑦𝐻𝐴) ↔ 𝑢 = (𝑦𝐻𝐴)))
2019rexbidv 3301 . . . . . . . . . 10 (𝑥 = 𝑢 → (∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴) ↔ ∃𝑦𝑋 𝑢 = (𝑦𝐻𝐴)))
21 oveq1 7158 . . . . . . . . . . . 12 (𝑦 = 𝑟 → (𝑦𝐻𝐴) = (𝑟𝐻𝐴))
2221eqeq2d 2835 . . . . . . . . . . 11 (𝑦 = 𝑟 → (𝑢 = (𝑦𝐻𝐴) ↔ 𝑢 = (𝑟𝐻𝐴)))
2322cbvrexv 3458 . . . . . . . . . 10 (∃𝑦𝑋 𝑢 = (𝑦𝐻𝐴) ↔ ∃𝑟𝑋 𝑢 = (𝑟𝐻𝐴))
2420, 23syl6bb 288 . . . . . . . . 9 (𝑥 = 𝑢 → (∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴) ↔ ∃𝑟𝑋 𝑢 = (𝑟𝐻𝐴)))
2524elrab 3683 . . . . . . . 8 (𝑢 ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ↔ (𝑢𝑋 ∧ ∃𝑟𝑋 𝑢 = (𝑟𝐻𝐴)))
26 eqeq1 2828 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑣 → (𝑥 = (𝑦𝐻𝐴) ↔ 𝑣 = (𝑦𝐻𝐴)))
2726rexbidv 3301 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑣 → (∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴) ↔ ∃𝑦𝑋 𝑣 = (𝑦𝐻𝐴)))
28 oveq1 7158 . . . . . . . . . . . . . . . . . 18 (𝑦 = 𝑠 → (𝑦𝐻𝐴) = (𝑠𝐻𝐴))
2928eqeq2d 2835 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑠 → (𝑣 = (𝑦𝐻𝐴) ↔ 𝑣 = (𝑠𝐻𝐴)))
3029cbvrexv 3458 . . . . . . . . . . . . . . . 16 (∃𝑦𝑋 𝑣 = (𝑦𝐻𝐴) ↔ ∃𝑠𝑋 𝑣 = (𝑠𝐻𝐴))
3127, 30syl6bb 288 . . . . . . . . . . . . . . 15 (𝑥 = 𝑣 → (∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴) ↔ ∃𝑠𝑋 𝑣 = (𝑠𝐻𝐴)))
3231elrab 3683 . . . . . . . . . . . . . 14 (𝑣 ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ↔ (𝑣𝑋 ∧ ∃𝑠𝑋 𝑣 = (𝑠𝐻𝐴)))
334, 9, 5rngodir 35052 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑅 ∈ RingOps ∧ (𝑟𝑋𝑠𝑋𝐴𝑋)) → ((𝑟𝐺𝑠)𝐻𝐴) = ((𝑟𝐻𝐴)𝐺(𝑠𝐻𝐴)))
34333exp2 1348 . . . . . . . . . . . . . . . . . . . . 21 (𝑅 ∈ RingOps → (𝑟𝑋 → (𝑠𝑋 → (𝐴𝑋 → ((𝑟𝐺𝑠)𝐻𝐴) = ((𝑟𝐻𝐴)𝐺(𝑠𝐻𝐴))))))
3534imp42 427 . . . . . . . . . . . . . . . . . . . 20 (((𝑅 ∈ RingOps ∧ (𝑟𝑋𝑠𝑋)) ∧ 𝐴𝑋) → ((𝑟𝐺𝑠)𝐻𝐴) = ((𝑟𝐻𝐴)𝐺(𝑠𝐻𝐴)))
364, 5rngogcl 35059 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑅 ∈ RingOps ∧ 𝑟𝑋𝑠𝑋) → (𝑟𝐺𝑠) ∈ 𝑋)
37363expib 1116 . . . . . . . . . . . . . . . . . . . . . 22 (𝑅 ∈ RingOps → ((𝑟𝑋𝑠𝑋) → (𝑟𝐺𝑠) ∈ 𝑋))
3837imdistani 569 . . . . . . . . . . . . . . . . . . . . 21 ((𝑅 ∈ RingOps ∧ (𝑟𝑋𝑠𝑋)) → (𝑅 ∈ RingOps ∧ (𝑟𝐺𝑠) ∈ 𝑋))
394, 9, 5rngocl 35048 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑅 ∈ RingOps ∧ (𝑟𝐺𝑠) ∈ 𝑋𝐴𝑋) → ((𝑟𝐺𝑠)𝐻𝐴) ∈ 𝑋)
40393expa 1112 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑅 ∈ RingOps ∧ (𝑟𝐺𝑠) ∈ 𝑋) ∧ 𝐴𝑋) → ((𝑟𝐺𝑠)𝐻𝐴) ∈ 𝑋)
41 eqid 2824 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑟𝐺𝑠)𝐻𝐴) = ((𝑟𝐺𝑠)𝐻𝐴)
42 oveq1 7158 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 = (𝑟𝐺𝑠) → (𝑦𝐻𝐴) = ((𝑟𝐺𝑠)𝐻𝐴))
4342rspceeqv 3641 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑟𝐺𝑠) ∈ 𝑋 ∧ ((𝑟𝐺𝑠)𝐻𝐴) = ((𝑟𝐺𝑠)𝐻𝐴)) → ∃𝑦𝑋 ((𝑟𝐺𝑠)𝐻𝐴) = (𝑦𝐻𝐴))
4441, 43mpan2 687 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑟𝐺𝑠) ∈ 𝑋 → ∃𝑦𝑋 ((𝑟𝐺𝑠)𝐻𝐴) = (𝑦𝐻𝐴))
4544ad2antlr 723 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑅 ∈ RingOps ∧ (𝑟𝐺𝑠) ∈ 𝑋) ∧ 𝐴𝑋) → ∃𝑦𝑋 ((𝑟𝐺𝑠)𝐻𝐴) = (𝑦𝐻𝐴))
46 eqeq1 2828 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = ((𝑟𝐺𝑠)𝐻𝐴) → (𝑥 = (𝑦𝐻𝐴) ↔ ((𝑟𝐺𝑠)𝐻𝐴) = (𝑦𝐻𝐴)))
4746rexbidv 3301 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = ((𝑟𝐺𝑠)𝐻𝐴) → (∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴) ↔ ∃𝑦𝑋 ((𝑟𝐺𝑠)𝐻𝐴) = (𝑦𝐻𝐴)))
4847elrab 3683 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑟𝐺𝑠)𝐻𝐴) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ↔ (((𝑟𝐺𝑠)𝐻𝐴) ∈ 𝑋 ∧ ∃𝑦𝑋 ((𝑟𝐺𝑠)𝐻𝐴) = (𝑦𝐻𝐴)))
4940, 45, 48sylanbrc 583 . . . . . . . . . . . . . . . . . . . . 21 (((𝑅 ∈ RingOps ∧ (𝑟𝐺𝑠) ∈ 𝑋) ∧ 𝐴𝑋) → ((𝑟𝐺𝑠)𝐻𝐴) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)})
5038, 49sylan 580 . . . . . . . . . . . . . . . . . . . 20 (((𝑅 ∈ RingOps ∧ (𝑟𝑋𝑠𝑋)) ∧ 𝐴𝑋) → ((𝑟𝐺𝑠)𝐻𝐴) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)})
5135, 50eqeltrrd 2918 . . . . . . . . . . . . . . . . . . 19 (((𝑅 ∈ RingOps ∧ (𝑟𝑋𝑠𝑋)) ∧ 𝐴𝑋) → ((𝑟𝐻𝐴)𝐺(𝑠𝐻𝐴)) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)})
5251an32s 648 . . . . . . . . . . . . . . . . . 18 (((𝑅 ∈ RingOps ∧ 𝐴𝑋) ∧ (𝑟𝑋𝑠𝑋)) → ((𝑟𝐻𝐴)𝐺(𝑠𝐻𝐴)) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)})
5352anassrs 468 . . . . . . . . . . . . . . . . 17 ((((𝑅 ∈ RingOps ∧ 𝐴𝑋) ∧ 𝑟𝑋) ∧ 𝑠𝑋) → ((𝑟𝐻𝐴)𝐺(𝑠𝐻𝐴)) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)})
54 oveq2 7159 . . . . . . . . . . . . . . . . . 18 (𝑣 = (𝑠𝐻𝐴) → ((𝑟𝐻𝐴)𝐺𝑣) = ((𝑟𝐻𝐴)𝐺(𝑠𝐻𝐴)))
5554eleq1d 2901 . . . . . . . . . . . . . . . . 17 (𝑣 = (𝑠𝐻𝐴) → (((𝑟𝐻𝐴)𝐺𝑣) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ↔ ((𝑟𝐻𝐴)𝐺(𝑠𝐻𝐴)) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)}))
5653, 55syl5ibrcom 248 . . . . . . . . . . . . . . . 16 ((((𝑅 ∈ RingOps ∧ 𝐴𝑋) ∧ 𝑟𝑋) ∧ 𝑠𝑋) → (𝑣 = (𝑠𝐻𝐴) → ((𝑟𝐻𝐴)𝐺𝑣) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)}))
5756rexlimdva 3288 . . . . . . . . . . . . . . 15 (((𝑅 ∈ RingOps ∧ 𝐴𝑋) ∧ 𝑟𝑋) → (∃𝑠𝑋 𝑣 = (𝑠𝐻𝐴) → ((𝑟𝐻𝐴)𝐺𝑣) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)}))
5857adantld 491 . . . . . . . . . . . . . 14 (((𝑅 ∈ RingOps ∧ 𝐴𝑋) ∧ 𝑟𝑋) → ((𝑣𝑋 ∧ ∃𝑠𝑋 𝑣 = (𝑠𝐻𝐴)) → ((𝑟𝐻𝐴)𝐺𝑣) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)}))
5932, 58syl5bi 243 . . . . . . . . . . . . 13 (((𝑅 ∈ RingOps ∧ 𝐴𝑋) ∧ 𝑟𝑋) → (𝑣 ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} → ((𝑟𝐻𝐴)𝐺𝑣) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)}))
6059ralrimiv 3185 . . . . . . . . . . . 12 (((𝑅 ∈ RingOps ∧ 𝐴𝑋) ∧ 𝑟𝑋) → ∀𝑣 ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ((𝑟𝐻𝐴)𝐺𝑣) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)})
614, 9, 5rngoass 35053 . . . . . . . . . . . . . . . . . 18 ((𝑅 ∈ RingOps ∧ (𝑤𝑋𝑟𝑋𝐴𝑋)) → ((𝑤𝐻𝑟)𝐻𝐴) = (𝑤𝐻(𝑟𝐻𝐴)))
62613exp2 1348 . . . . . . . . . . . . . . . . 17 (𝑅 ∈ RingOps → (𝑤𝑋 → (𝑟𝑋 → (𝐴𝑋 → ((𝑤𝐻𝑟)𝐻𝐴) = (𝑤𝐻(𝑟𝐻𝐴))))))
6362imp42 427 . . . . . . . . . . . . . . . 16 (((𝑅 ∈ RingOps ∧ (𝑤𝑋𝑟𝑋)) ∧ 𝐴𝑋) → ((𝑤𝐻𝑟)𝐻𝐴) = (𝑤𝐻(𝑟𝐻𝐴)))
6463an32s 648 . . . . . . . . . . . . . . 15 (((𝑅 ∈ RingOps ∧ 𝐴𝑋) ∧ (𝑤𝑋𝑟𝑋)) → ((𝑤𝐻𝑟)𝐻𝐴) = (𝑤𝐻(𝑟𝐻𝐴)))
654, 9, 5rngocl 35048 . . . . . . . . . . . . . . . . . . 19 ((𝑅 ∈ RingOps ∧ 𝑤𝑋𝑟𝑋) → (𝑤𝐻𝑟) ∈ 𝑋)
66653expib 1116 . . . . . . . . . . . . . . . . . 18 (𝑅 ∈ RingOps → ((𝑤𝑋𝑟𝑋) → (𝑤𝐻𝑟) ∈ 𝑋))
6766imdistani 569 . . . . . . . . . . . . . . . . 17 ((𝑅 ∈ RingOps ∧ (𝑤𝑋𝑟𝑋)) → (𝑅 ∈ RingOps ∧ (𝑤𝐻𝑟) ∈ 𝑋))
684, 9, 5rngocl 35048 . . . . . . . . . . . . . . . . . . 19 ((𝑅 ∈ RingOps ∧ (𝑤𝐻𝑟) ∈ 𝑋𝐴𝑋) → ((𝑤𝐻𝑟)𝐻𝐴) ∈ 𝑋)
69683expa 1112 . . . . . . . . . . . . . . . . . 18 (((𝑅 ∈ RingOps ∧ (𝑤𝐻𝑟) ∈ 𝑋) ∧ 𝐴𝑋) → ((𝑤𝐻𝑟)𝐻𝐴) ∈ 𝑋)
70 eqid 2824 . . . . . . . . . . . . . . . . . . . 20 ((𝑤𝐻𝑟)𝐻𝐴) = ((𝑤𝐻𝑟)𝐻𝐴)
71 oveq1 7158 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 = (𝑤𝐻𝑟) → (𝑦𝐻𝐴) = ((𝑤𝐻𝑟)𝐻𝐴))
7271rspceeqv 3641 . . . . . . . . . . . . . . . . . . . 20 (((𝑤𝐻𝑟) ∈ 𝑋 ∧ ((𝑤𝐻𝑟)𝐻𝐴) = ((𝑤𝐻𝑟)𝐻𝐴)) → ∃𝑦𝑋 ((𝑤𝐻𝑟)𝐻𝐴) = (𝑦𝐻𝐴))
7370, 72mpan2 687 . . . . . . . . . . . . . . . . . . 19 ((𝑤𝐻𝑟) ∈ 𝑋 → ∃𝑦𝑋 ((𝑤𝐻𝑟)𝐻𝐴) = (𝑦𝐻𝐴))
7473ad2antlr 723 . . . . . . . . . . . . . . . . . 18 (((𝑅 ∈ RingOps ∧ (𝑤𝐻𝑟) ∈ 𝑋) ∧ 𝐴𝑋) → ∃𝑦𝑋 ((𝑤𝐻𝑟)𝐻𝐴) = (𝑦𝐻𝐴))
75 eqeq1 2828 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = ((𝑤𝐻𝑟)𝐻𝐴) → (𝑥 = (𝑦𝐻𝐴) ↔ ((𝑤𝐻𝑟)𝐻𝐴) = (𝑦𝐻𝐴)))
7675rexbidv 3301 . . . . . . . . . . . . . . . . . . 19 (𝑥 = ((𝑤𝐻𝑟)𝐻𝐴) → (∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴) ↔ ∃𝑦𝑋 ((𝑤𝐻𝑟)𝐻𝐴) = (𝑦𝐻𝐴)))
7776elrab 3683 . . . . . . . . . . . . . . . . . 18 (((𝑤𝐻𝑟)𝐻𝐴) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ↔ (((𝑤𝐻𝑟)𝐻𝐴) ∈ 𝑋 ∧ ∃𝑦𝑋 ((𝑤𝐻𝑟)𝐻𝐴) = (𝑦𝐻𝐴)))
7869, 74, 77sylanbrc 583 . . . . . . . . . . . . . . . . 17 (((𝑅 ∈ RingOps ∧ (𝑤𝐻𝑟) ∈ 𝑋) ∧ 𝐴𝑋) → ((𝑤𝐻𝑟)𝐻𝐴) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)})
7967, 78sylan 580 . . . . . . . . . . . . . . . 16 (((𝑅 ∈ RingOps ∧ (𝑤𝑋𝑟𝑋)) ∧ 𝐴𝑋) → ((𝑤𝐻𝑟)𝐻𝐴) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)})
8079an32s 648 . . . . . . . . . . . . . . 15 (((𝑅 ∈ RingOps ∧ 𝐴𝑋) ∧ (𝑤𝑋𝑟𝑋)) → ((𝑤𝐻𝑟)𝐻𝐴) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)})
8164, 80eqeltrrd 2918 . . . . . . . . . . . . . 14 (((𝑅 ∈ RingOps ∧ 𝐴𝑋) ∧ (𝑤𝑋𝑟𝑋)) → (𝑤𝐻(𝑟𝐻𝐴)) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)})
8281anass1rs 651 . . . . . . . . . . . . 13 ((((𝑅 ∈ RingOps ∧ 𝐴𝑋) ∧ 𝑟𝑋) ∧ 𝑤𝑋) → (𝑤𝐻(𝑟𝐻𝐴)) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)})
8382ralrimiva 3186 . . . . . . . . . . . 12 (((𝑅 ∈ RingOps ∧ 𝐴𝑋) ∧ 𝑟𝑋) → ∀𝑤𝑋 (𝑤𝐻(𝑟𝐻𝐴)) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)})
8460, 83jca 512 . . . . . . . . . . 11 (((𝑅 ∈ RingOps ∧ 𝐴𝑋) ∧ 𝑟𝑋) → (∀𝑣 ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ((𝑟𝐻𝐴)𝐺𝑣) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑤𝑋 (𝑤𝐻(𝑟𝐻𝐴)) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)}))
85 oveq1 7158 . . . . . . . . . . . . . 14 (𝑢 = (𝑟𝐻𝐴) → (𝑢𝐺𝑣) = ((𝑟𝐻𝐴)𝐺𝑣))
8685eleq1d 2901 . . . . . . . . . . . . 13 (𝑢 = (𝑟𝐻𝐴) → ((𝑢𝐺𝑣) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ↔ ((𝑟𝐻𝐴)𝐺𝑣) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)}))
8786ralbidv 3201 . . . . . . . . . . . 12 (𝑢 = (𝑟𝐻𝐴) → (∀𝑣 ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} (𝑢𝐺𝑣) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ↔ ∀𝑣 ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ((𝑟𝐻𝐴)𝐺𝑣) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)}))
88 oveq2 7159 . . . . . . . . . . . . . 14 (𝑢 = (𝑟𝐻𝐴) → (𝑤𝐻𝑢) = (𝑤𝐻(𝑟𝐻𝐴)))
8988eleq1d 2901 . . . . . . . . . . . . 13 (𝑢 = (𝑟𝐻𝐴) → ((𝑤𝐻𝑢) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ↔ (𝑤𝐻(𝑟𝐻𝐴)) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)}))
9089ralbidv 3201 . . . . . . . . . . . 12 (𝑢 = (𝑟𝐻𝐴) → (∀𝑤𝑋 (𝑤𝐻𝑢) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ↔ ∀𝑤𝑋 (𝑤𝐻(𝑟𝐻𝐴)) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)}))
9187, 90anbi12d 630 . . . . . . . . . . 11 (𝑢 = (𝑟𝐻𝐴) → ((∀𝑣 ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} (𝑢𝐺𝑣) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑤𝑋 (𝑤𝐻𝑢) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)}) ↔ (∀𝑣 ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ((𝑟𝐻𝐴)𝐺𝑣) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑤𝑋 (𝑤𝐻(𝑟𝐻𝐴)) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)})))
9284, 91syl5ibrcom 248 . . . . . . . . . 10 (((𝑅 ∈ RingOps ∧ 𝐴𝑋) ∧ 𝑟𝑋) → (𝑢 = (𝑟𝐻𝐴) → (∀𝑣 ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} (𝑢𝐺𝑣) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑤𝑋 (𝑤𝐻𝑢) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)})))
9392rexlimdva 3288 . . . . . . . . 9 ((𝑅 ∈ RingOps ∧ 𝐴𝑋) → (∃𝑟𝑋 𝑢 = (𝑟𝐻𝐴) → (∀𝑣 ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} (𝑢𝐺𝑣) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑤𝑋 (𝑤𝐻𝑢) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)})))
9493adantld 491 . . . . . . . 8 ((𝑅 ∈ RingOps ∧ 𝐴𝑋) → ((𝑢𝑋 ∧ ∃𝑟𝑋 𝑢 = (𝑟𝐻𝐴)) → (∀𝑣 ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} (𝑢𝐺𝑣) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑤𝑋 (𝑤𝐻𝑢) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)})))
9525, 94syl5bi 243 . . . . . . 7 ((𝑅 ∈ RingOps ∧ 𝐴𝑋) → (𝑢 ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} → (∀𝑣 ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} (𝑢𝐺𝑣) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑤𝑋 (𝑤𝐻𝑢) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)})))
9695ralrimiv 3185 . . . . . 6 ((𝑅 ∈ RingOps ∧ 𝐴𝑋) → ∀𝑢 ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} (∀𝑣 ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} (𝑢𝐺𝑣) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑤𝑋 (𝑤𝐻𝑢) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)}))
973, 18, 963jca 1122 . . . . 5 ((𝑅 ∈ RingOps ∧ 𝐴𝑋) → ({𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑋 ∧ (GId‘𝐺) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑢 ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} (∀𝑣 ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} (𝑢𝐺𝑣) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑤𝑋 (𝑤𝐻𝑢) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)})))
981, 97sylan 580 . . . 4 ((𝑅 ∈ CRingOps ∧ 𝐴𝑋) → ({𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑋 ∧ (GId‘𝐺) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑢 ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} (∀𝑣 ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} (𝑢𝐺𝑣) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑤𝑋 (𝑤𝐻𝑢) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)})))
994, 9, 5, 6isidlc 35162 . . . . 5 (𝑅 ∈ CRingOps → ({𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ∈ (Idl‘𝑅) ↔ ({𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑋 ∧ (GId‘𝐺) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑢 ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} (∀𝑣 ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} (𝑢𝐺𝑣) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑤𝑋 (𝑤𝐻𝑢) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)}))))
10099adantr 481 . . . 4 ((𝑅 ∈ CRingOps ∧ 𝐴𝑋) → ({𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ∈ (Idl‘𝑅) ↔ ({𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑋 ∧ (GId‘𝐺) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑢 ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} (∀𝑣 ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} (𝑢𝐺𝑣) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑤𝑋 (𝑤𝐻𝑢) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)}))))
10198, 100mpbird 258 . . 3 ((𝑅 ∈ CRingOps ∧ 𝐴𝑋) → {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ∈ (Idl‘𝑅))
102 simpr 485 . . . . 5 ((𝑅 ∈ CRingOps ∧ 𝐴𝑋) → 𝐴𝑋)
1034rneqi 5805 . . . . . . . . . 10 ran 𝐺 = ran (1st𝑅)
1045, 103eqtri 2848 . . . . . . . . 9 𝑋 = ran (1st𝑅)
105 eqid 2824 . . . . . . . . 9 (GId‘𝐻) = (GId‘𝐻)
106104, 9, 105rngo1cl 35086 . . . . . . . 8 (𝑅 ∈ RingOps → (GId‘𝐻) ∈ 𝑋)
107106adantr 481 . . . . . . 7 ((𝑅 ∈ RingOps ∧ 𝐴𝑋) → (GId‘𝐻) ∈ 𝑋)
1089, 104, 105rngolidm 35084 . . . . . . . 8 ((𝑅 ∈ RingOps ∧ 𝐴𝑋) → ((GId‘𝐻)𝐻𝐴) = 𝐴)
109108eqcomd 2830 . . . . . . 7 ((𝑅 ∈ RingOps ∧ 𝐴𝑋) → 𝐴 = ((GId‘𝐻)𝐻𝐴))
110 oveq1 7158 . . . . . . . 8 (𝑦 = (GId‘𝐻) → (𝑦𝐻𝐴) = ((GId‘𝐻)𝐻𝐴))
111110rspceeqv 3641 . . . . . . 7 (((GId‘𝐻) ∈ 𝑋𝐴 = ((GId‘𝐻)𝐻𝐴)) → ∃𝑦𝑋 𝐴 = (𝑦𝐻𝐴))
112107, 109, 111syl2anc 584 . . . . . 6 ((𝑅 ∈ RingOps ∧ 𝐴𝑋) → ∃𝑦𝑋 𝐴 = (𝑦𝐻𝐴))
1131, 112sylan 580 . . . . 5 ((𝑅 ∈ CRingOps ∧ 𝐴𝑋) → ∃𝑦𝑋 𝐴 = (𝑦𝐻𝐴))
114 eqeq1 2828 . . . . . . 7 (𝑥 = 𝐴 → (𝑥 = (𝑦𝐻𝐴) ↔ 𝐴 = (𝑦𝐻𝐴)))
115114rexbidv 3301 . . . . . 6 (𝑥 = 𝐴 → (∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴) ↔ ∃𝑦𝑋 𝐴 = (𝑦𝐻𝐴)))
116115elrab 3683 . . . . 5 (𝐴 ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ↔ (𝐴𝑋 ∧ ∃𝑦𝑋 𝐴 = (𝑦𝐻𝐴)))
117102, 113, 116sylanbrc 583 . . . 4 ((𝑅 ∈ CRingOps ∧ 𝐴𝑋) → 𝐴 ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)})
118117snssd 4740 . . 3 ((𝑅 ∈ CRingOps ∧ 𝐴𝑋) → {𝐴} ⊆ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)})
119 snssg 4715 . . . . . . . . 9 (𝐴𝑋 → (𝐴𝑗 ↔ {𝐴} ⊆ 𝑗))
120119biimpar 478 . . . . . . . 8 ((𝐴𝑋 ∧ {𝐴} ⊆ 𝑗) → 𝐴𝑗)
1214, 9, 5idllmulcl 35167 . . . . . . . . . . . . . . 15 (((𝑅 ∈ RingOps ∧ 𝑗 ∈ (Idl‘𝑅)) ∧ (𝐴𝑗𝑦𝑋)) → (𝑦𝐻𝐴) ∈ 𝑗)
122121anassrs 468 . . . . . . . . . . . . . 14 ((((𝑅 ∈ RingOps ∧ 𝑗 ∈ (Idl‘𝑅)) ∧ 𝐴𝑗) ∧ 𝑦𝑋) → (𝑦𝐻𝐴) ∈ 𝑗)
123 eleq1 2904 . . . . . . . . . . . . . 14 (𝑥 = (𝑦𝐻𝐴) → (𝑥𝑗 ↔ (𝑦𝐻𝐴) ∈ 𝑗))
124122, 123syl5ibrcom 248 . . . . . . . . . . . . 13 ((((𝑅 ∈ RingOps ∧ 𝑗 ∈ (Idl‘𝑅)) ∧ 𝐴𝑗) ∧ 𝑦𝑋) → (𝑥 = (𝑦𝐻𝐴) → 𝑥𝑗))
125124rexlimdva 3288 . . . . . . . . . . . 12 (((𝑅 ∈ RingOps ∧ 𝑗 ∈ (Idl‘𝑅)) ∧ 𝐴𝑗) → (∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴) → 𝑥𝑗))
126125adantr 481 . . . . . . . . . . 11 ((((𝑅 ∈ RingOps ∧ 𝑗 ∈ (Idl‘𝑅)) ∧ 𝐴𝑗) ∧ 𝑥𝑋) → (∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴) → 𝑥𝑗))
127126ralrimiva 3186 . . . . . . . . . 10 (((𝑅 ∈ RingOps ∧ 𝑗 ∈ (Idl‘𝑅)) ∧ 𝐴𝑗) → ∀𝑥𝑋 (∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴) → 𝑥𝑗))
128 rabss 4051 . . . . . . . . . 10 ({𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑗 ↔ ∀𝑥𝑋 (∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴) → 𝑥𝑗))
129127, 128sylibr 235 . . . . . . . . 9 (((𝑅 ∈ RingOps ∧ 𝑗 ∈ (Idl‘𝑅)) ∧ 𝐴𝑗) → {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑗)
130129ex 413 . . . . . . . 8 ((𝑅 ∈ RingOps ∧ 𝑗 ∈ (Idl‘𝑅)) → (𝐴𝑗 → {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑗))
131120, 130syl5 34 . . . . . . 7 ((𝑅 ∈ RingOps ∧ 𝑗 ∈ (Idl‘𝑅)) → ((𝐴𝑋 ∧ {𝐴} ⊆ 𝑗) → {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑗))
132131expdimp 453 . . . . . 6 (((𝑅 ∈ RingOps ∧ 𝑗 ∈ (Idl‘𝑅)) ∧ 𝐴𝑋) → ({𝐴} ⊆ 𝑗 → {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑗))
133132an32s 648 . . . . 5 (((𝑅 ∈ RingOps ∧ 𝐴𝑋) ∧ 𝑗 ∈ (Idl‘𝑅)) → ({𝐴} ⊆ 𝑗 → {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑗))
134133ralrimiva 3186 . . . 4 ((𝑅 ∈ RingOps ∧ 𝐴𝑋) → ∀𝑗 ∈ (Idl‘𝑅)({𝐴} ⊆ 𝑗 → {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑗))
1351, 134sylan 580 . . 3 ((𝑅 ∈ CRingOps ∧ 𝐴𝑋) → ∀𝑗 ∈ (Idl‘𝑅)({𝐴} ⊆ 𝑗 → {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑗))
136101, 118, 1353jca 1122 . 2 ((𝑅 ∈ CRingOps ∧ 𝐴𝑋) → ({𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ∈ (Idl‘𝑅) ∧ {𝐴} ⊆ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑗 ∈ (Idl‘𝑅)({𝐴} ⊆ 𝑗 → {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑗)))
137 snssi 4739 . . 3 (𝐴𝑋 → {𝐴} ⊆ 𝑋)
1384, 5igenval2 35213 . . 3 ((𝑅 ∈ RingOps ∧ {𝐴} ⊆ 𝑋) → ((𝑅 IdlGen {𝐴}) = {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ↔ ({𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ∈ (Idl‘𝑅) ∧ {𝐴} ⊆ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑗 ∈ (Idl‘𝑅)({𝐴} ⊆ 𝑗 → {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑗))))
1391, 137, 138syl2an 595 . 2 ((𝑅 ∈ CRingOps ∧ 𝐴𝑋) → ((𝑅 IdlGen {𝐴}) = {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ↔ ({𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ∈ (Idl‘𝑅) ∧ {𝐴} ⊆ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑗 ∈ (Idl‘𝑅)({𝐴} ⊆ 𝑗 → {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑗))))
140136, 139mpbird 258 1 ((𝑅 ∈ CRingOps ∧ 𝐴𝑋) → (𝑅 IdlGen {𝐴}) = {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)})
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396  w3a 1081   = wceq 1530  wcel 2106  wral 3142  wrex 3143  {crab 3146  wss 3939  {csn 4563  ran crn 5554  cfv 6351  (class class class)co 7151  1st c1st 7681  2nd c2nd 7682  GIdcgi 28182  RingOpscrngo 35041  CRingOpsccring 35140  Idlcidl 35154   IdlGen cigen 35206
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2152  ax-12 2167  ax-13 2385  ax-ext 2796  ax-rep 5186  ax-sep 5199  ax-nul 5206  ax-pow 5262  ax-pr 5325  ax-un 7454
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2615  df-eu 2649  df-clab 2803  df-cleq 2817  df-clel 2897  df-nfc 2967  df-ne 3021  df-ral 3147  df-rex 3148  df-reu 3149  df-rmo 3150  df-rab 3151  df-v 3501  df-sbc 3776  df-csb 3887  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-nul 4295  df-if 4470  df-pw 4543  df-sn 4564  df-pr 4566  df-op 4570  df-uni 4837  df-int 4874  df-iun 4918  df-br 5063  df-opab 5125  df-mpt 5143  df-id 5458  df-xp 5559  df-rel 5560  df-cnv 5561  df-co 5562  df-dm 5563  df-rn 5564  df-res 5565  df-ima 5566  df-iota 6311  df-fun 6353  df-fn 6354  df-f 6355  df-f1 6356  df-fo 6357  df-f1o 6358  df-fv 6359  df-riota 7109  df-ov 7154  df-oprab 7155  df-mpo 7156  df-1st 7683  df-2nd 7684  df-grpo 28185  df-gid 28186  df-ginv 28187  df-ablo 28237  df-ass 34990  df-exid 34992  df-mgmOLD 34996  df-sgrOLD 35008  df-mndo 35014  df-rngo 35042  df-com2 35137  df-crngo 35141  df-idl 35157  df-igen 35207
This theorem is referenced by:  isfldidl  35215  ispridlc  35217
  Copyright terms: Public domain W3C validator