dihmeetbN

Description: Isomorphism H of a lattice meet when one element is 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	dihmeetbN	$⊢ ((K \in HL \land W \in H) \land X \in B \land (Y \in B \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		simpl1	$⊢ (((K \in HL \land W \in H) \land X \in B \land (Y \in B \land Y \underset{˙}{\leq} W)) \land X \underset{˙}{\leq} W) \to (K \in HL \land W \in H)$
7		simpl2	$⊢ (((K \in HL \land W \in H) \land X \in B \land (Y \in B \land Y \underset{˙}{\leq} W)) \land X \underset{˙}{\leq} W) \to X \in B$
8		simpr	$⊢ (((K \in HL \land W \in H) \land X \in B \land (Y \in B \land Y \underset{˙}{\leq} W)) \land X \underset{˙}{\leq} W) \to X \underset{˙}{\leq} W$
9		simpl3	$⊢ (((K \in HL \land W \in H) \land X \in B \land (Y \in B \land Y \underset{˙}{\leq} W)) \land X \underset{˙}{\leq} W) \to (Y \in B \land Y \underset{˙}{\leq} W)$
10		eqid	$⊢ join (K) = join (K)$
11		eqid	$⊢ Atoms (K) = Atoms (K)$
12		eqid	$⊢ oc (K) (W) = oc (K) (W)$
13		eqid	$⊢ LTrn (K) (W) = LTrn (K) (W)$
14		eqid	$⊢ trL (K) (W) = trL (K) (W)$
15		eqid	$⊢ TEndo (K) (W) = TEndo (K) (W)$
16		eqid	$⊢ (ι g \in LTrn (K) (W) \| g (oc (K) (W)) = q) = (ι g \in LTrn (K) (W) \| g (oc (K) (W)) = q)$
17		eqid	$⊢ (g \in LTrn (K) (W) ⟼ {I ↾}_{B}) = (g \in LTrn (K) (W) ⟼ {I ↾}_{B})$
18	1 3 4 5 2 10 11 12 13 14 15 16 17	dihmeetlem2N	$⊢ ((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \to I (X \underset{˙}{\land} Y) = I (X) \cap I (Y)$
19	6 7 8 9 18	syl121anc	$⊢ (((K \in HL \land W \in H) \land X \in B \land (Y \in B \land Y \underset{˙}{\leq} W)) \land X \underset{˙}{\leq} W) \to I (X \underset{˙}{\land} Y) = I (X) \cap I (Y)$
20		simpl1	$⊢ (((K \in HL \land W \in H) \land X \in B \land (Y \in B \land Y \underset{˙}{\leq} W)) \land \neg X \underset{˙}{\leq} W) \to (K \in HL \land W \in H)$
21		simpl2	$⊢ (((K \in HL \land W \in H) \land X \in B \land (Y \in B \land Y \underset{˙}{\leq} W)) \land \neg X \underset{˙}{\leq} W) \to X \in B$
22		simpr	$⊢ (((K \in HL \land W \in H) \land X \in B \land (Y \in B \land Y \underset{˙}{\leq} W)) \land \neg X \underset{˙}{\leq} W) \to \neg X \underset{˙}{\leq} W$
23		simpl3	$⊢ (((K \in HL \land W \in H) \land X \in B \land (Y \in B \land Y \underset{˙}{\leq} W)) \land \neg X \underset{˙}{\leq} W) \to (Y \in B \land Y \underset{˙}{\leq} W)$
24	1 3 4 5 2 10 11 12 13 14 15 16 17	dihmeetlem1N	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (Y \in B \land Y \underset{˙}{\leq} W)) \to I (X \underset{˙}{\land} Y) = I (X) \cap I (Y)$
25	20 21 22 23 24	syl121anc	$⊢ (((K \in HL \land W \in H) \land X \in B \land (Y \in B \land Y \underset{˙}{\leq} W)) \land \neg X \underset{˙}{\leq} W) \to I (X \underset{˙}{\land} Y) = I (X) \cap I (Y)$
26	19 25	pm2.61dan	$⊢ ((K \in HL \land W \in H) \land X \in B \land (Y \in B \land Y \underset{˙}{\leq} W)) \to I (X \underset{˙}{\land} Y) = I (X) \cap I (Y)$

Metamath Proof Explorer

Theorem dihmeetbN

Proof