Mathbox for Thierry Arnoux < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  rhmpreimacn Structured version   Visualization version   GIF version

Theorem rhmpreimacn 31301
 Description: The function mapping a prime ideal to its preimage by a surjective ring homomorphism is continuous, when considering the Zariski topology. Corollary 1.2.3 of [EGA], p. 83. Notice that the direction of the continuous map 𝐺 is reverse: the original ring homomorphism 𝐹 goes from 𝑅 to 𝑆, but the continuous map 𝐺 goes from 𝐵 to 𝐴. This mapping is also called "induced map on prime spectra" or "pullback on primes". (Contributed by Thierry Arnoux, 8-Jul-2024.)
Hypotheses
Ref Expression
rhmpreimacn.t 𝑇 = (Spec‘𝑅)
rhmpreimacn.u 𝑈 = (Spec‘𝑆)
rhmpreimacn.a 𝐴 = (PrmIdeal‘𝑅)
rhmpreimacn.b 𝐵 = (PrmIdeal‘𝑆)
rhmpreimacn.j 𝐽 = (TopOpen‘𝑇)
rhmpreimacn.k 𝐾 = (TopOpen‘𝑈)
rhmpreimacn.g 𝐺 = (𝑖𝐵 ↦ (𝐹𝑖))
rhmpreimacn.r (𝜑𝑅 ∈ CRing)
rhmpreimacn.s (𝜑𝑆 ∈ CRing)
rhmpreimacn.f (𝜑𝐹 ∈ (𝑅 RingHom 𝑆))
rhmpreimacn.1 (𝜑 → ran 𝐹 = (Base‘𝑆))
Assertion
Ref Expression
rhmpreimacn (𝜑𝐺 ∈ (𝐾 Cn 𝐽))
Distinct variable groups:   𝐴,𝑖   𝐵,𝑖   𝑖,𝐹   𝑖,𝐺   𝑖,𝐽   𝑅,𝑖   𝑆,𝑖   𝜑,𝑖
Allowed substitution hints:   𝑇(𝑖)   𝑈(𝑖)   𝐾(𝑖)

