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 ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑌 ∈ 𝐵 ∧ 𝑝 ∈ 𝐵 ) ∧ ( ( 𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊 ) ∧ 𝑟 ≤ 𝑌 ∧ ( 𝑌 ∧ 𝑝 ) ≤ 𝑊 ) ) → ( ( 𝐼 ‘ ( 𝑌 ∧ 𝑝 ) ) ⊕ ( ( 𝐼 ‘ 𝑟 ) ∩ ( 𝐼 ‘ 𝑝 ) ) ) = ( ( 𝐼 ‘ 𝑌 ) ∩ ( 𝐼 ‘ 𝑝 ) ) ) |