dihord4

Description: The isomorphism H for a lattice K is order-preserving in the region not under co-atom W . TODO: reformat ( q e. A /\ -. q .<_ W ) to eliminate adant*. (Contributed by NM, 6-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	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)$

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		eqid	$⊢ join (K) = join (K)$
6		eqid	$⊢ meet (K) = meet (K)$
7		eqid	$⊢ Atoms (K) = Atoms (K)$
8	1 2 5 6 7 3	lhpmcvr2	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W)) \to \exists q \in Atoms (K) (\neg q \underset{˙}{\leq} W \land q join (K) (X meet (K) W) = X)$
9	8	3adant3	$⊢ ((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 \exists q \in Atoms (K) (\neg q \underset{˙}{\leq} W \land q join (K) (X meet (K) W) = X)$
10	1 2 5 6 7 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	10	3adant2	$⊢ ((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 \exists r \in Atoms (K) (\neg r \underset{˙}{\leq} W \land r join (K) (Y meet (K) W) = Y)$
12		reeanv	$⊢ \exists q \in Atoms (K) \exists r \in Atoms (K) ((\neg q \underset{˙}{\leq} W \land q join (K) (X meet (K) W) = X) \land (\neg r \underset{˙}{\leq} W \land r join (K) (Y meet (K) W) = Y)) \leftrightarrow (\exists q \in Atoms (K) (\neg q \underset{˙}{\leq} W \land q join (K) (X meet (K) W) = X) \land \exists r \in Atoms (K) (\neg r \underset{˙}{\leq} W \land r join (K) (Y meet (K) W) = Y))$
13	9 11 12	sylanbrc	$⊢ ((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 \exists q \in Atoms (K) \exists r \in Atoms (K) ((\neg q \underset{˙}{\leq} W \land q join (K) (X meet (K) W) = X) \land (\neg r \underset{˙}{\leq} W \land r join (K) (Y meet (K) W) = Y))$
14		simp11	$⊢ (((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)) \land (q \in Atoms (K) \land r \in Atoms (K)) \land ((\neg q \underset{˙}{\leq} W \land q join (K) (X meet (K) W) = X) \land (\neg r \underset{˙}{\leq} W \land r join (K) (Y meet (K) W) = Y))) \to (K \in HL \land W \in H)$
15		simp12	$⊢ (((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)) \land (q \in Atoms (K) \land r \in Atoms (K)) \land ((\neg q \underset{˙}{\leq} W \land q join (K) (X meet (K) W) = X) \land (\neg r \underset{˙}{\leq} W \land r join (K) (Y meet (K) W) = Y))) \to (X \in B \land \neg X \underset{˙}{\leq} W)$
16		simp2l	$⊢ (((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)) \land (q \in Atoms (K) \land r \in Atoms (K)) \land ((\neg q \underset{˙}{\leq} W \land q join (K) (X meet (K) W) = X) \land (\neg r \underset{˙}{\leq} W \land r join (K) (Y meet (K) W) = Y))) \to q \in Atoms (K)$
17		simp3ll	$⊢ (((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)) \land (q \in Atoms (K) \land r \in Atoms (K)) \land ((\neg q \underset{˙}{\leq} W \land q join (K) (X meet (K) W) = X) \land (\neg r \underset{˙}{\leq} W \land r join (K) (Y meet (K) W) = Y))) \to \neg q \underset{˙}{\leq} W$
18	16 17	jca	$⊢ (((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)) \land (q \in Atoms (K) \land r \in Atoms (K)) \land ((\neg q \underset{˙}{\leq} W \land q join (K) (X meet (K) W) = X) \land (\neg r \underset{˙}{\leq} W \land r join (K) (Y meet (K) W) = Y))) \to (q \in Atoms (K) \land \neg q \underset{˙}{\leq} W)$
19		simp3lr	$⊢ (((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)) \land (q \in Atoms (K) \land r \in Atoms (K)) \land ((\neg q \underset{˙}{\leq} W \land q join (K) (X meet (K) W) = X) \land (\neg r \underset{˙}{\leq} W \land r join (K) (Y meet (K) W) = Y))) \to q join (K) (X meet (K) W) = X$
20		eqid	$⊢ DIsoB (K) (W) = DIsoB (K) (W)$
21		eqid	$⊢ DIsoC (K) (W) = DIsoC (K) (W)$
22		eqid	$⊢ DVecH (K) (W) = DVecH (K) (W)$
23		eqid	$⊢ LSSum (DVecH (K) (W)) = LSSum (DVecH (K) (W))$
24	1 2 5 6 7 3 4 20 21 22 23	dihvalcq	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((q \in Atoms (K) \land \neg q \underset{˙}{\leq} W) \land q join (K) (X meet (K) W) = X)) \to I (X) = DIsoC (K) (W) (q) LSSum (DVecH (K) (W)) DIsoB (K) (W) (X meet (K) W)$
25	14 15 18 19 24	syl112anc	$⊢ (((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)) \land (q \in Atoms (K) \land r \in Atoms (K)) \land ((\neg q \underset{˙}{\leq} W \land q join (K) (X meet (K) W) = X) \land (\neg r \underset{˙}{\leq} W \land r join (K) (Y meet (K) W) = Y))) \to I (X) = DIsoC (K) (W) (q) LSSum (DVecH (K) (W)) DIsoB (K) (W) (X meet (K) W)$
26		simp13	$⊢ (((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)) \land (q \in Atoms (K) \land r \in Atoms (K)) \land ((\neg q \underset{˙}{\leq} W \land q join (K) (X meet (K) W) = X) \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)$
27		simp2r	$⊢ (((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)) \land (q \in Atoms (K) \land r \in Atoms (K)) \land ((\neg q \underset{˙}{\leq} W \land q join (K) (X meet (K) W) = X) \land (\neg r \underset{˙}{\leq} W \land r join (K) (Y meet (K) W) = Y))) \to r \in Atoms (K)$
28		simp3rl	$⊢ (((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)) \land (q \in Atoms (K) \land r \in Atoms (K)) \land ((\neg q \underset{˙}{\leq} W \land q join (K) (X meet (K) W) = X) \land (\neg r \underset{˙}{\leq} W \land r join (K) (Y meet (K) W) = Y))) \to \neg r \underset{˙}{\leq} W$
29	27 28	jca	$⊢ (((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)) \land (q \in Atoms (K) \land r \in Atoms (K)) \land ((\neg q \underset{˙}{\leq} W \land q join (K) (X meet (K) W) = X) \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)$
30		simp3rr	$⊢ (((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)) \land (q \in Atoms (K) \land r \in Atoms (K)) \land ((\neg q \underset{˙}{\leq} W \land q join (K) (X meet (K) W) = X) \land (\neg r \underset{˙}{\leq} W \land r join (K) (Y meet (K) W) = Y))) \to r join (K) (Y meet (K) W) = Y$
31	1 2 5 6 7 3 4 20 21 22 23	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)$
32	14 26 29 30 31	syl112anc	$⊢ (((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)) \land (q \in Atoms (K) \land r \in Atoms (K)) \land ((\neg q \underset{˙}{\leq} W \land q join (K) (X meet (K) W) = X) \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)$
33	25 32	sseq12d	$⊢ (((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)) \land (q \in Atoms (K) \land r \in Atoms (K)) \land ((\neg q \underset{˙}{\leq} W \land q join (K) (X meet (K) W) = X) \land (\neg r \underset{˙}{\leq} W \land r join (K) (Y meet (K) W) = Y))) \to (I (X) \subseteq I (Y) \leftrightarrow DIsoC (K) (W) (q) LSSum (DVecH (K) (W)) DIsoB (K) (W) (X meet (K) W) \subseteq DIsoC (K) (W) (r) LSSum (DVecH (K) (W)) DIsoB (K) (W) (Y meet (K) W))$
34		simpl11	$⊢ ((((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)) \land (q \in Atoms (K) \land r \in Atoms (K)) \land ((\neg q \underset{˙}{\leq} W \land q join (K) (X meet (K) W) = X) \land (\neg r \underset{˙}{\leq} W \land r join (K) (Y meet (K) W) = Y))) \land DIsoC (K) (W) (q) LSSum (DVecH (K) (W)) DIsoB (K) (W) (X meet (K) W) \subseteq DIsoC (K) (W) (r) LSSum (DVecH (K) (W)) DIsoB (K) (W) (Y meet (K) W)) \to (K \in HL \land W \in H)$
35		simpl2l	$⊢ ((((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)) \land (q \in Atoms (K) \land r \in Atoms (K)) \land ((\neg q \underset{˙}{\leq} W \land q join (K) (X meet (K) W) = X) \land (\neg r \underset{˙}{\leq} W \land r join (K) (Y meet (K) W) = Y))) \land DIsoC (K) (W) (q) LSSum (DVecH (K) (W)) DIsoB (K) (W) (X meet (K) W) \subseteq DIsoC (K) (W) (r) LSSum (DVecH (K) (W)) DIsoB (K) (W) (Y meet (K) W)) \to q \in Atoms (K)$
36	17	adantr	$⊢ ((((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)) \land (q \in Atoms (K) \land r \in Atoms (K)) \land ((\neg q \underset{˙}{\leq} W \land q join (K) (X meet (K) W) = X) \land (\neg r \underset{˙}{\leq} W \land r join (K) (Y meet (K) W) = Y))) \land DIsoC (K) (W) (q) LSSum (DVecH (K) (W)) DIsoB (K) (W) (X meet (K) W) \subseteq DIsoC (K) (W) (r) LSSum (DVecH (K) (W)) DIsoB (K) (W) (Y meet (K) W)) \to \neg q \underset{˙}{\leq} W$
37	35 36	jca	$⊢ ((((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)) \land (q \in Atoms (K) \land r \in Atoms (K)) \land ((\neg q \underset{˙}{\leq} W \land q join (K) (X meet (K) W) = X) \land (\neg r \underset{˙}{\leq} W \land r join (K) (Y meet (K) W) = Y))) \land DIsoC (K) (W) (q) LSSum (DVecH (K) (W)) DIsoB (K) (W) (X meet (K) W) \subseteq DIsoC (K) (W) (r) LSSum (DVecH (K) (W)) DIsoB (K) (W) (Y meet (K) W)) \to (q \in Atoms (K) \land \neg q \underset{˙}{\leq} W)$
38		simpl2r	$⊢ ((((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)) \land (q \in Atoms (K) \land r \in Atoms (K)) \land ((\neg q \underset{˙}{\leq} W \land q join (K) (X meet (K) W) = X) \land (\neg r \underset{˙}{\leq} W \land r join (K) (Y meet (K) W) = Y))) \land DIsoC (K) (W) (q) LSSum (DVecH (K) (W)) DIsoB (K) (W) (X meet (K) W) \subseteq DIsoC (K) (W) (r) LSSum (DVecH (K) (W)) DIsoB (K) (W) (Y meet (K) W)) \to r \in Atoms (K)$
39	28	adantr	$⊢ ((((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)) \land (q \in Atoms (K) \land r \in Atoms (K)) \land ((\neg q \underset{˙}{\leq} W \land q join (K) (X meet (K) W) = X) \land (\neg r \underset{˙}{\leq} W \land r join (K) (Y meet (K) W) = Y))) \land DIsoC (K) (W) (q) LSSum (DVecH (K) (W)) DIsoB (K) (W) (X meet (K) W) \subseteq DIsoC (K) (W) (r) LSSum (DVecH (K) (W)) DIsoB (K) (W) (Y meet (K) W)) \to \neg r \underset{˙}{\leq} W$
40	38 39	jca	$⊢ ((((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)) \land (q \in Atoms (K) \land r \in Atoms (K)) \land ((\neg q \underset{˙}{\leq} W \land q join (K) (X meet (K) W) = X) \land (\neg r \underset{˙}{\leq} W \land r join (K) (Y meet (K) W) = Y))) \land DIsoC (K) (W) (q) LSSum (DVecH (K) (W)) DIsoB (K) (W) (X meet (K) W) \subseteq DIsoC (K) (W) (r) LSSum (DVecH (K) (W)) DIsoB (K) (W) (Y meet (K) W)) \to (r \in Atoms (K) \land \neg r \underset{˙}{\leq} W)$
41		simp12l	$⊢ (((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)) \land (q \in Atoms (K) \land r \in Atoms (K)) \land ((\neg q \underset{˙}{\leq} W \land q join (K) (X meet (K) W) = X) \land (\neg r \underset{˙}{\leq} W \land r join (K) (Y meet (K) W) = Y))) \to X \in B$
42	41	adantr	$⊢ ((((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)) \land (q \in Atoms (K) \land r \in Atoms (K)) \land ((\neg q \underset{˙}{\leq} W \land q join (K) (X meet (K) W) = X) \land (\neg r \underset{˙}{\leq} W \land r join (K) (Y meet (K) W) = Y))) \land DIsoC (K) (W) (q) LSSum (DVecH (K) (W)) DIsoB (K) (W) (X meet (K) W) \subseteq DIsoC (K) (W) (r) LSSum (DVecH (K) (W)) DIsoB (K) (W) (Y meet (K) W)) \to X \in B$
43		simp13l	$⊢ (((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)) \land (q \in Atoms (K) \land r \in Atoms (K)) \land ((\neg q \underset{˙}{\leq} W \land q join (K) (X meet (K) W) = X) \land (\neg r \underset{˙}{\leq} W \land r join (K) (Y meet (K) W) = Y))) \to Y \in B$
44	43	adantr	$⊢ ((((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)) \land (q \in Atoms (K) \land r \in Atoms (K)) \land ((\neg q \underset{˙}{\leq} W \land q join (K) (X meet (K) W) = X) \land (\neg r \underset{˙}{\leq} W \land r join (K) (Y meet (K) W) = Y))) \land DIsoC (K) (W) (q) LSSum (DVecH (K) (W)) DIsoB (K) (W) (X meet (K) W) \subseteq DIsoC (K) (W) (r) LSSum (DVecH (K) (W)) DIsoB (K) (W) (Y meet (K) W)) \to Y \in B$
45	19	adantr	$⊢ ((((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)) \land (q \in Atoms (K) \land r \in Atoms (K)) \land ((\neg q \underset{˙}{\leq} W \land q join (K) (X meet (K) W) = X) \land (\neg r \underset{˙}{\leq} W \land r join (K) (Y meet (K) W) = Y))) \land DIsoC (K) (W) (q) LSSum (DVecH (K) (W)) DIsoB (K) (W) (X meet (K) W) \subseteq DIsoC (K) (W) (r) LSSum (DVecH (K) (W)) DIsoB (K) (W) (Y meet (K) W)) \to q join (K) (X meet (K) W) = X$
46	30	adantr	$⊢ ((((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)) \land (q \in Atoms (K) \land r \in Atoms (K)) \land ((\neg q \underset{˙}{\leq} W \land q join (K) (X meet (K) W) = X) \land (\neg r \underset{˙}{\leq} W \land r join (K) (Y meet (K) W) = Y))) \land DIsoC (K) (W) (q) LSSum (DVecH (K) (W)) DIsoB (K) (W) (X meet (K) W) \subseteq DIsoC (K) (W) (r) LSSum (DVecH (K) (W)) DIsoB (K) (W) (Y meet (K) W)) \to r join (K) (Y meet (K) W) = Y$
47		simpr	$⊢ ((((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)) \land (q \in Atoms (K) \land r \in Atoms (K)) \land ((\neg q \underset{˙}{\leq} W \land q join (K) (X meet (K) W) = X) \land (\neg r \underset{˙}{\leq} W \land r join (K) (Y meet (K) W) = Y))) \land DIsoC (K) (W) (q) LSSum (DVecH (K) (W)) DIsoB (K) (W) (X meet (K) W) \subseteq DIsoC (K) (W) (r) LSSum (DVecH (K) (W)) DIsoB (K) (W) (Y meet (K) W)) \to DIsoC (K) (W) (q) LSSum (DVecH (K) (W)) DIsoB (K) (W) (X meet (K) W) \subseteq DIsoC (K) (W) (r) LSSum (DVecH (K) (W)) DIsoB (K) (W) (Y meet (K) W)$
48	1 2 5 6 7 3 20 21 22 23	dihord2	$⊢ (((K \in HL \land W \in H) \land (q \in Atoms (K) \land \neg q \underset{˙}{\leq} W) \land (r \in Atoms (K) \land \neg r \underset{˙}{\leq} W)) \land (X \in B \land Y \in B) \land (q join (K) (X meet (K) W) = X \land r join (K) (Y meet (K) W) = Y \land DIsoC (K) (W) (q) LSSum (DVecH (K) (W)) DIsoB (K) (W) (X meet (K) W) \subseteq DIsoC (K) (W) (r) LSSum (DVecH (K) (W)) DIsoB (K) (W) (Y meet (K) W))) \to X \underset{˙}{\leq} Y$
49	34 37 40 42 44 45 46 47 48	syl323anc	$⊢ ((((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)) \land (q \in Atoms (K) \land r \in Atoms (K)) \land ((\neg q \underset{˙}{\leq} W \land q join (K) (X meet (K) W) = X) \land (\neg r \underset{˙}{\leq} W \land r join (K) (Y meet (K) W) = Y))) \land DIsoC (K) (W) (q) LSSum (DVecH (K) (W)) DIsoB (K) (W) (X meet (K) W) \subseteq DIsoC (K) (W) (r) LSSum (DVecH (K) (W)) DIsoB (K) (W) (Y meet (K) W)) \to X \underset{˙}{\leq} Y$
50		simpl11	$⊢ ((((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)) \land (q \in Atoms (K) \land r \in Atoms (K)) \land ((\neg q \underset{˙}{\leq} W \land q join (K) (X meet (K) W) = X) \land (\neg r \underset{˙}{\leq} W \land r join (K) (Y meet (K) W) = Y))) \land X \underset{˙}{\leq} Y) \to (K \in HL \land W \in H)$
51		simpl2l	$⊢ ((((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)) \land (q \in Atoms (K) \land r \in Atoms (K)) \land ((\neg q \underset{˙}{\leq} W \land q join (K) (X meet (K) W) = X) \land (\neg r \underset{˙}{\leq} W \land r join (K) (Y meet (K) W) = Y))) \land X \underset{˙}{\leq} Y) \to q \in Atoms (K)$
52	17	adantr	$⊢ ((((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)) \land (q \in Atoms (K) \land r \in Atoms (K)) \land ((\neg q \underset{˙}{\leq} W \land q join (K) (X meet (K) W) = X) \land (\neg r \underset{˙}{\leq} W \land r join (K) (Y meet (K) W) = Y))) \land X \underset{˙}{\leq} Y) \to \neg q \underset{˙}{\leq} W$
53	51 52	jca	$⊢ ((((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)) \land (q \in Atoms (K) \land r \in Atoms (K)) \land ((\neg q \underset{˙}{\leq} W \land q join (K) (X meet (K) W) = X) \land (\neg r \underset{˙}{\leq} W \land r join (K) (Y meet (K) W) = Y))) \land X \underset{˙}{\leq} Y) \to (q \in Atoms (K) \land \neg q \underset{˙}{\leq} W)$
54		simpl2r	$⊢ ((((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)) \land (q \in Atoms (K) \land r \in Atoms (K)) \land ((\neg q \underset{˙}{\leq} W \land q join (K) (X meet (K) W) = X) \land (\neg r \underset{˙}{\leq} W \land r join (K) (Y meet (K) W) = Y))) \land X \underset{˙}{\leq} Y) \to r \in Atoms (K)$
55	28	adantr	$⊢ ((((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)) \land (q \in Atoms (K) \land r \in Atoms (K)) \land ((\neg q \underset{˙}{\leq} W \land q join (K) (X meet (K) W) = X) \land (\neg r \underset{˙}{\leq} W \land r join (K) (Y meet (K) W) = Y))) \land X \underset{˙}{\leq} Y) \to \neg r \underset{˙}{\leq} W$
56	54 55	jca	$⊢ ((((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)) \land (q \in Atoms (K) \land r \in Atoms (K)) \land ((\neg q \underset{˙}{\leq} W \land q join (K) (X meet (K) W) = X) \land (\neg r \underset{˙}{\leq} W \land r join (K) (Y meet (K) W) = Y))) \land X \underset{˙}{\leq} Y) \to (r \in Atoms (K) \land \neg r \underset{˙}{\leq} W)$
57	41	adantr	$⊢ ((((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)) \land (q \in Atoms (K) \land r \in Atoms (K)) \land ((\neg q \underset{˙}{\leq} W \land q join (K) (X meet (K) W) = X) \land (\neg r \underset{˙}{\leq} W \land r join (K) (Y meet (K) W) = Y))) \land X \underset{˙}{\leq} Y) \to X \in B$
58	43	adantr	$⊢ ((((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)) \land (q \in Atoms (K) \land r \in Atoms (K)) \land ((\neg q \underset{˙}{\leq} W \land q join (K) (X meet (K) W) = X) \land (\neg r \underset{˙}{\leq} W \land r join (K) (Y meet (K) W) = Y))) \land X \underset{˙}{\leq} Y) \to Y \in B$
59	19	adantr	$⊢ ((((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)) \land (q \in Atoms (K) \land r \in Atoms (K)) \land ((\neg q \underset{˙}{\leq} W \land q join (K) (X meet (K) W) = X) \land (\neg r \underset{˙}{\leq} W \land r join (K) (Y meet (K) W) = Y))) \land X \underset{˙}{\leq} Y) \to q join (K) (X meet (K) W) = X$
60	30	adantr	$⊢ ((((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)) \land (q \in Atoms (K) \land r \in Atoms (K)) \land ((\neg q \underset{˙}{\leq} W \land q join (K) (X meet (K) W) = X) \land (\neg r \underset{˙}{\leq} W \land r join (K) (Y meet (K) W) = Y))) \land X \underset{˙}{\leq} Y) \to r join (K) (Y meet (K) W) = Y$
61		simpr	$⊢ ((((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)) \land (q \in Atoms (K) \land r \in Atoms (K)) \land ((\neg q \underset{˙}{\leq} W \land q join (K) (X meet (K) W) = X) \land (\neg r \underset{˙}{\leq} W \land r join (K) (Y meet (K) W) = Y))) \land X \underset{˙}{\leq} Y) \to X \underset{˙}{\leq} Y$
62	1 2 5 6 7 3 20 21 22 23	dihord1	$⊢ (((K \in HL \land W \in H) \land (q \in Atoms (K) \land \neg q \underset{˙}{\leq} W) \land (r \in Atoms (K) \land \neg r \underset{˙}{\leq} W)) \land (X \in B \land Y \in B) \land (q join (K) (X meet (K) W) = X \land r join (K) (Y meet (K) W) = Y \land X \underset{˙}{\leq} Y)) \to DIsoC (K) (W) (q) LSSum (DVecH (K) (W)) DIsoB (K) (W) (X meet (K) W) \subseteq DIsoC (K) (W) (r) LSSum (DVecH (K) (W)) DIsoB (K) (W) (Y meet (K) W)$
63	50 53 56 57 58 59 60 61 62	syl323anc	$⊢ ((((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)) \land (q \in Atoms (K) \land r \in Atoms (K)) \land ((\neg q \underset{˙}{\leq} W \land q join (K) (X meet (K) W) = X) \land (\neg r \underset{˙}{\leq} W \land r join (K) (Y meet (K) W) = Y))) \land X \underset{˙}{\leq} Y) \to DIsoC (K) (W) (q) LSSum (DVecH (K) (W)) DIsoB (K) (W) (X meet (K) W) \subseteq DIsoC (K) (W) (r) LSSum (DVecH (K) (W)) DIsoB (K) (W) (Y meet (K) W)$
64	49 63	impbida	$⊢ (((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)) \land (q \in Atoms (K) \land r \in Atoms (K)) \land ((\neg q \underset{˙}{\leq} W \land q join (K) (X meet (K) W) = X) \land (\neg r \underset{˙}{\leq} W \land r join (K) (Y meet (K) W) = Y))) \to (DIsoC (K) (W) (q) LSSum (DVecH (K) (W)) DIsoB (K) (W) (X meet (K) W) \subseteq DIsoC (K) (W) (r) LSSum (DVecH (K) (W)) DIsoB (K) (W) (Y meet (K) W) \leftrightarrow X \underset{˙}{\leq} Y)$
65	33 64	bitrd	$⊢ (((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)) \land (q \in Atoms (K) \land r \in Atoms (K)) \land ((\neg q \underset{˙}{\leq} W \land q join (K) (X meet (K) W) = X) \land (\neg r \underset{˙}{\leq} W \land r join (K) (Y meet (K) W) = Y))) \to (I (X) \subseteq I (Y) \leftrightarrow X \underset{˙}{\leq} Y)$
66	65	3exp	$⊢ ((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 ((q \in Atoms (K) \land r \in Atoms (K)) \to (((\neg q \underset{˙}{\leq} W \land q join (K) (X meet (K) W) = X) \land (\neg r \underset{˙}{\leq} W \land r join (K) (Y meet (K) W) = Y)) \to (I (X) \subseteq I (Y) \leftrightarrow X \underset{˙}{\leq} Y)))$
67	66	rexlimdvv	$⊢ ((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 (\exists q \in Atoms (K) \exists r \in Atoms (K) ((\neg q \underset{˙}{\leq} W \land q join (K) (X meet (K) W) = X) \land (\neg r \underset{˙}{\leq} W \land r join (K) (Y meet (K) W) = Y)) \to (I (X) \subseteq I (Y) \leftrightarrow X \underset{˙}{\leq} Y))$
68	13 67	mpd	$⊢ ((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)$

Metamath Proof Explorer

Theorem dihord4

Proof