dihord5b

Description: Part of proof that isomorphism H is order-preserving. TODO: eliminate 3ad2ant1; combine with other way to have one lhpmcvr2 . (Contributed by NM, 7-Mar-2014)

	Ref	Expression
Hypotheses	dihord3.b	$⊢ B = {Base}_{K}$
	dihord3.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	dihord3.h	$⊢ H = LHyp (K)$
	dihord3.i	$⊢ I = DIsoH (K) (W)$
Assertion	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)$

Proof

Step	Hyp	Ref	Expression
1		dihord3.b	$⊢ B = {Base}_{K}$
2		dihord3.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		dihord3.h	$⊢ H = LHyp (K)$
4		dihord3.i	$⊢ I = DIsoH (K) (W)$
5		simpl1	$⊢ (((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 (K \in HL \land W \in H)$
6		simpl3	$⊢ (((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 (Y \in B \land \neg Y \underset{˙}{\leq} W)$
7		eqid	$⊢ join (K) = join (K)$
8		eqid	$⊢ meet (K) = meet (K)$
9		eqid	$⊢ Atoms (K) = Atoms (K)$
10	1 2 7 8 9 3	lhpmcvr2	$⊢ ((K \in HL \land W \in H) \land (Y \in B \land \neg Y \underset{˙}{\leq} W)) \to \exists r \in Atoms (K) (\neg r \underset{˙}{\leq} W \land r join (K) (Y meet (K) W) = Y)$
11	5 6 10	syl2anc	$⊢ (((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 \exists r \in Atoms (K) (\neg r \underset{˙}{\leq} W \land r join (K) (Y meet (K) W) = Y)$
12		simp1r	$⊢ ((((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) \land (r \in Atoms (K) \land \neg r \underset{˙}{\leq} W) \land r join (K) (Y meet (K) W) = Y) \to X \underset{˙}{\leq} Y$
13		simpl2r	$⊢ (((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 X \underset{˙}{\leq} W$
14	13	3ad2ant1	$⊢ ((((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) \land (r \in Atoms (K) \land \neg r \underset{˙}{\leq} W) \land r join (K) (Y meet (K) W) = Y) \to X \underset{˙}{\leq} W$
15		simpl1l	$⊢ (((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 K \in HL$
16	15	3ad2ant1	$⊢ ((((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) \land (r \in Atoms (K) \land \neg r \underset{˙}{\leq} W) \land r join (K) (Y meet (K) W) = Y) \to K \in HL$
17	16	hllatd	$⊢ ((((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) \land (r \in Atoms (K) \land \neg r \underset{˙}{\leq} W) \land r join (K) (Y meet (K) W) = Y) \to K \in Lat$
18		simpl2l	$⊢ (((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 X \in B$
19	18	3ad2ant1	$⊢ ((((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) \land (r \in Atoms (K) \land \neg r \underset{˙}{\leq} W) \land r join (K) (Y meet (K) W) = Y) \to X \in B$
20		simpl3l	$⊢ (((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 Y \in B$
21	20	3ad2ant1	$⊢ ((((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) \land (r \in Atoms (K) \land \neg r \underset{˙}{\leq} W) \land r join (K) (Y meet (K) W) = Y) \to Y \in B$
22		simpl1r	$⊢ (((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 W \in H$
23	22	3ad2ant1	$⊢ ((((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) \land (r \in Atoms (K) \land \neg r \underset{˙}{\leq} W) \land r join (K) (Y meet (K) W) = Y) \to W \in H$
24	1 3	lhpbase	$⊢ W \in H \to W \in B$
25	23 24	syl	$⊢ ((((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) \land (r \in Atoms (K) \land \neg r \underset{˙}{\leq} W) \land r join (K) (Y meet (K) W) = Y) \to W \in B$
26	1 2 8	latlem12	$⊢ (K \in Lat \land (X \in B \land Y \in B \land W \in B)) \to ((X \underset{˙}{\leq} Y \land X \underset{˙}{\leq} W) \leftrightarrow X \underset{˙}{\leq} (Y meet (K) W))$
27	17 19 21 25 26	syl13anc	$⊢ ((((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) \land (r \in Atoms (K) \land \neg r \underset{˙}{\leq} W) \land r join (K) (Y meet (K) W) = Y) \to ((X \underset{˙}{\leq} Y \land X \underset{˙}{\leq} W) \leftrightarrow X \underset{˙}{\leq} (Y meet (K) W))$
28	12 14 27	mpbi2and	$⊢ ((((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) \land (r \in Atoms (K) \land \neg r \underset{˙}{\leq} W) \land r join (K) (Y meet (K) W) = Y) \to X \underset{˙}{\leq} (Y meet (K) W)$
29		simp1l1	$⊢ ((((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) \land (r \in Atoms (K) \land \neg r \underset{˙}{\leq} W) \land r join (K) (Y meet (K) W) = Y) \to (K \in HL \land W \in H)$
30		simp1l2	$⊢ ((((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) \land (r \in Atoms (K) \land \neg r \underset{˙}{\leq} W) \land r join (K) (Y meet (K) W) = Y) \to (X \in B \land X \underset{˙}{\leq} W)$
31	1 8	latmcl	$⊢ (K \in Lat \land Y \in B \land W \in B) \to Y meet (K) W \in B$
32	17 21 25 31	syl3anc	$⊢ ((((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) \land (r \in Atoms (K) \land \neg r \underset{˙}{\leq} W) \land r join (K) (Y meet (K) W) = Y) \to Y meet (K) W \in B$
33	1 2 8	latmle2	$⊢ (K \in Lat \land Y \in B \land W \in B) \to (Y meet (K) W) \underset{˙}{\leq} W$
34	17 21 25 33	syl3anc	$⊢ ((((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) \land (r \in Atoms (K) \land \neg r \underset{˙}{\leq} W) \land r join (K) (Y meet (K) W) = Y) \to (Y meet (K) W) \underset{˙}{\leq} W$
35		eqid	$⊢ DIsoB (K) (W) = DIsoB (K) (W)$
36	1 2 3 35	dibord	$⊢ ((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W) \land (Y meet (K) W \in B \land (Y meet (K) W) \underset{˙}{\leq} W)) \to (DIsoB (K) (W) (X) \subseteq DIsoB (K) (W) (Y meet (K) W) \leftrightarrow X \underset{˙}{\leq} (Y meet (K) W))$
37	29 30 32 34 36	syl112anc	$⊢ ((((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) \land (r \in Atoms (K) \land \neg r \underset{˙}{\leq} W) \land r join (K) (Y meet (K) W) = Y) \to (DIsoB (K) (W) (X) \subseteq DIsoB (K) (W) (Y meet (K) W) \leftrightarrow X \underset{˙}{\leq} (Y meet (K) W))$
38	28 37	mpbird	$⊢ ((((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) \land (r \in Atoms (K) \land \neg r \underset{˙}{\leq} W) \land r join (K) (Y meet (K) W) = Y) \to DIsoB (K) (W) (X) \subseteq DIsoB (K) (W) (Y meet (K) W)$
39		eqid	$⊢ DVecH (K) (W) = DVecH (K) (W)$
40	3 39 29	dvhlmod	$⊢ ((((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) \land (r \in Atoms (K) \land \neg r \underset{˙}{\leq} W) \land r join (K) (Y meet (K) W) = Y) \to DVecH (K) (W) \in LMod$
41		eqid	$⊢ LSubSp (DVecH (K) (W)) = LSubSp (DVecH (K) (W))$
42	41	lsssssubg	$⊢ DVecH (K) (W) \in LMod \to LSubSp (DVecH (K) (W)) \subseteq SubGrp (DVecH (K) (W))$
43	40 42	syl	$⊢ ((((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) \land (r \in Atoms (K) \land \neg r \underset{˙}{\leq} W) \land r join (K) (Y meet (K) W) = Y) \to LSubSp (DVecH (K) (W)) \subseteq SubGrp (DVecH (K) (W))$
44		simp2	$⊢ ((((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) \land (r \in Atoms (K) \land \neg r \underset{˙}{\leq} W) \land r join (K) (Y meet (K) W) = Y) \to (r \in Atoms (K) \land \neg r \underset{˙}{\leq} W)$
45		eqid	$⊢ DIsoC (K) (W) = DIsoC (K) (W)$
46	2 9 3 39 45 41	diclss	$⊢ ((K \in HL \land W \in H) \land (r \in Atoms (K) \land \neg r \underset{˙}{\leq} W)) \to DIsoC (K) (W) (r) \in LSubSp (DVecH (K) (W))$
47	29 44 46	syl2anc	$⊢ ((((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) \land (r \in Atoms (K) \land \neg r \underset{˙}{\leq} W) \land r join (K) (Y meet (K) W) = Y) \to DIsoC (K) (W) (r) \in LSubSp (DVecH (K) (W))$
48	43 47	sseldd	$⊢ ((((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) \land (r \in Atoms (K) \land \neg r \underset{˙}{\leq} W) \land r join (K) (Y meet (K) W) = Y) \to DIsoC (K) (W) (r) \in SubGrp (DVecH (K) (W))$
49	1 2 3 39 35 41	diblss	$⊢ ((K \in HL \land W \in H) \land (Y meet (K) W \in B \land (Y meet (K) W) \underset{˙}{\leq} W)) \to DIsoB (K) (W) (Y meet (K) W) \in LSubSp (DVecH (K) (W))$
50	29 32 34 49	syl12anc	$⊢ ((((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) \land (r \in Atoms (K) \land \neg r \underset{˙}{\leq} W) \land r join (K) (Y meet (K) W) = Y) \to DIsoB (K) (W) (Y meet (K) W) \in LSubSp (DVecH (K) (W))$
51	43 50	sseldd	$⊢ ((((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) \land (r \in Atoms (K) \land \neg r \underset{˙}{\leq} W) \land r join (K) (Y meet (K) W) = Y) \to DIsoB (K) (W) (Y meet (K) W) \in SubGrp (DVecH (K) (W))$
52		eqid	$⊢ LSSum (DVecH (K) (W)) = LSSum (DVecH (K) (W))$
53	52	lsmub2	$⊢ (DIsoC (K) (W) (r) \in SubGrp (DVecH (K) (W)) \land DIsoB (K) (W) (Y meet (K) W) \in SubGrp (DVecH (K) (W))) \to DIsoB (K) (W) (Y meet (K) W) \subseteq DIsoC (K) (W) (r) LSSum (DVecH (K) (W)) DIsoB (K) (W) (Y meet (K) W)$
54	48 51 53	syl2anc	$⊢ ((((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) \land (r \in Atoms (K) \land \neg r \underset{˙}{\leq} W) \land r join (K) (Y meet (K) W) = Y) \to DIsoB (K) (W) (Y meet (K) W) \subseteq DIsoC (K) (W) (r) LSSum (DVecH (K) (W)) DIsoB (K) (W) (Y meet (K) W)$
55	38 54	sstrd	$⊢ ((((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) \land (r \in Atoms (K) \land \neg r \underset{˙}{\leq} W) \land r join (K) (Y meet (K) W) = Y) \to DIsoB (K) (W) (X) \subseteq DIsoC (K) (W) (r) LSSum (DVecH (K) (W)) DIsoB (K) (W) (Y meet (K) W)$
56	1 2 3 4 35	dihvalb	$⊢ ((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W)) \to I (X) = DIsoB (K) (W) (X)$
57	29 30 56	syl2anc	$⊢ ((((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) \land (r \in Atoms (K) \land \neg r \underset{˙}{\leq} W) \land r join (K) (Y meet (K) W) = Y) \to I (X) = DIsoB (K) (W) (X)$
58		simp1l3	$⊢ ((((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) \land (r \in Atoms (K) \land \neg r \underset{˙}{\leq} W) \land r join (K) (Y meet (K) W) = Y) \to (Y \in B \land \neg Y \underset{˙}{\leq} W)$
59		simp3	$⊢ ((((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) \land (r \in Atoms (K) \land \neg r \underset{˙}{\leq} W) \land r join (K) (Y meet (K) W) = Y) \to r join (K) (Y meet (K) W) = Y$
60	1 2 7 8 9 3 4 35 45 39 52	dihvalcq	$⊢ ((K \in HL \land W \in H) \land (Y \in B \land \neg Y \underset{˙}{\leq} W) \land ((r \in Atoms (K) \land \neg r \underset{˙}{\leq} W) \land r join (K) (Y meet (K) W) = Y)) \to I (Y) = DIsoC (K) (W) (r) LSSum (DVecH (K) (W)) DIsoB (K) (W) (Y meet (K) W)$
61	29 58 44 59 60	syl112anc	$⊢ ((((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) \land (r \in Atoms (K) \land \neg r \underset{˙}{\leq} W) \land r join (K) (Y meet (K) W) = Y) \to I (Y) = DIsoC (K) (W) (r) LSSum (DVecH (K) (W)) DIsoB (K) (W) (Y meet (K) W)$
62	55 57 61	3sstr4d	$⊢ ((((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) \land (r \in Atoms (K) \land \neg r \underset{˙}{\leq} W) \land r join (K) (Y meet (K) W) = Y) \to I (X) \subseteq I (Y)$
63	62	3exp	$⊢ (((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 ((r \in Atoms (K) \land \neg r \underset{˙}{\leq} W) \to (r join (K) (Y meet (K) W) = Y \to I (X) \subseteq I (Y)))$
64	63	expd	$⊢ (((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 (r \in Atoms (K) \to (\neg r \underset{˙}{\leq} W \to (r join (K) (Y meet (K) W) = Y \to I (X) \subseteq I (Y))))$
65	64	imp4a	$⊢ (((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 (r \in Atoms (K) \to ((\neg r \underset{˙}{\leq} W \land r join (K) (Y meet (K) W) = Y) \to I (X) \subseteq I (Y)))$
66	65	rexlimdv	$⊢ (((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 (\exists r \in Atoms (K) (\neg r \underset{˙}{\leq} W \land r join (K) (Y meet (K) W) = Y) \to I (X) \subseteq I (Y))$
67	11 66	mpd	$⊢ (((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)$

Metamath Proof Explorer

Theorem dihord5b

Proof