dibval2

Description: Value of the partial isomorphism B. (Contributed by NM, 18-Jan-2014)

	Ref	Expression
Hypotheses	dibval2.b	$⊢ B = {Base}_{K}$
	dibval2.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	dibval2.h	$⊢ H = LHyp (K)$
	dibval2.t	$⊢ T = LTrn (K) (W)$
	dibval2.o	$⊢ \underset{˙}{0} = (f \in T ⟼ {I ↾}_{B})$
	dibval2.j	$⊢ J = DIsoA (K) (W)$
	dibval2.i	$⊢ I = DIsoB (K) (W)$
Assertion	dibval2	$⊢ ((K \in V \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W)) \to I (X) = J (X) \times \{\underset{˙}{0}\}$

Step	Hyp	Ref	Expression
1		dibval2.b	$⊢ B = {Base}_{K}$
2		dibval2.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		dibval2.h	$⊢ H = LHyp (K)$
4		dibval2.t	$⊢ T = LTrn (K) (W)$
5		dibval2.o	$⊢ \underset{˙}{0} = (f \in T ⟼ {I ↾}_{B})$
6		dibval2.j	$⊢ J = DIsoA (K) (W)$
7		dibval2.i	$⊢ I = DIsoB (K) (W)$
8	1 2 3 6	diaeldm	$⊢ (K \in V \land W \in H) \to (X \in dom J \leftrightarrow (X \in B \land X \underset{˙}{\leq} W))$
9	8	biimpar	$⊢ ((K \in V \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W)) \to X \in dom J$
10	1 3 4 5 6 7	dibval	$⊢ ((K \in V \land W \in H) \land X \in dom J) \to I (X) = J (X) \times \{\underset{˙}{0}\}$
11	9 10	syldan	$⊢ ((K \in V \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W)) \to I (X) = J (X) \times \{\underset{˙}{0}\}$

Metamath Proof Explorer