dihglblem5apreN

Description: A conjunction property of isomorphism H. TODO: reduce antecedent size; general review for shorter proof. (Contributed by NM, 21-Mar-2014) (New usage is discouraged.)

	Ref	Expression
Hypotheses	dihglblem5a.b	$⊢ B = {Base}_{K}$
	dihglblem5a.m	$⊢ \underset{˙}{\land} = meet (K)$
	dihglblem5a.h	$⊢ H = LHyp (K)$
	dihglblem5a.i	$⊢ I = DIsoH (K) (W)$
	dihglblem5a.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	dihglblem5a.j	$⊢ \underset{˙}{\lor} = join (K)$
	dihglblem5a.a	$⊢ A = Atoms (K)$
	dihglblem5a.p	$⊢ P = oc (K) (W)$
	dihglblem5a.t	$⊢ T = LTrn (K) (W)$
	dihglblem5a.r	$⊢ R = trL (K) (W)$
	dihglblem5a.e	$⊢ E = TEndo (K) (W)$
	dihglblem5a.g	$⊢ G = (ι h \in T \| h (P) = q)$
	dihglblem5a.o	$⊢ \underset{˙}{0} = (h \in T ⟼ {I ↾}_{B})$
Assertion	dihglblem5apreN	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W)) \to I (X \underset{˙}{\land} W) = I (X) \cap I (W)$

Proof

