cdleme42d

Description: Part of proof of Lemma E in Crawley p. 113. Match ( s .\/ ( x ./\ W ) ) = x . (Contributed by NM, 6-Mar-2013)

	Ref	Expression
Hypotheses	cdleme42.b	$⊢ B = {Base}_{K}$
	cdleme42.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	cdleme42.j	$⊢ \underset{˙}{\lor} = join (K)$
	cdleme42.m	$⊢ \underset{˙}{\land} = meet (K)$
	cdleme42.a	$⊢ A = Atoms (K)$
	cdleme42.h	$⊢ H = LHyp (K)$
	cdleme42.v	$⊢ V = (R \underset{˙}{\lor} S) \underset{˙}{\land} W$
Assertion	cdleme42d	$⊢ ((K \in HL \land W \in H) \land (R \in A \land \neg R \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W)) \to R \underset{˙}{\lor} ((R \underset{˙}{\lor} V) \underset{˙}{\land} W) = R \underset{˙}{\lor} V$

Step	Hyp	Ref	Expression
1		cdleme42.b	$⊢ B = {Base}_{K}$
2		cdleme42.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		cdleme42.j	$⊢ \underset{˙}{\lor} = join (K)$
4		cdleme42.m	$⊢ \underset{˙}{\land} = meet (K)$
5		cdleme42.a	$⊢ A = Atoms (K)$
6		cdleme42.h	$⊢ H = LHyp (K)$
7		cdleme42.v	$⊢ V = (R \underset{˙}{\lor} S) \underset{˙}{\land} W$
8	7	oveq2i	$⊢ R \underset{˙}{\lor} V = R \underset{˙}{\lor} ((R \underset{˙}{\lor} S) \underset{˙}{\land} W)$
9	1 2 3 4 5 6 7	cdleme42a	$⊢ ((K \in HL \land W \in H) \land (R \in A \land \neg R \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W)) \to R \underset{˙}{\lor} S = R \underset{˙}{\lor} V$
10	9	oveq1d	$⊢ ((K \in HL \land W \in H) \land (R \in A \land \neg R \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W)) \to (R \underset{˙}{\lor} S) \underset{˙}{\land} W = (R \underset{˙}{\lor} V) \underset{˙}{\land} W$
11	10	oveq2d	$⊢ ((K \in HL \land W \in H) \land (R \in A \land \neg R \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W)) \to R \underset{˙}{\lor} ((R \underset{˙}{\lor} S) \underset{˙}{\land} W) = R \underset{˙}{\lor} ((R \underset{˙}{\lor} V) \underset{˙}{\land} W)$
12	8 11	eqtr2id	$⊢ ((K \in HL \land W \in H) \land (R \in A \land \neg R \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W)) \to R \underset{˙}{\lor} ((R \underset{˙}{\lor} V) \underset{˙}{\land} W) = R \underset{˙}{\lor} V$

Metamath Proof Explorer