dihord

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

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

Proof

Step	Hyp	Ref	Expression
1		dihord.b	$⊢ B = {Base}_{K}$
2		dihord.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		dihord.h	$⊢ H = LHyp (K)$
4		dihord.i	$⊢ I = DIsoH (K) (W)$
5		simpl1	$⊢ (((K \in HL \land W \in H) \land X \in B \land Y \in B) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W)) \to (K \in HL \land W \in H)$
6		simpl2	$⊢ (((K \in HL \land W \in H) \land X \in B \land Y \in B) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W)) \to X \in B$
7		simprl	$⊢ (((K \in HL \land W \in H) \land X \in B \land Y \in B) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W)) \to X \underset{˙}{\leq} W$
8		simpl3	$⊢ (((K \in HL \land W \in H) \land X \in B \land Y \in B) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W)) \to Y \in B$
9		simprr	$⊢ (((K \in HL \land W \in H) \land X \in B \land Y \in B) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W)) \to Y \underset{˙}{\leq} W$
10	1 2 3 4	dihord3	$⊢ ((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)$
11	5 6 7 8 9 10	syl122anc	$⊢ (((K \in HL \land W \in H) \land X \in B \land Y \in B) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W)) \to (I (X) \subseteq I (Y) \leftrightarrow X \underset{˙}{\leq} Y)$
12		simpl1	$⊢ (((K \in HL \land W \in H) \land X \in B \land Y \in B) \land (X \underset{˙}{\leq} W \land \neg Y \underset{˙}{\leq} W)) \to (K \in HL \land W \in H)$
13		simpl2	$⊢ (((K \in HL \land W \in H) \land X \in B \land Y \in B) \land (X \underset{˙}{\leq} W \land \neg Y \underset{˙}{\leq} W)) \to X \in B$
14		simprl	$⊢ (((K \in HL \land W \in H) \land X \in B \land Y \in B) \land (X \underset{˙}{\leq} W \land \neg Y \underset{˙}{\leq} W)) \to X \underset{˙}{\leq} W$
15		simpl3	$⊢ (((K \in HL \land W \in H) \land X \in B \land Y \in B) \land (X \underset{˙}{\leq} W \land \neg Y \underset{˙}{\leq} W)) \to Y \in B$
16		simprr	$⊢ (((K \in HL \land W \in H) \land X \in B \land Y \in B) \land (X \underset{˙}{\leq} W \land \neg Y \underset{˙}{\leq} W)) \to \neg Y \underset{˙}{\leq} W$
17	1 2 3 4	dihord5a	$⊢ (((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W) \land (Y \in B \land \neg Y \underset{˙}{\leq} W)) \land I (X) \subseteq I (Y)) \to X \underset{˙}{\leq} Y$
18	1 2 3 4	dihord5b	$⊢ (((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W) \land (Y \in B \land \neg Y \underset{˙}{\leq} W)) \land X \underset{˙}{\leq} Y) \to I (X) \subseteq I (Y)$
19	17 18	impbida	$⊢ ((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W) \land (Y \in B \land \neg Y \underset{˙}{\leq} W)) \to (I (X) \subseteq I (Y) \leftrightarrow X \underset{˙}{\leq} Y)$
20	12 13 14 15 16 19	syl122anc	$⊢ (((K \in HL \land W \in H) \land X \in B \land Y \in B) \land (X \underset{˙}{\leq} W \land \neg Y \underset{˙}{\leq} W)) \to (I (X) \subseteq I (Y) \leftrightarrow X \underset{˙}{\leq} Y)$
21		simpl1	$⊢ (((K \in HL \land W \in H) \land X \in B \land Y \in B) \land (\neg X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W)) \to (K \in HL \land W \in H)$
22		simpl2	$⊢ (((K \in HL \land W \in H) \land X \in B \land Y \in B) \land (\neg X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W)) \to X \in B$
23		simprl	$⊢ (((K \in HL \land W \in H) \land X \in B \land Y \in B) \land (\neg X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W)) \to \neg X \underset{˙}{\leq} W$
24		simpl3	$⊢ (((K \in HL \land W \in H) \land X \in B \land Y \in B) \land (\neg X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W)) \to Y \in B$
25		simprr	$⊢ (((K \in HL \land W \in H) \land X \in B \land Y \in B) \land (\neg X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W)) \to Y \underset{˙}{\leq} W$
26	1 2 3 4	dihord6a	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \land I (X) \subseteq I (Y)) \to X \underset{˙}{\leq} Y$
27	1 2 3 4	dihord6b	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \land X \underset{˙}{\leq} Y) \to I (X) \subseteq I (Y)$
28	26 27	impbida	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \to (I (X) \subseteq I (Y) \leftrightarrow X \underset{˙}{\leq} Y)$
29	21 22 23 24 25 28	syl122anc	$⊢ (((K \in HL \land W \in H) \land X \in B \land Y \in B) \land (\neg X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W)) \to (I (X) \subseteq I (Y) \leftrightarrow X \underset{˙}{\leq} Y)$
30		simpl1	$⊢ (((K \in HL \land W \in H) \land X \in B \land Y \in B) \land (\neg X \underset{˙}{\leq} W \land \neg Y \underset{˙}{\leq} W)) \to (K \in HL \land W \in H)$
31		simpl2	$⊢ (((K \in HL \land W \in H) \land X \in B \land Y \in B) \land (\neg X \underset{˙}{\leq} W \land \neg Y \underset{˙}{\leq} W)) \to X \in B$
32		simprl	$⊢ (((K \in HL \land W \in H) \land X \in B \land Y \in B) \land (\neg X \underset{˙}{\leq} W \land \neg Y \underset{˙}{\leq} W)) \to \neg X \underset{˙}{\leq} W$
33		simpl3	$⊢ (((K \in HL \land W \in H) \land X \in B \land Y \in B) \land (\neg X \underset{˙}{\leq} W \land \neg Y \underset{˙}{\leq} W)) \to Y \in B$
34		simprr	$⊢ (((K \in HL \land W \in H) \land X \in B \land Y \in B) \land (\neg X \underset{˙}{\leq} W \land \neg Y \underset{˙}{\leq} W)) \to \neg Y \underset{˙}{\leq} W$
35	1 2 3 4	dihord4	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Y \in B \land \neg Y \underset{˙}{\leq} W)) \to (I (X) \subseteq I (Y) \leftrightarrow X \underset{˙}{\leq} Y)$
36	30 31 32 33 34 35	syl122anc	$⊢ (((K \in HL \land W \in H) \land X \in B \land Y \in B) \land (\neg X \underset{˙}{\leq} W \land \neg Y \underset{˙}{\leq} W)) \to (I (X) \subseteq I (Y) \leftrightarrow X \underset{˙}{\leq} Y)$
37	11 20 29 36	4casesdan	$⊢ ((K \in HL \land W \in H) \land X \in B \land Y \in B) \to (I (X) \subseteq I (Y) \leftrightarrow X \underset{˙}{\leq} Y)$

Metamath Proof Explorer

Theorem dihord

Proof