Description: cdlemg16zz restated for easier studying. TODO: Discard this after everything is figured out. (Contributed by NM, 26-May-2013)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | cdlemg12.l | ⊢ ≤ = ( le ‘ 𝐾 ) | |
| cdlemg12.j | ⊢ ∨ = ( join ‘ 𝐾 ) | ||
| cdlemg12.m | ⊢ ∧ = ( meet ‘ 𝐾 ) | ||
| cdlemg12.a | ⊢ 𝐴 = ( Atoms ‘ 𝐾 ) | ||
| cdlemg12.h | ⊢ 𝐻 = ( LHyp ‘ 𝐾 ) | ||
| cdlemg12.t | ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) | ||
| cdlemg12b.r | ⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) | ||
| Assertion | cdlemg25zz | ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝐺 ∈ 𝑇 ∧ ¬ ( 𝑅 ‘ 𝐹 ) ≤ ( 𝑃 ∨ 𝑧 ) ∧ ¬ ( 𝑅 ‘ 𝐺 ) ≤ ( 𝑃 ∨ 𝑧 ) ) ) → ( ( 𝑃 ∨ ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ) ∧ 𝑊 ) = ( ( 𝑧 ∨ ( 𝐹 ‘ ( 𝐺 ‘ 𝑧 ) ) ) ∧ 𝑊 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cdlemg12.l | ⊢ ≤ = ( le ‘ 𝐾 ) | |
| 2 | cdlemg12.j | ⊢ ∨ = ( join ‘ 𝐾 ) | |
| 3 | cdlemg12.m | ⊢ ∧ = ( meet ‘ 𝐾 ) | |
| 4 | cdlemg12.a | ⊢ 𝐴 = ( Atoms ‘ 𝐾 ) | |
| 5 | cdlemg12.h | ⊢ 𝐻 = ( LHyp ‘ 𝐾 ) | |
| 6 | cdlemg12.t | ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) | |
| 7 | cdlemg12b.r | ⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) | |
| 8 | 1 2 3 4 5 6 7 | cdlemg16zz | ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝐺 ∈ 𝑇 ∧ ¬ ( 𝑅 ‘ 𝐹 ) ≤ ( 𝑃 ∨ 𝑧 ) ∧ ¬ ( 𝑅 ‘ 𝐺 ) ≤ ( 𝑃 ∨ 𝑧 ) ) ) → ( ( 𝑃 ∨ ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ) ∧ 𝑊 ) = ( ( 𝑧 ∨ ( 𝐹 ‘ ( 𝐺 ‘ 𝑧 ) ) ) ∧ 𝑊 ) ) |