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 \in V ⟼ (w \in LHyp (k) ⟼ (x \in dom DIsoA (k) (w) ⟼ DIsoA (k) (w) (x) \times \{(f \in 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 \in LTrn (k) (w) ⟼ {I ↾}_{{Base}_{k}})$
24	23	csn	$class \{(f \in LTrn (k) (w) ⟼ {I ↾}_{{Base}_{k}})\}$
25	14 24	cxp	$class (DIsoA (k) (w) (x) \times \{(f \in LTrn (k) (w) ⟼ {I ↾}_{{Base}_{k}})\})$
26	7 12 25	cmpt	$class (x \in dom DIsoA (k) (w) ⟼ DIsoA (k) (w) (x) \times \{(f \in LTrn (k) (w) ⟼ {I ↾}_{{Base}_{k}})\})$
27	3 6 26	cmpt	$class (w \in LHyp (k) ⟼ (x \in dom DIsoA (k) (w) ⟼ DIsoA (k) (w) (x) \times \{(f \in LTrn (k) (w) ⟼ {I ↾}_{{Base}_{k}})\}))$
28	1 2 27	cmpt	$class (k \in V ⟼ (w \in LHyp (k) ⟼ (x \in dom DIsoA (k) (w) ⟼ DIsoA (k) (w) (x) \times \{(f \in LTrn (k) (w) ⟼ {I ↾}_{{Base}_{k}})\})))$
29	0 28	wceq	$wff DIsoB = (k \in V ⟼ (w \in LHyp (k) ⟼ (x \in dom DIsoA (k) (w) ⟼ DIsoA (k) (w) (x) \times \{(f \in LTrn (k) (w) ⟼ {I ↾}_{{Base}_{k}})\})))$

Metamath Proof Explorer

Definition df-dib

Detailed syntax breakdown