dibopelval3

Description: Member of the partial isomorphism B. (Contributed by NM, 3-Mar-2014)

	Ref	Expression
Hypotheses	dibval3.b	$⊢ B = {Base}_{K}$
	dibval3.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	dibval3.h	$⊢ H = LHyp (K)$
	dibval3.t	$⊢ T = LTrn (K) (W)$
	dibval3.r	$⊢ R = trL (K) (W)$
	dibval3.o	$⊢ \underset{˙}{0} = (g \in T ⟼ {I ↾}_{B})$
	dibval3.i	$⊢ I = DIsoB (K) (W)$
Assertion	dibopelval3	$⊢ ((K \in V \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W)) \to (⟨F, S⟩ \in I (X) \leftrightarrow ((F \in T \land R (F) \underset{˙}{\leq} X) \land S = \underset{˙}{0}))$

Step	Hyp	Ref	Expression
1		dibval3.b	$⊢ B = {Base}_{K}$
2		dibval3.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		dibval3.h	$⊢ H = LHyp (K)$
4		dibval3.t	$⊢ T = LTrn (K) (W)$
5		dibval3.r	$⊢ R = trL (K) (W)$
6		dibval3.o	$⊢ \underset{˙}{0} = (g \in T ⟼ {I ↾}_{B})$
7		dibval3.i	$⊢ I = DIsoB (K) (W)$
8		eqid	$⊢ DIsoA (K) (W) = DIsoA (K) (W)$
9	1 2 3 4 6 8 7	dibopelval2	$⊢ ((K \in V \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W)) \to (⟨F, S⟩ \in I (X) \leftrightarrow (F \in DIsoA (K) (W) (X) \land S = \underset{˙}{0}))$
10	1 2 3 4 5 8	diaelval	$⊢ ((K \in V \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W)) \to (F \in DIsoA (K) (W) (X) \leftrightarrow (F \in T \land R (F) \underset{˙}{\leq} X))$
11	10	anbi1d	$⊢ ((K \in V \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W)) \to ((F \in DIsoA (K) (W) (X) \land S = \underset{˙}{0}) \leftrightarrow ((F \in T \land R (F) \underset{˙}{\leq} X) \land S = \underset{˙}{0}))$
12	9 11	bitrd	$⊢ ((K \in V \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W)) \to (⟨F, S⟩ \in I (X) \leftrightarrow ((F \in T \land R (F) \underset{˙}{\leq} X) \land S = \underset{˙}{0}))$

Metamath Proof Explorer