Proof of Theorem rhmpreimacn
Dummy variables 𝑗 𝑘 𝑥 𝑏 𝑎 𝑙 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 rhmpreimacn.s . . 3 (𝜑𝑆 ∈ CRing)
2 rhmpreimacn.u . . . 4 𝑈 = (Spec‘𝑆)
3 rhmpreimacn.k . . . 4 𝐾 = (TopOpen‘𝑈)
4 rhmpreimacn.b . . . 4 𝐵 = (PrmIdeal‘𝑆)
52, 3, 4zartopon 31293 . . 3 (𝑆 ∈ CRing → 𝐾 ∈ (TopOn‘𝐵))
61, 5syl 17 . 2 (𝜑𝐾 ∈ (TopOn‘𝐵))
7 rhmpreimacn.r . . 3 (𝜑𝑅 ∈ CRing)
8 rhmpreimacn.t . . . 4 𝑇 = (Spec‘𝑅)
9 rhmpreimacn.j . . . 4 𝐽 = (TopOpen‘𝑇)
10 rhmpreimacn.a . . . 4 𝐴 = (PrmIdeal‘𝑅)
118, 9, 10zartopon 31293 . . 3 (𝑅 ∈ CRing → 𝐽 ∈ (TopOn‘𝐴))
127, 11syl 17 . 2 (𝜑𝐽 ∈ (TopOn‘𝐴))
131adantr 484 . . . 4 ((𝜑𝑖𝐵) → 𝑆 ∈ CRing)
14 rhmpreimacn.f . . . . 5 (𝜑𝐹 ∈ (𝑅 RingHom 𝑆))
1514adantr 484 . . . 4 ((𝜑𝑖𝐵) → 𝐹 ∈ (𝑅 RingHom 𝑆))
16 simpr 488 . . . . 5 ((𝜑𝑖𝐵) → 𝑖𝐵)
1716, 4eleqtrdi 2900 . . . 4 ((𝜑𝑖𝐵) → 𝑖 ∈ (PrmIdeal‘𝑆))
1810rhmpreimaprmidl 31093 . . . 4 (((𝑆 ∈ CRing ∧ 𝐹 ∈ (𝑅 RingHom 𝑆)) ∧ 𝑖 ∈ (PrmIdeal‘𝑆)) → (𝐹𝑖) ∈ 𝐴)
1913, 15, 17, 18syl21anc 836 . . 3 ((𝜑𝑖𝐵) → (𝐹𝑖) ∈ 𝐴)
20 rhmpreimacn.g . . 3 𝐺 = (𝑖𝐵 ↦ (𝐹𝑖))
2119, 20fmptd 6862 . 2 (𝜑𝐺:𝐵𝐴)
224fvexi 6666 . . . . . . 7 𝐵 ∈ V
2322rabex 5202 . . . . . 6 {𝑘𝐵𝑗𝑘} ∈ V
24 sseq1 3941 . . . . . . . 8 (𝑙 = 𝑗 → (𝑙𝑘𝑗𝑘))
2524rabbidv 3427 . . . . . . 7 (𝑙 = 𝑗 → {𝑘𝐵𝑙𝑘} = {𝑘𝐵𝑗𝑘})
2625cbvmptv 5136 . . . . . 6 (𝑙 ∈ (LIdeal‘𝑆) ↦ {𝑘𝐵𝑙𝑘}) = (𝑗 ∈ (LIdeal‘𝑆) ↦ {𝑘𝐵𝑗𝑘})
2723, 26fnmpti 6468 . . . . 5 (𝑙 ∈ (LIdeal‘𝑆) ↦ {𝑘𝐵𝑙𝑘}) Fn (LIdeal‘𝑆)
2814ad3antrrr 729 . . . . . . . 8 ((((𝜑𝑥 ∈ (Clsd‘𝐽)) ∧ 𝑎 ∈ (LIdeal‘𝑅)) ∧ ((𝑙 ∈ (LIdeal‘𝑅) ↦ {𝑘𝐴𝑙𝑘})‘𝑎) = 𝑥) → 𝐹 ∈ (𝑅 RingHom 𝑆))
29 rhmpreimacn.1 . . . . . . . . 9 (𝜑 → ran 𝐹 = (Base‘𝑆))
3029ad3antrrr 729 . . . . . . . 8 ((((𝜑𝑥 ∈ (Clsd‘𝐽)) ∧ 𝑎 ∈ (LIdeal‘𝑅)) ∧ ((𝑙 ∈ (LIdeal‘𝑅) ↦ {𝑘𝐴𝑙𝑘})‘𝑎) = 𝑥) → ran 𝐹 = (Base‘𝑆))
31 simplr 768 . . . . . . . 8 ((((𝜑𝑥 ∈ (Clsd‘𝐽)) ∧ 𝑎 ∈ (LIdeal‘𝑅)) ∧ ((𝑙 ∈ (LIdeal‘𝑅) ↦ {𝑘𝐴𝑙𝑘})‘𝑎) = 𝑥) → 𝑎 ∈ (LIdeal‘𝑅))
32 eqid 2798 . . . . . . . . 9 (Base‘𝑆) = (Base‘𝑆)
33 eqid 2798 . . . . . . . . 9 (LIdeal‘𝑅) = (LIdeal‘𝑅)
34 eqid 2798 . . . . . . . . 9 (LIdeal‘𝑆) = (LIdeal‘𝑆)
3532, 33, 34rhmimaidl 31075 . . . . . . . 8 ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ ran 𝐹 = (Base‘𝑆) ∧ 𝑎 ∈ (LIdeal‘𝑅)) → (𝐹𝑎) ∈ (LIdeal‘𝑆))
3628, 30, 31, 35syl3anc 1368 . . . . . . 7 ((((𝜑𝑥 ∈ (Clsd‘𝐽)) ∧ 𝑎 ∈ (LIdeal‘𝑅)) ∧ ((𝑙 ∈ (LIdeal‘𝑅) ↦ {𝑘𝐴𝑙𝑘})‘𝑎) = 𝑥) → (𝐹𝑎) ∈ (LIdeal‘𝑆))
37 fveqeq2 6661 . . . . . . . 8 (𝑏 = (𝐹𝑎) → (((𝑙 ∈ (LIdeal‘𝑆) ↦ {𝑘𝐵𝑙𝑘})‘𝑏) = (𝐺𝑥) ↔ ((𝑙 ∈ (LIdeal‘𝑆) ↦ {𝑘𝐵𝑙𝑘})‘(𝐹𝑎)) = (𝐺𝑥)))
3837adantl 485 . . . . . . 7 (((((𝜑𝑥 ∈ (Clsd‘𝐽)) ∧ 𝑎 ∈ (LIdeal‘𝑅)) ∧ ((𝑙 ∈ (LIdeal‘𝑅) ↦ {𝑘𝐴𝑙𝑘})‘𝑎) = 𝑥) ∧ 𝑏 = (𝐹𝑎)) → (((𝑙 ∈ (LIdeal‘𝑆) ↦ {𝑘𝐵𝑙𝑘})‘𝑏) = (𝐺𝑥) ↔ ((𝑙 ∈ (LIdeal‘𝑆) ↦ {𝑘𝐵𝑙𝑘})‘(𝐹𝑎)) = (𝐺𝑥)))
397ad3antrrr 729 . . . . . . . . 9 ((((𝜑𝑥 ∈ (Clsd‘𝐽)) ∧ 𝑎 ∈ (LIdeal‘𝑅)) ∧ ((𝑙 ∈ (LIdeal‘𝑅) ↦ {𝑘𝐴𝑙𝑘})‘𝑎) = 𝑥) → 𝑅 ∈ CRing)
401ad3antrrr 729 . . . . . . . . 9 ((((𝜑𝑥 ∈ (Clsd‘𝐽)) ∧ 𝑎 ∈ (LIdeal‘𝑅)) ∧ ((𝑙 ∈ (LIdeal‘𝑅) ↦ {𝑘𝐴𝑙𝑘})‘𝑎) = 𝑥) → 𝑆 ∈ CRing)
4124rabbidv 3427 . . . . . . . . . 10 (𝑙 = 𝑗 → {𝑘𝐴𝑙𝑘} = {𝑘𝐴𝑗𝑘})
4241cbvmptv 5136 . . . . . . . . 9 (𝑙 ∈ (LIdeal‘𝑅) ↦ {𝑘𝐴𝑙𝑘}) = (𝑗 ∈ (LIdeal‘𝑅) ↦ {𝑘𝐴𝑗𝑘})
438, 2, 10, 4, 9, 3, 20, 39, 40, 28, 30, 31, 42, 26rhmpreimacnlem 31300 . . . . . . . 8 ((((𝜑𝑥 ∈ (Clsd‘𝐽)) ∧ 𝑎 ∈ (LIdeal‘𝑅)) ∧ ((𝑙 ∈ (LIdeal‘𝑅) ↦ {𝑘𝐴𝑙𝑘})‘𝑎) = 𝑥) → ((𝑙 ∈ (LIdeal‘𝑆) ↦ {𝑘𝐵𝑙𝑘})‘(𝐹𝑎)) = (𝐺 “ ((𝑙 ∈ (LIdeal‘𝑅) ↦ {𝑘𝐴𝑙𝑘})‘𝑎)))
44 simpr 488 . . . . . . . . 9 ((((𝜑𝑥 ∈ (Clsd‘𝐽)) ∧ 𝑎 ∈ (LIdeal‘𝑅)) ∧ ((𝑙 ∈ (LIdeal‘𝑅) ↦ {𝑘𝐴𝑙𝑘})‘𝑎) = 𝑥) → ((𝑙 ∈ (LIdeal‘𝑅) ↦ {𝑘𝐴𝑙𝑘})‘𝑎) = 𝑥)
4544imaeq2d 5899 . . . . . . . 8 ((((𝜑𝑥 ∈ (Clsd‘𝐽)) ∧ 𝑎 ∈ (LIdeal‘𝑅)) ∧ ((𝑙 ∈ (LIdeal‘𝑅) ↦ {𝑘𝐴𝑙𝑘})‘𝑎) = 𝑥) → (𝐺 “ ((𝑙 ∈ (LIdeal‘𝑅) ↦ {𝑘𝐴𝑙𝑘})‘𝑎)) = (𝐺𝑥))
4643, 45eqtrd 2833 . . . . . . 7 ((((𝜑𝑥 ∈ (Clsd‘𝐽)) ∧ 𝑎 ∈ (LIdeal‘𝑅)) ∧ ((𝑙 ∈ (LIdeal‘𝑅) ↦ {𝑘𝐴𝑙𝑘})‘𝑎) = 𝑥) → ((𝑙 ∈ (LIdeal‘𝑆) ↦ {𝑘𝐵𝑙𝑘})‘(𝐹𝑎)) = (𝐺𝑥))
4736, 38, 46rspcedvd 3574 . . . . . 6 ((((𝜑𝑥 ∈ (Clsd‘𝐽)) ∧ 𝑎 ∈ (LIdeal‘𝑅)) ∧ ((𝑙 ∈ (LIdeal‘𝑅) ↦ {𝑘𝐴𝑙𝑘})‘𝑎) = 𝑥) → ∃𝑏 ∈ (LIdeal‘𝑆)((𝑙 ∈ (LIdeal‘𝑆) ↦ {𝑘𝐵𝑙𝑘})‘𝑏) = (𝐺𝑥))
4810fvexi 6666 . . . . . . . . 9 𝐴 ∈ V
4948rabex 5202 . . . . . . . 8 {𝑘𝐴𝑗𝑘} ∈ V
5049, 42fnmpti 6468 . . . . . . 7 (𝑙 ∈ (LIdeal‘𝑅) ↦ {𝑘𝐴𝑙𝑘}) Fn (LIdeal‘𝑅)
51 simpr 488 . . . . . . . 8 ((𝜑𝑥 ∈ (Clsd‘𝐽)) → 𝑥 ∈ (Clsd‘𝐽))
527adantr 484 . . . . . . . . 9 ((𝜑𝑥 ∈ (Clsd‘𝐽)) → 𝑅 ∈ CRing)
538, 9, 10, 42zartopn 31291 . . . . . . . . . 10 (𝑅 ∈ CRing → (𝐽 ∈ (TopOn‘𝐴) ∧ ran (𝑙 ∈ (LIdeal‘𝑅) ↦ {𝑘𝐴𝑙𝑘}) = (Clsd‘𝐽)))
5453simprd 499 . . . . . . . . 9 (𝑅 ∈ CRing → ran (𝑙 ∈ (LIdeal‘𝑅) ↦ {𝑘𝐴𝑙𝑘}) = (Clsd‘𝐽))
5552, 54syl 17 . . . . . . . 8 ((𝜑𝑥 ∈ (Clsd‘𝐽)) → ran (𝑙 ∈ (LIdeal‘𝑅) ↦ {𝑘𝐴𝑙𝑘}) = (Clsd‘𝐽))
5651, 55eleqtrrd 2893 . . . . . . 7 ((𝜑𝑥 ∈ (Clsd‘𝐽)) → 𝑥 ∈ ran (𝑙 ∈ (LIdeal‘𝑅) ↦ {𝑘𝐴𝑙𝑘}))
57 fvelrnb 6708 . . . . . . . 8 ((𝑙 ∈ (LIdeal‘𝑅) ↦ {𝑘𝐴𝑙𝑘}) Fn (LIdeal‘𝑅) → (𝑥 ∈ ran (𝑙 ∈ (LIdeal‘𝑅) ↦ {𝑘𝐴𝑙𝑘}) ↔ ∃𝑎 ∈ (LIdeal‘𝑅)((𝑙 ∈ (LIdeal‘𝑅) ↦ {𝑘𝐴𝑙𝑘})‘𝑎) = 𝑥))
5857biimpa 480 . . . . . . 7 (((𝑙 ∈ (LIdeal‘𝑅) ↦ {𝑘𝐴𝑙𝑘}) Fn (LIdeal‘𝑅) ∧ 𝑥 ∈ ran (𝑙 ∈ (LIdeal‘𝑅) ↦ {𝑘𝐴𝑙𝑘})) → ∃𝑎 ∈ (LIdeal‘𝑅)((𝑙 ∈ (LIdeal‘𝑅) ↦ {𝑘𝐴𝑙𝑘})‘𝑎) = 𝑥)
5950, 56, 58sylancr 590 . . . . . 6 ((𝜑𝑥 ∈ (Clsd‘𝐽)) → ∃𝑎 ∈ (LIdeal‘𝑅)((𝑙 ∈ (LIdeal‘𝑅) ↦ {𝑘𝐴𝑙𝑘})‘𝑎) = 𝑥)
6047, 59r19.29a 3248 . . . . 5 ((𝜑𝑥 ∈ (Clsd‘𝐽)) → ∃𝑏 ∈ (LIdeal‘𝑆)((𝑙 ∈ (LIdeal‘𝑆) ↦ {𝑘𝐵𝑙𝑘})‘𝑏) = (𝐺𝑥))
61 fvelrnb 6708 . . . . . 6 ((𝑙 ∈ (LIdeal‘𝑆) ↦ {𝑘𝐵𝑙𝑘}) Fn (LIdeal‘𝑆) → ((𝐺𝑥) ∈ ran (𝑙 ∈ (LIdeal‘𝑆) ↦ {𝑘𝐵𝑙𝑘}) ↔ ∃𝑏 ∈ (LIdeal‘𝑆)((𝑙 ∈ (LIdeal‘𝑆) ↦ {𝑘𝐵𝑙𝑘})‘𝑏) = (𝐺𝑥)))
6261biimpar 481 . . . . 5 (((𝑙 ∈ (LIdeal‘𝑆) ↦ {𝑘𝐵𝑙𝑘}) Fn (LIdeal‘𝑆) ∧ ∃𝑏 ∈ (LIdeal‘𝑆)((𝑙 ∈ (LIdeal‘𝑆) ↦ {𝑘𝐵𝑙𝑘})‘𝑏) = (𝐺𝑥)) → (𝐺𝑥) ∈ ran (𝑙 ∈ (LIdeal‘𝑆) ↦ {𝑘𝐵𝑙𝑘}))
6327, 60, 62sylancr 590 . . . 4 ((𝜑𝑥 ∈ (Clsd‘𝐽)) → (𝐺𝑥) ∈ ran (𝑙 ∈ (LIdeal‘𝑆) ↦ {𝑘𝐵𝑙𝑘}))
642, 3, 4, 26zartopn 31291 . . . . . . 7 (𝑆 ∈ CRing → (𝐾 ∈ (TopOn‘𝐵) ∧ ran (𝑙 ∈ (LIdeal‘𝑆) ↦ {𝑘𝐵𝑙𝑘}) = (Clsd‘𝐾)))
6564simprd 499 . . . . . 6 (𝑆 ∈ CRing → ran (𝑙 ∈ (LIdeal‘𝑆) ↦ {𝑘𝐵𝑙𝑘}) = (Clsd‘𝐾))
661, 65syl 17 . . . . 5 (𝜑 → ran (𝑙 ∈ (LIdeal‘𝑆) ↦ {𝑘𝐵𝑙𝑘}) = (Clsd‘𝐾))
6766adantr 484 . . . 4 ((𝜑𝑥 ∈ (Clsd‘𝐽)) → ran (𝑙 ∈ (LIdeal‘𝑆) ↦ {𝑘𝐵𝑙𝑘}) = (Clsd‘𝐾))
6863, 67eleqtrd 2892 . . 3 ((𝜑𝑥 ∈ (Clsd‘𝐽)) → (𝐺𝑥) ∈ (Clsd‘𝐾))
6968ralrimiva 3149 . 2 (𝜑 → ∀𝑥 ∈ (Clsd‘𝐽)(𝐺𝑥) ∈ (Clsd‘𝐾))
70 iscncl 21912 . . 3 ((𝐾 ∈ (TopOn‘𝐵) ∧ 𝐽 ∈ (TopOn‘𝐴)) → (𝐺 ∈ (𝐾 Cn 𝐽) ↔ (𝐺:𝐵𝐴 ∧ ∀𝑥 ∈ (Clsd‘𝐽)(𝐺𝑥) ∈ (Clsd‘𝐾))))
7170biimpar 481 . 2 (((𝐾 ∈ (TopOn‘𝐵) ∧ 𝐽 ∈ (TopOn‘𝐴)) ∧ (𝐺:𝐵𝐴 ∧ ∀𝑥 ∈ (Clsd‘𝐽)(𝐺𝑥) ∈ (Clsd‘𝐾))) → 𝐺 ∈ (𝐾 Cn 𝐽))
726, 12, 21, 69, 71syl22anc 837 1 (𝜑𝐺 ∈ (𝐾 Cn 𝐽))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538   ∈ wcel 2111  ∀wral 3106  ∃wrex 3107  {crab 3110   ⊆ wss 3882   ↦ cmpt 5113  ◡ccnv 5521  ran crn 5523   “ cima 5525   Fn wfn 6324  ⟶wf 6325  ‘cfv 6329  (class class class)co 7142  Basecbs 16492  TopOpenctopn 16704  CRingccrg 19309   RingHom crh 19478  LIdealclidl 19953  TopOnctopon 21553  Clsdccld 21659   Cn ccn 21867  PrmIdealcprmidl 31076  Speccrspec 31278 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 2770  ax-rep 5157  ax-sep 5170  ax-nul 5177  ax-pow 5234  ax-pr 5298  ax-un 7451  ax-ac2 9889  ax-cnex 10597  ax-resscn 10598  ax-1cn 10599  ax-icn 10600  ax-addcl 10601  ax-addrcl 10602  ax-mulcl 10603  ax-mulrcl 10604  ax-mulcom 10605  ax-addass 10606  ax-mulass 10607  ax-distr 10608  ax-i2m1 10609  ax-1ne0 10610  ax-1rid 10611  ax-rnegex 10612  ax-rrecex 10613  ax-cnre 10614  ax-pre-lttri 10615  ax-pre-lttrn 10616  ax-pre-ltadd 10617  ax-pre-mulgt0 10618 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-nel 3092  df-ral 3111  df-rex 3112  df-reu 3113  df-rmo 3114  df-rab 3115  df-v 3443  df-sbc 3722  df-csb 3830  df-dif 3885  df-un 3887  df-in 3889  df-ss 3899  df-pss 3901  df-nul 4246  df-if 4428  df-pw 4501  df-sn 4528  df-pr 4530  df-tp 4532  df-op 4534  df-uni 4804  df-int 4842  df-iun 4886  df-iin 4887  df-br 5034  df-opab 5096  df-mpt 5114  df-tr 5140  df-id 5428  df-eprel 5433  df-po 5441  df-so 5442  df-fr 5481  df-se 5482  df-we 5483  df-xp 5528  df-rel 5529  df-cnv 5530  df-co 5531  df-dm 5532  df-rn 5533  df-res 5534  df-ima 5535  df-pred 6121  df-ord 6167  df-on 6168  df-lim 6169  df-suc 6170  df-iota 6288  df-fun 6331  df-fn 6332  df-f 6333  df-f1 6334  df-fo 6335  df-f1o 6336  df-fv 6337  df-isom 6338  df-riota 7100  df-ov 7145  df-oprab 7146  df-mpo 7147  df-rpss 7439  df-om 7571  df-1st 7681  df-2nd 7682  df-wrecs 7945  df-recs 8006  df-rdg 8044  df-1o 8100  df-oadd 8104  df-er 8287  df-map 8406  df-en 8508  df-dom 8509  df-sdom 8510  df-fin 8511  df-dju 9329  df-card 9367  df-ac 9542  df-pnf 10681  df-mnf 10682  df-xr 10683  df-ltxr 10684  df-le 10685  df-sub 10876  df-neg 10877  df-nn 11641  df-2 11703  df-3 11704  df-4 11705  df-5 11706  df-6 11707  df-7 11708  df-8 11709  df-9 11710  df-n0 11901  df-z 11987  df-dec 12104  df-uz 12249  df-fz 12903  df-struct 16494  df-ndx 16495  df-slot 16496  df-base 16498  df-sets 16499  df-ress 16500  df-plusg 16587  df-mulr 16588  df-sca 16590  df-vsca 16591  df-ip 16592  df-tset 16593  df-ple 16594  df-rest 16705  df-topn 16706  df-0g 16724  df-mre 16866  df-mgm 17861  df-sgrp 17910  df-mnd 17921  df-mhm 17965  df-submnd 17966  df-grp 18115  df-minusg 18116  df-sbg 18117  df-subg 18286  df-ghm 18366  df-cntz 18457  df-lsm 18771  df-cmn 18918  df-abl 18919  df-mgp 19251  df-ur 19263  df-ring 19310  df-cring 19311  df-rnghom 19481  df-subrg 19544  df-lmod 19647  df-lss 19715  df-lsp 19755  df-sra 19955  df-rgmod 19956  df-lidl 19957  df-rsp 19958  df-lpidl 20027  df-top 21537  df-topon 21554  df-cld 21662  df-cn 21870  df-prmidl 31077  df-mxidl 31098  df-idlsrg 31112  df-rspec 31279 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator