This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ‘ 𝑘 ) ) ) } ) ) ) )