dibffval

Description: The partial isomorphism B for a lattice K . (Contributed by NM, 8-Dec-2013)

	Ref	Expression
Hypotheses	dibval.b	$⊢ B = {Base}_{K}$
	dibval.h	$⊢ H = LHyp (K)$
Assertion	dibffval	$⊢ K \in V \to DIsoB (K) = (w \in H ⟼ (x \in dom DIsoA (K) (w) ⟼ DIsoA (K) (w) (x) \times \{(f \in LTrn (K) (w) ⟼ {I ↾}_{B})\}))$

Proof

Step	Hyp	Ref	Expression
1		dibval.b	$⊢ B = {Base}_{K}$
2		dibval.h	$⊢ H = LHyp (K)$
3		elex	$⊢ K \in V \to K \in V$
4		fveq2	$⊢ k = K \to LHyp (k) = LHyp (K)$
5	4 2	eqtr4di	$⊢ k = K \to LHyp (k) = H$
6		fveq2	$⊢ k = K \to DIsoA (k) = DIsoA (K)$
7	6	fveq1d	$⊢ k = K \to DIsoA (k) (w) = DIsoA (K) (w)$
8	7	dmeqd	$⊢ k = K \to dom DIsoA (k) (w) = dom DIsoA (K) (w)$
9	7	fveq1d	$⊢ k = K \to DIsoA (k) (w) (x) = DIsoA (K) (w) (x)$
10		fveq2	$⊢ k = K \to LTrn (k) = LTrn (K)$
11	10	fveq1d	$⊢ k = K \to LTrn (k) (w) = LTrn (K) (w)$
12		fveq2	$⊢ k = K \to {Base}_{k} = {Base}_{K}$
13	12 1	eqtr4di	$⊢ k = K \to {Base}_{k} = B$
14	13	reseq2d	$⊢ k = K \to {I ↾}_{{Base}_{k}} = {I ↾}_{B}$
15	11 14	mpteq12dv	$⊢ k = K \to (f \in LTrn (k) (w) ⟼ {I ↾}_{{Base}_{k}}) = (f \in LTrn (K) (w) ⟼ {I ↾}_{B})$
16	15	sneqd	$⊢ k = K \to \{(f \in LTrn (k) (w) ⟼ {I ↾}_{{Base}_{k}})\} = \{(f \in LTrn (K) (w) ⟼ {I ↾}_{B})\}$
17	9 16	xpeq12d	$⊢ k = K \to DIsoA (k) (w) (x) \times \{(f \in LTrn (k) (w) ⟼ {I ↾}_{{Base}_{k}})\} = DIsoA (K) (w) (x) \times \{(f \in LTrn (K) (w) ⟼ {I ↾}_{B})\}$
18	8 17	mpteq12dv	$⊢ k = K \to (x \in dom DIsoA (k) (w) ⟼ DIsoA (k) (w) (x) \times \{(f \in LTrn (k) (w) ⟼ {I ↾}_{{Base}_{k}})\}) = (x \in dom DIsoA (K) (w) ⟼ DIsoA (K) (w) (x) \times \{(f \in LTrn (K) (w) ⟼ {I ↾}_{B})\})$
19	5 18	mpteq12dv	$⊢ k = K \to (w \in LHyp (k) ⟼ (x \in dom DIsoA (k) (w) ⟼ DIsoA (k) (w) (x) \times \{(f \in LTrn (k) (w) ⟼ {I ↾}_{{Base}_{k}})\})) = (w \in H ⟼ (x \in dom DIsoA (K) (w) ⟼ DIsoA (K) (w) (x) \times \{(f \in LTrn (K) (w) ⟼ {I ↾}_{B})\}))$
20		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}})\})))$
21	19 20 2	mptfvmpt	$⊢ K \in V \to DIsoB (K) = (w \in H ⟼ (x \in dom DIsoA (K) (w) ⟼ DIsoA (K) (w) (x) \times \{(f \in LTrn (K) (w) ⟼ {I ↾}_{B})\}))$
22	3 21	syl	$⊢ K \in V \to DIsoB (K) = (w \in H ⟼ (x \in dom DIsoA (K) (w) ⟼ DIsoA (K) (w) (x) \times \{(f \in LTrn (K) (w) ⟼ {I ↾}_{B})\}))$

Metamath Proof Explorer

Theorem dibffval

Proof