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 35908
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 35907 . 2 class DIsoB
2 vk . . 3 setvar 𝑘
3 cvv 3186 . . 3 class V
4 vw . . . 4 setvar 𝑤
52cv 1479 . . . . 5 class 𝑘
6 clh 34750 . . . . 5 class LHyp
75, 6cfv 5847 . . . 4 class (LHyp‘𝑘)
8 vx . . . . 5 setvar 𝑥
94cv 1479 . . . . . . 7 class 𝑤
10 cdia 35797 . . . . . . . 8 class DIsoA
115, 10cfv 5847 . . . . . . 7 class (DIsoA‘𝑘)
129, 11cfv 5847 . . . . . 6 class ((DIsoA‘𝑘)‘𝑤)
1312cdm 5074 . . . . 5 class dom ((DIsoA‘𝑘)‘𝑤)
148cv 1479 . . . . . . 7 class 𝑥
1514, 12cfv 5847 . . . . . 6 class (((DIsoA‘𝑘)‘𝑤)‘𝑥)
16 vf . . . . . . . 8 setvar 𝑓
17 cltrn 34867 . . . . . . . . . 10 class LTrn
185, 17cfv 5847 . . . . . . . . 9 class (LTrn‘𝑘)
199, 18cfv 5847 . . . . . . . 8 class ((LTrn‘𝑘)‘𝑤)
20 cid 4984 . . . . . . . . 9 class I
21 cbs 15781 . . . . . . . . . 10 class Base
225, 21cfv 5847 . . . . . . . . 9 class (Base‘𝑘)
2320, 22cres 5076 . . . . . . . 8 class ( I ↾ (Base‘𝑘))
2416, 19, 23cmpt 4673 . . . . . . 7 class (𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ ( I ↾ (Base‘𝑘)))
2524csn 4148 . . . . . 6 class {(𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ ( I ↾ (Base‘𝑘)))}
2615, 25cxp 5072 . . . . 5 class ((((DIsoA‘𝑘)‘𝑤)‘𝑥) × {(𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ ( I ↾ (Base‘𝑘)))})
278, 13, 26cmpt 4673 . . . 4 class (𝑥 ∈ dom ((DIsoA‘𝑘)‘𝑤) ↦ ((((DIsoA‘𝑘)‘𝑤)‘𝑥) × {(𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ ( I ↾ (Base‘𝑘)))}))
284, 7, 27cmpt 4673 . . 3 class (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ dom ((DIsoA‘𝑘)‘𝑤) ↦ ((((DIsoA‘𝑘)‘𝑤)‘𝑥) × {(𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ ( I ↾ (Base‘𝑘)))})))
292, 3, 28cmpt 4673 . 2 class (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ dom ((DIsoA‘𝑘)‘𝑤) ↦ ((((DIsoA‘𝑘)‘𝑤)‘𝑥) × {(𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ ( I ↾ (Base‘𝑘)))}))))
301, 29wceq 1480 1 wff DIsoB = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ dom ((DIsoA‘𝑘)‘𝑤) ↦ ((((DIsoA‘𝑘)‘𝑤)‘𝑥) × {(𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ ( I ↾ (Base‘𝑘)))}))))
Colors of variables: wff setvar class
This definition is referenced by:  dibffval  35909
  Copyright terms: Public domain W3C validator