Definition df-dib 40010

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

Step	Hyp	Ref	Expression
1		cdib 40009	. 2 class DIsoB
2		vk	. . 3 setvar 𝑘
3		cvv 3475	. . 3 class V
4		vw	. . . 4 setvar 𝑤
5	2	cv 1541	. . . . 5 class 𝑘
6		clh 38855	. . . . 5 class LHyp
7	5, 6	cfv 6544	. . . 4 class (LHyp‘𝑘)
8		vx	. . . . 5 setvar 𝑥
9	4	cv 1541	. . . . . . 7 class 𝑤
10		cdia 39899	. . . . . . . 8 class DIsoA
11	5, 10	cfv 6544	. . . . . . 7 class (DIsoA‘𝑘)
12	9, 11	cfv 6544	. . . . . 6 class ((DIsoA‘𝑘)‘𝑤)
13	12	cdm 5677	. . . . 5 class dom ((DIsoA‘𝑘)‘𝑤)
14	8	cv 1541	. . . . . . 7 class 𝑥
15	14, 12	cfv 6544	. . . . . 6 class (((DIsoA‘𝑘)‘𝑤)‘𝑥)
16		vf	. . . . . . . 8 setvar 𝑓
17		cltrn 38972	. . . . . . . . . 10 class LTrn
18	5, 17	cfv 6544	. . . . . . . . 9 class (LTrn‘𝑘)
19	9, 18	cfv 6544	. . . . . . . 8 class ((LTrn‘𝑘)‘𝑤)
20		cid 5574	. . . . . . . . 9 class I
21		cbs 17144	. . . . . . . . . 10 class Base
22	5, 21	cfv 6544	. . . . . . . . 9 class (Base‘𝑘)
23	20, 22	cres 5679	. . . . . . . 8 class ( I ↾ (Base‘𝑘))
24	16, 19, 23	cmpt 5232	. . . . . . 7 class (𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ ( I ↾ (Base‘𝑘)))
25	24	csn 4629	. . . . . 6 class {(𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ ( I ↾ (Base‘𝑘)))}
26	15, 25	cxp 5675	. . . . 5 class ((((DIsoA‘𝑘)‘𝑤)‘𝑥) × {(𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ ( I ↾ (Base‘𝑘)))})
27	8, 13, 26	cmpt 5232	. . . 4 class (𝑥 ∈ dom ((DIsoA‘𝑘)‘𝑤) ↦ ((((DIsoA‘𝑘)‘𝑤)‘𝑥) × {(𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ ( I ↾ (Base‘𝑘)))}))
28	4, 7, 27	cmpt 5232	. . 3 class (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ dom ((DIsoA‘𝑘)‘𝑤) ↦ ((((DIsoA‘𝑘)‘𝑤)‘𝑥) × {(𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ ( I ↾ (Base‘𝑘)))})))
29	2, 3, 28	cmpt 5232	. 2 class (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ dom ((DIsoA‘𝑘)‘𝑤) ↦ ((((DIsoA‘𝑘)‘𝑤)‘𝑥) × {(𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ ( I ↾ (Base‘𝑘)))}))))
30	1, 29	wceq 1542	1 wff DIsoB = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ dom ((DIsoA‘𝑘)‘𝑤) ↦ ((((DIsoA‘𝑘)‘𝑤)‘𝑥) × {(𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ ( I ↾ (Base‘𝑘)))}))))

This definition is referenced by:  dibffval  40011