cdleme7a

Description: Part of proof of Lemma E in Crawley p. 113. Lemma leading to cdleme7ga and cdleme7 . (Contributed by NM, 7-Jun-2012)

	Ref	Expression
Hypotheses	cdleme4.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	cdleme4.j	$⊢ \underset{˙}{\lor} = join (K)$
	cdleme4.m	$⊢ \underset{˙}{\land} = meet (K)$
	cdleme4.a	$⊢ A = Atoms (K)$
	cdleme4.h	$⊢ H = LHyp (K)$
	cdleme4.u	$⊢ U = (P \underset{˙}{\lor} Q) \underset{˙}{\land} W$
	cdleme4.f	$⊢ F = (S \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} S) \underset{˙}{\land} W))$
	cdleme4.g	$⊢ G = (P \underset{˙}{\lor} Q) \underset{˙}{\land} (F \underset{˙}{\lor} ((R \underset{˙}{\lor} S) \underset{˙}{\land} W))$
	cdleme7.v	$⊢ V = (R \underset{˙}{\lor} S) \underset{˙}{\land} W$
Assertion	cdleme7a	$⊢ G = (P \underset{˙}{\lor} Q) \underset{˙}{\land} (F \underset{˙}{\lor} V)$

Step	Hyp	Ref	Expression
1		cdleme4.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		cdleme4.j	$⊢ \underset{˙}{\lor} = join (K)$
3		cdleme4.m	$⊢ \underset{˙}{\land} = meet (K)$
4		cdleme4.a	$⊢ A = Atoms (K)$
5		cdleme4.h	$⊢ H = LHyp (K)$
6		cdleme4.u	$⊢ U = (P \underset{˙}{\lor} Q) \underset{˙}{\land} W$
7		cdleme4.f	$⊢ F = (S \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} S) \underset{˙}{\land} W))$
8		cdleme4.g	$⊢ G = (P \underset{˙}{\lor} Q) \underset{˙}{\land} (F \underset{˙}{\lor} ((R \underset{˙}{\lor} S) \underset{˙}{\land} W))$
9		cdleme7.v	$⊢ V = (R \underset{˙}{\lor} S) \underset{˙}{\land} W$
10	9	oveq2i	$⊢ F \underset{˙}{\lor} V = F \underset{˙}{\lor} ((R \underset{˙}{\lor} S) \underset{˙}{\land} W)$
11	10	oveq2i	$⊢ (P \underset{˙}{\lor} Q) \underset{˙}{\land} (F \underset{˙}{\lor} V) = (P \underset{˙}{\lor} Q) \underset{˙}{\land} (F \underset{˙}{\lor} ((R \underset{˙}{\lor} S) \underset{˙}{\land} W))$
12	8 11	eqtr4i	$⊢ G = (P \underset{˙}{\lor} Q) \underset{˙}{\land} (F \underset{˙}{\lor} V)$

Metamath Proof Explorer