dihglb2

Description: Isomorphism H of a lattice glb. (Contributed by NM, 11-Apr-2014)

	Ref	Expression
Hypotheses	dihglb.b	$⊢ B = {Base}_{K}$
	dihglb.g	$⊢ G = glb (K)$
	dihglb.h	$⊢ H = LHyp (K)$
	dihglb.i	$⊢ I = DIsoH (K) (W)$
	dihglb2.u	$⊢ U = DVecH (K) (W)$
	dihglb2.v	$⊢ V = {Base}_{U}$
Assertion	dihglb2	$⊢ ((K \in HL \land W \in H) \land S \subseteq V) \to I (G (\{x \in B \| S \subseteq I (x)\})) = ⋂ \{y \in ran I \| S \subseteq y\}$

Proof

Step	Hyp	Ref	Expression
1		dihglb.b	$⊢ B = {Base}_{K}$
2		dihglb.g	$⊢ G = glb (K)$
3		dihglb.h	$⊢ H = LHyp (K)$
4		dihglb.i	$⊢ I = DIsoH (K) (W)$
5		dihglb2.u	$⊢ U = DVecH (K) (W)$
6		dihglb2.v	$⊢ V = {Base}_{U}$
7		simpl	$⊢ ((K \in HL \land W \in H) \land S \subseteq V) \to (K \in HL \land W \in H)$
8		ssrab2	$⊢ \{x \in B \| S \subseteq I (x)\} \subseteq B$
9	8	a1i	$⊢ ((K \in HL \land W \in H) \land S \subseteq V) \to \{x \in B \| S \subseteq I (x)\} \subseteq B$
10		hlop	$⊢ K \in HL \to K \in OP$
11	10	ad2antrr	$⊢ ((K \in HL \land W \in H) \land S \subseteq V) \to K \in OP$
12		eqid	$⊢ 1. (K) = 1. (K)$
13	1 12	op1cl	$⊢ K \in OP \to 1. (K) \in B$
14	11 13	syl	$⊢ ((K \in HL \land W \in H) \land S \subseteq V) \to 1. (K) \in B$
15		simpr	$⊢ ((K \in HL \land W \in H) \land S \subseteq V) \to S \subseteq V$
16	12 3 4 5 6	dih1	$⊢ (K \in HL \land W \in H) \to I (1. (K)) = V$
17	16	adantr	$⊢ ((K \in HL \land W \in H) \land S \subseteq V) \to I (1. (K)) = V$
18	15 17	sseqtrrd	$⊢ ((K \in HL \land W \in H) \land S \subseteq V) \to S \subseteq I (1. (K))$
19		fveq2	$⊢ x = 1. (K) \to I (x) = I (1. (K))$
20	19	sseq2d	$⊢ x = 1. (K) \to (S \subseteq I (x) \leftrightarrow S \subseteq I (1. (K)))$
21	20	elrab	$⊢ 1. (K) \in \{x \in B \| S \subseteq I (x)\} \leftrightarrow (1. (K) \in B \land S \subseteq I (1. (K)))$
22	14 18 21	sylanbrc	$⊢ ((K \in HL \land W \in H) \land S \subseteq V) \to 1. (K) \in \{x \in B \| S \subseteq I (x)\}$
23	22	ne0d	$⊢ ((K \in HL \land W \in H) \land S \subseteq V) \to \{x \in B \| S \subseteq I (x)\} \neq \emptyset$
24	1 2 3 4	dihglb	$⊢ ((K \in HL \land W \in H) \land (\{x \in B \| S \subseteq I (x)\} \subseteq B \land \{x \in B \| S \subseteq I (x)\} \neq \emptyset)) \to I (G (\{x \in B \| S \subseteq I (x)\})) = ⋂_{z \in \{x \in B \| S \subseteq I (x)\}} I (z)$
25	7 9 23 24	syl12anc	$⊢ ((K \in HL \land W \in H) \land S \subseteq V) \to I (G (\{x \in B \| S \subseteq I (x)\})) = ⋂_{z \in \{x \in B \| S \subseteq I (x)\}} I (z)$
26		fvex	$⊢ I (z) \in V$
27	26	dfiin2	$⊢ ⋂_{z \in \{x \in B \| S \subseteq I (x)\}} I (z) = ⋂ \{y \| \exists z \in \{x \in B \| S \subseteq I (x)\} y = I (z)\}$
28	1 3 4	dihfn	$⊢ (K \in HL \land W \in H) \to I Fn B$
29	28	ad2antrr	$⊢ (((K \in HL \land W \in H) \land S \subseteq V) \land S \subseteq y) \to I Fn B$
30		fvelrnb	$⊢ I Fn B \to (y \in ran I \leftrightarrow \exists z \in B I (z) = y)$
31	29 30	syl	$⊢ (((K \in HL \land W \in H) \land S \subseteq V) \land S \subseteq y) \to (y \in ran I \leftrightarrow \exists z \in B I (z) = y)$
32		eqcom	$⊢ I (z) = y \leftrightarrow y = I (z)$
33	32	rexbii	$⊢ \exists z \in B I (z) = y \leftrightarrow \exists z \in B y = I (z)$
34		df-rex	$⊢ \exists z \in B y = I (z) \leftrightarrow \exists z (z \in B \land y = I (z))$
35	33 34	bitri	$⊢ \exists z \in B I (z) = y \leftrightarrow \exists z (z \in B \land y = I (z))$
36	31 35	bitrdi	$⊢ (((K \in HL \land W \in H) \land S \subseteq V) \land S \subseteq y) \to (y \in ran I \leftrightarrow \exists z (z \in B \land y = I (z)))$
37	36	ex	$⊢ ((K \in HL \land W \in H) \land S \subseteq V) \to (S \subseteq y \to (y \in ran I \leftrightarrow \exists z (z \in B \land y = I (z))))$
38	37	pm5.32rd	$⊢ ((K \in HL \land W \in H) \land S \subseteq V) \to ((y \in ran I \land S \subseteq y) \leftrightarrow (\exists z (z \in B \land y = I (z)) \land S \subseteq y))$
39		df-rex	$⊢ \exists z \in \{x \in B \| S \subseteq I (x)\} y = I (z) \leftrightarrow \exists z (z \in \{x \in B \| S \subseteq I (x)\} \land y = I (z))$
40		fveq2	$⊢ x = z \to I (x) = I (z)$
41	40	sseq2d	$⊢ x = z \to (S \subseteq I (x) \leftrightarrow S \subseteq I (z))$
42	41	elrab	$⊢ z \in \{x \in B \| S \subseteq I (x)\} \leftrightarrow (z \in B \land S \subseteq I (z))$
43	42	anbi1i	$⊢ (z \in \{x \in B \| S \subseteq I (x)\} \land y = I (z)) \leftrightarrow ((z \in B \land S \subseteq I (z)) \land y = I (z))$
44		sseq2	$⊢ y = I (z) \to (S \subseteq y \leftrightarrow S \subseteq I (z))$
45	44	anbi2d	$⊢ y = I (z) \to ((z \in B \land S \subseteq y) \leftrightarrow (z \in B \land S \subseteq I (z)))$
46	45	pm5.32ri	$⊢ ((z \in B \land S \subseteq y) \land y = I (z)) \leftrightarrow ((z \in B \land S \subseteq I (z)) \land y = I (z))$
47		an32	$⊢ ((z \in B \land S \subseteq y) \land y = I (z)) \leftrightarrow ((z \in B \land y = I (z)) \land S \subseteq y)$
48	43 46 47	3bitr2i	$⊢ (z \in \{x \in B \| S \subseteq I (x)\} \land y = I (z)) \leftrightarrow ((z \in B \land y = I (z)) \land S \subseteq y)$
49	48	exbii	$⊢ \exists z (z \in \{x \in B \| S \subseteq I (x)\} \land y = I (z)) \leftrightarrow \exists z ((z \in B \land y = I (z)) \land S \subseteq y)$
50		19.41v	$⊢ \exists z ((z \in B \land y = I (z)) \land S \subseteq y) \leftrightarrow (\exists z (z \in B \land y = I (z)) \land S \subseteq y)$
51	39 49 50	3bitrri	$⊢ (\exists z (z \in B \land y = I (z)) \land S \subseteq y) \leftrightarrow \exists z \in \{x \in B \| S \subseteq I (x)\} y = I (z)$
52	38 51	bitr2di	$⊢ ((K \in HL \land W \in H) \land S \subseteq V) \to (\exists z \in \{x \in B \| S \subseteq I (x)\} y = I (z) \leftrightarrow (y \in ran I \land S \subseteq y))$
53	52	abbidv	$⊢ ((K \in HL \land W \in H) \land S \subseteq V) \to \{y \| \exists z \in \{x \in B \| S \subseteq I (x)\} y = I (z)\} = \{y \| (y \in ran I \land S \subseteq y)\}$
54		df-rab	$⊢ \{y \in ran I \| S \subseteq y\} = \{y \| (y \in ran I \land S \subseteq y)\}$
55	53 54	eqtr4di	$⊢ ((K \in HL \land W \in H) \land S \subseteq V) \to \{y \| \exists z \in \{x \in B \| S \subseteq I (x)\} y = I (z)\} = \{y \in ran I \| S \subseteq y\}$
56	55	inteqd	$⊢ ((K \in HL \land W \in H) \land S \subseteq V) \to ⋂ \{y \| \exists z \in \{x \in B \| S \subseteq I (x)\} y = I (z)\} = ⋂ \{y \in ran I \| S \subseteq y\}$
57	27 56	syl5eq	$⊢ ((K \in HL \land W \in H) \land S \subseteq V) \to ⋂_{z \in \{x \in B \| S \subseteq I (x)\}} I (z) = ⋂ \{y \in ran I \| S \subseteq y\}$
58	25 57	eqtrd	$⊢ ((K \in HL \land W \in H) \land S \subseteq V) \to I (G (\{x \in B \| S \subseteq I (x)\})) = ⋂ \{y \in ran I \| S \subseteq y\}$

Metamath Proof Explorer

Theorem dihglb2

Proof