cdleme43aN

Description: Part of proof of Lemma E in Crawley p. 113. TODO: FIX COMMENT p. 115 penultimate line: g(f(r)) = (p v q) ^ (g(s) v v_1). (Contributed by NM, 20-Mar-2013) (New usage is discouraged.)

	Ref	Expression
Hypotheses	cdleme43.b	$⊢ B = {Base}_{K}$
	cdleme43.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	cdleme43.j	$⊢ \underset{˙}{\lor} = join (K)$
	cdleme43.m	$⊢ \underset{˙}{\land} = meet (K)$
	cdleme43.a	$⊢ A = Atoms (K)$
	cdleme43.h	$⊢ H = LHyp (K)$
	cdleme43.u	$⊢ U = (P \underset{˙}{\lor} Q) \underset{˙}{\land} W$
	cdleme43.x	$⊢ X = (Q \underset{˙}{\lor} P) \underset{˙}{\land} W$
	cdleme43.c	$⊢ C = (S \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} S) \underset{˙}{\land} W))$
	cdleme43.f	$⊢ Z = (P \underset{˙}{\lor} Q) \underset{˙}{\land} (C \underset{˙}{\lor} ((R \underset{˙}{\lor} S) \underset{˙}{\land} W))$
	cdleme43.d	$⊢ D = (S \underset{˙}{\lor} X) \underset{˙}{\land} (P \underset{˙}{\lor} ((Q \underset{˙}{\lor} S) \underset{˙}{\land} W))$
	cdleme43.g	$⊢ G = (Q \underset{˙}{\lor} P) \underset{˙}{\land} (D \underset{˙}{\lor} ((Z \underset{˙}{\lor} S) \underset{˙}{\land} W))$
	cdleme43.e	$⊢ E = (D \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} D) \underset{˙}{\land} W))$
	cdleme43.v	$⊢ V = (Z \underset{˙}{\lor} S) \underset{˙}{\land} W$
	cdleme43.y	$⊢ Y = (R \underset{˙}{\lor} D) \underset{˙}{\land} W$
Assertion	cdleme43aN	$⊢ (K \in HL \land P \in A \land Q \in A) \to G = (P \underset{˙}{\lor} Q) \underset{˙}{\land} (D \underset{˙}{\lor} V)$

Proof

Step	Hyp	Ref	Expression
1		cdleme43.b	$⊢ B = {Base}_{K}$
2		cdleme43.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		cdleme43.j	$⊢ \underset{˙}{\lor} = join (K)$
4		cdleme43.m	$⊢ \underset{˙}{\land} = meet (K)$
5		cdleme43.a	$⊢ A = Atoms (K)$
6		cdleme43.h	$⊢ H = LHyp (K)$
7		cdleme43.u	$⊢ U = (P \underset{˙}{\lor} Q) \underset{˙}{\land} W$
8		cdleme43.x	$⊢ X = (Q \underset{˙}{\lor} P) \underset{˙}{\land} W$
9		cdleme43.c	$⊢ C = (S \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} S) \underset{˙}{\land} W))$
10		cdleme43.f	$⊢ Z = (P \underset{˙}{\lor} Q) \underset{˙}{\land} (C \underset{˙}{\lor} ((R \underset{˙}{\lor} S) \underset{˙}{\land} W))$
11		cdleme43.d	$⊢ D = (S \underset{˙}{\lor} X) \underset{˙}{\land} (P \underset{˙}{\lor} ((Q \underset{˙}{\lor} S) \underset{˙}{\land} W))$
12		cdleme43.g	$⊢ G = (Q \underset{˙}{\lor} P) \underset{˙}{\land} (D \underset{˙}{\lor} ((Z \underset{˙}{\lor} S) \underset{˙}{\land} W))$
13		cdleme43.e	$⊢ E = (D \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} D) \underset{˙}{\land} W))$
14		cdleme43.v	$⊢ V = (Z \underset{˙}{\lor} S) \underset{˙}{\land} W$
15		cdleme43.y	$⊢ Y = (R \underset{˙}{\lor} D) \underset{˙}{\land} W$
16	3 5	hlatjcom	$⊢ (K \in HL \land P \in A \land Q \in A) \to P \underset{˙}{\lor} Q = Q \underset{˙}{\lor} P$
17	14	oveq2i	$⊢ D \underset{˙}{\lor} V = D \underset{˙}{\lor} ((Z \underset{˙}{\lor} S) \underset{˙}{\land} W)$
18	17	a1i	$⊢ (K \in HL \land P \in A \land Q \in A) \to D \underset{˙}{\lor} V = D \underset{˙}{\lor} ((Z \underset{˙}{\lor} S) \underset{˙}{\land} W)$
19	16 18	oveq12d	$⊢ (K \in HL \land P \in A \land Q \in A) \to (P \underset{˙}{\lor} Q) \underset{˙}{\land} (D \underset{˙}{\lor} V) = (Q \underset{˙}{\lor} P) \underset{˙}{\land} (D \underset{˙}{\lor} ((Z \underset{˙}{\lor} S) \underset{˙}{\land} W))$
20	12 19	eqtr4id	$⊢ (K \in HL \land P \in A \land Q \in A) \to G = (P \underset{˙}{\lor} Q) \underset{˙}{\land} (D \underset{˙}{\lor} V)$

Metamath Proof Explorer

Theorem cdleme43aN

Proof