dihglblem2N

Description: The GLB of a set of lattice elements S is the same as that of the set T with elements of S cut down to be under W . (Contributed by NM, 19-Mar-2014) (New usage is discouraged.)

	Ref	Expression
Hypotheses	dihglblem.b	$⊢ B = {Base}_{K}$
	dihglblem.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	dihglblem.m	$⊢ \underset{˙}{\land} = meet (K)$
	dihglblem.g	$⊢ G = glb (K)$
	dihglblem.h	$⊢ H = LHyp (K)$
	dihglblem.t	$⊢ T = \{u \in B \| \exists v \in S u = v \underset{˙}{\land} W\}$
Assertion	dihglblem2N	$⊢ ((K \in HL \land W \in H) \land S \subseteq B \land G (S) \underset{˙}{\leq} W) \to G (S) = G (T)$

Proof

Step	Hyp	Ref	Expression
1		dihglblem.b	$⊢ B = {Base}_{K}$
2		dihglblem.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		dihglblem.m	$⊢ \underset{˙}{\land} = meet (K)$
4		dihglblem.g	$⊢ G = glb (K)$
5		dihglblem.h	$⊢ H = LHyp (K)$
6		dihglblem.t	$⊢ T = \{u \in B \| \exists v \in S u = v \underset{˙}{\land} W\}$
7		simpl1l	$⊢ (((K \in HL \land W \in H) \land S \subseteq B \land G (S) \underset{˙}{\leq} W) \land x \in S) \to K \in HL$
8	7	hllatd	$⊢ (((K \in HL \land W \in H) \land S \subseteq B \land G (S) \underset{˙}{\leq} W) \land x \in S) \to K \in Lat$
9		simp1l	$⊢ ((K \in HL \land W \in H) \land S \subseteq B \land G (S) \underset{˙}{\leq} W) \to K \in HL$
10		hlclat	$⊢ K \in HL \to K \in CLat$
11	9 10	syl	$⊢ ((K \in HL \land W \in H) \land S \subseteq B \land G (S) \underset{˙}{\leq} W) \to K \in CLat$
12		ssrab2	$⊢ \{u \in B \| \exists v \in S u = v \underset{˙}{\land} W\} \subseteq B$
13	6 12	eqsstri	$⊢ T \subseteq B$
14	1 4	clatglbcl	$⊢ (K \in CLat \land T \subseteq B) \to G (T) \in B$
15	11 13 14	sylancl	$⊢ ((K \in HL \land W \in H) \land S \subseteq B \land G (S) \underset{˙}{\leq} W) \to G (T) \in B$
16	15	adantr	$⊢ (((K \in HL \land W \in H) \land S \subseteq B \land G (S) \underset{˙}{\leq} W) \land x \in S) \to G (T) \in B$
17		simpl2	$⊢ (((K \in HL \land W \in H) \land S \subseteq B \land G (S) \underset{˙}{\leq} W) \land x \in S) \to S \subseteq B$
18		simpr	$⊢ (((K \in HL \land W \in H) \land S \subseteq B \land G (S) \underset{˙}{\leq} W) \land x \in S) \to x \in S$
19	17 18	sseldd	$⊢ (((K \in HL \land W \in H) \land S \subseteq B \land G (S) \underset{˙}{\leq} W) \land x \in S) \to x \in B$
20		simpl1r	$⊢ (((K \in HL \land W \in H) \land S \subseteq B \land G (S) \underset{˙}{\leq} W) \land x \in S) \to W \in H$
21	1 5	lhpbase	$⊢ W \in H \to W \in B$
22	20 21	syl	$⊢ (((K \in HL \land W \in H) \land S \subseteq B \land G (S) \underset{˙}{\leq} W) \land x \in S) \to W \in B$
23	1 3	latmcl	$⊢ (K \in Lat \land x \in B \land W \in B) \to x \underset{˙}{\land} W \in B$
24	8 19 22 23	syl3anc	$⊢ (((K \in HL \land W \in H) \land S \subseteq B \land G (S) \underset{˙}{\leq} W) \land x \in S) \to x \underset{˙}{\land} W \in B$
25	7 10	syl	$⊢ (((K \in HL \land W \in H) \land S \subseteq B \land G (S) \underset{˙}{\leq} W) \land x \in S) \to K \in CLat$
26		eqidd	$⊢ (((K \in HL \land W \in H) \land S \subseteq B \land G (S) \underset{˙}{\leq} W) \land x \in S) \to x \underset{˙}{\land} W = x \underset{˙}{\land} W$
27		oveq1	$⊢ v = x \to v \underset{˙}{\land} W = x \underset{˙}{\land} W$
28	27	rspceeqv	$⊢ (x \in S \land x \underset{˙}{\land} W = x \underset{˙}{\land} W) \to \exists v \in S x \underset{˙}{\land} W = v \underset{˙}{\land} W$
29	18 26 28	syl2anc	$⊢ (((K \in HL \land W \in H) \land S \subseteq B \land G (S) \underset{˙}{\leq} W) \land x \in S) \to \exists v \in S x \underset{˙}{\land} W = v \underset{˙}{\land} W$
30		eqeq1	$⊢ u = x \underset{˙}{\land} W \to (u = v \underset{˙}{\land} W \leftrightarrow x \underset{˙}{\land} W = v \underset{˙}{\land} W)$
31	30	rexbidv	$⊢ u = x \underset{˙}{\land} W \to (\exists v \in S u = v \underset{˙}{\land} W \leftrightarrow \exists v \in S x \underset{˙}{\land} W = v \underset{˙}{\land} W)$
32	31	elrab	$⊢ x \underset{˙}{\land} W \in \{u \in B \| \exists v \in S u = v \underset{˙}{\land} W\} \leftrightarrow (x \underset{˙}{\land} W \in B \land \exists v \in S x \underset{˙}{\land} W = v \underset{˙}{\land} W)$
33	24 29 32	sylanbrc	$⊢ (((K \in HL \land W \in H) \land S \subseteq B \land G (S) \underset{˙}{\leq} W) \land x \in S) \to x \underset{˙}{\land} W \in \{u \in B \| \exists v \in S u = v \underset{˙}{\land} W\}$
34	33 6	eleqtrrdi	$⊢ (((K \in HL \land W \in H) \land S \subseteq B \land G (S) \underset{˙}{\leq} W) \land x \in S) \to x \underset{˙}{\land} W \in T$
35	1 2 4	clatglble	$⊢ (K \in CLat \land T \subseteq B \land x \underset{˙}{\land} W \in T) \to G (T) \underset{˙}{\leq} (x \underset{˙}{\land} W)$
36	13 35	mp3an2	$⊢ (K \in CLat \land x \underset{˙}{\land} W \in T) \to G (T) \underset{˙}{\leq} (x \underset{˙}{\land} W)$
37	25 34 36	syl2anc	$⊢ (((K \in HL \land W \in H) \land S \subseteq B \land G (S) \underset{˙}{\leq} W) \land x \in S) \to G (T) \underset{˙}{\leq} (x \underset{˙}{\land} W)$
38	1 2 3	latmle1	$⊢ (K \in Lat \land x \in B \land W \in B) \to (x \underset{˙}{\land} W) \underset{˙}{\leq} x$
39	8 19 22 38	syl3anc	$⊢ (((K \in HL \land W \in H) \land S \subseteq B \land G (S) \underset{˙}{\leq} W) \land x \in S) \to (x \underset{˙}{\land} W) \underset{˙}{\leq} x$
40	1 2 8 16 24 19 37 39	lattrd	$⊢ (((K \in HL \land W \in H) \land S \subseteq B \land G (S) \underset{˙}{\leq} W) \land x \in S) \to G (T) \underset{˙}{\leq} x$
41		eqeq1	$⊢ u = w \to (u = v \underset{˙}{\land} W \leftrightarrow w = v \underset{˙}{\land} W)$
42	41	rexbidv	$⊢ u = w \to (\exists v \in S u = v \underset{˙}{\land} W \leftrightarrow \exists v \in S w = v \underset{˙}{\land} W)$
43		oveq1	$⊢ v = y \to v \underset{˙}{\land} W = y \underset{˙}{\land} W$
44	43	eqeq2d	$⊢ v = y \to (w = v \underset{˙}{\land} W \leftrightarrow w = y \underset{˙}{\land} W)$
45	44	cbvrexvw	$⊢ \exists v \in S w = v \underset{˙}{\land} W \leftrightarrow \exists y \in S w = y \underset{˙}{\land} W$
46	42 45	bitrdi	$⊢ u = w \to (\exists v \in S u = v \underset{˙}{\land} W \leftrightarrow \exists y \in S w = y \underset{˙}{\land} W)$
47	46 6	elrab2	$⊢ w \in T \leftrightarrow (w \in B \land \exists y \in S w = y \underset{˙}{\land} W)$
48		simp3	$⊢ ((((K \in HL \land W \in H) \land S \subseteq B \land G (S) \underset{˙}{\leq} W) \land z \in B \land \forall x \in S z \underset{˙}{\leq} x) \land w \in B \land y \in S) \to y \in S$
49		simp13	$⊢ ((((K \in HL \land W \in H) \land S \subseteq B \land G (S) \underset{˙}{\leq} W) \land z \in B \land \forall x \in S z \underset{˙}{\leq} x) \land w \in B \land y \in S) \to \forall x \in S z \underset{˙}{\leq} x$
50		breq2	$⊢ x = y \to (z \underset{˙}{\leq} x \leftrightarrow z \underset{˙}{\leq} y)$
51	50	rspcva	$⊢ (y \in S \land \forall x \in S z \underset{˙}{\leq} x) \to z \underset{˙}{\leq} y$
52	48 49 51	syl2anc	$⊢ ((((K \in HL \land W \in H) \land S \subseteq B \land G (S) \underset{˙}{\leq} W) \land z \in B \land \forall x \in S z \underset{˙}{\leq} x) \land w \in B \land y \in S) \to z \underset{˙}{\leq} y$
53		simp11l	$⊢ (((K \in HL \land W \in H) \land S \subseteq B \land G (S) \underset{˙}{\leq} W) \land z \in B \land \forall x \in S z \underset{˙}{\leq} x) \to K \in HL$
54	53	3ad2ant1	$⊢ ((((K \in HL \land W \in H) \land S \subseteq B \land G (S) \underset{˙}{\leq} W) \land z \in B \land \forall x \in S z \underset{˙}{\leq} x) \land w \in B \land y \in S) \to K \in HL$
55	54	hllatd	$⊢ ((((K \in HL \land W \in H) \land S \subseteq B \land G (S) \underset{˙}{\leq} W) \land z \in B \land \forall x \in S z \underset{˙}{\leq} x) \land w \in B \land y \in S) \to K \in Lat$
56		simp12	$⊢ ((((K \in HL \land W \in H) \land S \subseteq B \land G (S) \underset{˙}{\leq} W) \land z \in B \land \forall x \in S z \underset{˙}{\leq} x) \land w \in B \land y \in S) \to z \in B$
57	54 10	syl	$⊢ ((((K \in HL \land W \in H) \land S \subseteq B \land G (S) \underset{˙}{\leq} W) \land z \in B \land \forall x \in S z \underset{˙}{\leq} x) \land w \in B \land y \in S) \to K \in CLat$
58		simp112	$⊢ ((((K \in HL \land W \in H) \land S \subseteq B \land G (S) \underset{˙}{\leq} W) \land z \in B \land \forall x \in S z \underset{˙}{\leq} x) \land w \in B \land y \in S) \to S \subseteq B$
59	1 4	clatglbcl	$⊢ (K \in CLat \land S \subseteq B) \to G (S) \in B$
60	57 58 59	syl2anc	$⊢ ((((K \in HL \land W \in H) \land S \subseteq B \land G (S) \underset{˙}{\leq} W) \land z \in B \land \forall x \in S z \underset{˙}{\leq} x) \land w \in B \land y \in S) \to G (S) \in B$
61		simp11r	$⊢ (((K \in HL \land W \in H) \land S \subseteq B \land G (S) \underset{˙}{\leq} W) \land z \in B \land \forall x \in S z \underset{˙}{\leq} x) \to W \in H$
62	61	3ad2ant1	$⊢ ((((K \in HL \land W \in H) \land S \subseteq B \land G (S) \underset{˙}{\leq} W) \land z \in B \land \forall x \in S z \underset{˙}{\leq} x) \land w \in B \land y \in S) \to W \in H$
63	62 21	syl	$⊢ ((((K \in HL \land W \in H) \land S \subseteq B \land G (S) \underset{˙}{\leq} W) \land z \in B \land \forall x \in S z \underset{˙}{\leq} x) \land w \in B \land y \in S) \to W \in B$
64	1 2 4	clatleglb	$⊢ (K \in CLat \land z \in B \land S \subseteq B) \to (z \underset{˙}{\leq} G (S) \leftrightarrow \forall x \in S z \underset{˙}{\leq} x)$
65	57 56 58 64	syl3anc	$⊢ ((((K \in HL \land W \in H) \land S \subseteq B \land G (S) \underset{˙}{\leq} W) \land z \in B \land \forall x \in S z \underset{˙}{\leq} x) \land w \in B \land y \in S) \to (z \underset{˙}{\leq} G (S) \leftrightarrow \forall x \in S z \underset{˙}{\leq} x)$
66	49 65	mpbird	$⊢ ((((K \in HL \land W \in H) \land S \subseteq B \land G (S) \underset{˙}{\leq} W) \land z \in B \land \forall x \in S z \underset{˙}{\leq} x) \land w \in B \land y \in S) \to z \underset{˙}{\leq} G (S)$
67		simp113	$⊢ ((((K \in HL \land W \in H) \land S \subseteq B \land G (S) \underset{˙}{\leq} W) \land z \in B \land \forall x \in S z \underset{˙}{\leq} x) \land w \in B \land y \in S) \to G (S) \underset{˙}{\leq} W$
68	1 2 55 56 60 63 66 67	lattrd	$⊢ ((((K \in HL \land W \in H) \land S \subseteq B \land G (S) \underset{˙}{\leq} W) \land z \in B \land \forall x \in S z \underset{˙}{\leq} x) \land w \in B \land y \in S) \to z \underset{˙}{\leq} W$
69	58 48	sseldd	$⊢ ((((K \in HL \land W \in H) \land S \subseteq B \land G (S) \underset{˙}{\leq} W) \land z \in B \land \forall x \in S z \underset{˙}{\leq} x) \land w \in B \land y \in S) \to y \in B$
70	1 2 3	latlem12	$⊢ (K \in Lat \land (z \in B \land y \in B \land W \in B)) \to ((z \underset{˙}{\leq} y \land z \underset{˙}{\leq} W) \leftrightarrow z \underset{˙}{\leq} (y \underset{˙}{\land} W))$
71	55 56 69 63 70	syl13anc	$⊢ ((((K \in HL \land W \in H) \land S \subseteq B \land G (S) \underset{˙}{\leq} W) \land z \in B \land \forall x \in S z \underset{˙}{\leq} x) \land w \in B \land y \in S) \to ((z \underset{˙}{\leq} y \land z \underset{˙}{\leq} W) \leftrightarrow z \underset{˙}{\leq} (y \underset{˙}{\land} W))$
72	52 68 71	mpbi2and	$⊢ ((((K \in HL \land W \in H) \land S \subseteq B \land G (S) \underset{˙}{\leq} W) \land z \in B \land \forall x \in S z \underset{˙}{\leq} x) \land w \in B \land y \in S) \to z \underset{˙}{\leq} (y \underset{˙}{\land} W)$
73	72	3expia	$⊢ ((((K \in HL \land W \in H) \land S \subseteq B \land G (S) \underset{˙}{\leq} W) \land z \in B \land \forall x \in S z \underset{˙}{\leq} x) \land w \in B) \to (y \in S \to z \underset{˙}{\leq} (y \underset{˙}{\land} W))$
74		breq2	$⊢ w = y \underset{˙}{\land} W \to (z \underset{˙}{\leq} w \leftrightarrow z \underset{˙}{\leq} (y \underset{˙}{\land} W))$
75	74	biimprcd	$⊢ z \underset{˙}{\leq} (y \underset{˙}{\land} W) \to (w = y \underset{˙}{\land} W \to z \underset{˙}{\leq} w)$
76	73 75	syl6	$⊢ ((((K \in HL \land W \in H) \land S \subseteq B \land G (S) \underset{˙}{\leq} W) \land z \in B \land \forall x \in S z \underset{˙}{\leq} x) \land w \in B) \to (y \in S \to (w = y \underset{˙}{\land} W \to z \underset{˙}{\leq} w))$
77	76	rexlimdv	$⊢ ((((K \in HL \land W \in H) \land S \subseteq B \land G (S) \underset{˙}{\leq} W) \land z \in B \land \forall x \in S z \underset{˙}{\leq} x) \land w \in B) \to (\exists y \in S w = y \underset{˙}{\land} W \to z \underset{˙}{\leq} w)$
78	77	expimpd	$⊢ (((K \in HL \land W \in H) \land S \subseteq B \land G (S) \underset{˙}{\leq} W) \land z \in B \land \forall x \in S z \underset{˙}{\leq} x) \to ((w \in B \land \exists y \in S w = y \underset{˙}{\land} W) \to z \underset{˙}{\leq} w)$
79	47 78	syl5bi	$⊢ (((K \in HL \land W \in H) \land S \subseteq B \land G (S) \underset{˙}{\leq} W) \land z \in B \land \forall x \in S z \underset{˙}{\leq} x) \to (w \in T \to z \underset{˙}{\leq} w)$
80	79	ralrimiv	$⊢ (((K \in HL \land W \in H) \land S \subseteq B \land G (S) \underset{˙}{\leq} W) \land z \in B \land \forall x \in S z \underset{˙}{\leq} x) \to \forall w \in T z \underset{˙}{\leq} w$
81	53 10	syl	$⊢ (((K \in HL \land W \in H) \land S \subseteq B \land G (S) \underset{˙}{\leq} W) \land z \in B \land \forall x \in S z \underset{˙}{\leq} x) \to K \in CLat$
82		simp2	$⊢ (((K \in HL \land W \in H) \land S \subseteq B \land G (S) \underset{˙}{\leq} W) \land z \in B \land \forall x \in S z \underset{˙}{\leq} x) \to z \in B$
83	1 2 4	clatleglb	$⊢ (K \in CLat \land z \in B \land T \subseteq B) \to (z \underset{˙}{\leq} G (T) \leftrightarrow \forall w \in T z \underset{˙}{\leq} w)$
84	13 83	mp3an3	$⊢ (K \in CLat \land z \in B) \to (z \underset{˙}{\leq} G (T) \leftrightarrow \forall w \in T z \underset{˙}{\leq} w)$
85	81 82 84	syl2anc	$⊢ (((K \in HL \land W \in H) \land S \subseteq B \land G (S) \underset{˙}{\leq} W) \land z \in B \land \forall x \in S z \underset{˙}{\leq} x) \to (z \underset{˙}{\leq} G (T) \leftrightarrow \forall w \in T z \underset{˙}{\leq} w)$
86	80 85	mpbird	$⊢ (((K \in HL \land W \in H) \land S \subseteq B \land G (S) \underset{˙}{\leq} W) \land z \in B \land \forall x \in S z \underset{˙}{\leq} x) \to z \underset{˙}{\leq} G (T)$
87		simp2	$⊢ ((K \in HL \land W \in H) \land S \subseteq B \land G (S) \underset{˙}{\leq} W) \to S \subseteq B$
88	1 2 4 40 86 11 87 15	isglbd	$⊢ ((K \in HL \land W \in H) \land S \subseteq B \land G (S) \underset{˙}{\leq} W) \to G (S) = G (T)$

Metamath Proof Explorer

Theorem dihglblem2N

Proof