Metamath Proof Explorer


Theorem 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 ˙ = K
cdleme4.j ˙ = join K
cdleme4.m ˙ = meet K
cdleme4.a A = Atoms K
cdleme4.h H = LHyp K
cdleme4.u U = P ˙ Q ˙ W
cdleme4.f F = S ˙ U ˙ Q ˙ P ˙ S ˙ W
cdleme4.g G = P ˙ Q ˙ F ˙ R ˙ S ˙ W
cdleme7.v V = R ˙ S ˙ W
Assertion cdleme7a G = P ˙ Q ˙ F ˙ V

Proof

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