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 38074
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 38007 . . . . 5 (𝑅 ∈ CRingOps → 𝑅 ∈ RingOps)
2 ssrab2 4080 . . . . . . 7 {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑋
32a1i 11 . . . . . 6 ((𝑅 ∈ RingOps ∧ 𝐴𝑋) → {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑋)
4 prnc.1 . . . . . . . . 9 𝐺 = (1st𝑅)
5 prnc.3 . . . . . . . . 9 𝑋 = ran 𝐺
6 eqid 2737 . . . . . . . . 9 (GId‘𝐺) = (GId‘𝐺)
74, 5, 6rngo0cl 37926 . . . . . . . 8 (𝑅 ∈ RingOps → (GId‘𝐺) ∈ 𝑋)
87adantr 480 . . . . . . 7 ((𝑅 ∈ RingOps ∧ 𝐴𝑋) → (GId‘𝐺) ∈ 𝑋)
9 prnc.2 . . . . . . . . . 10 𝐻 = (2nd𝑅)
106, 5, 4, 9rngolz 37929 . . . . . . . . 9 ((𝑅 ∈ RingOps ∧ 𝐴𝑋) → ((GId‘𝐺)𝐻𝐴) = (GId‘𝐺))
1110eqcomd 2743 . . . . . . . 8 ((𝑅 ∈ RingOps ∧ 𝐴𝑋) → (GId‘𝐺) = ((GId‘𝐺)𝐻𝐴))
12 oveq1 7438 . . . . . . . . 9 (𝑦 = (GId‘𝐺) → (𝑦𝐻𝐴) = ((GId‘𝐺)𝐻𝐴))
1312rspceeqv 3645 . . . . . . . 8 (((GId‘𝐺) ∈ 𝑋 ∧ (GId‘𝐺) = ((GId‘𝐺)𝐻𝐴)) → ∃𝑦𝑋 (GId‘𝐺) = (𝑦𝐻𝐴))
148, 11, 13syl2anc 584 . . . . . . 7 ((𝑅 ∈ RingOps ∧ 𝐴𝑋) → ∃𝑦𝑋 (GId‘𝐺) = (𝑦𝐻𝐴))
15 eqeq1 2741 . . . . . . . . 9 (𝑥 = (GId‘𝐺) → (𝑥 = (𝑦𝐻𝐴) ↔ (GId‘𝐺) = (𝑦𝐻𝐴)))
1615rexbidv 3179 . . . . . . . 8 (𝑥 = (GId‘𝐺) → (∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴) ↔ ∃𝑦𝑋 (GId‘𝐺) = (𝑦𝐻𝐴)))
1716elrab 3692 . . . . . . 7 ((GId‘𝐺) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ↔ ((GId‘𝐺) ∈ 𝑋 ∧ ∃𝑦𝑋 (GId‘𝐺) = (𝑦𝐻𝐴)))
188, 14, 17sylanbrc 583 . . . . . 6 ((𝑅 ∈ RingOps ∧ 𝐴𝑋) → (GId‘𝐺) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)})
19 eqeq1 2741 . . . . . . . . . . 11 (𝑥 = 𝑢 → (𝑥 = (𝑦𝐻𝐴) ↔ 𝑢 = (𝑦𝐻𝐴)))
2019rexbidv 3179 . . . . . . . . . 10 (𝑥 = 𝑢 → (∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴) ↔ ∃𝑦𝑋 𝑢 = (𝑦𝐻𝐴)))
21 oveq1 7438 . . . . . . . . . . . 12 (𝑦 = 𝑟 → (𝑦𝐻𝐴) = (𝑟𝐻𝐴))
2221eqeq2d 2748 . . . . . . . . . . 11 (𝑦 = 𝑟 → (𝑢 = (𝑦𝐻𝐴) ↔ 𝑢 = (𝑟𝐻𝐴)))
2322cbvrexvw 3238 . . . . . . . . . 10 (∃𝑦𝑋 𝑢 = (𝑦𝐻𝐴) ↔ ∃𝑟𝑋 𝑢 = (𝑟𝐻𝐴))
2420, 23bitrdi 287 . . . . . . . . 9 (𝑥 = 𝑢 → (∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴) ↔ ∃𝑟𝑋 𝑢 = (𝑟𝐻𝐴)))
2524elrab 3692 . . . . . . . 8 (𝑢 ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ↔ (𝑢𝑋 ∧ ∃𝑟𝑋 𝑢 = (𝑟𝐻𝐴)))
26 eqeq1 2741 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑣 → (𝑥 = (𝑦𝐻𝐴) ↔ 𝑣 = (𝑦𝐻𝐴)))
2726rexbidv 3179 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑣 → (∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴) ↔ ∃𝑦𝑋 𝑣 = (𝑦𝐻𝐴)))
28 oveq1 7438 . . . . . . . . . . . . . . . . . 18 (𝑦 = 𝑠 → (𝑦𝐻𝐴) = (𝑠𝐻𝐴))
2928eqeq2d 2748 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑠 → (𝑣 = (𝑦𝐻𝐴) ↔ 𝑣 = (𝑠𝐻𝐴)))
3029cbvrexvw 3238 . . . . . . . . . . . . . . . 16 (∃𝑦𝑋 𝑣 = (𝑦𝐻𝐴) ↔ ∃𝑠𝑋 𝑣 = (𝑠𝐻𝐴))
3127, 30bitrdi 287 . . . . . . . . . . . . . . 15 (𝑥 = 𝑣 → (∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴) ↔ ∃𝑠𝑋 𝑣 = (𝑠𝐻𝐴)))
3231elrab 3692 . . . . . . . . . . . . . 14 (𝑣 ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ↔ (𝑣𝑋 ∧ ∃𝑠𝑋 𝑣 = (𝑠𝐻𝐴)))
334, 9, 5rngodir 37912 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑅 ∈ RingOps ∧ (𝑟𝑋𝑠𝑋𝐴𝑋)) → ((𝑟𝐺𝑠)𝐻𝐴) = ((𝑟𝐻𝐴)𝐺(𝑠𝐻𝐴)))
34333exp2 1355 . . . . . . . . . . . . . . . . . . . . 21 (𝑅 ∈ RingOps → (𝑟𝑋 → (𝑠𝑋 → (𝐴𝑋 → ((𝑟𝐺𝑠)𝐻𝐴) = ((𝑟𝐻𝐴)𝐺(𝑠𝐻𝐴))))))
3534imp42 426 . . . . . . . . . . . . . . . . . . . 20 (((𝑅 ∈ RingOps ∧ (𝑟𝑋𝑠𝑋)) ∧ 𝐴𝑋) → ((𝑟𝐺𝑠)𝐻𝐴) = ((𝑟𝐻𝐴)𝐺(𝑠𝐻𝐴)))
364, 5rngogcl 37919 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑅 ∈ RingOps ∧ 𝑟𝑋𝑠𝑋) → (𝑟𝐺𝑠) ∈ 𝑋)
37363expib 1123 . . . . . . . . . . . . . . . . . . . . . 22 (𝑅 ∈ RingOps → ((𝑟𝑋𝑠𝑋) → (𝑟𝐺𝑠) ∈ 𝑋))
3837imdistani 568 . . . . . . . . . . . . . . . . . . . . 21 ((𝑅 ∈ RingOps ∧ (𝑟𝑋𝑠𝑋)) → (𝑅 ∈ RingOps ∧ (𝑟𝐺𝑠) ∈ 𝑋))
394, 9, 5rngocl 37908 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑅 ∈ RingOps ∧ (𝑟𝐺𝑠) ∈ 𝑋𝐴𝑋) → ((𝑟𝐺𝑠)𝐻𝐴) ∈ 𝑋)
40393expa 1119 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑅 ∈ RingOps ∧ (𝑟𝐺𝑠) ∈ 𝑋) ∧ 𝐴𝑋) → ((𝑟𝐺𝑠)𝐻𝐴) ∈ 𝑋)
41 eqid 2737 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑟𝐺𝑠)𝐻𝐴) = ((𝑟𝐺𝑠)𝐻𝐴)
42 oveq1 7438 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 = (𝑟𝐺𝑠) → (𝑦𝐻𝐴) = ((𝑟𝐺𝑠)𝐻𝐴))
4342rspceeqv 3645 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑟𝐺𝑠) ∈ 𝑋 ∧ ((𝑟𝐺𝑠)𝐻𝐴) = ((𝑟𝐺𝑠)𝐻𝐴)) → ∃𝑦𝑋 ((𝑟𝐺𝑠)𝐻𝐴) = (𝑦𝐻𝐴))
4441, 43mpan2 691 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑟𝐺𝑠) ∈ 𝑋 → ∃𝑦𝑋 ((𝑟𝐺𝑠)𝐻𝐴) = (𝑦𝐻𝐴))
4544ad2antlr 727 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑅 ∈ RingOps ∧ (𝑟𝐺𝑠) ∈ 𝑋) ∧ 𝐴𝑋) → ∃𝑦𝑋 ((𝑟𝐺𝑠)𝐻𝐴) = (𝑦𝐻𝐴))
46 eqeq1 2741 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = ((𝑟𝐺𝑠)𝐻𝐴) → (𝑥 = (𝑦𝐻𝐴) ↔ ((𝑟𝐺𝑠)𝐻𝐴) = (𝑦𝐻𝐴)))
4746rexbidv 3179 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = ((𝑟𝐺𝑠)𝐻𝐴) → (∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴) ↔ ∃𝑦𝑋 ((𝑟𝐺𝑠)𝐻𝐴) = (𝑦𝐻𝐴)))
4847elrab 3692 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑟𝐺𝑠)𝐻𝐴) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ↔ (((𝑟𝐺𝑠)𝐻𝐴) ∈ 𝑋 ∧ ∃𝑦𝑋 ((𝑟𝐺𝑠)𝐻𝐴) = (𝑦𝐻𝐴)))
4940, 45, 48sylanbrc 583 . . . . . . . . . . . . . . . . . . . . 21 (((𝑅 ∈ RingOps ∧ (𝑟𝐺𝑠) ∈ 𝑋) ∧ 𝐴𝑋) → ((𝑟𝐺𝑠)𝐻𝐴) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)})
5038, 49sylan 580 . . . . . . . . . . . . . . . . . . . 20 (((𝑅 ∈ RingOps ∧ (𝑟𝑋𝑠𝑋)) ∧ 𝐴𝑋) → ((𝑟𝐺𝑠)𝐻𝐴) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)})
5135, 50eqeltrrd 2842 . . . . . . . . . . . . . . . . . . 19 (((𝑅 ∈ RingOps ∧ (𝑟𝑋𝑠𝑋)) ∧ 𝐴𝑋) → ((𝑟𝐻𝐴)𝐺(𝑠𝐻𝐴)) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)})
5251an32s 652 . . . . . . . . . . . . . . . . . 18 (((𝑅 ∈ RingOps ∧ 𝐴𝑋) ∧ (𝑟𝑋𝑠𝑋)) → ((𝑟𝐻𝐴)𝐺(𝑠𝐻𝐴)) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)})
5352anassrs 467 . . . . . . . . . . . . . . . . 17 ((((𝑅 ∈ RingOps ∧ 𝐴𝑋) ∧ 𝑟𝑋) ∧ 𝑠𝑋) → ((𝑟𝐻𝐴)𝐺(𝑠𝐻𝐴)) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)})
54 oveq2 7439 . . . . . . . . . . . . . . . . . 18 (𝑣 = (𝑠𝐻𝐴) → ((𝑟𝐻𝐴)𝐺𝑣) = ((𝑟𝐻𝐴)𝐺(𝑠𝐻𝐴)))
5554eleq1d 2826 . . . . . . . . . . . . . . . . 17 (𝑣 = (𝑠𝐻𝐴) → (((𝑟𝐻𝐴)𝐺𝑣) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ↔ ((𝑟𝐻𝐴)𝐺(𝑠𝐻𝐴)) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)}))
5653, 55syl5ibrcom 247 . . . . . . . . . . . . . . . 16 ((((𝑅 ∈ RingOps ∧ 𝐴𝑋) ∧ 𝑟𝑋) ∧ 𝑠𝑋) → (𝑣 = (𝑠𝐻𝐴) → ((𝑟𝐻𝐴)𝐺𝑣) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)}))
5756rexlimdva 3155 . . . . . . . . . . . . . . 15 (((𝑅 ∈ RingOps ∧ 𝐴𝑋) ∧ 𝑟𝑋) → (∃𝑠𝑋 𝑣 = (𝑠𝐻𝐴) → ((𝑟𝐻𝐴)𝐺𝑣) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)}))
5857adantld 490 . . . . . . . . . . . . . 14 (((𝑅 ∈ RingOps ∧ 𝐴𝑋) ∧ 𝑟𝑋) → ((𝑣𝑋 ∧ ∃𝑠𝑋 𝑣 = (𝑠𝐻𝐴)) → ((𝑟𝐻𝐴)𝐺𝑣) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)}))
5932, 58biimtrid 242 . . . . . . . . . . . . 13 (((𝑅 ∈ RingOps ∧ 𝐴𝑋) ∧ 𝑟𝑋) → (𝑣 ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} → ((𝑟𝐻𝐴)𝐺𝑣) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)}))
6059ralrimiv 3145 . . . . . . . . . . . 12 (((𝑅 ∈ RingOps ∧ 𝐴𝑋) ∧ 𝑟𝑋) → ∀𝑣 ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ((𝑟𝐻𝐴)𝐺𝑣) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)})
614, 9, 5rngoass 37913 . . . . . . . . . . . . . . . . . 18 ((𝑅 ∈ RingOps ∧ (𝑤𝑋𝑟𝑋𝐴𝑋)) → ((𝑤𝐻𝑟)𝐻𝐴) = (𝑤𝐻(𝑟𝐻𝐴)))
62613exp2 1355 . . . . . . . . . . . . . . . . 17 (𝑅 ∈ RingOps → (𝑤𝑋 → (𝑟𝑋 → (𝐴𝑋 → ((𝑤𝐻𝑟)𝐻𝐴) = (𝑤𝐻(𝑟𝐻𝐴))))))
6362imp42 426 . . . . . . . . . . . . . . . 16 (((𝑅 ∈ RingOps ∧ (𝑤𝑋𝑟𝑋)) ∧ 𝐴𝑋) → ((𝑤𝐻𝑟)𝐻𝐴) = (𝑤𝐻(𝑟𝐻𝐴)))
6463an32s 652 . . . . . . . . . . . . . . 15 (((𝑅 ∈ RingOps ∧ 𝐴𝑋) ∧ (𝑤𝑋𝑟𝑋)) → ((𝑤𝐻𝑟)𝐻𝐴) = (𝑤𝐻(𝑟𝐻𝐴)))
654, 9, 5rngocl 37908 . . . . . . . . . . . . . . . . . . 19 ((𝑅 ∈ RingOps ∧ 𝑤𝑋𝑟𝑋) → (𝑤𝐻𝑟) ∈ 𝑋)
66653expib 1123 . . . . . . . . . . . . . . . . . 18 (𝑅 ∈ RingOps → ((𝑤𝑋𝑟𝑋) → (𝑤𝐻𝑟) ∈ 𝑋))
6766imdistani 568 . . . . . . . . . . . . . . . . 17 ((𝑅 ∈ RingOps ∧ (𝑤𝑋𝑟𝑋)) → (𝑅 ∈ RingOps ∧ (𝑤𝐻𝑟) ∈ 𝑋))
684, 9, 5rngocl 37908 . . . . . . . . . . . . . . . . . . 19 ((𝑅 ∈ RingOps ∧ (𝑤𝐻𝑟) ∈ 𝑋𝐴𝑋) → ((𝑤𝐻𝑟)𝐻𝐴) ∈ 𝑋)
69683expa 1119 . . . . . . . . . . . . . . . . . 18 (((𝑅 ∈ RingOps ∧ (𝑤𝐻𝑟) ∈ 𝑋) ∧ 𝐴𝑋) → ((𝑤𝐻𝑟)𝐻𝐴) ∈ 𝑋)
70 eqid 2737 . . . . . . . . . . . . . . . . . . . 20 ((𝑤𝐻𝑟)𝐻𝐴) = ((𝑤𝐻𝑟)𝐻𝐴)
71 oveq1 7438 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 = (𝑤𝐻𝑟) → (𝑦𝐻𝐴) = ((𝑤𝐻𝑟)𝐻𝐴))
7271rspceeqv 3645 . . . . . . . . . . . . . . . . . . . 20 (((𝑤𝐻𝑟) ∈ 𝑋 ∧ ((𝑤𝐻𝑟)𝐻𝐴) = ((𝑤𝐻𝑟)𝐻𝐴)) → ∃𝑦𝑋 ((𝑤𝐻𝑟)𝐻𝐴) = (𝑦𝐻𝐴))
7370, 72mpan2 691 . . . . . . . . . . . . . . . . . . 19 ((𝑤𝐻𝑟) ∈ 𝑋 → ∃𝑦𝑋 ((𝑤𝐻𝑟)𝐻𝐴) = (𝑦𝐻𝐴))
7473ad2antlr 727 . . . . . . . . . . . . . . . . . 18 (((𝑅 ∈ RingOps ∧ (𝑤𝐻𝑟) ∈ 𝑋) ∧ 𝐴𝑋) → ∃𝑦𝑋 ((𝑤𝐻𝑟)𝐻𝐴) = (𝑦𝐻𝐴))
75 eqeq1 2741 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = ((𝑤𝐻𝑟)𝐻𝐴) → (𝑥 = (𝑦𝐻𝐴) ↔ ((𝑤𝐻𝑟)𝐻𝐴) = (𝑦𝐻𝐴)))
7675rexbidv 3179 . . . . . . . . . . . . . . . . . . 19 (𝑥 = ((𝑤𝐻𝑟)𝐻𝐴) → (∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴) ↔ ∃𝑦𝑋 ((𝑤𝐻𝑟)𝐻𝐴) = (𝑦𝐻𝐴)))
7776elrab 3692 . . . . . . . . . . . . . . . . . 18 (((𝑤𝐻𝑟)𝐻𝐴) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ↔ (((𝑤𝐻𝑟)𝐻𝐴) ∈ 𝑋 ∧ ∃𝑦𝑋 ((𝑤𝐻𝑟)𝐻𝐴) = (𝑦𝐻𝐴)))
7869, 74, 77sylanbrc 583 . . . . . . . . . . . . . . . . 17 (((𝑅 ∈ RingOps ∧ (𝑤𝐻𝑟) ∈ 𝑋) ∧ 𝐴𝑋) → ((𝑤𝐻𝑟)𝐻𝐴) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)})
7967, 78sylan 580 . . . . . . . . . . . . . . . 16 (((𝑅 ∈ RingOps ∧ (𝑤𝑋𝑟𝑋)) ∧ 𝐴𝑋) → ((𝑤𝐻𝑟)𝐻𝐴) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)})
8079an32s 652 . . . . . . . . . . . . . . 15 (((𝑅 ∈ RingOps ∧ 𝐴𝑋) ∧ (𝑤𝑋𝑟𝑋)) → ((𝑤𝐻𝑟)𝐻𝐴) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)})
8164, 80eqeltrrd 2842 . . . . . . . . . . . . . 14 (((𝑅 ∈ RingOps ∧ 𝐴𝑋) ∧ (𝑤𝑋𝑟𝑋)) → (𝑤𝐻(𝑟𝐻𝐴)) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)})
8281anass1rs 655 . . . . . . . . . . . . 13 ((((𝑅 ∈ RingOps ∧ 𝐴𝑋) ∧ 𝑟𝑋) ∧ 𝑤𝑋) → (𝑤𝐻(𝑟𝐻𝐴)) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)})
8382ralrimiva 3146 . . . . . . . . . . . 12 (((𝑅 ∈ RingOps ∧ 𝐴𝑋) ∧ 𝑟𝑋) → ∀𝑤𝑋 (𝑤𝐻(𝑟𝐻𝐴)) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)})
8460, 83jca 511 . . . . . . . . . . 11 (((𝑅 ∈ RingOps ∧ 𝐴𝑋) ∧ 𝑟𝑋) → (∀𝑣 ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ((𝑟𝐻𝐴)𝐺𝑣) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑤𝑋 (𝑤𝐻(𝑟𝐻𝐴)) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)}))
85 oveq1 7438 . . . . . . . . . . . . . 14 (𝑢 = (𝑟𝐻𝐴) → (𝑢𝐺𝑣) = ((𝑟𝐻𝐴)𝐺𝑣))
8685eleq1d 2826 . . . . . . . . . . . . 13 (𝑢 = (𝑟𝐻𝐴) → ((𝑢𝐺𝑣) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ↔ ((𝑟𝐻𝐴)𝐺𝑣) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)}))
8786ralbidv 3178 . . . . . . . . . . . 12 (𝑢 = (𝑟𝐻𝐴) → (∀𝑣 ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} (𝑢𝐺𝑣) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ↔ ∀𝑣 ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ((𝑟𝐻𝐴)𝐺𝑣) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)}))
88 oveq2 7439 . . . . . . . . . . . . . 14 (𝑢 = (𝑟𝐻𝐴) → (𝑤𝐻𝑢) = (𝑤𝐻(𝑟𝐻𝐴)))
8988eleq1d 2826 . . . . . . . . . . . . 13 (𝑢 = (𝑟𝐻𝐴) → ((𝑤𝐻𝑢) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ↔ (𝑤𝐻(𝑟𝐻𝐴)) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)}))
9089ralbidv 3178 . . . . . . . . . . . 12 (𝑢 = (𝑟𝐻𝐴) → (∀𝑤𝑋 (𝑤𝐻𝑢) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ↔ ∀𝑤𝑋 (𝑤𝐻(𝑟𝐻𝐴)) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)}))
9187, 90anbi12d 632 . . . . . . . . . . 11 (𝑢 = (𝑟𝐻𝐴) → ((∀𝑣 ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} (𝑢𝐺𝑣) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑤𝑋 (𝑤𝐻𝑢) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)}) ↔ (∀𝑣 ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ((𝑟𝐻𝐴)𝐺𝑣) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑤𝑋 (𝑤𝐻(𝑟𝐻𝐴)) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)})))
9284, 91syl5ibrcom 247 . . . . . . . . . 10 (((𝑅 ∈ RingOps ∧ 𝐴𝑋) ∧ 𝑟𝑋) → (𝑢 = (𝑟𝐻𝐴) → (∀𝑣 ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} (𝑢𝐺𝑣) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑤𝑋 (𝑤𝐻𝑢) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)})))
9392rexlimdva 3155 . . . . . . . . 9 ((𝑅 ∈ RingOps ∧ 𝐴𝑋) → (∃𝑟𝑋 𝑢 = (𝑟𝐻𝐴) → (∀𝑣 ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} (𝑢𝐺𝑣) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑤𝑋 (𝑤𝐻𝑢) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)})))
9493adantld 490 . . . . . . . 8 ((𝑅 ∈ RingOps ∧ 𝐴𝑋) → ((𝑢𝑋 ∧ ∃𝑟𝑋 𝑢 = (𝑟𝐻𝐴)) → (∀𝑣 ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} (𝑢𝐺𝑣) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑤𝑋 (𝑤𝐻𝑢) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)})))
9525, 94biimtrid 242 . . . . . . 7 ((𝑅 ∈ RingOps ∧ 𝐴𝑋) → (𝑢 ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} → (∀𝑣 ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} (𝑢𝐺𝑣) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑤𝑋 (𝑤𝐻𝑢) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)})))
9695ralrimiv 3145 . . . . . 6 ((𝑅 ∈ RingOps ∧ 𝐴𝑋) → ∀𝑢 ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} (∀𝑣 ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} (𝑢𝐺𝑣) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑤𝑋 (𝑤𝐻𝑢) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)}))
973, 18, 963jca 1129 . . . . 5 ((𝑅 ∈ RingOps ∧ 𝐴𝑋) → ({𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑋 ∧ (GId‘𝐺) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑢 ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} (∀𝑣 ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} (𝑢𝐺𝑣) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑤𝑋 (𝑤𝐻𝑢) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)})))
981, 97sylan 580 . . . 4 ((𝑅 ∈ CRingOps ∧ 𝐴𝑋) → ({𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑋 ∧ (GId‘𝐺) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑢 ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} (∀𝑣 ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} (𝑢𝐺𝑣) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑤𝑋 (𝑤𝐻𝑢) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)})))
994, 9, 5, 6isidlc 38022 . . . . 5 (𝑅 ∈ CRingOps → ({𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ∈ (Idl‘𝑅) ↔ ({𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑋 ∧ (GId‘𝐺) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑢 ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} (∀𝑣 ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} (𝑢𝐺𝑣) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑤𝑋 (𝑤𝐻𝑢) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)}))))
10099adantr 480 . . . 4 ((𝑅 ∈ CRingOps ∧ 𝐴𝑋) → ({𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ∈ (Idl‘𝑅) ↔ ({𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑋 ∧ (GId‘𝐺) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑢 ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} (∀𝑣 ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} (𝑢𝐺𝑣) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑤𝑋 (𝑤𝐻𝑢) ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)}))))
10198, 100mpbird 257 . . 3 ((𝑅 ∈ CRingOps ∧ 𝐴𝑋) → {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ∈ (Idl‘𝑅))
102 simpr 484 . . . . 5 ((𝑅 ∈ CRingOps ∧ 𝐴𝑋) → 𝐴𝑋)
1034rneqi 5948 . . . . . . . . . 10 ran 𝐺 = ran (1st𝑅)
1045, 103eqtri 2765 . . . . . . . . 9 𝑋 = ran (1st𝑅)
105 eqid 2737 . . . . . . . . 9 (GId‘𝐻) = (GId‘𝐻)
106104, 9, 105rngo1cl 37946 . . . . . . . 8 (𝑅 ∈ RingOps → (GId‘𝐻) ∈ 𝑋)
107106adantr 480 . . . . . . 7 ((𝑅 ∈ RingOps ∧ 𝐴𝑋) → (GId‘𝐻) ∈ 𝑋)
1089, 104, 105rngolidm 37944 . . . . . . . 8 ((𝑅 ∈ RingOps ∧ 𝐴𝑋) → ((GId‘𝐻)𝐻𝐴) = 𝐴)
109108eqcomd 2743 . . . . . . 7 ((𝑅 ∈ RingOps ∧ 𝐴𝑋) → 𝐴 = ((GId‘𝐻)𝐻𝐴))
110 oveq1 7438 . . . . . . . 8 (𝑦 = (GId‘𝐻) → (𝑦𝐻𝐴) = ((GId‘𝐻)𝐻𝐴))
111110rspceeqv 3645 . . . . . . 7 (((GId‘𝐻) ∈ 𝑋𝐴 = ((GId‘𝐻)𝐻𝐴)) → ∃𝑦𝑋 𝐴 = (𝑦𝐻𝐴))
112107, 109, 111syl2anc 584 . . . . . 6 ((𝑅 ∈ RingOps ∧ 𝐴𝑋) → ∃𝑦𝑋 𝐴 = (𝑦𝐻𝐴))
1131, 112sylan 580 . . . . 5 ((𝑅 ∈ CRingOps ∧ 𝐴𝑋) → ∃𝑦𝑋 𝐴 = (𝑦𝐻𝐴))
114 eqeq1 2741 . . . . . . 7 (𝑥 = 𝐴 → (𝑥 = (𝑦𝐻𝐴) ↔ 𝐴 = (𝑦𝐻𝐴)))
115114rexbidv 3179 . . . . . 6 (𝑥 = 𝐴 → (∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴) ↔ ∃𝑦𝑋 𝐴 = (𝑦𝐻𝐴)))
116115elrab 3692 . . . . 5 (𝐴 ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ↔ (𝐴𝑋 ∧ ∃𝑦𝑋 𝐴 = (𝑦𝐻𝐴)))
117102, 113, 116sylanbrc 583 . . . 4 ((𝑅 ∈ CRingOps ∧ 𝐴𝑋) → 𝐴 ∈ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)})
118117snssd 4809 . . 3 ((𝑅 ∈ CRingOps ∧ 𝐴𝑋) → {𝐴} ⊆ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)})
119 snssg 4783 . . . . . . . . 9 (𝐴𝑋 → (𝐴𝑗 ↔ {𝐴} ⊆ 𝑗))
120119biimpar 477 . . . . . . . 8 ((𝐴𝑋 ∧ {𝐴} ⊆ 𝑗) → 𝐴𝑗)
1214, 9, 5idllmulcl 38027 . . . . . . . . . . . . . . 15 (((𝑅 ∈ RingOps ∧ 𝑗 ∈ (Idl‘𝑅)) ∧ (𝐴𝑗𝑦𝑋)) → (𝑦𝐻𝐴) ∈ 𝑗)
122121anassrs 467 . . . . . . . . . . . . . 14 ((((𝑅 ∈ RingOps ∧ 𝑗 ∈ (Idl‘𝑅)) ∧ 𝐴𝑗) ∧ 𝑦𝑋) → (𝑦𝐻𝐴) ∈ 𝑗)
123 eleq1 2829 . . . . . . . . . . . . . 14 (𝑥 = (𝑦𝐻𝐴) → (𝑥𝑗 ↔ (𝑦𝐻𝐴) ∈ 𝑗))
124122, 123syl5ibrcom 247 . . . . . . . . . . . . 13 ((((𝑅 ∈ RingOps ∧ 𝑗 ∈ (Idl‘𝑅)) ∧ 𝐴𝑗) ∧ 𝑦𝑋) → (𝑥 = (𝑦𝐻𝐴) → 𝑥𝑗))
125124rexlimdva 3155 . . . . . . . . . . . 12 (((𝑅 ∈ RingOps ∧ 𝑗 ∈ (Idl‘𝑅)) ∧ 𝐴𝑗) → (∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴) → 𝑥𝑗))
126125adantr 480 . . . . . . . . . . 11 ((((𝑅 ∈ RingOps ∧ 𝑗 ∈ (Idl‘𝑅)) ∧ 𝐴𝑗) ∧ 𝑥𝑋) → (∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴) → 𝑥𝑗))
127126ralrimiva 3146 . . . . . . . . . 10 (((𝑅 ∈ RingOps ∧ 𝑗 ∈ (Idl‘𝑅)) ∧ 𝐴𝑗) → ∀𝑥𝑋 (∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴) → 𝑥𝑗))
128 rabss 4072 . . . . . . . . . 10 ({𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑗 ↔ ∀𝑥𝑋 (∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴) → 𝑥𝑗))
129127, 128sylibr 234 . . . . . . . . 9 (((𝑅 ∈ RingOps ∧ 𝑗 ∈ (Idl‘𝑅)) ∧ 𝐴𝑗) → {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑗)
130129ex 412 . . . . . . . 8 ((𝑅 ∈ RingOps ∧ 𝑗 ∈ (Idl‘𝑅)) → (𝐴𝑗 → {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑗))
131120, 130syl5 34 . . . . . . 7 ((𝑅 ∈ RingOps ∧ 𝑗 ∈ (Idl‘𝑅)) → ((𝐴𝑋 ∧ {𝐴} ⊆ 𝑗) → {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑗))
132131expdimp 452 . . . . . 6 (((𝑅 ∈ RingOps ∧ 𝑗 ∈ (Idl‘𝑅)) ∧ 𝐴𝑋) → ({𝐴} ⊆ 𝑗 → {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑗))
133132an32s 652 . . . . 5 (((𝑅 ∈ RingOps ∧ 𝐴𝑋) ∧ 𝑗 ∈ (Idl‘𝑅)) → ({𝐴} ⊆ 𝑗 → {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑗))
134133ralrimiva 3146 . . . 4 ((𝑅 ∈ RingOps ∧ 𝐴𝑋) → ∀𝑗 ∈ (Idl‘𝑅)({𝐴} ⊆ 𝑗 → {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑗))
1351, 134sylan 580 . . 3 ((𝑅 ∈ CRingOps ∧ 𝐴𝑋) → ∀𝑗 ∈ (Idl‘𝑅)({𝐴} ⊆ 𝑗 → {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑗))
136101, 118, 1353jca 1129 . 2 ((𝑅 ∈ CRingOps ∧ 𝐴𝑋) → ({𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ∈ (Idl‘𝑅) ∧ {𝐴} ⊆ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑗 ∈ (Idl‘𝑅)({𝐴} ⊆ 𝑗 → {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑗)))
137 snssi 4808 . . 3 (𝐴𝑋 → {𝐴} ⊆ 𝑋)
1384, 5igenval2 38073 . . 3 ((𝑅 ∈ RingOps ∧ {𝐴} ⊆ 𝑋) → ((𝑅 IdlGen {𝐴}) = {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ↔ ({𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ∈ (Idl‘𝑅) ∧ {𝐴} ⊆ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑗 ∈ (Idl‘𝑅)({𝐴} ⊆ 𝑗 → {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑗))))
1391, 137, 138syl2an 596 . 2 ((𝑅 ∈ CRingOps ∧ 𝐴𝑋) → ((𝑅 IdlGen {𝐴}) = {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ↔ ({𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ∈ (Idl‘𝑅) ∧ {𝐴} ⊆ {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ∧ ∀𝑗 ∈ (Idl‘𝑅)({𝐴} ⊆ 𝑗 → {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)} ⊆ 𝑗))))
140136, 139mpbird 257 1 ((𝑅 ∈ CRingOps ∧ 𝐴𝑋) → (𝑅 IdlGen {𝐴}) = {𝑥𝑋 ∣ ∃𝑦𝑋 𝑥 = (𝑦𝐻𝐴)})
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  w3a 1087   = wceq 1540  wcel 2108  wral 3061  wrex 3070  {crab 3436  wss 3951  {csn 4626  ran crn 5686  cfv 6561  (class class class)co 7431  1st c1st 8012  2nd c2nd 8013  GIdcgi 30509  RingOpscrngo 37901  CRingOpsccring 38000  Idlcidl 38014   IdlGen cigen 38066
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-rmo 3380  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-int 4947  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-1st 8014  df-2nd 8015  df-grpo 30512  df-gid 30513  df-ginv 30514  df-ablo 30564  df-ass 37850  df-exid 37852  df-mgmOLD 37856  df-sgrOLD 37868  df-mndo 37874  df-rngo 37902  df-com2 37997  df-crngo 38001  df-idl 38017  df-igen 38067
This theorem is referenced by:  isfldidl  38075  ispridlc  38077
  Copyright terms: Public domain W3C validator