Description: Lemma for isomorphism H of a lattice meet. (Contributed by NM, 7-Apr-2014) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | dihmeetlem14.b | ⊢ 𝐵 = ( Base ‘ 𝐾 ) | |
| dihmeetlem14.l | ⊢ ≤ = ( le ‘ 𝐾 ) | ||
| dihmeetlem14.h | ⊢ 𝐻 = ( LHyp ‘ 𝐾 ) | ||
| dihmeetlem14.j | ⊢ ∨ = ( join ‘ 𝐾 ) | ||
| dihmeetlem14.m | ⊢ ∧ = ( meet ‘ 𝐾 ) | ||
| dihmeetlem14.a | ⊢ 𝐴 = ( Atoms ‘ 𝐾 ) | ||
| dihmeetlem14.u | ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) | ||
| dihmeetlem14.s | ⊢ ⊕ = ( LSSum ‘ 𝑈 ) | ||
| dihmeetlem14.i | ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) | ||
| Assertion | dihmeetlem14N | ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑌 ∈ 𝐵 ∧ 𝑝 ∈ 𝐵 ) ∧ ( ( 𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊 ) ∧ 𝑟 ≤ 𝑌 ∧ ( 𝑌 ∧ 𝑝 ) ≤ 𝑊 ) ) → ( ( 𝐼 ‘ ( 𝑌 ∧ 𝑝 ) ) ⊕ ( ( 𝐼 ‘ 𝑟 ) ∩ ( 𝐼 ‘ 𝑝 ) ) ) = ( ( 𝐼 ‘ 𝑌 ) ∩ ( 𝐼 ‘ 𝑝 ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | dihmeetlem14.b | ⊢ 𝐵 = ( Base ‘ 𝐾 ) | |
| 2 | dihmeetlem14.l | ⊢ ≤ = ( le ‘ 𝐾 ) | |
| 3 | dihmeetlem14.h | ⊢ 𝐻 = ( LHyp ‘ 𝐾 ) | |
| 4 | dihmeetlem14.j | ⊢ ∨ = ( join ‘ 𝐾 ) | |
| 5 | dihmeetlem14.m | ⊢ ∧ = ( meet ‘ 𝐾 ) | |
| 6 | dihmeetlem14.a | ⊢ 𝐴 = ( Atoms ‘ 𝐾 ) | |
| 7 | dihmeetlem14.u | ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) | |
| 8 | dihmeetlem14.s | ⊢ ⊕ = ( LSSum ‘ 𝑈 ) | |
| 9 | dihmeetlem14.i | ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) | |
| 10 | 1 2 3 4 5 6 7 8 9 | dihmeetlem12N | ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑌 ∈ 𝐵 ∧ 𝑝 ∈ 𝐵 ) ∧ ( ( 𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊 ) ∧ 𝑟 ≤ 𝑌 ∧ ( 𝑌 ∧ 𝑝 ) ≤ 𝑊 ) ) → ( ( 𝐼 ‘ ( 𝑌 ∧ 𝑝 ) ) ⊕ ( ( 𝐼 ‘ 𝑟 ) ∩ ( 𝐼 ‘ 𝑝 ) ) ) = ( ( 𝐼 ‘ 𝑌 ) ∩ ( 𝐼 ‘ 𝑝 ) ) ) |