Metamath Proof Explorer


Theorem 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 ˙ = K
cdleme43.j ˙ = join K
cdleme43.m ˙ = meet K
cdleme43.a A = Atoms K
cdleme43.h H = LHyp K
cdleme43.u U = P ˙ Q ˙ W
cdleme43.x X = Q ˙ P ˙ W
cdleme43.c C = S ˙ U ˙ Q ˙ P ˙ S ˙ W
cdleme43.f Z = P ˙ Q ˙ C ˙ R ˙ S ˙ W
cdleme43.d D = S ˙ X ˙ P ˙ Q ˙ S ˙ W
cdleme43.g G = Q ˙ P ˙ D ˙ Z ˙ S ˙ W
cdleme43.e E = D ˙ U ˙ Q ˙ P ˙ D ˙ W
cdleme43.v V = Z ˙ S ˙ W
cdleme43.y Y = R ˙ D ˙ W
Assertion cdleme43aN K HL P A Q A G = P ˙ Q ˙ D ˙ V

Proof

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