Step	Hyp	Ref	Expression
1		dihglblem5a.b	$⊢ B = {Base}_{K}$
2		dihglblem5a.m	$⊢ \underset{˙}{\land} = meet (K)$
3		dihglblem5a.h	$⊢ H = LHyp (K)$
4		dihglblem5a.i	$⊢ I = DIsoH (K) (W)$
5		dihglblem5a.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
6		dihglblem5a.j	$⊢ \underset{˙}{\lor} = join (K)$
7		dihglblem5a.a	$⊢ A = Atoms (K)$
8		dihglblem5a.p	$⊢ P = oc (K) (W)$
9		dihglblem5a.t	$⊢ T = LTrn (K) (W)$
10		dihglblem5a.r	$⊢ R = trL (K) (W)$
11		dihglblem5a.e	$⊢ E = TEndo (K) (W)$
12		dihglblem5a.g	$⊢ G = (ι h \in T \| h (P) = q)$
13		dihglblem5a.o	$⊢ \underset{˙}{0} = (h \in T ⟼ {I ↾}_{B})$
14		hllat	$⊢ K \in HL \to K \in Lat$
15	14	ad2antrr	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W)) \to K \in Lat$
16		simprl	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W)) \to X \in B$
17	1 3	lhpbase	$⊢ W \in H \to W \in B$
18	17	ad2antlr	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W)) \to W \in B$
19	1 5 2	latmle1	$⊢ (K \in Lat \land X \in B \land W \in B) \to (X \underset{˙}{\land} W) \underset{˙}{\leq} X$
20	15 16 18 19	syl3anc	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W)) \to (X \underset{˙}{\land} W) \underset{˙}{\leq} X$
21		simpl	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W)) \to (K \in HL \land W \in H)$
22	1 2	latmcl	$⊢ (K \in Lat \land X \in B \land W \in B) \to X \underset{˙}{\land} W \in B$
23	15 16 18 22	syl3anc	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W)) \to X \underset{˙}{\land} W \in B$
24	1 5 3 4	dihord	$⊢ ((K \in HL \land W \in H) \land X \underset{˙}{\land} W \in B \land X \in B) \to (I (X \underset{˙}{\land} W) \subseteq I (X) \leftrightarrow (X \underset{˙}{\land} W) \underset{˙}{\leq} X)$
25	21 23 16 24	syl3anc	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W)) \to (I (X \underset{˙}{\land} W) \subseteq I (X) \leftrightarrow (X \underset{˙}{\land} W) \underset{˙}{\leq} X)$
26	20 25	mpbird	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W)) \to I (X \underset{˙}{\land} W) \subseteq I (X)$
27	1 5 2	latmle2	$⊢ (K \in Lat \land X \in B \land W \in B) \to (X \underset{˙}{\land} W) \underset{˙}{\leq} W$
28	15 16 18 27	syl3anc	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W)) \to (X \underset{˙}{\land} W) \underset{˙}{\leq} W$
29	1 5 3 4	dihord	$⊢ ((K \in HL \land W \in H) \land X \underset{˙}{\land} W \in B \land W \in B) \to (I (X \underset{˙}{\land} W) \subseteq I (W) \leftrightarrow (X \underset{˙}{\land} W) \underset{˙}{\leq} W)$
30	21 23 18 29	syl3anc	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W)) \to (I (X \underset{˙}{\land} W) \subseteq I (W) \leftrightarrow (X \underset{˙}{\land} W) \underset{˙}{\leq} W)$
31	28 30	mpbird	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W)) \to I (X \underset{˙}{\land} W) \subseteq I (W)$
32	26 31	ssind	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W)) \to I (X \underset{˙}{\land} W) \subseteq I (X) \cap I (W)$
33	3 4	dihvalrel	$⊢ (K \in HL \land W \in H) \to Rel I (X)$
34		relin1	$⊢ Rel I (X) \to Rel (I (X) \cap I (W))$
35	33 34	syl	$⊢ (K \in HL \land W \in H) \to Rel (I (X) \cap I (W))$
36	35	adantr	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W)) \to Rel (I (X) \cap I (W))$
37		elin	$⊢ ⟨f, s⟩ \in (I (X) \cap I (W)) \leftrightarrow (⟨f, s⟩ \in I (X) \land ⟨f, s⟩ \in I (W))$
38	1 5 6 2 7 3	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 \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)$
39		vex	$⊢ f \in V$
40		vex	$⊢ s \in V$
41	1 5 6 2 7 3 8 9 10 11 4 12 39 40	dihopelvalc	$⊢ ((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 \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \to (⟨f, s⟩ \in I (X) \leftrightarrow ((f \in T \land s \in E) \land R (f \circ {s (G)}^{-1}) \underset{˙}{\leq} X))$
42		id	$⊢ (K \in HL \land W \in H) \to (K \in HL \land W \in H)$
43	17	adantl	$⊢ (K \in HL \land W \in H) \to W \in B$
44	1 5	latref	$⊢ (K \in Lat \land W \in B) \to W \underset{˙}{\leq} W$
45	14 17 44	syl2an	$⊢ (K \in HL \land W \in H) \to W \underset{˙}{\leq} W$
46	1 5 3 9 10 13 4	dihopelvalbN	$⊢ ((K \in HL \land W \in H) \land (W \in B \land W \underset{˙}{\leq} W)) \to (⟨f, s⟩ \in I (W) \leftrightarrow ((f \in T \land R (f) \underset{˙}{\leq} W) \land s = \underset{˙}{0}))$
47	42 43 45 46	syl12anc	$⊢ (K \in HL \land W \in H) \to (⟨f, s⟩ \in I (W) \leftrightarrow ((f \in T \land R (f) \underset{˙}{\leq} W) \land s = \underset{˙}{0}))$
48	47	3ad2ant1	$⊢ ((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 \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \to (⟨f, s⟩ \in I (W) \leftrightarrow ((f \in T \land R (f) \underset{˙}{\leq} W) \land s = \underset{˙}{0}))$
49	41 48	anbi12d	$⊢ ((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 \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \to ((⟨f, s⟩ \in I (X) \land ⟨f, s⟩ \in I (W)) \leftrightarrow (((f \in T \land s \in E) \land R (f \circ {s (G)}^{-1}) \underset{˙}{\leq} X) \land ((f \in T \land R (f) \underset{˙}{\leq} W) \land s = \underset{˙}{0})))$
50		simprll	$⊢ (((f \in T \land s \in E) \land R (f \circ {s (G)}^{-1}) \underset{˙}{\leq} X) \land ((f \in T \land R (f) \underset{˙}{\leq} W) \land s = \underset{˙}{0})) \to f \in T$
51	50	adantl	$⊢ (((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 \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land (((f \in T \land s \in E) \land R (f \circ {s (G)}^{-1}) \underset{˙}{\leq} X) \land ((f \in T \land R (f) \underset{˙}{\leq} W) \land s = \underset{˙}{0}))) \to f \in T$
52		simprrr	$⊢ (((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 \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land (((f \in T \land s \in E) \land R (f \circ {s (G)}^{-1}) \underset{˙}{\leq} X) \land ((f \in T \land R (f) \underset{˙}{\leq} W) \land s = \underset{˙}{0}))) \to s = \underset{˙}{0}$
53	52	fveq1d	$⊢ (((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 \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land (((f \in T \land s \in E) \land R (f \circ {s (G)}^{-1}) \underset{˙}{\leq} X) \land ((f \in T \land R (f) \underset{˙}{\leq} W) \land s = \underset{˙}{0}))) \to s (G) = \underset{˙}{0} (G)$
54		simpl1	$⊢ (((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 \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land (((f \in T \land s \in E) \land R (f \circ {s (G)}^{-1}) \underset{˙}{\leq} X) \land ((f \in T \land R (f) \underset{˙}{\leq} W) \land s = \underset{˙}{0}))) \to (K \in HL \land W \in H)$
55	5 7 3 8	lhpocnel2	$⊢ (K \in HL \land W \in H) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
56	54 55	syl	$⊢ (((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 \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land (((f \in T \land s \in E) \land R (f \circ {s (G)}^{-1}) \underset{˙}{\leq} X) \land ((f \in T \land R (f) \underset{˙}{\leq} W) \land s = \underset{˙}{0}))) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
57		simpl3l	$⊢ (((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 \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land (((f \in T \land s \in E) \land R (f \circ {s (G)}^{-1}) \underset{˙}{\leq} X) \land ((f \in T \land R (f) \underset{˙}{\leq} W) \land s = \underset{˙}{0}))) \to (q \in A \land \neg q \underset{˙}{\leq} W)$
58	5 7 3 9 12	ltrniotacl	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (q \in A \land \neg q \underset{˙}{\leq} W)) \to G \in T$
59	54 56 57 58	syl3anc	$⊢ (((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 \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land (((f \in T \land s \in E) \land R (f \circ {s (G)}^{-1}) \underset{˙}{\leq} X) \land ((f \in T \land R (f) \underset{˙}{\leq} W) \land s = \underset{˙}{0}))) \to G \in T$
60	13 1	tendo02	$⊢ G \in T \to \underset{˙}{0} (G) = {I ↾}_{B}$
61	59 60	syl	$⊢ (((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 \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land (((f \in T \land s \in E) \land R (f \circ {s (G)}^{-1}) \underset{˙}{\leq} X) \land ((f \in T \land R (f) \underset{˙}{\leq} W) \land s = \underset{˙}{0}))) \to \underset{˙}{0} (G) = {I ↾}_{B}$
62	53 61	eqtrd	$⊢ (((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 \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land (((f \in T \land s \in E) \land R (f \circ {s (G)}^{-1}) \underset{˙}{\leq} X) \land ((f \in T \land R (f) \underset{˙}{\leq} W) \land s = \underset{˙}{0}))) \to s (G) = {I ↾}_{B}$
63	62	cnveqd	$⊢ (((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 \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land (((f \in T \land s \in E) \land R (f \circ {s (G)}^{-1}) \underset{˙}{\leq} X) \land ((f \in T \land R (f) \underset{˙}{\leq} W) \land s = \underset{˙}{0}))) \to {s (G)}^{-1} = {({I ↾}_{B})}^{-1}$
64		cnvresid	$⊢ {({I ↾}_{B})}^{-1} = {I ↾}_{B}$
65	63 64	eqtrdi	$⊢ (((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 \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land (((f \in T \land s \in E) \land R (f \circ {s (G)}^{-1}) \underset{˙}{\leq} X) \land ((f \in T \land R (f) \underset{˙}{\leq} W) \land s = \underset{˙}{0}))) \to {s (G)}^{-1} = {I ↾}_{B}$
66	65	coeq2d	$⊢ (((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 \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land (((f \in T \land s \in E) \land R (f \circ {s (G)}^{-1}) \underset{˙}{\leq} X) \land ((f \in T \land R (f) \underset{˙}{\leq} W) \land s = \underset{˙}{0}))) \to f \circ {s (G)}^{-1} = f \circ ({I ↾}_{B})$
67	1 3 9	ltrn1o	$⊢ ((K \in HL \land W \in H) \land f \in T) \to f : B \underset{1-1 onto}{⟶} B$
68	54 51 67	syl2anc	$⊢ (((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 \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land (((f \in T \land s \in E) \land R (f \circ {s (G)}^{-1}) \underset{˙}{\leq} X) \land ((f \in T \land R (f) \underset{˙}{\leq} W) \land s = \underset{˙}{0}))) \to f : B \underset{1-1 onto}{⟶} B$
69		f1of	$⊢ f : B \underset{1-1 onto}{⟶} B \to f : B ⟶ B$
70		fcoi1	$⊢ f : B ⟶ B \to f \circ ({I ↾}_{B}) = f$
71	68 69 70	3syl	$⊢ (((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 \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land (((f \in T \land s \in E) \land R (f \circ {s (G)}^{-1}) \underset{˙}{\leq} X) \land ((f \in T \land R (f) \underset{˙}{\leq} W) \land s = \underset{˙}{0}))) \to f \circ ({I ↾}_{B}) = f$
72	66 71	eqtrd	$⊢ (((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 \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land (((f \in T \land s \in E) \land R (f \circ {s (G)}^{-1}) \underset{˙}{\leq} X) \land ((f \in T \land R (f) \underset{˙}{\leq} W) \land s = \underset{˙}{0}))) \to f \circ {s (G)}^{-1} = f$
73	72	fveq2d	$⊢ (((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 \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land (((f \in T \land s \in E) \land R (f \circ {s (G)}^{-1}) \underset{˙}{\leq} X) \land ((f \in T \land R (f) \underset{˙}{\leq} W) \land s = \underset{˙}{0}))) \to R (f \circ {s (G)}^{-1}) = R (f)$
74		simprlr	$⊢ (((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 \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land (((f \in T \land s \in E) \land R (f \circ {s (G)}^{-1}) \underset{˙}{\leq} X) \land ((f \in T \land R (f) \underset{˙}{\leq} W) \land s = \underset{˙}{0}))) \to R (f \circ {s (G)}^{-1}) \underset{˙}{\leq} X$
75	73 74	eqbrtrrd	$⊢ (((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 \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land (((f \in T \land s \in E) \land R (f \circ {s (G)}^{-1}) \underset{˙}{\leq} X) \land ((f \in T \land R (f) \underset{˙}{\leq} W) \land s = \underset{˙}{0}))) \to R (f) \underset{˙}{\leq} X$
76	5 3 9 10	trlle	$⊢ ((K \in HL \land W \in H) \land f \in T) \to R (f) \underset{˙}{\leq} W$
77	54 51 76	syl2anc	$⊢ (((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 \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land (((f \in T \land s \in E) \land R (f \circ {s (G)}^{-1}) \underset{˙}{\leq} X) \land ((f \in T \land R (f) \underset{˙}{\leq} W) \land s = \underset{˙}{0}))) \to R (f) \underset{˙}{\leq} W$
78		simpl1l	$⊢ (((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 \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land (((f \in T \land s \in E) \land R (f \circ {s (G)}^{-1}) \underset{˙}{\leq} X) \land ((f \in T \land R (f) \underset{˙}{\leq} W) \land s = \underset{˙}{0}))) \to K \in HL$
79	78	hllatd	$⊢ (((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 \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land (((f \in T \land s \in E) \land R (f \circ {s (G)}^{-1}) \underset{˙}{\leq} X) \land ((f \in T \land R (f) \underset{˙}{\leq} W) \land s = \underset{˙}{0}))) \to K \in Lat$
80	1 3 9 10	trlcl	$⊢ ((K \in HL \land W \in H) \land f \in T) \to R (f) \in B$
81	54 51 80	syl2anc	$⊢ (((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 \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land (((f \in T \land s \in E) \land R (f \circ {s (G)}^{-1}) \underset{˙}{\leq} X) \land ((f \in T \land R (f) \underset{˙}{\leq} W) \land s = \underset{˙}{0}))) \to R (f) \in B$
82		simpl2l	$⊢ (((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 \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land (((f \in T \land s \in E) \land R (f \circ {s (G)}^{-1}) \underset{˙}{\leq} X) \land ((f \in T \land R (f) \underset{˙}{\leq} W) \land s = \underset{˙}{0}))) \to X \in B$
83		simpl1r	$⊢ (((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 \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land (((f \in T \land s \in E) \land R (f \circ {s (G)}^{-1}) \underset{˙}{\leq} X) \land ((f \in T \land R (f) \underset{˙}{\leq} W) \land s = \underset{˙}{0}))) \to W \in H$
84	83 17	syl	$⊢ (((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 \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land (((f \in T \land s \in E) \land R (f \circ {s (G)}^{-1}) \underset{˙}{\leq} X) \land ((f \in T \land R (f) \underset{˙}{\leq} W) \land s = \underset{˙}{0}))) \to W \in B$
85	1 5 2	latlem12	$⊢ (K \in Lat \land (R (f) \in B \land X \in B \land W \in B)) \to ((R (f) \underset{˙}{\leq} X \land R (f) \underset{˙}{\leq} W) \leftrightarrow R (f) \underset{˙}{\leq} (X \underset{˙}{\land} W))$
86	79 81 82 84 85	syl13anc	$⊢ (((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 \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land (((f \in T \land s \in E) \land R (f \circ {s (G)}^{-1}) \underset{˙}{\leq} X) \land ((f \in T \land R (f) \underset{˙}{\leq} W) \land s = \underset{˙}{0}))) \to ((R (f) \underset{˙}{\leq} X \land R (f) \underset{˙}{\leq} W) \leftrightarrow R (f) \underset{˙}{\leq} (X \underset{˙}{\land} W))$
87	75 77 86	mpbi2and	$⊢ (((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 \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land (((f \in T \land s \in E) \land R (f \circ {s (G)}^{-1}) \underset{˙}{\leq} X) \land ((f \in T \land R (f) \underset{˙}{\leq} W) \land s = \underset{˙}{0}))) \to R (f) \underset{˙}{\leq} (X \underset{˙}{\land} W)$
88	51 87	jca	$⊢ (((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 \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land (((f \in T \land s \in E) \land R (f \circ {s (G)}^{-1}) \underset{˙}{\leq} X) \land ((f \in T \land R (f) \underset{˙}{\leq} W) \land s = \underset{˙}{0}))) \to (f \in T \land R (f) \underset{˙}{\leq} (X \underset{˙}{\land} W))$
89	79 82 84 22	syl3anc	$⊢ (((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 \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land (((f \in T \land s \in E) \land R (f \circ {s (G)}^{-1}) \underset{˙}{\leq} X) \land ((f \in T \land R (f) \underset{˙}{\leq} W) \land s = \underset{˙}{0}))) \to X \underset{˙}{\land} W \in B$
90	79 82 84 27	syl3anc	$⊢ (((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 \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land (((f \in T \land s \in E) \land R (f \circ {s (G)}^{-1}) \underset{˙}{\leq} X) \land ((f \in T \land R (f) \underset{˙}{\leq} W) \land s = \underset{˙}{0}))) \to (X \underset{˙}{\land} W) \underset{˙}{\leq} W$
91	1 5 3 9 10 13 4	dihopelvalbN	$⊢ ((K \in HL \land W \in H) \land (X \underset{˙}{\land} W \in B \land (X \underset{˙}{\land} W) \underset{˙}{\leq} W)) \to (⟨f, s⟩ \in I (X \underset{˙}{\land} W) \leftrightarrow ((f \in T \land R (f) \underset{˙}{\leq} (X \underset{˙}{\land} W)) \land s = \underset{˙}{0}))$
92	54 89 90 91	syl12anc	$⊢ (((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 \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land (((f \in T \land s \in E) \land R (f \circ {s (G)}^{-1}) \underset{˙}{\leq} X) \land ((f \in T \land R (f) \underset{˙}{\leq} W) \land s = \underset{˙}{0}))) \to (⟨f, s⟩ \in I (X \underset{˙}{\land} W) \leftrightarrow ((f \in T \land R (f) \underset{˙}{\leq} (X \underset{˙}{\land} W)) \land s = \underset{˙}{0}))$
93	88 52 92	mpbir2and	$⊢ (((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 \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land (((f \in T \land s \in E) \land R (f \circ {s (G)}^{-1}) \underset{˙}{\leq} X) \land ((f \in T \land R (f) \underset{˙}{\leq} W) \land s = \underset{˙}{0}))) \to ⟨f, s⟩ \in I (X \underset{˙}{\land} W)$
94	93	ex	$⊢ ((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 \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \to ((((f \in T \land s \in E) \land R (f \circ {s (G)}^{-1}) \underset{˙}{\leq} X) \land ((f \in T \land R (f) \underset{˙}{\leq} W) \land s = \underset{˙}{0})) \to ⟨f, s⟩ \in I (X \underset{˙}{\land} W))$
95	49 94	sylbid	$⊢ ((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 \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \to ((⟨f, s⟩ \in I (X) \land ⟨f, s⟩ \in I (W)) \to ⟨f, s⟩ \in I (X \underset{˙}{\land} W))$
96	95	3expia	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W)) \to (((q \in A \land \neg q \underset{˙}{\leq} W) \land q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X) \to ((⟨f, s⟩ \in I (X) \land ⟨f, s⟩ \in I (W)) \to ⟨f, s⟩ \in I (X \underset{˙}{\land} W)))$
97	96	exp4c	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W)) \to (q \in A \to (\neg q \underset{˙}{\leq} W \to (q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X \to ((⟨f, s⟩ \in I (X) \land ⟨f, s⟩ \in I (W)) \to ⟨f, s⟩ \in I (X \underset{˙}{\land} W)))))$
98	97	imp4a	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W)) \to (q \in A \to ((\neg q \underset{˙}{\leq} W \land q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X) \to ((⟨f, s⟩ \in I (X) \land ⟨f, s⟩ \in I (W)) \to ⟨f, s⟩ \in I (X \underset{˙}{\land} W))))$
99	98	rexlimdv	$⊢ ((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 \underset{˙}{\lor} (X \underset{˙}{\land} W) = X) \to ((⟨f, s⟩ \in I (X) \land ⟨f, s⟩ \in I (W)) \to ⟨f, s⟩ \in I (X \underset{˙}{\land} W)))$
100	38 99	mpd	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W)) \to ((⟨f, s⟩ \in I (X) \land ⟨f, s⟩ \in I (W)) \to ⟨f, s⟩ \in I (X \underset{˙}{\land} W))$
101	37 100	biimtrid	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W)) \to (⟨f, s⟩ \in (I (X) \cap I (W)) \to ⟨f, s⟩ \in I (X \underset{˙}{\land} W))$
102	36 101	relssdv	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W)) \to I (X) \cap I (W) \subseteq I (X \underset{˙}{\land} W)$
103	32 102	eqssd	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W)) \to I (X \underset{˙}{\land} W) = I (X) \cap I (W)$

Metamath Proof Explorer

Theorem dihglblem5apreN

Proof