dibval

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)$
	dibval.t	$⊢ T = LTrn (K) (W)$
	dibval.o	$⊢ \underset{˙}{0} = (f \in T ⟼ {I ↾}_{B})$
	dibval.j	$⊢ J = DIsoA (K) (W)$
	dibval.i	$⊢ I = DIsoB (K) (W)$
Assertion	dibval	$⊢ ((K \in V \land W \in H) \land X \in dom J) \to I (X) = J (X) \times \{\underset{˙}{0}\}$

Step	Hyp	Ref	Expression
1		dibval.b	$⊢ B = {Base}_{K}$
2		dibval.h	$⊢ H = LHyp (K)$
3		dibval.t	$⊢ T = LTrn (K) (W)$
4		dibval.o	$⊢ \underset{˙}{0} = (f \in T ⟼ {I ↾}_{B})$
5		dibval.j	$⊢ J = DIsoA (K) (W)$
6		dibval.i	$⊢ I = DIsoB (K) (W)$
7	1 2 3 4 5 6	dibfval	$⊢ (K \in V \land W \in H) \to I = (x \in dom J ⟼ J (x) \times \{\underset{˙}{0}\})$
8	7	adantr	$⊢ ((K \in V \land W \in H) \land X \in dom J) \to I = (x \in dom J ⟼ J (x) \times \{\underset{˙}{0}\})$
9	8	fveq1d	$⊢ ((K \in V \land W \in H) \land X \in dom J) \to I (X) = (x \in dom J ⟼ J (x) \times \{\underset{˙}{0}\}) (X)$
10		fveq2	$⊢ x = X \to J (x) = J (X)$
11	10	xpeq1d	$⊢ x = X \to J (x) \times \{\underset{˙}{0}\} = J (X) \times \{\underset{˙}{0}\}$
12		eqid	$⊢ (x \in dom J ⟼ J (x) \times \{\underset{˙}{0}\}) = (x \in dom J ⟼ J (x) \times \{\underset{˙}{0}\})$
13		fvex	$⊢ J (X) \in V$
14		snex	$⊢ \{\underset{˙}{0}\} \in V$
15	13 14	xpex	$⊢ J (X) \times \{\underset{˙}{0}\} \in V$
16	11 12 15	fvmpt	$⊢ X \in dom J \to (x \in dom J ⟼ J (x) \times \{\underset{˙}{0}\}) (X) = J (X) \times \{\underset{˙}{0}\}$
17	16	adantl	$⊢ ((K \in V \land W \in H) \land X \in dom J) \to (x \in dom J ⟼ J (x) \times \{\underset{˙}{0}\}) (X) = J (X) \times \{\underset{˙}{0}\}$
18	9 17	eqtrd	$⊢ ((K \in V \land W \in H) \land X \in dom J) \to I (X) = J (X) \times \{\underset{˙}{0}\}$

Metamath Proof Explorer