dihmeetlem14N

Description: Lemma for isomorphism H of a lattice meet. (Contributed by NM, 7-Apr-2014) (New usage is discouraged.)

	Ref	Expression
Hypotheses	dihmeetlem14.b	$⊢ B = {Base}_{K}$
	dihmeetlem14.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	dihmeetlem14.h	$⊢ H = LHyp (K)$
	dihmeetlem14.j	$⊢ \underset{˙}{\lor} = join (K)$
	dihmeetlem14.m	$⊢ \underset{˙}{\land} = meet (K)$
	dihmeetlem14.a	$⊢ A = Atoms (K)$
	dihmeetlem14.u	$⊢ U = DVecH (K) (W)$
	dihmeetlem14.s	$⊢ \underset{˙}{\oplus} = LSSum (U)$
	dihmeetlem14.i	$⊢ I = DIsoH (K) (W)$
Assertion	dihmeetlem14N	$⊢ (((K \in HL \land W \in H) \land Y \in B \land p \in B) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land r \underset{˙}{\leq} Y \land (Y \underset{˙}{\land} p) \underset{˙}{\leq} W)) \to I (Y \underset{˙}{\land} p) \underset{˙}{\oplus} (I (r) \cap I (p)) = I (Y) \cap I (p)$

Step	Hyp	Ref	Expression
1		dihmeetlem14.b	$⊢ B = {Base}_{K}$
2		dihmeetlem14.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		dihmeetlem14.h	$⊢ H = LHyp (K)$
4		dihmeetlem14.j	$⊢ \underset{˙}{\lor} = join (K)$
5		dihmeetlem14.m	$⊢ \underset{˙}{\land} = meet (K)$
6		dihmeetlem14.a	$⊢ A = Atoms (K)$
7		dihmeetlem14.u	$⊢ U = DVecH (K) (W)$
8		dihmeetlem14.s	$⊢ \underset{˙}{\oplus} = LSSum (U)$
9		dihmeetlem14.i	$⊢ I = DIsoH (K) (W)$
10	1 2 3 4 5 6 7 8 9	dihmeetlem12N	$⊢ (((K \in HL \land W \in H) \land Y \in B \land p \in B) \land ((r \in A \land \neg r \underset{˙}{\leq} W) \land r \underset{˙}{\leq} Y \land (Y \underset{˙}{\land} p) \underset{˙}{\leq} W)) \to I (Y \underset{˙}{\land} p) \underset{˙}{\oplus} (I (r) \cap I (p)) = I (Y) \cap I (p)$

Metamath Proof Explorer