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 | ⊢ 𝐹 = ( ( 𝑅 ∨ 𝑈 ) ∧ ( 𝑄 ∨ 𝑉 ) ) |
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 | ⊢ 𝐹 = ( ( 𝑅 ∨ 𝑈 ) ∧ ( 𝑄 ∨ 𝑉 ) ) |