diameetN

Description: Partial isomorphism A of a lattice meet. (Contributed by NM, 5-Dec-2013) (New usage is discouraged.)

	Ref	Expression
Hypotheses	diam.m	$⊢ \underset{˙}{\land} = meet (K)$
	diam.h	$⊢ H = LHyp (K)$
	diam.i	$⊢ I = DIsoA (K) (W)$
Assertion	diameetN	$⊢ ((K \in HL \land W \in H) \land (X \in dom I \land Y \in dom I)) \to I (X \underset{˙}{\land} Y) = I (X) \cap I (Y)$

Proof

Step	Hyp	Ref	Expression
1		diam.m	$⊢ \underset{˙}{\land} = meet (K)$
2		diam.h	$⊢ H = LHyp (K)$
3		diam.i	$⊢ I = DIsoA (K) (W)$
4		eqid	$⊢ glb (K) = glb (K)$
5		simpll	$⊢ ((K \in HL \land W \in H) \land (X \in dom I \land Y \in dom I)) \to K \in HL$
6		eqid	$⊢ {Base}_{K} = {Base}_{K}$
7	6 2 3	diadmclN	$⊢ ((K \in HL \land W \in H) \land X \in dom I) \to X \in {Base}_{K}$
8	7	adantrr	$⊢ ((K \in HL \land W \in H) \land (X \in dom I \land Y \in dom I)) \to X \in {Base}_{K}$
9	6 2 3	diadmclN	$⊢ ((K \in HL \land W \in H) \land Y \in dom I) \to Y \in {Base}_{K}$
10	9	adantrl	$⊢ ((K \in HL \land W \in H) \land (X \in dom I \land Y \in dom I)) \to Y \in {Base}_{K}$
11	4 1 5 8 10	meetval	$⊢ ((K \in HL \land W \in H) \land (X \in dom I \land Y \in dom I)) \to X \underset{˙}{\land} Y = glb (K) (\{X, Y\})$
12	11	fveq2d	$⊢ ((K \in HL \land W \in H) \land (X \in dom I \land Y \in dom I)) \to I (X \underset{˙}{\land} Y) = I (glb (K) (\{X, Y\}))$
13		simpl	$⊢ ((K \in HL \land W \in H) \land (X \in dom I \land Y \in dom I)) \to (K \in HL \land W \in H)$
14		prssi	$⊢ (X \in dom I \land Y \in dom I) \to \{X, Y\} \subseteq dom I$
15	14	adantl	$⊢ ((K \in HL \land W \in H) \land (X \in dom I \land Y \in dom I)) \to \{X, Y\} \subseteq dom I$
16		prnzg	$⊢ X \in dom I \to \{X, Y\} \neq \emptyset$
17	16	ad2antrl	$⊢ ((K \in HL \land W \in H) \land (X \in dom I \land Y \in dom I)) \to \{X, Y\} \neq \emptyset$
18	4 2 3	diaglbN	$⊢ ((K \in HL \land W \in H) \land (\{X, Y\} \subseteq dom I \land \{X, Y\} \neq \emptyset)) \to I (glb (K) (\{X, Y\})) = ⋂_{x \in \{X, Y\}} I (x)$
19	13 15 17 18	syl12anc	$⊢ ((K \in HL \land W \in H) \land (X \in dom I \land Y \in dom I)) \to I (glb (K) (\{X, Y\})) = ⋂_{x \in \{X, Y\}} I (x)$
20		fveq2	$⊢ x = X \to I (x) = I (X)$
21		fveq2	$⊢ x = Y \to I (x) = I (Y)$
22	20 21	iinxprg	$⊢ (X \in dom I \land Y \in dom I) \to ⋂_{x \in \{X, Y\}} I (x) = I (X) \cap I (Y)$
23	22	adantl	$⊢ ((K \in HL \land W \in H) \land (X \in dom I \land Y \in dom I)) \to ⋂_{x \in \{X, Y\}} I (x) = I (X) \cap I (Y)$
24	12 19 23	3eqtrd	$⊢ ((K \in HL \land W \in H) \land (X \in dom I \land Y \in dom I)) \to I (X \underset{˙}{\land} Y) = I (X) \cap I (Y)$

Metamath Proof Explorer

Theorem diameetN

Proof