MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-ress Structured version   Visualization version   GIF version

Definition df-ress 17275
Description: Define a multifunction restriction operator for extensible structures, which can be used to turn statements about rings into statements about subrings, modules into submodules, etc. This definition knows nothing about individual structures and merely truncates the Base set while leaving operators alone; individual kinds of structures will need to handle this behavior, by ignoring operators' values outside the range (like Ring), defining a function using the base set and applying that (like TopGrp), or explicitly truncating the slot before use (like MetSp).

(Credit for this operator goes to Mario Carneiro.)

See ressbas 17280 for the altered base set, and resseqnbas 17287 (subrg0 20579, ressplusg 17334, subrg1 20582, ressmulr 17351) for the (un)altered other operations. (Contributed by Stefan O'Rear, 29-Nov-2014.)

Assertion
Ref Expression
df-ress s = (𝑤 ∈ V, 𝑥 ∈ V ↦ if((Base‘𝑤) ⊆ 𝑥, 𝑤, (𝑤 sSet ⟨(Base‘ndx), (𝑥 ∩ (Base‘𝑤))⟩)))
Distinct variable group:   𝑥,𝑤

Detailed syntax breakdown of Definition df-ress
StepHypRef Expression
1 cress 17274 . 2 class s
2 vw . . 3 setvar 𝑤
3 vx . . 3 setvar 𝑥
4 cvv 3480 . . 3 class V
52cv 1539 . . . . . 6 class 𝑤
6 cbs 17247 . . . . . 6 class Base
75, 6cfv 6561 . . . . 5 class (Base‘𝑤)
83cv 1539 . . . . 5 class 𝑥
97, 8wss 3951 . . . 4 wff (Base‘𝑤) ⊆ 𝑥
10 cnx 17230 . . . . . . 7 class ndx
1110, 6cfv 6561 . . . . . 6 class (Base‘ndx)
128, 7cin 3950 . . . . . 6 class (𝑥 ∩ (Base‘𝑤))
1311, 12cop 4632 . . . . 5 class ⟨(Base‘ndx), (𝑥 ∩ (Base‘𝑤))⟩
14 csts 17200 . . . . 5 class sSet
155, 13, 14co 7431 . . . 4 class (𝑤 sSet ⟨(Base‘ndx), (𝑥 ∩ (Base‘𝑤))⟩)
169, 5, 15cif 4525 . . 3 class if((Base‘𝑤) ⊆ 𝑥, 𝑤, (𝑤 sSet ⟨(Base‘ndx), (𝑥 ∩ (Base‘𝑤))⟩))
172, 3, 4, 4, 16cmpo 7433 . 2 class (𝑤 ∈ V, 𝑥 ∈ V ↦ if((Base‘𝑤) ⊆ 𝑥, 𝑤, (𝑤 sSet ⟨(Base‘ndx), (𝑥 ∩ (Base‘𝑤))⟩)))
181, 17wceq 1540 1 wff s = (𝑤 ∈ V, 𝑥 ∈ V ↦ if((Base‘𝑤) ⊆ 𝑥, 𝑤, (𝑤 sSet ⟨(Base‘ndx), (𝑥 ∩ (Base‘𝑤))⟩)))
Colors of variables: wff setvar class
This definition is referenced by:  reldmress  17276  ressval  17277
  Copyright terms: Public domain W3C validator