dihord6apre

Description: Part of proof that isomorphism H is order-preserving . (Contributed by NM, 7-Mar-2014)

	Ref	Expression
Hypotheses	dihord6apre.b	$⊢ B = {Base}_{K}$
	dihord6apre.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	dihord6apre.a	$⊢ A = Atoms (K)$
	dihord6apre.h	$⊢ H = LHyp (K)$
	dihord6apre.p	$⊢ P = oc (K) (W)$
	dihord6apre.o	$⊢ O = (h \in T ⟼ {I ↾}_{B})$
	dihord6apre.t	$⊢ T = LTrn (K) (W)$
	dihord6apre.e	$⊢ E = TEndo (K) (W)$
	dihord6apre.i	$⊢ I = DIsoH (K) (W)$
	dihord6apre.u	$⊢ U = DVecH (K) (W)$
	dihord6apre.s	$⊢ \underset{˙}{\oplus} = LSSum (U)$
	dihord6apre.g	$⊢ G = (ι h \in T \| h (P) = q)$
Assertion	dihord6apre	$⊢ (((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$

Proof

Step	Hyp	Ref	Expression
1		dihord6apre.b	$⊢ B = {Base}_{K}$
2		dihord6apre.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		dihord6apre.a	$⊢ A = Atoms (K)$
4		dihord6apre.h	$⊢ H = LHyp (K)$
5		dihord6apre.p	$⊢ P = oc (K) (W)$
6		dihord6apre.o	$⊢ O = (h \in T ⟼ {I ↾}_{B})$
7		dihord6apre.t	$⊢ T = LTrn (K) (W)$
8		dihord6apre.e	$⊢ E = TEndo (K) (W)$
9		dihord6apre.i	$⊢ I = DIsoH (K) (W)$
10		dihord6apre.u	$⊢ U = DVecH (K) (W)$
11		dihord6apre.s	$⊢ \underset{˙}{\oplus} = LSSum (U)$
12		dihord6apre.g	$⊢ G = (ι h \in T \| h (P) = q)$
13	1 4 7 8 6	tendo1ne0	$⊢ (K \in HL \land W \in H) \to {I ↾}_{T} \neq O$
14	13	3ad2ant1	$⊢ ((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 ↾}_{T} \neq O$
15	14	neneqd	$⊢ ((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 \neg {I ↾}_{T} = O$
16		eqid	$⊢ join (K) = join (K)$
17		eqid	$⊢ meet (K) = meet (K)$
18	1 2 16 17 3 4	lhpmcvr2	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W)) \to \exists q \in A (\neg q \underset{˙}{\leq} W \land q join (K) (X meet (K) W) = X)$
19	18	3adant3	$⊢ ((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 \exists q \in A (\neg q \underset{˙}{\leq} W \land q join (K) (X meet (K) W) = X)$
20		simpl1	$⊢ (((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 ((q \in A \land \neg q \underset{˙}{\leq} W) \land q join (K) (X meet (K) W) = X)) \to (K \in HL \land W \in H)$
21		simpl2	$⊢ (((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 ((q \in A \land \neg q \underset{˙}{\leq} W) \land q join (K) (X meet (K) W) = X)) \to (X \in B \land \neg X \underset{˙}{\leq} W)$
22		simpr	$⊢ (((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 ((q \in A \land \neg q \underset{˙}{\leq} W) \land q join (K) (X meet (K) W) = X)) \to ((q \in A \land \neg q \underset{˙}{\leq} W) \land q join (K) (X meet (K) W) = X)$
23		eqid	$⊢ DIsoB (K) (W) = DIsoB (K) (W)$
24		eqid	$⊢ DIsoC (K) (W) = DIsoC (K) (W)$
25	1 2 16 17 3 4 9 23 24 10 11	dihvalcq	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((q \in A \land \neg q \underset{˙}{\leq} W) \land q join (K) (X meet (K) W) = X)) \to I (X) = DIsoC (K) (W) (q) \underset{˙}{\oplus} DIsoB (K) (W) (X meet (K) W)$
26	20 21 22 25	syl3anc	$⊢ (((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 ((q \in A \land \neg q \underset{˙}{\leq} W) \land q join (K) (X meet (K) W) = X)) \to I (X) = DIsoC (K) (W) (q) \underset{˙}{\oplus} DIsoB (K) (W) (X meet (K) W)$
27		simpl3	$⊢ (((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 ((q \in A \land \neg q \underset{˙}{\leq} W) \land q join (K) (X meet (K) W) = X)) \to (Y \in B \land Y \underset{˙}{\leq} W)$
28	1 2 4 9 23	dihvalb	$⊢ ((K \in HL \land W \in H) \land (Y \in B \land Y \underset{˙}{\leq} W)) \to I (Y) = DIsoB (K) (W) (Y)$
29	20 27 28	syl2anc	$⊢ (((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 ((q \in A \land \neg q \underset{˙}{\leq} W) \land q join (K) (X meet (K) W) = X)) \to I (Y) = DIsoB (K) (W) (Y)$
30	26 29	sseq12d	$⊢ (((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 ((q \in A \land \neg q \underset{˙}{\leq} W) \land q join (K) (X meet (K) W) = X)) \to (I (X) \subseteq I (Y) \leftrightarrow DIsoC (K) (W) (q) \underset{˙}{\oplus} DIsoB (K) (W) (X meet (K) W) \subseteq DIsoB (K) (W) (Y))$
31	4 10 20	dvhlmod	$⊢ (((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 ((q \in A \land \neg q \underset{˙}{\leq} W) \land q join (K) (X meet (K) W) = X)) \to U \in LMod$
32		eqid	$⊢ LSubSp (U) = LSubSp (U)$
33	32	lsssssubg	$⊢ U \in LMod \to LSubSp (U) \subseteq SubGrp (U)$
34	31 33	syl	$⊢ (((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 ((q \in A \land \neg q \underset{˙}{\leq} W) \land q join (K) (X meet (K) W) = X)) \to LSubSp (U) \subseteq SubGrp (U)$
35		simprl	$⊢ (((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 ((q \in A \land \neg q \underset{˙}{\leq} W) \land q join (K) (X meet (K) W) = X)) \to (q \in A \land \neg q \underset{˙}{\leq} W)$
36	2 3 4 10 24 32	diclss	$⊢ ((K \in HL \land W \in H) \land (q \in A \land \neg q \underset{˙}{\leq} W)) \to DIsoC (K) (W) (q) \in LSubSp (U)$
37	20 35 36	syl2anc	$⊢ (((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 ((q \in A \land \neg q \underset{˙}{\leq} W) \land q join (K) (X meet (K) W) = X)) \to DIsoC (K) (W) (q) \in LSubSp (U)$
38	34 37	sseldd	$⊢ (((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 ((q \in A \land \neg q \underset{˙}{\leq} W) \land q join (K) (X meet (K) W) = X)) \to DIsoC (K) (W) (q) \in SubGrp (U)$
39		simpl1l	$⊢ (((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 ((q \in A \land \neg q \underset{˙}{\leq} W) \land q join (K) (X meet (K) W) = X)) \to K \in HL$
40	39	hllatd	$⊢ (((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 ((q \in A \land \neg q \underset{˙}{\leq} W) \land q join (K) (X meet (K) W) = X)) \to K \in Lat$
41		simpl2l	$⊢ (((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 ((q \in A \land \neg q \underset{˙}{\leq} W) \land q join (K) (X meet (K) W) = X)) \to X \in B$
42		simpl1r	$⊢ (((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 ((q \in A \land \neg q \underset{˙}{\leq} W) \land q join (K) (X meet (K) W) = X)) \to W \in H$
43	1 4	lhpbase	$⊢ W \in H \to W \in B$
44	42 43	syl	$⊢ (((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 ((q \in A \land \neg q \underset{˙}{\leq} W) \land q join (K) (X meet (K) W) = X)) \to W \in B$
45	1 17	latmcl	$⊢ (K \in Lat \land X \in B \land W \in B) \to X meet (K) W \in B$
46	40 41 44 45	syl3anc	$⊢ (((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 ((q \in A \land \neg q \underset{˙}{\leq} W) \land q join (K) (X meet (K) W) = X)) \to X meet (K) W \in B$
47	1 2 17	latmle2	$⊢ (K \in Lat \land X \in B \land W \in B) \to (X meet (K) W) \underset{˙}{\leq} W$
48	40 41 44 47	syl3anc	$⊢ (((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 ((q \in A \land \neg q \underset{˙}{\leq} W) \land q join (K) (X meet (K) W) = X)) \to (X meet (K) W) \underset{˙}{\leq} W$
49	1 2 4 10 23 32	diblss	$⊢ ((K \in HL \land W \in H) \land (X meet (K) W \in B \land (X meet (K) W) \underset{˙}{\leq} W)) \to DIsoB (K) (W) (X meet (K) W) \in LSubSp (U)$
50	20 46 48 49	syl12anc	$⊢ (((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 ((q \in A \land \neg q \underset{˙}{\leq} W) \land q join (K) (X meet (K) W) = X)) \to DIsoB (K) (W) (X meet (K) W) \in LSubSp (U)$
51	34 50	sseldd	$⊢ (((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 ((q \in A \land \neg q \underset{˙}{\leq} W) \land q join (K) (X meet (K) W) = X)) \to DIsoB (K) (W) (X meet (K) W) \in SubGrp (U)$
52	11	lsmub1	$⊢ (DIsoC (K) (W) (q) \in SubGrp (U) \land DIsoB (K) (W) (X meet (K) W) \in SubGrp (U)) \to DIsoC (K) (W) (q) \subseteq DIsoC (K) (W) (q) \underset{˙}{\oplus} DIsoB (K) (W) (X meet (K) W)$
53	38 51 52	syl2anc	$⊢ (((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 ((q \in A \land \neg q \underset{˙}{\leq} W) \land q join (K) (X meet (K) W) = X)) \to DIsoC (K) (W) (q) \subseteq DIsoC (K) (W) (q) \underset{˙}{\oplus} DIsoB (K) (W) (X meet (K) W)$
54		sstr	$⊢ (DIsoC (K) (W) (q) \subseteq DIsoC (K) (W) (q) \underset{˙}{\oplus} DIsoB (K) (W) (X meet (K) W) \land DIsoC (K) (W) (q) \underset{˙}{\oplus} DIsoB (K) (W) (X meet (K) W) \subseteq DIsoB (K) (W) (Y)) \to DIsoC (K) (W) (q) \subseteq DIsoB (K) (W) (Y)$
55		eqidd	$⊢ (((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 ((q \in A \land \neg q \underset{˙}{\leq} W) \land q join (K) (X meet (K) W) = X)) \to ({I ↾}_{T}) (G) = ({I ↾}_{T}) (G)$
56	4 7 8	tendoidcl	$⊢ (K \in HL \land W \in H) \to {I ↾}_{T} \in E$
57	20 56	syl	$⊢ (((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 ((q \in A \land \neg q \underset{˙}{\leq} W) \land q join (K) (X meet (K) W) = X)) \to {I ↾}_{T} \in E$
58		fvex	$⊢ ({I ↾}_{T}) (G) \in V$
59	7	fvexi	$⊢ T \in V$
60		resiexg	$⊢ T \in V \to {I ↾}_{T} \in V$
61	59 60	ax-mp	$⊢ {I ↾}_{T} \in V$
62	2 3 4 5 7 8 24 12 58 61	dicopelval2	$⊢ ((K \in HL \land W \in H) \land (q \in A \land \neg q \underset{˙}{\leq} W)) \to (⟨({I ↾}_{T}) (G), {I ↾}_{T}⟩ \in DIsoC (K) (W) (q) \leftrightarrow (({I ↾}_{T}) (G) = ({I ↾}_{T}) (G) \land {I ↾}_{T} \in E))$
63	20 35 62	syl2anc	$⊢ (((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 ((q \in A \land \neg q \underset{˙}{\leq} W) \land q join (K) (X meet (K) W) = X)) \to (⟨({I ↾}_{T}) (G), {I ↾}_{T}⟩ \in DIsoC (K) (W) (q) \leftrightarrow (({I ↾}_{T}) (G) = ({I ↾}_{T}) (G) \land {I ↾}_{T} \in E))$
64	55 57 63	mpbir2and	$⊢ (((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 ((q \in A \land \neg q \underset{˙}{\leq} W) \land q join (K) (X meet (K) W) = X)) \to ⟨({I ↾}_{T}) (G), {I ↾}_{T}⟩ \in DIsoC (K) (W) (q)$
65		ssel2	$⊢ (DIsoC (K) (W) (q) \subseteq DIsoB (K) (W) (Y) \land ⟨({I ↾}_{T}) (G), {I ↾}_{T}⟩ \in DIsoC (K) (W) (q)) \to ⟨({I ↾}_{T}) (G), {I ↾}_{T}⟩ \in DIsoB (K) (W) (Y)$
66		eqid	$⊢ DIsoA (K) (W) = DIsoA (K) (W)$
67	1 2 4 7 6 66 23	dibopelval2	$⊢ ((K \in HL \land W \in H) \land (Y \in B \land Y \underset{˙}{\leq} W)) \to (⟨({I ↾}_{T}) (G), {I ↾}_{T}⟩ \in DIsoB (K) (W) (Y) \leftrightarrow (({I ↾}_{T}) (G) \in DIsoA (K) (W) (Y) \land {I ↾}_{T} = O))$
68	20 27 67	syl2anc	$⊢ (((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 ((q \in A \land \neg q \underset{˙}{\leq} W) \land q join (K) (X meet (K) W) = X)) \to (⟨({I ↾}_{T}) (G), {I ↾}_{T}⟩ \in DIsoB (K) (W) (Y) \leftrightarrow (({I ↾}_{T}) (G) \in DIsoA (K) (W) (Y) \land {I ↾}_{T} = O))$
69		simpr	$⊢ (({I ↾}_{T}) (G) \in DIsoA (K) (W) (Y) \land {I ↾}_{T} = O) \to {I ↾}_{T} = O$
70	68 69	syl6bi	$⊢ (((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 ((q \in A \land \neg q \underset{˙}{\leq} W) \land q join (K) (X meet (K) W) = X)) \to (⟨({I ↾}_{T}) (G), {I ↾}_{T}⟩ \in DIsoB (K) (W) (Y) \to {I ↾}_{T} = O)$
71	65 70	syl5	$⊢ (((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 ((q \in A \land \neg q \underset{˙}{\leq} W) \land q join (K) (X meet (K) W) = X)) \to ((DIsoC (K) (W) (q) \subseteq DIsoB (K) (W) (Y) \land ⟨({I ↾}_{T}) (G), {I ↾}_{T}⟩ \in DIsoC (K) (W) (q)) \to {I ↾}_{T} = O)$
72	64 71	mpan2d	$⊢ (((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 ((q \in A \land \neg q \underset{˙}{\leq} W) \land q join (K) (X meet (K) W) = X)) \to (DIsoC (K) (W) (q) \subseteq DIsoB (K) (W) (Y) \to {I ↾}_{T} = O)$
73	54 72	syl5	$⊢ (((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 ((q \in A \land \neg q \underset{˙}{\leq} W) \land q join (K) (X meet (K) W) = X)) \to ((DIsoC (K) (W) (q) \subseteq DIsoC (K) (W) (q) \underset{˙}{\oplus} DIsoB (K) (W) (X meet (K) W) \land DIsoC (K) (W) (q) \underset{˙}{\oplus} DIsoB (K) (W) (X meet (K) W) \subseteq DIsoB (K) (W) (Y)) \to {I ↾}_{T} = O)$
74	53 73	mpand	$⊢ (((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 ((q \in A \land \neg q \underset{˙}{\leq} W) \land q join (K) (X meet (K) W) = X)) \to (DIsoC (K) (W) (q) \underset{˙}{\oplus} DIsoB (K) (W) (X meet (K) W) \subseteq DIsoB (K) (W) (Y) \to {I ↾}_{T} = O)$
75	30 74	sylbid	$⊢ (((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 ((q \in A \land \neg q \underset{˙}{\leq} W) \land q join (K) (X meet (K) W) = X)) \to (I (X) \subseteq I (Y) \to {I ↾}_{T} = O)$
76	75	exp44	$⊢ ((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 (q \in A \to (\neg q \underset{˙}{\leq} W \to (q join (K) (X meet (K) W) = X \to (I (X) \subseteq I (Y) \to {I ↾}_{T} = O))))$
77	76	imp4a	$⊢ ((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 (q \in A \to ((\neg q \underset{˙}{\leq} W \land q join (K) (X meet (K) W) = X) \to (I (X) \subseteq I (Y) \to {I ↾}_{T} = O)))$
78	77	rexlimdv	$⊢ ((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 (\exists q \in A (\neg q \underset{˙}{\leq} W \land q join (K) (X meet (K) W) = X) \to (I (X) \subseteq I (Y) \to {I ↾}_{T} = O))$
79	19 78	mpd	$⊢ ((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) \to {I ↾}_{T} = O)$
80	15 79	mtod	$⊢ ((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 \neg I (X) \subseteq I (Y)$
81	80	pm2.21d	$⊢ ((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) \to X \underset{˙}{\leq} Y)$
82	81	imp	$⊢ (((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$

Metamath Proof Explorer

Theorem dihord6apre

Proof