Metamath Proof Explorer

Theorem dia11N

Description: The partial isomorphism A for a lattice K is one-to-one in the region under co-atom W . Part of Lemma M of Crawley p. 120 line 28. (Contributed by NM, 25-Nov-2013) (New usage is discouraged.)

		Ref	Expression
	Hypotheses	dia11.b	$⊢ B = {Base}_{K}$
		dia11.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
		dia11.h	$⊢ H = LHyp (K)$
		dia11.i	$⊢ I = DIsoA (K) (W)$
	Assertion	dia11N	$⊢ ((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \to (I (X) = I (Y) \leftrightarrow X = Y)$

Proof

Step	Hyp	Ref	Expression
1		dia11.b	$⊢ B = {Base}_{K}$
2		dia11.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		dia11.h	$⊢ H = LHyp (K)$
4		dia11.i	$⊢ I = DIsoA (K) (W)$
5		eqss	$⊢ I (X) = I (Y) \leftrightarrow (I (X) \subseteq I (Y) \land I (Y) \subseteq I (X))$
6	1 2 3 4	diaord	$⊢ ((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \to (I (X) \subseteq I (Y) \leftrightarrow X \underset{˙}{\leq} Y)$
7	1 2 3 4	diaord	$⊢ ((K \in HL \land W \in H) \land (Y \in B \land Y \underset{˙}{\leq} W) \land (X \in B \land X \underset{˙}{\leq} W)) \to (I (Y) \subseteq I (X) \leftrightarrow Y \underset{˙}{\leq} X)$
8	7	3com23	$⊢ ((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \to (I (Y) \subseteq I (X) \leftrightarrow Y \underset{˙}{\leq} X)$
9	6 8	anbi12d	$⊢ ((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \to ((I (X) \subseteq I (Y) \land I (Y) \subseteq I (X)) \leftrightarrow (X \underset{˙}{\leq} Y \land Y \underset{˙}{\leq} X))$
10		simp1l	$⊢ ((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \to K \in HL$
11	10	hllatd	$⊢ ((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \to K \in Lat$
12		simp2l	$⊢ ((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \to X \in B$
13		simp3l	$⊢ ((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \to Y \in B$
14	1 2	latasymb	$⊢ (K \in Lat \land X \in B \land Y \in B) \to ((X \underset{˙}{\leq} Y \land Y \underset{˙}{\leq} X) \leftrightarrow X = Y)$
15	11 12 13 14	syl3anc	$⊢ ((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \to ((X \underset{˙}{\leq} Y \land Y \underset{˙}{\leq} X) \leftrightarrow X = Y)$
16	9 15	bitrd	$⊢ ((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \to ((I (X) \subseteq I (Y) \land I (Y) \subseteq I (X)) \leftrightarrow X = Y)$
17	5 16	bitrid	$⊢ ((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \to (I (X) = I (Y) \leftrightarrow X = Y)$