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 
|- .<_ = ( le ` 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 
 |-  .<_ = ( le ` 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 ) )