dihmeetcN

Description: Isomorphism H of a lattice meet when the meet is not under the fiducial hyperplane W . (Contributed by NM, 26-Mar-2014) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		dihmeetc.b	$⊢ B = {Base}_{K}$
2		dihmeetc.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		dihmeetc.m	$⊢ \underset{˙}{\land} = meet (K)$
4		dihmeetc.h	$⊢ H = LHyp (K)$
5		dihmeetc.i	$⊢ I = DIsoH (K) (W)$
6		eqid	$⊢ glb (K) = glb (K)$
7		simp1l	$⊢ ((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land \neg (X \underset{˙}{\land} Y) \underset{˙}{\leq} W) \to K \in HL$
8		simp2l	$⊢ ((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land \neg (X \underset{˙}{\land} Y) \underset{˙}{\leq} W) \to X \in B$
9		simp2r	$⊢ ((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land \neg (X \underset{˙}{\land} Y) \underset{˙}{\leq} W) \to Y \in B$
10	6 3 7 8 9	meetval	$⊢ ((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land \neg (X \underset{˙}{\land} Y) \underset{˙}{\leq} W) \to X \underset{˙}{\land} Y = glb (K) (\{X, Y\})$
11	10	fveq2d	$⊢ ((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land \neg (X \underset{˙}{\land} Y) \underset{˙}{\leq} W) \to I (X \underset{˙}{\land} Y) = I (glb (K) (\{X, Y\}))$
12		simp1	$⊢ ((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land \neg (X \underset{˙}{\land} Y) \underset{˙}{\leq} W) \to (K \in HL \land W \in H)$
13		prssi	$⊢ (X \in B \land Y \in B) \to \{X, Y\} \subseteq B$
14	13	3ad2ant2	$⊢ ((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land \neg (X \underset{˙}{\land} Y) \underset{˙}{\leq} W) \to \{X, Y\} \subseteq B$
15		prnzg	$⊢ X \in B \to \{X, Y\} \neq \emptyset$
16	8 15	syl	$⊢ ((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land \neg (X \underset{˙}{\land} Y) \underset{˙}{\leq} W) \to \{X, Y\} \neq \emptyset$
17		simp3	$⊢ ((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land \neg (X \underset{˙}{\land} Y) \underset{˙}{\leq} W) \to \neg (X \underset{˙}{\land} Y) \underset{˙}{\leq} W$
18	10	breq1d	$⊢ ((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land \neg (X \underset{˙}{\land} Y) \underset{˙}{\leq} W) \to ((X \underset{˙}{\land} Y) \underset{˙}{\leq} W \leftrightarrow glb (K) (\{X, Y\}) \underset{˙}{\leq} W)$
19	17 18	mtbid	$⊢ ((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land \neg (X \underset{˙}{\land} Y) \underset{˙}{\leq} W) \to \neg glb (K) (\{X, Y\}) \underset{˙}{\leq} W$
20	1 6 4 5 2	dihglbcN	$⊢ ((K \in HL \land W \in H) \land (\{X, Y\} \subseteq B \land \{X, Y\} \neq \emptyset) \land \neg glb (K) (\{X, Y\}) \underset{˙}{\leq} W) \to I (glb (K) (\{X, Y\})) = ⋂_{x \in \{X, Y\}} I (x)$
21	12 14 16 19 20	syl121anc	$⊢ ((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land \neg (X \underset{˙}{\land} Y) \underset{˙}{\leq} W) \to I (glb (K) (\{X, Y\})) = ⋂_{x \in \{X, Y\}} I (x)$
22		fveq2	$⊢ x = X \to I (x) = I (X)$
23		fveq2	$⊢ x = Y \to I (x) = I (Y)$
24	22 23	iinxprg	$⊢ (X \in B \land Y \in B) \to ⋂_{x \in \{X, Y\}} I (x) = I (X) \cap I (Y)$
25	24	3ad2ant2	$⊢ ((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land \neg (X \underset{˙}{\land} Y) \underset{˙}{\leq} W) \to ⋂_{x \in \{X, Y\}} I (x) = I (X) \cap I (Y)$
26	11 21 25	3eqtrd	$⊢ ((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land \neg (X \underset{˙}{\land} Y) \underset{˙}{\leq} W) \to I (X \underset{˙}{\land} Y) = I (X) \cap I (Y)$

Metamath Proof Explorer

Theorem dihmeetcN

Proof