dih11

Description: The isomorphism H is one-to-one. Part of proof after Lemma N of Crawley p. 122 line 6. (Contributed by NM, 7-Mar-2014)

	Ref	Expression
Hypotheses	dih11.b	$⊢ B = {Base}_{K}$
	dih11.h	$⊢ H = LHyp (K)$
	dih11.i	$⊢ I = DIsoH (K) (W)$
Assertion	dih11	$⊢ ((K \in HL \land W \in H) \land X \in B \land Y \in B) \to (I (X) = I (Y) \leftrightarrow X = Y)$

Step	Hyp	Ref	Expression
1		dih11.b	$⊢ B = {Base}_{K}$
2		dih11.h	$⊢ H = LHyp (K)$
3		dih11.i	$⊢ I = DIsoH (K) (W)$
4		eqss	$⊢ I (X) = I (Y) \leftrightarrow (I (X) \subseteq I (Y) \land I (Y) \subseteq I (X))$
5		eqid	$⊢ \leq_{K} = \leq_{K}$
6	1 5 2 3	dihord	$⊢ ((K \in HL \land W \in H) \land X \in B \land Y \in B) \to (I (X) \subseteq I (Y) \leftrightarrow X \leq_{K} Y)$
7	1 5 2 3	dihord	$⊢ ((K \in HL \land W \in H) \land Y \in B \land X \in B) \to (I (Y) \subseteq I (X) \leftrightarrow Y \leq_{K} X)$
8	7	3com23	$⊢ ((K \in HL \land W \in H) \land X \in B \land Y \in B) \to (I (Y) \subseteq I (X) \leftrightarrow Y \leq_{K} X)$
9	6 8	anbi12d	$⊢ ((K \in HL \land W \in H) \land X \in B \land Y \in B) \to ((I (X) \subseteq I (Y) \land I (Y) \subseteq I (X)) \leftrightarrow (X \leq_{K} Y \land Y \leq_{K} X))$
10		simp1l	$⊢ ((K \in HL \land W \in H) \land X \in B \land Y \in B) \to K \in HL$
11	10	hllatd	$⊢ ((K \in HL \land W \in H) \land X \in B \land Y \in B) \to K \in Lat$
12	1 5	latasymb	$⊢ (K \in Lat \land X \in B \land Y \in B) \to ((X \leq_{K} Y \land Y \leq_{K} X) \leftrightarrow X = Y)$
13	11 12	syld3an1	$⊢ ((K \in HL \land W \in H) \land X \in B \land Y \in B) \to ((X \leq_{K} Y \land Y \leq_{K} X) \leftrightarrow X = Y)$
14	9 13	bitrd	$⊢ ((K \in HL \land W \in H) \land X \in B \land Y \in B) \to ((I (X) \subseteq I (Y) \land I (Y) \subseteq I (X)) \leftrightarrow X = Y)$
15	4 14	bitrid	$⊢ ((K \in HL \land W \in H) \land X \in B \land Y \in B) \to (I (X) = I (Y) \leftrightarrow X = Y)$

Metamath Proof Explorer