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 35446
 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 35445 . 2 class DIsoB
2 vk . . 3 setvar 𝑘
3 cvv 3173 . . 3 class V
4 vw . . . 4 setvar 𝑤
52cv 1474 . . . . 5 class 𝑘
6 clh 34288 . . . . 5 class LHyp
75, 6cfv 5804 . . . 4 class (LHyp‘𝑘)
8 vx . . . . 5 setvar 𝑥
94cv 1474 . . . . . . 7 class 𝑤
10 cdia 35335 . . . . . . . 8 class DIsoA
115, 10cfv 5804 . . . . . . 7 class (DIsoA‘𝑘)
129, 11cfv 5804 . . . . . 6 class ((DIsoA‘𝑘)‘𝑤)
1312cdm 5038 . . . . 5 class dom ((DIsoA‘𝑘)‘𝑤)
148cv 1474 . . . . . . 7 class 𝑥
1514, 12cfv 5804 . . . . . 6 class (((DIsoA‘𝑘)‘𝑤)‘𝑥)
16 vf . . . . . . . 8 setvar 𝑓
17 cltrn 34405 . . . . . . . . . 10 class LTrn
185, 17cfv 5804 . . . . . . . . 9 class (LTrn‘𝑘)
199, 18cfv 5804 . . . . . . . 8 class ((LTrn‘𝑘)‘𝑤)
20 cid 4948 . . . . . . . . 9 class I
21 cbs 15695 . . . . . . . . . 10 class Base
225, 21cfv 5804 . . . . . . . . 9 class (Base‘𝑘)
2320, 22cres 5040 . . . . . . . 8 class ( I ↾ (Base‘𝑘))
2416, 19, 23cmpt 4643 . . . . . . 7 class (𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ ( I ↾ (Base‘𝑘)))
2524csn 4125 . . . . . 6 class {(𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ ( I ↾ (Base‘𝑘)))}
2615, 25cxp 5036 . . . . 5 class ((((DIsoA‘𝑘)‘𝑤)‘𝑥) × {(𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ ( I ↾ (Base‘𝑘)))})
278, 13, 26cmpt 4643 . . . 4 class (𝑥 ∈ dom ((DIsoA‘𝑘)‘𝑤) ↦ ((((DIsoA‘𝑘)‘𝑤)‘𝑥) × {(𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ ( I ↾ (Base‘𝑘)))}))
284, 7, 27cmpt 4643 . . 3 class (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ dom ((DIsoA‘𝑘)‘𝑤) ↦ ((((DIsoA‘𝑘)‘𝑤)‘𝑥) × {(𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ ( I ↾ (Base‘𝑘)))})))
292, 3, 28cmpt 4643 . 2 class (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ dom ((DIsoA‘𝑘)‘𝑤) ↦ ((((DIsoA‘𝑘)‘𝑤)‘𝑥) × {(𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ ( I ↾ (Base‘𝑘)))}))))
301, 29wceq 1475 1 wff DIsoB = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ dom ((DIsoA‘𝑘)‘𝑤) ↦ ((((DIsoA‘𝑘)‘𝑤)‘𝑥) × {(𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ ( I ↾ (Base‘𝑘)))}))))
 Colors of variables: wff setvar class This definition is referenced by:  dibffval  35447
 Copyright terms: Public domain W3C validator