dihmeetlem5

Description: Part of proof that isomorphism H is order-preserving . (Contributed by NM, 6-Apr-2014)

	Ref	Expression
Hypotheses	dihmeetlem5.b	$⊢ B = {Base}_{K}$
	dihmeetlem5.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	dihmeetlem5.j	$⊢ \underset{˙}{\lor} = join (K)$
	dihmeetlem5.m	$⊢ \underset{˙}{\land} = meet (K)$
	dihmeetlem5.a	$⊢ A = Atoms (K)$
Assertion	dihmeetlem5	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (Q \in A \land Q \underset{˙}{\leq} X)) \to X \underset{˙}{\land} (Y \underset{˙}{\lor} Q) = (X \underset{˙}{\land} Y) \underset{˙}{\lor} Q$

Step	Hyp	Ref	Expression
1		dihmeetlem5.b	$⊢ B = {Base}_{K}$
2		dihmeetlem5.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		dihmeetlem5.j	$⊢ \underset{˙}{\lor} = join (K)$
4		dihmeetlem5.m	$⊢ \underset{˙}{\land} = meet (K)$
5		dihmeetlem5.a	$⊢ A = Atoms (K)$
6		simpl1	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (Q \in A \land Q \underset{˙}{\leq} X)) \to K \in HL$
7		simprl	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (Q \in A \land Q \underset{˙}{\leq} X)) \to Q \in A$
8		simpl2	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (Q \in A \land Q \underset{˙}{\leq} X)) \to X \in B$
9		simpl3	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (Q \in A \land Q \underset{˙}{\leq} X)) \to Y \in B$
10		simprr	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (Q \in A \land Q \underset{˙}{\leq} X)) \to Q \underset{˙}{\leq} X$
11	1 2 3 4 5	atmod2i1	$⊢ (K \in HL \land (Q \in A \land X \in B \land Y \in B) \land Q \underset{˙}{\leq} X) \to (X \underset{˙}{\land} Y) \underset{˙}{\lor} Q = X \underset{˙}{\land} (Y \underset{˙}{\lor} Q)$
12	6 7 8 9 10 11	syl131anc	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (Q \in A \land Q \underset{˙}{\leq} X)) \to (X \underset{˙}{\land} Y) \underset{˙}{\lor} Q = X \underset{˙}{\land} (Y \underset{˙}{\lor} Q)$
13	12	eqcomd	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (Q \in A \land Q \underset{˙}{\leq} X)) \to X \underset{˙}{\land} (Y \underset{˙}{\lor} Q) = (X \underset{˙}{\land} Y) \underset{˙}{\lor} Q$

Metamath Proof Explorer