Definition df-dib

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 w . (Contributed by NM, 8-Dec-2013)

	Ref	Expression
Assertion	df-dib	⊢ DIsoB = ( 𝑘 ∈ V ↦ ( 𝑤 ∈ ( LHyp ‘ 𝑘 ) ↦ ( 𝑥 ∈ dom ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 ) ↦ ( ( ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑥 ) × { ( 𝑓 ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ↦ ( I ↾ ( Base ‘ 𝑘 ) ) ) } ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cdib	⊢ DIsoB
1		vk	⊢ 𝑘
2		cvv	⊢ V
3		vw	⊢ 𝑤
4		clh	⊢ LHyp
5	1	cv	⊢ 𝑘
6	5 4	cfv	⊢ ( LHyp ‘ 𝑘 )
7		vx	⊢ 𝑥
8		cdia	⊢ DIsoA
9	5 8	cfv	⊢ ( DIsoA ‘ 𝑘 )
10	3	cv	⊢ 𝑤
11	10 9	cfv	⊢ ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 )
12	11	cdm	⊢ dom ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 )
13	7	cv	⊢ 𝑥
14	13 11	cfv	⊢ ( ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑥 )
15		vf	⊢ 𝑓
16		cltrn	⊢ LTrn
17	5 16	cfv	⊢ ( LTrn ‘ 𝑘 )
18	10 17	cfv	⊢ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 )
19		cid	⊢ I
20		cbs	⊢ Base
21	5 20	cfv	⊢ ( Base ‘ 𝑘 )
22	19 21	cres	⊢ ( I ↾ ( Base ‘ 𝑘 ) )
23	15 18 22	cmpt	⊢ ( 𝑓 ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ↦ ( I ↾ ( Base ‘ 𝑘 ) ) )
24	23	csn	⊢ { ( 𝑓 ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ↦ ( I ↾ ( Base ‘ 𝑘 ) ) ) }
25	14 24	cxp	⊢ ( ( ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑥 ) × { ( 𝑓 ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ↦ ( I ↾ ( Base ‘ 𝑘 ) ) ) } )
26	7 12 25	cmpt	⊢ ( 𝑥 ∈ dom ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 ) ↦ ( ( ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑥 ) × { ( 𝑓 ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ↦ ( I ↾ ( Base ‘ 𝑘 ) ) ) } ) )
27	3 6 26	cmpt	⊢ ( 𝑤 ∈ ( LHyp ‘ 𝑘 ) ↦ ( 𝑥 ∈ dom ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 ) ↦ ( ( ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑥 ) × { ( 𝑓 ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ↦ ( I ↾ ( Base ‘ 𝑘 ) ) ) } ) ) )
28	1 2 27	cmpt	⊢ ( 𝑘 ∈ V ↦ ( 𝑤 ∈ ( LHyp ‘ 𝑘 ) ↦ ( 𝑥 ∈ dom ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 ) ↦ ( ( ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑥 ) × { ( 𝑓 ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ↦ ( I ↾ ( Base ‘ 𝑘 ) ) ) } ) ) ) )
29	0 28	wceq	⊢ DIsoB = ( 𝑘 ∈ V ↦ ( 𝑤 ∈ ( LHyp ‘ 𝑘 ) ↦ ( 𝑥 ∈ dom ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 ) ↦ ( ( ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑥 ) × { ( 𝑓 ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ↦ ( I ↾ ( Base ‘ 𝑘 ) ) ) } ) ) ) )