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 16487
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 16550 for the altered base set, and resslem 16553 (subrg0 19539, ressplusg 16608, subrg1 19542, ressmulr 16621) 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 16480 . 2 class s
2 vw . . 3 setvar 𝑤
3 vx . . 3 setvar 𝑥
4 cvv 3444 . . 3 class V
52cv 1537 . . . . . 6 class 𝑤
6 cbs 16479 . . . . . 6 class Base
75, 6cfv 6328 . . . . 5 class (Base‘𝑤)
83cv 1537 . . . . 5 class 𝑥
97, 8wss 3884 . . . 4 wff (Base‘𝑤) ⊆ 𝑥
10 cnx 16476 . . . . . . 7 class ndx
1110, 6cfv 6328 . . . . . 6 class (Base‘ndx)
128, 7cin 3883 . . . . . 6 class (𝑥 ∩ (Base‘𝑤))
1311, 12cop 4534 . . . . 5 class ⟨(Base‘ndx), (𝑥 ∩ (Base‘𝑤))⟩
14 csts 16477 . . . . 5 class sSet
155, 13, 14co 7139 . . . 4 class (𝑤 sSet ⟨(Base‘ndx), (𝑥 ∩ (Base‘𝑤))⟩)
169, 5, 15cif 4428 . . 3 class if((Base‘𝑤) ⊆ 𝑥, 𝑤, (𝑤 sSet ⟨(Base‘ndx), (𝑥 ∩ (Base‘𝑤))⟩))
172, 3, 4, 4, 16cmpo 7141 . 2 class (𝑤 ∈ V, 𝑥 ∈ V ↦ if((Base‘𝑤) ⊆ 𝑥, 𝑤, (𝑤 sSet ⟨(Base‘ndx), (𝑥 ∩ (Base‘𝑤))⟩)))
181, 17wceq 1538 1 wff s = (𝑤 ∈ V, 𝑥 ∈ V ↦ if((Base‘𝑤) ⊆ 𝑥, 𝑤, (𝑤 sSet ⟨(Base‘ndx), (𝑥 ∩ (Base‘𝑤))⟩)))
Colors of variables: wff setvar class
This definition is referenced by:  reldmress  16546  ressval  16547
  Copyright terms: Public domain W3C validator