dihord5apre

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

	Ref	Expression
Hypotheses	dihord5apre.b	$⊢ B = {Base}_{K}$
	dihord5apre.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	dihord5apre.h	$⊢ H = LHyp (K)$
	dihord5apre.j	$⊢ \underset{˙}{\lor} = join (K)$
	dihord5apre.m	$⊢ \underset{˙}{\land} = meet (K)$
	dihord5apre.a	$⊢ A = Atoms (K)$
	dihord5apre.u	$⊢ U = DVecH (K) (W)$
	dihord5apre.s	$⊢ \underset{˙}{\oplus} = LSSum (U)$
	dihord5apre.i	$⊢ I = DIsoH (K) (W)$
Assertion	dihord5apre	$⊢ (((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$

Proof

Step	Hyp	Ref	Expression
1		dihord5apre.b	$⊢ B = {Base}_{K}$
2		dihord5apre.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		dihord5apre.h	$⊢ H = LHyp (K)$
4		dihord5apre.j	$⊢ \underset{˙}{\lor} = join (K)$
5		dihord5apre.m	$⊢ \underset{˙}{\land} = meet (K)$
6		dihord5apre.a	$⊢ A = Atoms (K)$
7		dihord5apre.u	$⊢ U = DVecH (K) (W)$
8		dihord5apre.s	$⊢ \underset{˙}{\oplus} = LSSum (U)$
9		dihord5apre.i	$⊢ I = DIsoH (K) (W)$
10		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 I (X) \subseteq I (Y)) \to (K \in HL \land W \in H)$
11		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 I (X) \subseteq I (Y)) \to (Y \in B \land \neg Y \underset{˙}{\leq} W)$
12	1 2 4 5 6 3	lhpmcvr2	$⊢ ((K \in HL \land W \in H) \land (Y \in B \land \neg Y \underset{˙}{\leq} W)) \to \exists r \in A (\neg r \underset{˙}{\leq} W \land r \underset{˙}{\lor} (Y \underset{˙}{\land} W) = Y)$
13	10 11 12	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 I (X) \subseteq I (Y)) \to \exists r \in A (\neg r \underset{˙}{\leq} W \land r \underset{˙}{\lor} (Y \underset{˙}{\land} W) = Y)$
14		simp11l	$⊢ (((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) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land r \underset{˙}{\lor} (Y \underset{˙}{\land} W) = Y)) \to K \in HL$
15	14	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 I (X) \subseteq I (Y) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land r \underset{˙}{\lor} (Y \underset{˙}{\land} W) = Y)) \to K \in Lat$
16		simp12l	$⊢ (((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) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land r \underset{˙}{\lor} (Y \underset{˙}{\land} W) = Y)) \to X \in B$
17		simp3ll	$⊢ (((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) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land r \underset{˙}{\lor} (Y \underset{˙}{\land} W) = Y)) \to r \in A$
18	1 6	atbase	$⊢ r \in A \to r \in B$
19	17 18	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 I (X) \subseteq I (Y) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land r \underset{˙}{\lor} (Y \underset{˙}{\land} W) = Y)) \to r \in B$
20	1 4	latjcl	$⊢ (K \in Lat \land r \in B \land X \in B) \to r \underset{˙}{\lor} X \in B$
21	15 19 16 20	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 I (X) \subseteq I (Y) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land r \underset{˙}{\lor} (Y \underset{˙}{\land} W) = Y)) \to r \underset{˙}{\lor} X \in B$
22		simp13l	$⊢ (((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) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land r \underset{˙}{\lor} (Y \underset{˙}{\land} W) = Y)) \to Y \in B$
23	1 2 4	latlej2	$⊢ (K \in Lat \land r \in B \land X \in B) \to X \underset{˙}{\leq} (r \underset{˙}{\lor} X)$
24	15 19 16 23	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 I (X) \subseteq I (Y) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land r \underset{˙}{\lor} (Y \underset{˙}{\land} W) = Y)) \to X \underset{˙}{\leq} (r \underset{˙}{\lor} X)$
25		simp11	$⊢ (((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) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land r \underset{˙}{\lor} (Y \underset{˙}{\land} W) = Y)) \to (K \in HL \land W \in H)$
26		simp3lr	$⊢ (((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) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land r \underset{˙}{\lor} (Y \underset{˙}{\land} W) = Y)) \to \neg r \underset{˙}{\leq} W$
27	1 2 4	latlej1	$⊢ (K \in Lat \land r \in B \land X \in B) \to r \underset{˙}{\leq} (r \underset{˙}{\lor} X)$
28	15 19 16 27	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 I (X) \subseteq I (Y) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land r \underset{˙}{\lor} (Y \underset{˙}{\land} W) = Y)) \to r \underset{˙}{\leq} (r \underset{˙}{\lor} X)$
29		simp11r	$⊢ (((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) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land r \underset{˙}{\lor} (Y \underset{˙}{\land} W) = Y)) \to W \in H$
30	1 3	lhpbase	$⊢ W \in H \to W \in B$
31	29 30	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 I (X) \subseteq I (Y) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land r \underset{˙}{\lor} (Y \underset{˙}{\land} W) = Y)) \to W \in B$
32	1 2	lattr	$⊢ (K \in Lat \land (r \in B \land r \underset{˙}{\lor} X \in B \land W \in B)) \to ((r \underset{˙}{\leq} (r \underset{˙}{\lor} X) \land (r \underset{˙}{\lor} X) \underset{˙}{\leq} W) \to r \underset{˙}{\leq} W)$
33	15 19 21 31 32	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 I (X) \subseteq I (Y) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land r \underset{˙}{\lor} (Y \underset{˙}{\land} W) = Y)) \to ((r \underset{˙}{\leq} (r \underset{˙}{\lor} X) \land (r \underset{˙}{\lor} X) \underset{˙}{\leq} W) \to r \underset{˙}{\leq} W)$
34	28 33	mpand	$⊢ (((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) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land r \underset{˙}{\lor} (Y \underset{˙}{\land} W) = Y)) \to ((r \underset{˙}{\lor} X) \underset{˙}{\leq} W \to r \underset{˙}{\leq} W)$
35	26 34	mtod	$⊢ (((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) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land r \underset{˙}{\lor} (Y \underset{˙}{\land} W) = Y)) \to \neg (r \underset{˙}{\lor} X) \underset{˙}{\leq} W$
36		simp3l	$⊢ (((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) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land r \underset{˙}{\lor} (Y \underset{˙}{\land} W) = Y)) \to (r \in A \land \neg r \underset{˙}{\leq} W)$
37		simp12	$⊢ (((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) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land r \underset{˙}{\lor} (Y \underset{˙}{\land} W) = Y)) \to (X \in B \land X \underset{˙}{\leq} W)$
38	1 2 4 5 6 3	lhple	$⊢ ((K \in HL \land W \in H) \land (r \in A \land \neg r \underset{˙}{\leq} W) \land (X \in B \land X \underset{˙}{\leq} W)) \to (r \underset{˙}{\lor} X) \underset{˙}{\land} W = X$
39	25 36 37 38	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 I (X) \subseteq I (Y) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land r \underset{˙}{\lor} (Y \underset{˙}{\land} W) = Y)) \to (r \underset{˙}{\lor} X) \underset{˙}{\land} W = X$
40	39	oveq2d	$⊢ (((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) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land r \underset{˙}{\lor} (Y \underset{˙}{\land} W) = Y)) \to r \underset{˙}{\lor} ((r \underset{˙}{\lor} X) \underset{˙}{\land} W) = r \underset{˙}{\lor} X$
41		eqid	$⊢ DIsoB (K) (W) = DIsoB (K) (W)$
42		eqid	$⊢ DIsoC (K) (W) = DIsoC (K) (W)$
43	1 2 4 5 6 3 9 41 42 7 8	dihvalcq	$⊢ ((K \in HL \land W \in H) \land (r \underset{˙}{\lor} X \in B \land \neg (r \underset{˙}{\lor} X) \underset{˙}{\leq} W) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land r \underset{˙}{\lor} ((r \underset{˙}{\lor} X) \underset{˙}{\land} W) = r \underset{˙}{\lor} X)) \to I (r \underset{˙}{\lor} X) = DIsoC (K) (W) (r) \underset{˙}{\oplus} DIsoB (K) (W) ((r \underset{˙}{\lor} X) \underset{˙}{\land} W)$
44	25 21 35 36 40 43	syl122anc	$⊢ (((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) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land r \underset{˙}{\lor} (Y \underset{˙}{\land} W) = Y)) \to I (r \underset{˙}{\lor} X) = DIsoC (K) (W) (r) \underset{˙}{\oplus} DIsoB (K) (W) ((r \underset{˙}{\lor} X) \underset{˙}{\land} W)$
45	3 7 25	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 I (X) \subseteq I (Y) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land r \underset{˙}{\lor} (Y \underset{˙}{\land} W) = Y)) \to U \in LMod$
46		eqid	$⊢ LSubSp (U) = LSubSp (U)$
47	46	lsssssubg	$⊢ U \in LMod \to LSubSp (U) \subseteq SubGrp (U)$
48	45 47	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 I (X) \subseteq I (Y) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land r \underset{˙}{\lor} (Y \underset{˙}{\land} W) = Y)) \to LSubSp (U) \subseteq SubGrp (U)$
49	2 6 3 7 42 46	diclss	$⊢ ((K \in HL \land W \in H) \land (r \in A \land \neg r \underset{˙}{\leq} W)) \to DIsoC (K) (W) (r) \in LSubSp (U)$
50	25 36 49	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 I (X) \subseteq I (Y) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land r \underset{˙}{\lor} (Y \underset{˙}{\land} W) = Y)) \to DIsoC (K) (W) (r) \in LSubSp (U)$
51	48 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 I (X) \subseteq I (Y) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land r \underset{˙}{\lor} (Y \underset{˙}{\land} W) = Y)) \to DIsoC (K) (W) (r) \in SubGrp (U)$
52	1 5	latmcl	$⊢ (K \in Lat \land Y \in B \land W \in B) \to Y \underset{˙}{\land} W \in B$
53	15 22 31 52	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 I (X) \subseteq I (Y) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land r \underset{˙}{\lor} (Y \underset{˙}{\land} W) = Y)) \to Y \underset{˙}{\land} W \in B$
54	1 2 5	latmle2	$⊢ (K \in Lat \land Y \in B \land W \in B) \to (Y \underset{˙}{\land} W) \underset{˙}{\leq} W$
55	15 22 31 54	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 I (X) \subseteq I (Y) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land r \underset{˙}{\lor} (Y \underset{˙}{\land} W) = Y)) \to (Y \underset{˙}{\land} W) \underset{˙}{\leq} W$
56	1 2 3 7 41 46	diblss	$⊢ ((K \in HL \land W \in H) \land (Y \underset{˙}{\land} W \in B \land (Y \underset{˙}{\land} W) \underset{˙}{\leq} W)) \to DIsoB (K) (W) (Y \underset{˙}{\land} W) \in LSubSp (U)$
57	25 53 55 56	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 I (X) \subseteq I (Y) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land r \underset{˙}{\lor} (Y \underset{˙}{\land} W) = Y)) \to DIsoB (K) (W) (Y \underset{˙}{\land} W) \in LSubSp (U)$
58	48 57	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 I (X) \subseteq I (Y) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land r \underset{˙}{\lor} (Y \underset{˙}{\land} W) = Y)) \to DIsoB (K) (W) (Y \underset{˙}{\land} W) \in SubGrp (U)$
59	8	lsmub1	$⊢ (DIsoC (K) (W) (r) \in SubGrp (U) \land DIsoB (K) (W) (Y \underset{˙}{\land} W) \in SubGrp (U)) \to DIsoC (K) (W) (r) \subseteq DIsoC (K) (W) (r) \underset{˙}{\oplus} DIsoB (K) (W) (Y \underset{˙}{\land} W)$
60	51 58 59	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 I (X) \subseteq I (Y) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land r \underset{˙}{\lor} (Y \underset{˙}{\land} W) = Y)) \to DIsoC (K) (W) (r) \subseteq DIsoC (K) (W) (r) \underset{˙}{\oplus} DIsoB (K) (W) (Y \underset{˙}{\land} W)$
61		simp13	$⊢ (((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) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land r \underset{˙}{\lor} (Y \underset{˙}{\land} W) = Y)) \to (Y \in B \land \neg Y \underset{˙}{\leq} W)$
62		simp3r	$⊢ (((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) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land r \underset{˙}{\lor} (Y \underset{˙}{\land} W) = Y)) \to r \underset{˙}{\lor} (Y \underset{˙}{\land} W) = Y$
63	1 2 4 5 6 3 9 41 42 7 8	dihvalcq	$⊢ ((K \in HL \land W \in H) \land (Y \in B \land \neg Y \underset{˙}{\leq} W) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land r \underset{˙}{\lor} (Y \underset{˙}{\land} W) = Y)) \to I (Y) = DIsoC (K) (W) (r) \underset{˙}{\oplus} DIsoB (K) (W) (Y \underset{˙}{\land} W)$
64	25 61 36 62 63	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 I (X) \subseteq I (Y) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land r \underset{˙}{\lor} (Y \underset{˙}{\land} W) = Y)) \to I (Y) = DIsoC (K) (W) (r) \underset{˙}{\oplus} DIsoB (K) (W) (Y \underset{˙}{\land} W)$
65	60 64	sseqtrrd	$⊢ (((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) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land r \underset{˙}{\lor} (Y \underset{˙}{\land} W) = Y)) \to DIsoC (K) (W) (r) \subseteq I (Y)$
66	39	fveq2d	$⊢ (((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) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land r \underset{˙}{\lor} (Y \underset{˙}{\land} W) = Y)) \to DIsoB (K) (W) ((r \underset{˙}{\lor} X) \underset{˙}{\land} W) = DIsoB (K) (W) (X)$
67	1 2 3 9 41	dihvalb	$⊢ ((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W)) \to I (X) = DIsoB (K) (W) (X)$
68	25 37 67	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 I (X) \subseteq I (Y) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land r \underset{˙}{\lor} (Y \underset{˙}{\land} W) = Y)) \to I (X) = DIsoB (K) (W) (X)$
69	66 68	eqtr4d	$⊢ (((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) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land r \underset{˙}{\lor} (Y \underset{˙}{\land} W) = Y)) \to DIsoB (K) (W) ((r \underset{˙}{\lor} X) \underset{˙}{\land} W) = I (X)$
70		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 I (X) \subseteq I (Y) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land r \underset{˙}{\lor} (Y \underset{˙}{\land} W) = Y)) \to I (X) \subseteq I (Y)$
71	69 70	eqsstrd	$⊢ (((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) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land r \underset{˙}{\lor} (Y \underset{˙}{\land} W) = Y)) \to DIsoB (K) (W) ((r \underset{˙}{\lor} X) \underset{˙}{\land} W) \subseteq I (Y)$
72	1 5	latmcl	$⊢ (K \in Lat \land r \underset{˙}{\lor} X \in B \land W \in B) \to (r \underset{˙}{\lor} X) \underset{˙}{\land} W \in B$
73	15 21 31 72	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 I (X) \subseteq I (Y) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land r \underset{˙}{\lor} (Y \underset{˙}{\land} W) = Y)) \to (r \underset{˙}{\lor} X) \underset{˙}{\land} W \in B$
74	1 2 5	latmle2	$⊢ (K \in Lat \land r \underset{˙}{\lor} X \in B \land W \in B) \to ((r \underset{˙}{\lor} X) \underset{˙}{\land} W) \underset{˙}{\leq} W$
75	15 21 31 74	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 I (X) \subseteq I (Y) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land r \underset{˙}{\lor} (Y \underset{˙}{\land} W) = Y)) \to ((r \underset{˙}{\lor} X) \underset{˙}{\land} W) \underset{˙}{\leq} W$
76	1 2 3 7 41 46	diblss	$⊢ ((K \in HL \land W \in H) \land ((r \underset{˙}{\lor} X) \underset{˙}{\land} W \in B \land ((r \underset{˙}{\lor} X) \underset{˙}{\land} W) \underset{˙}{\leq} W)) \to DIsoB (K) (W) ((r \underset{˙}{\lor} X) \underset{˙}{\land} W) \in LSubSp (U)$
77	25 73 75 76	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 I (X) \subseteq I (Y) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land r \underset{˙}{\lor} (Y \underset{˙}{\land} W) = Y)) \to DIsoB (K) (W) ((r \underset{˙}{\lor} X) \underset{˙}{\land} W) \in LSubSp (U)$
78	48 77	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 I (X) \subseteq I (Y) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land r \underset{˙}{\lor} (Y \underset{˙}{\land} W) = Y)) \to DIsoB (K) (W) ((r \underset{˙}{\lor} X) \underset{˙}{\land} W) \in SubGrp (U)$
79	1 3 9 7 46	dihlss	$⊢ ((K \in HL \land W \in H) \land Y \in B) \to I (Y) \in LSubSp (U)$
80	25 22 79	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 I (X) \subseteq I (Y) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land r \underset{˙}{\lor} (Y \underset{˙}{\land} W) = Y)) \to I (Y) \in LSubSp (U)$
81	48 80	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 I (X) \subseteq I (Y) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land r \underset{˙}{\lor} (Y \underset{˙}{\land} W) = Y)) \to I (Y) \in SubGrp (U)$
82	8	lsmlub	$⊢ (DIsoC (K) (W) (r) \in SubGrp (U) \land DIsoB (K) (W) ((r \underset{˙}{\lor} X) \underset{˙}{\land} W) \in SubGrp (U) \land I (Y) \in SubGrp (U)) \to ((DIsoC (K) (W) (r) \subseteq I (Y) \land DIsoB (K) (W) ((r \underset{˙}{\lor} X) \underset{˙}{\land} W) \subseteq I (Y)) \leftrightarrow DIsoC (K) (W) (r) \underset{˙}{\oplus} DIsoB (K) (W) ((r \underset{˙}{\lor} X) \underset{˙}{\land} W) \subseteq I (Y))$
83	51 78 81 82	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 I (X) \subseteq I (Y) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land r \underset{˙}{\lor} (Y \underset{˙}{\land} W) = Y)) \to ((DIsoC (K) (W) (r) \subseteq I (Y) \land DIsoB (K) (W) ((r \underset{˙}{\lor} X) \underset{˙}{\land} W) \subseteq I (Y)) \leftrightarrow DIsoC (K) (W) (r) \underset{˙}{\oplus} DIsoB (K) (W) ((r \underset{˙}{\lor} X) \underset{˙}{\land} W) \subseteq I (Y))$
84	65 71 83	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 I (X) \subseteq I (Y) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land r \underset{˙}{\lor} (Y \underset{˙}{\land} W) = Y)) \to DIsoC (K) (W) (r) \underset{˙}{\oplus} DIsoB (K) (W) ((r \underset{˙}{\lor} X) \underset{˙}{\land} W) \subseteq I (Y)$
85	44 84	eqsstrd	$⊢ (((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) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land r \underset{˙}{\lor} (Y \underset{˙}{\land} W) = Y)) \to I (r \underset{˙}{\lor} X) \subseteq I (Y)$
86	1 2 3 9	dihord4	$⊢ ((K \in HL \land W \in H) \land (r \underset{˙}{\lor} X \in B \land \neg (r \underset{˙}{\lor} X) \underset{˙}{\leq} W) \land (Y \in B \land \neg Y \underset{˙}{\leq} W)) \to (I (r \underset{˙}{\lor} X) \subseteq I (Y) \leftrightarrow (r \underset{˙}{\lor} X) \underset{˙}{\leq} Y)$
87	25 21 35 61 86	syl121anc	$⊢ (((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) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land r \underset{˙}{\lor} (Y \underset{˙}{\land} W) = Y)) \to (I (r \underset{˙}{\lor} X) \subseteq I (Y) \leftrightarrow (r \underset{˙}{\lor} X) \underset{˙}{\leq} Y)$
88	85 87	mpbid	$⊢ (((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) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land r \underset{˙}{\lor} (Y \underset{˙}{\land} W) = Y)) \to (r \underset{˙}{\lor} X) \underset{˙}{\leq} Y$
89	1 2 15 16 21 22 24 88	lattrd	$⊢ (((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) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land r \underset{˙}{\lor} (Y \underset{˙}{\land} W) = Y)) \to X \underset{˙}{\leq} Y$
90	89	3expia	$⊢ (((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 (((r \in A \land \neg r \underset{˙}{\leq} W) \land r \underset{˙}{\lor} (Y \underset{˙}{\land} W) = Y) \to X \underset{˙}{\leq} Y)$
91	90	exp4c	$⊢ (((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 (r \in A \to (\neg r \underset{˙}{\leq} W \to (r \underset{˙}{\lor} (Y \underset{˙}{\land} W) = Y \to X \underset{˙}{\leq} Y)))$
92	91	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 I (X) \subseteq I (Y)) \to (r \in A \to ((\neg r \underset{˙}{\leq} W \land r \underset{˙}{\lor} (Y \underset{˙}{\land} W) = Y) \to X \underset{˙}{\leq} Y))$
93	92	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 I (X) \subseteq I (Y)) \to (\exists r \in A (\neg r \underset{˙}{\leq} W \land r \underset{˙}{\lor} (Y \underset{˙}{\land} W) = Y) \to X \underset{˙}{\leq} Y)$
94	13 93	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 I (X) \subseteq I (Y)) \to X \underset{˙}{\leq} Y$

Metamath Proof Explorer

Theorem dihord5apre

Proof