Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-dib Structured version   Visualization version   GIF version

Definition df-dib 38157
Description: Isomorphism B is isomorphism A extended with an extra dimension set to the zero vector component i.e. the zero endormorphism. Its domain is lattice elements less than or equal to the fiducial co-atom 𝑤. (Contributed by NM, 8-Dec-2013.)
Assertion
Ref Expression
df-dib DIsoB = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ dom ((DIsoA‘𝑘)‘𝑤) ↦ ((((DIsoA‘𝑘)‘𝑤)‘𝑥) × {(𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ ( I ↾ (Base‘𝑘)))}))))
Distinct variable group:   𝑤,𝑘,𝑥,𝑓

Detailed syntax breakdown of Definition df-dib
StepHypRef Expression
1 cdib 38156 . 2 class DIsoB
2 vk . . 3 setvar 𝑘
3 cvv 3495 . . 3 class V
4 vw . . . 4 setvar 𝑤
52cv 1527 . . . . 5 class 𝑘
6 clh 37002 . . . . 5 class LHyp
75, 6cfv 6349 . . . 4 class (LHyp‘𝑘)
8 vx . . . . 5 setvar 𝑥
94cv 1527 . . . . . . 7 class 𝑤
10 cdia 38046 . . . . . . . 8 class DIsoA
115, 10cfv 6349 . . . . . . 7 class (DIsoA‘𝑘)
129, 11cfv 6349 . . . . . 6 class ((DIsoA‘𝑘)‘𝑤)
1312cdm 5549 . . . . 5 class dom ((DIsoA‘𝑘)‘𝑤)
148cv 1527 . . . . . . 7 class 𝑥
1514, 12cfv 6349 . . . . . 6 class (((DIsoA‘𝑘)‘𝑤)‘𝑥)
16 vf . . . . . . . 8 setvar 𝑓
17 cltrn 37119 . . . . . . . . . 10 class LTrn
185, 17cfv 6349 . . . . . . . . 9 class (LTrn‘𝑘)
199, 18cfv 6349 . . . . . . . 8 class ((LTrn‘𝑘)‘𝑤)
20 cid 5453 . . . . . . . . 9 class I
21 cbs 16473 . . . . . . . . . 10 class Base
225, 21cfv 6349 . . . . . . . . 9 class (Base‘𝑘)
2320, 22cres 5551 . . . . . . . 8 class ( I ↾ (Base‘𝑘))
2416, 19, 23cmpt 5138 . . . . . . 7 class (𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ ( I ↾ (Base‘𝑘)))
2524csn 4559 . . . . . 6 class {(𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ ( I ↾ (Base‘𝑘)))}
2615, 25cxp 5547 . . . . 5 class ((((DIsoA‘𝑘)‘𝑤)‘𝑥) × {(𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ ( I ↾ (Base‘𝑘)))})
278, 13, 26cmpt 5138 . . . 4 class (𝑥 ∈ dom ((DIsoA‘𝑘)‘𝑤) ↦ ((((DIsoA‘𝑘)‘𝑤)‘𝑥) × {(𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ ( I ↾ (Base‘𝑘)))}))
284, 7, 27cmpt 5138 . . 3 class (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ dom ((DIsoA‘𝑘)‘𝑤) ↦ ((((DIsoA‘𝑘)‘𝑤)‘𝑥) × {(𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ ( I ↾ (Base‘𝑘)))})))
292, 3, 28cmpt 5138 . 2 class (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ dom ((DIsoA‘𝑘)‘𝑤) ↦ ((((DIsoA‘𝑘)‘𝑤)‘𝑥) × {(𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ ( I ↾ (Base‘𝑘)))}))))
301, 29wceq 1528 1 wff DIsoB = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ dom ((DIsoA‘𝑘)‘𝑤) ↦ ((((DIsoA‘𝑘)‘𝑤)‘𝑥) × {(𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ ( I ↾ (Base‘𝑘)))}))))
Colors of variables: wff setvar class
This definition is referenced by:  dibffval  38158
  Copyright terms: Public domain W3C validator