dihmeetlem1N

Description: Isomorphism H of a conjunction. (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	dihmeetlem1N	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \to I (X \underset{˙}{\land} Y) = I (X) \cap I (Y)$

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		simp1l	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \to K \in HL$
15	14	hllatd	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \to K \in Lat$
16		simp2l	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \to X \in B$
17		simp3l	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \to Y \in B$
18	1 5 2	latmle1	$⊢ (K \in Lat \land X \in B \land Y \in B) \to (X \underset{˙}{\land} Y) \underset{˙}{\leq} X$
19	15 16 17 18	syl3anc	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \to (X \underset{˙}{\land} Y) \underset{˙}{\leq} X$
20		simp1	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \to (K \in HL \land W \in H)$
21	1 2	latmcl	$⊢ (K \in Lat \land X \in B \land Y \in B) \to X \underset{˙}{\land} Y \in B$
22	15 16 17 21	syl3anc	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \to X \underset{˙}{\land} Y \in B$
23	1 5 3 4	dihord	$⊢ ((K \in HL \land W \in H) \land X \underset{˙}{\land} Y \in B \land X \in B) \to (I (X \underset{˙}{\land} Y) \subseteq I (X) \leftrightarrow (X \underset{˙}{\land} Y) \underset{˙}{\leq} X)$
24	20 22 16 23	syl3anc	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \to (I (X \underset{˙}{\land} Y) \subseteq I (X) \leftrightarrow (X \underset{˙}{\land} Y) \underset{˙}{\leq} X)$
25	19 24	mpbird	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \to I (X \underset{˙}{\land} Y) \subseteq I (X)$
26	1 5 2	latmle2	$⊢ (K \in Lat \land X \in B \land Y \in B) \to (X \underset{˙}{\land} Y) \underset{˙}{\leq} Y$
27	15 16 17 26	syl3anc	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \to (X \underset{˙}{\land} Y) \underset{˙}{\leq} Y$
28	1 5 3 4	dihord	$⊢ ((K \in HL \land W \in H) \land X \underset{˙}{\land} Y \in B \land Y \in B) \to (I (X \underset{˙}{\land} Y) \subseteq I (Y) \leftrightarrow (X \underset{˙}{\land} Y) \underset{˙}{\leq} Y)$
29	20 22 17 28	syl3anc	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \to (I (X \underset{˙}{\land} Y) \subseteq I (Y) \leftrightarrow (X \underset{˙}{\land} Y) \underset{˙}{\leq} Y)$
30	27 29	mpbird	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \to I (X \underset{˙}{\land} Y) \subseteq I (Y)$
31	25 30	ssind	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \to I (X \underset{˙}{\land} Y) \subseteq I (X) \cap I (Y)$
32	3 4	dihvalrel	$⊢ (K \in HL \land W \in H) \to Rel I (X)$
33		relin1	$⊢ Rel I (X) \to Rel (I (X) \cap I (Y))$
34	32 33	syl	$⊢ (K \in HL \land W \in H) \to Rel (I (X) \cap I (Y))$
35	34	3ad2ant1	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \to Rel (I (X) \cap I (Y))$
36		elin	$⊢ ⟨f, s⟩ \in (I (X) \cap I (Y)) \leftrightarrow (⟨f, s⟩ \in I (X) \land ⟨f, s⟩ \in I (Y))$
37	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)$
38	37	3adant3	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \to \exists q \in A (\neg q \underset{˙}{\leq} W \land q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)$
39		simpl1	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \land (q \in A \land (\neg q \underset{˙}{\leq} W \land q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X))) \to (K \in HL \land W \in H)$
40		simpl2	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \land (q \in A \land (\neg q \underset{˙}{\leq} W \land q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X))) \to (X \in B \land \neg X \underset{˙}{\leq} W)$
41		simprl	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \land (q \in A \land (\neg q \underset{˙}{\leq} W \land q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X))) \to q \in A$
42		simprrl	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \land (q \in A \land (\neg q \underset{˙}{\leq} W \land q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X))) \to \neg q \underset{˙}{\leq} W$
43	41 42	jca	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \land (q \in A \land (\neg q \underset{˙}{\leq} W \land q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X))) \to (q \in A \land \neg q \underset{˙}{\leq} W)$
44		simprrr	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \land (q \in A \land (\neg q \underset{˙}{\leq} W \land q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X))) \to q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X$
45		vex	$⊢ f \in V$
46		vex	$⊢ s \in V$
47	1 5 6 2 7 3 8 9 10 11 4 12 45 46	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))$
48	39 40 43 44 47	syl112anc	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Y \in B \land Y \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))$
49		simpr	$⊢ ((f \in T \land s \in E) \land R (f \circ {s (G)}^{-1}) \underset{˙}{\leq} X) \to R (f \circ {s (G)}^{-1}) \underset{˙}{\leq} X$
50	48 49	syl6bi	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Y \in B \land Y \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) \to R (f \circ {s (G)}^{-1}) \underset{˙}{\leq} X)$
51		simpl3	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \land (q \in A \land (\neg q \underset{˙}{\leq} W \land q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X))) \to (Y \in B \land Y \underset{˙}{\leq} W)$
52	1 5 3 9 10 13 4	dihopelvalbN	$⊢ ((K \in HL \land W \in H) \land (Y \in B \land Y \underset{˙}{\leq} W)) \to (⟨f, s⟩ \in I (Y) \leftrightarrow ((f \in T \land R (f) \underset{˙}{\leq} Y) \land s = \underset{˙}{0}))$
53	39 51 52	syl2anc	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Y \in B \land Y \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 (Y) \leftrightarrow ((f \in T \land R (f) \underset{˙}{\leq} Y) \land s = \underset{˙}{0}))$
54	53	biimpd	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Y \in B \land Y \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 (Y) \to ((f \in T \land R (f) \underset{˙}{\leq} Y) \land s = \underset{˙}{0}))$
55		simprll	$⊢ (R (f \circ {s (G)}^{-1}) \underset{˙}{\leq} X \land ((f \in T \land R (f) \underset{˙}{\leq} Y) \land s = \underset{˙}{0})) \to f \in T$
56	55	3ad2ant3	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \land (q \in A \land (\neg q \underset{˙}{\leq} W \land q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land (R (f \circ {s (G)}^{-1}) \underset{˙}{\leq} X \land ((f \in T \land R (f) \underset{˙}{\leq} Y) \land s = \underset{˙}{0}))) \to f \in T$
57		simp3rr	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \land (q \in A \land (\neg q \underset{˙}{\leq} W \land q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land (R (f \circ {s (G)}^{-1}) \underset{˙}{\leq} X \land ((f \in T \land R (f) \underset{˙}{\leq} Y) \land s = \underset{˙}{0}))) \to s = \underset{˙}{0}$
58	57	fveq1d	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \land (q \in A \land (\neg q \underset{˙}{\leq} W \land q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land (R (f \circ {s (G)}^{-1}) \underset{˙}{\leq} X \land ((f \in T \land R (f) \underset{˙}{\leq} Y) \land s = \underset{˙}{0}))) \to s (G) = \underset{˙}{0} (G)$
59		simp11	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \land (q \in A \land (\neg q \underset{˙}{\leq} W \land q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land (R (f \circ {s (G)}^{-1}) \underset{˙}{\leq} X \land ((f \in T \land R (f) \underset{˙}{\leq} Y) \land s = \underset{˙}{0}))) \to (K \in HL \land W \in H)$
60	5 7 3 8	lhpocnel2	$⊢ (K \in HL \land W \in H) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
61	59 60	syl	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \land (q \in A \land (\neg q \underset{˙}{\leq} W \land q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land (R (f \circ {s (G)}^{-1}) \underset{˙}{\leq} X \land ((f \in T \land R (f) \underset{˙}{\leq} Y) \land s = \underset{˙}{0}))) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
62		simp2l	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \land (q \in A \land (\neg q \underset{˙}{\leq} W \land q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land (R (f \circ {s (G)}^{-1}) \underset{˙}{\leq} X \land ((f \in T \land R (f) \underset{˙}{\leq} Y) \land s = \underset{˙}{0}))) \to q \in A$
63		simp2rl	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \land (q \in A \land (\neg q \underset{˙}{\leq} W \land q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land (R (f \circ {s (G)}^{-1}) \underset{˙}{\leq} X \land ((f \in T \land R (f) \underset{˙}{\leq} Y) \land s = \underset{˙}{0}))) \to \neg q \underset{˙}{\leq} W$
64	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$
65	59 61 62 63 64	syl112anc	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \land (q \in A \land (\neg q \underset{˙}{\leq} W \land q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land (R (f \circ {s (G)}^{-1}) \underset{˙}{\leq} X \land ((f \in T \land R (f) \underset{˙}{\leq} Y) \land s = \underset{˙}{0}))) \to G \in T$
66	13 1	tendo02	$⊢ G \in T \to \underset{˙}{0} (G) = {I ↾}_{B}$
67	65 66	syl	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \land (q \in A \land (\neg q \underset{˙}{\leq} W \land q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land (R (f \circ {s (G)}^{-1}) \underset{˙}{\leq} X \land ((f \in T \land R (f) \underset{˙}{\leq} Y) \land s = \underset{˙}{0}))) \to \underset{˙}{0} (G) = {I ↾}_{B}$
68	58 67	eqtrd	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \land (q \in A \land (\neg q \underset{˙}{\leq} W \land q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land (R (f \circ {s (G)}^{-1}) \underset{˙}{\leq} X \land ((f \in T \land R (f) \underset{˙}{\leq} Y) \land s = \underset{˙}{0}))) \to s (G) = {I ↾}_{B}$
69	68	cnveqd	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \land (q \in A \land (\neg q \underset{˙}{\leq} W \land q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land (R (f \circ {s (G)}^{-1}) \underset{˙}{\leq} X \land ((f \in T \land R (f) \underset{˙}{\leq} Y) \land s = \underset{˙}{0}))) \to {s (G)}^{-1} = {({I ↾}_{B})}^{-1}$
70		cnvresid	$⊢ {({I ↾}_{B})}^{-1} = {I ↾}_{B}$
71	69 70	eqtrdi	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \land (q \in A \land (\neg q \underset{˙}{\leq} W \land q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land (R (f \circ {s (G)}^{-1}) \underset{˙}{\leq} X \land ((f \in T \land R (f) \underset{˙}{\leq} Y) \land s = \underset{˙}{0}))) \to {s (G)}^{-1} = {I ↾}_{B}$
72	71	coeq2d	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \land (q \in A \land (\neg q \underset{˙}{\leq} W \land q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land (R (f \circ {s (G)}^{-1}) \underset{˙}{\leq} X \land ((f \in T \land R (f) \underset{˙}{\leq} Y) \land s = \underset{˙}{0}))) \to f \circ {s (G)}^{-1} = f \circ ({I ↾}_{B})$
73	1 3 9	ltrn1o	$⊢ ((K \in HL \land W \in H) \land f \in T) \to f : B \underset{1-1 onto}{⟶} B$
74	59 56 73	syl2anc	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \land (q \in A \land (\neg q \underset{˙}{\leq} W \land q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land (R (f \circ {s (G)}^{-1}) \underset{˙}{\leq} X \land ((f \in T \land R (f) \underset{˙}{\leq} Y) \land s = \underset{˙}{0}))) \to f : B \underset{1-1 onto}{⟶} B$
75		f1of	$⊢ f : B \underset{1-1 onto}{⟶} B \to f : B ⟶ B$
76		fcoi1	$⊢ f : B ⟶ B \to f \circ ({I ↾}_{B}) = f$
77	74 75 76	3syl	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \land (q \in A \land (\neg q \underset{˙}{\leq} W \land q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land (R (f \circ {s (G)}^{-1}) \underset{˙}{\leq} X \land ((f \in T \land R (f) \underset{˙}{\leq} Y) \land s = \underset{˙}{0}))) \to f \circ ({I ↾}_{B}) = f$
78	72 77	eqtrd	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \land (q \in A \land (\neg q \underset{˙}{\leq} W \land q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land (R (f \circ {s (G)}^{-1}) \underset{˙}{\leq} X \land ((f \in T \land R (f) \underset{˙}{\leq} Y) \land s = \underset{˙}{0}))) \to f \circ {s (G)}^{-1} = f$
79	78	fveq2d	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \land (q \in A \land (\neg q \underset{˙}{\leq} W \land q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land (R (f \circ {s (G)}^{-1}) \underset{˙}{\leq} X \land ((f \in T \land R (f) \underset{˙}{\leq} Y) \land s = \underset{˙}{0}))) \to R (f \circ {s (G)}^{-1}) = R (f)$
80		simp3l	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \land (q \in A \land (\neg q \underset{˙}{\leq} W \land q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land (R (f \circ {s (G)}^{-1}) \underset{˙}{\leq} X \land ((f \in T \land R (f) \underset{˙}{\leq} Y) \land s = \underset{˙}{0}))) \to R (f \circ {s (G)}^{-1}) \underset{˙}{\leq} X$
81	79 80	eqbrtrrd	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \land (q \in A \land (\neg q \underset{˙}{\leq} W \land q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land (R (f \circ {s (G)}^{-1}) \underset{˙}{\leq} X \land ((f \in T \land R (f) \underset{˙}{\leq} Y) \land s = \underset{˙}{0}))) \to R (f) \underset{˙}{\leq} X$
82		simprlr	$⊢ (R (f \circ {s (G)}^{-1}) \underset{˙}{\leq} X \land ((f \in T \land R (f) \underset{˙}{\leq} Y) \land s = \underset{˙}{0})) \to R (f) \underset{˙}{\leq} Y$
83	82	3ad2ant3	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \land (q \in A \land (\neg q \underset{˙}{\leq} W \land q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land (R (f \circ {s (G)}^{-1}) \underset{˙}{\leq} X \land ((f \in T \land R (f) \underset{˙}{\leq} Y) \land s = \underset{˙}{0}))) \to R (f) \underset{˙}{\leq} Y$
84		simp11l	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \land (q \in A \land (\neg q \underset{˙}{\leq} W \land q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land (R (f \circ {s (G)}^{-1}) \underset{˙}{\leq} X \land ((f \in T \land R (f) \underset{˙}{\leq} Y) \land s = \underset{˙}{0}))) \to K \in HL$
85	84	hllatd	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \land (q \in A \land (\neg q \underset{˙}{\leq} W \land q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land (R (f \circ {s (G)}^{-1}) \underset{˙}{\leq} X \land ((f \in T \land R (f) \underset{˙}{\leq} Y) \land s = \underset{˙}{0}))) \to K \in Lat$
86	1 3 9 10	trlcl	$⊢ ((K \in HL \land W \in H) \land f \in T) \to R (f) \in B$
87	59 56 86	syl2anc	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \land (q \in A \land (\neg q \underset{˙}{\leq} W \land q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land (R (f \circ {s (G)}^{-1}) \underset{˙}{\leq} X \land ((f \in T \land R (f) \underset{˙}{\leq} Y) \land s = \underset{˙}{0}))) \to R (f) \in B$
88		simp12l	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \land (q \in A \land (\neg q \underset{˙}{\leq} W \land q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land (R (f \circ {s (G)}^{-1}) \underset{˙}{\leq} X \land ((f \in T \land R (f) \underset{˙}{\leq} Y) \land s = \underset{˙}{0}))) \to X \in B$
89		simp13l	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \land (q \in A \land (\neg q \underset{˙}{\leq} W \land q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land (R (f \circ {s (G)}^{-1}) \underset{˙}{\leq} X \land ((f \in T \land R (f) \underset{˙}{\leq} Y) \land s = \underset{˙}{0}))) \to Y \in B$
90	1 5 2	latlem12	$⊢ (K \in Lat \land (R (f) \in B \land X \in B \land Y \in B)) \to ((R (f) \underset{˙}{\leq} X \land R (f) \underset{˙}{\leq} Y) \leftrightarrow R (f) \underset{˙}{\leq} (X \underset{˙}{\land} Y))$
91	85 87 88 89 90	syl13anc	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \land (q \in A \land (\neg q \underset{˙}{\leq} W \land q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land (R (f \circ {s (G)}^{-1}) \underset{˙}{\leq} X \land ((f \in T \land R (f) \underset{˙}{\leq} Y) \land s = \underset{˙}{0}))) \to ((R (f) \underset{˙}{\leq} X \land R (f) \underset{˙}{\leq} Y) \leftrightarrow R (f) \underset{˙}{\leq} (X \underset{˙}{\land} Y))$
92	81 83 91	mpbi2and	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \land (q \in A \land (\neg q \underset{˙}{\leq} W \land q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land (R (f \circ {s (G)}^{-1}) \underset{˙}{\leq} X \land ((f \in T \land R (f) \underset{˙}{\leq} Y) \land s = \underset{˙}{0}))) \to R (f) \underset{˙}{\leq} (X \underset{˙}{\land} Y)$
93	56 92	jca	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \land (q \in A \land (\neg q \underset{˙}{\leq} W \land q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land (R (f \circ {s (G)}^{-1}) \underset{˙}{\leq} X \land ((f \in T \land R (f) \underset{˙}{\leq} Y) \land s = \underset{˙}{0}))) \to (f \in T \land R (f) \underset{˙}{\leq} (X \underset{˙}{\land} Y))$
94	85 88 89 21	syl3anc	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \land (q \in A \land (\neg q \underset{˙}{\leq} W \land q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land (R (f \circ {s (G)}^{-1}) \underset{˙}{\leq} X \land ((f \in T \land R (f) \underset{˙}{\leq} Y) \land s = \underset{˙}{0}))) \to X \underset{˙}{\land} Y \in B$
95		simp11r	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \land (q \in A \land (\neg q \underset{˙}{\leq} W \land q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land (R (f \circ {s (G)}^{-1}) \underset{˙}{\leq} X \land ((f \in T \land R (f) \underset{˙}{\leq} Y) \land s = \underset{˙}{0}))) \to W \in H$
96	1 3	lhpbase	$⊢ W \in H \to W \in B$
97	95 96	syl	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \land (q \in A \land (\neg q \underset{˙}{\leq} W \land q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land (R (f \circ {s (G)}^{-1}) \underset{˙}{\leq} X \land ((f \in T \land R (f) \underset{˙}{\leq} Y) \land s = \underset{˙}{0}))) \to W \in B$
98	85 88 89 26	syl3anc	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \land (q \in A \land (\neg q \underset{˙}{\leq} W \land q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land (R (f \circ {s (G)}^{-1}) \underset{˙}{\leq} X \land ((f \in T \land R (f) \underset{˙}{\leq} Y) \land s = \underset{˙}{0}))) \to (X \underset{˙}{\land} Y) \underset{˙}{\leq} Y$
99		simp13r	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \land (q \in A \land (\neg q \underset{˙}{\leq} W \land q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land (R (f \circ {s (G)}^{-1}) \underset{˙}{\leq} X \land ((f \in T \land R (f) \underset{˙}{\leq} Y) \land s = \underset{˙}{0}))) \to Y \underset{˙}{\leq} W$
100	1 5 85 94 89 97 98 99	lattrd	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \land (q \in A \land (\neg q \underset{˙}{\leq} W \land q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land (R (f \circ {s (G)}^{-1}) \underset{˙}{\leq} X \land ((f \in T \land R (f) \underset{˙}{\leq} Y) \land s = \underset{˙}{0}))) \to (X \underset{˙}{\land} Y) \underset{˙}{\leq} W$
101	1 5 3 9 10 13 4	dihopelvalbN	$⊢ ((K \in HL \land W \in H) \land (X \underset{˙}{\land} Y \in B \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} W)) \to (⟨f, s⟩ \in I (X \underset{˙}{\land} Y) \leftrightarrow ((f \in T \land R (f) \underset{˙}{\leq} (X \underset{˙}{\land} Y)) \land s = \underset{˙}{0}))$
102	59 94 100 101	syl12anc	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \land (q \in A \land (\neg q \underset{˙}{\leq} W \land q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land (R (f \circ {s (G)}^{-1}) \underset{˙}{\leq} X \land ((f \in T \land R (f) \underset{˙}{\leq} Y) \land s = \underset{˙}{0}))) \to (⟨f, s⟩ \in I (X \underset{˙}{\land} Y) \leftrightarrow ((f \in T \land R (f) \underset{˙}{\leq} (X \underset{˙}{\land} Y)) \land s = \underset{˙}{0}))$
103	93 57 102	mpbir2and	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \land (q \in A \land (\neg q \underset{˙}{\leq} W \land q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land (R (f \circ {s (G)}^{-1}) \underset{˙}{\leq} X \land ((f \in T \land R (f) \underset{˙}{\leq} Y) \land s = \underset{˙}{0}))) \to ⟨f, s⟩ \in I (X \underset{˙}{\land} Y)$
104	103	3expia	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \land (q \in A \land (\neg q \underset{˙}{\leq} W \land q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X))) \to ((R (f \circ {s (G)}^{-1}) \underset{˙}{\leq} X \land ((f \in T \land R (f) \underset{˙}{\leq} Y) \land s = \underset{˙}{0})) \to ⟨f, s⟩ \in I (X \underset{˙}{\land} Y))$
105	50 54 104	syl2and	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Y \in B \land Y \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 (Y)) \to ⟨f, s⟩ \in I (X \underset{˙}{\land} Y))$
106	38 105	rexlimddv	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \to ((⟨f, s⟩ \in I (X) \land ⟨f, s⟩ \in I (Y)) \to ⟨f, s⟩ \in I (X \underset{˙}{\land} Y))$
107	36 106	syl5bi	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \to (⟨f, s⟩ \in (I (X) \cap I (Y)) \to ⟨f, s⟩ \in I (X \underset{˙}{\land} Y))$
108	35 107	relssdv	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \to I (X) \cap I (Y) \subseteq I (X \underset{˙}{\land} Y)$
109	31 108	eqssd	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \to I (X \underset{˙}{\land} Y) = I (X) \cap I (Y)$

Metamath Proof Explorer

Theorem dihmeetlem1N

Proof