dihmeet

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

	Ref	Expression
Hypotheses	dihmeet.b	$⊢ B = {Base}_{K}$
	dihmeet.m	$⊢ \underset{˙}{\land} = meet (K)$
	dihmeet.h	$⊢ H = LHyp (K)$
	dihmeet.i	$⊢ I = DIsoH (K) (W)$
Assertion	dihmeet	$⊢ ((K \in HL \land W \in H) \land X \in B \land Y \in B) \to I (X \underset{˙}{\land} Y) = I (X) \cap I (Y)$

Proof

Step	Hyp	Ref	Expression
1		dihmeet.b	$⊢ B = {Base}_{K}$
2		dihmeet.m	$⊢ \underset{˙}{\land} = meet (K)$
3		dihmeet.h	$⊢ H = LHyp (K)$
4		dihmeet.i	$⊢ I = DIsoH (K) (W)$
5		eqid	$⊢ glb (K) = glb (K)$
6		simp1l	$⊢ ((K \in HL \land W \in H) \land X \in B \land Y \in B) \to K \in HL$
7		simp2	$⊢ ((K \in HL \land W \in H) \land X \in B \land Y \in B) \to X \in B$
8		simp3	$⊢ ((K \in HL \land W \in H) \land X \in B \land Y \in B) \to Y \in B$
9	5 2 6 7 8	meetval	$⊢ ((K \in HL \land W \in H) \land X \in B \land Y \in B) \to X \underset{˙}{\land} Y = glb (K) (\{X, Y\})$
10	9	fveq2d	$⊢ ((K \in HL \land W \in H) \land X \in B \land Y \in B) \to I (X \underset{˙}{\land} Y) = I (glb (K) (\{X, Y\}))$
11		simp1	$⊢ ((K \in HL \land W \in H) \land X \in B \land Y \in B) \to (K \in HL \land W \in H)$
12		prssi	$⊢ (X \in B \land Y \in B) \to \{X, Y\} \subseteq B$
13	12	3adant1	$⊢ ((K \in HL \land W \in H) \land X \in B \land Y \in B) \to \{X, Y\} \subseteq B$
14		prnzg	$⊢ X \in B \to \{X, Y\} \neq \emptyset$
15	14	3ad2ant2	$⊢ ((K \in HL \land W \in H) \land X \in B \land Y \in B) \to \{X, Y\} \neq \emptyset$
16	1 5 3 4	dihglb	$⊢ ((K \in HL \land W \in H) \land (\{X, Y\} \subseteq B \land \{X, Y\} \neq \emptyset)) \to I (glb (K) (\{X, Y\})) = ⋂_{x \in \{X, Y\}} I (x)$
17	11 13 15 16	syl12anc	$⊢ ((K \in HL \land W \in H) \land X \in B \land Y \in B) \to I (glb (K) (\{X, Y\})) = ⋂_{x \in \{X, Y\}} I (x)$
18		fveq2	$⊢ x = X \to I (x) = I (X)$
19		fveq2	$⊢ x = Y \to I (x) = I (Y)$
20	18 19	iinxprg	$⊢ (X \in B \land Y \in B) \to ⋂_{x \in \{X, Y\}} I (x) = I (X) \cap I (Y)$
21	20	3adant1	$⊢ ((K \in HL \land W \in H) \land X \in B \land Y \in B) \to ⋂_{x \in \{X, Y\}} I (x) = I (X) \cap I (Y)$
22	10 17 21	3eqtrd	$⊢ ((K \in HL \land W \in H) \land X \in B \land Y \in B) \to I (X \underset{˙}{\land} Y) = I (X) \cap I (Y)$

Metamath Proof Explorer

Theorem dihmeet

Proof