Metamath Proof Explorer


Theorem cdleme3d

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

Ref Expression
Hypotheses cdleme1.l = ( le ‘ 𝐾 )
cdleme1.j = ( join ‘ 𝐾 )
cdleme1.m = ( meet ‘ 𝐾 )
cdleme1.a 𝐴 = ( Atoms ‘ 𝐾 )
cdleme1.h 𝐻 = ( LHyp ‘ 𝐾 )
cdleme1.u 𝑈 = ( ( 𝑃 𝑄 ) 𝑊 )
cdleme1.f 𝐹 = ( ( 𝑅 𝑈 ) ( 𝑄 ( ( 𝑃 𝑅 ) 𝑊 ) ) )
cdleme3.3 𝑉 = ( ( 𝑃 𝑅 ) 𝑊 )
Assertion cdleme3d 𝐹 = ( ( 𝑅 𝑈 ) ( 𝑄 𝑉 ) )

Proof

Step Hyp Ref Expression
1 cdleme1.l = ( le ‘ 𝐾 )
2 cdleme1.j = ( join ‘ 𝐾 )
3 cdleme1.m = ( meet ‘ 𝐾 )
4 cdleme1.a 𝐴 = ( Atoms ‘ 𝐾 )
5 cdleme1.h 𝐻 = ( LHyp ‘ 𝐾 )
6 cdleme1.u 𝑈 = ( ( 𝑃 𝑄 ) 𝑊 )
7 cdleme1.f 𝐹 = ( ( 𝑅 𝑈 ) ( 𝑄 ( ( 𝑃 𝑅 ) 𝑊 ) ) )
8 cdleme3.3 𝑉 = ( ( 𝑃 𝑅 ) 𝑊 )
9 8 oveq2i ( 𝑄 𝑉 ) = ( 𝑄 ( ( 𝑃 𝑅 ) 𝑊 ) )
10 9 oveq2i ( ( 𝑅 𝑈 ) ( 𝑄 𝑉 ) ) = ( ( 𝑅 𝑈 ) ( 𝑄 ( ( 𝑃 𝑅 ) 𝑊 ) ) )
11 7 10 eqtr4i 𝐹 = ( ( 𝑅 𝑈 ) ( 𝑄 𝑉 ) )