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

Theorem unichnidl 34143
Description: The union of a nonempty chain of ideals is an ideal. (Contributed by Jeff Madsen, 5-Jan-2011.)
Assertion
Ref Expression
unichnidl ((𝑅 ∈ RingOps ∧ (𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅) ∧ ∀𝑖𝐶𝑗𝐶 (𝑖𝑗𝑗𝑖))) → 𝐶 ∈ (Idl‘𝑅))
Distinct variable groups:   𝑅,𝑖   𝐶,𝑖,𝑗
Allowed substitution hint:   𝑅(𝑗)

Proof of Theorem unichnidl
Dummy variables 𝑘 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dfss3 3733 . . . . 5 (𝐶 ⊆ (Idl‘𝑅) ↔ ∀𝑖𝐶 𝑖 ∈ (Idl‘𝑅))
2 eqid 2760 . . . . . . . . 9 (1st𝑅) = (1st𝑅)
3 eqid 2760 . . . . . . . . 9 ran (1st𝑅) = ran (1st𝑅)
42, 3idlss 34128 . . . . . . . 8 ((𝑅 ∈ RingOps ∧ 𝑖 ∈ (Idl‘𝑅)) → 𝑖 ⊆ ran (1st𝑅))
54ex 449 . . . . . . 7 (𝑅 ∈ RingOps → (𝑖 ∈ (Idl‘𝑅) → 𝑖 ⊆ ran (1st𝑅)))
65ralimdv 3101 . . . . . 6 (𝑅 ∈ RingOps → (∀𝑖𝐶 𝑖 ∈ (Idl‘𝑅) → ∀𝑖𝐶 𝑖 ⊆ ran (1st𝑅)))
76imp 444 . . . . 5 ((𝑅 ∈ RingOps ∧ ∀𝑖𝐶 𝑖 ∈ (Idl‘𝑅)) → ∀𝑖𝐶 𝑖 ⊆ ran (1st𝑅))
81, 7sylan2b 493 . . . 4 ((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) → ∀𝑖𝐶 𝑖 ⊆ ran (1st𝑅))
9 unissb 4621 . . . 4 ( 𝐶 ⊆ ran (1st𝑅) ↔ ∀𝑖𝐶 𝑖 ⊆ ran (1st𝑅))
108, 9sylibr 224 . . 3 ((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) → 𝐶 ⊆ ran (1st𝑅))
11103ad2antr2 1205 . 2 ((𝑅 ∈ RingOps ∧ (𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅) ∧ ∀𝑖𝐶𝑗𝐶 (𝑖𝑗𝑗𝑖))) → 𝐶 ⊆ ran (1st𝑅))
12 eqid 2760 . . . . . . . . . . 11 (GId‘(1st𝑅)) = (GId‘(1st𝑅))
132, 12idl0cl 34130 . . . . . . . . . 10 ((𝑅 ∈ RingOps ∧ 𝑖 ∈ (Idl‘𝑅)) → (GId‘(1st𝑅)) ∈ 𝑖)
1413ex 449 . . . . . . . . 9 (𝑅 ∈ RingOps → (𝑖 ∈ (Idl‘𝑅) → (GId‘(1st𝑅)) ∈ 𝑖))
1514ralimdv 3101 . . . . . . . 8 (𝑅 ∈ RingOps → (∀𝑖𝐶 𝑖 ∈ (Idl‘𝑅) → ∀𝑖𝐶 (GId‘(1st𝑅)) ∈ 𝑖))
1615imp 444 . . . . . . 7 ((𝑅 ∈ RingOps ∧ ∀𝑖𝐶 𝑖 ∈ (Idl‘𝑅)) → ∀𝑖𝐶 (GId‘(1st𝑅)) ∈ 𝑖)
171, 16sylan2b 493 . . . . . 6 ((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) → ∀𝑖𝐶 (GId‘(1st𝑅)) ∈ 𝑖)
18 r19.2z 4204 . . . . . 6 ((𝐶 ≠ ∅ ∧ ∀𝑖𝐶 (GId‘(1st𝑅)) ∈ 𝑖) → ∃𝑖𝐶 (GId‘(1st𝑅)) ∈ 𝑖)
1917, 18sylan2 492 . . . . 5 ((𝐶 ≠ ∅ ∧ (𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅))) → ∃𝑖𝐶 (GId‘(1st𝑅)) ∈ 𝑖)
2019an12s 878 . . . 4 ((𝑅 ∈ RingOps ∧ (𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅))) → ∃𝑖𝐶 (GId‘(1st𝑅)) ∈ 𝑖)
21 eluni2 4592 . . . 4 ((GId‘(1st𝑅)) ∈ 𝐶 ↔ ∃𝑖𝐶 (GId‘(1st𝑅)) ∈ 𝑖)
2220, 21sylibr 224 . . 3 ((𝑅 ∈ RingOps ∧ (𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅))) → (GId‘(1st𝑅)) ∈ 𝐶)
23223adantr3 1177 . 2 ((𝑅 ∈ RingOps ∧ (𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅) ∧ ∀𝑖𝐶𝑗𝐶 (𝑖𝑗𝑗𝑖))) → (GId‘(1st𝑅)) ∈ 𝐶)
24 eluni2 4592 . . . 4 (𝑥 𝐶 ↔ ∃𝑘𝐶 𝑥𝑘)
25 sseq1 3767 . . . . . . . . . . . . . . . 16 (𝑖 = 𝑘 → (𝑖𝑗𝑘𝑗))
26 sseq2 3768 . . . . . . . . . . . . . . . 16 (𝑖 = 𝑘 → (𝑗𝑖𝑗𝑘))
2725, 26orbi12d 748 . . . . . . . . . . . . . . 15 (𝑖 = 𝑘 → ((𝑖𝑗𝑗𝑖) ↔ (𝑘𝑗𝑗𝑘)))
2827ralbidv 3124 . . . . . . . . . . . . . 14 (𝑖 = 𝑘 → (∀𝑗𝐶 (𝑖𝑗𝑗𝑖) ↔ ∀𝑗𝐶 (𝑘𝑗𝑗𝑘)))
2928rspcv 3445 . . . . . . . . . . . . 13 (𝑘𝐶 → (∀𝑖𝐶𝑗𝐶 (𝑖𝑗𝑗𝑖) → ∀𝑗𝐶 (𝑘𝑗𝑗𝑘)))
3029adantr 472 . . . . . . . . . . . 12 ((𝑘𝐶𝑥𝑘) → (∀𝑖𝐶𝑗𝐶 (𝑖𝑗𝑗𝑖) → ∀𝑗𝐶 (𝑘𝑗𝑗𝑘)))
3130ad2antlr 765 . . . . . . . . . . 11 (((𝑅 ∈ RingOps ∧ (𝑘𝐶𝑥𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) → (∀𝑖𝐶𝑗𝐶 (𝑖𝑗𝑗𝑖) → ∀𝑗𝐶 (𝑘𝑗𝑗𝑘)))
3231imp 444 . . . . . . . . . 10 ((((𝑅 ∈ RingOps ∧ (𝑘𝐶𝑥𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ ∀𝑖𝐶𝑗𝐶 (𝑖𝑗𝑗𝑖)) → ∀𝑗𝐶 (𝑘𝑗𝑗𝑘))
33 eluni2 4592 . . . . . . . . . . . 12 (𝑦 𝐶 ↔ ∃𝑖𝐶 𝑦𝑖)
34 sseq2 3768 . . . . . . . . . . . . . . . . . . 19 (𝑗 = 𝑖 → (𝑘𝑗𝑘𝑖))
35 sseq1 3767 . . . . . . . . . . . . . . . . . . 19 (𝑗 = 𝑖 → (𝑗𝑘𝑖𝑘))
3634, 35orbi12d 748 . . . . . . . . . . . . . . . . . 18 (𝑗 = 𝑖 → ((𝑘𝑗𝑗𝑘) ↔ (𝑘𝑖𝑖𝑘)))
3736rspcv 3445 . . . . . . . . . . . . . . . . 17 (𝑖𝐶 → (∀𝑗𝐶 (𝑘𝑗𝑗𝑘) → (𝑘𝑖𝑖𝑘)))
3837ad2antrl 766 . . . . . . . . . . . . . . . 16 ((((𝑅 ∈ RingOps ∧ (𝑘𝐶𝑥𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ (𝑖𝐶𝑦𝑖)) → (∀𝑗𝐶 (𝑘𝑗𝑗𝑘) → (𝑘𝑖𝑖𝑘)))
3938imp 444 . . . . . . . . . . . . . . 15 (((((𝑅 ∈ RingOps ∧ (𝑘𝐶𝑥𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ (𝑖𝐶𝑦𝑖)) ∧ ∀𝑗𝐶 (𝑘𝑗𝑗𝑘)) → (𝑘𝑖𝑖𝑘))
40 ssel2 3739 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑘𝑖𝑥𝑘) → 𝑥𝑖)
4140ancoms 468 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑥𝑘𝑘𝑖) → 𝑥𝑖)
4241adantll 752 . . . . . . . . . . . . . . . . . . . . 21 (((𝑘𝐶𝑥𝑘) ∧ 𝑘𝑖) → 𝑥𝑖)
43 ssel2 3739 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐶 ⊆ (Idl‘𝑅) ∧ 𝑖𝐶) → 𝑖 ∈ (Idl‘𝑅))
442idladdcl 34131 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑅 ∈ RingOps ∧ 𝑖 ∈ (Idl‘𝑅)) ∧ (𝑥𝑖𝑦𝑖)) → (𝑥(1st𝑅)𝑦) ∈ 𝑖)
4544ancom2s 879 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝑅 ∈ RingOps ∧ 𝑖 ∈ (Idl‘𝑅)) ∧ (𝑦𝑖𝑥𝑖)) → (𝑥(1st𝑅)𝑦) ∈ 𝑖)
4645expr 644 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑅 ∈ RingOps ∧ 𝑖 ∈ (Idl‘𝑅)) ∧ 𝑦𝑖) → (𝑥𝑖 → (𝑥(1st𝑅)𝑦) ∈ 𝑖))
4746an32s 881 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑅 ∈ RingOps ∧ 𝑦𝑖) ∧ 𝑖 ∈ (Idl‘𝑅)) → (𝑥𝑖 → (𝑥(1st𝑅)𝑦) ∈ 𝑖))
4843, 47sylan2 492 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑅 ∈ RingOps ∧ 𝑦𝑖) ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ 𝑖𝐶)) → (𝑥𝑖 → (𝑥(1st𝑅)𝑦) ∈ 𝑖))
4948an42s 905 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ (𝑖𝐶𝑦𝑖)) → (𝑥𝑖 → (𝑥(1st𝑅)𝑦) ∈ 𝑖))
5049anasss 682 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑅 ∈ RingOps ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ (𝑖𝐶𝑦𝑖))) → (𝑥𝑖 → (𝑥(1st𝑅)𝑦) ∈ 𝑖))
5150imp 444 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑅 ∈ RingOps ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ (𝑖𝐶𝑦𝑖))) ∧ 𝑥𝑖) → (𝑥(1st𝑅)𝑦) ∈ 𝑖)
52 simprl 811 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐶 ⊆ (Idl‘𝑅) ∧ (𝑖𝐶𝑦𝑖)) → 𝑖𝐶)
5352ad2antlr 765 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑅 ∈ RingOps ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ (𝑖𝐶𝑦𝑖))) ∧ 𝑥𝑖) → 𝑖𝐶)
54 elunii 4593 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑥(1st𝑅)𝑦) ∈ 𝑖𝑖𝐶) → (𝑥(1st𝑅)𝑦) ∈ 𝐶)
5551, 53, 54syl2anc 696 . . . . . . . . . . . . . . . . . . . . 21 (((𝑅 ∈ RingOps ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ (𝑖𝐶𝑦𝑖))) ∧ 𝑥𝑖) → (𝑥(1st𝑅)𝑦) ∈ 𝐶)
5642, 55sylan2 492 . . . . . . . . . . . . . . . . . . . 20 (((𝑅 ∈ RingOps ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ (𝑖𝐶𝑦𝑖))) ∧ ((𝑘𝐶𝑥𝑘) ∧ 𝑘𝑖)) → (𝑥(1st𝑅)𝑦) ∈ 𝐶)
5756expr 644 . . . . . . . . . . . . . . . . . . 19 (((𝑅 ∈ RingOps ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ (𝑖𝐶𝑦𝑖))) ∧ (𝑘𝐶𝑥𝑘)) → (𝑘𝑖 → (𝑥(1st𝑅)𝑦) ∈ 𝐶))
5857an32s 881 . . . . . . . . . . . . . . . . . 18 (((𝑅 ∈ RingOps ∧ (𝑘𝐶𝑥𝑘)) ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ (𝑖𝐶𝑦𝑖))) → (𝑘𝑖 → (𝑥(1st𝑅)𝑦) ∈ 𝐶))
5958anassrs 683 . . . . . . . . . . . . . . . . 17 ((((𝑅 ∈ RingOps ∧ (𝑘𝐶𝑥𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ (𝑖𝐶𝑦𝑖)) → (𝑘𝑖 → (𝑥(1st𝑅)𝑦) ∈ 𝐶))
6059imp 444 . . . . . . . . . . . . . . . 16 (((((𝑅 ∈ RingOps ∧ (𝑘𝐶𝑥𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ (𝑖𝐶𝑦𝑖)) ∧ 𝑘𝑖) → (𝑥(1st𝑅)𝑦) ∈ 𝐶)
61 ssel2 3739 . . . . . . . . . . . . . . . . . . . 20 ((𝑖𝑘𝑦𝑖) → 𝑦𝑘)
6261ancoms 468 . . . . . . . . . . . . . . . . . . 19 ((𝑦𝑖𝑖𝑘) → 𝑦𝑘)
6362adantll 752 . . . . . . . . . . . . . . . . . 18 (((𝑖𝐶𝑦𝑖) ∧ 𝑖𝑘) → 𝑦𝑘)
64 ssel2 3739 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐶 ⊆ (Idl‘𝑅) ∧ 𝑘𝐶) → 𝑘 ∈ (Idl‘𝑅))
652idladdcl 34131 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑅 ∈ RingOps ∧ 𝑘 ∈ (Idl‘𝑅)) ∧ (𝑥𝑘𝑦𝑘)) → (𝑥(1st𝑅)𝑦) ∈ 𝑘)
6665expr 644 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑅 ∈ RingOps ∧ 𝑘 ∈ (Idl‘𝑅)) ∧ 𝑥𝑘) → (𝑦𝑘 → (𝑥(1st𝑅)𝑦) ∈ 𝑘))
6766an32s 881 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑅 ∈ RingOps ∧ 𝑥𝑘) ∧ 𝑘 ∈ (Idl‘𝑅)) → (𝑦𝑘 → (𝑥(1st𝑅)𝑦) ∈ 𝑘))
6864, 67sylan2 492 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑅 ∈ RingOps ∧ 𝑥𝑘) ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ 𝑘𝐶)) → (𝑦𝑘 → (𝑥(1st𝑅)𝑦) ∈ 𝑘))
6968an42s 905 . . . . . . . . . . . . . . . . . . . . 21 (((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ (𝑘𝐶𝑥𝑘)) → (𝑦𝑘 → (𝑥(1st𝑅)𝑦) ∈ 𝑘))
7069an32s 881 . . . . . . . . . . . . . . . . . . . 20 (((𝑅 ∈ RingOps ∧ (𝑘𝐶𝑥𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) → (𝑦𝑘 → (𝑥(1st𝑅)𝑦) ∈ 𝑘))
7170imp 444 . . . . . . . . . . . . . . . . . . 19 ((((𝑅 ∈ RingOps ∧ (𝑘𝐶𝑥𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ 𝑦𝑘) → (𝑥(1st𝑅)𝑦) ∈ 𝑘)
72 simprl 811 . . . . . . . . . . . . . . . . . . . 20 ((𝑅 ∈ RingOps ∧ (𝑘𝐶𝑥𝑘)) → 𝑘𝐶)
7372ad2antrr 764 . . . . . . . . . . . . . . . . . . 19 ((((𝑅 ∈ RingOps ∧ (𝑘𝐶𝑥𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ 𝑦𝑘) → 𝑘𝐶)
74 elunii 4593 . . . . . . . . . . . . . . . . . . 19 (((𝑥(1st𝑅)𝑦) ∈ 𝑘𝑘𝐶) → (𝑥(1st𝑅)𝑦) ∈ 𝐶)
7571, 73, 74syl2anc 696 . . . . . . . . . . . . . . . . . 18 ((((𝑅 ∈ RingOps ∧ (𝑘𝐶𝑥𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ 𝑦𝑘) → (𝑥(1st𝑅)𝑦) ∈ 𝐶)
7663, 75sylan2 492 . . . . . . . . . . . . . . . . 17 ((((𝑅 ∈ RingOps ∧ (𝑘𝐶𝑥𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ ((𝑖𝐶𝑦𝑖) ∧ 𝑖𝑘)) → (𝑥(1st𝑅)𝑦) ∈ 𝐶)
7776anassrs 683 . . . . . . . . . . . . . . . 16 (((((𝑅 ∈ RingOps ∧ (𝑘𝐶𝑥𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ (𝑖𝐶𝑦𝑖)) ∧ 𝑖𝑘) → (𝑥(1st𝑅)𝑦) ∈ 𝐶)
7860, 77jaodan 861 . . . . . . . . . . . . . . 15 (((((𝑅 ∈ RingOps ∧ (𝑘𝐶𝑥𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ (𝑖𝐶𝑦𝑖)) ∧ (𝑘𝑖𝑖𝑘)) → (𝑥(1st𝑅)𝑦) ∈ 𝐶)
7939, 78syldan 488 . . . . . . . . . . . . . 14 (((((𝑅 ∈ RingOps ∧ (𝑘𝐶𝑥𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ (𝑖𝐶𝑦𝑖)) ∧ ∀𝑗𝐶 (𝑘𝑗𝑗𝑘)) → (𝑥(1st𝑅)𝑦) ∈ 𝐶)
8079an32s 881 . . . . . . . . . . . . 13 (((((𝑅 ∈ RingOps ∧ (𝑘𝐶𝑥𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ ∀𝑗𝐶 (𝑘𝑗𝑗𝑘)) ∧ (𝑖𝐶𝑦𝑖)) → (𝑥(1st𝑅)𝑦) ∈ 𝐶)
8180rexlimdvaa 3170 . . . . . . . . . . . 12 ((((𝑅 ∈ RingOps ∧ (𝑘𝐶𝑥𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ ∀𝑗𝐶 (𝑘𝑗𝑗𝑘)) → (∃𝑖𝐶 𝑦𝑖 → (𝑥(1st𝑅)𝑦) ∈ 𝐶))
8233, 81syl5bi 232 . . . . . . . . . . 11 ((((𝑅 ∈ RingOps ∧ (𝑘𝐶𝑥𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ ∀𝑗𝐶 (𝑘𝑗𝑗𝑘)) → (𝑦 𝐶 → (𝑥(1st𝑅)𝑦) ∈ 𝐶))
8382ralrimiv 3103 . . . . . . . . . 10 ((((𝑅 ∈ RingOps ∧ (𝑘𝐶𝑥𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ ∀𝑗𝐶 (𝑘𝑗𝑗𝑘)) → ∀𝑦 𝐶(𝑥(1st𝑅)𝑦) ∈ 𝐶)
8432, 83syldan 488 . . . . . . . . 9 ((((𝑅 ∈ RingOps ∧ (𝑘𝐶𝑥𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ ∀𝑖𝐶𝑗𝐶 (𝑖𝑗𝑗𝑖)) → ∀𝑦 𝐶(𝑥(1st𝑅)𝑦) ∈ 𝐶)
8584anasss 682 . . . . . . . 8 (((𝑅 ∈ RingOps ∧ (𝑘𝐶𝑥𝑘)) ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ ∀𝑖𝐶𝑗𝐶 (𝑖𝑗𝑗𝑖))) → ∀𝑦 𝐶(𝑥(1st𝑅)𝑦) ∈ 𝐶)
86853adantr1 1175 . . . . . . 7 (((𝑅 ∈ RingOps ∧ (𝑘𝐶𝑥𝑘)) ∧ (𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅) ∧ ∀𝑖𝐶𝑗𝐶 (𝑖𝑗𝑗𝑖))) → ∀𝑦 𝐶(𝑥(1st𝑅)𝑦) ∈ 𝐶)
8786an32s 881 . . . . . 6 (((𝑅 ∈ RingOps ∧ (𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅) ∧ ∀𝑖𝐶𝑗𝐶 (𝑖𝑗𝑗𝑖))) ∧ (𝑘𝐶𝑥𝑘)) → ∀𝑦 𝐶(𝑥(1st𝑅)𝑦) ∈ 𝐶)
88 eqid 2760 . . . . . . . . . . . . . . . . . 18 (2nd𝑅) = (2nd𝑅)
892, 88, 3idllmulcl 34132 . . . . . . . . . . . . . . . . 17 (((𝑅 ∈ RingOps ∧ 𝑘 ∈ (Idl‘𝑅)) ∧ (𝑥𝑘𝑧 ∈ ran (1st𝑅))) → (𝑧(2nd𝑅)𝑥) ∈ 𝑘)
9089exp43 641 . . . . . . . . . . . . . . . 16 (𝑅 ∈ RingOps → (𝑘 ∈ (Idl‘𝑅) → (𝑥𝑘 → (𝑧 ∈ ran (1st𝑅) → (𝑧(2nd𝑅)𝑥) ∈ 𝑘))))
9190com23 86 . . . . . . . . . . . . . . 15 (𝑅 ∈ RingOps → (𝑥𝑘 → (𝑘 ∈ (Idl‘𝑅) → (𝑧 ∈ ran (1st𝑅) → (𝑧(2nd𝑅)𝑥) ∈ 𝑘))))
9291imp41 620 . . . . . . . . . . . . . 14 ((((𝑅 ∈ RingOps ∧ 𝑥𝑘) ∧ 𝑘 ∈ (Idl‘𝑅)) ∧ 𝑧 ∈ ran (1st𝑅)) → (𝑧(2nd𝑅)𝑥) ∈ 𝑘)
9364, 92sylanl2 686 . . . . . . . . . . . . 13 ((((𝑅 ∈ RingOps ∧ 𝑥𝑘) ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ 𝑘𝐶)) ∧ 𝑧 ∈ ran (1st𝑅)) → (𝑧(2nd𝑅)𝑥) ∈ 𝑘)
94 simplrr 820 . . . . . . . . . . . . 13 ((((𝑅 ∈ RingOps ∧ 𝑥𝑘) ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ 𝑘𝐶)) ∧ 𝑧 ∈ ran (1st𝑅)) → 𝑘𝐶)
95 elunii 4593 . . . . . . . . . . . . 13 (((𝑧(2nd𝑅)𝑥) ∈ 𝑘𝑘𝐶) → (𝑧(2nd𝑅)𝑥) ∈ 𝐶)
9693, 94, 95syl2anc 696 . . . . . . . . . . . 12 ((((𝑅 ∈ RingOps ∧ 𝑥𝑘) ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ 𝑘𝐶)) ∧ 𝑧 ∈ ran (1st𝑅)) → (𝑧(2nd𝑅)𝑥) ∈ 𝐶)
972, 88, 3idlrmulcl 34133 . . . . . . . . . . . . . . . . 17 (((𝑅 ∈ RingOps ∧ 𝑘 ∈ (Idl‘𝑅)) ∧ (𝑥𝑘𝑧 ∈ ran (1st𝑅))) → (𝑥(2nd𝑅)𝑧) ∈ 𝑘)
9897exp43 641 . . . . . . . . . . . . . . . 16 (𝑅 ∈ RingOps → (𝑘 ∈ (Idl‘𝑅) → (𝑥𝑘 → (𝑧 ∈ ran (1st𝑅) → (𝑥(2nd𝑅)𝑧) ∈ 𝑘))))
9998com23 86 . . . . . . . . . . . . . . 15 (𝑅 ∈ RingOps → (𝑥𝑘 → (𝑘 ∈ (Idl‘𝑅) → (𝑧 ∈ ran (1st𝑅) → (𝑥(2nd𝑅)𝑧) ∈ 𝑘))))
10099imp41 620 . . . . . . . . . . . . . 14 ((((𝑅 ∈ RingOps ∧ 𝑥𝑘) ∧ 𝑘 ∈ (Idl‘𝑅)) ∧ 𝑧 ∈ ran (1st𝑅)) → (𝑥(2nd𝑅)𝑧) ∈ 𝑘)
10164, 100sylanl2 686 . . . . . . . . . . . . 13 ((((𝑅 ∈ RingOps ∧ 𝑥𝑘) ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ 𝑘𝐶)) ∧ 𝑧 ∈ ran (1st𝑅)) → (𝑥(2nd𝑅)𝑧) ∈ 𝑘)
102 elunii 4593 . . . . . . . . . . . . 13 (((𝑥(2nd𝑅)𝑧) ∈ 𝑘𝑘𝐶) → (𝑥(2nd𝑅)𝑧) ∈ 𝐶)
103101, 94, 102syl2anc 696 . . . . . . . . . . . 12 ((((𝑅 ∈ RingOps ∧ 𝑥𝑘) ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ 𝑘𝐶)) ∧ 𝑧 ∈ ran (1st𝑅)) → (𝑥(2nd𝑅)𝑧) ∈ 𝐶)
10496, 103jca 555 . . . . . . . . . . 11 ((((𝑅 ∈ RingOps ∧ 𝑥𝑘) ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ 𝑘𝐶)) ∧ 𝑧 ∈ ran (1st𝑅)) → ((𝑧(2nd𝑅)𝑥) ∈ 𝐶 ∧ (𝑥(2nd𝑅)𝑧) ∈ 𝐶))
105104ralrimiva 3104 . . . . . . . . . 10 (((𝑅 ∈ RingOps ∧ 𝑥𝑘) ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ 𝑘𝐶)) → ∀𝑧 ∈ ran (1st𝑅)((𝑧(2nd𝑅)𝑥) ∈ 𝐶 ∧ (𝑥(2nd𝑅)𝑧) ∈ 𝐶))
106105an42s 905 . . . . . . . . 9 (((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ (𝑘𝐶𝑥𝑘)) → ∀𝑧 ∈ ran (1st𝑅)((𝑧(2nd𝑅)𝑥) ∈ 𝐶 ∧ (𝑥(2nd𝑅)𝑧) ∈ 𝐶))
107106an32s 881 . . . . . . . 8 (((𝑅 ∈ RingOps ∧ (𝑘𝐶𝑥𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) → ∀𝑧 ∈ ran (1st𝑅)((𝑧(2nd𝑅)𝑥) ∈ 𝐶 ∧ (𝑥(2nd𝑅)𝑧) ∈ 𝐶))
1081073ad2antr2 1205 . . . . . . 7 (((𝑅 ∈ RingOps ∧ (𝑘𝐶𝑥𝑘)) ∧ (𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅) ∧ ∀𝑖𝐶𝑗𝐶 (𝑖𝑗𝑗𝑖))) → ∀𝑧 ∈ ran (1st𝑅)((𝑧(2nd𝑅)𝑥) ∈ 𝐶 ∧ (𝑥(2nd𝑅)𝑧) ∈ 𝐶))
109108an32s 881 . . . . . 6 (((𝑅 ∈ RingOps ∧ (𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅) ∧ ∀𝑖𝐶𝑗𝐶 (𝑖𝑗𝑗𝑖))) ∧ (𝑘𝐶𝑥𝑘)) → ∀𝑧 ∈ ran (1st𝑅)((𝑧(2nd𝑅)𝑥) ∈ 𝐶 ∧ (𝑥(2nd𝑅)𝑧) ∈ 𝐶))
11087, 109jca 555 . . . . 5 (((𝑅 ∈ RingOps ∧ (𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅) ∧ ∀𝑖𝐶𝑗𝐶 (𝑖𝑗𝑗𝑖))) ∧ (𝑘𝐶𝑥𝑘)) → (∀𝑦 𝐶(𝑥(1st𝑅)𝑦) ∈ 𝐶 ∧ ∀𝑧 ∈ ran (1st𝑅)((𝑧(2nd𝑅)𝑥) ∈ 𝐶 ∧ (𝑥(2nd𝑅)𝑧) ∈ 𝐶)))
111110rexlimdvaa 3170 . . . 4 ((𝑅 ∈ RingOps ∧ (𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅) ∧ ∀𝑖𝐶𝑗𝐶 (𝑖𝑗𝑗𝑖))) → (∃𝑘𝐶 𝑥𝑘 → (∀𝑦 𝐶(𝑥(1st𝑅)𝑦) ∈ 𝐶 ∧ ∀𝑧 ∈ ran (1st𝑅)((𝑧(2nd𝑅)𝑥) ∈ 𝐶 ∧ (𝑥(2nd𝑅)𝑧) ∈ 𝐶))))
11224, 111syl5bi 232 . . 3 ((𝑅 ∈ RingOps ∧ (𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅) ∧ ∀𝑖𝐶𝑗𝐶 (𝑖𝑗𝑗𝑖))) → (𝑥 𝐶 → (∀𝑦 𝐶(𝑥(1st𝑅)𝑦) ∈ 𝐶 ∧ ∀𝑧 ∈ ran (1st𝑅)((𝑧(2nd𝑅)𝑥) ∈ 𝐶 ∧ (𝑥(2nd𝑅)𝑧) ∈ 𝐶))))
113112ralrimiv 3103 . 2 ((𝑅 ∈ RingOps ∧ (𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅) ∧ ∀𝑖𝐶𝑗𝐶 (𝑖𝑗𝑗𝑖))) → ∀𝑥 𝐶(∀𝑦 𝐶(𝑥(1st𝑅)𝑦) ∈ 𝐶 ∧ ∀𝑧 ∈ ran (1st𝑅)((𝑧(2nd𝑅)𝑥) ∈ 𝐶 ∧ (𝑥(2nd𝑅)𝑧) ∈ 𝐶)))
1142, 88, 3, 12isidl 34126 . . 3 (𝑅 ∈ RingOps → ( 𝐶 ∈ (Idl‘𝑅) ↔ ( 𝐶 ⊆ ran (1st𝑅) ∧ (GId‘(1st𝑅)) ∈ 𝐶 ∧ ∀𝑥 𝐶(∀𝑦 𝐶(𝑥(1st𝑅)𝑦) ∈ 𝐶 ∧ ∀𝑧 ∈ ran (1st𝑅)((𝑧(2nd𝑅)𝑥) ∈ 𝐶 ∧ (𝑥(2nd𝑅)𝑧) ∈ 𝐶)))))
115114adantr 472 . 2 ((𝑅 ∈ RingOps ∧ (𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅) ∧ ∀𝑖𝐶𝑗𝐶 (𝑖𝑗𝑗𝑖))) → ( 𝐶 ∈ (Idl‘𝑅) ↔ ( 𝐶 ⊆ ran (1st𝑅) ∧ (GId‘(1st𝑅)) ∈ 𝐶 ∧ ∀𝑥 𝐶(∀𝑦 𝐶(𝑥(1st𝑅)𝑦) ∈ 𝐶 ∧ ∀𝑧 ∈ ran (1st𝑅)((𝑧(2nd𝑅)𝑥) ∈ 𝐶 ∧ (𝑥(2nd𝑅)𝑧) ∈ 𝐶)))))
11611, 23, 113, 115mpbir3and 1428 1 ((𝑅 ∈ RingOps ∧ (𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅) ∧ ∀𝑖𝐶𝑗𝐶 (𝑖𝑗𝑗𝑖))) → 𝐶 ∈ (Idl‘𝑅))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wo 382  wa 383  w3a 1072  wcel 2139  wne 2932  wral 3050  wrex 3051  wss 3715  c0 4058   cuni 4588  ran crn 5267  cfv 6049  (class class class)co 6813  1st c1st 7331  2nd c2nd 7332  GIdcgi 27653  RingOpscrngo 34006  Idlcidl 34119
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7114
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-ral 3055  df-rex 3056  df-rab 3059  df-v 3342  df-sbc 3577  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-op 4328  df-uni 4589  df-br 4805  df-opab 4865  df-mpt 4882  df-id 5174  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-iota 6012  df-fun 6051  df-fv 6057  df-ov 6816  df-idl 34122
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator