dihord2pre

Description: Part of proof after Lemma N of Crawley p. 122. Reverse ordering property. (Contributed by NM, 3-Mar-2014)

	Ref	Expression
Hypotheses	dihjust.b	$⊢ B = {Base}_{K}$
	dihjust.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	dihjust.j	$⊢ \underset{˙}{\lor} = join (K)$
	dihjust.m	$⊢ \underset{˙}{\land} = meet (K)$
	dihjust.a	$⊢ A = Atoms (K)$
	dihjust.h	$⊢ H = LHyp (K)$
	dihjust.i	$⊢ I = DIsoB (K) (W)$
	dihjust.J	$⊢ J = DIsoC (K) (W)$
	dihjust.u	$⊢ U = DVecH (K) (W)$
	dihjust.s	$⊢ \underset{˙}{\oplus} = LSSum (U)$
	dihord2c.t	$⊢ T = LTrn (K) (W)$
	dihord2c.r	$⊢ R = trL (K) (W)$
	dihord2c.o	$⊢ O = (h \in T ⟼ {I ↾}_{B})$
	dihord2.p	$⊢ P = oc (K) (W)$
	dihord2.e	$⊢ E = TEndo (K) (W)$
	dihord2.d	$⊢ \underset{˙}{+} = +_{U}$
	dihord2.g	$⊢ G = (ι h \in T \| h (P) = N)$
Assertion	dihord2pre	$⊢ (((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (N \in A \land \neg N \underset{˙}{\leq} W)) \land (X \in B \land Y \in B) \land J (Q) \underset{˙}{\oplus} I (X \underset{˙}{\land} W) \subseteq J (N) \underset{˙}{\oplus} I (Y \underset{˙}{\land} W)) \to (X \underset{˙}{\land} W) \underset{˙}{\leq} (Y \underset{˙}{\land} W)$

Proof

Step	Hyp	Ref	Expression
1		dihjust.b	$⊢ B = {Base}_{K}$
2		dihjust.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		dihjust.j	$⊢ \underset{˙}{\lor} = join (K)$
4		dihjust.m	$⊢ \underset{˙}{\land} = meet (K)$
5		dihjust.a	$⊢ A = Atoms (K)$
6		dihjust.h	$⊢ H = LHyp (K)$
7		dihjust.i	$⊢ I = DIsoB (K) (W)$
8		dihjust.J	$⊢ J = DIsoC (K) (W)$
9		dihjust.u	$⊢ U = DVecH (K) (W)$
10		dihjust.s	$⊢ \underset{˙}{\oplus} = LSSum (U)$
11		dihord2c.t	$⊢ T = LTrn (K) (W)$
12		dihord2c.r	$⊢ R = trL (K) (W)$
13		dihord2c.o	$⊢ O = (h \in T ⟼ {I ↾}_{B})$
14		dihord2.p	$⊢ P = oc (K) (W)$
15		dihord2.e	$⊢ E = TEndo (K) (W)$
16		dihord2.d	$⊢ \underset{˙}{+} = +_{U}$
17		dihord2.g	$⊢ G = (ι h \in T \| h (P) = N)$
18		simpl1	$⊢ ((((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (N \in A \land \neg N \underset{˙}{\leq} W)) \land (X \in B \land Y \in B) \land J (Q) \underset{˙}{\oplus} I (X \underset{˙}{\land} W) \subseteq J (N) \underset{˙}{\oplus} I (Y \underset{˙}{\land} W)) \land (f \in T \land R (f) \underset{˙}{\leq} (X \underset{˙}{\land} W))) \to ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (N \in A \land \neg N \underset{˙}{\leq} W))$
19		simpl2l	$⊢ ((((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (N \in A \land \neg N \underset{˙}{\leq} W)) \land (X \in B \land Y \in B) \land J (Q) \underset{˙}{\oplus} I (X \underset{˙}{\land} W) \subseteq J (N) \underset{˙}{\oplus} I (Y \underset{˙}{\land} W)) \land (f \in T \land R (f) \underset{˙}{\leq} (X \underset{˙}{\land} W))) \to X \in B$
20		simpl2r	$⊢ ((((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (N \in A \land \neg N \underset{˙}{\leq} W)) \land (X \in B \land Y \in B) \land J (Q) \underset{˙}{\oplus} I (X \underset{˙}{\land} W) \subseteq J (N) \underset{˙}{\oplus} I (Y \underset{˙}{\land} W)) \land (f \in T \land R (f) \underset{˙}{\leq} (X \underset{˙}{\land} W))) \to Y \in B$
21		simpl3	$⊢ ((((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (N \in A \land \neg N \underset{˙}{\leq} W)) \land (X \in B \land Y \in B) \land J (Q) \underset{˙}{\oplus} I (X \underset{˙}{\land} W) \subseteq J (N) \underset{˙}{\oplus} I (Y \underset{˙}{\land} W)) \land (f \in T \land R (f) \underset{˙}{\leq} (X \underset{˙}{\land} W))) \to J (Q) \underset{˙}{\oplus} I (X \underset{˙}{\land} W) \subseteq J (N) \underset{˙}{\oplus} I (Y \underset{˙}{\land} W)$
22		simprl	$⊢ ((((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (N \in A \land \neg N \underset{˙}{\leq} W)) \land (X \in B \land Y \in B) \land J (Q) \underset{˙}{\oplus} I (X \underset{˙}{\land} W) \subseteq J (N) \underset{˙}{\oplus} I (Y \underset{˙}{\land} W)) \land (f \in T \land R (f) \underset{˙}{\leq} (X \underset{˙}{\land} W))) \to f \in T$
23		simprr	$⊢ ((((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (N \in A \land \neg N \underset{˙}{\leq} W)) \land (X \in B \land Y \in B) \land J (Q) \underset{˙}{\oplus} I (X \underset{˙}{\land} W) \subseteq J (N) \underset{˙}{\oplus} I (Y \underset{˙}{\land} W)) \land (f \in T \land R (f) \underset{˙}{\leq} (X \underset{˙}{\land} W))) \to R (f) \underset{˙}{\leq} (X \underset{˙}{\land} W)$
24	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17	dihord11c	$⊢ (((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (N \in A \land \neg N \underset{˙}{\leq} W)) \land (X \in B \land Y \in B) \land (J (Q) \underset{˙}{\oplus} I (X \underset{˙}{\land} W) \subseteq J (N) \underset{˙}{\oplus} I (Y \underset{˙}{\land} W) \land f \in T \land R (f) \underset{˙}{\leq} (X \underset{˙}{\land} W))) \to \exists y \in J (N) \exists z \in I (Y \underset{˙}{\land} W) ⟨f, O⟩ = y \underset{˙}{+} z$
25	18 19 20 21 22 23 24	syl123anc	$⊢ ((((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (N \in A \land \neg N \underset{˙}{\leq} W)) \land (X \in B \land Y \in B) \land J (Q) \underset{˙}{\oplus} I (X \underset{˙}{\land} W) \subseteq J (N) \underset{˙}{\oplus} I (Y \underset{˙}{\land} W)) \land (f \in T \land R (f) \underset{˙}{\leq} (X \underset{˙}{\land} W))) \to \exists y \in J (N) \exists z \in I (Y \underset{˙}{\land} W) ⟨f, O⟩ = y \underset{˙}{+} z$
26		simpl11	$⊢ ((((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (N \in A \land \neg N \underset{˙}{\leq} W)) \land (X \in B \land Y \in B) \land J (Q) \underset{˙}{\oplus} I (X \underset{˙}{\land} W) \subseteq J (N) \underset{˙}{\oplus} I (Y \underset{˙}{\land} W)) \land (f \in T \land R (f) \underset{˙}{\leq} (X \underset{˙}{\land} W))) \to (K \in HL \land W \in H)$
27		simpl13	$⊢ ((((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (N \in A \land \neg N \underset{˙}{\leq} W)) \land (X \in B \land Y \in B) \land J (Q) \underset{˙}{\oplus} I (X \underset{˙}{\land} W) \subseteq J (N) \underset{˙}{\oplus} I (Y \underset{˙}{\land} W)) \land (f \in T \land R (f) \underset{˙}{\leq} (X \underset{˙}{\land} W))) \to (N \in A \land \neg N \underset{˙}{\leq} W)$
28	2 5 6 14 11 15 8 17	dicelval3	$⊢ ((K \in HL \land W \in H) \land (N \in A \land \neg N \underset{˙}{\leq} W)) \to (y \in J (N) \leftrightarrow \exists s \in E y = ⟨s (G), s⟩)$
29	26 27 28	syl2anc	$⊢ ((((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (N \in A \land \neg N \underset{˙}{\leq} W)) \land (X \in B \land Y \in B) \land J (Q) \underset{˙}{\oplus} I (X \underset{˙}{\land} W) \subseteq J (N) \underset{˙}{\oplus} I (Y \underset{˙}{\land} W)) \land (f \in T \land R (f) \underset{˙}{\leq} (X \underset{˙}{\land} W))) \to (y \in J (N) \leftrightarrow \exists s \in E y = ⟨s (G), s⟩)$
30		simp11l	$⊢ (((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (N \in A \land \neg N \underset{˙}{\leq} W)) \land (X \in B \land Y \in B) \land J (Q) \underset{˙}{\oplus} I (X \underset{˙}{\land} W) \subseteq J (N) \underset{˙}{\oplus} I (Y \underset{˙}{\land} W)) \to K \in HL$
31	30	adantr	$⊢ ((((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (N \in A \land \neg N \underset{˙}{\leq} W)) \land (X \in B \land Y \in B) \land J (Q) \underset{˙}{\oplus} I (X \underset{˙}{\land} W) \subseteq J (N) \underset{˙}{\oplus} I (Y \underset{˙}{\land} W)) \land (f \in T \land R (f) \underset{˙}{\leq} (X \underset{˙}{\land} W))) \to K \in HL$
32	31	hllatd	$⊢ ((((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (N \in A \land \neg N \underset{˙}{\leq} W)) \land (X \in B \land Y \in B) \land J (Q) \underset{˙}{\oplus} I (X \underset{˙}{\land} W) \subseteq J (N) \underset{˙}{\oplus} I (Y \underset{˙}{\land} W)) \land (f \in T \land R (f) \underset{˙}{\leq} (X \underset{˙}{\land} W))) \to K \in Lat$
33		simp11r	$⊢ (((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (N \in A \land \neg N \underset{˙}{\leq} W)) \land (X \in B \land Y \in B) \land J (Q) \underset{˙}{\oplus} I (X \underset{˙}{\land} W) \subseteq J (N) \underset{˙}{\oplus} I (Y \underset{˙}{\land} W)) \to W \in H$
34	33	adantr	$⊢ ((((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (N \in A \land \neg N \underset{˙}{\leq} W)) \land (X \in B \land Y \in B) \land J (Q) \underset{˙}{\oplus} I (X \underset{˙}{\land} W) \subseteq J (N) \underset{˙}{\oplus} I (Y \underset{˙}{\land} W)) \land (f \in T \land R (f) \underset{˙}{\leq} (X \underset{˙}{\land} W))) \to W \in H$
35	1 6	lhpbase	$⊢ W \in H \to W \in B$
36	34 35	syl	$⊢ ((((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (N \in A \land \neg N \underset{˙}{\leq} W)) \land (X \in B \land Y \in B) \land J (Q) \underset{˙}{\oplus} I (X \underset{˙}{\land} W) \subseteq J (N) \underset{˙}{\oplus} I (Y \underset{˙}{\land} W)) \land (f \in T \land R (f) \underset{˙}{\leq} (X \underset{˙}{\land} W))) \to W \in B$
37	1 4	latmcl	$⊢ (K \in Lat \land Y \in B \land W \in B) \to Y \underset{˙}{\land} W \in B$
38	32 20 36 37	syl3anc	$⊢ ((((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (N \in A \land \neg N \underset{˙}{\leq} W)) \land (X \in B \land Y \in B) \land J (Q) \underset{˙}{\oplus} I (X \underset{˙}{\land} W) \subseteq J (N) \underset{˙}{\oplus} I (Y \underset{˙}{\land} W)) \land (f \in T \land R (f) \underset{˙}{\leq} (X \underset{˙}{\land} W))) \to Y \underset{˙}{\land} W \in B$
39	1 2 4	latmle2	$⊢ (K \in Lat \land Y \in B \land W \in B) \to (Y \underset{˙}{\land} W) \underset{˙}{\leq} W$
40	32 20 36 39	syl3anc	$⊢ ((((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (N \in A \land \neg N \underset{˙}{\leq} W)) \land (X \in B \land Y \in B) \land J (Q) \underset{˙}{\oplus} I (X \underset{˙}{\land} W) \subseteq J (N) \underset{˙}{\oplus} I (Y \underset{˙}{\land} W)) \land (f \in T \land R (f) \underset{˙}{\leq} (X \underset{˙}{\land} W))) \to (Y \underset{˙}{\land} W) \underset{˙}{\leq} W$
41	1 2 6 11 12 13 7	dibelval3	$⊢ ((K \in HL \land W \in H) \land (Y \underset{˙}{\land} W \in B \land (Y \underset{˙}{\land} W) \underset{˙}{\leq} W)) \to (z \in I (Y \underset{˙}{\land} W) \leftrightarrow \exists g \in T (z = ⟨g, O⟩ \land R (g) \underset{˙}{\leq} (Y \underset{˙}{\land} W)))$
42	26 38 40 41	syl12anc	$⊢ ((((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (N \in A \land \neg N \underset{˙}{\leq} W)) \land (X \in B \land Y \in B) \land J (Q) \underset{˙}{\oplus} I (X \underset{˙}{\land} W) \subseteq J (N) \underset{˙}{\oplus} I (Y \underset{˙}{\land} W)) \land (f \in T \land R (f) \underset{˙}{\leq} (X \underset{˙}{\land} W))) \to (z \in I (Y \underset{˙}{\land} W) \leftrightarrow \exists g \in T (z = ⟨g, O⟩ \land R (g) \underset{˙}{\leq} (Y \underset{˙}{\land} W)))$
43	29 42	anbi12d	$⊢ ((((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (N \in A \land \neg N \underset{˙}{\leq} W)) \land (X \in B \land Y \in B) \land J (Q) \underset{˙}{\oplus} I (X \underset{˙}{\land} W) \subseteq J (N) \underset{˙}{\oplus} I (Y \underset{˙}{\land} W)) \land (f \in T \land R (f) \underset{˙}{\leq} (X \underset{˙}{\land} W))) \to ((y \in J (N) \land z \in I (Y \underset{˙}{\land} W)) \leftrightarrow (\exists s \in E y = ⟨s (G), s⟩ \land \exists g \in T (z = ⟨g, O⟩ \land R (g) \underset{˙}{\leq} (Y \underset{˙}{\land} W))))$
44		reeanv	$⊢ \exists s \in E \exists g \in T (y = ⟨s (G), s⟩ \land (z = ⟨g, O⟩ \land R (g) \underset{˙}{\leq} (Y \underset{˙}{\land} W))) \leftrightarrow (\exists s \in E y = ⟨s (G), s⟩ \land \exists g \in T (z = ⟨g, O⟩ \land R (g) \underset{˙}{\leq} (Y \underset{˙}{\land} W)))$
45		simpll1	$⊢ (((((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (N \in A \land \neg N \underset{˙}{\leq} W)) \land (X \in B \land Y \in B) \land J (Q) \underset{˙}{\oplus} I (X \underset{˙}{\land} W) \subseteq J (N) \underset{˙}{\oplus} I (Y \underset{˙}{\land} W)) \land (f \in T \land R (f) \underset{˙}{\leq} (X \underset{˙}{\land} W))) \land ((s \in E \land g \in T) \land R (g) \underset{˙}{\leq} (Y \underset{˙}{\land} W) \land ⟨f, O⟩ = ⟨s (G), s⟩ \underset{˙}{+} ⟨g, O⟩)) \to ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (N \in A \land \neg N \underset{˙}{\leq} W))$
46		simplr	$⊢ (((((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (N \in A \land \neg N \underset{˙}{\leq} W)) \land (X \in B \land Y \in B) \land J (Q) \underset{˙}{\oplus} I (X \underset{˙}{\land} W) \subseteq J (N) \underset{˙}{\oplus} I (Y \underset{˙}{\land} W)) \land (f \in T \land R (f) \underset{˙}{\leq} (X \underset{˙}{\land} W))) \land ((s \in E \land g \in T) \land R (g) \underset{˙}{\leq} (Y \underset{˙}{\land} W) \land ⟨f, O⟩ = ⟨s (G), s⟩ \underset{˙}{+} ⟨g, O⟩)) \to (f \in T \land R (f) \underset{˙}{\leq} (X \underset{˙}{\land} W))$
47		simpr	$⊢ (((((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (N \in A \land \neg N \underset{˙}{\leq} W)) \land (X \in B \land Y \in B) \land J (Q) \underset{˙}{\oplus} I (X \underset{˙}{\land} W) \subseteq J (N) \underset{˙}{\oplus} I (Y \underset{˙}{\land} W)) \land (f \in T \land R (f) \underset{˙}{\leq} (X \underset{˙}{\land} W))) \land ((s \in E \land g \in T) \land R (g) \underset{˙}{\leq} (Y \underset{˙}{\land} W) \land ⟨f, O⟩ = ⟨s (G), s⟩ \underset{˙}{+} ⟨g, O⟩)) \to ((s \in E \land g \in T) \land R (g) \underset{˙}{\leq} (Y \underset{˙}{\land} W) \land ⟨f, O⟩ = ⟨s (G), s⟩ \underset{˙}{+} ⟨g, O⟩)$
48	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17	dihord10	$⊢ (((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (N \in A \land \neg N \underset{˙}{\leq} W)) \land (f \in T \land R (f) \underset{˙}{\leq} (X \underset{˙}{\land} W)) \land ((s \in E \land g \in T) \land R (g) \underset{˙}{\leq} (Y \underset{˙}{\land} W) \land ⟨f, O⟩ = ⟨s (G), s⟩ \underset{˙}{+} ⟨g, O⟩)) \to R (f) \underset{˙}{\leq} (Y \underset{˙}{\land} W)$
49	45 46 47 48	syl3anc	$⊢ (((((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (N \in A \land \neg N \underset{˙}{\leq} W)) \land (X \in B \land Y \in B) \land J (Q) \underset{˙}{\oplus} I (X \underset{˙}{\land} W) \subseteq J (N) \underset{˙}{\oplus} I (Y \underset{˙}{\land} W)) \land (f \in T \land R (f) \underset{˙}{\leq} (X \underset{˙}{\land} W))) \land ((s \in E \land g \in T) \land R (g) \underset{˙}{\leq} (Y \underset{˙}{\land} W) \land ⟨f, O⟩ = ⟨s (G), s⟩ \underset{˙}{+} ⟨g, O⟩)) \to R (f) \underset{˙}{\leq} (Y \underset{˙}{\land} W)$
50	49	3exp2	$⊢ ((((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (N \in A \land \neg N \underset{˙}{\leq} W)) \land (X \in B \land Y \in B) \land J (Q) \underset{˙}{\oplus} I (X \underset{˙}{\land} W) \subseteq J (N) \underset{˙}{\oplus} I (Y \underset{˙}{\land} W)) \land (f \in T \land R (f) \underset{˙}{\leq} (X \underset{˙}{\land} W))) \to ((s \in E \land g \in T) \to (R (g) \underset{˙}{\leq} (Y \underset{˙}{\land} W) \to (⟨f, O⟩ = ⟨s (G), s⟩ \underset{˙}{+} ⟨g, O⟩ \to R (f) \underset{˙}{\leq} (Y \underset{˙}{\land} W))))$
51		oveq12	$⊢ (y = ⟨s (G), s⟩ \land z = ⟨g, O⟩) \to y \underset{˙}{+} z = ⟨s (G), s⟩ \underset{˙}{+} ⟨g, O⟩$
52	51	eqeq2d	$⊢ (y = ⟨s (G), s⟩ \land z = ⟨g, O⟩) \to (⟨f, O⟩ = y \underset{˙}{+} z \leftrightarrow ⟨f, O⟩ = ⟨s (G), s⟩ \underset{˙}{+} ⟨g, O⟩)$
53	52	imbi1d	$⊢ (y = ⟨s (G), s⟩ \land z = ⟨g, O⟩) \to ((⟨f, O⟩ = y \underset{˙}{+} z \to R (f) \underset{˙}{\leq} (Y \underset{˙}{\land} W)) \leftrightarrow (⟨f, O⟩ = ⟨s (G), s⟩ \underset{˙}{+} ⟨g, O⟩ \to R (f) \underset{˙}{\leq} (Y \underset{˙}{\land} W)))$
54	53	imbi2d	$⊢ (y = ⟨s (G), s⟩ \land z = ⟨g, O⟩) \to ((R (g) \underset{˙}{\leq} (Y \underset{˙}{\land} W) \to (⟨f, O⟩ = y \underset{˙}{+} z \to R (f) \underset{˙}{\leq} (Y \underset{˙}{\land} W))) \leftrightarrow (R (g) \underset{˙}{\leq} (Y \underset{˙}{\land} W) \to (⟨f, O⟩ = ⟨s (G), s⟩ \underset{˙}{+} ⟨g, O⟩ \to R (f) \underset{˙}{\leq} (Y \underset{˙}{\land} W))))$
55	54	biimprd	$⊢ (y = ⟨s (G), s⟩ \land z = ⟨g, O⟩) \to ((R (g) \underset{˙}{\leq} (Y \underset{˙}{\land} W) \to (⟨f, O⟩ = ⟨s (G), s⟩ \underset{˙}{+} ⟨g, O⟩ \to R (f) \underset{˙}{\leq} (Y \underset{˙}{\land} W))) \to (R (g) \underset{˙}{\leq} (Y \underset{˙}{\land} W) \to (⟨f, O⟩ = y \underset{˙}{+} z \to R (f) \underset{˙}{\leq} (Y \underset{˙}{\land} W))))$
56	55	com23	$⊢ (y = ⟨s (G), s⟩ \land z = ⟨g, O⟩) \to (R (g) \underset{˙}{\leq} (Y \underset{˙}{\land} W) \to ((R (g) \underset{˙}{\leq} (Y \underset{˙}{\land} W) \to (⟨f, O⟩ = ⟨s (G), s⟩ \underset{˙}{+} ⟨g, O⟩ \to R (f) \underset{˙}{\leq} (Y \underset{˙}{\land} W))) \to (⟨f, O⟩ = y \underset{˙}{+} z \to R (f) \underset{˙}{\leq} (Y \underset{˙}{\land} W))))$
57	56	impr	$⊢ (y = ⟨s (G), s⟩ \land (z = ⟨g, O⟩ \land R (g) \underset{˙}{\leq} (Y \underset{˙}{\land} W))) \to ((R (g) \underset{˙}{\leq} (Y \underset{˙}{\land} W) \to (⟨f, O⟩ = ⟨s (G), s⟩ \underset{˙}{+} ⟨g, O⟩ \to R (f) \underset{˙}{\leq} (Y \underset{˙}{\land} W))) \to (⟨f, O⟩ = y \underset{˙}{+} z \to R (f) \underset{˙}{\leq} (Y \underset{˙}{\land} W)))$
58	57	com12	$⊢ (R (g) \underset{˙}{\leq} (Y \underset{˙}{\land} W) \to (⟨f, O⟩ = ⟨s (G), s⟩ \underset{˙}{+} ⟨g, O⟩ \to R (f) \underset{˙}{\leq} (Y \underset{˙}{\land} W))) \to ((y = ⟨s (G), s⟩ \land (z = ⟨g, O⟩ \land R (g) \underset{˙}{\leq} (Y \underset{˙}{\land} W))) \to (⟨f, O⟩ = y \underset{˙}{+} z \to R (f) \underset{˙}{\leq} (Y \underset{˙}{\land} W)))$
59	50 58	syl6	$⊢ ((((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (N \in A \land \neg N \underset{˙}{\leq} W)) \land (X \in B \land Y \in B) \land J (Q) \underset{˙}{\oplus} I (X \underset{˙}{\land} W) \subseteq J (N) \underset{˙}{\oplus} I (Y \underset{˙}{\land} W)) \land (f \in T \land R (f) \underset{˙}{\leq} (X \underset{˙}{\land} W))) \to ((s \in E \land g \in T) \to ((y = ⟨s (G), s⟩ \land (z = ⟨g, O⟩ \land R (g) \underset{˙}{\leq} (Y \underset{˙}{\land} W))) \to (⟨f, O⟩ = y \underset{˙}{+} z \to R (f) \underset{˙}{\leq} (Y \underset{˙}{\land} W))))$
60	59	rexlimdvv	$⊢ ((((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (N \in A \land \neg N \underset{˙}{\leq} W)) \land (X \in B \land Y \in B) \land J (Q) \underset{˙}{\oplus} I (X \underset{˙}{\land} W) \subseteq J (N) \underset{˙}{\oplus} I (Y \underset{˙}{\land} W)) \land (f \in T \land R (f) \underset{˙}{\leq} (X \underset{˙}{\land} W))) \to (\exists s \in E \exists g \in T (y = ⟨s (G), s⟩ \land (z = ⟨g, O⟩ \land R (g) \underset{˙}{\leq} (Y \underset{˙}{\land} W))) \to (⟨f, O⟩ = y \underset{˙}{+} z \to R (f) \underset{˙}{\leq} (Y \underset{˙}{\land} W)))$
61	44 60	syl5bir	$⊢ ((((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (N \in A \land \neg N \underset{˙}{\leq} W)) \land (X \in B \land Y \in B) \land J (Q) \underset{˙}{\oplus} I (X \underset{˙}{\land} W) \subseteq J (N) \underset{˙}{\oplus} I (Y \underset{˙}{\land} W)) \land (f \in T \land R (f) \underset{˙}{\leq} (X \underset{˙}{\land} W))) \to ((\exists s \in E y = ⟨s (G), s⟩ \land \exists g \in T (z = ⟨g, O⟩ \land R (g) \underset{˙}{\leq} (Y \underset{˙}{\land} W))) \to (⟨f, O⟩ = y \underset{˙}{+} z \to R (f) \underset{˙}{\leq} (Y \underset{˙}{\land} W)))$
62	43 61	sylbid	$⊢ ((((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (N \in A \land \neg N \underset{˙}{\leq} W)) \land (X \in B \land Y \in B) \land J (Q) \underset{˙}{\oplus} I (X \underset{˙}{\land} W) \subseteq J (N) \underset{˙}{\oplus} I (Y \underset{˙}{\land} W)) \land (f \in T \land R (f) \underset{˙}{\leq} (X \underset{˙}{\land} W))) \to ((y \in J (N) \land z \in I (Y \underset{˙}{\land} W)) \to (⟨f, O⟩ = y \underset{˙}{+} z \to R (f) \underset{˙}{\leq} (Y \underset{˙}{\land} W)))$
63	62	rexlimdvv	$⊢ ((((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (N \in A \land \neg N \underset{˙}{\leq} W)) \land (X \in B \land Y \in B) \land J (Q) \underset{˙}{\oplus} I (X \underset{˙}{\land} W) \subseteq J (N) \underset{˙}{\oplus} I (Y \underset{˙}{\land} W)) \land (f \in T \land R (f) \underset{˙}{\leq} (X \underset{˙}{\land} W))) \to (\exists y \in J (N) \exists z \in I (Y \underset{˙}{\land} W) ⟨f, O⟩ = y \underset{˙}{+} z \to R (f) \underset{˙}{\leq} (Y \underset{˙}{\land} W))$
64	25 63	mpd	$⊢ ((((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (N \in A \land \neg N \underset{˙}{\leq} W)) \land (X \in B \land Y \in B) \land J (Q) \underset{˙}{\oplus} I (X \underset{˙}{\land} W) \subseteq J (N) \underset{˙}{\oplus} I (Y \underset{˙}{\land} W)) \land (f \in T \land R (f) \underset{˙}{\leq} (X \underset{˙}{\land} W))) \to R (f) \underset{˙}{\leq} (Y \underset{˙}{\land} W)$
65	64	exp32	$⊢ (((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (N \in A \land \neg N \underset{˙}{\leq} W)) \land (X \in B \land Y \in B) \land J (Q) \underset{˙}{\oplus} I (X \underset{˙}{\land} W) \subseteq J (N) \underset{˙}{\oplus} I (Y \underset{˙}{\land} W)) \to (f \in T \to (R (f) \underset{˙}{\leq} (X \underset{˙}{\land} W) \to R (f) \underset{˙}{\leq} (Y \underset{˙}{\land} W)))$
66	65	ralrimiv	$⊢ (((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (N \in A \land \neg N \underset{˙}{\leq} W)) \land (X \in B \land Y \in B) \land J (Q) \underset{˙}{\oplus} I (X \underset{˙}{\land} W) \subseteq J (N) \underset{˙}{\oplus} I (Y \underset{˙}{\land} W)) \to \forall f \in T (R (f) \underset{˙}{\leq} (X \underset{˙}{\land} W) \to R (f) \underset{˙}{\leq} (Y \underset{˙}{\land} W))$
67		simp11	$⊢ (((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (N \in A \land \neg N \underset{˙}{\leq} W)) \land (X \in B \land Y \in B) \land J (Q) \underset{˙}{\oplus} I (X \underset{˙}{\land} W) \subseteq J (N) \underset{˙}{\oplus} I (Y \underset{˙}{\land} W)) \to (K \in HL \land W \in H)$
68	30	hllatd	$⊢ (((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (N \in A \land \neg N \underset{˙}{\leq} W)) \land (X \in B \land Y \in B) \land J (Q) \underset{˙}{\oplus} I (X \underset{˙}{\land} W) \subseteq J (N) \underset{˙}{\oplus} I (Y \underset{˙}{\land} W)) \to K \in Lat$
69		simp2l	$⊢ (((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (N \in A \land \neg N \underset{˙}{\leq} W)) \land (X \in B \land Y \in B) \land J (Q) \underset{˙}{\oplus} I (X \underset{˙}{\land} W) \subseteq J (N) \underset{˙}{\oplus} I (Y \underset{˙}{\land} W)) \to X \in B$
70	33 35	syl	$⊢ (((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (N \in A \land \neg N \underset{˙}{\leq} W)) \land (X \in B \land Y \in B) \land J (Q) \underset{˙}{\oplus} I (X \underset{˙}{\land} W) \subseteq J (N) \underset{˙}{\oplus} I (Y \underset{˙}{\land} W)) \to W \in B$
71	1 4	latmcl	$⊢ (K \in Lat \land X \in B \land W \in B) \to X \underset{˙}{\land} W \in B$
72	68 69 70 71	syl3anc	$⊢ (((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (N \in A \land \neg N \underset{˙}{\leq} W)) \land (X \in B \land Y \in B) \land J (Q) \underset{˙}{\oplus} I (X \underset{˙}{\land} W) \subseteq J (N) \underset{˙}{\oplus} I (Y \underset{˙}{\land} W)) \to X \underset{˙}{\land} W \in B$
73	1 2 4	latmle2	$⊢ (K \in Lat \land X \in B \land W \in B) \to (X \underset{˙}{\land} W) \underset{˙}{\leq} W$
74	68 69 70 73	syl3anc	$⊢ (((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (N \in A \land \neg N \underset{˙}{\leq} W)) \land (X \in B \land Y \in B) \land J (Q) \underset{˙}{\oplus} I (X \underset{˙}{\land} W) \subseteq J (N) \underset{˙}{\oplus} I (Y \underset{˙}{\land} W)) \to (X \underset{˙}{\land} W) \underset{˙}{\leq} W$
75		simp2r	$⊢ (((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (N \in A \land \neg N \underset{˙}{\leq} W)) \land (X \in B \land Y \in B) \land J (Q) \underset{˙}{\oplus} I (X \underset{˙}{\land} W) \subseteq J (N) \underset{˙}{\oplus} I (Y \underset{˙}{\land} W)) \to Y \in B$
76	68 75 70 37	syl3anc	$⊢ (((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (N \in A \land \neg N \underset{˙}{\leq} W)) \land (X \in B \land Y \in B) \land J (Q) \underset{˙}{\oplus} I (X \underset{˙}{\land} W) \subseteq J (N) \underset{˙}{\oplus} I (Y \underset{˙}{\land} W)) \to Y \underset{˙}{\land} W \in B$
77	68 75 70 39	syl3anc	$⊢ (((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (N \in A \land \neg N \underset{˙}{\leq} W)) \land (X \in B \land Y \in B) \land J (Q) \underset{˙}{\oplus} I (X \underset{˙}{\land} W) \subseteq J (N) \underset{˙}{\oplus} I (Y \underset{˙}{\land} W)) \to (Y \underset{˙}{\land} W) \underset{˙}{\leq} W$
78	1 2 5 6 11 12	trlord	$⊢ ((K \in HL \land W \in H) \land (X \underset{˙}{\land} W \in B \land (X \underset{˙}{\land} W) \underset{˙}{\leq} W) \land (Y \underset{˙}{\land} W \in B \land (Y \underset{˙}{\land} W) \underset{˙}{\leq} W)) \to ((X \underset{˙}{\land} W) \underset{˙}{\leq} (Y \underset{˙}{\land} W) \leftrightarrow \forall f \in T (R (f) \underset{˙}{\leq} (X \underset{˙}{\land} W) \to R (f) \underset{˙}{\leq} (Y \underset{˙}{\land} W)))$
79	67 72 74 76 77 78	syl122anc	$⊢ (((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (N \in A \land \neg N \underset{˙}{\leq} W)) \land (X \in B \land Y \in B) \land J (Q) \underset{˙}{\oplus} I (X \underset{˙}{\land} W) \subseteq J (N) \underset{˙}{\oplus} I (Y \underset{˙}{\land} W)) \to ((X \underset{˙}{\land} W) \underset{˙}{\leq} (Y \underset{˙}{\land} W) \leftrightarrow \forall f \in T (R (f) \underset{˙}{\leq} (X \underset{˙}{\land} W) \to R (f) \underset{˙}{\leq} (Y \underset{˙}{\land} W)))$
80	66 79	mpbird	$⊢ (((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (N \in A \land \neg N \underset{˙}{\leq} W)) \land (X \in B \land Y \in B) \land J (Q) \underset{˙}{\oplus} I (X \underset{˙}{\land} W) \subseteq J (N) \underset{˙}{\oplus} I (Y \underset{˙}{\land} W)) \to (X \underset{˙}{\land} W) \underset{˙}{\leq} (Y \underset{˙}{\land} W)$

Metamath Proof Explorer

Theorem dihord2pre

Proof