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 = k ∈ V ⟼ w ∈ LHyp ⁡ k ⟼ x ∈ dom ⁡ DIsoA ⁡ k ⁡ w ⟼ DIsoA ⁡ k ⁡ w ⁡ x × f ∈ LTrn ⁡ k ⁡ w ⟼ I ↾ Base k

Detailed syntax breakdown

Step Hyp Ref Expression
0 cdib class DIsoB
1 vk setvar k
2 cvv class V
3 vw setvar w
4 clh class LHyp
5 1 cv setvar k
6 5 4 cfv class LHyp ⁡ k
7 vx setvar x
8 cdia class DIsoA
9 5 8 cfv class DIsoA ⁡ k
10 3 cv setvar w
11 10 9 cfv class DIsoA ⁡ k ⁡ w
12 11 cdm class dom ⁡ DIsoA ⁡ k ⁡ w
13 7 cv setvar x
14 13 11 cfv class DIsoA ⁡ k ⁡ w ⁡ x
15 vf setvar f
16 cltrn class LTrn
17 5 16 cfv class LTrn ⁡ k
18 10 17 cfv class LTrn ⁡ k ⁡ w
19 cid class I
20 cbs class Base
21 5 20 cfv class Base k
22 19 21 cres class I ↾ Base k
23 15 18 22 cmpt class f ∈ LTrn ⁡ k ⁡ w ⟼ I ↾ Base k
24 23 csn class f ∈ LTrn ⁡ k ⁡ w ⟼ I ↾ Base k
25 14 24 cxp class DIsoA ⁡ k ⁡ w ⁡ x × f ∈ LTrn ⁡ k ⁡ w ⟼ I ↾ Base k
26 7 12 25 cmpt class x ∈ dom ⁡ DIsoA ⁡ k ⁡ w ⟼ DIsoA ⁡ k ⁡ w ⁡ x × f ∈ LTrn ⁡ k ⁡ w ⟼ I ↾ Base k
27 3 6 26 cmpt class w ∈ LHyp ⁡ k ⟼ x ∈ dom ⁡ DIsoA ⁡ k ⁡ w ⟼ DIsoA ⁡ k ⁡ w ⁡ x × f ∈ LTrn ⁡ k ⁡ w ⟼ I ↾ Base k
28 1 2 27 cmpt class k ∈ V ⟼ w ∈ LHyp ⁡ k ⟼ x ∈ dom ⁡ DIsoA ⁡ k ⁡ w ⟼ DIsoA ⁡ k ⁡ w ⁡ x × f ∈ LTrn ⁡ k ⁡ w ⟼ I ↾ Base k
29 0 28 wceq wff DIsoB = k ∈ V ⟼ w ∈ LHyp ⁡ k ⟼ x ∈ dom ⁡ DIsoA ⁡ k ⁡ w ⟼ DIsoA ⁡ k ⁡ w ⁡ x × f ∈ LTrn ⁡ k ⁡ w ⟼ I ↾ Base k