dihglblem3N

Description: Isomorphism H of a lattice glb. (Contributed by NM, 20-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\}$
	dihglblem.i	$⊢ J = DIsoB (K) (W)$
	dihglblem.ih	$⊢ I = DIsoH (K) (W)$
Assertion	dihglblem3N	$⊢ ((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset) \land G (S) \underset{˙}{\leq} W) \to I (G (T)) = ⋂_{x \in T} I (x)$

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		dihglblem.i	$⊢ J = DIsoB (K) (W)$
8		dihglblem.ih	$⊢ I = DIsoH (K) (W)$
9		simp1	$⊢ ((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset) \land G (S) \underset{˙}{\leq} W) \to (K \in HL \land W \in H)$
10		simp11l	$⊢ (((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset) \land G (S) \underset{˙}{\leq} W) \land u \in B \land v \in S) \to K \in HL$
11	10	hllatd	$⊢ (((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset) \land G (S) \underset{˙}{\leq} W) \land u \in B \land v \in S) \to K \in Lat$
12		simp12l	$⊢ (((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset) \land G (S) \underset{˙}{\leq} W) \land u \in B \land v \in S) \to S \subseteq B$
13		simp3	$⊢ (((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset) \land G (S) \underset{˙}{\leq} W) \land u \in B \land v \in S) \to v \in S$
14	12 13	sseldd	$⊢ (((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset) \land G (S) \underset{˙}{\leq} W) \land u \in B \land v \in S) \to v \in B$
15		simp11r	$⊢ (((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset) \land G (S) \underset{˙}{\leq} W) \land u \in B \land v \in S) \to W \in H$
16	1 5	lhpbase	$⊢ W \in H \to W \in B$
17	15 16	syl	$⊢ (((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset) \land G (S) \underset{˙}{\leq} W) \land u \in B \land v \in S) \to W \in B$
18	1 2 3	latmle2	$⊢ (K \in Lat \land v \in B \land W \in B) \to (v \underset{˙}{\land} W) \underset{˙}{\leq} W$
19	11 14 17 18	syl3anc	$⊢ (((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset) \land G (S) \underset{˙}{\leq} W) \land u \in B \land v \in S) \to (v \underset{˙}{\land} W) \underset{˙}{\leq} W$
20	19	3expia	$⊢ (((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset) \land G (S) \underset{˙}{\leq} W) \land u \in B) \to (v \in S \to (v \underset{˙}{\land} W) \underset{˙}{\leq} W)$
21		breq1	$⊢ u = v \underset{˙}{\land} W \to (u \underset{˙}{\leq} W \leftrightarrow (v \underset{˙}{\land} W) \underset{˙}{\leq} W)$
22	21	biimprcd	$⊢ (v \underset{˙}{\land} W) \underset{˙}{\leq} W \to (u = v \underset{˙}{\land} W \to u \underset{˙}{\leq} W)$
23	20 22	syl6	$⊢ (((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset) \land G (S) \underset{˙}{\leq} W) \land u \in B) \to (v \in S \to (u = v \underset{˙}{\land} W \to u \underset{˙}{\leq} W))$
24	23	rexlimdv	$⊢ (((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset) \land G (S) \underset{˙}{\leq} W) \land u \in B) \to (\exists v \in S u = v \underset{˙}{\land} W \to u \underset{˙}{\leq} W)$
25	24	ss2rabdv	$⊢ ((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset) \land G (S) \underset{˙}{\leq} W) \to \{u \in B \| \exists v \in S u = v \underset{˙}{\land} W\} \subseteq \{u \in B \| u \underset{˙}{\leq} W\}$
26	6 25	eqsstrid	$⊢ ((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset) \land G (S) \underset{˙}{\leq} W) \to T \subseteq \{u \in B \| u \underset{˙}{\leq} W\}$
27	1 2 5 7	dibdmN	$⊢ (K \in HL \land W \in H) \to dom J = \{u \in B \| u \underset{˙}{\leq} W\}$
28	27	3ad2ant1	$⊢ ((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset) \land G (S) \underset{˙}{\leq} W) \to dom J = \{u \in B \| u \underset{˙}{\leq} W\}$
29	26 28	sseqtrrd	$⊢ ((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset) \land G (S) \underset{˙}{\leq} W) \to T \subseteq dom J$
30	1 2 3 4 5 6	dihglblem2aN	$⊢ ((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset)) \to T \neq \emptyset$
31	30	3adant3	$⊢ ((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset) \land G (S) \underset{˙}{\leq} W) \to T \neq \emptyset$
32	4 5 7	dibglbN	$⊢ ((K \in HL \land W \in H) \land (T \subseteq dom J \land T \neq \emptyset)) \to J (G (T)) = ⋂_{x \in T} J (x)$
33	9 29 31 32	syl12anc	$⊢ ((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset) \land G (S) \underset{˙}{\leq} W) \to J (G (T)) = ⋂_{x \in T} J (x)$
34	1 2 3 4 5 6	dihglblem2N	$⊢ ((K \in HL \land W \in H) \land S \subseteq B \land G (S) \underset{˙}{\leq} W) \to G (S) = G (T)$
35	34	3adant2r	$⊢ ((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset) \land G (S) \underset{˙}{\leq} W) \to G (S) = G (T)$
36	35	fveq2d	$⊢ ((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset) \land G (S) \underset{˙}{\leq} W) \to J (G (S)) = J (G (T))$
37		simpl1	$⊢ (((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset) \land G (S) \underset{˙}{\leq} W) \land x \in T) \to (K \in HL \land W \in H)$
38	26	sselda	$⊢ (((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset) \land G (S) \underset{˙}{\leq} W) \land x \in T) \to x \in \{u \in B \| u \underset{˙}{\leq} W\}$
39		breq1	$⊢ u = x \to (u \underset{˙}{\leq} W \leftrightarrow x \underset{˙}{\leq} W)$
40	39	elrab	$⊢ x \in \{u \in B \| u \underset{˙}{\leq} W\} \leftrightarrow (x \in B \land x \underset{˙}{\leq} W)$
41	38 40	sylib	$⊢ (((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset) \land G (S) \underset{˙}{\leq} W) \land x \in T) \to (x \in B \land x \underset{˙}{\leq} W)$
42	1 2 5 8 7	dihvalb	$⊢ ((K \in HL \land W \in H) \land (x \in B \land x \underset{˙}{\leq} W)) \to I (x) = J (x)$
43	37 41 42	syl2anc	$⊢ (((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset) \land G (S) \underset{˙}{\leq} W) \land x \in T) \to I (x) = J (x)$
44	43	iineq2dv	$⊢ ((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset) \land G (S) \underset{˙}{\leq} W) \to ⋂_{x \in T} I (x) = ⋂_{x \in T} J (x)$
45	33 36 44	3eqtr4rd	$⊢ ((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset) \land G (S) \underset{˙}{\leq} W) \to ⋂_{x \in T} I (x) = J (G (S))$
46		simp1l	$⊢ ((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset) \land G (S) \underset{˙}{\leq} W) \to K \in HL$
47		hlclat	$⊢ K \in HL \to K \in CLat$
48	46 47	syl	$⊢ ((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset) \land G (S) \underset{˙}{\leq} W) \to K \in CLat$
49		simp2l	$⊢ ((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset) \land G (S) \underset{˙}{\leq} W) \to S \subseteq B$
50	1 4	clatglbcl	$⊢ (K \in CLat \land S \subseteq B) \to G (S) \in B$
51	48 49 50	syl2anc	$⊢ ((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset) \land G (S) \underset{˙}{\leq} W) \to G (S) \in B$
52		simp3	$⊢ ((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset) \land G (S) \underset{˙}{\leq} W) \to G (S) \underset{˙}{\leq} W$
53	1 2 5 8 7	dihvalb	$⊢ ((K \in HL \land W \in H) \land (G (S) \in B \land G (S) \underset{˙}{\leq} W)) \to I (G (S)) = J (G (S))$
54	9 51 52 53	syl12anc	$⊢ ((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset) \land G (S) \underset{˙}{\leq} W) \to I (G (S)) = J (G (S))$
55	35	fveq2d	$⊢ ((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset) \land G (S) \underset{˙}{\leq} W) \to I (G (S)) = I (G (T))$
56	45 54 55	3eqtr2rd	$⊢ ((K \in HL \land W \in H) \land (S \subseteq B \land S \neq \emptyset) \land G (S) \underset{˙}{\leq} W) \to I (G (T)) = ⋂_{x \in T} I (x)$

Metamath Proof Explorer

Theorem dihglblem3N

Proof