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